Section Exercices.
Variable A B C : Prop.


(* Démontrez les formules suivantes (en les notant comme des théorèmes, comme
dans les exemples précédents. (il vous faut donc donner un nom à ces théorèmes)).

Il vous est très vivement recommandé de faire votre preuve au brouillon avant de
commencer en Coq !

Ex0 : Bases/Rappels

- A -> A
- A -> B -> A
- (A/\B)-> B
- (A\/B)-> C -> (A/\C)\/(B/\C)
- (A/\~A) -> B

Ex 1 : Commutativité et associativité (si pas déjà fait) 

- (A/\B) -> (B/\A)
- (A\/B) -> (B\/A)
- ((A/\B)/\ C) -> (A/\(B/\ C))
- (plus difficile : ) (A\/(B\/ C)) -> ((A\/B)\/ C)

Ex 2 : De Morgan

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

Ex 3 : Contraposée
- (A->B) -> (~B->~A)

Ex 4 : Distributivité (Difficile)
- (A \/ (B/\C)) <-> ( (A\/B) /\ (A\/C))

Ex 5 (difficile) :
- ~~(A\/~A)
Indice : regardez la dernière preuve du cours sur la déduction naturelle, et
remplacez le raisonnement par l’absurde par une introduction de la négation.

Ex 6.

(A/\~B) -> ~(A->B).
~ A \/ B -> A -> B.
~(A\/B) -> ~A /\ ~B.
A /\ (B \/ C) <-> A /\ B \/ A /\ C.
A \/ False <-> A.
(A -> ~A) -> ~A.
(~A -> A) -> ~~A.

*)

End Exercices