From 027cc8dc14d364818b0db8dc42541e581b405552 Mon Sep 17 00:00:00 2001
From: Michael Zhang <iptq@protonmail.com>
Date: Thu, 4 Jun 2020 05:32:54 -0500
Subject: [PATCH] Poly.v

---
 Poly.v | 57 ++++++++++++++++++++++++++++++++++++++++++---------------
 1 file changed, 42 insertions(+), 15 deletions(-)

diff --git a/Poly.v b/Poly.v
index 84ab9a5..34a9338 100644
--- a/Poly.v
+++ b/Poly.v
@@ -406,18 +406,29 @@ Definition list123''' := [1; 2; 3].
 Theorem app_nil_r : forall (X:Type), forall l:list X,
   l ++ [] = l.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros H L.
+  induction L.
+  - reflexivity.
+  - simpl. rewrite -> IHL. reflexivity.
+Qed.
 
 Theorem app_assoc : forall A (l m n:list A),
   l ++ m ++ n = (l ++ m) ++ n.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros A.
+  induction l.
+  - reflexivity.
+  - intros m n. simpl. rewrite <- IHl. reflexivity.
+Qed.
 
 Lemma app_length : forall (X:Type) (l1 l2 : list X),
   length (l1 ++ l2) = length l1 + length l2.
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  intros X.
+  induction l1.
+  - reflexivity.
+  - intros l2. simpl. rewrite <- IHl1. reflexivity.
+Qed.
 
 (** **** Exercise: 2 stars, standard, optional (more_poly_exercises)  
 
@@ -426,13 +437,25 @@ Proof.
 Theorem rev_app_distr: forall X (l1 l2 : list X),
   rev (l1 ++ l2) = rev l2 ++ rev l1.
 Proof.
-  (* FILL IN HERE *) Admitted.
+  intros X.
+  induction l1. induction l2.
+  - reflexivity.
+  - simpl. rewrite -> app_nil_r. reflexivity.
+  - intros l2. simpl. rewrite -> IHl1. rewrite <- app_assoc. reflexivity.
+Qed.
 
 Theorem rev_involutive : forall X : Type, forall l : list X,
   rev (rev l) = l.
 Proof.
-  (* FILL IN HERE *) Admitted.
-(** [] *)
+  intros X.
+  induction l.
+  - reflexivity.
+  - simpl.
+    rewrite -> rev_app_distr.
+    simpl.
+    rewrite -> IHl.
+    reflexivity.
+Qed.
 
 (* ================================================================= *)
 (** ** Polymorphic Pairs *)
@@ -515,13 +538,17 @@ Fixpoint combine {X Y : Type} (lx : list X) (ly : list Y)
     given unit test. *)
 
 Fixpoint split {X Y : Type} (l : list (X*Y))
-               : (list X) * (list Y)
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+               : (list X) * (list Y) :=
+  match l with
+  | nil => (nil, nil)
+  | (x, y) :: t => match split t with
+    | (a, b) => (x :: a, y :: b)
+    end
+  end.
 
 Example test_split:
   split [(1,false);(2,false)] = ([1;2],[false;false]).
-Proof.
-(* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 (** [] *)
 
 (* ================================================================= *)
@@ -696,16 +723,16 @@ Proof. reflexivity.  Qed.
     and returns a list of just those that are even and greater than
     7. *)
 
-Definition filter_even_gt7 (l : list nat) : list nat
-  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+Definition filter_even_gt7 (l : list nat) : list nat :=
+  filter (fun n => andb (7 <? n) (evenb n)) l.
 
 Example test_filter_even_gt7_1 :
   filter_even_gt7 [1;2;6;9;10;3;12;8] = [10;12;8].
- (* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 
 Example test_filter_even_gt7_2 :
   filter_even_gt7 [5;2;6;19;129] = [].
- (* FILL IN HERE *) Admitted.
+Proof. reflexivity. Qed.
 (** [] *)
 
 (** **** Exercise: 3 stars, standard (partition)