--- a/src/DataStruct.v	Wed Aug 01 16:09:37 2012 -0400
+++ b/src/DataStruct.v	Wed Aug 01 16:32:04 2012 -0400
@@ -44,7 +44,6 @@
   (** An instance of [fin] is essentially a more richly typed copy of the natural numbers.  Every element is a [First] iterated through applying [Next] a number of times that indicates which number is being selected.  For instance, the three values of type [fin 3] are [First 2], [Next (First 1)], and [Next (Next (First 0))].
 
      Now it is easy to pick a [Prop]-free type for a selection function.  As usual, our first implementation attempt will not convince the type checker, and we will attack the deficiencies one at a time.
-
      [[
   Fixpoint get n (ls : ilist n) : fin n -> A :=
     match ls with
@@ -55,11 +54,8 @@
           | Next _ idx' => get ls' idx'
         end
     end.
-
     ]]
-
-    We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses.  This still leaves us with a quandary in each of the [match] cases.  First, we need to figure out how to take advantage of the contradiction in the [Nil] case.  Every [fin] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case.  The solution we adopt is another case of [match]-within-[return].
-
+    %\vspace{-.15in}%We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses.  This still leaves us with a quandary in each of the [match] cases.  First, we need to figure out how to take advantage of the contradiction in the [Nil] case.  Every [fin] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case.  The solution we adopt is another case of [match]-within-[return].
     [[
   Fixpoint get n (ls : ilist n) : fin n -> A :=
     match ls with
@@ -77,13 +73,10 @@
           | Next _ idx' => get ls' idx'
         end
     end.
-
     ]]
-
-    Now the first [match] case type-checks, and we see that the problem with the [Cons] case is that the pattern-bound variable [idx'] does not have an apparent type compatible with [ls'].  In fact, the error message Coq gives for this exact code can be confusing, thanks to an overenthusiastic type inference heuristic.  We are told that the [Nil] case body has type [match X with | 0 => A | S _ => unit end] for a unification variable [X], while it is expected to have type [A].  We can see that setting [X] to [0] resolves the conflict, but Coq is not yet smart enough to do this unification automatically.  Repeating the function's type in a [return] annotation, used with an [in] annotation, leads us to a more informative error message, saying that [idx'] has type [fin n1] while it is expected to have type [fin n0], where [n0] is bound by the [Cons] pattern and [n1] by the [Next] pattern.  As the code is written above, nothing forces these two natural numbers to be equal, though we know intuitively that they must be.
+    %\vspace{-.15in}%Now the first [match] case type-checks, and we see that the problem with the [Cons] case is that the pattern-bound variable [idx'] does not have an apparent type compatible with [ls'].  In fact, the error message Coq gives for this exact code can be confusing, thanks to an overenthusiastic type inference heuristic.  We are told that the [Nil] case body has type [match X with | 0 => A | S _ => unit end] for a unification variable [X], while it is expected to have type [A].  We can see that setting [X] to [0] resolves the conflict, but Coq is not yet smart enough to do this unification automatically.  Repeating the function's type in a [return] annotation, used with an [in] annotation, leads us to a more informative error message, saying that [idx'] has type [fin n1] while it is expected to have type [fin n0], where [n0] is bound by the [Cons] pattern and [n1] by the [Next] pattern.  As the code is written above, nothing forces these two natural numbers to be equal, though we know intuitively that they must be.
 
     We need to use [match] annotations to make the relationship explicit.  Unfortunately, the usual trick of postponing argument binding will not help us here.  We need to match on both [ls] and [idx]; one or the other must be matched first.  To get around this, we apply the convoy pattern that we met last chapter.  This application is a little more clever than those we saw before; we use the natural number predecessor function [pred] to express the relationship between the types of these variables.
-
     [[
   Fixpoint get n (ls : ilist n) : fin n -> A :=
     match ls with
@@ -101,10 +94,8 @@
           | Next _ idx' => fun ls' => get ls' idx'
         end ls'
     end.
-
     ]]
-
-    There is just one problem left with this implementation.  Though we know that the local [ls'] in the [Next] case is equal to the original [ls'], the type-checker is not satisfied that the recursive call to [get] does not introduce non-termination.  We solve the problem by convoy-binding the partial application of [get] to [ls'], rather than [ls'] by itself. *)
+    %\vspace{-.15in}%There is just one problem left with this implementation.  Though we know that the local [ls'] in the [Next] case is equal to the original [ls'], the type-checker is not satisfied that the recursive call to [get] does not introduce non-termination.  We solve the problem by convoy-binding the partial application of [get] to [ls'], rather than [ls'] by itself. *)
 
   Fixpoint get n (ls : ilist n) : fin n -> A :=
     match ls with
@@ -285,6 +276,8 @@
 Example somePairs : hlist (fun T : Set => T * T)%type someTypes :=
   MCons (1, 2) (MCons (true, false) MNil).
 
+(** There are many more useful applications of heterogeneous lists, based on different choices of the first argument to [hlist]. *)
+
 (* end thide *)
 
 
@@ -444,7 +437,6 @@
   (** The definition of [fmember] follows the definition of [ffin].  Empty lists have no members, and member types for nonempty lists are built by adding one new option to the type of members of the list tail.  While for [ffin] we needed no new information associated with the option that we add, here we need to know that the head of the list equals the element we are searching for.  We express that with a sum type whose left branch is the appropriate equality proposition.  Since we define [fmember] to live in [Type], we can insert [Prop] types as needed, because [Prop] is a subtype of [Type].
 
      We know all of the tricks needed to write a first attempt at a [get] function for [fhlist]s.
-
      [[
   Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
     match ls with
@@ -455,10 +447,8 @@
           | inr idx' => fhget ls' (snd mls) idx'
         end
     end.
-
     ]]
-
-    Only one problem remains.  The expression [fst mls] is not known to have the proper type.  To demonstrate that it does, we need to use the proof available in the [inl] case of the inner [match]. *)
+    %\vspace{-.15in}%Only one problem remains.  The expression [fst mls] is not known to have the proper type.  To demonstrate that it does, we need to use the proof available in the [inl] case of the inner [match]. *)
 
   Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
     match ls with
@@ -483,7 +473,6 @@
   Print eq.
   (** %\vspace{-.15in}% [[
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
- 
 ]]
 
 In a proposition [x = y], we see that [x] is a parameter and [y] is a regular argument.  The type of the constructor [eq_refl] shows that [y] can only ever be instantiated to [x].  Thus, within a pattern-match with [eq_refl], occurrences of [y] can be replaced with occurrences of [x] for typing purposes. *)
@@ -555,7 +544,6 @@
        (forall a : A, P (Leaf a)) ->
        (forall (n : nat) (i : ilist (tree A) n), P (Node i)) ->
        forall t : tree A, P t
- 
 ]]
 
 The automatically generated induction principle is too weak.  For the [Node] case, it gives us no inductive hypothesis.  We could write our own induction principle, as we did in Chapter 3, but there is an easier way, if we are willing to alter the definition of [tree]. *)
@@ -713,6 +701,27 @@
 
 (** Now the expression interpreter is straightforward to write. *)
 
+(* begin thide *)
+Fixpoint exp'Denote t (e : exp' t) : type'Denote t :=
+  match e with
+    | NConst n => n
+    | Plus e1 e2 => exp'Denote e1 + exp'Denote e2
+    | Eq e1 e2 =>
+      if eq_nat_dec (exp'Denote e1) (exp'Denote e2) then true else false
+
+    | BConst b => b
+    | Cond _ _ tests bodies default =>
+      cond
+      (exp'Denote default)
+      (fun idx => exp'Denote (tests idx))
+      (fun idx => exp'Denote (bodies idx))
+  end.
+(* begin hide *)
+Reset exp'Denote.
+(* end hide *)
+(* end thide *)
+
+(* begin hide *)
 Fixpoint exp'Denote t (e : exp' t) : type'Denote t :=
   match e with
     | NConst n => n
@@ -729,6 +738,7 @@
       (fun idx => exp'Denote (bodies idx))
 (* end thide *)
   end.
+(* end hide *)
 
 (** We will implement a constant-folding function that optimizes conditionals, removing cases with known-[false] tests and cases that come after known-[true] tests.  A function [cfoldCond] implements the heart of this logic.  The convoy pattern is used again near the end of the implementation. *)
 
@@ -821,7 +831,8 @@
         specialize (IHn (fun idx => tests (Some idx)) (fun idx => bodies (Some idx)))
     end;
     repeat (match goal with
-              | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] => dep_destruct E
+              | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] =>
+                dep_destruct E
               | [ |- context[if ?B then _ else _] ] => destruct B
             end; crush).
 Qed.

--- a/src/MoreDep.v	Wed Aug 01 16:09:37 2012 -0400
+++ b/src/MoreDep.v	Wed Aug 01 16:32:04 2012 -0400
@@ -87,18 +87,14 @@
 (* EX: Implement statically checked "car"/"hd" *)
 
 (** Now let us attempt a function that is surprisingly tricky to write.  In ML, the list head function raises an exception when passed an empty list.  With length-indexed lists, we can rule out such invalid calls statically, and here is a first attempt at doing so.  We write [???] as a placeholder for a term that we do not know how to write, not for any real Coq notation like those introduced two chapters ago.
-
 [[
 Definition hd n (ls : ilist (S n)) : A :=
   match ls with
     | Nil => ???
     | Cons _ h _ => h
   end.
- 
 ]]
-
 It is not clear what to write for the [Nil] case, so we are stuck before we even turn our function over to the type checker.  We could try omitting the [Nil] case:
-
 [[
 Definition hd n (ls : ilist (S n)) : A :=
   match ls with
@@ -141,7 +137,6 @@
                                   | 0 => unit
                                   | S _ => A
                                   end
- 
   ]]
   *)
 
@@ -243,7 +238,6 @@
 (** Despite the fancy type, the function definition is routine.  In fact, it is less complicated than what we would write in ML or Haskell 98, since we do not need to worry about pushing final values in and out of an algebraic datatype.  The only unusual thing is the use of an expression of the form [if E then true else false] in the [Eq] case.  Remember that [eq_nat_dec] has a rich dependent type, rather than a simple boolean type.  Coq's native [if] is overloaded to work on a test of any two-constructor type, so we can use [if] to build a simple boolean from the [sumbool] that [eq_nat_dec] returns.
 
    We can implement our old favorite, a constant folding function, and prove it correct.  It will be useful to write a function [pairOut] that checks if an [exp] of [Prod] type is a pair, returning its two components if so.  Unsurprisingly, a first attempt leads to a type error.
-
 [[
 Definition pairOut t1 t2 (e : exp (Prod t1 t2)) : option (exp t1 * exp t2) :=
   match e in (exp (Prod t1 t2)) return option (exp t1 * exp t2) with
@@ -374,7 +368,6 @@
      ]]
 
      We would like to do a case analysis on [cfold e1], and we attempt that in the way that has worked so far.
-
      [[
   destruct (cfold e1).
 ]]
@@ -537,14 +530,14 @@
 (** Insertion relies on two balancing operations.  It will be useful to give types to these operations using a relative of the subset types from last chapter.  While subset types let us pair a value with a proof about that value, here we want to pair a value with another non-proof dependently typed value.  The %\index{Gallina terms!sigT}%[sigT] type fills this role. *)
 
 Locate "{ _ : _ & _ }".
-(** [[
+(** %\vspace{-.15in}%[[
 Notation            Scope     
 "{ x : A  & P }" := sigT (fun x : A => P)
 ]]
 *)
 
 Print sigT.
-(** [[
+(** %\vspace{-.15in}%[[
 Inductive sigT (A : Type) (P : A -> Type) : Type :=
     existT : forall x : A, P x -> sigT P
 ]]