Module PropositionalLogic. (* The following lines are black magic; just keep them here *) Require Import Classical. Axiom dep_extensionality: forall (A: Type) (B: A -> Type) (f g : forall x: A, B x), (forall x, f x = g x) -> f = g. Implicit Arguments dep_extensionality. Lemma extensionality: forall (A B: Type) (f g : A -> B), (forall x, f x = g x) -> f = g. Proof. intros; apply dep_extensionality; auto. Qed. Implicit Arguments extensionality. Tactic Notation "extensionality" := (match goal with | |- ?f = ?g => apply (extensionality f g); intro end). Tactic Notation "extensionality" ident(x) := (match goal with | |- ?f = ?g => apply (extensionality f g); intro x end). Require Import Omega. Axiom prop_ext: ClassicalFacts.prop_extensionality. Implicit Arguments prop_ext. Tactic Notation "spec" hyp(H) := match type of H with ?a -> _ => let H1 := fresh in (assert (H1: a); [|generalize (H H1); clear H H1; intro H]) end. Tactic Notation "spec" hyp(H) constr(a) := (generalize (H a); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) := (generalize (H a b); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) := (generalize (H a b c); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) := (generalize (H a b c d); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) constr(e) := (generalize (H a b c d e); clear H; intro H). Tactic Notation "LEM" constr(P) := (destruct (classic (P))). (* end #include section *) Parameter p q r: Prop. Definition ExampleFormula: Prop := (((~ p) /\ q) -> ( True /\ ( q \/ (~ r)))). Section RainExample. Hypothesis H1: p /\ ~ q -> r. Hypothesis H2: ~ r. Hypothesis H3: p. Lemma ThereWereTaxis: q. Proof. admit. Qed. End RainExample. Section Example. Hypothesis H_1: p /\ q. Hypothesis H_2: r. Lemma Ex: q /\ r. Proof. split. destruct H_1. apply H0. apply H_2. Qed. End Example. Section Example2. Hypothesis H: p /\ (q \/ r). Lemma Ex2: (p /\ q) \/ (p /\ r). Proof. destruct H. destruct H1. left. split. apply H0. apply H1. right. split. apply H0. apply H1. Qed. End Example2. End PropositionalLogic.