Download Le Coq` Art (V8)

4.6. COMPOSITION DE TACTIQUES
89
Composition simple
La composition simple permet d’enchaîner l’application de deux tactiques
sans s’arréter aux sous-buts intermédiaires. Plus précisément, soient tac et tac’
deux tactiques ; alors la tactique composée tac ;tac’ , appliquée à un but g
consiste à appliquer tac à g, puis tac’ à chacun des sous-buts ainsi engendrés. En
cas d’échec de tac ou tac’, la tactique composée échoue entièrement. Considérons
par exemple le début de preuve ci-dessous :
Theorem then_example : P→Q→(P→Q→R)→R.
Proof.
intros p q H.
1 subgoal
...
p:P
q:Q
H : P→Q→R
============================
R
On devine que la tactique “ apply H ” va engendrer deux sous-buts, d’énoncés respectifs P et Q. Chacun de ces nouveaux sous-buts se résout par assumption.
La composition de tactiques “ apply H; assumption ” permet donc de résoudre
ce but en une seule interaction.
apply H; assumption.
Qed.
Il est possible d’enchaîner ainsi plusieurs tactiques, sous la forme
tac 1 ;tac 2 ;...;tac n .
Il faut remarquer que l’utilisation de cette composition demande à l’utilisateur suffisamment d’intuition pour prévoir quels sous-buts seront engendrés à
chaque étape de cette composition et quelle tactique sera appropriée pour résoudre tous ces nouveaux sous-buts. Cette intuition vient avec la pratique de
Coq. Ceci est à rapprocher des jeux — tels les échecs par exemple —, où le
joueur averti intègre dans ses tactiques les réponses prévisibles de l’adversaire.
L’exemple suivant montre une composition de 5 tactiques :
Theorem triple_impl_one_shot : (((P→Q)→Q)→Q)→P→Q.
Proof.
intros H p; apply H; intro H0; apply H0; assumption.
Qed.
Composition généralisée
La composition simple tac ;tac’ présuppose que la tactique tac’ peut s’appliquer à tous les sous-buts crées par tac. Il peut cependant arriver que chacun
de ces nouveaux sous-buts requière une tactique différente des autres.