Table of Contents
- 1. Égalités immédiates "faciles" par calcul
- 2. Égalité prouvée
- 3. Une autre égalité : l'égalité booléenne
- 4. Égalités contagieuses
LANGAGES ET TRADUCTEURS – Chapitre 3 Jean-François Monin, 2021
ÉgalitéS
Plusieurs manières d'avoir des égalités. Deux grandes catégories :
- égalités immédiates par calcul
- égalités obtenues avec quelque créativité
- utilisation de théorèmes parfois non triviaux
- raisonnement par récurrence
- raisonnement par cas
1 Égalités immédiates "faciles" par calcul
Tactiques associées : reflexivity et cbn
1.1 Par constat de l'identité des deux expressions comparées
reflexivity
1.1.1 Ne comprenant que des constantes
Cst 3 = Cst 3 Amu (Apl (Cst 1) (Cst 2)) (Cst 3) = Amu (Apl (Cst 1) (Cst 2)) (Cst 3)
1.1.2 Comprenant des appels de fonction
transform (Amu (Apl (Cst 1) (Cst 2)) (Cst 3)) = transform (Amu (Apl (Cst 1) (Cst 2)) (Cst 3))
1.1.3 Comprenant des variables inconnues
Cst n = Cst n transform (Amu x (Cst 3)) = transform (Amu x (Cst 3)) f x y (g z) = f x y (g z)
1.2 Par calcul
cbn
1.2.1 Utilisation combinée de 3 mécanismes
eval (Apl (Cst 1) (Cst 2)) = (* def de eval, passage de param, reduction de match *) eval (Cst 1) + eval (Cst 2)
- Par définition
L'égalité "par définition" est très particulière et asymétrique
nom := expression -------------------- nom = expression
- Par réduction d'un match
match Apl (Cst 1) (Cst 2) with | Cst n => n | Apl e1 e2 => eval e1 + eval e2 | Amu e1 e2 => eval e1 * eval e2 end = (* réduction du match *) eval (Cst 1) + eval (Cst 2)
- Appel de fonction : passage du paramètre effectif
(fun a => match a with | Cst n => n | Apl e1 e2 => eval e1 + eval e2 | Amu e1 e2 => eval e1 * eval e2 end) (Apl (Cst 1) (Cst 2)) = (* substitution de a par le paramètre effectif *) match Apl (Cst 1) (Cst 2) with | Cst n => n | Apl e1 e2 => eval e1 + eval e2 | Amu e1 e2 => eval e1 * eval e2 end
1.3 Par combinaison calcul/identité
1.3.1 Ne comprenant que des constantes
transform (Amu (Apl (Cst 1) (Cst 2)) (Cst 3)) = transform (Apl (Amu (Cst 7) (Cst 6)) (Cst 5)) Definition exp_1 := Amu (Apl (Cst 1) (Cst 2)) (Cst 3). transform exp_1 = transform (Apl (Amu (Cst 7) (Cst 6)) (Cst 5))
1.3.2 Avec des variables inconnues
Variable e : Aexp. transform (Amu e (Cst 3)) = transform (Apl e (Cst 5)) Les deux membres se réduisent en Apl (transform e) (Cst 1)
2 Égalité prouvée
- soit par un théorème préalable
- soit par une hypothèse
2.1 Tactique associée : rewrite
2.2 Exemples
Situation : on a mis à notre disposition une égalité ee, exemples
ee : eval (simpl e) = eval e ee : c = rouge ee : (x + y) + z = x + (y + z)
Intuitivement, quelqu'un a auparavant prouvé cette égalité pour nous mais on ne cherche pas à savoir comment. Voire : on se donne cette égalité en hypothèse ; peut-être que quelqu'un pourrait la prouver, on ne sait comment. Eh bien on peut quand même raisonner à partir de là. C'est le principe de Leibniz, le remplacement de quelque chose par quelque chose qui lui est égal.
2.3 Principe de Leibniz
Formellement, soient e1 et e2 deux expressions Coq de même type (On parle ici d'expressions obtenues en appliquant des fonctions sur des arguments, et non pas d'AST d'expressions arithmétiques). Soit P une propriété portant sur ce type.
e1 = e2 P e1
---------------- rew
P e2
Lire : si on peut prouver e1 = e2 d'une part, P e1 d'autre part, on en déduit P e2.
Ce qui amène à une question qu'est-ce qu'une propriété ? –> C'est quelque chose que l'on peut essayer de prouver.
- Exemples déjà vus :
- des égalités
- des égalités quantifiées universellement
- des égalités conditionnées (i.e., des implications)
- On peut avoir autre chose que des égalités
- être pair
Lecture montante : Si on veut prouver P e2, sous l'hypothése e1 = e2, il suffit de prouver P e1.
Remarque : on peut utiliser une égalité dans les deux directions (gauche vers droite ou droite vers gauche) car la seconde direction se déduit de la première.
2.4 Propriétés de l'égalité prouvée
2.4.1 Réflexivité
2.4.2 Transitivité (facile)
e2 = e3 e1 = e2
------------------- rew
e1 = e3
2.4.3 Symétrie (plus subtile)
------- eq_refl
e1 = e2 e1 = e1
------------------- rew
e2 = e1
2.5 Autre définition possible (Leibniz)
En fait, une autre manière (équivalente) de définir l'égalité entre e1 et e2 consiste à dire que toute propriété de e1 est aussi une propriété de e2.
2.5.1 Exercice 1
Montrer que cette égalité est réflexive, symétrique et transitive.
2.5.2 Exercice 2
Montrer que l'égalité de Leibniz et l'égalité définie par eqrefl et rew sont équivalentes.
2.6 À retenir : l'égalité est quelque chose qui se prouve
- en réfléchissant
- en produisant une arbre de preuve
3 Une autre égalité : l'égalité booléenne
L'égalité booléenne entre deux valeurs de type T est définie par un programme prenant ces deux valeurs en argument et rendant une réponse binaire, habituellement notée true ou false.
Quel est le lien entre égalité booléenne et égalité prouvée ? Même si, par exemple sur nat, on peut prouver l'équivalence entre égalité booléenne et égalité prouvée,
Lemma eqiffeqnatb : forall n1 n2, eqnatb n1 n2 = true <-> n1 = n2.
… leurs significations sont différentes.
3.1 Exemples
3.1.1 Égalités
6 = 8 8 = 8 2 + 6 = 6 + 2 fact 2000 + fact 66666 = fact 66666 + fact 2000
–> on peut remplacer (rewrite)
3.1.2 Calculs booléens
eqnatb 6 8 eqnatb 8 8 eqnatb (2+6) (6+2) eqnatb (fact 2000 + fact 66666) (fact 66666 + fact 2000)
–> rien du tout
3.1.3 Calculs booléens avec résultat attendu
eqnatb 6 8 = false eqnatb 8 8 = true eqnatb (2+6) (6+2) = true eqnatb (fact 2000 + fact 66666) (fact 66666 + fact 2000) = true
–> on peut remplacer eqnatb (2+6) (6+2) par true, assez peu intéressant
3.1.4 Avec des variables libres
- eqnatb (fact 2000 + n) (n + fact 2000) –> le calcul ne donne aucune information exploitable
- fact 2000 + n = n + fact 2000 –> on peut encore remplacer
3.1.5 Avec des variables quantifiées
- ∀n, eqnatb (fact 2000 + n) (n + fact 2000) –> n'a pas de sens
- ∀n, fact 2000 + n = n + fact 2000 –> sensé, facile à démontrer, utilisable
3.2 La Vérité n'est pas sacrée
vert / rouge à la place de true false, ça marche aussi bien.
3.3 Intérêt et limites du calcul booléen
On peut faire du calcul booléen (des tables de vérité) en vue de prouver des égalités en nombre fini. Le calcul booléen est hors jeu sur des ensembles infinis. Et difficilement jouable sur des grands ensembles.
3.4 Moralité
Ce qui signifie "être vrai" est moins clair que cela en a l'air. Par contre "être prouvé" l'est beaucoup plus : c'est être la conclusion d'un arbre de preuve
Le calcul booléen peut être utile à autre chose : garantir qu'il n'y a PAS d'arbre de preuve. En effet une proposition P démontrable (par un arbre de preuve) respecte les tables de vérité au sens suivant : quelles que soient les valeurs de vérité assignées à chacune des propositions atomiques de P, la valeur de vérité de P est "vrai".
Démonstration (esquisse) : par récurrence structurelle sur l'arbre de preuve de P.
Là encore, le nom donné aux valeurs de vérité n'a pas d'importance, elles servent en quelque sorte à exprimer un invariant associé aux règles de déduction, invariant que l'on peut aussi bien interpréter comme la propagation d'un coloriage.
4 Égalités contagieuses
Lemma contagion1 : Rouge = Vert -> true = false. Lemma contagion2 : Rouge = Vert -> 3 = 8. Lemma contagion3 : Rouge = Vert -> ∀n1 n2 : nat, n1 = n2. Lemma contagion4 : Rouge = Vert -> Rouge = Orange.
On pose
f := fun c => match x with Rouge => 3 | Vert => 8 | _ => 8 end
Le but
3 = 8
se réduit à
f Rouge = f Vert
Et on termine par rewrite; reflexivity ou fapply.