(* 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. intros H p q. apply H;split;assumption. Qed. Lemma and_e_left : P /\ Q -> P. Proof. intro H;destruct H;assumption. Qed. Lemma and_e_right : P /\ Q -> Q. Proof. intro H;destruct H;assumption. Qed. Lemma and_sym : P /\ Q -> Q /\ P. Proof. intro H;destruct H;split;assumption. Qed. Lemma and_assoc : P /\ (Q /\ R) -> (P /\ Q) /\ R. Proof. intro H;destruct H. destruct H0. split;trivial. split;trivial. Qed. Lemma imp_to_and : (P -> Q -> R) -> P /\ Q -> R. Proof. intros H H0;destruct H0;apply H;assumption. 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. intros H p;apply H;left;assumption. Qed. Theorem Th4: (P \/ Q -> R) -> (P -> R) /\ (Q -> R). Proof. intro H;split. intro p;apply H;left;assumption. intro p;apply H;right;assumption. Qed. Theorem Th5: (Q -> R) /\ (P -> R) -> (P \/ Q -> R). Proof. intros H H0;destruct H. destruct H0. apply H1;trivial. apply H;trivial. Qed. Theorem Th6 : (P -> R) \/ (Q -> R) -> (P /\ Q) -> R. Proof. intros H H0;destruct H;destruct H0. apply H;trivial. apply H;trivial. 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. intros p Np. destruct Np;trivial. Qed. Theorem demorgan_1 : ~(P \/ Q) -> ~P /\ ~Q. Proof. intros H;split. intro p;destruct H;left;trivial. intro q;destruct H;right;trivial. Qed. Theorem demorgan_2 : ~P /\ ~Q -> ~(P \/ Q). Proof. intros H H0. destruct H. destruct H0. destruct H;trivial. destruct H1;trivial. Qed. Theorem demorgan_3 : ~P \/ ~Q -> ~(P /\ Q). Proof. intros H H0. destruct H0. destruct H. destruct H;trivial. destruct H;trivial. Qed. (* sur le tiers exclu *) Theorem exm_to_peirce : (P \/ ~P) -> (((P -> Q)->P)->P). Proof. intros D H. destruct D;trivial. apply H. intro p; destruct H0;trivial. Qed. (* en revanche, impossible de prouver (en logique intuitionniste) *) Theorem bad_peirce_to_exm : (((P -> Q)-> P)->P) -> P \/~P. Proof. intro H. 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. intro H;destruct (classic P). right;apply H;trivial. left;trivial. Qed. Theorem and_imp_disj : (P /\ Q -> R) -> (P -> R) \/ (Q -> R). Proof. intros H;destruct (classic P). right;intro q;apply H. split;trivial. left;intro p;destruct H0;trivial. Qed. Theorem Peirce : ((P -> Q) -> P) -> P. Proof. intro H. destruct (classic P);trivial. apply H. intro p;destruct H0;trivial. Qed. End classic.