changeset 204:cbf2f74a5130

Parts I want to keep compile with 8.2
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 10:52:43 -0500
parents 71ade09024ac
children f05514cc6c0d
files .hgignore Makefile html/.dir src/DataStruct.v src/Extensional.v src/Impure.v src/Intensional.v src/Interps.v src/Match.v src/MoreDep.v src/Subset.v src/Tactics.v
diffstat 11 files changed, 41 insertions(+), 1519 deletions(-) [+]
line wrap: on
line diff
--- a/.hgignore	Sun Jan 04 08:18:59 2009 -0500
+++ b/.hgignore	Fri Nov 06 10:52:43 2009 -0500
@@ -18,3 +18,6 @@
 
 staging/html/.dir
 cpdt.tgz
+
+*.glob
+*.v.d
--- a/Makefile	Sun Jan 04 08:18:59 2009 -0500
+++ b/Makefile	Fri Nov 06 10:52:43 2009 -0500
@@ -1,4 +1,4 @@
-MODULES_NODOC := Axioms AxiomsImpred Tactics MoreSpecif DepList
+MODULES_NODOC := Axioms Tactics MoreSpecif DepList
 MODULES_PROSE := Intro
 MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset \
 	MoreDep DataStruct Equality Match Reflection Firstorder Hoas Interps \
@@ -17,7 +17,7 @@
 
 Makefile.coq: Makefile $(VS)
 	coq_makefile $(VS) \
-		COQC = "coqc -impredicative-set -I src -dump-glob $(GLOBALS)" \
+		COQC = "coqc -I src -dump-glob $(GLOBALS)" \
 		COQDEP = "coqdep -I src" \
 		-o Makefile.coq
 
--- a/src/DataStruct.v	Sun Jan 04 08:18:59 2009 -0500
+++ b/src/DataStruct.v	Fri Nov 06 10:52:43 2009 -0500
@@ -699,7 +699,7 @@
     match n return (findex n -> exp' Bool) -> (findex n -> exp' t) -> exp' t with
       | O => fun _ _ => default
       | S n' => fun tests bodies =>
-        match tests None with
+        match tests None return _ with
           | BConst true => bodies None
           | BConst false => cfoldCond n'
             (fun idx => tests (Some idx))
@@ -743,14 +743,14 @@
     | Plus e1 e2 =>
       let e1' := cfold e1 in
       let e2' := cfold e2 in
-      match e1', e2' with
+      match e1', e2' return _ with
         | NConst n1, NConst n2 => NConst (n1 + n2)
         | _, _ => Plus e1' e2'
       end
     | Eq e1 e2 =>
       let e1' := cfold e1 in
       let e2' := cfold e2 in
-      match e1', e2' with
+      match e1', e2' return _ with
         | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
         | _, _ => Eq e1' e2'
       end
--- a/src/Extensional.v	Sun Jan 04 08:18:59 2009 -0500
+++ b/src/Extensional.v	Fri Nov 06 10:52:43 2009 -0500
@@ -963,6 +963,7 @@
                  | [ H : forall env, Some _ = Some env -> _ |- _ ] =>
                    destruct (H _ (refl_equal _)); clear H; intuition
                  | [ H : _ |- _ ] => rewrite H; intuition
+                 | [ |- context[match ?v with inl _ => _ | inr _ => _ end] ] => destruct v; auto
                end.
   Qed.
 
--- a/src/Impure.v	Sun Jan 04 08:18:59 2009 -0500
+++ b/src/Impure.v	Fri Nov 06 10:52:43 2009 -0500
@@ -7,232 +7,8 @@
  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
  *)
 
-(* begin hide *)
-Require Import Arith List Omega.
-
-Require Import Axioms Tactics.
-
-Set Implicit Arguments.
-(* end hide *)
 
 
 (** %\chapter{Modeling Impure Languages}% *)
 
-(** TODO: Prose for this chapter *)
-
-Section var.
-  Variable var : Type.
-
-  Inductive term : Type :=
-  | Var : var -> term
-  | App : term -> term -> term
-  | Abs : (var -> term) -> term
-  | Unit : term.
-End var.
-
-Implicit Arguments Unit [var].
-
-Notation "# v" := (Var v) (at level 70).
-Notation "()" := Unit.
-
-Infix "@" := App (left associativity, at level 72).
-Notation "\ x , e" := (Abs (fun x => e)) (at level 73).
-Notation "\ ? , e" := (Abs (fun _ => e)) (at level 73).
-
-Definition Term := forall var, term var.
-
-Definition ident : Term := fun _ => \x, #x.
-Definition unite : Term := fun _ => ().
-Definition ident_self : Term := fun _ => ident _ @ ident _.
-Definition ident_unit : Term := fun _ => ident _ @ unite _.
-
-
-Module impredicative.
-  Inductive dynamic : Set :=
-  | Dyn : forall (dynTy : Type), dynTy -> dynamic.
-
-  Inductive computation (T : Type) : Set :=
-  | Return : T -> computation T
-  | Bind : forall (T' : Type),
-    computation T' -> (T' -> computation T) -> computation T
-  | Unpack : dynamic -> computation T.
-
-  Inductive eval : forall T, computation T -> T -> Prop :=
-  | EvalReturn : forall T (v : T),
-    eval (Return v) v
-  | EvalUnpack : forall T (v : T),
-    eval (Unpack T (Dyn v)) v
-  | EvalBind : forall T1 T2 (c1 : computation T1) (c2 : T1 -> computation T2) v1 v2,
-    eval c1 v1
-    -> eval (c2 v1) v2
-    -> eval (Bind c1 c2) v2.
-
-(* begin thide *)
-  Fixpoint termDenote (e : term dynamic) : computation dynamic :=
-    match e with
-      | Var v => Return v
-      | App e1 e2 => Bind (termDenote e1) (fun f =>
-        Bind (termDenote e2) (fun x =>
-          Bind (Unpack (dynamic -> computation dynamic) f) (fun f' =>
-            f' x)))
-      | Abs e' => Return (Dyn (fun x => termDenote (e' x)))
-
-      | Unit => Return (Dyn tt)
-    end.
-(* end thide *)
-
-  Definition TermDenote (E : Term) := termDenote (E _).
-
-  Eval compute in TermDenote ident.
-  Eval compute in TermDenote unite.
-  Eval compute in TermDenote ident_self.
-  Eval compute in TermDenote ident_unit.
-
-  Theorem eval_ident_unit : eval (TermDenote ident_unit) (Dyn tt).
-(* begin thide *)
-    compute.
-    repeat econstructor.
-    simpl.
-    constructor.
-  Qed.
-(* end thide *)
-
-  Theorem invert_ident : forall (E : Term) d,
-    eval (TermDenote (fun _ => ident _ @ E _)) d
-    -> eval (TermDenote E) d.
-(* begin thide *)
-    inversion 1.
-
-    crush.
-
-    Focus 3.
-    crush.
-    unfold TermDenote in H0.
-    simpl in H0.
-    (** [injection H0.] *)
-  Abort.
-(* end thide *)
-
-End impredicative.
-
-
-Module predicative.
-
-  Inductive val : Type :=
-  | Func : nat -> val
-  | VUnit.
-
-  Inductive computation : Type :=
-  | Return : val -> computation
-  | Bind : computation -> (val -> computation) -> computation
-  | CAbs : (val -> computation) -> computation
-  | CApp : val -> val -> computation.
-
-  Definition func := val -> computation.
-
-  Fixpoint get (n : nat) (ls : list func) {struct ls} : option func :=
-    match ls with
-      | nil => None
-      | x :: ls' =>
-        if eq_nat_dec n (length ls')
-          then Some x
-          else get n ls'
-    end.
-
-  Inductive eval : list func -> computation -> list func -> val -> Prop :=
-  | EvalReturn : forall ds d,
-    eval ds (Return d) ds d
-  | EvalBind : forall ds c1 c2 ds' d1 ds'' d2,
-    eval ds c1 ds' d1
-    -> eval ds' (c2 d1) ds'' d2
-    -> eval ds (Bind c1 c2) ds'' d2
-  | EvalCAbs : forall ds f,
-    eval ds (CAbs f) (f :: ds) (Func (length ds))
-  | EvalCApp : forall ds i d2 f ds' d3,
-    get i ds = Some f
-    -> eval ds (f d2) ds' d3
-    -> eval ds (CApp (Func i) d2) ds' d3.
-
-(* begin thide *)
-  Fixpoint termDenote (e : term val) : computation :=
-    match e with
-      | Var v => Return v
-      | App e1 e2 => Bind (termDenote e1) (fun f =>
-        Bind (termDenote e2) (fun x =>
-          CApp f x))
-      | Abs e' => CAbs (fun x => termDenote (e' x))
-
-      | Unit => Return VUnit
-    end.
-(* end thide *)
-
-  Definition TermDenote (E : Term) := termDenote (E _).
-
-  Eval compute in TermDenote ident.
-  Eval compute in TermDenote unite.
-  Eval compute in TermDenote ident_self.
-  Eval compute in TermDenote ident_unit.
-
-  Theorem eval_ident_unit : exists ds, eval nil (TermDenote ident_unit) ds VUnit.
-(* begin thide *)
-    compute.
-    repeat econstructor.
-    simpl.
-    rewrite (eta Return).
-    reflexivity.
-  Qed.
-
-  Hint Constructors eval.
-
-  Lemma app_nil_start : forall A (ls : list A),
-    ls = nil ++ ls.
-    reflexivity.
-  Qed.
-
-  Lemma app_cons : forall A (x : A) (ls : list A),
-    x :: ls = (x :: nil) ++ ls.
-    reflexivity.
-  Qed.
-
-  Theorem eval_monotone : forall ds c ds' d,
-    eval ds c ds' d
-    -> exists ds'', ds' = ds'' ++ ds.
-    Hint Resolve app_nil_start app_ass app_cons.
-
-    induction 1; firstorder; subst; eauto.
-  Qed.
-
-  Lemma length_app : forall A (ds2 ds1 : list A),
-    length (ds1 ++ ds2) = length ds1 + length ds2.
-    induction ds1; simpl; intuition.
-  Qed.
-
-  Lemma get_app : forall ds2 d ds1,
-    get (length ds2) (ds1 ++ d :: ds2) = Some d.
-    Hint Rewrite length_app : cpdt.
-
-    induction ds1; crush;
-      match goal with
-        | [ |- context[if ?E then _ else _] ] => destruct E
-      end; crush.
-  Qed.
-(* end thide *)
-
-  Theorem invert_ident : forall (E : Term) ds ds' d,
-    eval ds (TermDenote (fun _ => ident _ @ E _)) ds' d
-    -> eval ((fun x => Return x) :: ds) (TermDenote E) ds' d.
-(* begin thide *)
-    inversion 1; subst.
-    clear H.
-    inversion H3; clear H3; subst.
-    inversion H6; clear H6; subst.
-    generalize (eval_monotone H2); crush.
-    inversion H5; clear H5; subst.
-    rewrite get_app in H3.
-    inversion H3; clear H3; subst.
-    inversion H7; clear H7; subst.
-    assumption.
-  Qed.
-(* end thide *)
-
-End predicative.
+(** TODO: This chapter!  (Old version was too impredicative) *)
--- a/src/Intensional.v	Sun Jan 04 08:18:59 2009 -0500
+++ b/src/Intensional.v	Fri Nov 06 10:52:43 2009 -0500
@@ -7,1078 +7,7 @@
  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
  *)
 
-(* begin hide *)
-Require Import Arith Bool String List Eqdep JMeq.
-
-Require Import Axioms Tactics DepList.
-
-Set Implicit Arguments.
-
-Infix "==" := JMeq (at level 70, no associativity).
-(* end hide *)
-
-
-
 
 (** %\chapter{Intensional Transformations}% *)
 
-(** TODO: Prose for this chapter *)
-
-
-(** * Closure Conversion *)
-
-Module Source.
-  Inductive type : Type :=
-  | TNat : type
-  | Arrow : type -> type -> type.
-
-  Notation "'Nat'" := TNat : source_scope.
-  Infix "-->" := Arrow (right associativity, at level 60) : source_scope.
-
-  Open Scope source_scope.
-  Bind Scope source_scope with type.
-  Delimit Scope source_scope with source.
-
-  Section vars.
-    Variable var : type -> Type.
-
-    Inductive exp : type -> Type :=
-    | Var : forall t,
-      var t
-      -> exp t
-
-    | Const : nat -> exp Nat
-    | Plus : exp Nat -> exp Nat -> exp Nat
-
-    | App : forall t1 t2,
-      exp (t1 --> t2)
-      -> exp t1
-      -> exp t2
-    | Abs : forall t1 t2,
-      (var t1 -> exp t2)
-      -> exp (t1 --> t2).
-  End vars.
-
-  Definition Exp t := forall var, exp var t.
-
-  Implicit Arguments Var [var t].
-  Implicit Arguments Const [var].
-  Implicit Arguments Plus [var].
-  Implicit Arguments App [var t1 t2].
-  Implicit Arguments Abs [var t1 t2].
-
-  Notation "# v" := (Var v) (at level 70) : source_scope.
-
-  Notation "^ n" := (Const n) (at level 70) : source_scope.
-  Infix "+^" := Plus (left associativity, at level 79) : source_scope.
-
-  Infix "@" := App (left associativity, at level 77) : source_scope.
-  Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
-  Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope.
-
-  Bind Scope source_scope with exp.
-
-  Definition zero : Exp Nat := fun _ => ^0.
-  Definition one : Exp Nat := fun _ => ^1.
-  Definition zpo : Exp Nat := fun _ => zero _ +^ one _.
-  Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x.
-  Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
-  Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
-    \f, \x, #f @ #x.
-  Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
-
-  Fixpoint typeDenote (t : type) : Set :=
-    match t with
-      | Nat => nat
-      | t1 --> t2 => typeDenote t1 -> typeDenote t2
-    end.
-
-  Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
-    match e in (exp _ t) return (typeDenote t) with
-      | Var _ v => v
-        
-      | Const n => n
-      | Plus e1 e2 => expDenote e1 + expDenote e2
-        
-      | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
-      | Abs _ _ e' => fun x => expDenote (e' x)
-    end.
-
-  Definition ExpDenote t (e : Exp t) := expDenote (e _).
-
-  Section exp_equiv.
-    Variables var1 var2 : type -> Type.
-
-    Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop :=
-    | EqVar : forall G t (v1 : var1 t) v2,
-      In (existT _ t (v1, v2)) G
-      -> exp_equiv G (#v1) (#v2)
-
-    | EqConst : forall G n,
-      exp_equiv G (^n) (^n)
-    | EqPlus : forall G x1 y1 x2 y2,
-      exp_equiv G x1 x2
-      -> exp_equiv G y1 y2
-      -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
-
-    | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
-      exp_equiv G f1 f2
-      -> exp_equiv G x1 x2
-      -> exp_equiv G (f1 @ x1) (f2 @ x2)
-    | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
-      (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
-      -> exp_equiv G (Abs f1) (Abs f2).
-  End exp_equiv.
-
-  Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
-    exp_equiv nil (E var1) (E var2).
-End Source.
-
-Module Closed.
-  Inductive type : Type :=
-  | TNat : type
-  | Arrow : type -> type -> type
-  | Code : type -> type -> type -> type
-  | Prod : type -> type -> type
-  | TUnit : type.
-
-  Notation "'Nat'" := TNat : cc_scope.
-  Notation "'Unit'" := TUnit : cc_scope.
-  Infix "-->" := Arrow (right associativity, at level 60) : cc_scope.
-  Infix "**" := Prod (right associativity, at level 59) : cc_scope.
-  Notation "env @@ dom ---> ran" := (Code env dom ran) (no associativity, at level 62, dom at next level) : cc_scope.
-
-  Bind Scope cc_scope with type.
-  Delimit Scope cc_scope with cc.
-
-  Open Local Scope cc_scope.
-
-  Section vars.
-    Variable var : type -> Set.
-
-    Inductive exp : type -> Type :=
-    | Var : forall t,
-      var t
-      -> exp t
-
-    | Const : nat -> exp Nat
-    | Plus : exp Nat -> exp Nat -> exp Nat
-
-    | App : forall dom ran,
-      exp (dom --> ran)
-      -> exp dom
-      -> exp ran
-
-    | Pack : forall env dom ran,
-      exp (env @@ dom ---> ran)
-      -> exp env
-      -> exp (dom --> ran)
-
-    | EUnit : exp Unit
-
-    | Pair : forall t1 t2,
-      exp t1
-      -> exp t2
-      -> exp (t1 ** t2)
-    | Fst : forall t1 t2,
-      exp (t1 ** t2)
-      -> exp t1
-    | Snd : forall t1 t2,
-      exp (t1 ** t2)
-      -> exp t2
-
-    | Let : forall t1 t2,
-      exp t1
-      -> (var t1 -> exp t2)
-      -> exp t2.
-
-    Section funcs.
-      Variable T : Type.
-
-      Inductive funcs : Type :=
-      | Main : T -> funcs
-      | Abs : forall env dom ran,
-        (var env -> var dom -> exp ran)
-        -> (var (env @@ dom ---> ran) -> funcs)
-        -> funcs.
-    End funcs.
-
-    Definition prog t := funcs (exp t).
-  End vars.
-
-  Implicit Arguments Var [var t].
-  Implicit Arguments Const [var].
-  Implicit Arguments EUnit [var].
-  Implicit Arguments Fst [var t1 t2].
-  Implicit Arguments Snd [var t1 t2].
-
-  Implicit Arguments Main [var T].
-  Implicit Arguments Abs [var T env dom ran].
-
-  Notation "# v" := (Var v) (at level 70) : cc_scope.
-
-  Notation "^ n" := (Const n) (at level 70) : cc_scope.
-  Infix "+^" := Plus (left associativity, at level 79) : cc_scope.
-
-  Infix "@" := App (left associativity, at level 77) : cc_scope.
-  Infix "##" := Pack (no associativity, at level 71) : cc_scope.
-
-  Notation "()" := EUnit : cc_scope.
-
-  Notation "[ x1 , x2 ]" := (Pair x1 x2) (at level 73) : cc_scope.
-  Notation "#1 x" := (Fst x) (at level 72) : cc_scope.
-  Notation "#2 x" := (Snd x) (at level 72) : cc_scope.
-
-  Notation "f <== \\ x , y , e ; fs" :=
-    (Abs (fun x y => e) (fun f => fs))
-    (right associativity, at level 80, e at next level) : cc_scope.
-  Notation "f <== \\ ! , y , e ; fs" :=
-    (Abs (fun _ y => e) (fun f => fs))
-    (right associativity, at level 80, e at next level) : cc_scope.
-  Notation "f <== \\ x , ! , e ; fs" :=
-    (Abs (fun x _ => e) (fun f => fs))
-    (right associativity, at level 80, e at next level) : cc_scope.
-  Notation "f <== \\ ! , ! , e ; fs" :=
-    (Abs (fun _ _ => e) (fun f => fs))
-    (right associativity, at level 80, e at next level) : cc_scope.
-
-  Notation "x <- e1 ; e2" := (Let e1 (fun x => e2))
-    (right associativity, at level 80, e1 at next level) : cc_scope.
-
-  Bind Scope cc_scope with exp funcs prog.
-
-  Fixpoint typeDenote (t : type) : Set :=
-    match t with
-      | Nat => nat
-      | Unit => unit
-      | dom --> ran => typeDenote dom -> typeDenote ran
-      | t1 ** t2 => typeDenote t1 * typeDenote t2
-      | env @@ dom ---> ran => typeDenote env -> typeDenote dom -> typeDenote ran
-    end%type.
-
-  Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
-    match e in (exp _ t) return (typeDenote t) with
-      | Var _ v => v
-
-      | Const n => n
-      | Plus e1 e2 => expDenote e1 + expDenote e2
-
-      | App _ _ f x => (expDenote f) (expDenote x)
-      | Pack _ _ _ f env => (expDenote f) (expDenote env)
-
-      | EUnit => tt
-
-      | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
-      | Fst _ _ e' => fst (expDenote e')
-      | Snd _ _ e' => snd (expDenote e')
-
-      | Let _ _ e1 e2 => expDenote (e2 (expDenote e1))
-    end.
-
-  Fixpoint funcsDenote T (fs : funcs typeDenote T) : T :=
-    match fs with
-      | Main v => v
-      | Abs _ _ _ e fs =>
-        funcsDenote (fs (fun env arg => expDenote (e env arg)))
-    end.
-
-  Definition progDenote t (p : prog typeDenote t) : typeDenote t :=
-    expDenote (funcsDenote p).
-
-  Definition Exp t := forall var, exp var t.
-  Definition Prog t := forall var, prog var t.
-
-  Definition ExpDenote t (E : Exp t) := expDenote (E _).
-  Definition ProgDenote t (P : Prog t) := progDenote (P _).
-End Closed.
-
-Import Source Closed.
-
-Section splice.
-  Open Local Scope cc_scope.
-
-  Fixpoint spliceFuncs var T1 (fs : funcs var T1)
-    T2 (f : T1 -> funcs var T2) {struct fs} : funcs var T2 :=
-    match fs with
-      | Main v => f v
-      | Abs _ _ _ e fs' => Abs e (fun x => spliceFuncs (fs' x) f)
-    end.
-End splice.
-
-Notation "x <-- e1 ; e2" := (spliceFuncs e1 (fun x => e2))
-  (right associativity, at level 80, e1 at next level) : cc_scope.
-
-Definition natvar (_ : Source.type) := nat.
-Definition isfree := hlist (fun (_ : Source.type) => bool).
-
-Ltac maybe_destruct E :=
-  match goal with
-    | [ x : _ |- _ ] =>
-      match E with
-        | x => idtac
-      end
-    | _ =>
-      match E with
-        | eq_nat_dec _ _ => idtac
-      end
-  end; destruct E.
-
-Ltac my_crush :=
-  crush; repeat (match goal with
-                   | [ x : (_ * _)%type |- _ ] => destruct x
-                   | [ |- context[if ?B then _ else _] ] => maybe_destruct B
-                   | [ _ : context[if ?B then _ else _] |- _ ] => maybe_destruct B
-                 end; crush).
-
-Section isfree.
-  Import Source.
-  Open Local Scope source_scope.
-
-  Fixpoint lookup_type (envT : list Source.type) (n : nat) {struct envT}
-    : isfree envT -> option Source.type :=
-    match envT return (isfree envT -> _) with
-      | nil => fun _ => None
-      | first :: rest => fun fvs =>
-        if eq_nat_dec n (length rest)
-          then match fvs with
-                 | (true, _) => Some first
-                 | (false, _) => None
-               end
-          else lookup_type rest n (snd fvs)
-    end.
-  
-  Implicit Arguments lookup_type [envT].
-
-  Notation ok := (fun (envT : list Source.type) (fvs : isfree envT)
-    (n : nat) (t : Source.type)
-    => lookup_type n fvs = Some t).
-
-  Fixpoint wfExp (envT : list Source.type) (fvs : isfree envT)
-    t (e : Source.exp natvar t) {struct e} : Prop :=
-    match e with
-      | Var t v => ok envT fvs v t
-
-      | Const _ => True
-      | Plus e1 e2 => wfExp envT fvs e1 /\ wfExp envT fvs e2
-
-      | App _ _ e1 e2 => wfExp envT fvs e1 /\ wfExp envT fvs e2
-      | Abs dom _ e' => wfExp (dom :: envT) (true ::: fvs) (e' (length envT))
-    end.
-
-  Implicit Arguments wfExp [envT t].
-
-  Theorem wfExp_weaken : forall t (e : exp natvar t) envT (fvs fvs' : isfree envT),
-    wfExp fvs e
-    -> (forall n t, ok _ fvs n t -> ok _ fvs' n t)
-    -> wfExp fvs' e.
-    Hint Extern 1 (lookup_type (envT := _ :: _) _ _ = Some _) =>
-      simpl in *; my_crush.
-
-    induction e; my_crush; eauto.
-  Defined.
-
-  Fixpoint isfree_none (envT : list Source.type) : isfree envT :=
-    match envT return (isfree envT) with
-      | nil => tt
-      | _ :: _ => (false, isfree_none _)
-    end.
-
-  Implicit Arguments isfree_none [envT].
-
-  Fixpoint isfree_one (envT : list Source.type) (n : nat) {struct envT} : isfree envT :=
-    match envT return (isfree envT) with
-      | nil => tt
-      | _ :: rest =>
-        if eq_nat_dec n (length rest)
-          then (true, isfree_none)
-          else (false, isfree_one _ n)
-    end.
-
-  Implicit Arguments isfree_one [envT].
-
-  Fixpoint isfree_merge (envT : list Source.type) : isfree envT -> isfree envT -> isfree envT :=
-    match envT return (isfree envT -> isfree envT -> isfree envT) with
-      | nil => fun _ _ => tt
-      | _ :: _ => fun fv1 fv2 => (fst fv1 || fst fv2, isfree_merge _ (snd fv1) (snd fv2))
-    end.
-
-  Implicit Arguments isfree_merge [envT].
-
-  Fixpoint fvsExp t (e : exp natvar t)
-    (envT : list Source.type) {struct e} : isfree envT :=
-    match e with
-      | Var _ n => isfree_one n
-
-      | Const _ => isfree_none
-      | Plus e1 e2 => isfree_merge (fvsExp e1 envT) (fvsExp e2 envT)
-
-      | App _ _ e1 e2 => isfree_merge (fvsExp e1 envT) (fvsExp e2 envT)
-      | Abs dom _ e' => snd (fvsExp (e' (length envT)) (dom :: envT))
-    end.
-
-  Lemma isfree_one_correct : forall t (v : natvar t) envT fvs,
-    ok envT fvs v t
-    -> ok envT (isfree_one (envT:=envT) v) v t.
-    induction envT; my_crush; eauto.
-  Defined.
-
-  Lemma isfree_merge_correct1 : forall t (v : natvar t) envT fvs1 fvs2,
-    ok envT fvs1 v t
-    -> ok envT (isfree_merge (envT:=envT) fvs1 fvs2) v t.
-    induction envT; my_crush; eauto.
-  Defined.
-
-  Hint Rewrite orb_true_r : cpdt.
-
-  Lemma isfree_merge_correct2 : forall t (v : natvar t) envT fvs1 fvs2,
-    ok envT fvs2 v t
-    -> ok envT (isfree_merge (envT:=envT) fvs1 fvs2) v t.
-    induction envT; my_crush; eauto.
-  Defined.
-
-  Hint Resolve isfree_one_correct isfree_merge_correct1 isfree_merge_correct2.
-  
-  Lemma fvsExp_correct : forall t (e : exp natvar t)
-    envT (fvs : isfree envT), wfExp fvs e
-    -> forall (fvs' : isfree envT),
-      (forall v t, ok envT (fvsExp e envT) v t -> ok envT fvs' v t)
-      -> wfExp fvs' e.
-    Hint Extern 1 (_ = _) =>
-      match goal with
-        | [ H : lookup_type _ (fvsExp ?X ?Y) = _ |- _ ] =>
-          destruct (fvsExp X Y); my_crush
-      end.
-
-    induction e; my_crush; eauto.
-  Defined.
-
-  Lemma lookup_type_unique : forall v t1 t2 envT (fvs1 fvs2 : isfree envT),
-    lookup_type v fvs1 = Some t1
-    -> lookup_type v fvs2 = Some t2
-    -> t1 = t2.
-    induction envT; my_crush; eauto.
-  Defined.
-
-  Implicit Arguments lookup_type_unique [v t1 t2 envT fvs1 fvs2].
-
-  Hint Extern 2 (lookup_type _ _ = Some _) =>
-    match goal with
-      | [ H1 : lookup_type ?v _ = Some _,
-        H2 : lookup_type ?v _ = Some _ |- _ ] =>
-      (generalize (lookup_type_unique H1 H2); intro; subst)
-      || rewrite <- (lookup_type_unique H1 H2)
-    end.
-
-  Lemma lookup_none : forall v t envT,
-    lookup_type (envT:=envT) v (isfree_none (envT:=envT)) = Some t
-    -> False.
-    induction envT; my_crush.
-  Defined.
-
-  Hint Extern 2 (_ = _) => elimtype False; eapply lookup_none; eassumption.
-
-  Lemma lookup_one : forall v' v t envT,
-    lookup_type (envT:=envT) v' (isfree_one (envT:=envT) v) = Some t
-    -> v' = v.
-    induction envT; my_crush.
-  Defined.
-
-  Implicit Arguments lookup_one [v' v t envT].
-
-  Hint Extern 2 (lookup_type _ _ = Some _) =>
-    match goal with
-      | [ H : lookup_type _ _ = Some _ |- _ ] =>
-        generalize (lookup_one H); intro; subst
-    end.
-
-  Lemma lookup_merge : forall v t envT (fvs1 fvs2 : isfree envT),
-    lookup_type v (isfree_merge fvs1 fvs2) = Some t
-    -> lookup_type v fvs1 = Some t
-    \/ lookup_type v fvs2 = Some t.
-    induction envT; my_crush.
-  Defined.
-
-  Implicit Arguments lookup_merge [v t envT fvs1 fvs2].
-
-  Lemma lookup_bound : forall v t envT (fvs : isfree envT),
-    lookup_type v fvs = Some t
-    -> v < length envT.
-    Hint Resolve lt_S.
-    induction envT; my_crush; eauto.
-  Defined.
-
-  Hint Resolve lookup_bound.
-
-  Lemma lookup_bound_contra : forall t envT (fvs : isfree envT),
-    lookup_type (length envT) fvs = Some t
-    -> False.
-    intros; assert (length envT < length envT); eauto; crush.
-  Defined.
-
-  Hint Resolve lookup_bound_contra.
-
-  Lemma lookup_push_drop : forall v t t' envT fvs,
-    v < length envT
-    -> lookup_type (envT := t :: envT) v (true, fvs) = Some t'
-    -> lookup_type (envT := envT) v fvs = Some t'.
-    my_crush.
-  Defined.
-
-  Lemma lookup_push_add : forall v t t' envT fvs,
-    lookup_type (envT := envT) v (snd fvs) = Some t'
-    -> lookup_type (envT := t :: envT) v fvs = Some t'.
-    my_crush; elimtype False; eauto.
-  Defined.
-
-  Hint Resolve lookup_bound lookup_push_drop lookup_push_add.
-
-  Theorem fvsExp_minimal : forall t (e : exp natvar t)
-    envT (fvs : isfree envT), wfExp fvs e
-    -> (forall v t, ok envT (fvsExp e envT) v t -> ok envT fvs v t).
-    Hint Extern 1 (_ = _) =>
-      match goal with
-        | [ H : lookup_type _ (isfree_merge _ _) = Some _ |- _ ] =>
-          destruct (lookup_merge H); clear H; eauto
-      end.
-
-    induction e; my_crush; eauto.
-  Defined.
-
-  Fixpoint ccType (t : Source.type) : Closed.type :=
-    match t with
-      | Nat%source => Nat
-      | (dom --> ran)%source => ccType dom --> ccType ran
-    end%cc.
-
-  Open Local Scope cc_scope.
-
-  Fixpoint envType (envT : list Source.type) : isfree envT -> Closed.type :=
-    match envT return (isfree envT -> _) with
-      | nil => fun _ => Unit
-      | t :: _ => fun tup =>
-        if fst tup
-          then ccType t ** envType _ (snd tup)
-          else envType _ (snd tup)
-    end.
-
-  Implicit Arguments envType [envT].
-
-  Fixpoint envOf (var : Closed.type -> Set) (envT : list Source.type) {struct envT}
-    : isfree envT -> Set :=
-    match envT return (isfree envT -> _) with
-      | nil => fun _ => unit
-      | first :: rest => fun fvs =>
-        match fvs with
-          | (true, fvs') => (var (ccType first) * envOf var rest fvs')%type
-          | (false, fvs') => envOf var rest fvs'
-        end
-    end.
-
-  Implicit Arguments envOf [envT].
-
-  Notation "var <| to" := (match to with
-                             | None => unit
-                             | Some t => var (ccType t)
-                           end) (no associativity, at level 70).
-
-  Fixpoint lookup (var : Closed.type -> Set) (envT : list Source.type) :
-    forall (n : nat) (fvs : isfree envT), envOf var fvs -> var <| lookup_type n fvs :=
-      match envT return (forall (n : nat) (fvs : isfree envT), envOf var fvs
-        -> var <| lookup_type n fvs) with
-        | nil => fun _ _ _ => tt
-        | first :: rest => fun n fvs =>
-          match (eq_nat_dec n (length rest)) as Heq return
-            (envOf var (envT := first :: rest) fvs
-              -> var <| (if Heq
-                then match fvs with
-                       | (true, _) => Some first
-                       | (false, _) => None
-                     end
-                else lookup_type n (snd fvs))) with
-            | left _ =>
-              match fvs return (envOf var (envT := first :: rest) fvs
-                -> var <| (match fvs with
-                             | (true, _) => Some first
-                             | (false, _) => None
-                           end)) with
-                | (true, _) => fun env => fst env
-                | (false, _) => fun _ => tt
-              end
-            | right _ =>
-              match fvs return (envOf var (envT := first :: rest) fvs
-                -> var <| (lookup_type n (snd fvs))) with
-                | (true, fvs') => fun env => lookup var rest n fvs' (snd env)
-                | (false, fvs') => fun env => lookup var rest n fvs' env
-              end
-          end
-      end.
-
-  Theorem lok : forall var n t envT (fvs : isfree envT),
-    lookup_type n fvs = Some t
-    -> var <| lookup_type n fvs = var (ccType t).
-    crush.
-  Defined.
-End isfree.
-
-Implicit Arguments lookup_type [envT].
-Implicit Arguments lookup [envT fvs].
-Implicit Arguments wfExp [t envT].
-Implicit Arguments envType [envT].
-Implicit Arguments envOf [envT].
-Implicit Arguments lok [var n t envT fvs].
-
-Section lookup_hints.
-  Hint Resolve lookup_bound_contra.
-
-  Hint Resolve lookup_bound_contra.
-
-  Lemma lookup_type_push : forall t' envT (fvs1 fvs2 : isfree envT) b1 b2,
-    (forall (n : nat) (t : Source.type),
-      lookup_type (envT := t' :: envT) n (b1, fvs1) = Some t ->
-      lookup_type (envT := t' :: envT) n (b2, fvs2) = Some t)
-    -> (forall (n : nat) (t : Source.type),
-      lookup_type n fvs1 = Some t ->
-      lookup_type n fvs2 = Some t).
-    intros until b2; intro H; intros n t;
-      generalize (H n t); my_crush; elimtype False; eauto.
-  Defined.
-
-  Lemma lookup_type_push_contra : forall t' envT (fvs1 fvs2 : isfree envT),
-    (forall (n : nat) (t : Source.type),
-      lookup_type (envT := t' :: envT) n (true, fvs1) = Some t ->
-      lookup_type (envT := t' :: envT) n (false, fvs2) = Some t)
-    -> False.
-    intros until fvs2; intro H; generalize (H (length envT) t'); my_crush.
-  Defined.
-End lookup_hints.
-
-Section packing.
-  Open Local Scope cc_scope.
-
-  Hint Resolve lookup_type_push lookup_type_push_contra.
-
-  Definition packExp (var : Closed.type -> Set) (envT : list Source.type)
-    (fvs1 fvs2 : isfree envT)
-    : (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t)
-    -> envOf var fvs2 -> exp var (envType fvs1).
-    refine (fix packExp (var : Closed.type -> Set) (envT : list Source.type) {struct envT}
-      : forall fvs1 fvs2 : isfree envT,
-        (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t)
-        -> envOf var fvs2 -> exp var (envType fvs1) :=
-        match envT return (forall fvs1 fvs2 : isfree envT,
-          (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t)
-          -> envOf var fvs2
-          -> exp var (envType fvs1)) with
-          | nil => fun _ _ _ _ => ()
-          | first :: rest => fun fvs1 =>
-            match fvs1 return (forall fvs2 : isfree (first :: rest),
-              (forall n t, lookup_type (envT := first :: rest) n fvs1 = Some t
-                -> lookup_type n fvs2 = Some t)
-              -> envOf var fvs2
-              -> exp var (envType (envT := first :: rest) fvs1)) with
-              | (false, fvs1') => fun fvs2 =>
-                match fvs2 return ((forall n t, lookup_type (envT := first :: rest) n (false, fvs1') = Some t
-                  -> lookup_type (envT := first :: rest) n fvs2 = Some t)
-                -> envOf (envT := first :: rest) var fvs2
-                -> exp var (envType (envT := first :: rest) (false, fvs1'))) with
-                  | (false, fvs2') => fun Hmin env =>
-                    packExp var _  fvs1' fvs2' _ env
-                  | (true, fvs2') => fun Hmin env =>
-                    packExp var _  fvs1' fvs2' _ (snd env)
-                end
-              | (true, fvs1') => fun fvs2 =>
-                match fvs2 return ((forall n t, lookup_type (envT := first :: rest) n (true, fvs1') = Some t
-                  -> lookup_type (envT := first :: rest) n fvs2 = Some t)
-                -> envOf (envT := first :: rest) var fvs2
-                -> exp var (envType (envT := first :: rest) (true, fvs1'))) with
-                  | (false, fvs2') => fun Hmin env =>
-                    False_rect _ _
-                  | (true, fvs2') => fun Hmin env =>
-                    [#(fst env), packExp var _ fvs1' fvs2' _ (snd env)]
-                end
-            end
-        end); eauto.
-  Defined.
-
-  Hint Resolve fvsExp_correct fvsExp_minimal.
-  Hint Resolve lookup_push_drop lookup_bound lookup_push_add.
-
-  Implicit Arguments packExp [var envT].
-
-  Fixpoint unpackExp (var : Closed.type -> Set) t (envT : list Source.type) {struct envT}
-    : forall fvs : isfree envT,
-      exp var (envType fvs)
-      -> (envOf var fvs -> exp var t) -> exp var t :=
-      match envT return (forall fvs : isfree envT,
-        exp var (envType fvs)
-        -> (envOf var fvs -> exp var t) -> exp var t) with
-        | nil => fun _ _ f => f tt
-        | first :: rest => fun fvs =>
-          match fvs return (exp var (envType (envT := first :: rest) fvs)
-            -> (envOf var (envT := first :: rest) fvs -> exp var t)
-            -> exp var t) with
-            | (false, fvs') => fun p f =>
-              unpackExp rest fvs' p f
-            | (true, fvs') => fun p f =>
-              x <- #1 p;
-              unpackExp rest fvs' (#2 p)
-              (fun env => f (x, env))
-          end
-      end.
-  
-  Implicit Arguments unpackExp [var t envT fvs].
-
-  Theorem wfExp_lax : forall t t' envT (fvs : isfree envT) (e : Source.exp natvar t),
-    wfExp (envT := t' :: envT) (true, fvs) e
-    -> wfExp (envT := t' :: envT) (true, snd (fvsExp e (t' :: envT))) e.
-    Hint Extern 1 (_ = _) =>
-      match goal with
-        | [ H : lookup_type _ (fvsExp ?X ?Y) = _ |- _ ] =>
-          destruct (fvsExp X Y); my_crush
-      end.
-    eauto.
-  Defined.
-
-  Implicit Arguments wfExp_lax [t t' envT fvs e].
-
-  Lemma inclusion : forall t t' envT fvs (e : Source.exp natvar t),
-    wfExp (envT := t' :: envT) (true, fvs) e
-    -> (forall n t, lookup_type n (snd (fvsExp e (t' :: envT))) = Some t
-      -> lookup_type n fvs = Some t).
-    eauto.
-  Defined.
-
-  Implicit Arguments inclusion [t t' envT fvs e].
-
-  Definition env_prog var t envT (fvs : isfree envT) :=
-    funcs var (envOf var fvs -> Closed.exp var t).
-
-  Implicit Arguments env_prog [envT].
-
-  Import Source.
-  Open Local Scope cc_scope.
-
-  Definition proj1 A B (pf : A /\ B) : A :=
-    let (x, _) := pf in x.
-  Definition proj2 A B (pf : A /\ B) : B :=
-    let (_, y) := pf in y.
-
-  Fixpoint ccExp var t (e : Source.exp natvar t)
-    (envT : list Source.type) (fvs : isfree envT)
-    {struct e} : wfExp fvs e -> env_prog var (ccType t) fvs :=
-    match e in (Source.exp _ t) return (wfExp fvs e -> env_prog var (ccType t) fvs) with
-      | Const n => fun _ => Main (fun _ => ^n)
-      | Plus e1 e2 => fun wf =>
-        n1 <-- ccExp var e1 _ fvs (proj1 wf);
-        n2 <-- ccExp var e2 _ fvs (proj2 wf);
-        Main (fun env => n1 env +^ n2 env)
-
-      | Var _ n => fun wf =>
-        Main (fun env => #(match lok wf in _ = T return T with
-                             | refl_equal => lookup var n env
-                           end))
-
-      | App _ _ f x => fun wf =>
-        f' <-- ccExp var f _ fvs (proj1 wf);
-        x' <-- ccExp var x _ fvs (proj2 wf);
-        Main (fun env => f' env @ x' env)
-
-      | Abs dom _ b => fun wf =>
-        b' <-- ccExp var (b (length envT)) (dom :: envT) _ (wfExp_lax wf);
-        f <== \\env, arg, unpackExp (#env) (fun env => b' (arg, env));
-        Main (fun env => #f ##
-          packExp
-          (snd (fvsExp (b (length envT)) (dom :: envT)))
-          fvs (inclusion wf) env)
-    end.
-End packing.
-
-Implicit Arguments packExp [var envT].
-Implicit Arguments unpackExp [var t envT fvs].
-
-Implicit Arguments ccExp [var t envT].
-
-Fixpoint map_funcs var T1 T2 (f : T1 -> T2) (fs : funcs var T1) {struct fs}
-  : funcs var T2 :=
-  match fs with
-    | Main v => Main (f v)
-    | Abs _ _ _ e fs' => Abs e (fun x => map_funcs f (fs' x))
-  end.
-
-Definition CcExp' t (E : Source.Exp t) (Hwf : wfExp (envT := nil) tt (E _)) : Prog (ccType t) :=
-  fun _ => map_funcs (fun f => f tt) (ccExp (E _) (envT := nil) tt Hwf).
-
-
-(** ** Examples *)
-
-Open Local Scope source_scope.
-
-Definition ident : Source.Exp (Nat --> Nat) := fun _ => \x, #x.
-Theorem ident_ok : wfExp (envT := nil) tt (ident _).
-  crush.
-Defined.
-Eval compute in CcExp' ident ident_ok.
-Eval compute in ProgDenote (CcExp' ident ident_ok).
-
-Definition app_ident : Source.Exp Nat := fun _ => ident _ @ ^0.
-Theorem app_ident_ok : wfExp (envT := nil) tt (app_ident _).
-  crush.
-Defined.
-Eval compute in CcExp' app_ident app_ident_ok.
-Eval compute in ProgDenote (CcExp' app_ident app_ident_ok).
-
-Definition first : Source.Exp (Nat --> Nat --> Nat) := fun _ =>
-  \x, \y, #x.
-Theorem first_ok : wfExp (envT := nil) tt (first _).
-  crush.
-Defined.
-Eval compute in CcExp' first first_ok.
-Eval compute in ProgDenote (CcExp' first first_ok).
-
-Definition app_first : Source.Exp Nat := fun _ => first _ @ ^1 @ ^0.
-Theorem app_first_ok : wfExp (envT := nil) tt (app_first _).
-  crush.
-Defined.
-Eval compute in CcExp' app_first app_first_ok.
-Eval compute in ProgDenote (CcExp' app_first app_first_ok).
-
-
-(** ** Correctness *)
-
-Section spliceFuncs_correct.
-  Variables T1 T2 : Type.
-  Variable f : T1 -> funcs typeDenote T2.
-
-  Theorem spliceFuncs_correct : forall fs,
-    funcsDenote (spliceFuncs fs f)
-    = funcsDenote (f (funcsDenote fs)).
-    induction fs; crush.
-  Qed.
-End spliceFuncs_correct.
-
-
-Notation "var <| to" := (match to return Set with
-                           | None => unit
-                           | Some t => var (ccType t)
-                         end) (no associativity, at level 70).
-
-Section packing_correct.
-  Fixpoint makeEnv (envT : list Source.type) : forall (fvs : isfree envT),
-    Closed.typeDenote (envType fvs)
-    -> envOf Closed.typeDenote fvs :=
-    match envT return (forall (fvs : isfree envT),
-      Closed.typeDenote (envType fvs)
-      -> envOf Closed.typeDenote fvs) with
-      | nil => fun _ _ => tt
-      | first :: rest => fun fvs =>
-        match fvs return (Closed.typeDenote (envType (envT := first :: rest) fvs)
-          -> envOf (envT := first :: rest) Closed.typeDenote fvs) with
-          | (false, fvs') => fun env => makeEnv rest fvs' env
-          | (true, fvs') => fun env => (fst env, makeEnv rest fvs' (snd env))
-        end
-    end.
-
-  Implicit Arguments makeEnv [envT fvs].
-
-  Theorem unpackExp_correct : forall t (envT : list Source.type) (fvs : isfree envT)
-    (e1 : Closed.exp Closed.typeDenote (envType fvs))
-    (e2 : envOf Closed.typeDenote fvs -> Closed.exp Closed.typeDenote t),
-    Closed.expDenote (unpackExp e1 e2)
-    = Closed.expDenote (e2 (makeEnv (Closed.expDenote e1))).
-    induction envT; my_crush.
-  Qed.
-
-  Lemma lookup_type_more : forall v2 envT (fvs : isfree envT) t b v,
-    (v2 = length envT -> False)
-    -> lookup_type v2 (envT := t :: envT) (b, fvs) = v
-    -> lookup_type v2 fvs = v.
-    my_crush.
-  Qed.
-
-  Lemma lookup_type_less : forall v2 t envT (fvs : isfree (t :: envT)) v,
-    (v2 = length envT -> False)
-    -> lookup_type v2 (snd fvs) = v
-    -> lookup_type v2 (envT := t :: envT) fvs = v.
-    my_crush.
-  Qed.
-
-  Hint Resolve lookup_bound_contra.
-
-  Lemma lookup_bound_contra_eq : forall t envT (fvs : isfree envT) v,
-    lookup_type v fvs = Some t
-    -> v = length envT
-    -> False.
-    my_crush; elimtype False; eauto.
-  Qed.
-
-  Lemma lookup_type_inner : forall t t' envT v t'' (fvs : isfree envT) e,
-    wfExp (envT := t' :: envT) (true, fvs) e
-    -> lookup_type v (snd (fvsExp (t := t) e (t' :: envT))) = Some t''
-    -> lookup_type v fvs = Some t''.
-    Hint Resolve lookup_bound_contra_eq fvsExp_minimal
-      lookup_type_more lookup_type_less.
-    Hint Extern 2 (Some _ = Some _) => elimtype False.
-
-    eauto 6.
-  Qed.
-
-  Lemma cast_irrel : forall T1 T2 x (H1 H2 : T1 = T2),
-    match H1 in _ = T return T with
-      | refl_equal => x
-    end
-    = match H2 in _ = T return T with
-        | refl_equal => x
-      end.
-    intros; generalize H1; crush;
-      repeat match goal with
-               | [ |- context[match ?pf with refl_equal => _ end] ] =>
-                 rewrite (UIP_refl _ _ pf)
-             end;
-      reflexivity.
-  Qed.
-
-  Hint Immediate cast_irrel.
-
-  Hint Extern 3 (_ == _) =>
-    match goal with
-      | [ |- context[False_rect _ ?H] ] =>
-        apply False_rect; exact H
-    end.
-
-  Theorem packExp_correct : forall v t envT (fvs1 fvs2 : isfree envT)
-    Hincl env,
-    lookup_type v fvs1 = Some t
-    -> lookup Closed.typeDenote v env
-    == lookup Closed.typeDenote v
-    (makeEnv (Closed.expDenote
-      (packExp fvs1 fvs2 Hincl env))).
-    induction envT; my_crush.
-  Qed.
-End packing_correct.
-
-Implicit Arguments packExp_correct [v envT fvs1].
-Implicit Arguments lookup_type_inner [t t' envT v t'' fvs e].
-Implicit Arguments inclusion [t t' envT fvs e].
-
-Lemma typeDenote_same : forall t,
-  Source.typeDenote t = Closed.typeDenote (ccType t).
-  induction t; crush.
-Qed.
-
-Hint Resolve typeDenote_same.
-
-Fixpoint lr (t : Source.type) : Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop :=
-  match t return Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop with
-    | Nat => @eq nat
-    | dom --> ran => fun f1 f2 =>
-      forall x1 x2, lr dom x1 x2
-        -> lr ran (f1 x1) (f2 x2)
-  end.
-
-Theorem ccExp_correct : forall t G
-  (e1 : Source.exp Source.typeDenote t)
-  (e2 : Source.exp natvar t),
-  exp_equiv G e1 e2
-  -> forall (envT : list Source.type) (fvs : isfree envT)
-    (env : envOf Closed.typeDenote fvs) (wf : wfExp fvs e2),
-    (forall t (v1 : Source.typeDenote t) (v2 : natvar t),
-      In (existT _ _ (v1, v2)) G
-      -> v2 < length envT)
-    -> (forall t (v1 : Source.typeDenote t) (v2 : natvar t),
-      In (existT _ _ (v1, v2)) G
-      -> forall pf,
-        lr t v1 (match lok pf in _ = T return T with
-                   | refl_equal => lookup Closed.typeDenote v2 env
-                 end))
-    -> lr t (Source.expDenote e1) (Closed.expDenote (funcsDenote (ccExp e2 fvs wf) env)).
-
-  Hint Rewrite spliceFuncs_correct unpackExp_correct : cpdt.
-  Hint Resolve packExp_correct lookup_type_inner.
-
-  induction 1; crush;
-    match goal with
-      | [ IH : _, Hlr : lr ?T ?X1 ?X2, ENV : list Source.type, F2 : natvar _ -> _ |- _ ] =>
-        apply (IH X1 (length ENV) (T :: ENV) (true, snd (fvsExp (F2 (length ENV)) (T :: ENV))))
-    end; crush;
-    match goal with
-      | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In _ _ |- _ ] =>
-        solve [ generalize (Hlt _ _ _ Hin); crush ]
-      | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
-    end; simpl;
-    match goal with
-      | [ |- context[if ?E then _ else _] ] => destruct E
-    end; intuition; subst;
-    match goal with
-      | [ |- context[match ?pf with refl_equal => _ end] ] => rewrite (UIP_refl _ _ pf); assumption
-      | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In (existT _ _ (_, length _)) _ |- _ ] =>
-        generalize (Hlt _ _ _ Hin); crush
-      | [ HG : _, Hin : In _ _, wf : wfExp _ _, pf : _ = Some _,
-        fvs : isfree _, env : envOf _ _ |- _ ] =>
-      generalize (HG _ _ _ Hin (lookup_type_inner wf pf)); clear_all;
-        repeat match goal with
-                 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
-               end; simpl;
-        generalize (packExp_correct _ fvs (inclusion wf) env pf); simpl;
-          match goal with
-            | [ |- ?X == ?Y -> _ ] =>
-              generalize X Y
-          end;
-          rewrite pf; rewrite (lookup_type_inner wf pf);
-            intros lhs rhs Heq; intros;
-              repeat match goal with
-                       | [ H : _ = _ |- _ ] => rewrite (UIP_refl _ _ H) in *
-                     end;
-              rewrite <- Heq; assumption
-    end.
-Qed.
-
-
-(** * Parametric version *)
-
-Section wf.
-  Lemma Exp_wf' : forall G t (e1 e2 : Source.exp natvar t),
-    exp_equiv G e1 e2
-    -> forall envT (fvs : isfree envT),
-      (forall t (v1 v2 : natvar t), In (existT _ _ (v1, v2)) G
-        -> lookup_type v1 fvs = Some t)
-      -> wfExp fvs e1.
-    Hint Extern 3 (Some _ = Some _) => elimtype False; eapply lookup_bound_contra; eauto.
-
-    induction 1; crush; eauto;
-      match goal with
-        | [ H : _, envT : list Source.type |- _ ] =>
-          apply H with (length envT); my_crush; eauto
-      end.
-  Qed.
-
-  Theorem Exp_wf : forall t (E : Source.Exp t),
-    wfExp (envT := nil) tt (E _).
-    Hint Resolve Exp_equiv.
-
-    intros; eapply Exp_wf'; crush.
-  Qed.
-End wf.
-
-Definition CcExp t (E : Source.Exp t) : Prog (ccType t) :=
-  CcExp' E (Exp_wf E).
-
-Lemma map_funcs_correct : forall T1 T2 (f : T1 -> T2) (fs : funcs Closed.typeDenote T1),
-  funcsDenote (map_funcs f fs) = f (funcsDenote fs).
-  induction fs; crush.
-Qed.
-
-Theorem CcExp_correct : forall (E : Source.Exp Nat),
-  Source.ExpDenote E
-  = ProgDenote (CcExp E).
-  Hint Rewrite map_funcs_correct : cpdt.
-
-  unfold Source.ExpDenote, ProgDenote, CcExp, CcExp', progDenote; crush;
-    apply (ccExp_correct
-      (G := nil)
-      (e1 := E _)
-      (e2 := E _)
-      (Exp_equiv _ _ _)
-      nil
-      tt
-      tt); crush.
-Qed.
+(** TODO: This chapter!  (Old version was too complicated) *)
--- a/src/Interps.v	Sun Jan 04 08:18:59 2009 -0500
+++ b/src/Interps.v	Fri Nov 06 10:52:43 2009 -0500
@@ -10,7 +10,7 @@
 (* begin hide *)
 Require Import String List.
 
-Require Import AxiomsImpred Tactics.
+Require Import Axioms Tactics.
 
 Set Implicit Arguments.
 (* end hide *)
@@ -121,7 +121,7 @@
         | Plus e1 e2 =>
           let e1' := cfold e1 in
           let e2' := cfold e2 in
-          match e1', e2' with
+          match e1', e2' return _ with
             | Const n1, Const n2 => ^(n1 + n2)
             | _, _ => e1' +^ e2'
           end
@@ -301,7 +301,7 @@
     Variable var : type -> Type.
 
     Definition pairOutType t :=
-      match t with
+      match t return Type with
         | t1 ** t2 => option (exp var t1 * exp var t2)
         | _ => unit
       end.
@@ -326,7 +326,7 @@
         | Plus e1 e2 =>
           let e1' := cfold e1 in
           let e2' := cfold e2 in
-          match e1', e2' with
+          match e1', e2' return _ with
             | Const n1, Const n2 => ^(n1 + n2)
             | _, _ => e1' +^ e2'
           end
@@ -392,196 +392,3 @@
   Qed.
 (* end thide *)
 End PSLC.
-
-
-(** * Type Variables *)
-
-Module SysF.
-  (* EX: Follow a similar progression for System F. *)
-
-(* begin thide *)
-  Section vars.
-    Variable tvar : Type.
-
-    Inductive type : Type :=
-    | Nat : type
-    | Arrow : type -> type -> type
-    | TVar : tvar -> type
-    | All : (tvar -> type) -> type.
-
-    Notation "## v" := (TVar v) (at level 40).
-    Infix "-->" := Arrow (right associativity, at level 60).
-
-    Section Subst.
-      Variable t : type.
-
-      Inductive Subst : (tvar -> type) -> type -> Prop :=
-      | SNat : Subst (fun _ => Nat) Nat
-      | SArrow : forall dom ran dom' ran',
-        Subst dom dom'
-        -> Subst ran ran'
-        -> Subst (fun v => dom v --> ran v) (dom' --> ran')
-      | SVarEq : Subst TVar t
-      | SVarNe : forall v, Subst (fun _ => ##v) (##v)
-      | SAll : forall ran ran',
-        (forall v', Subst (fun v => ran v v') (ran' v'))
-        -> Subst (fun v => All (ran v)) (All ran').
-    End Subst.
-
-    Variable var : type -> Type.
-
-    Inductive exp : type -> Type :=
-    | Var : forall t,
-      var t
-      -> exp t
-
-    | Const : nat -> exp Nat
-    | Plus : exp Nat -> exp Nat -> exp Nat
-
-    | App : forall t1 t2,
-      exp (t1 --> t2)
-      -> exp t1
-      -> exp t2
-    | Abs : forall t1 t2,
-      (var t1 -> exp t2)
-      -> exp (t1 --> t2)
-
-    | TApp : forall tf,
-      exp (All tf)
-      -> forall t tf', Subst t tf tf'
-        -> exp tf'
-    | TAbs : forall tf,
-      (forall v, exp (tf v))
-      -> exp (All tf).
-  End vars.
-
-  Definition Typ := forall tvar, type tvar.
-  Definition Exp (T : Typ) := forall tvar (var : type tvar -> Type), exp var (T _).
-(* end thide *)
-
-  Implicit Arguments Nat [tvar].
-
-  Notation "## v" := (TVar v) (at level 40).
-  Infix "-->" := Arrow (right associativity, at level 60).
-  Notation "\\\ x , t" := (All (fun x => t)) (at level 65).
-
-  Implicit Arguments Var [tvar var t].
-  Implicit Arguments Const [tvar var].
-  Implicit Arguments Plus [tvar var].
-  Implicit Arguments App [tvar var t1 t2].
-  Implicit Arguments Abs [tvar var t1 t2].
-
-  Implicit Arguments TAbs [tvar var tf].
-
-  Notation "# v" := (Var v) (at level 70).
-
-  Notation "^ n" := (Const n) (at level 70).
-  Infix "+^" := Plus (left associativity, at level 79).
-
-  Infix "@" := App (left associativity, at level 77).
-  Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
-  Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
-
-  Notation "e @@ t" := (TApp e (t := t) _) (left associativity, at level 77).
-  Notation "\\ x , e" := (TAbs (fun x => e)) (at level 78).
-  Notation "\\ ! , e" := (TAbs (fun _ => e)) (at level 78).
-
-  Definition zero : Exp (fun _ => Nat) := fun _ _ =>
-    ^0.
-  Definition ident : Exp (fun _ => \\\T, ##T --> ##T) := fun _ _ =>
-    \\T, \x, #x.
-  Definition ident_zero : Exp (fun _ => Nat).
-    do 2 intro; refine (ident _ @@ _ @ zero _);
-      repeat constructor.
-  Defined.
-  Definition ident_ident : Exp (fun _ => \\\T, ##T --> ##T).
-    do 2 intro; refine (ident _ @@ _ @ ident _);
-      repeat constructor.
-  Defined.
-  Definition ident5 : Exp (fun _ => \\\T, ##T --> ##T).
-    do 2 intro; refine (ident_ident _ @@ _ @ ident_ident _ @@ _ @ ident _);
-      repeat constructor.
-  Defined.
-
-(* begin thide *)
-  Fixpoint typeDenote (t : type Set) : Set :=
-    match t with
-      | Nat => nat
-      | t1 --> t2 => typeDenote t1 -> typeDenote t2
-      | ##v => v
-      | All tf => forall T, typeDenote (tf T)
-    end.
-
-  Lemma Subst_typeDenote : forall t tf tf',
-    Subst t tf tf'
-    -> typeDenote (tf (typeDenote t)) = typeDenote tf'.
-    induction 1; crush; ext_eq; crush.
-  Defined.
-
-  Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
-    match e in (exp _ t) return (typeDenote t) with
-      | Var _ v => v
-        
-      | Const n => n
-      | Plus e1 e2 => expDenote e1 + expDenote e2
-        
-      | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
-      | Abs _ _ e' => fun x => expDenote (e' x)
-
-      | TApp _ e' t' _ pf => match Subst_typeDenote pf in _ = T return T with
-                               | refl_equal => (expDenote e') (typeDenote t')
-                             end
-      | TAbs _ e' => fun T => expDenote (e' T)
-    end.
-
-  Definition ExpDenote T (E : Exp T) := expDenote (E _ _).
-(* end thide *)
-
-  Eval compute in ExpDenote zero.
-  Eval compute in ExpDenote ident.
-  Eval compute in ExpDenote ident_zero.
-  Eval compute in ExpDenote ident_ident.
-  Eval compute in ExpDenote ident5.
-
-(* begin thide *)
-  Section cfold.
-    Variable tvar : Type.
-    Variable var : type tvar -> Type.
-
-    Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
-      match e in exp _ t return exp _ t with
-        | Var _ v => #v
-
-        | Const n => ^n
-        | Plus e1 e2 =>
-          let e1' := cfold e1 in
-          let e2' := cfold e2 in
-          match e1', e2' with
-            | Const n1, Const n2 => ^(n1 + n2)
-            | _, _ => e1' +^ e2'
-          end
-
-        | App _ _ e1 e2 => cfold e1 @ cfold e2
-        | Abs _ _ e' => Abs (fun x => cfold (e' x))
-
-        | TApp _ e' _ _ pf => TApp (cfold e') pf
-        | TAbs _ e' => \\T, cfold (e' T)
-      end.
-  End cfold.
-
-  Definition Cfold T (E : Exp T) : Exp T := fun _ _ => cfold (E _ _).
-
-  Lemma cfold_correct : forall t (e : exp _ t),
-    expDenote (cfold e) = expDenote e.
-    induction e; crush; try (ext_eq; crush);
-      repeat (match goal with
-                | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
-              end; crush).
-  Qed.
-
-  Theorem Cfold_correct : forall t (E : Exp t),
-    ExpDenote (Cfold E) = ExpDenote E.
-    unfold ExpDenote, Cfold; intros; apply cfold_correct.
-  Qed.
-(* end thide *)
-End SysF.
--- a/src/Match.v	Sun Jan 04 08:18:59 2009 -0500
+++ b/src/Match.v	Fri Nov 06 10:52:43 2009 -0500
@@ -784,10 +784,10 @@
 
 Ltac matcher :=
   intros;
-    repeat search_prem ltac:(apply False_prem || (apply ex_prem; intro));
-      repeat search_conc ltac:(apply True_conc || eapply ex_conc
-        || search_prem ltac:(apply Match));
-      try apply imp_True.
+    repeat search_prem ltac:(simple apply False_prem || (simple apply ex_prem; intro));
+      repeat search_conc ltac:(simple apply True_conc || simple eapply ex_conc
+        || search_prem ltac:(simple apply Match));
+      try simple apply imp_True.
 (* end thide *)
 
 (** Our tactic succeeds at proving a simple example. *)
--- a/src/MoreDep.v	Sun Jan 04 08:18:59 2009 -0500
+++ b/src/MoreDep.v	Fri Nov 06 10:52:43 2009 -0500
@@ -247,20 +247,20 @@
 
 With [pairOut] available, we can write [cfold] in a straightforward way.  There are really no surprises beyond that Coq verifies that this code has such an expressive type, given the small annotation burden. *)
 
-Fixpoint cfold t (e : exp t) {struct e} : exp t :=
-  match e in (exp t) return (exp t) with
+Fixpoint cfold t (e : exp t) : exp t :=
+  match e with
     | NConst n => NConst n
     | Plus e1 e2 =>
       let e1' := cfold e1 in
       let e2' := cfold e2 in
-      match e1', e2' with
+      match e1', e2' return _ with
         | NConst n1, NConst n2 => NConst (n1 + n2)
         | _, _ => Plus e1' e2'
       end
     | Eq e1 e2 =>
       let e1' := cfold e1 in
       let e2' := cfold e2 in
-      match e1', e2' with
+      match e1', e2' return _ with
         | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
         | _, _ => Eq e1' e2'
       end
@@ -269,7 +269,7 @@
     | And e1 e2 =>
       let e1' := cfold e1 in
       let e2' := cfold e2 in
-      match e1', e2' with
+      match e1', e2' return _ with
         | BConst b1, BConst b2 => BConst (b1 && b2)
         | _, _ => And e1' e2'
       end
@@ -1028,7 +1028,7 @@
   (** Finally, we have [dec_star].  It has a straightforward implementation.  We introduce a spurious match on [s] so that [simpl] will know to reduce calls to [dec_star].  The heuristic that [simpl] uses is only to unfold identifier definitions when doing so would simplify some [match] expression. *)
 
   Definition dec_star : {star P s} + { ~star P s}.
-    refine (match s with
+    refine (match s return _ with
               | "" => Reduce (dec_star' (n := length s) 0 _)
               | _ => Reduce (dec_star' (n := length s) 0 _)
             end); crush.
--- a/src/Subset.v	Sun Jan 04 08:18:59 2009 -0500
+++ b/src/Subset.v	Fri Nov 06 10:52:43 2009 -0500
@@ -376,7 +376,7 @@
 We can build "smart" versions of the usual boolean operators and put them to good use in certified programming.  For instance, here is a [sumbool] version of boolean "or." *)
 
 (* begin thide *)
-Notation "x || y" := (if x then Yes else Reduce y) (at level 50).
+Notation "x || y" := (if x then Yes else Reduce y).
 
 (** Let us use it for building a function that decides list membership.  We need to assume the existence of an equality decision procedure for the type of list elements. *)
 
--- a/src/Tactics.v	Sun Jan 04 08:18:59 2009 -0500
+++ b/src/Tactics.v	Fri Nov 06 10:52:43 2009 -0500
@@ -48,15 +48,21 @@
   match goal with
     | [ H : ex _ |- _ ] => destruct H
 
-    | [ H : ?F ?X = ?F ?Y |- _ ] => injection H;
-      match goal with
-        | [ |- F X = F Y -> _ ] => fail 1
-        | [ |- _ = _ -> _ ] => try clear H; intros; try subst
-      end
-    | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H;
-      match goal with
-        | [ |- _ = _ -> _ = _ -> _ ] => try clear H; intros; try subst
-      end
+    | [ H : ?F ?X = ?F ?Y |- ?G ] =>
+      (assert (X = Y); [ assumption | fail 1 ])
+      || (injection H;
+        match goal with
+          | [ |- X = Y -> G ] =>
+            try clear H; intros; try subst
+        end)
+    | [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] =>
+      (assert (X = Y); [ assumption
+        | assert (U = V); [ assumption | fail 1 ] ])
+      || (injection H;
+        match goal with
+          | [ |- U = V -> X = Y -> G ] =>
+            try clear H; intros; try subst
+        end)
 
     | [ H : ?F _ |- _ ] => invert H F
     | [ H : ?F _ _ |- _ ] => invert H F