X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=114f2d9bbd0527432cdf37a8837df3eae2f85db3;hp=5f3baa38a4abcf62264768b577b20ad45df14b7d;hb=3282a2b78028238987a5a49e59d8e8d495aea0e1;hpb=b83e779e742413ca84df565263dafbdf9f79920a diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 5f3baa3..114f2d9 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -6,6 +6,7 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import NaturalDeduction. +Require Import NaturalDeductionContext. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import Coq.Init.Specif. @@ -15,20 +16,7 @@ Require Import HaskStrong. Require Import HaskProof. 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 ]. - eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ]. - apply RAssoc. - Defined. - + Context {VV:Type}{eqd_vv:EqDecidable VV}. (* maintenance of Xi *) @@ -330,7 +318,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. @@ -459,10 +447,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 ]. @@ -510,18 +498,18 @@ 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. Qed. -Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV := - match exp as E in Expr Γ Δ ξ τ with +Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}{l'}(exp:Expr Γ' Δ' ξ' τ' l') : Tree ??VV := + match exp as E in Expr Γ Δ ξ τ l with | EGlobal Γ Δ ξ _ _ _ => [] | EVar Γ Δ ξ ev => [ev] | ELit Γ Δ ξ lit lev => [] @@ -531,7 +519,7 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? | EEsc Γ Δ ξ ec t lev e => expr2antecedent e | EBrak Γ Δ ξ ec t lev e => expr2antecedent e | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e - | ENote Γ Δ ξ t n e => expr2antecedent e + | ENote Γ Δ ξ t l n e => expr2antecedent e | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e @@ -543,10 +531,10 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? | 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) - (weakLT' (tbranches@@l)) } } + & Expr (sac_gamma sac Γ) + (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) + (weakT' tbranches) (weakL' l)} } ): Tree ??VV := match alts with | T_Leaf None => [] @@ -563,10 +551,10 @@ end. Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes} (alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ 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) + (weakT' tbranches) (weakL' l) } }) : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }. destruct alt. exists x. @@ -633,16 +621,16 @@ Definition factorContextLeft (* where the leaf is v *) apply inr. subst. - apply RuCanR. + apply AuCanR. (* where the leaf is NOT v *) apply inl. - apply RuCanL. + apply AuCanL. (* empty leaf *) destruct case_None. apply inl; simpl in *. - apply RuCanR. + apply AuCanR. (* branch *) refine ( @@ -662,45 +650,45 @@ Definition factorContextLeft destruct case_Neither. apply inl. simpl. - eapply RComp; [idtac | apply RuCanL ]. - exact (RComp + eapply AComp; [idtac | apply AuCanL ]. + exact (AComp (* order will not matter because these are central as morphisms *) - (RRight _ (RComp lpf (RCanL _))) - (RLeft _ (RComp rpf (RCanL _)))). + (ARight _ (AComp lpf (ACanL _))) + (ALeft _ (AComp rpf (ACanL _)))). 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. + eapply AComp; [ idtac | eapply pivotContext' ]. + eapply AComp. + eapply ARight. + eapply AComp. apply lpf. - apply RCanL. - eapply RLeft. + apply ACanL. + eapply ALeft. apply rpf. destruct case_Left. apply inr. fold (stripOutVars (v::nil)). simpl. - eapply RComp. - eapply RLeft. - eapply RComp. + eapply AComp. + eapply ALeft. + eapply AComp. apply rpf. simpl. - eapply RCanL. - eapply RComp; [ idtac | eapply RCossa ]. - eapply RRight. + eapply ACanL. + eapply AComp; [ idtac | eapply AuAssoc ]. + eapply ARight. 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 ]. + eapply AComp; [ idtac | eapply ARight; eapply ACont ]. + eapply AComp; [ eapply ARight; eapply lpf | idtac ]. + eapply AComp; [ eapply ALeft; eapply rpf | idtac ]. clear lpf rpf. simpl. apply arrangeSwapMiddle. @@ -738,16 +726,16 @@ Definition factorContextRight (* where the leaf is v *) apply inr. subst. - apply RuCanL. + apply AuCanL. (* where the leaf is NOT v *) apply inl. - apply RuCanR. + apply AuCanR. (* empty leaf *) destruct case_None. apply inl; simpl in *. - apply RuCanR. + apply AuCanR. (* branch *) refine ( @@ -766,51 +754,51 @@ Definition factorContextRight destruct case_Neither. apply inl. - eapply RComp; [idtac | apply RuCanR ]. - exact (RComp + eapply AComp; [idtac | apply AuCanR ]. + exact (AComp (* order will not matter because these are central as morphisms *) - (RRight _ (RComp lpf (RCanR _))) - (RLeft _ (RComp rpf (RCanR _)))). + (ARight _ (AComp lpf (ACanR _))) + (ALeft _ (AComp rpf (ACanR _)))). destruct case_Right. apply inr. fold (stripOutVars (v::nil)). - set (RRight (mapOptionTree ξ ctx2) (RComp lpf ((RCanR _)))) as q. + set (ARight (mapOptionTree ξ ctx2) (AComp lpf ((ACanR _)))) as q. simpl in *. - eapply RComp. + eapply AComp. apply q. clear q. clear lpf. unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. - eapply RComp; [ idtac | apply RAssoc ]. - apply RLeft. + eapply AComp; [ idtac | apply AAssoc ]. + apply ALeft. apply rpf. destruct case_Left. apply inr. unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. fold (stripOutVars (v::nil)). - eapply RComp; [ idtac | eapply pivotContext ]. - set (RComp rpf (RCanR _ )) as rpf'. - set (RLeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq. + eapply AComp; [ idtac | eapply pivotContext ]. + set (AComp rpf (ACanR _ )) as rpf'. + set (ALeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq. simpl in *. - eapply RComp; [ idtac | apply qq ]. + eapply AComp; [ idtac | apply qq ]. clear qq rpf' rpf. - apply (RRight (mapOptionTree ξ ctx2)). + apply (ARight (mapOptionTree ξ ctx2)). apply lpf. destruct case_Both. apply inr. unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. fold (stripOutVars (v::nil)). - eapply RComp; [ idtac | eapply copyAndPivotContext ]. + eapply AComp; [ idtac | eapply copyAndPivotContext ]. (* order will not matter because these are central as morphisms *) - exact (RComp (RRight _ lpf) (RLeft _ rpf)). + exact (AComp (ARight _ lpf) (ALeft _ rpf)). Defined. -(* same as before, but use RWeak if necessary *) +(* same as before, but use AWeak if necessary *) Definition factorContextLeftAndWeaken (Γ:TypeEnv)(Δ:CoercionEnv Γ) v (* variable to be pivoted, if found *) @@ -821,8 +809,8 @@ Definition factorContextLeftAndWeaken (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx)) ). set (factorContextLeft Γ Δ v ctx ξ) as q. destruct q; auto. - eapply RComp; [ apply a | idtac ]. - refine (RRight _ (RWeak _)). + eapply AComp; [ apply a | idtac ]. + refine (ARight _ (AWeak _)). Defined. Definition factorContextLeftAndWeaken'' @@ -848,7 +836,7 @@ Definition factorContextLeftAndWeaken'' unfold mapOptionTree; simpl in *. intros. rewrite (@stripping_nothing_is_inert Γ); auto. - apply RuCanL. + apply AuCanL. intros. unfold mapOptionTree in *. simpl in *. @@ -867,15 +855,15 @@ Definition factorContextLeftAndWeaken'' unfold stripOutVars in q. rewrite q in IHv1'. clear q. - eapply RComp; [ idtac | eapply RAssoc ]. - eapply RComp; [ idtac | eapply IHv1' ]. + eapply AComp; [ idtac | eapply AAssoc ]. + eapply AComp; [ idtac | eapply IHv1' ]. clear IHv1'. apply IHv2; auto. auto. auto. Defined. -(* same as before, but use RWeak if necessary *) +(* same as before, but use AWeak if necessary *) Definition factorContextRightAndWeaken (Γ:TypeEnv)(Δ:CoercionEnv Γ) v (* variable to be pivoted, if found *) @@ -886,8 +874,8 @@ Definition factorContextRightAndWeaken (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) ). set (factorContextRight Γ Δ v ctx ξ) as q. destruct q; auto. - eapply RComp; [ apply a | idtac ]. - refine (RLeft _ (RWeak _)). + eapply AComp; [ apply a | idtac ]. + refine (ALeft _ (AWeak _)). Defined. Definition factorContextRightAndWeaken'' @@ -911,7 +899,7 @@ Definition factorContextRightAndWeaken'' unfold mapOptionTree; simpl in *. intros. rewrite (@stripping_nothing_is_inert Γ); auto. - apply RuCanR. + apply AuCanR. intros. unfold mapOptionTree in *. simpl in *. @@ -930,20 +918,20 @@ Definition factorContextRightAndWeaken'' fold X in IHv2'. set (distinct_app _ _ _ H) as H'. destruct H' as [H1 H2]. - set (RComp (IHv1 _ H1) (IHv2' H2)) as qq. - eapply RComp. + set (AComp (IHv1 _ H1) (IHv2' H2)) as qq. + eapply AComp. apply qq. clear qq IHv2' IHv2 IHv1. rewrite strip_swap_lemma. rewrite strip_twice_lemma. rewrite (notin_strip_inert' v1 (leaves v2)). - apply RCossa. + apply AuAssoc. apply distinct_swap. auto. 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. @@ -955,7 +943,7 @@ Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v t Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type := | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _) | lrsp_leaf : forall v t e , - (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t@@lev]]) -> + (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 -> @@ -965,7 +953,7 @@ Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ l Lemma letRecSubproofsToND Γ Δ ξ lev tree branches : LetRecSubproofs Γ Δ ξ lev tree branches -> ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches) - |- (mapOptionTree (@snd _ _) tree) @@@ lev ]. + |- (mapOptionTree (@snd _ _) tree) @ lev ]. intro X; induction X; intros; simpl in *. apply nd_rule. apply RVoid. @@ -973,16 +961,19 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches : destruct q. simpl in *. apply n. - eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod; auto. - Defined. + eapply nd_comp; [ idtac | eapply RCut' ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply IHX1. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ]. + apply IHX2. + Defined. 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 ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches body)) |- [τ @@ lev]]. + 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 *) intro branches. @@ -995,10 +986,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. @@ -1006,7 +997,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : eapply nd_comp; [ idtac | eapply nd_rule; apply z ]. clear z. - set (@factorContextRightAndWeaken'' Γ Δ pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'. + set (@factorContextLeftAndWeaken'' Γ Δ pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'. unfold passback in *; clear passback. unfold pctx in *; clear pctx. set (q' disti) as q''. @@ -1021,28 +1012,30 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : simpl. rewrite <- mapOptionTree_compose in q''. rewrite <- ξlemma. - eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ q'') ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ _ q'') ]. clear q'. clear q''. simpl. set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q. - eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. - eapply nd_comp; [ apply nd_rlecnac | idtac ]. - apply nd_prod; auto. - rewrite ξlemma. - apply q. - Defined. + + eapply nd_comp; [ idtac | eapply RCut' ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ]. + apply pf. + Defined. 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. @@ -1068,8 +1061,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) (weakT' tbranches) (weakL' l)}}), (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) (mapOptionTree mkProofCaseBranch alts')) @@ -1096,48 +1089,48 @@ Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e Qed. Definition expr2proof : - forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ), - ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]]. + forall Γ Δ ξ τ l (e:Expr Γ Δ ξ τ l), + ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ] @ l]. - refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp} - : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] := - match exp as E in Expr Γ Δ ξ τ with + refine (fix expr2proof Γ' Δ' ξ' τ' l' (exp:Expr Γ' Δ' ξ' τ' l') {struct exp} + : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ'] @ l'] := + match exp as E in Expr Γ Δ ξ τ l with | 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 - (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2) - | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e) + (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 - (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody) + (fun pf_let pf_body => _) (expr2proof _ _ _ _ _ ev) (expr2proof _ _ _ _ _ ebody) | ELetRec Γ Δ ξ lev t tree disti branches ebody => - let ξ' := update_ξ ξ lev (leaves tree) in - let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody) + 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') : 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 t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ e) + | 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) - | 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) + | 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: Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ 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) + (weakT' tbranches) (weakL' l) } }) : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) := match alts as ALTS return ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with @@ -1146,12 +1139,12 @@ Definition expr2proof : | T_Leaf (Some x) => match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with existT sac (existT scbx ex) => - (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex) + (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ _ ex) end end) alts') - in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e) + in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) end - ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp. + ); clear exp ξ' τ' Γ' Δ' l' expr2proof; try clear mkdcsp. destruct case_EGlobal. apply nd_rule. @@ -1179,13 +1172,13 @@ Definition expr2proof : 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 (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. @@ -1196,22 +1189,22 @@ Definition expr2proof : inversion H. destruct case_ELet; intros; simpl in *. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply pf_let. eapply nd_comp; [ apply pf_body | idtac ]. fold (@mapOptionTree VV). fold (mapOptionTree ξ). - set (update_ξ ξ v ((lev,tv)::nil)) as ξ'. + 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. @@ -1230,7 +1223,6 @@ Definition expr2proof : auto. destruct case_ENote. - destruct t. eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ]. apply e'. auto. @@ -1266,15 +1258,15 @@ 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 (@factorContextRightAndWeaken'') as q. - unfold scbwv_ξ. + 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. @@ -1285,7 +1277,7 @@ Definition expr2proof : 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.