(* logique propositionnelle *) Parameters P Q R : Prop. (* exercices sur la conjonction tactique d'introduction : split tactique d'elimination : elim t, avec t : A /\ B *) (* prouver les théorèmes suivants :*) Lemma and_to_imp: (P /\ Q -> R) -> (P -> (Q -> R)). Proof. Qed. Lemma and_e_left : P /\ Q -> P. Proof. Qed. Lemma and_e_right : P /\ Q -> Q. Proof. Qed. Lemma and_sym : P /\ Q -> Q /\ P. Proof. Qed. Lemma and_assoc : P /\ (Q /\ R) -> (P /\ Q) /\ R. Proof. Qed. Lemma imp_to_and : (P -> Q -> R) -> P /\ Q -> R. Proof. Qed. (* exercices sur la disjonction tactiques d'introduction left right tactique d'elimination : elim t, avec t : A \/ B *) (* completer les preuves suivantes *) Theorem Th3 : (P \/ Q -> R) -> P -> R. Proof. Qed. Theorem Th4: (P \/ Q -> R) -> (P -> R) /\ (Q -> R). Proof. Qed. Theorem Th5: (Q -> R) /\ (P -> R) -> (P \/ Q -> R). Proof. Qed. Theorem Th6 : (P -> R) \/ (Q -> R) -> (P /\ Q) -> R. Proof. Qed. (* Le faux et la négation (intuitionniste) *) (* tactique d'elimination du faux elim t, avec t : False *) Theorem False_P : False -> P. Proof. intros ff. elim ff. Qed. (* tactique d'élimination de la négation : elim t, avec t : ~A (engendre une Obligation de preuve sur A). introduction de la négation : intro H. ou unfold not ou red *) (* finir les preuves suivantes *) Theorem Absurd: P -> ~ P -> Q. Proof. Qed. Theorem demorgan_1 : ~(P \/ Q) -> ~P /\ ~Q. Proof. Qed. Theorem demorgan_2 : ~P /\ ~Q -> ~(P \/ Q). Proof. Qed. Theorem demorgan_3 : ~P \/ ~Q -> ~(P /\ Q). Proof. Qed. (* sur le tiers exclu *) Theorem exm_to_peirce : (P \/ ~P) -> (((P -> Q)->P)->P). Qed. (* en revanche, impossible de prouver (en logique intuitionniste) *) Theorem bad_peirce_to_exm : (((P -> Q)-> P)->P) -> P \/~P. Proof. Abort. (* Mais on pourra prouver (plus tard) en passant à l'ordre supérieur Theorem peirce_to_exm : (forall A B:Prop, (((A -> B)->A)->A)) -> (forall A:Prop,A \/~A). *) (* Logique classique *) Section classic. (* On importe un module permettant le raisonnement Classique *) Require Import Classical. (* A toute étape d'une preuve, la tactique "destruct (classic A)" où A est une proposition quelconque (celle qui vous arrange) engendre une preuve par cas : deux buts sont créés, l'un avec une hypothèse d'énoncé A, l'autre supposant ~A. Exemple : *) Theorem demorgan_4 : ~(P /\ Q) -> ~P \/ ~Q. Proof. intro H. destruct (classic P). right; intro H1; destruct H;auto. left;trivial. Qed. (* finir les preuves suivantes *) Theorem imp_disj : (P -> Q) -> ~P \/ Q. Proof. Qed. Theorem and_imp_disj : (P /\ Q -> R) -> (P -> R) \/ (Q -> R). Qed. Theorem Peirce : ((P -> Q) -> P) -> P. Qed. End classic.