Section Negation.
Variable A B:Prop.

(*Regardons maintenant les règles liées à la négation. "non A" en Coq s’écrit ~A.

Rappelez-vous qu’on déduction naturelle, pour introduire ~A, on a la règle suivante :

   A|- _|_
   --------- (not-i)
   |- ~A
   
(La contradiction en Coq s’écrit simplement 'false'.)


En Coq, cette règle ne change pas. En effet, essayez d’utiliser 'intro' sur la preuve suivante :*)
Lemma Neg_test : ~A.
Proof.
intro H.
Abort.

(* ATTENTION : Si vous utilisez "intros" (avec S), dans le cas où il y a plusieurs hypothèses,
  Coq ne va pas forcément décomposer ~A du premier coup. Par exemple, sur jsCoq (éditeur en ligne)
  la formule A -> (B -> ~C) ne génèrera que les hypothèses pour A et B si vous utilisez "intros".
  Soit il vous faudra retaper "intro" pour décomposer ~C, soit (c’est mieux), vous pouvez nommer 
  toutes les hypothèses avec "intros Ha Hb Hc", et vous vous retrouverez bien avec la formule "False" en but,
  et A,B,C dans les hypothèses.
  

En revanche, pour utiliser une hypothèse de la forme ~A, c’est un peu différent.

On a vu dans le cours que la formule ~A pouvait être vue comme un raccourci pour la formule A -> False.
En Coq c’est exactement ça. Et donc si on peut utiliser une hypothèse ~A pour montrer False (il faudra ensuite prouver A).

Essayons :
*)

Lemma Neg_test_2 : ~A -> A -> False.
Proof.
intros Hna Ha.
(*On a deux hypothèses, et on doit montrer False.
Ici je peux donc me rappeler que Hna est en fait une implication A->False,
et je peux alors utiliser la règle 'apply' (voir section "Modus Ponens"). *)
apply Hna.
(*Et je dois en effet prouver A. C’est bon ! *)
assumption.
Qed.

(*Remarquez qu’on a plus besoin d’une règle spécifique pour éliminer la négation,
car en déduction naturelle, c’était :

|- A     |- ~A
---------------
|- False


En Coq, on utilise simplement la règle 'apply' de l’implication, et ça fait exactement la même chose. 

 ATTENTION !!!
 
Coq est basé sur la logique intuitionniste, c’est-à-dire que le raisonnement par l’absure est IMPOSSIBLE.
En particulier, vous ne pouvez pas démontrer A\/~A en Coq, ni ~~A -> A. (essayez si vous voulez !).


En revanche, la règle qui nous permettait de prouver n’importe quelle formule à
partir d’une contradiction reste valide. Rappelez-vous :

|- _|_
--------abs
|- A

En Coq, cette règle s’apple 'contradiction'. Elle marche légèrement
différemment : quel que soit votre but, si vous avez 'False' dans vos
hypothèses, alors vous pouvez prouver votre but immédiatement.

Cela termine une preuve, c’est un peu comme un nouvel axiome qu’on pourrait
écrire comme ceci :

-----------contradiction
False |- A

Voilà :
)*

Lemma Contra_test : False -> A.
Proof.
intro Hf.
contradiction.
Qed.



Exercices : Démontrez les formules suivantes :

A -> ~~A.  
~~A -> ~~~~A.
A/\~A -> B.

*)

End Negation.