Section Modus_Ponens.
Variable A B C : Prop.
(* dans le premier tuto, nous avons vu comment démontrer
des formules de la forme A->B (prouver B sous hypothèse A).

Nous n’avons pas encore vu comment utiliser une hypothèse
de la forme A->B.

La règle qui permet cela s’appelle historiquement 
le 'Modus Ponens' (nous l’appelons aussi 'élimination 
de la flèche', ou 'application'). Elle peut être résumée
ainsi : si je connais A->B, alors je peux prouver A pour
en conclure B :

|- A-> B      |- A
--------------------(-> elim)
    |- B

En Coq, la forme de la règle est à peine différente,
on pourrait l’écrire ainsi :

Γ, A->B |- A
------------(apply)
Γ, A->B |- B

On pourrait la lire ainsi : 
'si je sais prouver A, et que A->B est dans mes 
hypothèses, alors je sais aussi prouver B.'
Remarquez que l’on conserve toutes les hypothèses:
    cela permet de s’en resservir si nécessaire.
    (dans la règle (->elim), si l’on veut
    réutiliser plusieurs fois l’implication,
    il faut reproduire la preuve, ce n’est pas
    ce qui est le plus efficace…)

La règle apply permet donc de modifier l’objectif
en cours : si l’objectif est B, et qu’une hypothèse 
de la forme A->B est présente, alors on peut dire à Coq
qu’il nous suffit de montrer A. L’objectif qui était B 
devient A, comme l’illustre l’exemple ci-dessous.

*)

Theorem modus_ponens : (A -> B) -> (A -> B).
Proof.
intros Hab Ha. 
(* c’est un raccourci pour introduire plusieurs hypothèses d’un coup 
   Hab est A->B et Ha est A.
*) 
apply Hab. 
(*il suffit donc maintenant de prouver A*)
assumption.
Qed.

(*Dans l’application de cette règle, il est possible
d’avoir plusieurs alternatives. On peut avoir un objectif C,
et deux hypothèses A->C et B->C. Dans ce cas, comment savoir
laquelle utiliser ?*)

Theorem modus_ponens_affaibli:B->((C->A)->((B->A)->A)).
Proof.
intros Hb Hca Hba.
(*Regardez les hypothèses à ce stade.
Il est clair que l’on doit utiliser Hba, car on doit
prouver A, et que Hba:B->A et que Hb: B sont dans les hypothèses.
Mais on a tout à fait le droit d’utiliser d’abord Hca,
essayez 'apply Hca' ci-dessous au lieu de Hba.
Vous serez bloqué, car il est impossible de prouver C.*)
apply Hba.
assumption.
Qed.


Theorem affaiblissement : A-> ((B->A)->((C->A)->A)).
Proof.
intros Ha Hba Hca.
(*ici on peut utiliser H0 ou H1, mais alors
on devrait ensuite prouver soit B soit C, ce qui
est impossible ici. Essayez en effet d’entrer
'apply H0' ou 'apply H1' ci-dessous, vous serez bloqué…
La solution est de n’utiliser aucune des hypothèses
implicatives, mais directement Ha:A*)

assumption.

(*d’ailleurs, au lieu de 'assumption', vous pouvez utiliser 'apply Ha', ça
fonctionne également*)

Qed.



(*En général, ca dépend du contexte.
 Dans les exemples simples de ces tutos, les
hypothèses à utiliser sont toujours évidentes. Dans
des preuves plus sophistiquées, plus longues, on peut
avoir plein d’hypothèses utilisables : il est alors
d’autant plus important de faire la preuve au brouillon 
avant de se lancer en Coq ! 
*)