É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 On réécrit via hyp. La commande pour affirmer que le but à démontrer est exactement l'hypothèse nommée hyp est On conclut par 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.

example (x y z : ℝ) (h : x = y) (h' : y = z) : x = z :=

  On réécrit via h,

x y z : ℝ,
h : x = y,
h' : y = z
⊢ x = z

x y z : ℝ,
h : x = y,
h' : y = z
⊢ y = z

  On conclut par h',

x y z : ℝ,
h : x = y,
h' : y = z
⊢ y = z

Gagné ! 🎉

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 On réécrit via ← à la place de On réécrit via pour réécrire ainsi « de la droite vers la gauche ». On peut ainsi donner une variante de la démonstration précédente.

example (x y z : ℝ) (h : x = y) (h' : y = z) : x = z :=

  On réécrit via ← h',

x y z : ℝ,
h : x = y,
h' : y = z
⊢ x = z

x y z : ℝ,
h : x = y,
h' : y = z
⊢ x = y

  On conclut par h,

x y z : ℝ,
h : x = y,
h' : y = z
⊢ x = y

Gagné ! 🎉

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.

example (a b c : ℝ) : (a * b) * c = b * (a * c) :=

  On réécrit via mul_comm a b,

a b c : ℝ
⊢ a * b * c = b * (a * c)

a b c : ℝ
⊢ b * a * c = b * (a * c)

  On conclut par mul_assoc b a c,

a b c : ℝ
⊢ b * a * c = b * (a * c)

Gagné ! 🎉

On peut aussi réécrire dans une hypothèse du contexte local, en utilisant par exemple On réécrit via mul_comm a b dans 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.

example (a b c d : ℝ) (hyp : c = d*a + b) (hyp' : b = a*d) : c = 2*a*d :=

  On réécrit via hyp' dans 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

  On réécrit via mul_comm d a dans 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

  On réécrit via ← two_mul (a*d) dans 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

  On réécrit via ← mul_assoc 2 a d dans 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

  On conclut par hyp,

a b c d : ℝ,
hyp' : b = a * d,
hyp : c = 2 * a * d
⊢ c = 2 * a * d

Gagné ! 🎉

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.

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 { On réécrit via 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 { On conclut par mul_assoc b a c },

a b c : ℝ
⊢ a * b * c = b * (a * c)

Gagné ! 🎉

Bien sûr il est hors de question de passer le semestre à invoquer explicitement l'associativité ou la commutativité. On utilisera la commande On calcule pour démontrer des égalités n'utilisant que ce genre de propriétés, ou bien On calcule dans 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 On calcule.

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 { On conclut par 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 { On réécrit via 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 { On calcule },

a b c d : ℝ,
hyp : c = d * a + b,
hyp' : b = a * d
⊢ c = 2 * a * d

Gagné ! 🎉

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.