From LF Require Export Polymorphism.
From LF Require Export Lists.

Theorem silly : forall (n m o p : nat),
    n = m ->
    (n = m -> [n ; o] = [m ; p]) ->
    [n;o] = [m;p].
Proof.
  intros n m o p eq1 eq2.
  apply eq2.
  apply eq1.
Qed.

Theorem rev_involutive : forall (X : Type) (l : list X),
    rev (rev l) = l.
Proof.
  intros X.
  induction l as [ | h t IHt].
  - reflexivity.
  - simpl.
    rewrite rev_app_distr.
    rewrite IHt.
    reflexivity.
Qed.    

Theorem rev_exercise1 : forall (X : Type ) (l l' : list X),
    l = rev l' -> l' = rev l.
Proof.
  intros X l l' H.
  rewrite H.
  symmetry.
  apply rev_involutive.
Qed.

Theorem trans_eq : forall (X : Type) (n m o : X),
    n = m -> m = o -> n = o.
Proof.
  intros X n m o eq1 eq2.
  rewrite eq1.
  rewrite eq2.
  reflexivity.
Qed.

Example trans_eq_exercise : forall (n m o p : nat),
    m = S o ->
    (n + p) = m ->
    (n + p) = S o.
Proof.
  intros n m o p eq1 eq2.
  transitivity m.
  - apply eq2.
  - apply eq1.
Qed.

Example injection_ex_1 : forall (n m o : nat),
    [n ; m] = [o ; o] ->
    n = m.
Proof.
  intros n m o H.
  injection H as H1 H2.
  rewrite H1.
  rewrite H2.
  reflexivity.
Qed.

Example injection_ex_2 : forall (X : Type) (x y z : X) (l j : list X),
    x :: y :: l = z :: j ->
    j = z :: l ->
    x = y.
Proof.
  intros X x y z l j H1 H2.
  injection H1 as H1'.
  rewrite H1'.
  rewrite H2 in H.
  injection H as H'.
  symmetry.
  apply H'.
Qed.

Theorem eqb_0_l : forall n,
    0 =? n = true -> n = 0.
Proof.
  intros [ | n'].
  - reflexivity.
  - intros H.
    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.
  intros n m H.
  apply f_equal.
  apply H.
Qed.

Theorem S_inj : forall (n m : nat) (b : bool),
    ((S n) =? (S m)) = b ->
    (n =? m) = b.
Proof.
  intros n m b H.
  simpl in H.
  apply H.
Qed.

Example specialize_example : forall n,
    (forall m, m * n = 0)
    -> n = 0.
Proof.
  intros n H.
  specialize H with (m := 1).
  simpl in H.
  rewrite add_0_r in H.
  apply H.
Qed.

Theorem double_injective : forall n m,
    double n = double m ->
    n = m.
Proof.
  induction n as [ | n' IHn'].
  - simpl.
    intros m H.
    destruct m as [ | m'].
    + reflexivity.
    + discriminate.
  - simpl.
    intros m H.
    destruct m as [ | m'].
    + discriminate.
    + f_equal.
      apply IHn'.
      simpl in H.
      injection H as H.
      apply H.
Qed.

Theorem eqb_true : forall n m,
    n =? m = true -> n = m.
Proof.
  induction n as [ | n' IHn'].
  - simpl.
    intros m H.
    destruct m as [ | m'] eqn:Eqm.
    + reflexivity.
    + discriminate.
  - simpl.
    intros m H.
    destruct m as [ | m'] eqn:Eqm.
    + discriminate.
    + f_equal.
      apply IHn' in H.
      apply H.
Qed.
  
Theorem plus_n_n_injective : forall n m,
    n + n = m + m ->
    n = m.
Proof.
  induction n as [ | n' IHn'].
  - simpl.
    intros m H.
    destruct m as [ | m' ].
    + trivial.
    + discriminate.
  - simpl.
    intros m H.
    destruct m as [ | m' ].
    + discriminate.
    + simpl in H.
      injection H as H.
      rewrite <- plus_n_Sm in H.
      rewrite <- plus_n_Sm in H.
      injection H as H.
      apply IHn' in H.
      rewrite H.
      reflexivity.
Qed.

Theorem nth_error_after_last : forall (n : nat) (X : Type) (l : list X),
    length l = n ->
    nth_error l n = None.
Proof.
  intros n X l.
  generalize dependent n.
  induction l as [ | h t IHt].
  - intros n H.
    reflexivity.
  - intros n H.
    destruct n as [ | n'].
    + simpl.
      discriminate.
    + simpl.
      simpl in H.
      injection H as H.
      apply IHt in H.
      apply H.
Qed.

Definition square n := n * n.

Lemma square_mult : forall n m, square (n * m) = square n * square m.
Proof.
  intros n m.
  unfold square.
  rewrite mult_assoc.
  assert (H : n * m * n = n * n * m).
  { rewrite mul_comm. apply mult_assoc. }
  rewrite H. rewrite mult_assoc. reflexivity.
Qed.

Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
    split l = (l1, l2) ->
    combine l1 l2 = l.
Proof.
  intros X Y l l1 l2.
  generalize dependent l2.
  generalize dependent l1.
  induction l as [ | (h1, h2) t IHt].
  - intros l1 l2.
    simpl.
    intros H.
    injection H as H1 H2.
    rewrite <- H1.
    rewrite <- H2.
    reflexivity.
  - intros l1 l2 H.
    simpl in H.
    destruct (split t) as [t1 t2] eqn:Eqnt in H.
    apply IHt in Eqnt.
    injection H as H1 H2.
    rewrite <- H1.
    rewrite <- H2.
    simpl.
    rewrite Eqnt.
    reflexivity.
Qed.

Theorem bool_fn_applied_thrice :
  forall (f : bool -> bool) (b : bool),
    f (f (f b)) = f b.
Proof.
  intros f b.
  destruct b as [ | ] eqn:Eqb
  ; destruct (f true) as [ | ] eqn:Eqft
  ; destruct (f false) as [ | ] eqn:Eqff.
  - repeat rewrite Eqft. reflexivity.
  - repeat rewrite Eqft. reflexivity.
  - rewrite Eqft. reflexivity.
  - rewrite Eqff. reflexivity.
  - repeat rewrite Eqft. reflexivity.
  - repeat rewrite Eqff. reflexivity.
  - rewrite Eqft. rewrite Eqff. reflexivity.
  - repeat rewrite Eqff. reflexivity.
Qed.

Theorem eqb_sym : forall (n m : nat),
    (n =? m) = (m =? n).
Proof.
  induction n as [ | n' IHn'].
  - intros m.
    destruct (0 =? m) as [ | ] eqn:Eqmz.
    + apply eqb_true in Eqmz.
      rewrite <- Eqmz.
      reflexivity.
    + simpl in Eqmz.
      destruct m as [ | m' ] eqn:Eqm.
      * discriminate.
      * reflexivity.
  - intros m.
    destruct (S n' =? m) as [ | ] eqn:EqmSn.
    + simpl in EqmSn.
      destruct m as [ | m' ] eqn:Eqm.
      * discriminate.
      * apply eqb_true in EqmSn.
        rewrite EqmSn.
        rewrite eqb_refl.
        reflexivity.
    + destruct m as [ | m' ] eqn:Eqm.
      * reflexivity.
      * simpl.
        simpl in EqmSn.
        rewrite IHn' with (m := m') in EqmSn.
        symmetry.
        apply EqmSn.
Qed.

Theorem eqb_trans : forall n m p,
    n =? m = true ->
    m =? p = true ->
    n =? p = true.
Proof.
  intros n m p H1 H2.
  apply eqb_true in H1.
  apply eqb_true in H2.
  rewrite <- H1 in H2.
  rewrite H2.
  rewrite eqb_refl.
  reflexivity.
Qed.

Theorem filter_exercise : forall (X : Type) (test : X -> bool)
                                 (x : X) (l lf : list X),
    filter test l = x :: lf ->
    test x = true.
Proof.
  intros X test x l lf.
  generalize dependent lf.
  induction l as [ | h t IHt].
  - intros lf H.
    simpl in H.
    discriminate H.
  - intros lf H.
    destruct (test h) as [ | ] eqn:Eqtesth.
    + simpl in H.
      rewrite Eqtesth in H.
      injection H as H1 H2.
      rewrite H1 in Eqtesth.
      apply Eqtesth.
    + simpl in H.
      rewrite Eqtesth in H.
      apply IHt in H.
      apply H.
Qed.

Fixpoint forallb {X : Type} (test : X -> bool) (l : list X) :=
  match l with
  | [] => true
  | h :: t => if test h
              then forallb test t
              else false
  end.

Fixpoint existsb {X : Type} (test : X -> bool) (l : list X) :=
  match l with
  | [] => false
  | h :: t => if test h
              then true
              else existsb test t
  end.

Definition existsb' {X : Type} (test : X -> bool) (l : list X) :=
  negb (forallb (fun x => negb (test x)) l).

Theorem existsb_existsb' : forall (X : Type) (test : X -> bool) (l : list X),
    existsb test l = existsb' test l.
Proof.
  intros X test.
  induction l as [ | h t IHt].
  - reflexivity.
  - simpl.
    destruct (test h) as [ | ] eqn:Eqtesth.
    + unfold existsb'.
      simpl.
      rewrite Eqtesth.
      reflexivity.
    + unfold existsb'.
      simpl.
      rewrite Eqtesth.
      simpl.
      unfold existsb' in IHt.
      apply IHt.
Qed.