X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=0ad9214c79e4c799bd01b03d2c1501e6d020c086;hp=8cd5688ac1950940bbf361936870f3dfafdc3a15;hb=a45824c7d03fcf797e22d2919187a7e97fb567cc;hpb=e4fcbccb71fc54544e9acc62e95d1d15ec86294b diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 8cd5688..0ad9214 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -19,6 +19,9 @@ Section HaskStrongToProof. Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) := RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _). +Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) := + RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _). + Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b). eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ]. eapply RComp; [ idtac | apply RCossa ]. @@ -327,7 +330,7 @@ Lemma updating_stripped_tree_is_inert' {Γ} lev (ξ:VV -> LeveledHaskType Γ ★) lv tree2 : - mapOptionTree (update_ξ ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2) + mapOptionTree (update_xi ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2) = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2). induction tree2. @@ -456,10 +459,10 @@ Lemma distinct_swap : forall {T}(a b:list T), distinct (app a b) -> distinct (ap inversion H; auto. Qed. -Lemma update_ξ_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) : +Lemma update_xiv_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) : forall v1 v2, distinct (map (@fst _ _) (leaves (v1,,(varstypes,,v2)))) -> - mapOptionTree (update_ξ ξ lev (leaves (v1,,(varstypes,,v2)))) (mapOptionTree (@fst _ _) varstypes) = + mapOptionTree (update_xi ξ lev (leaves (v1,,(varstypes,,v2)))) (mapOptionTree (@fst _ _) varstypes) = mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes). induction varstypes; intros. destruct a; simpl; [ idtac | reflexivity ]. @@ -507,11 +510,11 @@ Lemma update_ξ_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstyp repeat rewrite ass_app in *; auto. Qed. -Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) : +Lemma update_xiv_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) : distinct (map (@fst _ _) (leaves varstypes)) -> - mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = + mapOptionTree (update_xi ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes). - set (update_ξ_lemma' Γ ξ lev varstypes [] []) as q. + set (update_xiv_lemma' Γ ξ lev varstypes [] []) as q. simpl in q. rewrite <- app_nil_end in q. apply q. @@ -524,7 +527,7 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? | ELit Γ Δ ξ lit lev => [] | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2) | ELam Γ Δ ξ t1 t2 lev v e => stripOutVars (v::nil) (expr2antecedent e) - | ELet Γ Δ ξ tv t lev v ev ebody => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev)) + | ELet Γ Δ ξ tv t lev v ev ebody => (expr2antecedent ev),,((stripOutVars (v::nil) (expr2antecedent ebody))) | EEsc Γ Δ ξ ec t lev e => expr2antecedent e | EBrak Γ Δ ξ ec t lev e => expr2antecedent e | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e @@ -535,14 +538,14 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e | ELetRec Γ Δ ξ l τ vars _ branches body => let branch_context := eLetRecContext branches - in let all_contexts := (expr2antecedent body),,branch_context + in let all_contexts := branch_context,,(expr2antecedent body) in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts | ECase Γ Δ ξ l tc tbranches atypes e' alts => ((fix varsfromalts (alts: Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac - & Expr (sac_Γ sac Γ) - (sac_Δ sac Γ atypes (weakCK'' Δ)) - (scbwv_ξ scb ξ l) + & Expr (sac_gamma sac Γ) + (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) (weakLT' (tbranches@@l)) } } ): Tree ??VV := match alts with @@ -560,9 +563,9 @@ end. Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes} (alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac - & Expr (sac_Γ sac Γ) - (sac_Δ sac Γ atypes (weakCK'' Δ)) - (scbwv_ξ scb ξ l) + & Expr (sac_gamma sac Γ) + (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) (weakLT' (tbranches@@l)) } }) : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }. destruct alt. @@ -598,7 +601,112 @@ Lemma stripping_nothing_is_inert reflexivity. Qed. -Definition arrangeContext +Definition factorContextLeft + (Γ:TypeEnv)(Δ:CoercionEnv Γ) + v (* variable to be pivoted, if found *) + ctx (* initial context *) + (ξ:VV -> LeveledHaskType Γ ★) + : + + (* a proof concluding in a context where that variable does not appear *) + sum (Arrange + (mapOptionTree ξ ctx ) + (mapOptionTree ξ ([],,(stripOutVars (v::nil) ctx)) )) + + (* or a proof concluding in a context where that variable appears exactly once in the left branch *) + (Arrange + (mapOptionTree ξ ctx ) + (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx)) )). + + induction ctx. + + 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); subst. + + (* where the leaf is v *) + apply inr. + subst. + apply RuCanR. + + (* where the leaf is NOT v *) + apply inl. + apply RuCanL. + + (* empty leaf *) + destruct case_None. + apply inl; simpl in *. + apply RuCanR. + + (* branch *) + refine ( + match IHctx1 with + | inr lpf => + match IHctx2 with + | inr rpf => let case_Both := tt in _ + | inl rpf => let case_Left := tt in _ + end + | inl lpf => + match IHctx2 with + | inr rpf => let case_Right := tt in _ + | inl rpf => let case_Neither := tt in _ + end + end); clear IHctx1; clear IHctx2. + + destruct case_Neither. + apply inl. + simpl. + eapply RComp; [idtac | apply RuCanL ]. + exact (RComp + (* order will not matter because these are central as morphisms *) + (RRight _ (RComp lpf (RCanL _))) + (RLeft _ (RComp rpf (RCanL _)))). + + destruct case_Right. + apply inr. + unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. + fold (stripOutVars (v::nil)). + eapply RComp; [ idtac | eapply pivotContext' ]. + eapply RComp. + eapply RRight. + eapply RComp. + apply lpf. + apply RCanL. + eapply RLeft. + apply rpf. + + destruct case_Left. + apply inr. + fold (stripOutVars (v::nil)). + simpl. + eapply RComp. + eapply RLeft. + eapply RComp. + apply rpf. + simpl. + eapply RCanL. + eapply RComp; [ idtac | eapply RCossa ]. + eapply RRight. + apply lpf. + + destruct case_Both. + apply inr. + simpl. + eapply RComp; [ idtac | eapply RRight; eapply RCont ]. + eapply RComp; [ eapply RRight; eapply lpf | idtac ]. + eapply RComp; [ eapply RLeft; eapply rpf | idtac ]. + clear lpf rpf. + simpl. + apply arrangeSwapMiddle. + Defined. + +Definition factorContextRight (Γ:TypeEnv)(Δ:CoercionEnv Γ) v (* variable to be pivoted, if found *) ctx (* initial context *) @@ -703,7 +811,72 @@ Definition arrangeContext Defined. (* same as before, but use RWeak if necessary *) -Definition arrangeContextAndWeaken +Definition factorContextLeftAndWeaken + (Γ:TypeEnv)(Δ:CoercionEnv Γ) + v (* variable to be pivoted, if found *) + ctx (* initial context *) + (ξ:VV -> LeveledHaskType Γ ★) : + Arrange + (mapOptionTree ξ ctx ) + (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx)) ). + set (factorContextLeft Γ Δ v ctx ξ) as q. + destruct q; auto. + eapply RComp; [ apply a | idtac ]. + refine (RRight _ (RWeak _)). + Defined. + +Definition factorContextLeftAndWeaken'' + (Γ:TypeEnv)(Δ:CoercionEnv Γ) + v (* variable to be pivoted, if found *) + (ξ:VV -> LeveledHaskType Γ ★) : forall ctx, + distinct (leaves v) -> + Arrange + ((mapOptionTree ξ ctx) ) + ((mapOptionTree ξ v),,(mapOptionTree ξ (stripOutVars (leaves v) ctx))). + + induction v; intros. + destruct a. + unfold mapOptionTree in *. + simpl in *. + fold (mapOptionTree ξ) in *. + intros. + set (@factorContextLeftAndWeaken) as q. + simpl in q. + apply q. + apply Δ. + + unfold mapOptionTree; simpl in *. + intros. + rewrite (@stripping_nothing_is_inert Γ); auto. + apply RuCanL. + intros. + unfold mapOptionTree in *. + simpl in *. + fold (mapOptionTree ξ) in *. + set (mapOptionTree ξ) as X in *. + + set (distinct_app _ _ _ H) as H'. + destruct H' as [H1 H2]. + + set (IHv1 (v2,,(stripOutVars (leaves v2) ctx))) as IHv1'. + + unfold X in *. + simpl in *. + rewrite <- strip_twice_lemma. + set (notin_strip_inert' v2 (leaves v1)) as q. + unfold stripOutVars in q. + rewrite q in IHv1'. + clear q. + eapply RComp; [ idtac | eapply RAssoc ]. + eapply RComp; [ idtac | eapply IHv1' ]. + clear IHv1'. + apply IHv2; auto. + auto. + auto. + Defined. + +(* same as before, but use RWeak if necessary *) +Definition factorContextRightAndWeaken (Γ:TypeEnv)(Δ:CoercionEnv Γ) v (* variable to be pivoted, if found *) ctx (* initial context *) @@ -711,13 +884,13 @@ Definition arrangeContextAndWeaken Arrange (mapOptionTree ξ ctx ) (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) ). - set (arrangeContext Γ Δ v ctx ξ) as q. + set (factorContextRight Γ Δ v ctx ξ) as q. destruct q; auto. eapply RComp; [ apply a | idtac ]. refine (RLeft _ (RWeak _)). Defined. -Definition arrangeContextAndWeaken'' +Definition factorContextRightAndWeaken'' (Γ:TypeEnv)(Δ:CoercionEnv Γ) v (* variable to be pivoted, if found *) (ξ:VV -> LeveledHaskType Γ ★) : forall ctx, @@ -732,7 +905,7 @@ Definition arrangeContextAndWeaken'' simpl in *. fold (mapOptionTree ξ) in *. intros. - apply arrangeContextAndWeaken. + apply factorContextRightAndWeaken. apply Δ. unfold mapOptionTree; simpl in *. @@ -770,7 +943,7 @@ Definition arrangeContextAndWeaken'' Defined. Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev : - mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree) + mapOptionTree (update_xi ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree) = mapOptionTree ξ (stripOutVars (v :: nil) tree). set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p. rewrite p. @@ -807,8 +980,8 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches : Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))), - ND Rule [] [Γ > Δ > mapOptionTree (update_ξ ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] -> - LetRecSubproofs Γ Δ (update_ξ ξ lev (leaves tree)) lev tree branches -> + ND Rule [] [Γ > Δ > mapOptionTree (update_xi ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] -> + LetRecSubproofs Γ Δ (update_xi ξ lev (leaves tree)) lev tree branches -> ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches body)) |- [τ @@ lev]]. (* NOTE: how we interpret stuff here affects the order-of-side-effects *) @@ -822,10 +995,10 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : apply disti. rewrite mapleaves in disti'. - set (@update_ξ_lemma _ Γ ξ lev tree disti') as ξlemma. + set (@update_xiv_lemma _ Γ ξ lev tree disti') as ξlemma. rewrite <- mapOptionTree_compose in ξlemma. - set ((update_ξ ξ lev (leaves tree))) as ξ' in *. + set ((update_xi ξ 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. @@ -833,7 +1006,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : eapply nd_comp; [ idtac | eapply nd_rule; apply z ]. clear z. - set (@arrangeContextAndWeaken'' Γ Δ pctx ξ' (expr2antecedent body,,eLetRecContext branches)) as q'. + set (@factorContextRightAndWeaken'' Γ Δ pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'. unfold passback in *; clear passback. unfold pctx in *; clear pctx. set (q' disti) as q''. @@ -855,7 +1028,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q. eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod; auto. rewrite ξlemma. apply q. @@ -864,12 +1037,12 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} : forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac, forall l ξ, - vec2list (vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb)) = + vec2list (vec_map (scbwv_xi scb ξ l) (scbwv_exprvars scb)) = vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)). intros. - unfold scbwv_ξ. + unfold scbwv_xi. unfold scbwv_varstypes. - set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l) + set (@update_xiv_lemma _ _ (weakLT' ○ ξ) (weakL' l) (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes)))) ) as q. rewrite <- mapleaves' in q. @@ -895,8 +1068,8 @@ Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e (alts':Tree ??{sac : StrongAltCon & {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac & - Expr (sac_Γ sac Γ) (sac_Δ sac Γ atypes (weakCK'' Δ)) - (scbwv_ξ scb ξ l) (weakLT' (tbranches @@ l))}}), + Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) (weakLT' (tbranches @@ l))}}), (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) (mapOptionTree mkProofCaseBranch alts')) @@ -938,7 +1111,7 @@ Definition expr2proof : | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody) | ELetRec Γ Δ ξ lev t tree disti branches ebody => - let ξ' := update_ξ ξ lev (leaves tree) in + let ξ' := update_xi ξ 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') @@ -961,9 +1134,9 @@ Definition expr2proof : let dcsp := ((fix mkdcsp (alts: Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac - & Expr (sac_Γ sac Γ) - (sac_Δ sac Γ atypes (weakCK'' Δ)) - (scbwv_ξ scb ξ l) + & Expr (sac_gamma sac Γ) + (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) (weakLT' (tbranches@@l)) } }) : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) := match alts as ALTS return ND Rule [] @@ -997,22 +1170,22 @@ Definition expr2proof : destruct case_EApp. unfold mapOptionTree; simpl; fold (mapOptionTree ξ). - eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ]. + eapply nd_comp; [ idtac + | eapply nd_rule; + apply (@RApp _ _ _ _ t2 t1) ]. 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_ξ ξ lev ((v,t1)::nil)) as ξ'. - set (arrangeContextAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx. + set (update_xi ξ lev ((v,t1)::nil)) as ξ'. + set (factorContextRightAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx. eapply RArrange in pfx. unfold mapOptionTree in pfx; simpl in pfx. unfold ξ' in pfx. rewrite updating_stripped_tree_is_inert in pfx. - unfold update_ξ in pfx. + unfold update_xi in pfx. destruct (eqd_dec v v). eapply nd_comp; [ idtac | apply (nd_rule pfx) ]. clear pfx. @@ -1024,23 +1197,21 @@ Definition expr2proof : destruct case_ELet; intros; simpl in *. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. - apply pf_let. - clear pf_let. - eapply nd_comp; [ apply pf_body | idtac ]. - clear pf_body. + apply pf_let. + eapply nd_comp; [ apply pf_body | idtac ]. fold (@mapOptionTree VV). fold (mapOptionTree ξ). - set (update_ξ ξ v ((lev,tv)::nil)) as ξ'. - set (arrangeContextAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n. + set (update_xi ξ v ((lev,tv)::nil)) as ξ'. + set (factorContextLeftAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n. unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n. unfold ξ' in n. rewrite updating_stripped_tree_is_inert in n. - unfold update_ξ in n. + unfold update_xi in n. destruct (eqd_dec lev lev). unfold ξ'. - unfold update_ξ. + unfold update_xi. eapply RArrange in n. apply (nd_rule n). assert False. apply n0; auto. inversion H. @@ -1095,25 +1266,26 @@ Definition expr2proof : rewrite mapleaves'. simpl. rewrite <- mapOptionTree_compose. - unfold scbwv_ξ. + unfold scbwv_xi. rewrite <- mapleaves'. rewrite vec2list_map_list2vec. - unfold sac_Γ. + unfold sac_gamma. rewrite <- (scbwv_coherent scbx l ξ). rewrite <- vec2list_map_list2vec. rewrite mapleaves'. - set (@arrangeContextAndWeaken'') as q. - unfold scbwv_ξ. + set (@factorContextRightAndWeaken'') as q. + unfold scbwv_xi. set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z. unfold scbwv_varstypes in z. rewrite vec2list_map_list2vec in z. rewrite fst_zip in z. rewrite <- z. clear z. + replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))). apply q. - apply (sac_Δ sac Γ atypes (weakCK'' Δ)). + apply (sac_delta sac Γ atypes (weakCK'' Δ)). rewrite leaves_unleaves. apply (scbwv_exprvars_distinct scbx). rewrite leaves_unleaves.