Section Propositional_Logic. Variables P Q R S: Prop. Theorem P_or_False : P \/ False -> P. Proof. intro H; elim H; intro H0. assumption. elim H0. Qed. Theorem and_idempotent_1 : P -> P /\ P. intro p; split; assumption. Qed. Theorem and_idempotent_2 : P/\P -> P. intro H; elim H; intros; assumption. Qed. Theorem and_or_dist : (P\/Q)/\R -> (P/\R)\/(Q/\R). Proof. intros ([H1|H2], H3). left;split;trivial. right;split;trivial. Qed. Theorem absurd : P -> ~P -> Q. Proof. intros p H; elim H; assumption. Qed. Theorem demorgan1 : P /\ Q -> ~(~P \/ ~Q). Proof. intros (p,q); red; intros [p'|q']. elim p'; trivial. elim q'; trivial. Qed. Theorem demorgan2 : ~(P \/ Q) -> ~P /\ ~Q. Proof. intro H; split ; red ; intro H0. elim H; left ; trivial. elim H; right; trivial. Qed. Theorem demorgan3 : P \/ Q -> ~(~P /\ ~Q). Proof. intros [H | H]; red ; intros (p',q'). elim p'; trivial. elim q'; trivial. Qed. End Propositional_Logic.