Download Le Coq` Art (V8)

150
CHAPITRE 6. LOGIQUE DE TOUS LES JOURS
right; right; left; assumption.
Qed.
En fait, un seul appel à auto suffit pour chacun de ces théorèmes (voir chapitre 8).
Les règles d’élimination sont utiles pour utiliser des hypothèses qui sont des
disjonctions ou des conjonctions. La tactique elim est particulièrement adaptée pour ce besoin : elle applique la règle d’élimination associée au connecteur
logique.
Voici un exemple utilisant l’élimination et l’introduction de conjonctions :
Theorem and_commutes : ∀ A B:Prop, A∧B→B∧A.
Proof.
intros A B H.
...
H : A∧B
============================
B∧A
elim H.
...
H : A∧B
============================
A→B→B∧A
split; assumption.
Qed.
Après l’étape “ elim H ”, le nouveau but contient deux implications dont les
prémisses sont les deux termes de la conjonction. L’exemple similaire pour la
disjonction doit être traité avec soin. Malgré l’apparente symétrie de l’énoncé,
la preuve doit commencer par une élimination de l’hypothèse A ∨ B, suivie
d’une introduction par left (resp. right) ; en effet, commencer par une règle
d’introduction sur la conclusion B ∨ A obligerait à choisir dès le départ entre
left et right et casserait la symétrie du but à prouver.
Theorem or_commutes : ∀ A B:Prop, A∨B→B∨A.
Proof.
intros A B H.
...
H : A∨B
============================
B∨A
elim H.
...
============================
A→B∨A
subgoal 2 is: