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.
*)

End Exercices