(* logique propositionnelle *) (* 1 - cas intuitionniste *) (* 1.1 - preuves sans composition de tactiques *) Section intuitionistic. Variables P Q R: Prop. Lemma and_to_imp: ((P /\ Q) -> R) -> (P -> (Q -> R)). Proof. intro H. intro p. intro q. apply H. split. assumption. assumption. Qed. Lemma and_e_left: (P /\ Q) -> P. Proof. intro H. destruct H as (p, q). assumption. Qed. Lemma and_e_right: (P /\ Q) -> Q. Proof. intro H. destruct H as (p, q). assumption. Qed. Lemma and_sym: (P /\ Q) -> (Q /\ P). Proof. intro H. destruct H as (p, q). split. assumption. assumption. Qed. Lemma and_assoc: (P /\ (Q /\ R)) -> ((P /\ Q) /\ R). Proof. intro H1. destruct H1 as (p, H2). destruct H2 as (q, r). split. split. assumption. assumption. assumption. Qed. Lemma imp_to_and: (P -> (Q -> R)) -> ((P /\ Q) -> R). Proof. intro H1. intro H2. destruct H2 as (p, q). apply H1. assumption. assumption. Qed. Theorem Th3: ((P \/ Q) -> R) -> (P -> R). Proof. intro H. intro 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 q. apply H. right. assumption. Qed. Theorem Th5: ((Q -> R) /\ (P -> R)) -> ((P \/ Q) -> R). Proof. intro H1. destruct H1 as (H2, H3). intro H4. destruct H4 as [p | q]. apply H3. assumption. apply H2. assumption. Qed. Theorem Th6: ((P -> R) \/ (Q -> R)) -> ((P /\ Q) -> R). Proof. intro H1. intro H2. destruct H2 as (p, q). destruct H1 as [H3 | H4]. apply H3. assumption. apply H4. assumption. Qed. Theorem False_Q: False -> Q. Proof. intro ff. destruct ff. Qed. Theorem Absurd: P -> ((~ P) -> Q). Proof. intro p. intro np. destruct np. assumption. Qed. Theorem demorgan_1: (~ (P \/ Q)) -> ((~ P) /\ (~ Q)). Proof. intro H. split. intro p. destruct H. left. assumption. intro q. destruct H. right. assumption. Qed. Theorem demorgan_2: ((~ P) /\ (~ Q)) -> (~ (P \/ Q)). Proof. intro H1. destruct H1 as (np, nq). intro H2. destruct H2 as [p| q]. destruct np. assumption. destruct nq. assumption. Qed. Theorem demorgan_3: ((~ P) \/ (~ Q)) -> (~ (P /\ Q)). Proof. intro H1. intro H2. destruct H2 as (p, q). destruct H1 as [np | nq]. destruct np. assumption. destruct nq. assumption. Qed. Theorem exm_to_peirce: (P \/ (~ P)) -> (((P -> Q) -> P) -> P). intro H1. intro H2. destruct H1 as [p | np]. assumption. apply H2. intro p. destruct np. assumption. Qed. End intuitionistic. (* 1.2 - preuves avec composition de tactiques *) (* Section intuitionistic_comp. Variables P Q R: Prop. 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 H1; destruct H1 as (p, H2); destruct H2; split; [split | ]; assumption. Qed. Lemma imp_to_and: (P -> Q -> R) -> P /\ Q -> R. Proof. intros H1 H2; destruct H2; apply H1; assumption. Qed. 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; apply H; [left | right]; assumption. Qed. Theorem Th5: (Q -> R) /\ (P -> R) -> P \/ Q -> R. Proof. intro H1; destruct H1 as (H2, H3); intro H4; destruct H4; [apply H3 | apply H2]; assumption. Qed. Theorem Th6: (P -> R) \/ (Q -> R) -> P /\ Q -> R. Proof. intros H1 H2; destruct H2; destruct H1 as [H3 | H4]; [apply H3 | apply H4]; assumption. Qed. Theorem False_Q: False -> Q. Proof. intro ff; destruct ff. Qed. Theorem Absurd: P -> ~ P -> Q. Proof. intros p np; destruct np; assumption. Qed. Theorem demorgan_1: ~ (P \/ Q) -> ~ P /\ ~ Q. Proof. intro H; split; intro; destruct H; [left | right]; assumption. Qed. Theorem demorgan_2: ~ P /\ ~ Q -> ~ (P \/ Q). Proof. intro H1; destruct H1 as (np, nq); intro H2; destruct H2; [destruct np | destruct nq]; assumption. Qed. Theorem demorgan_3: ~ P \/ ~ Q -> ~ (P /\ Q). Proof. intros H1 H2; destruct H2; destruct H1 as [np | nq]; [destruct np | destruct nq]; assumption. Qed. Theorem exm_to_peirce: P \/ ~ P -> ((P -> Q) -> P) -> P. Proof. intros H1 H2; destruct H1 as [p | np]; [ | apply H2; intro; destruct np]; assumption. Qed. End intuitionistic_comp. *) (* 2 - cas classique *) (* 2.1 - preuves sans composition de tactiques *) Section classic. Require Import Classical. Variables P Q R: Prop. Theorem demorgan_4: (~ (P /\ Q)) -> ((~ P) \/ (~ Q)). Proof. intro H. destruct (classic P) as [p | np]. right. intro q. destruct H. split. assumption. assumption. left. assumption. (* ~ P *) Qed. Theorem imp_disj: (P -> Q) -> ((~ P) \/ Q). Proof. intro H. destruct (classic P) as [p | np]. right. apply H. assumption. left. assumption. (* ~ P *) Qed. Theorem and_imp_disj: ((P /\ Q) -> R) -> ((P -> R) \/ (Q -> R)). Proof. intro H. destruct (classic P) as [p | np]. right. intro q. apply H. split. assumption. assumption. left. intro p. destruct np. assumption. Qed. Theorem Peirce: ((P -> Q) -> P) -> P. intro H. destruct (classic P) as [p | np]. assumption. apply H. intro p. destruct np. assumption. Qed. End classic. (* 2.2 - preuves avec composition de tactiques *) (* Section classic_comp. Require Import Classical. Variables P Q R: Prop. Theorem demorgan_4: ~ (P /\ Q) -> ~ P \/ ~ Q. Proof. intro H; destruct (classic P); [ right; intro; destruct H; split | left]; assumption. Qed. Theorem imp_disj: (P -> Q) -> ~ P \/ Q. Proof. intro H; destruct (classic P); [ right; apply H | left]; assumption. Qed. Theorem and_imp_disj: (P /\ Q -> R) -> (P -> R) \/ (Q -> R). Proof. intro H; destruct (classic P) as [p | np]; [ right; intro; apply H; split | left; intro; destruct np]; assumption. Qed. Theorem Peirce: ((P -> Q) -> P) -> P. Proof. intro H; destruct (classic P) as [p | np]; [ | apply H; intro; destruct np]; assumption. Qed. End classic_comp. *)