--- a/src/Equality.v	Wed Nov 11 14:34:24 2009 -0500
+++ b/src/Equality.v	Wed Nov 11 15:12:40 2009 -0500
@@ -34,6 +34,7 @@
   end.
 
 Theorem reduce_me : pred' 1 = 0.
+
 (* begin thide *)
   (** CIC follows the traditions of lambda calculus in associating reduction rules with Greek letters.  Coq can certainly be said to support the familiar alpha reduction rule, which allows capture-avoiding renaming of bound variables, but we never need to apply alpha explicitly, since Coq uses a de Bruijn representation that encodes terms canonically.
 
@@ -41,51 +42,51 @@
 
   cbv delta.
   (** [[
-
   ============================
    (fun x : nat => match x with
                    | 0 => 0
                    | S n' => let y := n' in y
                    end) 1 = 0
+ 
       ]]
 
       At this point, we want to apply the famous beta reduction of lambda calculus, to simplify the application of a known function abstraction. *)
 
   cbv beta.
   (** [[
-
   ============================
    match 1 with
    | 0 => 0
    | S n' => let y := n' in y
    end = 0
+ 
    ]]
 
    Next on the list is the iota reduction, which simplifies a single [match] term by determining which pattern matches. *)
 
   cbv iota.
   (** [[
-
   ============================
    (fun n' : nat => let y := n' in y) 0 = 0
+ 
       ]]
 
    Now we need another beta reduction. *)
 
   cbv beta.
   (** [[
-
   ============================
    (let y := 0 in y) = 0
+ 
       ]]
    
       The final reduction rule is zeta, which replaces a [let] expression by its body with the appropriate term subsituted. *)
 
   cbv zeta.
   (** [[
-
   ============================
    0 = 0
+ 
    ]] *)
 
   reflexivity.
@@ -99,7 +100,7 @@
 
 (** * Heterogeneous Lists Revisited *)
 
-(** One of our example dependent data structures from the last chapter was heterogeneous lists and their associated "cursor" type. *)
+(** One of our example dependent data structures from the last chapter was heterogeneous lists and their associated "cursor" type.  The recursive version poses some special challenges related to equality proofs, since it uses such proofs in its definition of [member] types. *)
 
 Section fhlist.
   Variable A : Type.
@@ -161,7 +162,6 @@
     (** Part of our single remaining subgoal is:
 
        [[
-   
   a0 : a = elm
   ============================
    match a0 in (_ = a2) return (C a2) with
@@ -169,31 +169,26 @@
    end = f match a0 in (_ = a2) return (B a2) with
            | refl_equal => a1
            end
+ 
        ]]
 
    This seems like a trivial enough obligation.  The equality proof [a0] must be [refl_equal], since that is the only constructor of [eq].  Therefore, both the [match]es reduce to the point where the conclusion follows by reflexivity.
 
     [[
-
     destruct a0.
 
-    ]]
-
-    [[
 User error: Cannot solve a second-order unification problem
+ 
 ]]
 
     This is one of Coq's standard error messages for informing us that its heuristics for attempting an instance of an undecidable problem about dependent typing have failed.  We might try to nudge things in the right direction by stating the lemma that we believe makes the conclusion trivial.
 
     [[
-
     assert (a0 = refl_equal _).
 
-    ]]
-
-    [[
 The term "refl_equal ?98" has type "?98 = ?98"
  while it is expected to have type "a = elm"
+ 
     ]]
 
     In retrospect, the problem is not so hard to see.  Reflexivity proofs only show [x = x] for particular values of [x], whereas here we are thinking in terms of a proof of [a = elm], where the two sides of the equality are not equal syntactically.  Thus, the essential lemma we need does not even type-check!
@@ -204,9 +199,9 @@
 
     case a0.
     (** [[
-
   ============================
    f a1 = f a1
+ 
    ]]
 
     It seems that [destruct] was trying to be too smart for its own good. *)
@@ -226,9 +221,7 @@
   (** [simple destruct pf] is a convenient form for applying [case].  It runs [intro] to bring into scope all quantified variables up to its argument. *)
 
   Print lemma1.
-
-  (** [[
-
+  (** %\vspace{-.15in}% [[
 lemma1 = 
 fun (x : A) (pf : x = elm) =>
 match pf as e in (_ = y) return (0 = match e with
@@ -239,6 +232,7 @@
      : forall (x : A) (pf : x = elm), 0 = match pf with
                                           | refl_equal => 0
                                           end
+ 
     ]]
 
     Using what we know about shorthands for [match] annotations, we can write this proof in shorter form manually. *)
@@ -258,14 +252,10 @@
   Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end.
 (* begin thide *)
     (** [[
-
     simple destruct pf.
 
-    ]]
-    
-      [[
-
 User error: Cannot solve a second-order unification problem
+ 
       ]] *)
   Abort.
 
@@ -286,33 +276,25 @@
   Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
 (* begin thide *)
     (** [[
-
     simple destruct pf.
 
-    ]]
-    
-      [[
-
 User error: Cannot solve a second-order unification problem
       ]] *)
+
   Abort.
 
   (** This time, even our manual attempt fails.
 
      [[
-
   Definition lemma3' :=
     fun (x : A) (pf : x = x) =>
       match pf as pf' in (_ = x') return (pf' = refl_equal x') with
         | refl_equal => refl_equal _
       end.
 
-      ]]
-
-     [[
-
 The term "refl_equal x'" has type "x' = x'" while it is expected to have type
  "x = x'"
+ 
      ]]
 
      The type error comes from our [return] annotation.  In that annotation, the [as]-bound variable [pf'] has type [x = x'], refering to the [in]-bound variable [x'].  To do a dependent [match], we %\textit{%#<i>#must#</i>#%}% choose a fresh name for the second argument of [eq].  We are just as constrained to use the "real" value [x] for the first argument.  Thus, within the [return] clause, the proof we are matching on %\textit{%#<i>#must#</i>#%}% equate two non-matching terms, which makes it impossible to equate that proof with reflexivity.
@@ -324,21 +306,21 @@
   Qed.
 
   Check UIP_refl.
-  (** [[
-
+  (** %\vspace{-.15in}% [[
 UIP_refl
      : forall (U : Type) (x : U) (p : x = x), p = refl_equal x
+ 
      ]]
 
      [UIP_refl] comes from the [Eqdep] module of the standard library.  Do the Coq authors know of some clever trick for building such proofs that we have not seen yet?  If they do, they did not use it for this proof.  Rather, the proof is based on an %\textit{%#<i>#axiom#</i>#%}%. *)
 
   Print eq_rect_eq.
-  (** [[
-
+  (** %\vspace{-.15in}% [[
 eq_rect_eq = 
 fun U : Type => Eq_rect_eq.eq_rect_eq U
      : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
        x = eq_rect p Q x p h
+ 
       ]]
 
       [eq_rect_eq] states a "fact" that seems like common sense, once the notation is deciphered.  [eq_rect] is the automatically-generated recursion principle for [eq].  Calling [eq_rect] is another way of [match]ing on an equality proof.  The proof we match on is the argument [h], and [x] is the body of the [match].  [eq_rect_eq] just says that [match]es on proofs of [p = p], for any [p], are superfluous and may be removed.
@@ -349,12 +331,12 @@
 
   Print Streicher_K.
 (* end thide *)
-(** [[
-
+(** %\vspace{-.15in}% [[
 Streicher_K = 
 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
      : forall (U : Type) (x : U) (P : x = x -> Prop),
        P (refl_equal x) -> forall p : x = x, P p
+ 
   ]]
 
   This is the unfortunately-named "Streicher's axiom K," which says that a predicate on properly-typed equality proofs holds of all such proofs if it holds of reflexivity. *)
@@ -370,9 +352,9 @@
   Variable A : Type.
   Variable B : A -> Type.
 
-  Fixpoint fhapp (ls1 ls2 : list A) {struct ls1}
+  Fixpoint fhapp (ls1 ls2 : list A)
     : fhlist B ls1 -> fhlist B ls2 -> fhlist B (ls1 ++ ls2) :=
-    match ls1 return fhlist _ ls1 -> _ -> fhlist _ (ls1 ++ ls2) with
+    match ls1 with
       | nil => fun _ hls2 => hls2
       | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)
     end.
@@ -385,19 +367,15 @@
   (** We might like to prove that [fhapp] is associative.
 
      [[
-
   Theorem fhapp_ass : forall ls1 ls2 ls3
     (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
     fhapp hls1 (fhapp hls2 hls3) = fhapp (fhapp hls1 hls2) hls3.
 
-    ]]
-
-     [[
-
 The term
  "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2)
     hls3" has type "fhlist B ((ls1 ++ ls2) ++ ls3)"
  while it is expected to have type "fhlist B (ls1 ++ ls2 ++ ls3)"
+ 
      ]]
 
      This first cut at the theorem statement does not even type-check.  We know that the two [fhlist] types appearing in the error message are always equal, by associativity of normal list append, but this fact is not apparent to the type checker.  This stems from the fact that Coq's equality is %\textit{%#<i>#intensional#</i>#%}%, in the sense that type equality theorems can never be applied after the fact to get a term to type-check.  Instead, we need to make use of equality explicitly in the theorem statement. *)
@@ -414,12 +392,12 @@
     (** The first remaining subgoal looks trivial enough:
 
        [[
-
   ============================
    fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
    match pf in (_ = ls) return (fhlist B ls) with
    | refl_equal => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
    end
+ 
        ]]
 
        We can try what worked in previous examples.
@@ -427,21 +405,18 @@
        [[
     case pf.
 
-    ]]
-
-       [[
-
 User error: Cannot solve a second-order unification problem
+ 
          ]]
 
         It seems we have reached another case where it is unclear how to use a dependent [match] to implement case analysis on our proof.  The [UIP_refl] theorem can come to our rescue again. *)
 
     rewrite (UIP_refl _ _ pf).
     (** [[
-
   ============================
    fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
    fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
+ 
         ]] *)
 
     reflexivity.
@@ -449,7 +424,6 @@
     (** Our second subgoal is trickier.
 
        [[
-
   pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
   ============================
    (a0,
@@ -461,25 +435,18 @@
        fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
          (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
    end
-       ]]
-
-
-       [[
 
     rewrite (UIP_refl _ _ pf).
 
-    ]]
-
-       [[
 The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3"
  while it is expected to have type "?556 = ?556"
+ 
        ]]
 
        We can only apply [UIP_refl] on proofs of equality with syntactically equal operands, which is not the case of [pf] here.  We will need to manipulate the form of this subgoal to get us to a point where we may use [UIP_refl].  A first step is obtaining a proof suitable to use in applying the induction hypothesis.  Inversion on the structure of [pf] is sufficient for that. *)
 
     injection pf; intro pf'.
     (** [[
-
   pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3
   pf' : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3
   ============================
@@ -492,13 +459,13 @@
        fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
          (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
    end
+ 
    ]]
 
    Now we can rewrite using the inductive hypothesis. *)
 
     rewrite (IHls1 _ _ pf').
     (** [[
-
   ============================
    (a0,
    match pf' in (_ = ls) return (fhlist B ls) with
@@ -512,13 +479,13 @@
        fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
          (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
    end
+ 
         ]]
 
         We have made an important bit of progress, as now only a single call to [fhapp] appears in the conclusion.  Trying case analysis on our proofs still will not work, but there is a move we can make to enable it.  Not only does just one call to [fhapp] matter to us now, but it also %\textit{%#<i>#does not matter what the result of the call is#</i>#%}%.  In other words, the subgoal should remain true if we replace this [fhapp] call with a fresh variable.  The [generalize] tactic helps us do exactly that. *)
 
     generalize (fhapp (fhapp b hls2) hls3).
     (** [[
-
    forall f : fhlist B ((ls1 ++ ls2) ++ ls3),
    (a0,
    match pf' in (_ = ls) return (fhlist B ls) with
@@ -527,6 +494,7 @@
    match pf in (_ = ls) return (fhlist B ls) with
    | refl_equal => (a0, f)
    end
+ 
         ]]
 
         The conclusion has gotten markedly simpler.  It seems counterintuitive that we can have an easier time of proving a more general theorem, but that is exactly the case here and for many other proofs that use dependent types heavily.  Speaking informally, the reason why this kind of activity helps is that [match] annotations only support variables in certain positions.  By reducing more elements of a goal to variables, built-in tactics can have more success building [match] terms under the hood.
@@ -535,7 +503,6 @@
 
     generalize pf pf'.
     (** [[
-
    forall (pf0 : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
      (pf'0 : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3)
      (f : fhlist B ((ls1 ++ ls2) ++ ls3)),
@@ -546,6 +513,7 @@
    match pf0 in (_ = ls) return (fhlist B ls) with
    | refl_equal => (a0, f)
    end
+ 
         ]]
 
         To an experienced dependent types hacker, the appearance of this goal term calls for a celebration.  The formula has a critical property that indicates that our problems are over.  To get our proofs into the right form to apply [UIP_refl], we need to use associativity of list append to rewrite their types.  We could not do that before because other parts of the goal require the proofs to retain their original types.  In particular, the call to [fhapp] that we generalized must have type [(ls1 ++ ls2) ++ ls3], for some values of the list variables.  If we rewrite the type of the proof used to type-cast this value to something like [ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3], then the lefthand side of the equality would no longer match the type of the term we are trying to cast.
@@ -554,7 +522,6 @@
 
     rewrite app_ass.
     (** [[
-
   ============================
    forall (pf0 : a :: ls1 ++ ls2 ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
      (pf'0 : ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3)
@@ -566,6 +533,7 @@
    match pf0 in (_ = ls) return (fhlist B ls) with
    | refl_equal => (a0, f)
    end
+ 
         ]]
 
         We can see that we have achieved the crucial property: the type of each generalized equality proof has syntactically equal operands.  This makes it easy to finish the proof with [UIP_refl]. *)
@@ -586,10 +554,10 @@
 (** There is another equality predicate, defined in the [JMeq] module of the standard library, implementing %\textit{%#<i>#heterogeneous equality#</i>#%}%. *)
 
 Print JMeq.
-(** [[
-
+(** %\vspace{-.15in}% [[
 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
     JMeq_refl : JMeq x x
+ 
     ]]
 
 [JMeq] stands for "John Major equality," a name coined by Conor McBride as a sort of pun about British politics.  [JMeq] starts out looking a lot like [eq].  The crucial difference is that we may use [JMeq] %\textit{%#<i>#on arguments of different types#</i>#%}%.  For instance, a lemma that we failed to establish before is trivial with [JMeq].  It makes for prettier theorem statements to define some syntactic shorthand first. *)
@@ -618,13 +586,13 @@
 (** All in all, refreshingly straightforward, but there really is no such thing as a free lunch.  The use of [rewrite] is implemented in terms of an axiom: *)
 
 Check JMeq_eq.
-(** [[
-
+(** %\vspace{-.15in}% [[
 JMeq_eq
      : forall (A : Type) (x y : A), x == y -> x = y
-    ]] *)
+ 
+    ]]
 
-(** It may be surprising that we cannot prove that heterogeneous equality implies normal equality.  The difficulties are the same kind we have seen so far, based on limitations of [match] annotations.
+    It may be surprising that we cannot prove that heterogeneous equality implies normal equality.  The difficulties are the same kind we have seen so far, based on limitations of [match] annotations.
 
    We can redo our [fhapp] associativity proof based around [JMeq]. *)
 
@@ -645,7 +613,6 @@
     (** Even better, [crush] discharges the first subgoal automatically.  The second subgoal is:
 
        [[
-
   ============================
    (a0,
    fhapp (B:=B) (ls1:=ls1) (ls2:=ls2 ++ ls3) b
@@ -653,20 +620,17 @@
    (a0,
    fhapp (B:=B) (ls1:=ls1 ++ ls2) (ls2:=ls3)
      (fhapp (B:=B) (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
+ 
        ]]
 
        It looks like one rewrite with the inductive hypothesis should be enough to make the goal trivial.
 
        [[
-
     rewrite IHls1.
 
-    ]]
-
-       [[
-
 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
  "fhlist B (ls1 ++ ?1572 ++ ?1573)"
+ 
        ]]
 
        We see that [JMeq] is not a silver bullet.  We can use it to simplify the statements of equality facts, but the Coq type-checker uses non-trivial heterogeneous equality facts no more readily than it uses standard equality facts.  Here, the problem is that the form [(e1, e2)] is syntactic sugar for an explicit application of a constructor of an inductive type.  That application mentions the type of each tuple element explicitly, and our [rewrite] tries to change one of those elements without updating the corresponding type argument.
@@ -677,19 +641,19 @@
       (fhapp (fhapp b hls2) hls3)
       (IHls1 _ _ b hls2 hls3).
     (** [[
-
   ============================
    forall (f : fhlist B (ls1 ++ ls2 ++ ls3))
      (f0 : fhlist B ((ls1 ++ ls2) ++ ls3)), f == f0 -> (a0, f) == (a0, f0)
+ 
         ]]
 
         Now we can rewrite with append associativity, as before. *)
 
     rewrite app_ass.
     (** [[
-
   ============================
    forall f f0 : fhlist B (ls1 ++ ls2 ++ ls3), f == f0 -> (a0, f) == (a0, f0)
+ 
        ]]
 
        From this point, the goal is trivial. *)
@@ -737,34 +701,34 @@
   x === y -> x = y.
   unfold JMeq'; intros.
   (** [[
-
   H : exists pf : A = A,
         x = match pf in (_ = T) return T with
             | refl_equal => y
             end
   ============================
    x = y
+ 
       ]] *)
 
   destruct H.
   (** [[
-
   x0 : A = A
   H : x = match x0 in (_ = T) return T with
           | refl_equal => y
           end
   ============================
    x = y
+ 
       ]] *)
 
   rewrite H.
   (** [[
-
   x0 : A = A
   ============================
    match x0 in (_ = T) return T with
    | refl_equal => y
    end = y
+ 
       ]] *)
 
   rewrite (UIP_refl _ _ x0); reflexivity.
@@ -779,9 +743,8 @@
 (** * Equality of Functions *)
 
 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[
-
    Theorem S_eta : S = (fun n => S n).
-
+ 
    ]]
 
    Unfortunately, this theorem is not provable in CIC without additional axioms.  None of the definitional equality rules force function equality to be %\textit{%#<i>#extensional#</i>#%}%.  That is, the fact that two functions return equal results on equal inputs does not imply that the functions are equal.  We %\textit{%#<i>#can#</i>#%}% assert function extensionality as an axiom. *)
@@ -820,7 +783,6 @@
                               | S _ => True
                             end) (fun _ => True)).
   (** [[
-
 2 subgoals
   
   ============================
@@ -833,7 +795,6 @@
                  end = True
       ]] *)
 
-
   reflexivity.
 
   destruct x; constructor.
@@ -855,6 +816,7 @@
   [[
 forall t' ts t (e : exp (t' :: ts) t) (e' : exp ts t') (s : hlist typeDenote ts),
   expDenote (subst e e') s = expDenote e (expDenote e' s ::: s)
+ 
   ]]
   where [:::] is an infix operator for heterogeneous "cons" that is defined in the book's [DepList] module.#</li>#
 #</ol>#%\end{enumerate}%