adamc@175: (* Copyright (c) 2008, Adam Chlipala
adamc@175:  * 
adamc@175:  * This work is licensed under a
adamc@175:  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@175:  * Unported License.
adamc@175:  * The license text is available at:
adamc@175:  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@175:  *)
adamc@175: 
adamc@175: (* begin hide *)
adamc@175: Require Import String List.
adamc@175: 
adamc@177: Require Import AxiomsImpred Tactics DepList.
adamc@175: 
adamc@175: Set Implicit Arguments.
adamc@175: (* end hide *)
adamc@175: 
adamc@175: 
adamc@175: (** %\chapter{Certifying Extensional Transformations}% *)
adamc@175: 
adamc@175: (** TODO: Prose for this chapter *)
adamc@175: 
adamc@175: 
adamc@175: (** * Simply-Typed Lambda Calculus *)
adamc@175: 
adamc@175: Module STLC.
adamc@175:   Module Source.
adamc@175:     Inductive type : Type :=
adamc@175:     | TNat : type
adamc@175:     | Arrow : type -> type -> type.
adamc@175: 
adamc@175:     Notation "'Nat'" := TNat : source_scope.
adamc@175:     Infix "-->" := Arrow (right associativity, at level 60) : source_scope.
adamc@175: 
adamc@175:     Open Scope source_scope.
adamc@175:     Bind Scope source_scope with type.
adamc@175:     Delimit Scope source_scope with source.
adamc@175: 
adamc@175:     Section vars.
adamc@175:       Variable var : type -> Type.
adamc@175: 
adamc@175:       Inductive exp : type -> Type :=
adamc@175:       | Var : forall t,
adamc@175:         var t
adamc@175:         -> exp t
adamc@175: 
adamc@175:       | Const : nat -> exp Nat
adamc@175:       | Plus : exp Nat -> exp Nat -> exp Nat
adamc@175: 
adamc@175:       | App : forall t1 t2,
adamc@175:         exp (t1 --> t2)
adamc@175:         -> exp t1
adamc@175:         -> exp t2
adamc@175:       | Abs : forall t1 t2,
adamc@175:         (var t1 -> exp t2)
adamc@175:         -> exp (t1 --> t2).
adamc@175:     End vars.
adamc@175: 
adamc@175:     Definition Exp t := forall var, exp var t.
adamc@175: 
adamc@175:     Implicit Arguments Var [var t].
adamc@175:     Implicit Arguments Const [var].
adamc@175:     Implicit Arguments Plus [var].
adamc@175:     Implicit Arguments App [var t1 t2].
adamc@175:     Implicit Arguments Abs [var t1 t2].
adamc@175: 
adamc@175:     Notation "# v" := (Var v) (at level 70) : source_scope.
adamc@175: 
adamc@175:     Notation "^ n" := (Const n) (at level 70) : source_scope.
adamc@175:     Infix "+^" := Plus (left associativity, at level 79) : source_scope.
adamc@175: 
adamc@175:     Infix "@" := App (left associativity, at level 77) : source_scope.
adamc@175:     Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
adamc@175:     Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope.
adamc@175: 
adamc@175:     Bind Scope source_scope with exp.
adamc@175: 
adamc@175:     Definition zero : Exp Nat := fun _ => ^0.
adamc@175:     Definition one : Exp Nat := fun _ => ^1.
adamc@175:     Definition zpo : Exp Nat := fun _ => zero _ +^ one _.
adamc@175:     Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x.
adamc@175:     Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
adamc@175:     Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
adamc@175:       \f, \x, #f @ #x.
adamc@175:     Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
adamc@175: 
adamc@175:     Fixpoint typeDenote (t : type) : Set :=
adamc@175:       match t with
adamc@175:         | Nat => nat
adamc@175:         | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@175:       end.
adamc@175: 
adamc@175:     Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@175:       match e in (exp _ t) return (typeDenote t) with
adamc@175:         | Var _ v => v
adamc@175:           
adamc@175:         | Const n => n
adamc@175:         | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@175:           
adamc@175:         | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@175:         | Abs _ _ e' => fun x => expDenote (e' x)
adamc@175:       end.
adamc@175: 
adamc@175:     Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@176: 
adamc@180: (* begin thide *)
adamc@176:     Section exp_equiv.
adamc@176:       Variables var1 var2 : type -> Type.
adamc@176: 
adamc@176:       Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop :=
adamc@176:       | EqEVar : forall G t (v1 : var1 t) v2,
adamc@176:         In (existT _ t (v1, v2)) G
adamc@176:         -> exp_equiv G (#v1) (#v2)
adamc@176: 
adamc@176:       | EqEConst : forall G n,
adamc@176:         exp_equiv G (^n) (^n)
adamc@176:       | EqEPlus : forall G x1 y1 x2 y2,
adamc@176:         exp_equiv G x1 x2
adamc@176:         -> exp_equiv G y1 y2
adamc@176:         -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
adamc@176: 
adamc@176:       | EqEApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
adamc@176:         exp_equiv G f1 f2
adamc@176:         -> exp_equiv G x1 x2
adamc@176:         -> exp_equiv G (f1 @ x1) (f2 @ x2)
adamc@176:       | EqEAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
adamc@176:         (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
adamc@176:         -> exp_equiv G (Abs f1) (Abs f2).
adamc@176:     End exp_equiv.
adamc@176: 
adamc@176:     Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
adamc@176:       exp_equiv nil (E var1) (E var2).
adamc@180: (* end thide *)
adamc@175:   End Source.
adamc@175: 
adamc@175:   Module CPS.
adamc@175:     Inductive type : Type :=
adamc@175:     | TNat : type
adamc@175:     | Cont : type -> type
adamc@175:     | TUnit : type
adamc@175:     | Prod : type -> type -> type.
adamc@175: 
adamc@175:     Notation "'Nat'" := TNat : cps_scope.
adamc@175:     Notation "'Unit'" := TUnit : cps_scope.
adamc@175:     Notation "t --->" := (Cont t) (at level 61) : cps_scope.
adamc@175:     Infix "**" := Prod (right associativity, at level 60) : cps_scope.
adamc@175: 
adamc@175:     Bind Scope cps_scope with type.
adamc@175:     Delimit Scope cps_scope with cps.
adamc@175: 
adamc@175:     Section vars.
adamc@175:       Variable var : type -> Type.
adamc@175: 
adamc@175:       Inductive prog : Type :=
adamc@175:       | PHalt :
adamc@175:         var Nat
adamc@175:         -> prog
adamc@175:       | App : forall t,
adamc@175:         var (t --->)
adamc@175:         -> var t
adamc@175:         -> prog
adamc@175:       | Bind : forall t,
adamc@175:         primop t
adamc@175:         -> (var t -> prog)
adamc@175:         -> prog
adamc@175: 
adamc@175:       with primop : type -> Type :=
adamc@175:       | Var : forall t,
adamc@175:         var t
adamc@175:         -> primop t
adamc@175:         
adamc@175:       | Const : nat -> primop Nat
adamc@175:       | Plus : var Nat -> var Nat -> primop Nat
adamc@175:         
adamc@175:       | Abs : forall t,
adamc@175:         (var t -> prog)
adamc@175:         -> primop (t --->)
adamc@175: 
adamc@175:       | Pair : forall t1 t2,
adamc@175:         var t1
adamc@175:         -> var t2
adamc@175:         -> primop (t1 ** t2)
adamc@175:       | Fst : forall t1 t2,
adamc@175:         var (t1 ** t2)
adamc@175:         -> primop t1
adamc@175:       | Snd : forall t1 t2,
adamc@175:         var (t1 ** t2)
adamc@175:         -> primop t2.
adamc@175:     End vars.
adamc@175: 
adamc@175:     Implicit Arguments PHalt [var].
adamc@175:     Implicit Arguments App [var t].
adamc@175: 
adamc@175:     Implicit Arguments Var [var t].
adamc@175:     Implicit Arguments Const [var].
adamc@175:     Implicit Arguments Plus [var].
adamc@175:     Implicit Arguments Abs [var t].
adamc@175:     Implicit Arguments Pair [var t1 t2].
adamc@175:     Implicit Arguments Fst [var t1 t2].
adamc@175:     Implicit Arguments Snd [var t1 t2].
adamc@175: 
adamc@175:     Notation "'Halt' x" := (PHalt x) (no associativity, at level 75) : cps_scope.
adamc@175:     Infix "@@" := App (no associativity, at level 75) : cps_scope.
adamc@175:     Notation "x <- p ; e" := (Bind p (fun x => e))
adamc@175:       (right associativity, at level 76, p at next level) : cps_scope.
adamc@175:     Notation "! <- p ; e" := (Bind p (fun _ => e))
adamc@175:       (right associativity, at level 76, p at next level) : cps_scope.
adamc@175: 
adamc@175:     Notation "# v" := (Var v) (at level 70) : cps_scope.
adamc@175: 
adamc@175:     Notation "^ n" := (Const n) (at level 70) : cps_scope.
adamc@175:     Infix "+^" := Plus (left associativity, at level 79) : cps_scope.
adamc@175: 
adamc@175:     Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : cps_scope.
adamc@175:     Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : cps_scope.
adamc@175: 
adamc@179:     Notation "[ x1 , x2 ]" := (Pair x1 x2) : cps_scope.
adamc@175:     Notation "#1 x" := (Fst x) (at level 72) : cps_scope.
adamc@175:     Notation "#2 x" := (Snd x) (at level 72) : cps_scope.
adamc@175: 
adamc@175:     Bind Scope cps_scope with prog primop.
adamc@175: 
adamc@175:     Open Scope cps_scope.
adamc@175: 
adamc@175:     Fixpoint typeDenote (t : type) : Set :=
adamc@175:       match t with
adamc@175:         | Nat => nat
adamc@175:         | t' ---> => typeDenote t' -> nat
adamc@175:         | Unit => unit
adamc@175:         | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
adamc@175:       end.
adamc@175: 
adamc@175:     Fixpoint progDenote (e : prog typeDenote) : nat :=
adamc@175:       match e with
adamc@175:         | PHalt n => n
adamc@175:         | App _ f x => f x
adamc@175:         | Bind _ p x => progDenote (x (primopDenote p))
adamc@175:       end
adamc@175: 
adamc@175:     with primopDenote t (p : primop typeDenote t) {struct p} : typeDenote t :=
adamc@175:       match p in (primop _ t) return (typeDenote t) with
adamc@175:         | Var _ v => v
adamc@175: 
adamc@175:         | Const n => n
adamc@175:         | Plus n1 n2 => n1 + n2
adamc@175: 
adamc@175:         | Abs _ e => fun x => progDenote (e x)
adamc@175: 
adamc@175:         | Pair _ _ v1 v2 => (v1, v2)
adamc@175:         | Fst _ _ v => fst v
adamc@175:         | Snd _ _ v => snd v
adamc@175:       end.
adamc@175: 
adamc@175:     Definition Prog := forall var, prog var.
adamc@175:     Definition Primop t := forall var, primop var t.
adamc@175:     Definition ProgDenote (E : Prog) := progDenote (E _).
adamc@175:     Definition PrimopDenote t (P : Primop t) := primopDenote (P _).
adamc@175:   End CPS.
adamc@175: 
adamc@175:   Import Source CPS.
adamc@175: 
adamc@180: (* begin thide *)
adamc@175:   Fixpoint cpsType (t : Source.type) : CPS.type :=
adamc@175:     match t with
adamc@175:       | Nat => Nat%cps
adamc@175:       | t1 --> t2 => (cpsType t1 ** (cpsType t2 --->) --->)%cps
adamc@175:     end%source.
adamc@175: 
adamc@175:   Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
adamc@175: 
adamc@175:   Section cpsExp.
adamc@175:     Variable var : CPS.type -> Type.
adamc@175: 
adamc@175:     Import Source.
adamc@175:     Open Scope cps_scope.
adamc@175: 
adamc@175:     Fixpoint cpsExp t (e : exp (fun t => var (cpsType t)) t) {struct e}
adamc@175:       : (var (cpsType t) -> prog var) -> prog var :=
adamc@175:       match e in (exp _ t) return ((var (cpsType t) -> prog var) -> prog var) with
adamc@175:         | Var _ v => fun k => k v
adamc@175: 
adamc@175:         | Const n => fun k =>
adamc@175:           x <- ^n;
adamc@175:           k x
adamc@175:         | Plus e1 e2 => fun k =>
adamc@175:           x1 <-- e1;
adamc@175:           x2 <-- e2;
adamc@175:           x <- x1 +^ x2;
adamc@175:           k x
adamc@175: 
adamc@175:         | App _ _ e1 e2 => fun k =>
adamc@175:           f <-- e1;
adamc@175:           x <-- e2;
adamc@175:           kf <- \r, k r;
adamc@175:           p <- [x, kf];
adamc@175:           f @@ p
adamc@175:         | Abs _ _ e' => fun k =>
adamc@175:           f <- CPS.Abs (var := var) (fun p =>
adamc@175:             x <- #1 p;
adamc@175:             kf <- #2 p;
adamc@175:             r <-- e' x;
adamc@175:             kf @@ r);
adamc@175:           k f
adamc@175:       end
adamc@175: 
adamc@175:       where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
adamc@175:   End cpsExp.
adamc@175: 
adamc@175:   Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)) : cps_scope.
adamc@175:   Notation "! <-- e1 ; e2" := (cpsExp e1 (fun _ => e2))
adamc@175:     (right associativity, at level 76, e1 at next level) : cps_scope.
adamc@175: 
adamc@175:   Implicit Arguments cpsExp [var t].
adamc@175:   Definition CpsExp (E : Exp Nat) : Prog :=
adamc@175:     fun var => cpsExp (E _) (PHalt (var := _)).
adamc@180: (* end thide *)
adamc@175: 
adamc@175:   Eval compute in CpsExp zero.
adamc@175:   Eval compute in CpsExp one.
adamc@175:   Eval compute in CpsExp zpo.
adamc@175:   Eval compute in CpsExp app_ident.
adamc@175:   Eval compute in CpsExp app_ident'.
adamc@175: 
adamc@175:   Eval compute in ProgDenote (CpsExp zero).
adamc@175:   Eval compute in ProgDenote (CpsExp one).
adamc@175:   Eval compute in ProgDenote (CpsExp zpo).
adamc@175:   Eval compute in ProgDenote (CpsExp app_ident).
adamc@175:   Eval compute in ProgDenote (CpsExp app_ident').
adamc@175: 
adamc@180: (* begin thide *)
adamc@176:   Fixpoint lr (t : Source.type) : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop :=
adamc@176:     match t return (Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop) with
adamc@176:       | Nat => fun n1 n2 => n1 = n2
adamc@176:       | t1 --> t2 => fun f1 f2 =>
adamc@176:         forall x1 x2, lr _ x1 x2
adamc@176:           -> forall k, exists r,
adamc@176:             f2 (x2, k) = k r
adamc@176:             /\ lr _ (f1 x1) r
adamc@176:     end%source.
adamc@176: 
adamc@176:   Lemma cpsExp_correct : forall G t (e1 : exp _ t) (e2 : exp _ t),
adamc@176:     exp_equiv G e1 e2
adamc@176:     -> (forall t v1 v2, In (existT _ t (v1, v2)) G -> lr t v1 v2)
adamc@176:     -> forall k, exists r,
adamc@176:       progDenote (cpsExp e2 k) = progDenote (k r)
adamc@176:       /\ lr t (expDenote e1) r.
adamc@176:     induction 1; crush; fold typeDenote in *;
adamc@176:       repeat (match goal with
adamc@176:                 | [ H : forall k, exists r, progDenote (cpsExp ?E k) = _ /\ _
adamc@176:                   |- context[cpsExp ?E ?K] ] =>
adamc@176:                   generalize (H K); clear H
adamc@176:                 | [ |- exists r, progDenote (_ ?R) = progDenote (_ r) /\ _ ] =>
adamc@176:                   exists R
adamc@176:                 | [ t1 : Source.type |- _ ] =>
adamc@176:                   match goal with
adamc@176:                     | [ Hlr : lr t1 ?X1 ?X2, IH : forall v1 v2, _ |- _ ] =>
adamc@176:                       generalize (IH X1 X2); clear IH; intro IH;
adamc@176:                         match type of IH with
adamc@176:                           | ?P -> _ => assert P
adamc@176:                         end
adamc@176:                   end
adamc@176:               end; crush); eauto.
adamc@176:   Qed.
adamc@176: 
adamc@176:   Lemma vars_easy : forall (t : Source.type) (v1 : Source.typeDenote t)
adamc@176:     (v2 : typeDenote (cpsType t)),
adamc@176:     In
adamc@176:     (existT
adamc@176:       (fun t0 : Source.type =>
adamc@176:         (Source.typeDenote t0 * typeDenote (cpsType t0))%type) t
adamc@176:       (v1, v2)) nil -> lr t v1 v2.
adamc@176:     crush.
adamc@176:   Qed.
adamc@176: 
adamc@176:   Theorem CpsExp_correct : forall (E : Exp Nat),
adamc@176:     ProgDenote (CpsExp E) = ExpDenote E.
adamc@176:     unfold ProgDenote, CpsExp, ExpDenote; intros;
adamc@176:       generalize (cpsExp_correct (e1 := E _) (e2 := E _)
adamc@176:         (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush.
adamc@176:   Qed.
adamc@180: (* end thide *)
adamc@176: 
adamc@175: End STLC.
adamc@177: 
adamc@177: 
adamc@177: (** * A Pattern Compiler *)
adamc@177: 
adamc@177: Module PatMatch.
adamc@177:   Module Source.
adamc@177:     Inductive type : Type :=
adamc@177:     | Unit : type
adamc@177:     | Arrow : type -> type -> type
adamc@177:     | Prod : type -> type -> type
adamc@177:     | Sum : type -> type -> type.
adamc@177: 
adamc@177:     Infix "-->" := Arrow (right associativity, at level 61).
adamc@177:     Infix "++" := Sum (right associativity, at level 60).
adamc@177:     Infix "**" := Prod (right associativity, at level 59).
adamc@177: 
adamc@177:     Inductive pat : type -> list type -> Type :=
adamc@177:     | PVar : forall t,
adamc@177:       pat t (t :: nil)
adamc@177:     | PPair : forall t1 t2 ts1 ts2,
adamc@177:       pat t1 ts1
adamc@177:       -> pat t2 ts2
adamc@177:       -> pat (t1 ** t2) (ts1 ++ ts2)
adamc@177:     | PInl : forall t1 t2 ts,
adamc@177:       pat t1 ts
adamc@177:       -> pat (t1 ++ t2) ts
adamc@177:     | PInr : forall t1 t2 ts,
adamc@177:       pat t2 ts
adamc@177:       -> pat (t1 ++ t2) ts.
adamc@177: 
adamc@177:     Implicit Arguments PVar [t].
adamc@177:     Implicit Arguments PInl [t1 t2 ts].
adamc@177:     Implicit Arguments PInr [t1 t2 ts].
adamc@177: 
adamc@177:     Notation "##" := PVar (at level 70) : pat_scope.
adamc@179:     Notation "[ p1 , p2 ]" := (PPair p1 p2) : pat_scope.
adamc@177:     Notation "'Inl' p" := (PInl p) (at level 71) : pat_scope.
adamc@177:     Notation "'Inr' p" := (PInr p) (at level 71) : pat_scope.
adamc@177: 
adamc@177:     Bind Scope pat_scope with pat.
adamc@177:     Delimit Scope pat_scope with pat.
adamc@177: 
adamc@177:     Section vars.
adamc@177:       Variable var : type -> Type.
adamc@177: 
adamc@177:       Inductive exp : type -> Type :=
adamc@177:       | Var : forall t,
adamc@177:         var t
adamc@177:         -> exp t
adamc@177: 
adamc@177:       | EUnit : exp Unit
adamc@177: 
adamc@177:       | App : forall t1 t2,
adamc@177:         exp (t1 --> t2)
adamc@177:         -> exp t1
adamc@177:         -> exp t2
adamc@177:       | Abs : forall t1 t2,
adamc@177:         (var t1 -> exp t2)
adamc@177:         -> exp (t1 --> t2)
adamc@177: 
adamc@177:       | Pair : forall t1 t2,
adamc@177:         exp t1
adamc@177:         -> exp t2
adamc@177:         -> exp (t1 ** t2)
adamc@177: 
adamc@177:       | EInl : forall t1 t2,
adamc@177:         exp t1
adamc@177:         -> exp (t1 ++ t2)
adamc@177:       | EInr : forall t1 t2,
adamc@177:         exp t2
adamc@177:         -> exp (t1 ++ t2)
adamc@177: 
adamc@177:       | Case : forall t1 t2 (tss : list (list type)),
adamc@177:         exp t1
adamc@177:         -> (forall ts, member ts tss -> pat t1 ts)
adamc@177:         -> (forall ts, member ts tss -> hlist var ts -> exp t2)
adamc@177:         -> exp t2
adamc@177:         -> exp t2.
adamc@177:     End vars.
adamc@177: 
adamc@177:     Definition Exp t := forall var, exp var t.
adamc@177: 
adamc@177:     Implicit Arguments Var [var t].
adamc@177:     Implicit Arguments EUnit [var].
adamc@177:     Implicit Arguments App [var t1 t2].
adamc@177:     Implicit Arguments Abs [var t1 t2].
adamc@177:     Implicit Arguments Pair [var t1 t2].
adamc@177:     Implicit Arguments EInl [var t1 t2].
adamc@177:     Implicit Arguments EInr [var t1 t2].
adamc@177:     Implicit Arguments Case [var t1 t2].
adamc@177: 
adamc@177:     Notation "# v" := (Var v) (at level 70) : source_scope.
adamc@177: 
adamc@177:     Notation "()" := EUnit : source_scope.
adamc@177: 
adamc@177:     Infix "@" := App (left associativity, at level 77) : source_scope.
adamc@177:     Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
adamc@177: 
adamc@179:     Notation "[ x , y ]" := (Pair x y) : source_scope.
adamc@177: 
adamc@177:     Notation "'Inl' e" := (EInl e) (at level 71) : source_scope.
adamc@177:     Notation "'Inr' e" := (EInr e) (at level 71) : source_scope.
adamc@177: 
adamc@178:     Delimit Scope source_scope with source.
adamc@177:     Bind Scope source_scope with exp.
adamc@177: 
adamc@177:     Open Local Scope source_scope.
adamc@177: 
adamc@177:     Fixpoint typeDenote (t : type) : Set :=
adamc@177:       match t with
adamc@177:         | Unit => unit
adamc@177:         | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@177:         | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
adamc@177:         | t1 ++ t2 => (typeDenote t1 + typeDenote t2)%type
adamc@177:       end.
adamc@177: 
adamc@177:     Fixpoint patDenote t ts (p : pat t ts) {struct p} : typeDenote t -> option (hlist typeDenote ts) :=
adamc@177:       match p in (pat t ts) return (typeDenote t -> option (hlist typeDenote ts)) with
adamc@177:         | PVar _ => fun v => Some (v, tt)
adamc@177:         | PPair _ _ _ _ p1 p2 => fun v =>
adamc@177:           match patDenote p1 (fst v), patDenote p2 (snd v) with
adamc@177:             | Some tup1, Some tup2 => Some (happ tup1 tup2)
adamc@177:             | _, _ => None
adamc@177:           end
adamc@177:         | PInl _ _ _ p' => fun v =>
adamc@177:           match v with
adamc@177:             | inl v' => patDenote p' v'
adamc@177:             | _ => None
adamc@177:           end
adamc@177:         | PInr _ _ _ p' => fun v =>
adamc@177:           match v with
adamc@177:             | inr v' => patDenote p' v'
adamc@177:             | _ => None
adamc@177:           end
adamc@177:       end.
adamc@177: 
adamc@177:     Section matchesDenote.
adamc@177:       Variables t2 : type.
adamc@177:       Variable default : typeDenote t2.
adamc@177: 
adamc@177:       Fixpoint matchesDenote (tss : list (list type))
adamc@177:         : (forall ts, member ts tss -> option (hlist typeDenote ts))
adamc@177:         -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
adamc@177:         -> typeDenote t2 :=
adamc@177:         match tss return (forall ts, member ts tss -> _)
adamc@177:           -> (forall ts, member ts tss -> _)
adamc@177:           -> _ with
adamc@177:           | nil => fun _ _ =>
adamc@177:             default
adamc@177:           | ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss') -> option (hlist typeDenote ts'))
adamc@177:             (bodies : forall ts', member ts' (ts :: tss') -> hlist typeDenote ts' -> typeDenote t2) =>
adamc@177:             match envs _ (hfirst (refl_equal _)) with
adamc@177:               | None => matchesDenote tss'
adamc@177:                 (fun _ mem => envs _ (hnext mem))
adamc@177:                 (fun _ mem => bodies _ (hnext mem))
adamc@177:               | Some env => (bodies _ (hfirst (refl_equal _))) env
adamc@177:             end
adamc@177:         end.
adamc@177:     End matchesDenote.
adamc@177: 
adamc@177:     Implicit Arguments matchesDenote [t2 tss].
adamc@177: 
adamc@177:     Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@177:       match e in (exp _ t) return (typeDenote t) with
adamc@177:         | Var _ v => v
adamc@177: 
adamc@177:         | EUnit => tt
adamc@177: 
adamc@177:         | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@177:         | Abs _ _ e' => fun x => expDenote (e' x)
adamc@177: 
adamc@177:         | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@177: 
adamc@177:         | EInl _ _ e' => inl _ (expDenote e')
adamc@177:         | EInr _ _ e' => inr _ (expDenote e')
adamc@177: 
adamc@177:         | Case _ _ _ e ps es def =>
adamc@177:           matchesDenote (expDenote def)
adamc@177:           (fun _ mem => patDenote (ps _ mem) (expDenote e))
adamc@177:           (fun _ mem env => expDenote (es _ mem env))
adamc@177:       end.
adamc@177: 
adamc@177:     Definition ExpDenote t (E : Exp t) := expDenote (E _).
adamc@177:   End Source.
adamc@177: 
adamc@177:   Import Source.
adamc@177: 
adamc@178:   Module Elab.
adamc@177:     Section vars.
adamc@177:       Variable var : type -> Type.
adamc@177: 
adamc@177:       Inductive exp : type -> Type :=
adamc@177:       | Var : forall t,
adamc@177:         var t
adamc@177:         -> exp t
adamc@177: 
adamc@177:       | EUnit : exp Unit
adamc@177: 
adamc@177:       | App : forall t1 t2,
adamc@177:         exp (t1 --> t2)
adamc@177:         -> exp t1
adamc@177:         -> exp t2
adamc@177:       | Abs : forall t1 t2,
adamc@177:         (var t1 -> exp t2)
adamc@177:         -> exp (t1 --> t2)
adamc@177: 
adamc@177:       | Pair : forall t1 t2,
adamc@177:         exp t1
adamc@177:         -> exp t2
adamc@177:         -> exp (t1 ** t2)
adamc@177:       | Fst : forall t1 t2,
adamc@177:         exp (t1 ** t2)
adamc@177:         -> exp t1
adamc@177:       | Snd : forall t1 t2,
adamc@177:         exp (t1 ** t2)
adamc@177:         -> exp t2
adamc@177: 
adamc@177:       | EInl : forall t1 t2,
adamc@177:         exp t1
adamc@177:         -> exp (t1 ++ t2)
adamc@177:       | EInr : forall t1 t2,
adamc@177:         exp t2
adamc@177:         -> exp (t1 ++ t2)
adamc@177:       | Case : forall t1 t2 t,
adamc@177:         exp (t1 ++ t2)
adamc@177:         -> (var t1 -> exp t)
adamc@177:         -> (var t2 -> exp t)
adamc@177:         -> exp t.
adamc@177:     End vars.
adamc@177: 
adamc@177:     Definition Exp t := forall var, exp var t.
adamc@177: 
adamc@177:     Implicit Arguments Var [var t].
adamc@177:     Implicit Arguments EUnit [var].
adamc@177:     Implicit Arguments App [var t1 t2].
adamc@177:     Implicit Arguments Abs [var t1 t2].
adamc@177:     Implicit Arguments Pair [var t1 t2].
adamc@177:     Implicit Arguments Fst [var t1 t2].
adamc@177:     Implicit Arguments Snd [var t1 t2].
adamc@177:     Implicit Arguments EInl [var t1 t2].
adamc@177:     Implicit Arguments EInr [var t1 t2].
adamc@177:     Implicit Arguments Case [var t1 t2 t].
adamc@177: 
adamc@177: 
adamc@177:     Notation "# v" := (Var v) (at level 70) : elab_scope.
adamc@177: 
adamc@177:     Notation "()" := EUnit : elab_scope.
adamc@177: 
adamc@177:     Infix "@" := App (left associativity, at level 77) : elab_scope.
adamc@177:     Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : elab_scope.
adamc@177:     Notation "\ ? , e" := (Abs (fun _ => e)) (at level 78) : elab_scope.
adamc@177: 
adamc@179:     Notation "[ x , y ]" := (Pair x y) : elab_scope.
adamc@177:     Notation "#1 e" := (Fst e) (at level 72) : elab_scope.
adamc@177:     Notation "#2 e" := (Snd e) (at level 72) : elab_scope.
adamc@177: 
adamc@177:     Notation "'Inl' e" := (EInl e) (at level 71) : elab_scope.
adamc@177:     Notation "'Inr' e" := (EInr e) (at level 71) : elab_scope.
adamc@177: 
adamc@177:     Bind Scope elab_scope with exp.
adamc@177:     Delimit Scope elab_scope with elab.
adamc@177: 
adamc@177:     Open Scope elab_scope.
adamc@177: 
adamc@177:     Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@177:       match e in (exp _ t) return (typeDenote t) with
adamc@177:         | Var _ v => v
adamc@177: 
adamc@177:         | EUnit => tt
adamc@177: 
adamc@177:         | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@177:         | Abs _ _ e' => fun x => expDenote (e' x)
adamc@177: 
adamc@177:         | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@177:         | Fst _ _ e' => fst (expDenote e')
adamc@177:         | Snd _ _ e' => snd (expDenote e')
adamc@177: 
adamc@177:         | EInl _ _ e' => inl _ (expDenote e')
adamc@177:         | EInr _ _ e' => inr _ (expDenote e')
adamc@177:         | Case _ _ _ e' e1 e2 =>
adamc@177:           match expDenote e' with
adamc@177:             | inl v => expDenote (e1 v)
adamc@177:             | inr v => expDenote (e2 v)
adamc@177:           end
adamc@177:       end.
adamc@177: 
adamc@177:     Definition ExpDenote t (E : Exp t) := expDenote (E _).
adamc@177:   End Elab.
adamc@177: 
adamc@178:   Import Elab.
adamc@178: 
adamc@178:   Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%source
adamc@178:     (right associativity, at level 76, e1 at next level) : source_scope.
adamc@178:   Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%elab
adamc@178:     (right associativity, at level 76, e1 at next level) : elab_scope.
adamc@178: 
adamc@178:   Section choice_tree.
adamc@178:     Open Scope source_scope.
adamc@178: 
adamc@178:     Fixpoint choice_tree var (t : type) (result : Type) : Type :=
adamc@178:       match t with
adamc@178:         | t1 ** t2 =>
adamc@178:           choice_tree var t1
adamc@178:           (choice_tree var t2
adamc@178:             result)
adamc@178:         | t1 ++ t2 =>
adamc@178:           choice_tree var t1 result
adamc@178:           * choice_tree var t2 result
adamc@178:         | t => exp var t -> result
adamc@178:       end%type.
adamc@178: 
adamc@178:     Fixpoint merge var t result {struct t}
adamc@178:       : (result -> result -> result)
adamc@178:       -> choice_tree var t result -> choice_tree var t result -> choice_tree var t result :=
adamc@178:       match t return ((result -> result -> result)
adamc@178:         -> choice_tree var t result -> choice_tree var t result -> choice_tree var t result) with
adamc@178:         | _ ** _ => fun mr ct1 ct2 =>
adamc@178:           merge _ _
adamc@178:           (merge _ _ mr)
adamc@178:           ct1 ct2
adamc@178: 
adamc@178:         | _ ++ _ => fun mr ct1 ct2 =>
adamc@178:           (merge var _ mr (fst ct1) (fst ct2),
adamc@178:             merge var _ mr (snd ct1) (snd ct2))
adamc@178: 
adamc@178:         | _ => fun mr ct1 ct2 e => mr (ct1 e) (ct2 e)
adamc@178:       end.
adamc@178: 
adamc@178:     Fixpoint everywhere var t result {struct t}
adamc@178:       : (exp var t -> result) -> choice_tree var t result :=
adamc@178:       match t return ((exp var t -> result) -> choice_tree var t result) with
adamc@178:         | t1 ** t2 => fun r =>
adamc@178:           everywhere (t := t1) (fun e1 =>
adamc@178:             everywhere (t := t2) (fun e2 =>
adamc@178:               r ([e1, e2])%elab))
adamc@178: 
adamc@178:         | _ ++ _ => fun r =>
adamc@178:           (everywhere (fun e => r (Inl e)%elab),
adamc@178:             everywhere (fun e => r (Inr e)%elab))
adamc@178: 
adamc@178:         | _ => fun r => r
adamc@178:       end.
adamc@178:   End choice_tree.
adamc@178: 
adamc@178:   Implicit Arguments merge [var t result].
adamc@178: 
adamc@178:   Section elaborate.
adamc@178:     Open Local Scope elab_scope.
adamc@178: 
adamc@178:     Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) {struct p} :
adamc@178:       (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result :=
adamc@178:       match p in (pat t1 ts) return ((hlist (exp var) ts -> result)
adamc@178:         -> result -> choice_tree var t1 result) with
adamc@178:         | PVar _ => fun succ fail =>
adamc@178:           everywhere (fun disc => succ (disc, tt))
adamc@178: 
adamc@178:         | PPair _ _ _ _ p1 p2 => fun succ fail =>
adamc@178:           elaboratePat _ p1
adamc@178:           (fun tup1 =>
adamc@178:             elaboratePat _ p2
adamc@178:             (fun tup2 =>
adamc@178:               succ (happ tup1 tup2))
adamc@178:             fail)
adamc@178:           (everywhere (fun _ => fail))
adamc@178: 
adamc@178:         | PInl _ _ _ p' => fun succ fail =>
adamc@178:           (elaboratePat _ p' succ fail,
adamc@178:             everywhere (fun _ => fail))
adamc@178:         | PInr _ _ _ p' => fun succ fail =>
adamc@178:           (everywhere (fun _ => fail),
adamc@178:             elaboratePat _ p' succ fail)
adamc@178:       end.
adamc@178: 
adamc@178:     Implicit Arguments elaboratePat [var t1 ts result].
adamc@178: 
adamc@178:     Fixpoint letify var t ts {struct ts} : (hlist var ts -> exp var t)
adamc@178:       -> hlist (exp var) ts -> exp var t :=
adamc@178:       match ts return ((hlist var ts -> exp var t)
adamc@178:         -> hlist (exp var) ts -> exp var t) with
adamc@178:         | nil => fun f _ => f tt
adamc@178:         | _ :: _ => fun f tup => letify _ (fun tup' => x <- fst tup; f (x, tup')) (snd tup)
adamc@178:       end.
adamc@178: 
adamc@178:     Implicit Arguments letify [var t ts].
adamc@178: 
adamc@178:     Fixpoint expand var result t1 t2
adamc@178:       (out : result -> exp var t2) {struct t1}
adamc@178:       : forall ct : choice_tree var t1 result,
adamc@178:         exp var t1
adamc@178:         -> exp var t2 :=
adamc@178:         match t1 return (forall ct : choice_tree var t1 result, exp var t1
adamc@178:           -> exp var t2) with
adamc@178:           | (_ ** _)%source => fun ct disc =>
adamc@178:             expand
adamc@178:             (fun ct' => expand out ct' (#2 disc)%source)
adamc@178:             ct
adamc@178:             (#1 disc)
adamc@178:             
adamc@178:           | (_ ++ _)%source => fun ct disc =>
adamc@178:             Case disc
adamc@178:             (fun x => expand out (fst ct) (#x))
adamc@178:             (fun y => expand out (snd ct) (#y))
adamc@178:                   
adamc@178:           | _ => fun ct disc =>
adamc@178:             x <- disc; out (ct (#x))
adamc@178:         end.
adamc@178: 
adamc@178:     Definition mergeOpt A (o1 o2 : option A) :=
adamc@178:       match o1 with
adamc@178:         | None => o2
adamc@178:         | _ => o1
adamc@178:       end.
adamc@178: 
adamc@178:     Import Source.
adamc@178: 
adamc@178:     Fixpoint elaborateMatches var t1 t2
adamc@178:       (tss : list (list type)) {struct tss}
adamc@178:       : (forall ts, member ts tss -> pat t1 ts)
adamc@178:       -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2)
adamc@178:       -> choice_tree var t1 (option (Elab.exp var t2)) :=
adamc@178:       match tss return (forall ts, member ts tss -> pat t1 ts)
adamc@178:         -> (forall ts, member ts tss -> _)
adamc@178:         -> _ with
adamc@178:         | nil => fun _ _ =>
adamc@178:           everywhere (fun _ => None)
adamc@178:         | ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts')
adamc@178:           (es : forall ts', member ts' (ts :: tss') -> hlist var ts' -> Elab.exp var t2) =>
adamc@178:           merge (@mergeOpt _)
adamc@178:           (elaboratePat (ps _ (hfirst (refl_equal _)))
adamc@178:             (fun ts => Some (letify
adamc@178:               (fun ts' => es _ (hfirst (refl_equal _)) ts')
adamc@178:               ts))
adamc@178:             None)
adamc@178:           (elaborateMatches tss'
adamc@178:             (fun _ mem => ps _ (hnext mem))
adamc@178:             (fun _ mem => es _ (hnext mem)))
adamc@178:       end.
adamc@178: 
adamc@178:     Implicit Arguments elaborateMatches [var t1 t2 tss].
adamc@178: 
adamc@178:     Open Scope cps_scope.
adamc@178: 
adamc@178:     Fixpoint elaborate var t (e : Source.exp var t) {struct e} : Elab.exp var t :=
adamc@178:       match e in (Source.exp _ t) return (Elab.exp var t) with
adamc@178:         | Var _ v => #v
adamc@178: 
adamc@178:         | EUnit => ()
adamc@178: 
adamc@178:         | App _ _ e1 e2 => elaborate e1 @ elaborate e2
adamc@178:         | Abs _ _ e' => \x, elaborate (e' x) 
adamc@178: 
adamc@178:         | Pair _ _ e1 e2 => [elaborate e1, elaborate e2]
adamc@178:         | EInl _ _ e' => Inl (elaborate e')
adamc@178:         | EInr _ _ e' => Inr (elaborate e')
adamc@178: 
adamc@178:         | Case _ _ _ e' ps es def =>
adamc@178:           expand
adamc@178:           (fun eo => match eo with
adamc@178:                        | None => elaborate def
adamc@178:                        | Some e => e
adamc@178:                      end)
adamc@178:           (elaborateMatches ps (fun _ mem env => elaborate (es _ mem env)))
adamc@178:           (elaborate e')
adamc@178:       end.
adamc@178:   End elaborate.
adamc@178: 
adamc@178:   Definition Elaborate t (E : Source.Exp t) : Elab.Exp t :=
adamc@178:     fun _ => elaborate (E _).
adamc@178: 
adamc@179:   Fixpoint grab t result : choice_tree typeDenote t result -> typeDenote t -> result :=
adamc@179:     match t return (choice_tree typeDenote t result -> typeDenote t -> result) with
adamc@179:       | t1 ** t2 => fun ct v =>
adamc@179:         grab t2 _ (grab t1 _ ct (fst v)) (snd v)
adamc@179:       | t1 ++ t2 => fun ct v =>
adamc@179:         match v with
adamc@179:           | inl v' => grab t1 _ (fst ct) v'
adamc@179:           | inr v' => grab t2 _ (snd ct) v'
adamc@179:         end
adamc@179:       | t => fun ct v => ct (#v)%elab
adamc@179:     end%source%type.
adamc@179: 
adamc@179:   Implicit Arguments grab [t result].
adamc@179: 
adamc@179:   Ltac my_crush :=
adamc@179:     crush;
adamc@179:     repeat (match goal with
adamc@179:               | [ |- context[match ?E with inl _ => _ | inr _ => _ end] ] =>
adamc@179:                 destruct E
adamc@179:             end; crush).
adamc@179: 
adamc@179:   Lemma expand_grab : forall t2 t1 result
adamc@179:     (out : result -> Elab.exp typeDenote t2)
adamc@179:     (ct : choice_tree typeDenote t1 result)
adamc@179:     (disc : Elab.exp typeDenote t1),
adamc@179:     Elab.expDenote (expand out ct disc) = Elab.expDenote (out (grab ct (Elab.expDenote disc))).
adamc@179:     induction t1; my_crush.
adamc@179:   Qed.
adamc@179: 
adamc@179:   Lemma recreate_pair : forall t1 t2
adamc@179:     (x : Elab.exp typeDenote t1)
adamc@179:     (x0 : Elab.exp typeDenote t2)
adamc@179:     (v : typeDenote (t1 ** t2)),
adamc@179:     expDenote x = fst v
adamc@179:     -> expDenote x0 = snd v
adamc@179:     -> @eq (typeDenote t1 * typeDenote t2) (expDenote [x, x0]) v.
adamc@179:     destruct v; crush.
adamc@179:   Qed.
adamc@179: 
adamc@179:   Lemma everywhere_correct : forall t1 result
adamc@179:     (succ : Elab.exp typeDenote t1 -> result) disc,
adamc@179:     exists disc', grab (everywhere succ) (Elab.expDenote disc) = succ disc'
adamc@179:       /\ Elab.expDenote disc' = Elab.expDenote disc.
adamc@179:     Hint Resolve recreate_pair.
adamc@179: 
adamc@179:     induction t1; my_crush; eauto; fold choice_tree;
adamc@179:       repeat (fold typeDenote in *; crush;
adamc@179:         match goal with
adamc@179:           | [ IH : forall result succ, _ |- context[grab (everywhere ?S) _] ] =>
adamc@179:             generalize (IH _ S); clear IH
adamc@179:           | [ e : exp typeDenote (?T ** _), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
adamc@179:             generalize (IH (#1 e)); clear IH
adamc@179:           | [ e : exp typeDenote (_ ** ?T), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
adamc@179:             generalize (IH (#2 e)); clear IH
adamc@179:           | [ e : typeDenote ?T, IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
adamc@179:             generalize (IH (#e)); clear IH
adamc@179:         end; crush); eauto.
adamc@179:   Qed.
adamc@179: 
adamc@179:   Lemma merge_correct : forall t result
adamc@179:     (ct1 ct2 : choice_tree typeDenote t result)
adamc@179:     (mr : result -> result -> result) v,
adamc@179:     grab (merge mr ct1 ct2) v = mr (grab ct1 v) (grab ct2 v).
adamc@179:     induction t; crush.
adamc@179:   Qed.
adamc@179: 
adamc@179:   Lemma everywhere_fail : forall t result
adamc@179:     (fail : result) v,
adamc@179:     grab (everywhere (fun _ : Elab.exp typeDenote t => fail)) v = fail.
adamc@179:     induction t; crush.
adamc@179:   Qed.
adamc@179: 
adamc@179:   Lemma elaboratePat_correct : forall t1 ts (p : pat t1 ts)
adamc@179:     result (succ : hlist (Elab.exp typeDenote) ts -> result)
adamc@179:     (fail : result) v env,
adamc@179:     patDenote p v = Some env
adamc@179:     -> exists env', grab (elaboratePat typeDenote p succ fail) v = succ env'
adamc@179:       /\ env = hmap Elab.expDenote env'.
adamc@179:     Hint Resolve hmap_happ.
adamc@179: 
adamc@179:     induction p; crush; fold choice_tree;
adamc@179:       repeat (match goal with
adamc@179:                 | [ |- context[grab (everywhere ?succ) ?v] ] =>
adamc@179:                   generalize (everywhere_correct succ (#v)%elab)
adamc@179: 
adamc@179:                 | [ H : forall result sudc fail, _ |- context[grab (elaboratePat _ _ ?S ?F) ?V] ] =>
adamc@179:                   generalize (H _ S F V); clear H
adamc@179:                 | [ H1 : context[match ?E with Some _ => _ | None => _ end],
adamc@179:                   H2 : forall env, ?E = Some env -> _ |- _ ] =>
adamc@179:                 destruct E
adamc@179:                 | [ H : forall env, Some ?E = Some env -> _ |- _ ] =>
adamc@179:                   generalize (H _ (refl_equal _)); clear H
adamc@179:               end; crush); eauto.
adamc@179:   Qed.
adamc@179: 
adamc@179:   Lemma elaboratePat_fails : forall t1 ts (p : pat t1 ts)
adamc@179:     result (succ : hlist (Elab.exp typeDenote) ts -> result)
adamc@179:     (fail : result) v,
adamc@179:     patDenote p v = None
adamc@179:     -> grab (elaboratePat typeDenote p succ fail) v = fail.
adamc@179:     Hint Resolve everywhere_fail.
adamc@179: 
adamc@179:     induction p; try solve [ crush ];
adamc@179:       simpl; fold choice_tree; intuition; simpl in *;
adamc@179:         repeat match goal with
adamc@179:                  | [ IH : forall result succ fail v, patDenote ?P v = _ -> _
adamc@179:                    |- context[grab (elaboratePat _ ?P ?S ?F) ?V] ] =>
adamc@179:                    generalize (IH _ S F V); clear IH; intro IH;
adamc@179:                      generalize (elaboratePat_correct P S F V); intros;
adamc@179:                        destruct (patDenote P V); try discriminate
adamc@179:                  | [ H : forall env, Some _ = Some env -> _ |- _ ] =>
adamc@179:                    destruct (H _ (refl_equal _)); clear H; intuition
adamc@179:                  | [ H : _ |- _ ] => rewrite H; intuition
adamc@179:                end.
adamc@179:   Qed.
adamc@179: 
adamc@179:   Implicit Arguments letify [var t ts].
adamc@179: 
adamc@179:   Lemma letify_correct : forall t ts (f : hlist typeDenote ts -> Elab.exp typeDenote t)
adamc@179:     (env : hlist (Elab.exp typeDenote) ts),
adamc@179:     Elab.expDenote (letify f env)
adamc@179:     = Elab.expDenote (f (hmap Elab.expDenote env)).
adamc@179:     induction ts; crush.
adamc@179:   Qed.
adamc@179: 
adamc@179:   Theorem elaborate_correct : forall t (e : Source.exp typeDenote t),
adamc@179:     Elab.expDenote (elaborate e) = Source.expDenote e.
adamc@179:     Hint Rewrite expand_grab merge_correct letify_correct : cpdt.
adamc@179:     Hint Rewrite everywhere_fail elaboratePat_fails using assumption : cpdt.
adamc@179: 
adamc@179:     induction e; crush; try (ext_eq; crush);
adamc@179:       match goal with
adamc@179:         | [ tss : list (list type) |- _ ] =>
adamc@179:           induction tss; crush;
adamc@179:             match goal with
adamc@179:               | [ |- context[grab (elaboratePat _ ?P ?S ?F) ?V] ] =>
adamc@179:                 case_eq (patDenote P V); [intros env Heq;
adamc@179:                   destruct (elaboratePat_correct P S F _ Heq); crush;
adamc@179:                     match goal with
adamc@179:                       | [ H : _ |- _ ] => rewrite <- H; crush
adamc@179:                     end
adamc@179:                   | crush ]
adamc@179:             end
adamc@179:       end.
adamc@179:   Qed.
adamc@179: 
adamc@179:   Theorem Elaborate_correct : forall t (E : Source.Exp t),
adamc@179:     Elab.ExpDenote (Elaborate E) = Source.ExpDenote E.
adamc@179:     unfold Elab.ExpDenote, Elaborate, Source.ExpDenote;
adamc@179:       intros; apply elaborate_correct.
adamc@179:   Qed.
adamc@179: 
adamc@177: End PatMatch.