From aa31e628a62eb0692e614277278e60cd311f72b9 Mon Sep 17 00:00:00 2001
From: William Ball <williampi103@gmail.com>
Date: Sun, 31 Mar 2024 20:08:27 -0700
Subject: [PATCH] more

---
 Logic.v       | 965 ++++++++++++++++++++++++++++++++++++++++++++++++++
 Makefile      |   2 +-
 Makefile.conf |   4 +-
 Tactics.v     |   8 -
 4 files changed, 968 insertions(+), 11 deletions(-)
 create mode 100644 Logic.v

diff --git a/Logic.v b/Logic.v
new file mode 100644
index 0000000..6c24b70
--- /dev/null
+++ b/Logic.v
@@ -0,0 +1,965 @@
+Require Nat.
+From LF Require Export Tactics.
+
+Definition injective {A B} (f : A -> B) :=
+  forall x y : A, f x = f y -> x = y.
+
+Lemma succ_inj : injective S.
+Proof.
+  intros n m H.
+  injection H as H1.
+  apply H1.
+Qed.
+
+Lemma and_example :
+  forall n m : nat, n = 0 /\ m = 0 -> n + m = 0.
+Proof.
+  intros n m [Hn Hm].
+  rewrite Hn. rewrite Hm.
+  reflexivity.
+Qed.
+
+Example and_exercise :
+  forall n m : nat, n + m = 0 -> n = 0 /\ m = 0.
+Proof.
+  intros n m H.
+  split.
+  - destruct n as [ | n'].
+    + reflexivity.
+    + discriminate.
+  - destruct m as [ | m'].
+    + reflexivity.
+    + rewrite add_comm in H.
+      discriminate.
+Qed.    
+    
+Lemma and_example2 :
+  forall n m : nat, n + m = 0 -> n * m = 0.
+Proof.
+  intros n m H.
+  apply and_exercise in H.
+  destruct H as [Hn Hm].
+  rewrite Hn.
+  reflexivity.
+Qed.
+
+Lemma proj1 : forall P Q : Prop,
+    P /\ Q -> P.
+Proof.
+  intros P Q [HP _].
+  apply HP.
+Qed.
+
+Lemma proj2 : forall P Q : Prop,
+    P /\ Q -> Q.
+Proof.
+  intros P Q [_ HQ].
+  apply HQ.
+Qed.
+
+Theorem and_comm : forall P Q : Prop,
+    P /\ Q -> Q /\ P.
+Proof.
+  intros P Q [HP HQ].
+  split.
+  - apply HQ.
+  - apply HP.
+Qed.
+
+Theorem and_assoc : forall P Q R : Prop,
+    P /\ (Q /\ R) -> (P /\ Q) /\ R.
+Proof.
+  intros P Q R [HP [HQ HR]].
+  split.
+  - split.
+    + apply HP.
+    + apply HQ.
+  - apply HR.
+Qed.
+
+Theorem mult_n_0 : forall n,
+    n * 0 = 0.
+Proof.
+  intros n.
+  rewrite mul_comm.
+  reflexivity.
+Qed.
+  
+Lemma factor_is_0:
+  forall n m : nat, n = 0 \/ m = 0 -> n * m = 0.
+Proof.
+  intros n m [Hn | Hm].
+  - rewrite Hn. reflexivity.
+  - rewrite Hm.
+    rewrite <- mult_n_O.
+    reflexivity.
+Qed.
+
+Lemma zero_or_succ :
+  forall n : nat,
+    n = 0 \/ n = S (pred n).
+Proof.
+  intros [ | n'].
+  - left. reflexivity.
+  - right. reflexivity.
+Qed.
+
+Lemma zero_product_property :
+  forall n m, n * m = 0 -> n = 0 \/ m = 0.
+Proof.
+  intros [ | n'] m H.
+  - left. reflexivity.
+  - destruct m as [ | m'].
+    + right. reflexivity.
+    + discriminate.
+Qed.
+
+Theorem or_commut : forall P Q : Prop,
+    P \/ Q -> Q \/ P.
+Proof.
+  intros P Q [HP | HQ].
+  - right. apply HP.
+  - left. apply HQ.
+Qed.
+
+Theorem ex_falso_quodlibet : forall (P : Prop),
+    False -> P.
+Proof.
+  intros P contra.
+  destruct contra.
+Qed.
+
+Theorem not_implies_our_not : forall (P : Prop),
+    ~ P -> (forall (Q: Prop), P -> Q).
+Proof.
+  intros P H Q HP.
+  apply H in HP.
+  destruct HP.
+Qed.
+
+Theorem zero_not_one : 0 <> 1.
+Proof.
+  intros contra.
+  discriminate.
+Qed.
+
+Theorem not_False : ~ False.
+Proof.
+  intros contra.
+  apply contra.
+Qed.
+
+Theorem contradiction_implies_anything : forall P Q : Prop,
+    (P /\ ~P) -> Q.
+Proof.
+  intros P Q [HP HNP].
+  apply HNP in HP.
+  destruct HP.
+Qed.
+
+Theorem double_neg : forall P : Prop,
+    P -> ~~P.
+Proof.
+  intros P H.
+  intros HN.
+  apply HN.
+  apply H.
+Qed.
+
+Theorem contrapositive : forall (P Q : Prop),
+    (P -> Q) -> (~Q -> ~P).
+Proof.
+  intros P Q H.
+  intros HNQ HP.
+  apply HNQ.
+  apply H.
+  apply HP.
+Qed.
+
+Theorem not_both_true_and_false : forall P : Prop,
+    ~ (P /\ ~P).
+Proof.
+  intros P [HP HNP].
+  apply HNP. apply HP.
+Qed.
+
+Theorem de_morgan_not_or : forall (P Q : Prop),
+    ~ (P \/ Q) -> ~P /\ ~Q.
+Proof.
+  intros P Q H.
+  split.
+  - intros HP.
+    apply H.
+    left. apply HP.
+  - intros HQ.
+    apply H.
+    right. apply HQ.
+Qed.
+
+Theorem not_true_is_false : forall b : bool,
+    b <> true -> b = false.
+Proof.
+  intros b H.
+  destruct b eqn:HE.
+  - exfalso.
+    apply H.
+    reflexivity.
+  - reflexivity.
+Qed.
+
+Theorem iff_sym : forall P Q : Prop,
+    (P <-> Q) -> (Q <-> P).
+Proof.
+  intros P Q [HPQ HQP].
+  split.
+  - apply HQP.
+  - apply HPQ.
+Qed.
+
+Lemma not_true_iff_false : forall b,
+    b <> true <-> b = false.
+Proof.
+  intros b.
+  split.
+  - apply not_true_is_false.
+  - intros H.
+    rewrite H.
+    intros H'.
+    discriminate.
+Qed.
+
+Theorem or_distributes_over_and : forall P Q R : Prop,
+    P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R).
+Proof.
+  intros P Q R.
+  split.
+  - intros [HP | [HQ HR]].
+    + split.
+      * left. apply HP.
+      * left. apply HP.
+    + split.
+      * right. apply HQ.
+      * right. apply HR.
+  - intros [[HP | HQ] [HP' | HR]].
+    + left. apply HP.
+    + left. apply HP.
+    + left. apply HP'.
+    + right. split.
+      * apply HQ.
+      * apply HR.
+Qed.
+
+From Coq Require Import Setoids.Setoid.
+
+Lemma mul_eq_0 : forall n m, n * m = 0 <-> n = 0 \/ m = 0.
+Proof.
+  split.
+  - apply zero_product_property.
+  - apply factor_is_0.
+Qed.
+
+Theorem or_assoc :
+  forall P Q R : Prop, P \/ (Q \/ R) <-> (P \/ Q) \/ R.
+Proof.
+  intros P Q R. split.
+  - intros [H | [H | H]].
+    + left. left. apply H.
+    + left. right. apply H.
+    + right. apply H.
+  - intros [[H | H] | H].
+    + left. apply H.
+    + right. left. apply H.
+    + right. right. apply H.
+Qed.
+
+Lemma mul_eq_0_ternary :
+  forall n m p, n * m * p = 0 <-> n = 0 \/ m = 0 \/ p = 0.
+Proof.
+  intros n m p.
+  rewrite mul_eq_0.
+  rewrite mul_eq_0.
+  rewrite or_assoc.
+  reflexivity.
+Qed.
+
+Definition Even x := exists n : nat, x = double n.
+
+Lemma four_is_Even : Even 4.
+Proof.
+  unfold Even.
+  exists 2.
+  reflexivity.
+Qed.
+
+Example exists_example_2 : forall n,
+    (exists m, n = 4 + m) ->
+    (exists o, n = 2 + o).
+Proof.
+  intros n [m Hm].
+  exists (2 + m).
+  apply Hm.
+Qed.
+
+Theorem dist_not_exists : forall (X : Type) (P : X -> Prop),
+    (forall x, P x) -> ~(exists x, ~ P x).
+Proof.
+  intros X P H [x E].
+  apply E.
+  apply H.
+Qed.
+
+Theorem dist_exists_or : forall (X : Type) (P Q : X -> Prop),
+    (exists x, P x \/ Q x) <-> (exists x, P x) \/ (exists x, Q x).
+Proof.
+  intros X P Q.
+  split.
+  - intros [x [HP | HQ]].
+    + left.
+      exists x.
+      apply HP.
+    + right.
+      exists x.
+      apply HQ.
+  - intros [[x HP] | [x HQ]].
+    + exists x.
+      left. apply HP.
+    + exists x.
+      right. apply HQ.
+Qed.
+
+Theorem leb_plus_exists : forall n m,
+    n <=? m = true -> exists x, m = n + x.
+Proof.
+  induction n as [ | n' Hn'].
+  - intros m H.
+    simpl.
+    exists m.
+    reflexivity.
+  - intros m H.
+    simpl.
+    destruct m as [ | m'].
+    + simpl in H.
+      discriminate H.
+    + simpl in H.
+      apply Hn' in H.
+      destruct H as [x H].
+      exists x.
+      rewrite H.
+      reflexivity.
+Qed.
+
+Theorem plus_exists_leb : forall n m, (exists x, m = n + x) -> n <=? m = true.
+Proof.
+  induction n as [ | n' IHn'].
+  - intros m [x H].
+    reflexivity.
+  - intros [ | m'] [x H].
+    + simpl. discriminate.
+    + simpl. simpl in H.
+      injection H as H.
+      apply IHn'.
+      exists x.
+      apply H.
+Qed.
+
+Fixpoint In {A : Type} (x : A) (l : list A) : Prop :=
+  match l with
+  | [] => False
+  | x' :: l' => x' = x \/ In x l'
+  end.
+
+Example In_example_1 : In 4 [1; 2; 3; 4; 5].
+Proof.
+  simpl.
+  right. right. right. left. reflexivity.
+Qed.
+
+Example In_example_2 :
+  forall n, In n [2; 4] ->
+            exists n', n = 2 * n'.
+Proof.
+  simpl.
+  intros n [H | [H | []]].
+  - exists 1. rewrite <- H. reflexivity.
+  - exists 2. rewrite <- H. reflexivity.
+Qed.
+
+Theorem In_map :
+  forall (A B : Type) (f : A -> B) (l : list A) (x : A),
+    In x l ->
+    In (f x) (map f l).
+Proof.
+  intros A B f l x.
+  induction l as [ | h t IHt].
+  - simpl. intros [].
+  - simpl. intros [H | H].
+    + rewrite H.
+      left.
+      reflexivity.
+    + right.
+      apply IHt.
+      apply H.
+Qed.
+
+Theorem In_map_iff :
+  forall (A B : Type) (f : A -> B) (l : list A) (y : B),
+    In y (map f l) <->
+      exists x, f x = y /\ In x l.
+Proof.
+  intros A B f l y. split.
+  - induction l as [ | h t IHt].
+    + simpl.
+      intros contra.
+      exfalso.
+      apply contra.
+    + simpl.
+      intros [H | H].
+      * exists h.
+        split.
+        -- apply H.
+        -- left. reflexivity.
+      * apply IHt in H.
+        destruct H as [x [H1 H2]].
+        exists x.
+        split.
+        -- apply H1.
+        -- right. apply H2.
+  - induction l as [ | h t IHt].
+    + intros [x [H1 H2]].
+      simpl. simpl in H2. apply H2.
+    + intros [x [H1 H2]].
+      simpl.
+      simpl in H2.
+      destruct H2 as [H3 | H4].
+      * rewrite H3.
+        left.
+        apply H1.
+      * right.
+        apply IHt.
+        exists x.
+        split.
+        -- apply H1.
+        -- apply H4.
+Qed.
+
+Theorem In_app_iff : forall A l l' (a : A),
+    In a (l ++ l') <-> In a l \/ In a l'.
+Proof.
+  intros A l.
+  induction l as [ | h t IH].
+  - intros l' a.
+    simpl.
+    split.
+    + intros H.
+      right. apply H.
+    + intros [H | H].
+      * exfalso. apply H.
+      * apply H.
+  - intros l' a.
+    split.
+    + simpl.
+      intros [H | H].
+      * left. left. apply H.
+      * apply IH in H.
+        destruct H as [H | H].
+        -- left. right. apply H.
+        -- right. apply H.
+    + simpl.
+      intros [[H | H] | H].
+      * left. apply H.
+      * right.
+        apply IH.
+        left.
+        apply H.
+      * right.
+        apply IH.
+        right.
+        apply H.
+Qed.
+
+Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop :=
+  match l with
+  | [] => True
+  | h :: t => P h /\ All P t
+  end.
+
+Theorem All_in :
+  forall T (P : T -> Prop) (l : list T),
+    (forall x, In x l -> P x) <->
+      All P l.
+Proof.
+  intros T P.
+  induction l as [ | h t IHt].
+  - simpl.
+    split.
+    + intros H.
+      apply I.
+    + intros H x contra.
+      exfalso. apply contra.
+  - simpl.
+    split.
+    + intros H.
+      split.
+      * apply H.
+        left.
+        reflexivity.
+      * apply IHt.
+        intros x H1.
+        apply H.
+        right.
+        apply H1.
+    + intros [H1 H2] x.
+      intros [G1 | G2].
+      * rewrite <- G1.
+        apply H1.
+      * rewrite <- IHt in H2.
+        apply H2.
+        apply G2.
+Qed.
+
+Fixpoint Odd (n : nat) : Prop :=
+  match n with
+  | O => False
+  | S n' => ~(Odd n')
+  end.
+
+
+Definition combine_odd_even (Podd Peven : nat -> Prop) (n : nat) : Prop :=
+  (even n = true /\ Peven n) \/ (odd n = true /\ Podd n).
+
+Theorem combine_odd_even_intro :
+  forall (Podd Peven : nat -> Prop) (n : nat),
+    (odd n = true -> Podd n) ->
+    (odd n = false -> Peven n) ->
+    combine_odd_even Podd Peven n.
+Proof.
+  intros Podd Peven.
+  induction n as [ | n' IHn'].
+  - intros H1 H2.
+    unfold combine_odd_even.
+    left.
+    split.
+    + reflexivity.
+    + apply H2.
+      reflexivity.
+  - intros H1 H2.
+    unfold combine_odd_even.
+    destruct (odd (S n')) as [] eqn:EqSnodd.
+    + right.
+      split.
+      * reflexivity.
+      * apply H1.
+        reflexivity.
+    + left.
+      split.
+      * destruct n' as [ | n''].
+        -- discriminate.
+        -- simpl.
+           unfold odd in EqSnodd.
+           simpl in EqSnodd.
+           apply (f_equal negb) in EqSnodd.
+           simpl in EqSnodd.
+           rewrite <- negb_involutive with (b := even n'').
+           apply EqSnodd.
+      * apply H2.
+        reflexivity.
+Qed.
+
+Theorem combine_odd_even_elim_odd :
+  forall (Podd Peven : nat -> Prop) (n : nat),
+    combine_odd_even Podd Peven n ->
+    odd n = true ->
+    Podd n.
+Proof.
+  intros Podd Peven [ | n].
+  - unfold combine_odd_even.
+    simpl.
+    intros [H1 | H1] H2.
+    + unfold odd in H2.
+      simpl in H2.
+      exfalso.
+      discriminate.
+    + apply proj2 in H1.
+      apply H1.
+  - unfold combine_odd_even.
+    simpl.
+    intros [H1 | H1] H2.
+    + destruct n as [ | n'].
+      * exfalso.
+        apply proj1 in H1.
+        discriminate.
+      * exfalso.
+        apply proj1 in H1.
+        unfold odd in H2.
+        apply (f_equal negb) in H2.
+        rewrite negb_involutive in H2.
+        simpl in H2.
+        rewrite H1 in H2.
+        discriminate.
+    + apply proj2 in H1.
+      apply H1.
+Qed.
+
+Theorem in_not_nil :
+  forall A (x : A) (l : list A), In x l -> l <> [].
+Proof.
+  intros A x l H.
+  intro H1.
+  rewrite H1 in H.
+  simpl in H.
+  apply H.
+Qed.
+
+Lemma in_not_nil_42 :
+  forall l : list nat, In 42 l -> l <> [].
+Proof.
+  intros l H.
+  apply in_not_nil with (x := 42).
+  apply H.
+Qed.
+
+Example lemma_application_ex :
+  forall {n : nat} {ns : list nat},
+    In n (map (fun m => m * 0) ns) ->
+    n = 0.
+Proof.
+  intros n ns H.
+  destruct (proj1 _ _ (In_map_iff _ _ _ _ _) H) as [m [Hm _]].
+  rewrite mul_0_r in Hm.
+  rewrite <- Hm.
+  reflexivity.
+Qed.
+
+Lemma even_double : forall k, even (double k) = true.
+Proof.
+  induction k as [ | k' IHk'].
+  - reflexivity.
+  - simpl.
+    apply IHk'.
+Qed.
+
+Lemma even_double_conv : forall n, exists k,
+    n = if even n then double k else S (double k).
+Proof.
+  induction n as [ | n' IHn'].
+  - simpl.
+    exists 0.
+    reflexivity.
+  - destruct (even (S n')) as [] eqn:Eqeven.
+    + rewrite even_S in Eqeven.
+      apply (f_equal negb) in Eqeven.
+      rewrite negb_involutive in Eqeven.
+      simpl in Eqeven.
+      rewrite Eqeven in IHn'.
+      destruct IHn' as [k Hk].
+      apply (f_equal S) in Hk.
+      rewrite <- double_incr in Hk.
+      exists (S k).
+      apply Hk.
+    + rewrite even_S in Eqeven.
+      apply (f_equal negb) in Eqeven.
+      rewrite negb_involutive in Eqeven.
+      simpl in Eqeven.
+      rewrite Eqeven in IHn'.
+      destruct IHn' as [k Hk].
+      exists k.
+      apply (f_equal S) in Hk.
+      apply Hk.
+Qed.
+
+Theorem even_bool_prop : forall n,
+    even n = true <-> Even n.
+Proof.
+  intros n.
+  split.
+  - intros H.
+    destruct (even_double_conv n) as [k Hk].
+    rewrite Hk.
+    rewrite H.
+    exists k.
+    reflexivity.
+  - intros [k Hk].
+    rewrite Hk.
+    apply even_double.
+Qed.
+
+Theorem eqb_eq : forall n1 n2 : nat,
+    n1 =? n2 = true <-> n1 = n2.
+Proof.
+  intros n1 n2.
+  split.
+  - apply eqb_true.
+  - intros H.
+    rewrite H.
+    rewrite eqb_refl.
+    reflexivity.
+Qed.
+
+Theorem andb_true_iff : forall b1 b2 : bool,
+    b1 && b2 = true <-> b1 = true /\ b2 = true.
+Proof.
+  intros b1 b2.
+  split.
+  - intros H.
+    split.
+    + destruct b2 as [].
+      * rewrite andb_commutative in H.
+        simpl in H.
+        apply H.
+      * rewrite andb_commutative in H.
+        simpl in H.
+        discriminate.
+    + destruct b2 as [].
+      * reflexivity.
+      * rewrite andb_commutative in H.
+        simpl in H.
+        apply H.
+  - intros [H1 H2].
+    rewrite H1.
+    rewrite H2.
+    reflexivity.
+Qed.
+
+Theorem orb_true_iff : forall b1 b2,
+    b1 || b2 = true <-> b1 = true \/ b2 = true.
+Proof.
+  intros b1 b2.
+  split.
+  - intros H.
+    destruct b1 as [].
+    + left. reflexivity.
+    + right. rewrite false_or_b in H. apply H.
+  - intros [H | H].
+    + rewrite H. reflexivity.
+    + rewrite H.
+      destruct b1 as [] ; reflexivity.
+Qed.
+
+Theorem eqb_neq : forall x y : nat,
+    x =? y = false <-> x <> y.
+Proof.
+  intros x y.
+  split.
+  - intros H.
+    apply not_true_iff_false in H.
+    intros G.
+    apply eqb_eq in G.
+    apply H in G.
+    apply G.
+  - intros H.
+    apply not_true_iff_false.
+    intros G.
+    apply eqb_eq in G.
+    apply H in G.
+    apply G.
+Qed.
+
+Fixpoint eqb_list {A : Type} (eqb : A -> A -> bool)
+  (l1 l2 : list A) : bool :=
+  match l1, l2 with
+  | [], [] => true
+  | [], _ => false
+  | _, [] => false
+  | h1 :: t1, h2 :: t2 => eqb h1 h2 && eqb_list eqb t1 t2
+  end.
+
+Theorem eqb_list_true_iff :
+  forall A (eqb : A -> A -> bool),
+    (forall a1 a2, eqb a1 a2 = true <-> a1 = a2) ->
+    forall l1 l2, eqb_list eqb l1 l2 = true <-> l1 = l2.
+Proof.
+  intros A eqb H.
+  induction l1 as [ | h t IHt].
+  - intros [ | h2 t2].
+    + split ; reflexivity.
+    + split ; discriminate.
+  - intros [ | h2 t2].
+    + split ; discriminate.
+    + split.
+      * intros G.
+        simpl in G.
+        apply andb_true_iff in G.
+        destruct G as [G1 G2].
+        apply H in G1.
+        apply IHt in G2.
+        rewrite G1. rewrite G2. reflexivity.
+      * intros G.
+        simpl.
+        apply andb_true_iff.
+        split.
+        -- apply H.
+           injection G as G1 G2.
+           apply G1.
+        -- apply IHt.
+           injection G as G1 G2.
+           apply G2.
+Qed.
+
+Theorem forallb_true_iff : forall X test (l : list X),
+    forallb test l = true <-> All (fun x => test x = true) l.
+Proof.
+  intros X test.
+  induction l as [ | h t IHt].
+  - simpl. split ; trivial.
+  - split.
+    + intros H.
+      simpl.
+      simpl in H.
+      destruct (test h) as [].
+      * split.
+        { reflexivity. }
+        apply IHt.
+        apply H.
+      * discriminate H.
+    + simpl.        
+      intros [H1 H2].
+      rewrite H1.
+      apply IHt.
+      apply H2.
+Qed.
+
+Fixpoint rev_append {X} (l1 l2 : list X) : list X :=
+  match l1 with
+  | [] => l2
+  | x :: l1' => rev_append l1' (x :: l2)
+  end.
+
+Definition tr_rev {X} (l : list X) : list X :=
+  rev_append l [].
+
+Axiom functional_extensionality : forall {X Y : Type} {f g : X -> Y},
+    (forall (x : X), f x = g x) -> f = g.
+
+Lemma rev_rev_append : forall X (l1 l2 : list X),
+    rev_append l1 l2 = rev l1 ++ l2.
+Proof.
+  induction l1 as [ | h t IHt].
+  - intros l2. reflexivity.
+  - intros l2.
+    simpl.
+    rewrite <- app_assoc.
+    simpl.
+    apply IHt.
+Qed.    
+
+Theorem tr_rev_correct : forall X, @tr_rev X = @rev X.
+Proof.
+  intros X.
+  apply functional_extensionality.
+  induction x as [ | h t IHt].
+  - reflexivity.
+  - simpl.
+    unfold tr_rev.
+    simpl.
+    unfold tr_rev in IHt.
+    apply rev_rev_append.
+Qed.
+
+Theorem excluded_middle_irrefutable: forall (P : Prop),
+    ~~(P \/ ~P).
+Proof.
+  intros P contra.
+  apply de_morgan_not_or in contra.
+  destruct contra as [A B].
+  apply B in A.
+  apply A.
+Qed.
+
+Definition excluded_middle := forall P : Prop, P \/ ~P.
+
+Theorem not_exists_dist :
+  (forall P : Prop, P \/ ~P) ->
+  forall (X : Type) (P : X -> Prop),
+    ~(exists x, ~P x) -> (forall x, P x).
+Proof.
+  intros EM X P H.
+  intros x.
+  specialize EM with (P := P x) as [HP | HNP].
+  - apply HP.
+  - exfalso.
+    apply H.
+    exists x.
+    apply HNP.
+Qed.
+
+Definition peirce := forall P Q: Prop,
+    ((P -> Q) -> P) -> P.
+
+Definition dne := forall P : Prop,
+    ~~P -> P.
+
+Definition de_morgan_not_and_not := forall P Q : Prop,
+    ~(~P /\ ~Q) -> P \/ Q.
+
+Definition implies_to_or := forall P Q : Prop,
+    (P -> Q) -> (~P \/ Q).
+
+Theorem em_to_peirce : excluded_middle -> peirce.
+Proof.
+  unfold excluded_middle.
+  unfold peirce.
+  intros EM P Q PQP.
+  specialize EM with (P := P) as EM'.
+  destruct EM' as [HP | NHP].
+  - apply HP.
+  - apply PQP.
+    intros HP.
+    exfalso.
+    apply NHP in HP.
+    apply HP.
+Qed.
+
+Theorem peirce_dne : peirce -> dne.
+Proof.
+  unfold peirce.
+  unfold dne.
+  intros HP P NNP.
+  specialize HP with (P := P) (Q := False) as HP'.
+  apply HP'.
+  intros HNP.
+  exfalso.
+  apply NNP in HNP.
+  apply HNP.
+Qed.
+
+Theorem dne_de_morgan_not_and_not : dne -> de_morgan_not_and_not.
+Proof.
+  unfold dne.
+  unfold de_morgan_not_and_not.
+  intros DNE P Q H.
+  apply (DNE (P \/ Q)).
+  intros NPQ.
+  apply H.
+  split.
+  - intros HP.
+    apply NPQ.
+    left. apply HP.
+  - intros HQ.
+    apply NPQ.
+    right. apply HQ.
+Qed.
+
+Theorem de_morgan_not_and_not_implies_to_or :
+  de_morgan_not_and_not -> implies_to_or.
+Proof.
+  unfold de_morgan_not_and_not.
+  unfold implies_to_or.
+  intros DM P Q H.
+  apply DM.
+  intros [NNP NQ].
+  apply NNP.
+  apply contrapositive in H.
+  - apply H.
+  - apply NQ.
+Qed.
+
+Theorem implies_to_or_excluded_middle :
+  implies_to_or -> excluded_middle.
+Proof.
+  unfold implies_to_or.
+  unfold excluded_middle.
+  intros IO P.
+  apply or_comm.
+  apply IO.
+  trivial.
+Qed.
diff --git a/Makefile b/Makefile
index fda94e9..ab8ad86 100644
--- a/Makefile
+++ b/Makefile
@@ -45,7 +45,7 @@ HASNATDYNLINK     := $(COQMF_HASNATDYNLINK)
 OCAMLWARN         := $(COQMF_WARN)
 
 Makefile.conf: _CoqProject
-	coq_makefile -f _CoqProject Basics.v Induction.v Lists.v Polymorphism.v Tactics.v -o Makefile
+	coq_makefile -f _CoqProject Basics.v Induction.v Lists.v Logic.v Polymorphism.v Tactics.v -o Makefile
 
 # This file can be created by the user to hook into double colon rules or
 # add any other Makefile code he may need
diff --git a/Makefile.conf b/Makefile.conf
index 3682eec..be67555 100644
--- a/Makefile.conf
+++ b/Makefile.conf
@@ -1,5 +1,5 @@
 # This configuration file was generated by running:
-# coq_makefile -f _CoqProject Basics.v Induction.v Lists.v Polymorphism.v Tactics.v -o Makefile
+# coq_makefile -f _CoqProject Basics.v Induction.v Lists.v Logic.v Polymorphism.v Tactics.v -o Makefile
 
 COQBIN?=
 ifneq (,$(COQBIN))
@@ -14,7 +14,7 @@ COQMKFILE ?= "$(COQBIN)coq_makefile"
 #                                                                             #
 ###############################################################################
 
-COQMF_CMDLINE_VFILES := Basics.v Induction.v Lists.v Polymorphism.v Tactics.v
+COQMF_CMDLINE_VFILES := Basics.v Induction.v Lists.v Logic.v Polymorphism.v Tactics.v
 COQMF_SOURCES := $(shell $(COQMKFILE) -sources-of -f _CoqProject $(COQMF_CMDLINE_VFILES))
 COQMF_VFILES := $(filter %.v, $(COQMF_SOURCES))
 COQMF_MLIFILES := $(filter %.mli, $(COQMF_SOURCES))
diff --git a/Tactics.v b/Tactics.v
index ca172ac..d6d156f 100644
--- a/Tactics.v
+++ b/Tactics.v
@@ -86,14 +86,6 @@ Proof.
     discriminate H.
 Qed.
 
-Theorem f_equal : forall (A B : Type) (f : A -> B) (x y : A),
-    x = y -> f x = f y.
-Proof.
-  intros A B f x y eq.
-  rewrite eq.
-  reflexivity.
-Qed.
-
 Theorem eq_implies_succ_eq : forall (n m : nat),
     n = m -> S n = S m.
 Proof.