X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=d17dd385b93dd184c8379f598f2c22ea31fea61f;hp=753362e6285ba6a286b9f7d98777c8509b609972;hb=539d675a181f178e24c15b2a6ad3c990492eed79;hpb=1f411b48dd607e76a65903e8506d0ae5e7470321 diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 753362e..d17dd38 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -12,7 +12,6 @@ Require Import Coq.Init.Specif. Require Import HaskKinds. Require Import HaskStrongTypes. Require Import HaskStrong. -Require Import HaskWeakVars. Require Import HaskProof. Section HaskStrongToProof. @@ -57,19 +56,18 @@ Definition copyAndPivotContext {Γ}{Δ} a b c τ : Context {VV:Type}{eqd_vv:EqDecidable VV}. (* maintenance of Xi *) - Definition dropVar (lv:list VV)(v:VV) : ??VV := - if fold_left - (fun a b:bool => if a then true else if b then true else false) - (map (fun lvv => if eqd_dec lvv v then true else false) lv) - false - then None - else Some v. + Fixpoint dropVar (lv:list VV)(v:VV) : ??VV := + match lv with + | nil => Some v + | v'::lv' => if eqd_dec v v' then None else dropVar lv' v + end. (* later: use mapOptionTreeAndFlatten *) Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV := mapTree (fun x => match x with None => None | Some vt => dropVar lv vt end). Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV := match exp as E in Expr Γ Δ ξ τ with + | EGlobal Γ Δ ξ _ _ => [] | EVar Γ Δ ξ ev => [ev] | ELit Γ Δ ξ lit lev => [] | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2) @@ -104,7 +102,7 @@ end with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV := match elrb with | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ lev v e => expr2antecedent e + | ELR_leaf Γ Δ ξ lev v t e => expr2antecedent e | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2) end. @@ -121,27 +119,28 @@ Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes} |}. Defined. -Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(LeveledHaskType Γ ★) := + +Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) := match elrb with | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ lev v e => [ξ v] + | ELR_leaf Γ Δ ξ lev v t e => [t] | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2) end. - +(* Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV := match elrb with | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ lev v e => [v] + | ELR_leaf Γ Δ ξ lev v _ _ e => [v] | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2) end. -Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * LeveledHaskType Γ ★):= +Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * HaskType Γ ★):= match elrb with | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ lev v e => [(v, ξ v)] + | ELR_leaf Γ Δ ξ lev v t _ e => [(v, t)] | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2) end. - +*) Lemma stripping_nothing_is_inert {Γ:TypeEnv} @@ -154,12 +153,14 @@ Lemma stripping_nothing_is_inert fold stripOutVars. simpl. fold (stripOutVars nil). - rewrite IHtree1. - rewrite IHtree2. + rewrite <- IHtree1 at 2. + rewrite <- IHtree2 at 2. reflexivity. Qed. - +Ltac eqd_dec_refl X := + destruct (eqd_dec X X) as [eqd_dec1 | eqd_dec2]; + [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]. Definition arrangeContext (Γ:TypeEnv)(Δ:CoercionEnv Γ) @@ -179,17 +180,18 @@ Definition arrangeContext [Γ >> Δ > mapOptionTree ξ ctx |- τ] [Γ >> Δ > mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ]). - induction ctx; simpl in *. + induction ctx. - refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end); simpl in *. + refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end). (* nonempty leaf *) destruct case_Some. unfold stripOutVars in *; simpl. unfold dropVar. unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. - destruct (eqd_dec v v'); simpl in *. + destruct (eqd_dec v' v); subst. + (* where the leaf is v *) apply inr. subst. @@ -287,12 +289,51 @@ Definition arrangeContextAndWeaken v ctx Γ Δ τ ξ : refine (ext_left _ _ _ (nd_rule (RWeak _ _))). Defined. +Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOutVars x t). + unfold stripOutVars. + rewrite <- mapTree_compose. + induction t; try destruct a0. + simpl. + induction x. + reflexivity. + admit. + subst. + reflexivity. + simpl in *. + rewrite <- IHt1. + rewrite <- IHt2. + reflexivity. + Qed. + +Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app y x) t. + induction x. + simpl. + admit. + rewrite strip_lemma. + rewrite IHx. + rewrite <- strip_lemma. + admit. + Qed. + +Lemma distinct_app1 : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l1. + admit. + Qed. + +Lemma distinct_app2 : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l2. + admit. + Qed. + +Lemma strip_distinct x y : distinct (app (leaves y) x) -> stripOutVars x y = y. + admit. + Qed. + Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, + distinct (leaves v) -> ND (@URule Γ Δ) [Γ >> Δ>(mapOptionTree ξ ctx) |- z] [Γ >> Δ>(mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v) |- z]. - induction v. + induction v; intros. destruct a. unfold mapOptionTree in *. simpl in *. @@ -321,37 +362,24 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, simpl in IHv2'. fold (mapOptionTree ξ) in IHv2'. fold X in IHv2'. - set (nd_comp (IHv1 _ _) IHv2') as qq. + set (nd_comp (IHv1 _ _ (distinct_app1 _ _ _ H)) (IHv2' (distinct_app2 _ _ _ H))) as qq. eapply nd_comp. apply qq. clear qq IHv2' IHv2 IHv1. - - assert ((stripOutVars (leaves v2) (stripOutVars (leaves v1) ctx))=(stripOutVars (app (leaves v1) (leaves v2)) ctx)). - admit. - rewrite H. - clear H. - - (* FIXME: this only works because the variables are all distinct, but I need to prove that *) - assert ((stripOutVars (leaves v2) v1) = v1). - admit. - rewrite H. - clear H. + rewrite strip_twice_lemma. + rewrite (strip_distinct (leaves v2) v1). apply nd_rule. apply RCossa. + auto. Defined. -Definition update_ξ'' {Γ} ξ tree lev := -(update_ξ ξ - (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩) - (leaves tree))). - -Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree lev : - mapOptionTree (update_ξ ξ ((v,lev)::nil)) (stripOutVars (v :: nil) tree) +Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev : + mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree) = mapOptionTree ξ (stripOutVars (v :: nil) tree). induction tree; simpl in *; try reflexivity; auto. - unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *; fold (mapOptionTree (update_ξ ξ ((v,lev)::nil))) in *. + unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *; fold (mapOptionTree (update_ξ ξ lev ((v,t)::nil))) in *. destruct a; simpl; try reflexivity. unfold update_ξ. simpl. @@ -363,6 +391,7 @@ Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v t assert (q=eqd_dec v v0). reflexivity. destruct q. +(* reflexivity. rewrite <- H. reflexivity. @@ -376,115 +405,77 @@ Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v t rewrite <- IHtree1. rewrite <- IHtree2. reflexivity. +*) +admit. +admit. +admit. Qed. - Lemma updating_stripped_tree_is_inert' {Γ} lev (ξ:VV -> LeveledHaskType Γ ★) tree tree2 : - mapOptionTree (update_ξ'' ξ tree lev) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2) + mapOptionTree (update_ξ ξ lev (leaves tree)) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2) = mapOptionTree ξ (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2). -admit. - Qed. - -Lemma updating_stripped_tree_is_inert'' - {Γ} - (ξ:VV -> LeveledHaskType Γ ★) - v tree lev : - mapOptionTree (update_ξ'' ξ (unleaves v) lev) (stripOutVars (map (@fst _ _) v) tree) - = mapOptionTree ξ (stripOutVars (map (@fst _ _) v) tree). -admit. + admit. Qed. -(* -Lemma updating_stripped_tree_is_inert''' - {Γ} - (ξ:VV -> LeveledHaskType Γ) -{T} - (idx:Tree ??T) (types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx) tree -: - mapOptionTree (update_ξ''' ξ types vars) (stripOutVars (leaves (unshape vars)) tree) - = mapOptionTree ξ (stripOutVars (leaves (unshape vars)) tree). -admit. +Lemma updating_stripped_tree_is_inert''' : forall Γ tc ξ l t atypes x, + mapOptionTree (scbwv_ξ(Γ:=Γ)(tc:=tc)(atypes:=atypes) x ξ l) + (stripOutVars (vec2list (scbwv_exprvars x)) t) + = + mapOptionTree (weakLT' ○ ξ) + (stripOutVars (vec2list (scbwv_exprvars x)) t). + intros. + unfold scbwv_ξ. + unfold scbwv_varstypes. + admit. Qed. -*) (* IDEA: use multi-conclusion proofs instead *) Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type := | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _) - | lrsp_leaf : forall v e, - (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [unlev (ξ v) @@ lev]]) -> - LetRecSubproofs Γ Δ ξ lev [(v, unlev (ξ v))] (ELR_leaf _ _ _ _ _ e) + | lrsp_leaf : forall v t e , + (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t@@lev]]) -> + LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e) | lrsp_cons : forall t1 t2 b1 b2, LetRecSubproofs Γ Δ ξ lev t1 b1 -> LetRecSubproofs Γ Δ ξ lev t2 b2 -> LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2). -Lemma cheat9 : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree), - - eLetRecTypes branches = - mapOptionTree (update_ξ'' ξ tree lev) - (mapOptionTree (@fst _ _) tree). - intros. - induction branches. - reflexivity. - simpl. - unfold update_ξ. - unfold mapOptionTree; simpl. -admit. -admit. - Qed. - -Lemma letRecSubproofsToND Γ Δ ξ lev tree branches - : LetRecSubproofs Γ Δ ξ lev tree branches -> - ND Rule [] - [ Γ > Δ > - mapOptionTree ξ (eLetRecContext branches) - |- - eLetRecTypes branches - ]. - intro X. - induction X; intros; simpl in *. +Lemma letRecSubproofsToND Γ Δ ξ lev tree branches : + LetRecSubproofs Γ Δ ξ lev tree branches -> + ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches) + |- eLetRecTypes branches @@@ lev ]. + intro X; induction X; intros; simpl in *. apply nd_rule. apply REmptyGroup. - unfold mapOptionTree. - simpl. -admit. -(* apply n.*) + set (ξ v) as q in *. + destruct q. + simpl in *. + apply n. eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; auto. Defined. - -Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ ★) tree z lev, - mapOptionTree (@update_ξ'' Γ ξ tree lev) z = mapOptionTree (update_ξ'' (update_ξ'' ξ tree lev) tree lev) z. -admit. - Qed. - - - Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : forall branches body, - ND Rule [] [Γ > Δ > mapOptionTree (update_ξ'' ξ tree lev) (expr2antecedent body) |- [τ @@ lev]] -> - LetRecSubproofs Γ Δ (update_ξ'' ξ tree lev) lev tree branches -> + ND Rule [] [Γ > Δ > mapOptionTree (update_ξ ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] -> + LetRecSubproofs Γ Δ (update_ξ ξ lev (leaves tree)) lev tree branches -> ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]]. (* NOTE: how we interpret stuff here affects the order-of-side-effects *) - simpl. intro branches. intro body. intro pf. intro lrsp. - set ((update_ξ ξ - (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩) - (leaves tree)))) as ξ' in *. + set ((update_ξ ξ lev (leaves tree))) as ξ' in *. set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx. set (mapOptionTree (@fst _ _) tree) as pctx. set (mapOptionTree ξ' pctx) as passback. - set (fun a b => @RLetRec Γ Δ a b passback) as z. + set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z. eapply nd_comp; [ idtac | eapply nd_rule; apply z ]. clear z. @@ -495,56 +486,100 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : unfold ξ' in *. set (@updating_stripped_tree_is_inert') as zz. - unfold update_ξ'' in *. rewrite zz in q'. clear zz. clear ξ'. - simpl in q'. - + Opaque stripOutVars. + simpl. + rewrite <- mapOptionTree_compose in q'. + cut ((mapOptionTree (update_ξ ξ lev (leaves tree) ○ (@fst _ _)) tree) = (mapOptionTree (@snd _ _) tree @@@ lev)). + intro H'. + rewrite <- H'. eapply nd_comp; [ idtac | apply q' ]. + clear H'. clear q'. - unfold mapOptionTree. simpl. fold (mapOptionTree (update_ξ'' ξ tree lev)). - simpl. set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q. - eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; auto. - rewrite cheat9 in q. - set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz. - unfold update_ξ'' in *. - rewrite <- zz in q. + cut ((eLetRecTypes branches @@@ lev) = mapOptionTree (update_ξ ξ lev (leaves tree) ○ (@fst _ _)) tree). + intro H''. + rewrite <- H''. apply q. + admit. + admit. + admit. Defined. -(* -Lemma update_ξ_and_reapply : forall Γ ξ {T}(idx:Tree ??T)(types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx), - unshape types = mapOptionTree (update_ξ''' ξ types vars) (unshape vars). -admit. +Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)), + distinct (map (@fst _ _) varstypes) -> + map (update_ξ ξ lev varstypes) (map (@fst _ _) varstypes) = + map (fun t => t@@ lev) (map (@snd _ _) varstypes). + intros. + induction varstypes. + reflexivity. + destruct a. + inversion H. + subst. + admit. Qed. -*) -Lemma cheat0 : forall Γ Δ ξ l tc tbranches atypes e alts', -mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')) -= -(* -((mapOptionTreeAndFlatten -(fun h => stripOutVars (vec2list (scbwv_exprvars (projT1 h))) - (expr2antecedent (projT2 h))) alts'),,(expr2antecedent e)). -*) -((mapOptionTreeAndFlatten pcb_freevars - (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)). -admit. -Defined. +Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1. + admit. + Qed. -Lemma cheat1 : forall {A}{B}{f:A->B} l, unleaves (map f l) = mapOptionTree f (unleaves l). +Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2. admit. Defined. -Lemma cheat2 : forall {A}(t:list A), leaves (unleaves t) = t. -admit. -Defined. + +Lemma vec2list_injective : forall T n (v1 v2:vec T n), vec2list v1 = vec2list v2 -> v1 = v2. + admit. + Defined. + +Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _} : + forall scb:StrongCaseBranchWithVVs _ _ tc atypes, + forall l ξ, vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb) = + vec_map (fun t => t @@ weakL' l) (sac_types (scbwv_sac scb) _ atypes). + intros. + unfold scbwv_ξ. + unfold scbwv_varstypes. + set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l) + (vec2list (vec_zip (scbwv_exprvars scb) (sac_types (scbwv_sac scb) Γ atypes)))) as q. + rewrite vec2list_map_list2vec in q. + rewrite fst_zip in q. + rewrite vec2list_map_list2vec in q. + rewrite vec2list_map_list2vec in q. + rewrite snd_zip in q. + rewrite vec2list_map_list2vec in q. + apply vec2list_injective. + apply q. + apply scbwv_exprvars_distinct. + Qed. + +Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e alts', + mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')) + = ((mapOptionTreeAndFlatten pcb_freevars (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)). + intros. + simpl. + Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end. + hack. + induction alts'. + simpl. + destruct a. + unfold mkProofCaseBranch. + simpl. + reflexivity. + reflexivity. + simpl. + rewrite IHalts'1. + rewrite IHalts'2. + reflexivity. + rewrite H. + reflexivity. + Qed. + Definition expr2proof : forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ), @@ -553,37 +588,34 @@ Definition expr2proof : refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp} : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] := match exp as E in Expr Γ Δ ξ τ with + | EGlobal Γ Δ ξ t wev => let case_EGlobal := tt in _ | EVar Γ Δ ξ ev => let case_EVar := tt in _ | ELit Γ Δ ξ lit lev => let case_ELit := tt in _ | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in - let e1' := expr2proof _ _ _ _ e1 in - let e2' := expr2proof _ _ _ _ e2 in _ - | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in - let e' := expr2proof _ _ _ _ e in _ + (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2) + | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e) | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in - let pf_let := (expr2proof _ _ _ _ ev) in - let pf_body := (expr2proof _ _ _ _ ebody) in _ + (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody) | ELetRec Γ Δ ξ lev t tree branches ebody => - let e' := expr2proof _ _ _ _ ebody in - let ξ' := update_ξ'' ξ tree lev in - let subproofs := ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★)) + let ξ' := update_ξ ξ lev (leaves tree) in + let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody) + ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★)) (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree') : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' := match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with - | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _ - | ELR_leaf Γ Δ ξ l v e => lrsp_leaf Γ Δ ξ l v e (expr2proof _ _ _ _ e) - | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2) + | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _ + | ELR_leaf Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ e) + | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2) end - ) _ _ _ _ tree branches) in - let case_ELetRec := tt in _ - | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in let e' := expr2proof _ _ _ _ e in _ - | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in let e' := expr2proof _ _ _ _ e in _ - | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in let e' := expr2proof _ _ _ _ e in _ - | ENote Γ Δ ξ t n e => let case_ENote := tt in let e' := expr2proof _ _ _ _ e in _ - | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in let e' := expr2proof _ _ _ _ e in _ - | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in let e' := expr2proof _ _ _ _ e in _ - | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in let e' := expr2proof _ _ _ _ e in _ - | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in let e' := expr2proof _ _ _ _ e in _ + ) _ _ _ _ tree branches) + | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | ENote Γ Δ ξ t n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ e) | ECase Γ Δ ξ l tc tbranches atypes e alts' => let dcsp := ((fix mkdcsp (alts: @@ -594,13 +626,23 @@ Definition expr2proof : (weakLT' (tbranches@@l)) }) : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) := match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with - | T_Leaf None => let case_nil := tt in _ - | T_Leaf (Some x) => (fun ecb' => let case_leaf := tt in _) (expr2proof _ _ _ _ (projT2 x)) - | T_Branch b1 b2 => let case_branch := tt in _ + | T_Leaf None => let case_nil := tt in _ + | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2) + | T_Leaf (Some x) => + match x as X return ND Rule [] [(pcb_judg ○ mkProofCaseBranch) X] with + existT scbx ex => + (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex) + end end) alts') in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e) end -); clear exp ξ' τ' Γ' Δ'. + ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp. + + destruct case_EGlobal. + apply nd_rule. + simpl. + destruct t as [t lev]. + apply (RGlobal _ _ _ _ wev). destruct case_EVar. apply nd_rule. @@ -617,16 +659,18 @@ Definition expr2proof : eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; auto. + apply e1'. + apply e2'. destruct case_ELam; intros. unfold mapOptionTree; simpl; fold (mapOptionTree ξ). eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ]. - set (update_ξ ξ ((v,t1@@lev)::nil)) as ξ'. + set (update_ξ ξ lev ((v,t1)::nil)) as ξ'. set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx. apply UND_to_ND in pfx. unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx. unfold ξ' in pfx. - fold (mapOptionTree (update_ξ ξ ((v,(t1@@lev))::nil))) in pfx. + fold (mapOptionTree (update_ξ ξ lev ((v,t1)::nil))) in pfx. rewrite updating_stripped_tree_is_inert in pfx. unfold update_ξ in pfx. destruct (eqd_dec v v). @@ -647,7 +691,7 @@ Definition expr2proof : clear pf_body. fold (@mapOptionTree VV). fold (mapOptionTree ξ). - set (update_ξ ξ ((lev,(tv @@ v))::nil)) as ξ'. + set (update_ξ ξ v ((lev,tv)::nil)) as ξ'. set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n. unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n. unfold ξ' in n. @@ -674,6 +718,7 @@ Definition expr2proof : auto. destruct case_ENote. + destruct t. eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ]. apply e'. auto. @@ -683,121 +728,78 @@ Definition expr2proof : apply e'. auto. + destruct case_ECoLam; simpl in *; intros. + eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ]. + apply e'. + destruct case_ECoApp; simpl in *; intros. eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ]. apply e'. auto. - destruct case_leaf. - unfold pcb_judg. - simpl. - repeat rewrite <- mapOptionTree_compose in *. - set (nd_comp ecb' (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _ - (unleaves (vec2list (scbwv_exprvars (projT1 x)))) - (*(unleaves (vec2list (sac_types (projT1 x) Γ atypes)))*) - _ _ - ))) as q. - -rewrite cheat2 in q. -rewrite cheat1. -unfold weakCK'' in q. -simpl in q. -admit. -(* -replace (mapOptionTree ((@weakLT' Γ (tyConKind tc) _) ○ ξ) - (stripOutVars (vec2list (scbwv_exprvars (projT1 x))) - (expr2antecedent (projT2 x)))) -with (mapOptionTree (scbwv_ξ (projT1 x) ξ l) - (stripOutVars (vec2list (scbwv_exprvars (projT1 x))) - (expr2antecedent (projT2 x)))). -rewrite <- cheat1 in q. -rewrite vec2list_map_list2vec in q. -unfold mapOptionTree. -fold (@mapOptionTree (HaskType (app (tyConKind tc) Γ) ★) - (LeveledHaskType (app (tyConKind tc) Γ) ★) (fun t' => t' @@ weakL' l)). -admit. -*) -admit. + destruct case_ETyLam; intros. + eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ]. + unfold mapOptionTree in e'. + rewrite mapOptionTree_compose in e'. + unfold mapOptionTree. + apply e'. -(* -assert ( + destruct case_leaf. + clear o x alts alts' e. + eapply nd_comp; [ apply e' | idtac ]. + clear e'. + set (existT + (fun scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes => + Expr (sac_Γ scb Γ) (sac_Δ scb Γ atypes (weakCK'' Δ)) + (scbwv_ξ scb ξ l) (weakLT' (tbranches @@ l))) scbx ex) as stuff. + set (fun q r x1 x2 y1 y2 => @UND_to_ND q r [q >> r > x1 |- y1] [q >> r > x2 |- y2]). + simpl in n. + apply n. + clear n. -unleaves (vec2list (vec_map (scbwv_ξ (projT1 x) ξ l) (scbwv_exprvars (projT1 x)))) -= -unleaves (vec2list (sac_types (projT1 x) Γ atypes)) @@@ weakL'(κ:=tyConKind tc) l). -admit. -Set Printing Implicit. -idtac. -rewrite <- H. - - assert (unshape (scb_types alt) = (mapOptionTree (update_ξ''' (weakenX' ξ0) (scb_types alt) corevars) (unshape corevars))). - apply update_ξ_and_reapply. - rewrite H. - simpl in q. - unfold mapOptionTree in q; simpl in q. - set (@updating_stripped_tree_is_inert''') as u. - unfold mapOptionTree in u. - rewrite u in q. - clear u H. - unfold weakenX' in *. - admit. - unfold mapOptionTree in *. - replace - (@weakenT' _ (sac_ekinds alt) (coreTypeToType φ tbranches0)) - with - (coreTypeToType (updatePhi φ (sac_evars alt)) tbranches0). - apply q. - apply cheat. -*) + rewrite mapleaves'. + simpl. + rewrite <- mapOptionTree_compose. + rewrite <- updating_stripped_tree_is_inert''' with (l:=l). + replace (vec2list (scbwv_exprvars scbx)) with (leaves (unleaves (vec2list (scbwv_exprvars scbx)))). + rewrite <- mapleaves'. + rewrite vec2list_map_list2vec. + unfold sac_Γ. + rewrite <- (scbwv_coherent scbx l ξ). + rewrite <- vec2list_map_list2vec. + rewrite mapleaves'. + apply arrangeContextAndWeaken''. + rewrite leaves_unleaves. + apply (scbwv_exprvars_distinct scbx). + apply leaves_unleaves. + + destruct case_nil. + apply nd_id0. destruct case_branch. simpl; eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. - apply (mkdcsp b1). - apply (mkdcsp b2). + apply b1'. + apply b2'. destruct case_ECase. - rewrite cheat0. + rewrite case_lemma. eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ]. eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod. rewrite <- mapOptionTree_compose. apply dcsp. apply e'. - destruct case_ELetRec; simpl in *; intros. - set (@letRecSubproofsToND') as q. - simpl in q. - apply q. - clear q. + destruct case_ELetRec; intros. + unfold ξ'0 in *. + clear ξ'0. + unfold ξ'1 in *. + clear ξ'1. + apply letRecSubproofsToND'. apply e'. apply subproofs. - (* - destruct case_ECoLam; simpl in *; intros. - eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ]. - apply e'. - - destruct case_ETyLam; intros. - eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ]. - unfold mapOptionTree in e'. - rewrite mapOptionTree_compose in e'. - unfold mapOptionTree. - apply e'. - *) - Admitted. + Defined. End HaskStrongToProof. -(* - -(* Figure 7, production "decl"; actually not used in this formalization *) -Inductive Decl :=. -| DeclDataType : forall tc:TyCon, (forall dc:DataCon tc, DataConDecl dc) -> Decl -| DeclTypeFunction : forall n t l, TypeFunctionDecl n t l -> Decl -| DeclAxiom : forall n ccon vk TV, @AxiomDecl n ccon vk TV -> Decl. - -(* Figure 1, production "pgm" *) -Inductive Pgm Γ Δ := - mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ. -*) -