(* Les règles de la déduction naturelle doivent être ajoutées à Coq. *)
Require Import Naturelle.

(* Ouverture d\u2019une section *)
Section CalculPropositionnel.

(* Déclaration de variables propositionnelles *)
Variable A B C E Y R : Prop.

(*Exerice 1*)

Theorem Thm00 : A /\ B -> B /\ A.
I_imp H.
I_et.
E_et_d A.
Hyp H.
E_et_g B.
Hyp H.
Qed.

Theorem Thm_1 : ((A \/ B) -> C) -> (B -> C).
I_imp H.
I_imp H2.
E_imp (A \/ B).
Hyp H.
I_ou_d.
Hyp H2.
Qed.

Theorem Thm_2 : A -> ~~A.
I_imp H.
I_non H2.
I_antiT A.
Hyp H.
Hyp H2.
Qed.

Theorem Thm_3 : (A -> B) -> (~B -> ~A).
I_imp H.
I_imp H2.
I_non H3.
I_antiT B.
E_imp A.
Hyp H.
Hyp H3.
Hyp H2.
Qed.

Theorem Thm_4 : ~~A -> A.
I_imp H.
absurde H2.
I_antiT (~A).
Hyp H2.
Hyp H.
Qed.

Theorem Thm_5 : (~B -> ~A) -> (A -> B).

I_imp H.
I_imp H2.
absurde H3.
I_antiT (A).
Hyp H2.
E_imp (~B).
trivial.
trivial.
Qed.

Theorem Thm_6 : ((E -> (Y \/ R)) /\ (Y -> R)) -> (~R -> ~E).
intros.
I_non H1.
I_antiT (R).
E_ou Y R.
E_imp E.
E_et_g (Y -> R).
Hyp H.
Hyp H1.
E_et_d (E -> Y \/ R).
Hyp H.
I_imp H2.
tauto.
tauto.
Qed.

(*Exerice 2*)

Theorem Coq_E_imp : ((A -> B) /\ A) -> B.
intros.
destruct H as (H1,H2).
tauto.
Qed.

Theorem Coq_E_et_g : (A /\ B) -> A.
intros.
destruct H as (H1,H2).
trivial.
Qed.

Theorem Coq_E_ou : ((A \/ B) /\ (A -> C) /\ (B -> C)) -> C.
intros.
destruct H as (H1,H2).
destruct H2 as (H2,H3).
destruct H1 as [H4 | H5].
E_imp A.
Hyp H2.
Hyp H4.
E_imp B.
trivial.
trivial.
Qed.

Theorem Thm_7 : ((E -> (Y \/ R)) /\ (Y -> R)) -> (~R -> ~E).
intros.
destruct H as (H1,H2).
tauto. (* à détailler *)
Qed. 

End CalculPropositionnel.