X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=5f3baa38a4abcf62264768b577b20ad45df14b7d;hp=b0c5b11180c4e2775354ec25704507d839f4bc01;hb=b83e779e742413ca84df565263dafbdf9f79920a;hpb=fd337b235014f43000773eb0d95168d89e93a893 diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index b0c5b11..5f3baa3 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 ]. @@ -121,31 +124,83 @@ Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOu reflexivity. Qed. -Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app y x) t. -(* - induction x. - simpl. +Lemma strip_nil_lemma t : stripOutVars nil t = t. + induction t; simpl. + unfold stripOutVars. + destruct a; reflexivity. + rewrite <- IHt1 at 2. + rewrite <- IHt2 at 2. + reflexivity. + Qed. + +Lemma strip_swap0_lemma : forall a a0 y t, + stripOutVars (a :: a0 :: y) t = stripOutVars (a0 :: a :: y) t. + intros. unfold stripOutVars. - simpl. - rewrite mapOptionTree'_compose. induction t. - destruct a; try reflexivity. - simpl. - destruct (dropVar y v); reflexivity. - simpl. - rewrite IHt1. - rewrite IHt2. - reflexivity. - rewrite strip_lemma. - rewrite IHx. - rewrite <- strip_lemma. - rewrite app_comm_cons. - reflexivity. -*) -admit. + destruct a1; simpl; [ idtac | reflexivity ]. + destruct (eqd_dec v a); subst. + destruct (eqd_dec a a0); subst. + reflexivity. + reflexivity. + destruct (eqd_dec v a0); subst. + reflexivity. + reflexivity. + simpl in *. + rewrite IHt1. + rewrite IHt2. + reflexivity. + Qed. + +Lemma strip_swap1_lemma : forall a y t, + stripOutVars (a :: nil) (stripOutVars y t) = + stripOutVars y (stripOutVars (a :: nil) t). + intros. + induction y. + rewrite strip_nil_lemma. + rewrite strip_nil_lemma. + reflexivity. + rewrite (strip_lemma a0 y (stripOutVars (a::nil) t)). + rewrite <- IHy. + clear IHy. + rewrite <- (strip_lemma a y t). + rewrite <- strip_lemma. + rewrite <- strip_lemma. + apply strip_swap0_lemma. + Qed. + +Lemma strip_swap_lemma : forall x y t, stripOutVars x (stripOutVars y t) = stripOutVars y (stripOutVars x t). + intros; induction t. + destruct a; simpl. + + induction x. + rewrite strip_nil_lemma. + rewrite strip_nil_lemma. + reflexivity. + rewrite strip_lemma. + rewrite (strip_lemma a x [v]). + rewrite IHx. + clear IHx. + apply strip_swap1_lemma. + reflexivity. + unfold stripOutVars in *. + simpl. + rewrite IHt1. + rewrite IHt2. + reflexivity. Qed. -Lemma strip_distinct a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y. +Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app x y) t. + induction x; simpl. + apply strip_nil_lemma. + rewrite strip_lemma. + rewrite IHx. + clear IHx. + rewrite <- strip_lemma. + reflexivity. + Qed. + +Lemma notin_strip_inert a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y. intros. induction y. destruct a0; try reflexivity. @@ -232,7 +287,7 @@ Lemma distinct3 {T}(a b c:list T) : distinct (app (app a b) c) -> distinct (app auto. Qed. -Lemma strip_distinct' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y. +Lemma notin_strip_inert' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y. induction x; intros. simpl in H. unfold stripOutVars. @@ -250,7 +305,7 @@ Lemma strip_distinct' y : forall x, distinct (app x (leaves y)) -> stripOutVars set (IHx H3) as qq. rewrite strip_lemma. rewrite IHx. - apply strip_distinct. + apply notin_strip_inert. unfold not; intros. apply H2. apply In_both'. @@ -258,55 +313,221 @@ Lemma strip_distinct' y : forall x, distinct (app x (leaves y)) -> stripOutVars auto. Qed. +Lemma dropvar_lemma v v' y : dropVar y v = Some v' -> v=v'. + intros. + induction y; auto. + simpl in H. + inversion H. + auto. + apply IHy. + simpl in H. + destruct (eqd_dec v a). + inversion H. + auto. + Qed. + Lemma updating_stripped_tree_is_inert' {Γ} lev (ξ:VV -> LeveledHaskType Γ ★) lv tree2 : mapOptionTree (update_ξ ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2) = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2). + induction tree2. - destruct a. - simpl. - induction lv. - reflexivity. - simpl. - destruct a. - simpl. - set (eqd_dec v v0) as q. - destruct q. - auto. - set (dropVar (map (@fst _ _) lv) v) as b in *. - destruct b. - inversion IHlv. - admit. - auto. - reflexivity. + destruct a; [ idtac | reflexivity ]; simpl. + induction lv; [ reflexivity | idtac ]; simpl. + destruct a; simpl. + set (eqd_dec v v0) as q; destruct q; auto. + set (dropVar (map (@fst _ _) lv) v) as b in *. + assert (dropVar (map (@fst _ _) lv) v=b). reflexivity. + destruct b; [ idtac | reflexivity ]. + apply dropvar_lemma in H. + subst. + inversion IHlv. + rewrite H0. + clear H0 IHlv. + destruct (eqd_dec v0 v1). + subst. + assert False. apply n. intros; auto. inversion H. + reflexivity. + unfold stripOutVars in *. + simpl. + rewrite <- IHtree2_1. + rewrite <- IHtree2_2. + reflexivity. + Qed. + +Lemma distinct_bogus : forall {T}a0 (a:list T), distinct (a0::(app a (a0::nil))) -> False. + intros; induction a; auto. + simpl in H. + inversion H; subst. + apply H2; auto. + unfold In; simpl. + left; auto. + apply IHa. + clear IHa. + rewrite <- app_comm_cons in H. + inversion H; subst. + inversion H3; subst. + apply distinct_cons; auto. + intros. + apply H2. simpl. - unfold stripOutVars in *. - rewrite <- IHtree2_1. - rewrite <- IHtree2_2. - reflexivity. + right; auto. Qed. -Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)), - distinct (map (@fst _ _) (leaves varstypes)) -> - mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = - mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes). - admit. +Lemma distinct_swap' : forall {T}a (b:list T), distinct (app b (a::nil)) -> distinct (a::b). + intros. + apply distinct_cons. + induction b; intros; simpl; auto. + rewrite <- app_comm_cons in H. + inversion H; subst. + set (IHb H4) as H4'. + apply H4'. + inversion H0; subst; auto. + apply distinct_bogus in H; inversion H. + induction b; intros; simpl; auto. + apply distinct_nil. + apply distinct_app in H. + destruct H; auto. + Qed. + +Lemma in_both : forall {T}(a b:list T) x, In x (app a b) -> In x a \/ In x b. + induction a; intros; simpl; auto. + rewrite <- app_comm_cons in H. + inversion H. + subst. + left; left; auto. + set (IHa _ _ H0) as H'. + destruct H'. + left; right; auto. + right; auto. + Qed. + +Lemma distinct_lemma : forall {T} (a b:list T) a0, distinct (app a (a0 :: b)) -> distinct (app a b). + intros. + induction a; simpl; auto. + simpl in H. + inversion H; auto. + assert (distinct (app a1 b)) as Q. + intros. + apply IHa. + clear IHa. + rewrite <- app_comm_cons in H. + inversion H; subst; auto. + apply distinct_cons; [ idtac | apply Q ]. + intros. + apply in_both in H0. + destruct H0. + rewrite <- app_comm_cons in H. + inversion H; subst; auto. + apply H3. + apply In_both; auto. + rewrite <- app_comm_cons in H. + inversion H; subst; auto. + apply H3. + apply In_both'; auto. + simpl. + right; auto. Qed. +Lemma nil_app : forall {T}(a:list T) x, x::a = (app (x::nil) a). + induction a; intros; simpl; auto. + Qed. +Lemma distinct_swap : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a). + intros. + induction b. + rewrite <- app_nil_end in H; auto. + rewrite <- app_comm_cons. + set (distinct_lemma _ _ _ H) as H'. + set (IHb H') as H''. + apply distinct_cons; [ idtac | apply H'' ]. + intros. + apply in_both in H0. + clear H'' H'. + destruct H0. + apply distinct_app in H. + destruct H. + inversion H1; auto. + clear IHb. + rewrite nil_app in H. + rewrite ass_app in H. + apply distinct_app in H. + destruct H; auto. + apply distinct_swap' in H. + inversion H; auto. + Qed. +Lemma update_ξ_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 (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes). + induction varstypes; intros. + destruct a; simpl; [ idtac | reflexivity ]. + destruct p. + simpl. + simpl in H. + induction (leaves v1). + simpl; auto. + destruct (eqd_dec v v); auto. + assert False. apply n. auto. inversion H0. + simpl. + destruct a. + destruct (eqd_dec v0 v); subst; auto. + simpl in H. + rewrite map_app in H. + simpl in H. + rewrite nil_app in H. + apply distinct_swap in H. + rewrite app_ass in H. + apply distinct_app in H. + destruct H. + apply distinct_swap in H0. + simpl in H0. + inversion H0; subst. + assert False. + apply H3. + simpl; left; auto. + inversion H1. + apply IHl. + simpl in H. + inversion H; auto. + set (IHvarstypes1 v1 (varstypes2,,v2)) as i1. + set (IHvarstypes2 (v1,,varstypes1) v2) as i2. + simpl in *. + rewrite <- i1. + rewrite <- i2. + rewrite ass_app. + rewrite ass_app. + rewrite ass_app. + rewrite ass_app. + reflexivity. + clear i1 i2 IHvarstypes1 IHvarstypes2. + repeat rewrite ass_app in *; auto. + clear i1 i2 IHvarstypes1 IHvarstypes2. + repeat rewrite ass_app in *; auto. + Qed. +Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) : + distinct (map (@fst _ _) (leaves varstypes)) -> + mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = + mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes). + set (update_ξ_lemma' Γ ξ lev varstypes [] []) as q. + simpl in q. + rewrite <- app_nil_end in q. + apply q. + Qed. Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV := match exp as E in Expr Γ Δ ξ τ with - | EGlobal Γ Δ ξ _ _ => [] + | EGlobal Γ Δ ξ _ _ _ => [] | EVar Γ Δ ξ ev => [ev] | 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 @@ -315,9 +536,9 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e - | ELetRec Γ Δ ξ l τ vars branches body => + | 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: @@ -363,21 +584,6 @@ Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ | 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_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2) - end. - -Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * HaskType Γ ★):= - match elrb with - | ELR_nil Γ Δ ξ lev => [] - | 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} @@ -395,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 *) @@ -500,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 *) @@ -508,17 +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. -Lemma cheat : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a). - admit. - Qed. - -Definition arrangeContextAndWeaken'' +Definition factorContextRightAndWeaken'' (Γ:TypeEnv)(Δ:CoercionEnv Γ) v (* variable to be pivoted, if found *) (ξ:VV -> LeveledHaskType Γ ★) : forall ctx, @@ -533,7 +905,7 @@ Definition arrangeContextAndWeaken'' simpl in *. fold (mapOptionTree ξ) in *. intros. - apply arrangeContextAndWeaken. + apply factorContextRightAndWeaken. apply Δ. unfold mapOptionTree; simpl in *. @@ -562,11 +934,11 @@ Definition arrangeContextAndWeaken'' eapply RComp. apply qq. clear qq IHv2' IHv2 IHv1. + rewrite strip_swap_lemma. rewrite strip_twice_lemma. - - rewrite (strip_distinct' v1 (leaves v2)). + rewrite (notin_strip_inert' v1 (leaves v2)). apply RCossa. - apply cheat. + apply distinct_swap. auto. Defined. @@ -579,7 +951,7 @@ Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v t reflexivity. Qed. -(* IDEA: use multi-conclusion proofs instead *) +(* TODO: use multi-conclusion proofs instead *) Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type := | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _) | lrsp_leaf : forall v t e , @@ -596,22 +968,21 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches : |- (mapOptionTree (@snd _ _) tree) @@@ lev ]. intro X; induction X; intros; simpl in *. apply nd_rule. - apply REmptyGroup. + apply RVoid. set (ξ v) as q in *. destruct q. simpl in *. apply n. - eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; auto. Defined. Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : - forall branches body, - distinct (leaves (mapOptionTree (@fst _ _) 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 ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]]. + ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches body)) |- [τ @@ lev]]. (* NOTE: how we interpret stuff here affects the order-of-side-effects *) intro branches. @@ -620,8 +991,11 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : intro pf. intro lrsp. - rewrite mapleaves in disti. - set (@update_ξ_lemma _ Γ ξ lev tree disti) as ξlemma. + assert (distinct (leaves (mapOptionTree (@fst _ _) tree))) as disti'. + apply disti. + rewrite mapleaves in disti'. + + set (@update_ξ_lemma _ Γ ξ lev tree disti') as ξlemma. rewrite <- mapOptionTree_compose in ξlemma. set ((update_ξ ξ lev (leaves tree))) as ξ' in *. @@ -632,10 +1006,9 @@ 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. - rewrite <- mapleaves in disti. set (q' disti) as q''. unfold ξ' in *. @@ -654,8 +1027,8 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : simpl. set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q. - eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod; auto. rewrite ξlemma. apply q. @@ -729,7 +1102,7 @@ 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 _ + | EGlobal Γ Δ ξ g v lev => 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 @@ -737,7 +1110,7 @@ Definition expr2proof : | 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 (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody) - | ELetRec Γ Δ ξ lev t tree branches ebody => + | ELetRec Γ Δ ξ lev t tree disti branches ebody => let ξ' := update_ξ ξ lev (leaves tree) in let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody) ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★)) @@ -783,8 +1156,7 @@ Definition expr2proof : destruct case_EGlobal. apply nd_rule. simpl. - destruct t as [t lev]. - apply (RGlobal _ _ _ _ wev). + apply (RGlobal _ _ _ g). destruct case_EVar. apply nd_rule. @@ -798,17 +1170,17 @@ 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 (factorContextRightAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx. eapply RArrange in pfx. unfold mapOptionTree in pfx; simpl in pfx. unfold ξ' in pfx. @@ -825,15 +1197,14 @@ Definition expr2proof : destruct case_ELet; intros; simpl in *. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod; [ idtac | apply pf_let]. - clear pf_let. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. + apply nd_prod. + apply pf_let. eapply nd_comp; [ apply pf_body | idtac ]. - clear pf_body. fold (@mapOptionTree VV). fold (mapOptionTree ξ). set (update_ξ ξ v ((lev,tv)::nil)) as ξ'. - set (arrangeContextAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n. + 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. @@ -902,7 +1273,7 @@ Definition expr2proof : rewrite <- (scbwv_coherent scbx l ξ). rewrite <- vec2list_map_list2vec. rewrite mapleaves'. - set (@arrangeContextAndWeaken'') as q. + set (@factorContextRightAndWeaken'') as q. unfold scbwv_ξ. set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z. unfold scbwv_varstypes in z. @@ -910,6 +1281,7 @@ Definition expr2proof : 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. @@ -943,7 +1315,6 @@ Definition expr2proof : unfold ξ'1 in *. clear ξ'1. apply letRecSubproofsToND'. - admit. apply e'. apply subproofs.