120 lines
1.6 KiB
Coq
Executable file
120 lines
1.6 KiB
Coq
Executable file
(* 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.
|
|
|