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.