Égalité et calculs
La forme de raisonnement la plus simple est le calcul basé sur la notion d'égalité. Dire que deux objets mathématiques $A$ et $B$ sont égaux signifie que, dans tout énoncé où intervient $A$, on peut le remplacer par $B$ sans changer la véracité de l'énoncé. Ce remplacement est appelé « réécriture de l'énoncé ».
Dans Lean la commande pour réécrire le but à l'aide d'une hypothèse d'égalité
hyp est rw hyp (rw est l'abréviation de rewrite).
La commande pour affirmer que le but à démontrer est exactement l'hypothèse
nommée hyp est exact hyp. On verra plus loin que ces deux commandes
peuvent utiliser des expressions plus compliquées que le simple nom d'une hypothèse
du contexte local.
Pour l'instant, on se fixe l'objectif modeste de démontrer la transitivité de l'égalité entre nombres réels.
Soit $x$, $y$ et $z$ trois nombres réels. On suppose que $x = y$ et $y = z$. Alors $x = z$.
example (x y z : ℝ) (h : x = y) (h' : y = z) : x = z :=
rw h,
x y z : ℝ,
h : x = y,
h' : y = z
⊢ x = z
x y z : ℝ,
h : x = y,
h' : y = z
⊢ y = z
exact h',
x y z : ℝ,
h : x = y,
h' : y = z
⊢ y = z
no goals
La relation d'égalité est symétrique, il est donc possible de réécrire
en remplaçant $B$ par $A$ si $A = B$. Dans Lean on utilise rw ←
à la place de rw pour réécrire ainsi « de la droite vers la gauche ».
On peut ainsi donner une variante de la démonstration précédente.
Soit $x$, $y$ et $z$ trois nombres réels. On suppose que $x = y$ et $y = z$. Alors $x = z$.
example (x y z : ℝ) (h : x = y) (h' : y = z) : x = z :=
rw ← h',
x y z : ℝ,
h : x = y,
h' : y = z
⊢ x = z
x y z : ℝ,
h : x = y,
h' : y = z
⊢ x = y
exact h,
x y z : ℝ,
h : x = y,
h' : y = z
⊢ x = y
no goals
Les égalités peuvent provenir de théorèmes ou propriétés générales. Par exemple la multiplication des nombres réels est associative et commutative. Habituellement ces propriétés sont utilisées implicitement mais, simplement pour ce chapitre, nous allons expliciter leur utilisation.
Dans Lean, l'associativité de la multiplication pour trois nombres a, b et c est
l'énoncé mul_assoc a b c qui affirme l'égalité a * b * c = a * (b * c).
Il y a plusieurs choses à observer ici. D'abord mul_assoc est vu comme une fonction
qui prend en argument trois nombres séparés par des espaces et renvoie une démonstration
d'une égalité. Ensuite la multiplication est notée * qui est plus facile à taper
que × et la multiplication implicite (sans symbole) n'est pas autorisée. Enfin
Lean considère que le symbole de multiplication est associatif à gauche donc, en l'absence
de parenthèse, a * b * c est interprété comme (a * b) * c, ce qui fait que l'égalité
affirmée n'est pas évidente.
La commutativité de la multiplication fait l'objet du lemme mul_comm. Plus précisément,
mul_comm a b est une démonstration de l'égalité a * b = b * a.
Soit $a$, $b$ et $c$ des nombres réels. On a $(a × b) × c = b × (a × c)$
example (a b c : ℝ) : (a * b) * c = b * (a * c) :=
rw mul_comm a b,
a b c : ℝ
⊢ a * b * c = b * (a * c)
a b c : ℝ
⊢ b * a * c = b * (a * c)
exact mul_assoc b a c,
a b c : ℝ
⊢ b * a * c = b * (a * c)
no goals
On peut aussi réécrire dans une hypothèse du contexte local, en utilisant
par exemple rw mul_comm a b at hyp, pour remplacer a*b par b*a
dans l'hypothèse hyp.
Dans l'exemple suivant on utilise aussi le fait two_mul a : 2*a = a + a.
Soit $a$, $b$, $c$ et $d$ des nombres réels. On suppose que $c = da + b$ et $b = ad$. Alors $c = 2ad$.
example (a b c d : ℝ) (hyp : c = d*a + b) (hyp' : b = a*d) : c = 2*a*d :=
rw hyp' at hyp,
a b c d : ℝ,
hyp : c = d * a + b,
hyp' : b = a * d
⊢ c = 2 * a * d
a b c d : ℝ,
hyp' : b = a * d,
hyp : c = d * a + a * d
⊢ c = 2 * a * d
rw mul_comm d a at hyp,
a b c d : ℝ,
hyp' : b = a * d,
hyp : c = d * a + a * d
⊢ c = 2 * a * d
a b c d : ℝ,
hyp' : b = a * d,
hyp : c = a * d + a * d
⊢ c = 2 * a * d
rw ← two_mul (a*d) at hyp,
a b c d : ℝ,
hyp' : b = a * d,
hyp : c = a * d + a * d
⊢ c = 2 * a * d
a b c d : ℝ,
hyp' : b = a * d,
hyp : c = 2 * (a * d)
⊢ c = 2 * a * d
rw ← mul_assoc 2 a d at hyp,
a b c d : ℝ,
hyp' : b = a * d,
hyp : c = 2 * (a * d)
⊢ c = 2 * a * d
a b c d : ℝ,
hyp' : b = a * d,
hyp : c = 2 * a * d
⊢ c = 2 * a * d
exact hyp,
a b c d : ℝ,
hyp' : b = a * d,
hyp : c = 2 * a * d
⊢ c = 2 * a * d
no goals
Les démonstrations précédentes ne ressemblent pas tellement à des calculs sur papier, même en admettant qu'on veuille expliciter les applications de l'associativité et la commutativité de la multiplication. En effet les calculs sur papier tirent implicitement parti de la transitivité de l'égalité. Par exemple, dans le cas de $(ab)c = b(ac)$, la démonstration est vraiment en trois temps : on montre que $(ab)c = (ba)c$, puis que $(ba)c=b(ac)$ et on utilise la transitivité pour conclure de ces deux égalités que $(ab)c = b(ac)$. La façon de cacher cet appel à la transitivité sur papier est d'écrire :
\[ \begin{align*} (ab)c &= (ba)c \\ &= b(ac). \end{align*} \]
L'exemple suivant montre comment faire de même avec Lean à l'aide de la commande
calc. La conversion du fichier Lean en page web n'est pas vraiment adaptée à ces blocs
de calcul. Dans l'éditeur on pourrait placer le curseur entre les accolades pour voir
que le but à démontrer est (a * b) * c = (b * a) * c puis
(b * a) * c = b * a * c.
Soit $a$, $b$ et $c$ des nombres réels. On a $(a × b) × c = b × (a × c)$
example (a b c : ℝ) : (a * b) * c = b * (a * c) :=
calc
a b c : ℝ
⊢ a * b * c = b * (a * c)
a b c : ℝ
⊢ a * b * c = b * (a * c)
(a * b) * c = (b * a) * c : by { rw mul_comm a b }
a b c : ℝ
⊢ a * b * c = b * (a * c)
a b c : ℝ
⊢ a * b * c = b * (a * c)
... = b * (a * c) : by { exact mul_assoc b a c },
a b c : ℝ
⊢ a * b * c = b * (a * c)
no goals
Bien sûr il est hors de question de passer le semestre à invoquer explicitement
l'associativité ou la commutativité. On utilisera la commande compute pour démontrer
des égalités n'utilisant que ce genre de propriétés, ou bien compute at hyp pour simplifier
une hypothèse hyp à l'aide de ces propriétés.
Revoici un des exemples précédents traité à l'aide de calc et compute.
Soit $a$, $b$, $c$ et $d$ des nombres réels. On suppose que $c = da + b$ et $b = ad$. Alors $c = 2ad$.
example (a b c d : ℝ) (hyp : c = d*a + b) (hyp' : b = a*d) : c = 2*a*d :=
calc
a b c d : ℝ,
hyp : c = d * a + b,
hyp' : b = a * d
⊢ c = 2 * a * d
a b c d : ℝ,
hyp : c = d * a + b,
hyp' : b = a * d
⊢ c = 2 * a * d
c = d*a + b : by { exact hyp }
a b c d : ℝ,
hyp : c = d * a + b,
hyp' : b = a * d
⊢ c = 2 * a * d
a b c d : ℝ,
hyp : c = d * a + b,
hyp' : b = a * d
⊢ c = 2 * a * d
... = d*a + a*d : by { rw hyp' }
a b c d : ℝ,
hyp : c = d * a + b,
hyp' : b = a * d
⊢ c = 2 * a * d
a b c d : ℝ,
hyp : c = d * a + b,
hyp' : b = a * d
⊢ c = 2 * a * d
... = 2*a*d : by { compute },
a b c d : ℝ,
hyp : c = d * a + b,
hyp' : b = a * d
⊢ c = 2 * a * d
no goals
La démonstration ci-dessus est bien la version raisonnable qu'on utilisera par la suite,
et il est inutile de chercher à retenir les noms des énoncés mul_assoc, mul_comm et
two_mul.
Mais, en plus de faire découvrir le logiciel, les versions l'ayant précédée mettent en
lumière les règles et mécanismes utilisés implicitement dans les calculs de ce genre.
La prise de conscience de l'existence de règles et mécanismes plus ou moins implicites
est un objectif central de ce cours.
Le cours continue avec le chapitre 2.