adamc@158: (* Copyright (c) 2008, Adam Chlipala
adamc@158:  * 
adamc@158:  * This work is licensed under a
adamc@158:  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@158:  * Unported License.
adamc@158:  * The license text is available at:
adamc@158:  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@158:  *)
adamc@158: 
adamc@158: (* begin hide *)
adamc@158: Require Import Arith Eqdep String List.
adamc@158: 
adamc@160: Require Import Axioms DepList Tactics.
adamc@158: 
adamc@158: Set Implicit Arguments.
adamc@158: (* end hide *)
adamc@158: 
adamc@158: 
adamc@158: (** %\chapter{Higher-Order Abstract Syntax}% *)
adamc@158: 
adamc@158: (** TODO: Prose for this chapter *)
adamc@158: 
adamc@158: 
adamc@158: (** * Parametric Higher-Order Abstract Syntax *)
adamc@158: 
adamc@158: Inductive type : Type :=
adamc@159: | Nat : type
adamc@158: | Arrow : type -> type -> type.
adamc@158: 
adamc@158: Infix "-->" := Arrow (right associativity, at level 60).
adamc@158: 
adamc@158: Section exp.
adamc@158:   Variable var : type -> Type.
adamc@158: 
adamc@158:   Inductive exp : type -> Type :=
adamc@159:   | Const' : nat -> exp Nat
adamc@159:   | Plus' : exp Nat -> exp Nat -> exp Nat
adamc@159: 
adamc@158:   | Var : forall t, var t -> exp t
adamc@158:   | App' : forall dom ran, exp (dom --> ran) -> exp dom -> exp ran
adamc@158:   | Abs' : forall dom ran, (var dom -> exp ran) -> exp (dom --> ran).
adamc@158: End exp.
adamc@158: 
adamc@158: Implicit Arguments Const' [var].
adamc@158: Implicit Arguments Var [var t].
adamc@158: Implicit Arguments Abs' [var dom ran].
adamc@158: 
adamc@158: Definition Exp t := forall var, exp var t.
adamc@158: Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2.
adamc@158: 
adamc@159: Definition Const (n : nat) : Exp Nat :=
adamc@159:   fun _ => Const' n.
adamc@159: Definition Plus (E1 E2 : Exp Nat) : Exp Nat :=
adamc@159:   fun _ => Plus' (E1 _) (E2 _).
adamc@158: Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran :=
adamc@158:   fun _ => App' (F _) (X _).
adamc@158: Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) :=
adamc@158:   fun _ => Abs' (B _).
adamc@158: 
adamc@158: Section flatten.
adamc@158:   Variable var : type -> Type.
adamc@158: 
adamc@158:   Fixpoint flatten t (e : exp (exp var) t) {struct e} : exp var t :=
adamc@158:     match e in exp _ t return exp _ t with
adamc@159:       | Const' n => Const' n
adamc@159:       | Plus' e1 e2 => Plus' (flatten e1) (flatten e2)
adamc@158:       | Var _ e' => e'
adamc@158:       | App' _ _ e1 e2 => App' (flatten e1) (flatten e2)
adamc@158:       | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x)))
adamc@158:     end.
adamc@158: End flatten.
adamc@158: 
adamc@158: Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ =>
adamc@158:   flatten (E2 _ (E1 _)).
adamc@158: 
adamc@158: 
adamc@158: (** * A Type Soundness Proof *)
adamc@158: 
adamc@158: Reserved Notation "E1 ==> E2" (no associativity, at level 90).
adamc@158: 
adamc@158: Inductive Val : forall t, Exp t -> Prop :=
adamc@159: | VConst : forall n, Val (Const n)
adamc@158: | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B).
adamc@158: 
adamc@158: Hint Constructors Val.
adamc@158: 
adamc@162: Inductive Ctx : type -> type -> Type :=
adamc@162: | AppCong1 : forall (dom ran : type),
adamc@162:   Exp dom -> Ctx (dom --> ran) ran
adamc@162: | AppCong2 : forall (dom ran : type),
adamc@162:   Exp (dom --> ran) -> Ctx dom ran
adamc@162: | PlusCong1 : Exp Nat -> Ctx Nat Nat
adamc@162: | PlusCong2 : Exp Nat -> Ctx Nat Nat.
adamc@162: 
adamc@162: Inductive isCtx : forall t1 t2, Ctx t1 t2 -> Prop :=
adamc@162: | IsApp1 : forall dom ran (X : Exp dom), isCtx (AppCong1 ran X)
adamc@162: | IsApp2 : forall dom ran (F : Exp (dom --> ran)), Val F -> isCtx (AppCong2 F)
adamc@162: | IsPlus1 : forall E2, isCtx (PlusCong1 E2)
adamc@162: | IsPlus2 : forall E1, Val E1 -> isCtx (PlusCong2 E1).
adamc@162: 
adamc@162: Definition plug t1 t2 (C : Ctx t1 t2) : Exp t1 -> Exp t2 :=
adamc@162:   match C in Ctx t1 t2 return Exp t1 -> Exp t2 with
adamc@162:     | AppCong1 _ _ X => fun F => App F X
adamc@162:     | AppCong2 _ _ F => fun X => App F X
adamc@162:     | PlusCong1 E2 => fun E1 => Plus E1 E2
adamc@162:     | PlusCong2 E1 => fun E2 => Plus E1 E2
adamc@162:   end.
adamc@162: 
adamc@162: Infix "@" := plug (no associativity, at level 60).
adamc@162: 
adamc@158: Inductive Step : forall t, Exp t -> Exp t -> Prop :=
adamc@158: | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom),
adamc@160:   Val X
adamc@160:   -> App (Abs B) X ==> Subst X B
adamc@159: | Sum : forall n1 n2,
adamc@159:   Plus (Const n1) (Const n2) ==> Const (n1 + n2)
adamc@162: | Cong : forall t t' (C : Ctx t t') E E' E1,
adamc@162:   isCtx C
adamc@162:   -> E1 = C @ E
adamc@162:   -> E ==> E'
adamc@162:   -> E1 ==> C @ E'
adamc@159: 
adamc@158:   where "E1 ==> E2" := (Step E1 E2).
adamc@158: 
adamc@162: Hint Constructors isCtx Step.
adamc@158: 
adamc@158: Inductive Closed : forall t, Exp t -> Prop :=
adamc@164: | CConst : forall n,
adamc@164:   Closed (Const n)
adamc@159: | CPlus : forall E1 E2,
adamc@159:   Closed E1
adamc@159:   -> Closed E2
adamc@159:   -> Closed (Plus E1 E2)
adamc@158: | CApp : forall dom ran (E1 : Exp (dom --> ran)) E2,
adamc@158:   Closed E1
adamc@158:   -> Closed E2
adamc@158:   -> Closed (App E1 E2)
adamc@158: | CAbs : forall dom ran (E1 : Exp1 dom ran),
adamc@158:   Closed (Abs E1).
adamc@158: 
adamc@158: Axiom closed : forall t (E : Exp t), Closed E.
adamc@158: 
adamc@163: Ltac my_subst :=
adamc@163:   repeat match goal with
adamc@163:            | [ x : type |- _ ] => subst x
adamc@163:          end.
adamc@163: 
adamc@160: Ltac my_crush' :=
adamc@163:   crush; my_subst;
adamc@158:   repeat (match goal with
adamc@158:             | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H
adamc@163:           end; crush; my_subst).
adamc@163: 
adamc@163: Ltac equate_conj F G :=
adamc@163:   match constr:(F, G) with
adamc@163:     | (_ ?x1, _ ?x2) => constr:(x1 = x2)
adamc@163:     | (_ ?x1 ?y1, _ ?x2 ?y2) => constr:(x1 = x2 /\ y1 = y2)
adamc@163:     | (_ ?x1 ?y1 ?z1, _ ?x2 ?y2 ?z2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2)
adamc@163:     | (_ ?x1 ?y1 ?z1 ?u1, _ ?x2 ?y2 ?z2 ?u2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2)
adamc@163:     | (_ ?x1 ?y1 ?z1 ?u1 ?v1, _ ?x2 ?y2 ?z2 ?u2 ?v2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2 /\ v1 = v2)
adamc@163:   end.
adamc@158: 
adamc@160: Ltac my_crush :=
adamc@160:   my_crush';
adamc@163:   repeat (match goal with
adamc@163:             | [ H : ?F = ?G |- _ ] =>
adamc@163:               (let H' := fresh "H'" in
adamc@163:                 assert (H' : F (fun _ => unit) = G (fun _ => unit)); [ congruence
adamc@163:                   | discriminate || injection H'; clear H' ];
adamc@163:                 my_crush';
adamc@163:                 repeat match goal with
adamc@163:                          | [ H : context[fun _ => unit] |- _ ] => clear H
adamc@163:                        end;
adamc@163:                 match type of H with
adamc@163:                   | ?F = ?G =>
adamc@163:                     let ec := equate_conj F G in
adamc@163:                       let var := fresh "var" in
adamc@163:                         assert ec; [ intuition; unfold Exp; apply ext_eq; intro var;
adamc@163:                           assert (H' : F var = G var); try congruence;
adamc@163:                             match type of H' with
adamc@163:                               | ?X = ?Y =>
adamc@163:                                 let X := eval hnf in X in
adamc@163:                                   let Y := eval hnf in Y in
adamc@163:                                     change (X = Y) in H'
adamc@163:                             end; injection H'; my_crush'; tauto
adamc@163:                           | intuition; subst ]
adamc@163:                 end);
adamc@163:               clear H
adamc@163:           end; my_crush');
adamc@163:   my_crush'.
adamc@160: 
adamc@162: Hint Extern 1 (_ = _ @ _) => simpl.
adamc@162: 
adamc@158: Lemma progress' : forall t (E : Exp t),
adamc@158:   Closed E
adamc@158:   -> Val E \/ exists E', E ==> E'.
adamc@158:   induction 1; crush;
adamc@159:     repeat match goal with
adamc@159:              | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush
adamc@162:            end; eauto 6.
adamc@158: Qed.
adamc@158: 
adamc@158: Theorem progress : forall t (E : Exp t),
adamc@158:   Val E \/ exists E', E ==> E'.
adamc@158:   intros; apply progress'; apply closed.
adamc@158: Qed.
adamc@158: 
adamc@160: 
adamc@160: (** * Big-Step Semantics *)
adamc@160: 
adamc@160: Reserved Notation "E1 ===> E2" (no associativity, at level 90).
adamc@160: 
adamc@160: Inductive BigStep : forall t, Exp t -> Exp t -> Prop :=
adamc@160: | SConst : forall n,
adamc@160:   Const n ===> Const n
adamc@160: | SPlus : forall E1 E2 n1 n2,
adamc@160:   E1 ===> Const n1
adamc@160:   -> E2 ===> Const n2
adamc@160:   -> Plus E1 E2 ===> Const (n1 + n2)
adamc@160: 
adamc@160: | SApp : forall dom ran (E1 : Exp (dom --> ran)) E2 B V2 V,
adamc@160:   E1 ===> Abs B
adamc@160:   -> E2 ===> V2
adamc@160:   -> Subst V2 B ===> V
adamc@160:   -> App E1 E2 ===> V
adamc@160: | SAbs : forall dom ran (B : Exp1 dom ran),
adamc@160:   Abs B ===> Abs B
adamc@160: 
adamc@160:   where "E1 ===> E2" := (BigStep E1 E2).
adamc@160: 
adamc@160: Hint Constructors BigStep.
adamc@160: 
adamc@160: Reserved Notation "E1 ==>* E2" (no associativity, at level 90).
adamc@160: 
adamc@160: Inductive MultiStep : forall t, Exp t -> Exp t -> Prop :=
adamc@160: | Done : forall t (E : Exp t), E ==>* E
adamc@160: | OneStep : forall t (E E' E'' : Exp t),
adamc@160:   E ==> E'
adamc@160:   -> E' ==>* E''
adamc@160:   -> E ==>* E''
adamc@160: 
adamc@160:   where "E1 ==>* E2" := (MultiStep E1 E2).
adamc@160: 
adamc@160: Hint Constructors MultiStep.
adamc@160: 
adamc@160: Theorem MultiStep_trans : forall t (E1 E2 E3 : Exp t),
adamc@160:   E1 ==>* E2
adamc@160:   -> E2 ==>* E3
adamc@160:   -> E1 ==>* E3.
adamc@160:   induction 1; eauto.
adamc@160: Qed.
adamc@160: 
adamc@160: Theorem Big_Val : forall t (E V : Exp t),
adamc@160:   E ===> V
adamc@160:   -> Val V.
adamc@160:   induction 1; crush.
adamc@160: Qed.
adamc@160: 
adamc@160: Theorem Val_Big : forall t (V : Exp t),
adamc@160:   Val V
adamc@160:   -> V ===> V.
adamc@160:   destruct 1; crush.
adamc@160: Qed.
adamc@160: 
adamc@160: Hint Resolve Big_Val Val_Big.
adamc@160: 
adamc@162: Lemma Multi_Cong : forall t t' (C : Ctx t t'),
adamc@162:   isCtx C
adamc@162:   -> forall E E', E ==>* E'
adamc@162:     -> C @ E ==>* C @ E'.
adamc@160:   induction 2; crush; eauto.
adamc@160: Qed.
adamc@160: 
adamc@162: Lemma Multi_Cong' : forall t t' (C : Ctx t t') E1 E2 E E',
adamc@162:   isCtx C
adamc@162:   -> E1 = C @ E
adamc@162:   -> E2 = C @ E'
adamc@162:   -> E ==>* E'
adamc@162:   -> E1 ==>* E2.
adamc@162:   crush; apply Multi_Cong; auto.
adamc@162: Qed.
adamc@162: 
adamc@162: Hint Resolve Multi_Cong'.
adamc@162: 
adamc@162: Ltac mtrans E :=
adamc@162:   match goal with
adamc@162:     | [ |- E ==>* _ ] => fail 1
adamc@162:     | _ => apply MultiStep_trans with E; [ solve [ eauto ] | eauto ]
adamc@162:   end.
adamc@160: 
adamc@160: Theorem Big_Multi : forall t (E V : Exp t),
adamc@160:   E ===> V
adamc@160:   -> E ==>* V.
adamc@162:   induction 1; crush; eauto;
adamc@162:     repeat match goal with
adamc@162:              | [ n1 : _, E2 : _ |- _ ] => mtrans (Plus (Const n1) E2)
adamc@162:              | [ n1 : _, n2 : _ |- _ ] => mtrans (Plus (Const n1) (Const n2))
adamc@162:              | [ B : _, E2 : _ |- _ ] => mtrans (App (Abs B) E2)
adamc@162:            end.
adamc@160: Qed.
adamc@160: 
adamc@160: Lemma Big_Val' : forall t (V1 V2 : Exp t),
adamc@160:   Val V2
adamc@160:   -> V1 = V2
adamc@160:   -> V1 ===> V2.
adamc@160:   crush.
adamc@160: Qed.
adamc@160: 
adamc@160: Hint Resolve Big_Val'.
adamc@160: 
adamc@160: Lemma Multi_Big' : forall t (E E' : Exp t),
adamc@160:   E ==> E'
adamc@160:   -> forall E'', E' ===> E''
adamc@160:     -> E ===> E''.
adamc@160:   induction 1; crush; eauto;
adamc@160:     match goal with
adamc@160:       | [ H : _ ===> _ |- _ ] => inversion H; my_crush; eauto
adamc@162:     end;
adamc@162:     match goal with
adamc@162:       | [ H : isCtx _ |- _ ] => inversion H; my_crush; eauto
adamc@160:     end.
adamc@160: Qed.
adamc@160: 
adamc@160: Hint Resolve Multi_Big'.
adamc@160: 
adamc@160: Theorem Multi_Big : forall t (E V : Exp t),
adamc@160:   E ==>* V
adamc@160:   -> Val V
adamc@160:   -> E ===> V.
adamc@160:   induction 1; crush; eauto.
adamc@160: Qed.
adamc@160: 
adamc@160: 
adamc@160: (** * Constant folding *)
adamc@160: 
adamc@160: Section cfold.
adamc@160:   Variable var : type -> Type.
adamc@160: 
adamc@160:   Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
adamc@160:     match e in exp _ t return exp _ t with
adamc@160:       | Const' n => Const' n
adamc@160:       | Plus' e1 e2 =>
adamc@160:         let e1' := cfold e1 in
adamc@160:         let e2' := cfold e2 in
adamc@160:           match e1', e2' with
adamc@160:             | Const' n1, Const' n2 => Const' (n1 + n2)
adamc@160:             | _, _ => Plus' e1' e2'
adamc@160:           end
adamc@160: 
adamc@160:       | Var _ x => Var x
adamc@160:       | App' _ _ e1 e2 => App' (cfold e1) (cfold e2)
adamc@160:       | Abs' _ _ e' => Abs' (fun x => cfold (e' x))
adamc@160:     end.
adamc@160: End cfold.
adamc@160: 
adamc@160: Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@163: Definition Cfold1 t1 t2 (E : Exp1 t1 t2) : Exp1 t1 t2 := fun _ x => cfold (E _ x).
adamc@163: 
adamc@163: Lemma fold_Cfold : forall t (E : Exp t),
adamc@163:   (fun _ => cfold (E _)) = Cfold E.
adamc@163:   reflexivity.
adamc@163: Qed.
adamc@163: 
adamc@163: Hint Rewrite fold_Cfold : fold.
adamc@163: 
adamc@163: Lemma fold_Cfold1 : forall t1 t2 (E : Exp1 t1 t2),
adamc@163:   (fun _ x => cfold (E _ x)) = Cfold1 E.
adamc@163:   reflexivity.
adamc@163: Qed.
adamc@163: 
adamc@164: Hint Rewrite fold_Cfold1 : fold.
adamc@164: 
adamc@163: Lemma fold_Subst_Cfold1 : forall t1 t2 (E : Exp1 t1 t2) (V : Exp t1),
adamc@163:   (fun _ => flatten (cfold (E _ (V _))))
adamc@163:   = Subst V (Cfold1 E).
adamc@163:   reflexivity.
adamc@163: Qed.
adamc@163: 
adamc@163: Axiom cheat : forall T, T.
adamc@163: 
adamc@163: 
adamc@163: Lemma fold_Const : forall n, (fun _ => Const' n) = Const n.
adamc@163:   reflexivity.
adamc@163: Qed.
adamc@163: Lemma fold_Plus : forall (E1 E2 : Exp _), (fun _ => Plus' (E1 _) (E2 _)) = Plus E1 E2.
adamc@163:   reflexivity.
adamc@163: Qed.
adamc@163: Lemma fold_App : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom),
adamc@163:   (fun _ => App' (F _) (X _)) = App F X.
adamc@163:   reflexivity.
adamc@163: Qed.
adamc@163: Lemma fold_Abs : forall dom ran (B : Exp1 dom ran),
adamc@163:   (fun _ => Abs' (B _)) = Abs B.
adamc@163:   reflexivity.
adamc@163: Qed.
adamc@163: 
adamc@163: Hint Rewrite fold_Const fold_Plus fold_App fold_Abs : fold.
adamc@163: 
adamc@163: Lemma fold_Subst : forall t1 t2 (E1 : Exp1 t1 t2) (V : Exp t1),
adamc@163:   (fun _ => flatten (E1 _ (V _))) = Subst V E1.
adamc@163:   reflexivity.
adamc@163: Qed.
adamc@163: 
adamc@163: Hint Rewrite fold_Subst : fold.
adamc@163: 
adamc@163: Section Closed1.
adamc@163:   Variable xt : type.
adamc@163: 
adamc@163:   Definition Const1 (n : nat) : Exp1 xt Nat :=
adamc@163:     fun _ _ => Const' n.
adamc@163:   Definition Var1 : Exp1 xt xt := fun _ x => Var x.
adamc@163:   Definition Plus1 (E1 E2 : Exp1 xt Nat) : Exp1 xt Nat :=
adamc@163:     fun _ s => Plus' (E1 _ s) (E2 _ s).
adamc@163:   Definition App1 dom ran (F : Exp1 xt (dom --> ran)) (X : Exp1 xt dom) : Exp1 xt ran :=
adamc@163:     fun _ s => App' (F _ s) (X _ s).
adamc@163:   Definition Abs1 dom ran (B : forall var, var dom -> Exp1 xt ran) : Exp1 xt (dom --> ran) :=
adamc@163:     fun _ s => Abs' (fun x => B _ x _ s).
adamc@163: 
adamc@163:   Inductive Closed1 : forall t, Exp1 xt t -> Prop :=
adamc@164:   | CConst1 : forall n,
adamc@164:     Closed1 (Const1 n)
adamc@163:   | CPlus1 : forall E1 E2,
adamc@163:     Closed1 E1
adamc@163:     -> Closed1 E2
adamc@163:     -> Closed1 (Plus1 E1 E2)
adamc@163:   | CApp1 : forall dom ran (E1 : Exp1 _ (dom --> ran)) E2,
adamc@163:     Closed1 E1
adamc@163:     -> Closed1 E2
adamc@163:     -> Closed1 (App1 E1 E2)
adamc@163:   | CAbs1 : forall dom ran (E1 : forall var, var dom -> Exp1 _ ran),
adamc@163:     Closed1 (Abs1 E1).
adamc@163: 
adamc@163:   Axiom closed1 : forall t (E : Exp1 xt t), Closed1 E.
adamc@163: End Closed1.
adamc@163: 
adamc@163: Hint Resolve closed1.
adamc@163: 
adamc@164: Ltac ssimp := unfold Subst, Cfold in *; simpl in *; autorewrite with fold in *;
adamc@163:   repeat match goal with
adamc@163:            | [ xt : type |- _ ] =>
adamc@163:              rewrite (@fold_Subst xt) in *
adamc@163:          end;
adamc@163:   autorewrite with fold in *.
adamc@163: 
adamc@164: Lemma Cfold_Subst' : forall t (E V : Exp t),
adamc@164:   E ===> V
adamc@164:   -> forall t' B (V' : Exp t') V'', E = Cfold (Subst V' B)
adamc@164:     -> V = Cfold V'' 
adamc@164:     -> Closed1 B
adamc@164:     -> Subst (Cfold V') (Cfold1 B) ===> Cfold V''.
adamc@164:   induction 1; inversion 3; my_crush; ssimp; my_crush.
adamc@163: 
adamc@164:   rewrite <- H0; auto.
adamc@163: 
adamc@163:   apply cheat.
adamc@164:   apply cheat.
adamc@163:   apply cheat.
adamc@163: 
adamc@164:   repeat rewrite (@fold_Subst_Cfold1 t') in *.
adamc@164:   repeat rewrite fold_Cfold in *.
adamc@164:   apply SApp with (Cfold1 B) V2.
adamc@163: 
adamc@164:   unfold Abs, Subst, Cfold, Cfold1 in *.
adamc@164:   match goal with
adamc@164:     | [ |- _ ===> ?F ] =>
adamc@164:       replace F with (fun var => cfold (Abs' (fun x : var _ => B var x)))
adamc@164:   end.
adamc@164:   apply IHBigStep1; auto.
adamc@164:   apply cheat.
adamc@164:   reflexivity.
adamc@163: 
adamc@164:   replace V2 with (Cfold V2).
adamc@164:   unfold Cfold, Subst.
adamc@164:   apply IHBigStep2; auto.
adamc@164:   apply cheat.
adamc@164:   apply cheat.
adamc@163: 
adamc@164:   replace V2 with (Cfold V2).
adamc@164:   unfold Subst, Cfold.
adamc@164:   apply IHBigStep3; auto.
adamc@164:   apply cheat.
adamc@164:   apply cheat.
adamc@163: 
adamc@164:   apply cheat.  
adamc@164: Qed.
adamc@163: 
adamc@163: Theorem Cfold_Subst : forall t1 t2 (V : Exp t1) B (V' : Exp t2),
adamc@164:   Subst (Cfold V) (Cfold1 B) ===> Cfold V'
adamc@163:   -> Subst (Cfold V) (Cfold1 B) ===> Cfold V'.
adamc@164:   Hint Resolve Cfold_Subst'.
adamc@164: 
adamc@164:   eauto.
adamc@164: Qed.
adamc@164: 
adamc@164: Hint Resolve Cfold_Subst.
adamc@163: 
adamc@163: Theorem Cfold_correct : forall t (E V : Exp t),
adamc@163:   E ===> V
adamc@163:   -> Cfold E ===> Cfold V.
adamc@164:   induction 1; unfold Cfold in *; crush; ssimp; eauto.
adamc@163: 
adamc@164:   change ((fun H1 : type -> Type =>
adamc@164:     match Cfold E1 H1 with
adamc@164:       | Const' n3 =>
adamc@164:         match Cfold E2 H1 with
adamc@164:           | Const' n4 => Const' (var:=H1) (n3 + n4)
adamc@164:           | Plus' _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1))
adamc@164:           | Var _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1))
adamc@164:           | App' _ _ _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1))
adamc@164:           | Abs' _ _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1))
adamc@164:         end
adamc@164:       | Plus' _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1))
adamc@164:       | Var _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1))
adamc@164:       | App' _ _ _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1))
adamc@164:       | Abs' _ _ _ => Plus' (cfold (E1 H1)) (cfold (E2 H1))
adamc@164:     end) ===> Const (n1 + n2)).
adamc@163: 
adamc@164:   Ltac simp :=
adamc@164:     repeat match goal with
adamc@164:              | [ H : _ = Cfold _ |- _ ] => rewrite <- H in *
adamc@164:              | [ H : Const _ ===> Const _ |- _ ] =>
adamc@164:                inversion H; clear H; my_crush
adamc@164:            end.
adamc@163: 
adamc@164:   generalize (closed (Cfold E1)); inversion 1; my_crush; simp;
adamc@164:     try solve [ ssimp; simp; eauto ];
adamc@164:       generalize (closed (Cfold E2)); inversion 1; my_crush; simp; ssimp; simp; eauto.
adamc@164: Qed.