# HG changeset patch # User Adam Chlipala # Date 1225835150 18000 # Node ID ba306bf9ec80172b8e29587e913d836e9b0c5c1b # Parent df02642f93b86fb427fecd1cfc724cceaec209ca Feeling stuck with Hoas diff -r df02642f93b8 -r ba306bf9ec80 src/DepList.v --- a/src/DepList.v Tue Nov 04 12:39:28 2008 -0500 +++ b/src/DepList.v Tue Nov 04 16:45:50 2008 -0500 @@ -142,3 +142,18 @@ Infix ":::" := hcons (right associativity, at level 60). Infix "+++" := happ (right associativity, at level 60). + +Section hmap. + Variable A : Type. + Variables B1 B2 : A -> Type. + + Variable f : forall x, B1 x -> B2 x. + + Fixpoint hmap (ls : list A) : hlist B1 ls -> hlist B2 ls := + match ls return hlist B1 ls -> hlist B2 ls with + | nil => fun _ => hnil + | _ :: _ => fun hl => f (fst hl) ::: hmap _ (snd hl) + end. +End hmap. + +Implicit Arguments hmap [A B1 B2 ls]. diff -r df02642f93b8 -r ba306bf9ec80 src/Hoas.v --- a/src/Hoas.v Tue Nov 04 12:39:28 2008 -0500 +++ b/src/Hoas.v Tue Nov 04 16:45:50 2008 -0500 @@ -140,42 +140,54 @@ Axiom closed : forall t (E : Exp t), Closed E. +Ltac my_subst := + repeat match goal with + | [ x : type |- _ ] => subst x + end. + Ltac my_crush' := - crush; + crush; my_subst; repeat (match goal with | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H - end; crush). + end; crush; my_subst). + +Ltac equate_conj F G := + match constr:(F, G) with + | (_ ?x1, _ ?x2) => constr:(x1 = x2) + | (_ ?x1 ?y1, _ ?x2 ?y2) => constr:(x1 = x2 /\ y1 = y2) + | (_ ?x1 ?y1 ?z1, _ ?x2 ?y2 ?z2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2) + | (_ ?x1 ?y1 ?z1 ?u1, _ ?x2 ?y2 ?z2 ?u2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2) + | (_ ?x1 ?y1 ?z1 ?u1 ?v1, _ ?x2 ?y2 ?z2 ?u2 ?v2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2 /\ v1 = v2) + end. Ltac my_crush := my_crush'; - try (match goal with - | [ H : ?F = ?G |- _ ] => - match goal with - (*| [ _ : F (fun _ => unit) = G (fun _ => unit) |- _ ] => fail 1*) - | _ => - let H' := fresh "H'" in - assert (H' : F (fun _ => unit) = G (fun _ => unit)); [ congruence - | discriminate || injection H' ]; - clear H' - end - end; my_crush'); - repeat match goal with - | [ H : ?F = ?G, H2 : ?X (fun _ => unit) = ?Y (fun _ => unit) |- _ ] => - match X with - | Y => fail 1 - | _ => - assert (X = Y); [ unfold Exp; apply ext_eq; intro var; - let H' := fresh "H'" in - assert (H' : F var = G var); [ congruence - | match type of H' with - | ?X = ?Y => - let X := eval hnf in X in - let Y := eval hnf in Y in - change (X = Y) in H' - end; injection H'; clear H'; my_crush' ] - | my_crush'; clear H2 ] - end - end. + repeat (match goal with + | [ H : ?F = ?G |- _ ] => + (let H' := fresh "H'" in + assert (H' : F (fun _ => unit) = G (fun _ => unit)); [ congruence + | discriminate || injection H'; clear H' ]; + my_crush'; + repeat match goal with + | [ H : context[fun _ => unit] |- _ ] => clear H + end; + match type of H with + | ?F = ?G => + let ec := equate_conj F G in + let var := fresh "var" in + assert ec; [ intuition; unfold Exp; apply ext_eq; intro var; + assert (H' : F var = G var); try congruence; + match type of H' with + | ?X = ?Y => + let X := eval hnf in X in + let Y := eval hnf in Y in + change (X = Y) in H' + end; injection H'; my_crush'; tauto + | intuition; subst ] + end); + clear H + end; my_crush'); + my_crush'. Hint Extern 1 (_ = _ @ _) => simpl. @@ -342,6 +354,386 @@ End cfold. Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _). +Definition Cfold1 t1 t2 (E : Exp1 t1 t2) : Exp1 t1 t2 := fun _ x => cfold (E _ x). + +Lemma fold_Cfold : forall t (E : Exp t), + (fun _ => cfold (E _)) = Cfold E. + reflexivity. +Qed. + +Hint Rewrite fold_Cfold : fold. + +Lemma fold_Cfold1 : forall t1 t2 (E : Exp1 t1 t2), + (fun _ x => cfold (E _ x)) = Cfold1 E. + reflexivity. +Qed. + +Lemma fold_Subst_Cfold1 : forall t1 t2 (E : Exp1 t1 t2) (V : Exp t1), + (fun _ => flatten (cfold (E _ (V _)))) + = Subst V (Cfold1 E). + reflexivity. +Qed. + +Axiom cheat : forall T, T. + + +Lemma fold_Const : forall n, (fun _ => Const' n) = Const n. + reflexivity. +Qed. +Lemma fold_Plus : forall (E1 E2 : Exp _), (fun _ => Plus' (E1 _) (E2 _)) = Plus E1 E2. + reflexivity. +Qed. +Lemma fold_App : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom), + (fun _ => App' (F _) (X _)) = App F X. + reflexivity. +Qed. +Lemma fold_Abs : forall dom ran (B : Exp1 dom ran), + (fun _ => Abs' (B _)) = Abs B. + reflexivity. +Qed. + +Hint Rewrite fold_Const fold_Plus fold_App fold_Abs : fold. + +Lemma fold_Subst : forall t1 t2 (E1 : Exp1 t1 t2) (V : Exp t1), + (fun _ => flatten (E1 _ (V _))) = Subst V E1. + reflexivity. +Qed. + +Hint Rewrite fold_Subst : fold. + +Definition ExpN (G : list type) (t : type) := forall var, hlist var G -> exp var t. + +Definition ConstN G (n : nat) : ExpN G Nat := + fun _ _ => Const' n. +Definition VarN G t (m : member t G) : ExpN G t := fun _ s => Var (hget s m). +Definition PlusN G (E1 E2 : ExpN G Nat) : ExpN G Nat := + fun _ s => Plus' (E1 _ s) (E2 _ s). +Definition AppN G dom ran (F : ExpN G (dom --> ran)) (X : ExpN G dom) : ExpN G ran := + fun _ s => App' (F _ s) (X _ s). +Definition AbsN G dom ran (B : ExpN (dom :: G) ran) : ExpN G (dom --> ran) := + fun _ s => Abs' (fun x => B _ (x ::: s)). + +Inductive ClosedN : forall G t, ExpN G t -> Prop := +| CConstN : forall G b, + ClosedN (ConstN G b) +| CPlusN : forall G (E1 E2 : ExpN G _), + ClosedN E1 + -> ClosedN E2 + -> ClosedN (PlusN E1 E2) +| CAppN : forall G dom ran (E1 : ExpN G (dom --> ran)) E2, + ClosedN E1 + -> ClosedN E2 + -> ClosedN (AppN E1 E2) +| CAbsN : forall G dom ran (E1 : ExpN (dom :: G) ran), + ClosedN E1 + -> ClosedN (AbsN E1). + +Axiom closedN : forall G t (E : ExpN G t), ClosedN E. + +Hint Resolve closedN. + +Section Closed1. + Variable xt : type. + + Definition Const1 (n : nat) : Exp1 xt Nat := + fun _ _ => Const' n. + Definition Var1 : Exp1 xt xt := fun _ x => Var x. + Definition Plus1 (E1 E2 : Exp1 xt Nat) : Exp1 xt Nat := + fun _ s => Plus' (E1 _ s) (E2 _ s). + Definition App1 dom ran (F : Exp1 xt (dom --> ran)) (X : Exp1 xt dom) : Exp1 xt ran := + fun _ s => App' (F _ s) (X _ s). + Definition Abs1 dom ran (B : forall var, var dom -> Exp1 xt ran) : Exp1 xt (dom --> ran) := + fun _ s => Abs' (fun x => B _ x _ s). + + Inductive Closed1 : forall t, Exp1 xt t -> Prop := + | CConst1 : forall b, + Closed1 (Const1 b) + | CPlus1 : forall E1 E2, + Closed1 E1 + -> Closed1 E2 + -> Closed1 (Plus1 E1 E2) + | CApp1 : forall dom ran (E1 : Exp1 _ (dom --> ran)) E2, + Closed1 E1 + -> Closed1 E2 + -> Closed1 (App1 E1 E2) + | CAbs1 : forall dom ran (E1 : forall var, var dom -> Exp1 _ ran), + Closed1 (Abs1 E1). + + Axiom closed1 : forall t (E : Exp1 xt t), Closed1 E. +End Closed1. + +Hint Resolve closed1. + +Definition CfoldN G t (E : ExpN G t) : ExpN G t := fun _ s => cfold (E _ s). + +Theorem fold_CfoldN : forall G t (E : ExpN G t), + (fun _ s => cfold (E _ s)) = CfoldN E. + reflexivity. +Qed. + +Definition SubstN t1 G t2 (E1 : ExpN G t1) (E2 : ExpN (G ++ t1 :: nil) t2) : ExpN G t2 := + fun _ s => flatten (E2 _ (hmap (@Var _) s +++ E1 _ s ::: hnil)). + +Lemma fold_SubstN : forall t1 G t2 (E1 : ExpN G t1) (E2 : ExpN (G ++ t1 :: nil) t2), + (fun _ s => flatten (E2 _ (hmap (@Var _) s +++ E1 _ s ::: hnil))) = SubstN E1 E2. + reflexivity. +Qed. + +Hint Rewrite fold_CfoldN fold_SubstN : fold. + +Ltac ssimp := unfold Subst, Cfold, CfoldN, SubstN in *; simpl in *; autorewrite with fold in *; + repeat match goal with + | [ xt : type |- _ ] => + rewrite (@fold_Subst xt) in * + end; + autorewrite with fold in *. + +Ltac uiper := + repeat match goal with + | [ H : _ = _ |- _ ] => + generalize H; subst; intro H; rewrite (UIP_refl _ _ H) + end. + +Section eq_arg. + Variable A : Type. + Variable B : A -> Type. + + Variable x : A. + + Variables f g : forall x, B x. + Hypothesis Heq : f = g. + + Theorem eq_arg : f x = g x. + congruence. + Qed. +End eq_arg. + +Implicit Arguments eq_arg [A B f g]. + +(*Lemma Cfold_Subst_comm : forall G t (E : ExpN G t), + ClosedN E + -> forall t1 G' (pf : G = G' ++ t1 :: nil) V, + CfoldN (SubstN V (match pf in _ = G return ExpN G _ with refl_equal => E end)) + = SubstN (CfoldN V) (CfoldN (match pf in _ = G return ExpN G _ with refl_equal => E end)). + induction 1; my_crush; uiper; ssimp; crush; + unfold ExpN; do 2 ext_eq. + + generalize (eq_arg x0 (eq_arg x (IHClosedN1 _ _ (refl_equal _) V))). + generalize (eq_arg x0 (eq_arg x (IHClosedN2 _ _ (refl_equal _) V))). + crush. + + match goal with + | [ |- _ = flatten (match ?E with + | Const' _ => _ + | Plus' _ _ => _ + | Var _ _ => _ + | App' _ _ _ _ => _ + | Abs' _ _ _ => _ + end) ] => dep_destruct E + end; crush. + + match goal with + | [ |- _ = flatten (match ?E with + | Const' _ => _ + | Plus' _ _ => _ + | Var _ _ => _ + | App' _ _ _ _ => _ + | Abs' _ _ _ => _ + end) ] => dep_destruct E + end; crush. + + match goal with + | [ |- match ?E with + | Const' _ => _ + | Plus' _ _ => _ + | Var _ _ => _ + | App' _ _ _ _ => _ + | Abs' _ _ _ => _ + end = _ ] => dep_destruct E + end; crush. + rewrite <- H2. + + dep_destruct e. + intro + + + apply cheat. + + unfold ExpN; do 2 ext_eq. + generalize (eq_arg x0 (eq_arg x (IHClosedN1 _ _ (refl_equal _) V))). + generalize (eq_arg x0 (eq_arg x (IHClosedN2 _ _ (refl_equal _) V))). + congruence. + + unfold ExpN; do 2 ext_eq. + f_equal. + ext_eq. + exact (eq_arg (x1 ::: x0) (eq_arg x (IHClosedN _ (dom :: G') (refl_equal _) (fun _ s => V _ (snd s))))). +Qed.*) + +Lemma Cfold_Subst' : forall t (E V' : Exp t), + E ===> V' + -> forall G xt (V : ExpN G xt) B, E = SubstN V B + -> ClosedN B + -> Subst (Cfold V) (Cfold1 B) ===> Cfold V'. + induction 1; inversion 2; my_crush; ssimp. + + auto. + + apply cheat. + + my_crush. + econstructor. + instantiate (1 := Cfold1 B). + unfold Subst, Cfold1 in *; eauto. + unfold Subst, Cfold1 in *; eauto. + unfold Subst, Cfold; eauto. + + my_crush; ssimp. + + + + + Lemma Cfold_Subst' : forall t (B : Exp1 xt t), + Closed1 B + -> forall V', Subst V B ===> V' + -> Subst (Cfold V) (Cfold1 B) ===> Cfold V'. + induction 1; my_crush; ssimp. + + inversion H; my_crush. + + apply cheat. + + inversion H1; my_crush. + econstructor. + instantiate (1 := Cfold1 B). + eauto. + change (Abs (Cfold1 B)) with (Cfold (Abs B)). + auto. + eauto. + eauto. + + apply IHClosed1_1. + eauto. + + match goal with + | [ (*H : ?F = ?G,*) H2 : ?X (fun _ => unit) = ?Y _ _ _ _ (fun _ => unit) |- _ ] => + idtac(*match X with + | Y => fail 1 + | _ => + idtac(*assert (X = Y); [ unfold Exp; apply ext_eq; intro var; + let H' := fresh "H'" in + assert (H' : F var = G var); [ congruence + | match type of H' with + | ?X = ?Y => + let X := eval hnf in X in + let Y := eval hnf in Y in + change (X = Y) in H' + end; injection H'; clear H'; my_crush' ] + | my_crush'; clear H2 ]*) + end*) + end. + + clear H5 H3. + my_crush. + + + unfold Subst in *; simpl in *; autorewrite with fold in *. + + + Check fold_Subst. + + repeat rewrite (@fold_Subst t1) in *. + + simp (Subst (t2 := Nat) V). + + + induction 1; my_crush. +End Exp1. + +Axiom closed1 : forall t1 t2 (E : Exp1 t1 t2), Closed1 E. + + + +Lemma Cfold_Subst' : forall t1 (V : Exp t1) t2 (B : Exp1 t1 t2), + Closed1 B + -> forall V', Subst V B ===> V' + -> Subst (Cfold V) (Cfold1 B) ===> Cfold V'. + induction 1; my_crush. + + unfold Subst in *; simpl in *; autorewrite with fold in *. + inversion H; my_crush. + + unfold Subst in *; simpl in *; autorewrite with fold in *. + Check fold_Subst. + + repeat rewrite (@fold_Subst t1) in *. + + simp (Subst (t2 := Nat) V). + + + induction 1; my_crush. + +Theorem Cfold_Subst : forall t1 t2 (V : Exp t1) B (V' : Exp t2), + Subst V B ===> V' + -> Subst (Cfold V) (Cfold1 B) ===> Cfold V'. + +Theorem Cfold_correct : forall t (E V : Exp t), + E ===> V + -> Cfold E ===> Cfold V. + induction 1; unfold Cfold in *; crush; simp; auto. + + simp. + simp. + apply cheat. + + simp. + econstructor; eauto. + + + + match goal with + | [ |- ?E ===> ?V ] => + try simp1 ltac:(fun E' => change (E' ===> V)); + try match goal with + | [ |- ?E' ===> _ ] => + simp1 ltac:(fun V' => change (E' ===> V')) + end + | [ H : ?E ===> ?V |- _ ] => + try simp1 ltac:(fun E' => change (E' ===> V) in H); + try match type of H with + | ?E' ===> _ => + simp1 ltac:(fun V' => change (E' ===> V') in H) + end + end. + simp. + + let H := IHBigStep1 in + match type of H with + | ?E ===> ?V => + try simp1 ltac:(fun E' => change (E' ===> V) in H); + try match type of H with + | ?E' ===> _ => + simp1 ltac:(fun V' => change (E' ===> V') in H) + end + end. + +try simp1 ltac:(fun E' => change (E' ===> V) in H) + end. + + simp. + + try simp1 ltac:(fun E' => change (fun H : type -> Type => cfold (E1 H)) with E' in IHBigStep1). + try simp1 ltac:(fun V' => change (fun H : type -> Type => + Abs' (dom:=dom) (fun x : H dom => cfold (B H x))) with V' in IHBigStep1). + + simp1 ltac:(fun E => change ((fun H : type -> Type => cfold (E1 H)) ===> E) in IHBigStep1). + + change ((fun H : type -> Type => cfold (E1 H)) ===> Abs (fun _ x => cfold (B _ x))) in IHBigStep1. + (fun H : type -> Type => + Abs' (dom:=dom) (fun x : H dom => cfold (B H x))) + + fold Cfold. + Definition ExpN (G : list type) (t : type) := forall var, hlist var G -> exp var t.