From 1646475f967361dddc605f0f2f8ed99ffb7509af Mon Sep 17 00:00:00 2001
From: William Ball <williampi103@gmail.com>
Date: Sat, 30 Mar 2024 22:45:43 -0700
Subject: [PATCH] more

---
 .gitignore              |   2 +
 Structured.v => Lists.v |   0
 Makefile                |   2 +-
 Makefile.conf           |   4 +-
 Polymorphism.v          | 291 +++++++++++++++++++++++++++++++
 Tactics.v               | 371 ++++++++++++++++++++++++++++++++++++++++
 6 files changed, 667 insertions(+), 3 deletions(-)
 rename Structured.v => Lists.v (100%)
 create mode 100644 Polymorphism.v
 create mode 100644 Tactics.v

diff --git a/.gitignore b/.gitignore
index da8f6cd..d95d939 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,5 @@
 *.vos
 .Makefile.d
 *.aux
+Makefile
+Makefile.conf
diff --git a/Structured.v b/Lists.v
similarity index 100%
rename from Structured.v
rename to Lists.v
diff --git a/Makefile b/Makefile
index 7dce943..fda94e9 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 Structured.v -o Makefile
+	coq_makefile -f _CoqProject Basics.v Induction.v Lists.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 a49f604..3682eec 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 Structured.v -o Makefile
+# coq_makefile -f _CoqProject Basics.v Induction.v Lists.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 Structured.v
+COQMF_CMDLINE_VFILES := Basics.v Induction.v Lists.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/Polymorphism.v b/Polymorphism.v
new file mode 100644
index 0000000..0c04c57
--- /dev/null
+++ b/Polymorphism.v
@@ -0,0 +1,291 @@
+From LF Require Export Lists.
+
+Inductive list (X : Type) : Type :=
+| nil
+| cons (x : X) (l : list X).
+
+Fixpoint repeat X x count : list X :=
+  match count with
+  | 0 => nil X
+  | S count' => cons X x (repeat X x count')
+  end.
+
+Arguments nil {X}.
+Arguments cons {X}.
+Arguments repeat {X}.
+
+Fixpoint app {X : Type} (l1 l2 : list X) : list X :=
+  match l1 with
+  | nil => l2
+  | cons h t => cons h (app t l2)
+  end.
+
+Fixpoint rev {X : Type} (l: list X) : list X :=
+  match l with
+  | nil => nil
+  | cons h t => app (rev t) (cons h nil)
+  end.
+
+Fixpoint length {X : Type} (l : list X) : nat :=
+  match l with
+  | nil => 0
+  | cons _ l' => S (length l')
+  end.
+
+Notation "x :: y" := (cons x y)
+                       (at level 60, right associativity).
+
+Notation "[ ]" := nil.
+Notation "[ x ; .. ; y ]" := (cons x .. (cons y []) ..).
+Notation "x ++ y" := (app x y)
+                       (at level 60, right associativity).
+
+Theorem app_nil_r : forall (X: Type), forall l:list X,
+    l ++ [] = l.
+Proof.
+  intros X.
+  induction l as [ | h t IHt].
+  - reflexivity.
+  - simpl.
+    rewrite IHt.
+    reflexivity.
+Qed.
+
+Theorem app_assoc : forall A (l m n: list A),
+    l ++ m ++ n = (l ++ m) ++ n.
+Proof.
+  intros A l m n.
+  induction l as [ | h t IHt].
+  - reflexivity.
+  - simpl.
+    rewrite IHt.
+    reflexivity.
+Qed.
+
+Lemma app_length : forall X (l1 l2 : list X),
+    length (l1 ++ l2) = length l1 + length l2.
+Proof.
+  intros X l1 l2.
+  induction l1 as [ | h t IHt].
+  - reflexivity.
+  - simpl. rewrite IHt. reflexivity.
+Qed.
+
+Theorem rev_app_distr: forall X (l1 l2 : list X),
+    rev (l1 ++ l2) = rev l2 ++ rev l1.
+Proof.
+  intros X l1 l2.
+  induction l1 as [ | h t IHt].
+  - simpl.
+    rewrite app_nil_r.
+    reflexivity.
+  - simpl.
+    rewrite IHt.
+    rewrite app_assoc.
+    reflexivity.
+Qed.
+
+Inductive prod (X Y : Type) : Type :=
+| pair (x : X) (y : Y).
+
+Arguments pair {X Y}.
+
+Notation "( x , y )" := (pair x y).
+Notation "X * Y" := (prod X Y) : type_scope.
+
+Definition fst {X Y : Type} (p : X * Y) : X :=
+  match p with
+  | (x, y) => x
+  end.
+
+Definition snd {X Y : Type} (p : X * Y) : Y :=
+  match p with
+  | (x, y) => y
+  end.
+
+Fixpoint combine {X Y : Type} (lx : list X) (ly : list Y) : list (X * Y) :=
+  match lx, ly with
+  | [], _ => []
+  | _, [] => []
+  | x :: tx, y :: ty => (x, y) :: (combine tx ty)
+  end.
+
+Fixpoint split {X Y : Type} (l : list (X * Y)) : (list X) * (list Y) :=
+  match l with
+  | [] => ([], [])
+  | (x, y) :: rest => match split rest with
+                      | (xs, ys) => (x :: xs, y :: ys)
+                      end
+  end.
+
+Fixpoint nth_error {X : Type} (l : list X) (n : nat) : option X :=
+  match l with
+  | nil => None
+  | a :: l' => match n with
+               | O => Some a
+               | S n' => nth_error l' n'
+               end
+  end.
+
+Definition hd_error {X : Type} (l : list X) : option X :=
+  match l with
+  | [] => None
+  | h :: _ => Some h
+  end.
+
+Definition doit3times {X : Type} (f : X -> X) (n : X) : X :=
+  f (f (f n)).
+
+Fixpoint filter {X : Type} (test : X -> bool) (l : list X) : list X :=
+  match l with
+  | [] => []
+  | h :: t => if test h
+              then h :: (filter test t)
+              else filter test t
+  end.
+
+Definition filter_even_gt_7 : list nat -> list nat :=
+  filter (fun n => even n && (7 <? n)).
+
+Definition partition {X : Type}
+  (test : X -> bool)
+  (l : list X)
+  : list X * list X :=
+  match l with
+  | [] => ([], [])
+  | h :: t => if test h
+              then (h :: filter test t, filter (fun y => negb (test y)) t)
+              else (filter test t, h :: filter (fun y => negb (test y)) t)
+  end.
+
+Fixpoint map {X Y : Type} (f : X -> Y) (l : list X) : list Y :=
+  match l with
+  | [] => []
+  | h :: t => f h :: map f t
+  end.
+
+Theorem map_app : forall (X Y : Type) (f : X -> Y) (l1 l2 : list X),
+    map f (l1 ++ l2) = map f l1 ++ map f l2.
+Proof.
+  intros X Y f l1 l2.
+  induction l1 as [ | h t IHt].
+  - reflexivity.
+  - simpl.
+    rewrite IHt.
+    reflexivity.
+Qed.
+    
+Theorem map_rev : forall (X Y : Type) (f : X -> Y) (l : list X),
+    map f (rev l) = rev (map f l).
+Proof.
+  intros X Y f.
+  induction l as [ | h t IHt].
+  - reflexivity.
+  - simpl.
+    rewrite map_app.
+    simpl.
+    rewrite IHt.
+    reflexivity.
+Qed.
+
+Fixpoint flat_map {X Y : Type} (f : X -> list Y) (l : list X) : list Y :=
+  match l with
+  | [] => []
+  | h :: t => f h ++ flat_map f t
+  end.
+
+Definition option_map {X Y : Type} (f : X -> Y) (xo : option X) : option Y :=
+  match xo with
+  | None => None
+  | Some x => Some (f x)
+  end.
+
+Fixpoint fold {X Y : Type} (f : X -> Y -> Y) (l : list X) (b : Y) : Y :=
+  match l with
+  | nil => b
+  | h :: t => f h (fold f t b)
+  end.
+
+Definition constfun {X : Type} (x : X) : nat -> X :=
+  fun (k : nat) => x.
+
+Module Exercises.
+  Definition fold_length {X : Type} (l : list X) : nat :=
+    fold (fun _ n => S n) l 0.
+
+  Theorem fold_length_correct : forall X (l : list X),
+      fold_length l = length l.
+  Proof.
+    intros X.
+    induction l as [ | h t IHt].
+    - reflexivity.
+    - simpl.
+      rewrite <- IHt.
+      reflexivity.
+  Qed.
+
+  Definition fold_map {X Y : Type} (f : X -> Y) (l : list X) : list Y :=
+    fold (fun x acc => f x :: acc) l [].
+
+  Theorem fold_map_correct : forall X Y (f : X -> Y) (l : list X),
+      fold_map f l = map f l.
+  Proof.
+    intros X Y f.
+    induction l as [ | h t IHt].
+    - reflexivity.
+    - simpl.
+      rewrite <- IHt.
+      reflexivity.
+  Qed.
+
+  Definition prod_curry {X Y Z : Type}
+    (f : X * Y -> Z) (x : X) (y : Y) : Z := f (x, y).
+
+  Definition prod_uncurry {X Y Z : Type}
+    (f : X -> Y -> Z) (p : X * Y) : Z :=
+    match p with
+    | (x, y) => f x y
+    end.
+
+  Theorem uncurry_curry : forall (X Y Z : Type)
+                                 (f : X -> Y -> Z)
+                                 x y,
+      prod_curry (prod_uncurry f) x y = f x y.
+  Proof.
+    intros X Y Z f x y.
+    unfold prod_uncurry.
+    unfold prod_curry.
+    reflexivity.
+  Qed.
+
+  Theorem curry_uncurry : forall (X Y Z : Type)
+                                 (f : X * Y -> Z)
+                                 x y,
+      prod_uncurry (prod_curry f) (x, y) = f (x, y).
+  Proof.
+    intros X Y Z f x y.
+    unfold prod_uncurry, prod_curry.
+    reflexivity.
+  Qed.
+  
+  Module Church.
+    Definition cnat := forall X : Type, (X -> X) -> X -> X.
+
+    Definition zero : cnat :=
+      fun (X : Type) (f : X -> X) (x : X) => x.
+
+    Definition scc (n : cnat) : cnat :=
+      fun (X : Type) (f : X -> X) (x : X) => f ((n X f) x).
+
+    Definition one := scc zero.
+    Definition two := scc one.
+
+    Definition plus (n m : cnat) : cnat :=
+      fun (X : Type) (f : X -> X) (x : X) => (n X f) ((m X f) x).
+
+    Definition mult (n m : cnat) : cnat :=
+      fun (X : Type) (f : X -> X) (x : X) =>
+        (m X (n X f)) x.
+
+  End Church.
+End Exercises.
diff --git a/Tactics.v b/Tactics.v
new file mode 100644
index 0000000..ca172ac
--- /dev/null
+++ b/Tactics.v
@@ -0,0 +1,371 @@
+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.