# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1257967727 18000
# Node ID d1464997078dbf0d1db6838b11c5ef4220203970
# Parent  f8bcd33bdd91aa5fb6df8cf5ab82637b8c8566cd
Switch DepList to inductive, not recursive, types

diff -r f8bcd33bdd91 -r d1464997078d src/DataStruct.v
--- a/src/DataStruct.v	Wed Nov 11 14:00:04 2009 -0500
+++ b/src/DataStruct.v	Wed Nov 11 14:28:47 2009 -0500
@@ -841,7 +841,7 @@
 
 (** remove printing * *)
 
-(** Some of the type family definitions from this chapter are duplicated in the [DepList] module of the book source.  Only the recursive versions of length-indexed and heterogeneous lists are included, and they are renamed without the [f] prefixes, e.g., [ilist] in place of [filist].
+(** Some of the type family definitions and associated functions from this chapter are duplicated in the [DepList] module of the book source.  Some of their names have been changed to be more sensible in a general context.
 
 %\begin{enumerate}%#<ol>#
 
diff -r f8bcd33bdd91 -r d1464997078d src/DepList.v
--- a/src/DepList.v	Wed Nov 11 14:00:04 2009 -0500
+++ b/src/DepList.v	Wed Nov 11 14:28:47 2009 -0500
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2009, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -17,56 +17,68 @@
 Section ilist.
   Variable A : Type.
 
-  Fixpoint ilist (n : nat) : Type :=
-    match n with
-      | O => unit
-      | S n' => A * ilist n'
-    end%type.
+  Inductive ilist : nat -> Type :=
+  | INil : ilist O
+  | ICons : forall n, A -> ilist n -> ilist (S n).
 
-  Definition inil : ilist O := tt.
-  Definition icons n x (ls : ilist n) : ilist (S n) := (x, ls).
-
-  Definition hd n (ls : ilist (S n)) : A := fst ls.
-  Definition tl n (ls : ilist (S n)) : ilist n := snd ls.
-
-  Implicit Arguments icons [n].
-
-  Fixpoint fin (n : nat) : Type :=
-    match n with
-      | O => Empty_set
-      | S n' => option (fin n')
+  Definition hd n (ls : ilist (S n)) :=
+    match ls in ilist n' return match n' with
+                                  | O => unit
+                                  | S _ => A
+                                end with
+      | INil => tt
+      | ICons _ x _ => x
+    end.
+  Definition tl n (ls : ilist (S n)) :=
+    match ls in ilist n' return match n' with
+                                  | O => unit
+                                  | S n => ilist n
+                                end with
+      | INil => tt
+      | ICons _ _ ls' => ls'
     end.
 
-  Fixpoint get (n : nat) : ilist n -> fin n -> A :=
-    match n return ilist n -> fin n -> A with
-      | O => fun _ idx => match idx with end
-      | S n' => fun ls idx =>
-        match idx with
-          | None => fst ls
-          | Some idx' => get n' (snd ls) idx'
+  Inductive fin : nat -> Set :=
+  | First : forall n, fin (S n)
+  | Next : forall n, fin n -> fin (S n).
+
+  Fixpoint get n (ls : ilist n) : fin n -> A :=
+    match ls with
+      | INil => fun idx =>
+        match idx in fin n' return (match n' with
+                                        | O => A
+                                        | S _ => unit
+                                      end) with
+          | First _ => tt
+          | Next _ _ => tt
         end
+      | ICons _ x ls' => fun idx =>
+        match idx in fin n' return (fin (pred n') -> A) -> A with
+          | First _ => fun _ => x
+          | Next _ idx' => fun get_ls' => get_ls' idx'
+        end (get ls')
     end.
 
   Section everywhere.
     Variable x : A.
 
     Fixpoint everywhere (n : nat) : ilist n :=
-      match n return ilist n with
-        | O => inil
-        | S n' => icons x (everywhere n')
+      match n with
+        | O => INil
+        | S n' => ICons x (everywhere n')
       end.
   End everywhere.
 
   Section singleton.
     Variables x default : A.
 
-    Fixpoint singleton (n m : nat) {struct n} : ilist n :=
-      match n return ilist n with
-        | O => inil
+    Fixpoint singleton (n m : nat) : ilist n :=
+      match n with
+        | O => INil
         | S n' =>
           match m with
-            | O => icons x (everywhere default n')
-            | S m' => icons default (singleton n' m')
+            | O => ICons x (everywhere default n')
+            | S m' => ICons default (singleton n' m')
           end
       end.
   End singleton.
@@ -74,10 +86,10 @@
   Section map2.
     Variable f : A -> A -> A.
 
-    Fixpoint map2 (n : nat) : ilist n -> ilist n -> ilist n :=
-      match n return ilist n -> ilist n -> ilist n with
-        | O => fun _ _ => inil
-        | S n' => fun ls1 ls2 => icons (f (hd ls1) (hd ls2)) (map2 _ (tl ls1) (tl ls2))
+    Fixpoint map2 n (il1 : ilist n) : ilist n -> ilist n :=
+      match il1 in ilist n return ilist n -> ilist n with
+        | INil => fun _ => INil
+        | ICons _ x il1' => fun il2 => ICons (f x (hd il2)) (map2 il1' (tl il2))
       end.
   End map2.
 
@@ -86,107 +98,112 @@
     Variable f : A -> B -> B.
     Variable i : B.
 
-    Fixpoint foldr (n : nat) : ilist n -> B :=
-      match n return ilist n -> B with
-        | O => fun _ => i
-        | S n' => fun ils => f (hd ils) (foldr n' (tl ils))
+    Fixpoint foldr n (il : ilist n) : B :=
+      match il with
+        | INil => i
+        | ICons _ x il' => f x (foldr il')
       end.
   End fold.
 End ilist.
 
-Implicit Arguments inil [A].
-Implicit Arguments icons [A n].
-
-Implicit Arguments icons [A n].
-Implicit Arguments get [A n].
-Implicit Arguments map2 [A n].
-Implicit Arguments foldr [A B n].
+Implicit Arguments INil [A].
+Implicit Arguments First [n].
 
 Section imap.
   Variables A B : Type.
   Variable f : A -> B.
 
-  Fixpoint imap (n : nat) : ilist A n -> ilist B n :=
-    match n return ilist A n -> ilist B n with
-      | O => fun _ => inil
-      | S n' => fun ls => icons (f (hd ls)) (imap _ (tl ls))
+  Fixpoint imap n (il : ilist A n) : ilist B n :=
+    match il with
+      | INil => INil
+      | ICons _ x il' => ICons (f x) (imap il')
     end.
 End imap.
 
-Implicit Arguments imap [A B n].
-
 Section hlist.
   Variable A : Type.
   Variable B : A -> Type.
 
-  Fixpoint hlist (ls : list A) : Type :=
-    match ls with
-      | nil => unit
-      | x :: ls' => B x * hlist ls'
-    end%type.
+  Inductive hlist : list A -> Type :=
+  | HNil : hlist nil
+  | HCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
 
-  Definition hnil : hlist nil := tt.
-  Definition hcons (x : A) (ls : list A) (v : B x) (hls : hlist ls) : hlist (x :: ls) :=
-    (v, hls).
+  Definition hhd ls (hl : hlist ls) :=
+    match hl in hlist ls return match ls with
+                                  | nil => unit
+                                  | x :: _ => B x
+                                end with
+      | HNil => tt
+      | HCons _ _ v _ => v
+    end.
+
+  Definition htl ls (hl : hlist ls) :=
+    match hl in hlist ls return match ls with
+                                  | nil => unit
+                                  | _ :: ls' => hlist ls'
+                                end with
+      | HNil => tt
+      | HCons _ _ _ hl' => hl'
+    end.
 
   Variable elm : A.
 
-  Fixpoint member (ls : list A) : Type :=
-    match ls with
-      | nil => Empty_set
-      | x :: ls' => (x = elm) + member ls'
-    end%type.
+  Inductive member : list A -> Type :=
+  | HFirst : forall ls, member (elm :: ls)
+  | HNext : forall x ls, member ls -> member (x :: ls).
 
-  Definition hfirst (x : A) (ls : list A) (pf : x = elm) : member (x :: ls) :=
-    inl _ pf.
-  Definition hnext (x : A) (ls : list A) (m : member ls) : member (x :: ls) :=
-    inr _ m.
-
-  Fixpoint hget (ls : list A) : hlist ls -> member ls -> B elm :=
-    match ls return hlist ls -> member ls -> B elm with
-      | nil => fun _ idx => match idx with end
-      | _ :: ls' => fun mls idx =>
-        match idx with
-          | inl pf => match pf with
-                        | refl_equal => fst mls
-                      end
-          | inr idx' => hget ls' (snd mls) idx'
+  Fixpoint hget ls (mls : hlist ls) : member ls -> B elm :=
+    match mls with
+      | HNil => fun mem =>
+        match mem in member ls' return (match ls' with
+                                          | nil => B elm
+                                          | _ :: _ => unit
+                                        end) with
+          | HFirst _ => tt
+          | HNext _ _ _ => tt
         end
+      | HCons _ _ x mls' => fun mem =>
+        match mem in member ls' return (match ls' with
+                                          | nil => Empty_set
+                                          | x' :: ls'' =>
+                                            B x' -> (member ls'' -> B elm) -> B elm
+                                        end) with
+          | HFirst _ => fun x _ => x
+          | HNext _ _ mem' => fun _ get_mls' => get_mls' mem'
+        end x (hget mls')
     end.
 
-  Fixpoint happ (ls1 ls2 : list A) {struct ls1} : hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) :=
-    match ls1 return hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) with
-      | nil => fun _ hls2 => hls2
-      | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2)
+  Fixpoint happ (ls1 : list A) (hl1 : hlist ls1) : forall ls2, hlist ls2 -> hlist (ls1 ++ ls2) :=
+    match hl1 in hlist ls1 return forall ls2, hlist ls2 -> hlist (ls1 ++ ls2) with
+      | HNil => fun _ hl2 => hl2
+      | HCons _ _ x hl1' => fun _ hl2 => HCons x (happ hl1' hl2)
     end.
 
   Variable f : forall x, B x.
 
   Fixpoint hmake (ls : list A) : hlist ls :=
-    match ls return hlist ls with
-      | nil => hnil
-      | x :: ls' => hcons _ (f x) (hmake ls')
+    match ls with
+      | nil => HNil
+      | x :: ls' => HCons (f x) (hmake ls')
     end.
 
-  Implicit Arguments hget [ls].
-
   Theorem hget_hmake : forall ls (m : member ls),
     hget (hmake ls) m = f elm.
-    induction ls; crush.
-    case a0; reflexivity.
+    induction ls; crush;
+      match goal with
+        | [ |- context[match ?E with HFirst _ => _ | HNext _ _ _ => _ end] ] => dep_destruct E
+      end; crush.
   Qed.
 End hlist.
 
-Implicit Arguments hnil [A B].
-Implicit Arguments hcons [A B x ls].
-Implicit Arguments hget [A B elm ls].
-Implicit Arguments happ [A B ls1 ls2].
+Implicit Arguments HNil [A B].
+Implicit Arguments HCons [A B x ls].
 Implicit Arguments hmake [A B].
 
-Implicit Arguments hfirst [A elm x ls].
-Implicit Arguments hnext [A elm x ls].
+Implicit Arguments HFirst [A elm ls].
+Implicit Arguments HNext [A elm x ls].
 
-Infix ":::" := hcons (right associativity, at level 60).
+Infix ":::" := HCons (right associativity, at level 60).
 Infix "+++" := happ (right associativity, at level 60).
 
 Section hmap.
@@ -195,23 +212,23 @@
 
   Variable f : forall x, B1 x -> B2 x.
 
-  Fixpoint hmap (ls : list A) : hlist B1 ls -> hlist B2 ls :=
-    match ls return hlist B1 ls -> hlist B2 ls with
-      | nil => fun _ => hnil
-      | _ :: _ => fun hl => f (fst hl) ::: hmap _ (snd hl)
+  Fixpoint hmap (ls : list A) (hl : hlist B1 ls) : hlist B2 ls :=
+    match hl with
+      | HNil => HNil
+      | HCons _ _ x hl' => f x ::: hmap hl'
     end.
 
-  Implicit Arguments hmap [ls].
-
   Theorem hmap_happ : forall ls2 (h2 : hlist B1 ls2) ls1 (h1 : hlist B1 ls1),
     hmap h1 +++ hmap h2 = hmap (h1 +++ h2).
-    induction ls1; crush.
+    induction h1; crush.
   Qed.
 
   Theorem hget_hmap : forall elm ls (hls : hlist B1 ls) (m : member elm ls),
     hget (hmap hls) m = f (hget hls m).
-    induction ls; crush.
-    case a1; crush.
+    induction hls; crush;
+      match goal with
+        | [ |- context[match ?E with HFirst _ => _ | HNext _ _ _ => _ end] ] => dep_destruct E
+      end; crush.
   Qed.
 End hmap.
 
diff -r f8bcd33bdd91 -r d1464997078d src/Extensional.v
--- a/src/Extensional.v	Wed Nov 11 14:00:04 2009 -0500
+++ b/src/Extensional.v	Wed Nov 11 14:28:47 2009 -0500
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2009, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -499,7 +499,7 @@
 
     Fixpoint patDenote t ts (p : pat t ts) {struct p} : typeDenote t -> option (hlist typeDenote ts) :=
       match p in (pat t ts) return (typeDenote t -> option (hlist typeDenote ts)) with
-        | PVar _ => fun v => Some (v, tt)
+        | PVar _ => fun v => Some (v ::: HNil)
         | PPair _ _ _ _ p1 p2 => fun v =>
           match patDenote p1 (fst v), patDenote p2 (snd v) with
             | Some tup1, Some tup2 => Some (happ tup1 tup2)
@@ -525,18 +525,18 @@
         : (forall ts, member ts tss -> option (hlist typeDenote ts))
         -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
         -> typeDenote t2 :=
-        match tss return (forall ts, member ts tss -> _)
-          -> (forall ts, member ts tss -> _)
+        match tss return (forall ts, member ts tss -> option (hlist typeDenote ts))
+          -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
           -> _ with
           | nil => fun _ _ =>
             default
           | ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss') -> option (hlist typeDenote ts'))
             (bodies : forall ts', member ts' (ts :: tss') -> hlist typeDenote ts' -> typeDenote t2) =>
-            match envs _ (hfirst (refl_equal _)) with
-              | None => matchesDenote tss'
-                (fun _ mem => envs _ (hnext mem))
-                (fun _ mem => bodies _ (hnext mem))
-              | Some env => (bodies _ (hfirst (refl_equal _))) env
+            match envs _ HFirst with
+              | None => matchesDenote
+                (fun _ mem => envs _ (HNext mem))
+                (fun _ mem => bodies _ (HNext mem))
+              | Some env => (bodies _ HFirst) env
             end
         end.
     End matchesDenote.
@@ -735,23 +735,23 @@
       match p in (pat t1 ts) return ((hlist (exp var) ts -> result)
         -> result -> choice_tree var t1 result) with
         | PVar _ => fun succ fail =>
-          everywhere (fun disc => succ (disc, tt))
+          everywhere (fun disc => succ (disc ::: HNil))
 
         | PPair _ _ _ _ p1 p2 => fun succ fail =>
-          elaboratePat _ p1
+          elaboratePat p1
           (fun tup1 =>
-            elaboratePat _ p2
+            elaboratePat p2
             (fun tup2 =>
               succ (happ tup1 tup2))
             fail)
           (everywhere (fun _ => fail))
 
         | PInl _ _ _ p' => fun succ fail =>
-          (elaboratePat _ p' succ fail,
+          (elaboratePat p' succ fail,
             everywhere (fun _ => fail))
         | PInr _ _ _ p' => fun succ fail =>
           (everywhere (fun _ => fail),
-            elaboratePat _ p' succ fail)
+            elaboratePat p' succ fail)
       end.
 
     Implicit Arguments elaboratePat [var t1 ts result].
@@ -760,8 +760,8 @@
       -> hlist (exp var) ts -> exp var t :=
       match ts return ((hlist var ts -> exp var t)
         -> hlist (exp var) ts -> exp var t) with
-        | nil => fun f _ => f tt
-        | _ :: _ => fun f tup => letify _ (fun tup' => x <- fst tup; f (x, tup')) (snd tup)
+        | nil => fun f _ => f HNil
+        | _ :: _ => fun f tup => letify (fun tup' => x <- hhd tup; f (x ::: tup')) (htl tup)
       end.
 
     Implicit Arguments letify [var t ts].
@@ -809,14 +809,14 @@
         | ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts')
           (es : forall ts', member ts' (ts :: tss') -> hlist var ts' -> Elab.exp var t2) =>
           merge (@mergeOpt _)
-          (elaboratePat (ps _ (hfirst (refl_equal _)))
+          (elaboratePat (ps _ HFirst)
             (fun ts => Some (letify
-              (fun ts' => es _ (hfirst (refl_equal _)) ts')
+              (fun ts' => es _ HFirst ts')
               ts))
             None)
-          (elaborateMatches tss'
-            (fun _ mem => ps _ (hnext mem))
-            (fun _ mem => es _ (hnext mem)))
+          (elaborateMatches
+            (fun _ mem => ps _ (HNext mem))
+            (fun _ mem => es _ (HNext mem)))
       end.
 
     Implicit Arguments elaborateMatches [var t1 t2 tss].
@@ -926,7 +926,7 @@
     result (succ : hlist (Elab.exp typeDenote) ts -> result)
     (fail : result) v env,
     patDenote p v = Some env
-    -> exists env', grab (elaboratePat typeDenote p succ fail) v = succ env'
+    -> exists env', grab (elaboratePat p succ fail) v = succ env'
       /\ env = hmap Elab.expDenote env'.
     Hint Resolve hmap_happ.
 
@@ -935,11 +935,11 @@
                 | [ |- context[grab (everywhere ?succ) ?v] ] =>
                   generalize (everywhere_correct succ (#v)%elab)
 
-                | [ H : forall result sudc fail, _ |- context[grab (elaboratePat _ _ ?S ?F) ?V] ] =>
+                | [ H : forall result succ fail, _ |- context[grab (elaboratePat _ ?S ?F) ?V] ] =>
                   generalize (H _ S F V); clear H
                 | [ H1 : context[match ?E with Some _ => _ | None => _ end],
-                  H2 : forall env, ?E = Some env -> _ |- _ ] =>
-                destruct E
+                    H2 : forall env, ?E = Some env -> _ |- _ ] =>
+                  destruct E
                 | [ H : forall env, Some ?E = Some env -> _ |- _ ] =>
                   generalize (H _ (refl_equal _)); clear H
               end; crush); eauto.
@@ -949,14 +949,14 @@
     result (succ : hlist (Elab.exp typeDenote) ts -> result)
     (fail : result) v,
     patDenote p v = None
-    -> grab (elaboratePat typeDenote p succ fail) v = fail.
+    -> grab (elaboratePat p succ fail) v = fail.
     Hint Resolve everywhere_fail.
 
     induction p; try solve [ crush ];
       simpl; fold choice_tree; intuition; simpl in *;
         repeat match goal with
                  | [ IH : forall result succ fail v, patDenote ?P v = _ -> _
-                   |- context[grab (elaboratePat _ ?P ?S ?F) ?V] ] =>
+                   |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
                    generalize (IH _ S F V); clear IH; intro IH;
                      generalize (elaboratePat_correct P S F V); intros;
                        destruct (patDenote P V); try discriminate
@@ -973,7 +973,7 @@
     (env : hlist (Elab.exp typeDenote) ts),
     Elab.expDenote (letify f env)
     = Elab.expDenote (f (hmap Elab.expDenote env)).
-    induction ts; crush.
+    induction ts; crush; dep_destruct env; crush.
   Qed.
 
   Theorem elaborate_correct : forall t (e : Source.exp typeDenote t),
@@ -986,7 +986,7 @@
         | [ tss : list (list type) |- _ ] =>
           induction tss; crush;
             match goal with
-              | [ |- context[grab (elaboratePat _ ?P ?S ?F) ?V] ] =>
+              | [ |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
                 case_eq (patDenote P V); [intros env Heq;
                   destruct (elaboratePat_correct P S F _ Heq); crush;
                     match goal with
diff -r f8bcd33bdd91 -r d1464997078d src/Generic.v
--- a/src/Generic.v	Wed Nov 11 14:00:04 2009 -0500
+++ b/src/Generic.v	Wed Nov 11 14:28:47 2009 -0500
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2009, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -70,17 +70,17 @@
 
 (* begin thide *)
 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt :=
-  hnil.
+  HNil.
 Definition unit_den : datatypeDenote unit unit_dt :=
-  [!, ! ~> tt] ::: hnil.
+  [!, ! ~> tt] ::: HNil.
 Definition bool_den : datatypeDenote bool bool_dt :=
-  [!, ! ~> true] ::: [!, ! ~> false] ::: hnil.
+  [!, ! ~> true] ::: [!, ! ~> false] ::: HNil.
 Definition nat_den : datatypeDenote nat nat_dt :=
-  [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: hnil.
+  [!, ! ~> O] ::: [!, r # 1 ~> S (hd r)] ::: HNil.
 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) :=
-  [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: hnil.
+  [!, ! ~> nil] ::: [x, r # 1 ~> x :: hd r] ::: HNil.
 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
-  [v, ! ~> Leaf v] ::: [!, r # 2 ~> Node (hd r) (hd (tl r))] ::: hnil.
+  [v, ! ~> Leaf v] ::: [!, r # 2 ~> Node (hd r) (hd (tl r))] ::: HNil.
 (* end thide *)
 
 
@@ -100,36 +100,36 @@
 Eval compute in size Empty_set_fix.
 
 Definition unit_fix : fixDenote unit unit_dt :=
-  fun R cases _ => (fst cases) tt inil.
+  fun R cases _ => (hhd cases) tt INil.
 Eval compute in size unit_fix.
 
 Definition bool_fix : fixDenote bool bool_dt :=
   fun R cases b => if b
-    then (fst cases) tt inil
-    else (fst (snd cases)) tt inil.
+    then (hhd cases) tt INil
+    else (hhd (htl cases)) tt INil.
 Eval compute in size bool_fix.
 
 Definition nat_fix : fixDenote nat nat_dt :=
   fun R cases => fix F (n : nat) : R :=
     match n with
-      | O => (fst cases) tt inil
-      | S n' => (fst (snd cases)) tt (icons (F n') inil)
+      | O => (hhd cases) tt INil
+      | S n' => (hhd (htl cases)) tt (ICons (F n') INil)
     end.
 Eval cbv beta iota delta -[plus] in size nat_fix.
 
 Definition list_fix (A : Type) : fixDenote (list A) (list_dt A) :=
   fun R cases => fix F (ls : list A) : R :=
     match ls with
-      | nil => (fst cases) tt inil
-      | x :: ls' => (fst (snd cases)) x (icons (F ls') inil)
+      | nil => (hhd cases) tt INil
+      | x :: ls' => (hhd (htl cases)) x (ICons (F ls') INil)
     end.
 Eval cbv beta iota delta -[plus] in fun A => size (@list_fix A).
 
 Definition tree_fix (A : Type) : fixDenote (tree A) (tree_dt A) :=
   fun R cases => fix F (t : tree A) : R :=
     match t with
-      | Leaf x => (fst cases) x inil
-      | Node t1 t2 => (fst (snd cases)) tt (icons (F t1) (icons (F t2) inil))
+      | Leaf x => (hhd cases) x INil
+      | Node t1 t2 => (hhd (htl cases)) tt (ICons (F t1) (ICons (F t2) INil))
     end.
 Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A).
 (* end thide *)
@@ -157,15 +157,15 @@
       ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr).
 (* end thide *)
 
-Eval compute in print hnil Empty_set_fix.
-Eval compute in print (^ "tt" (fun _ => "") ::: hnil) unit_fix.
+Eval compute in print HNil Empty_set_fix.
+Eval compute in print (^ "tt" (fun _ => "") ::: HNil) unit_fix.
 Eval compute in print (^ "true" (fun _ => "")
   ::: ^ "false" (fun _ => "")
-  ::: hnil) bool_fix.
+  ::: HNil) bool_fix.
 
 Definition print_nat := print (^ "O" (fun _ => "")
   ::: ^ "S" (fun _ => "")
-  ::: hnil) nat_fix.
+  ::: HNil) nat_fix.
 Eval cbv beta iota delta -[append] in print_nat.
 Eval simpl in print_nat 0.
 Eval simpl in print_nat 1.
@@ -174,11 +174,11 @@
 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
   print (^ "nil" (fun _ => "")
   ::: ^ "cons" pr
-  ::: hnil) (@list_fix A).
+  ::: HNil) (@list_fix A).
 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
   print (^ "Leaf" pr
   ::: ^ "Node" (fun _ => "")
-  ::: hnil) (@tree_fix A).
+  ::: HNil) (@tree_fix A).
 
 
 (** ** Mapping *)
@@ -225,16 +225,15 @@
     forall (R : Type) (cases : datatypeDenote R dt)
       c (m : member c dt)
       (x : nonrecursive c) (r : ilist T (recursive c)),
-      fx R cases ((hget dd m) x r)
-      = (hget cases m) x (imap (fx R cases) r).
+      fx cases ((hget dd m) x r)
+      = (hget cases m) x (imap (fx cases) r).
 End ok.
 
 Implicit Arguments datatypeDenoteOk [T dt].
 
 Lemma foldr_plus : forall n (ils : ilist nat n),
   foldr plus 1 ils > 0.
-  induction n; crush.
-  generalize (IHn b); crush.
+  induction ils; crush.
 Qed.
 (* end thide *)
 
@@ -265,12 +264,11 @@
   end; crush.
 
   induction (recursive c); crush.
-  destruct r; reflexivity.
-  destruct r; crush.
-  rewrite (H None).
-  unfold icons.
+  dep_destruct r; reflexivity.
+  dep_destruct r; crush.
+  rewrite (H First).
   f_equal.
   apply IHn; crush.
-  apply (H (Some i0)).
+  apply (H (Next i)).
 Qed.
 (* end thide *)