From 54576fa37345a8d355cb336256f74ad33d49b4e1 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 11 Feb 2018 19:06:52 -0500
Subject: [PATCH] Revising Polymorphism

---
 Polymorphism.v          | 22 +++++++++++-----------
 Polymorphism_template.v | 17 ++++++-----------
 2 files changed, 17 insertions(+), 22 deletions(-)

diff --git a/Polymorphism.v b/Polymorphism.v
index b458dce..ea932a0 100644
--- a/Polymorphism.v
+++ b/Polymorphism.v
@@ -56,8 +56,7 @@ Definition add_optional (po : option (nat * nat)) : option nat :=
 (** * Lists *)
 
 (* For functional programming (as in Coq), the king of all generic data
- * structures is the *list*, which you explored a bit in the first problem set.
- * Let's recap that type definition. *)
+ * structures is the *list*. *)
 Inductive list (A : Set) : Set :=
 | nil
 | cons (hd : A) (tl : list A).
@@ -98,9 +97,9 @@ Example nats2'' : list nat := [1; 2].
 Example nats3'' : list nat := [1; 2; 3].
 
 (* Here are some classic recursive functions that operate over lists.
- * First, here is how to compute the length of a list.  Recall that we put
- * *implicit* function arguments in curly braces, asking Coq to infer them at
- * call sites. *)
+ * First, here is how to compute the length of a list.  We put *implicit*
+ * function arguments in curly braces, asking Coq to infer them at call
+ * sites. *)
 
 Fixpoint length {A} (ls : list A) : nat :=
   match ls with
@@ -108,11 +107,9 @@ Fixpoint length {A} (ls : list A) : nat :=
   | _ :: ls' => 1 + length ls'
   end.
 
-(* The first problem set involved an exercise with list append and reverse
- * operations.  To avoid spoiling the proofs there about those functions, we
- * will give their definitions here without proving the classic theorems from
- * the problem set. *)
+(* Here are two classic recursive functions on lists. *)
 
+(* First, concatenation: *)
 Fixpoint app {A} (ls1 ls2 : list A) : list A :=
   match ls1 with
   | nil => ls2
@@ -121,6 +118,7 @@ Fixpoint app {A} (ls1 ls2 : list A) : list A :=
 
 Infix "++" := app.
 
+(* Next, reversal: *)
 Fixpoint rev {A} (ls : list A) : list A :=
   match ls with
   | nil => nil
@@ -129,7 +127,9 @@ Fixpoint rev {A} (ls : list A) : list A :=
 
 Theorem length_app : forall A (ls1 ls2 : list A),
     length (ls1 ++ ls2) = length ls1 + length ls2.
-Admitted.
+Proof.
+  induct ls1; simplify; equality.
+Qed.
 
 (* One of the classic gotchas in functional-programming class is how slow this
  * naive [rev] is.  Each [app] operation requires linear time, so running
@@ -558,7 +558,7 @@ Proof.
 Qed.
 
 (* Other transformations are also possible, like the Swedish-Chef optimization,
- * that turns every variable into "bork".  It saves many bits when most variable
+ * which turns every variable into "bork".  It saves many bits when most variable
  * names are longer than 4 characters. *)
 
 Fixpoint swedishExpression (e : expression) : expression :=
diff --git a/Polymorphism_template.v b/Polymorphism_template.v
index 178dbae..b858ea3 100644
--- a/Polymorphism_template.v
+++ b/Polymorphism_template.v
@@ -45,8 +45,7 @@ Definition add_optional (po : option (nat * nat)) : option nat :=
 (** * Lists *)
 
 (* For functional programming (as in Coq), the king of all generic data
- * structures is the *list*, which you explored a bit in the first problem set.
- * Let's recap that type definition. *)
+ * structures is the *list*. *)
 Inductive list (A : Set) : Set :=
 | nil
 | cons (hd : A) (tl : list A).
@@ -97,8 +96,7 @@ Fixpoint length {A} (ls : list A) : nat :=
   | _ :: ls' => 1 + length ls'
   end.
 
-(* More familiar operations from Pset1 *)
-
+(* Concatenation: *)
 Fixpoint app {A} (ls1 ls2 : list A) : list A :=
   match ls1 with
   | nil => ls2
@@ -107,6 +105,7 @@ Fixpoint app {A} (ls1 ls2 : list A) : list A :=
 
 Infix "++" := app.
 
+(* Reversal: *)
 Fixpoint rev {A} (ls : list A) : list A :=
   match ls with
   | nil => nil
@@ -115,6 +114,7 @@ Fixpoint rev {A} (ls : list A) : list A :=
 
 Theorem length_app : forall A (ls1 ls2 : list A),
     length (ls1 ++ ls2) = length ls1 + length ls2.
+Proof.
 Admitted.
 
 (* One of the classic gotchas in functional-programming class is how slow this
@@ -143,9 +143,7 @@ Compute rev' [1; 2; 3; 4].
 Compute rev ["hi"; "bye"; "sky"].
 Compute rev' ["hi"; "bye"; "sky"].
 
-(* OK, great.  Now it seems worth investing in a correctness proof.  We'll
- * discover it interactively in class, but here's a worked-out final
- * answer, with the several lemmas that we discover are useful. *)
+(* OK, great.  Now it seems worth investing in a correctness proof. *)
 
 Theorem rev'_ok : forall A (ls : list A),
     rev' ls = rev ls.
@@ -374,16 +372,13 @@ Fixpoint listifyStatement (s : statement) : list var :=
 
 Compute listifyStatement factorial.
 
-(* At this point, I can't resist switching to a more automated proof style,
- * though still a pretty tame one. *)
-
 Theorem length_listifyStatement : forall s,
     length (listifyStatement s) = varsInStatement s.
 Proof.
 Admitted.
 
 (* Other transformations are also possible, like the Swedish-Chef optimization,
- * that turns every variable into "bork".  It saves many bits when most variable
+ * which turns every variable into "bork".  It saves many bits when most variable
  * names are longer than 4 characters. *)
 
 Fixpoint swedishExpression (e : expression) : expression :=