forall v1 v2,
distinct (map (@fst _ _) (leaves (v1,,(varstypes,,v2)))) ->
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 ].
mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
induction varstypes; intros.
destruct a; simpl; [ idtac | reflexivity ].
| ECase Γ Δ ξ l tc tbranches atypes e' alts =>
((fix varsfromalts (alts:
Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
| ECase Γ Δ ξ l tc tbranches atypes e' alts =>
((fix varsfromalts (alts:
Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
(alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
(alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
= mapOptionTree ξ (stripOutVars (v :: nil) tree).
set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
rewrite p.
= mapOptionTree ξ (stripOutVars (v :: nil) tree).
set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
rewrite p.
Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
| lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
| lrsp_leaf : forall v t e ,
Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
| lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
| lrsp_leaf : forall v t e ,
LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)
| lrsp_cons : forall t1 t2 b1 b2,
LetRecSubproofs Γ Δ ξ lev t1 b1 ->
LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)
| lrsp_cons : forall t1 t2 b1 b2,
LetRecSubproofs Γ Δ ξ lev t1 b1 ->
Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
LetRecSubproofs Γ Δ ξ lev tree branches ->
ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
LetRecSubproofs Γ Δ ξ lev tree branches ->
ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree :
forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))),
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].
set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
set (mapOptionTree (@fst _ _) tree) as pctx.
set (mapOptionTree ξ' pctx) as passback.
set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
set (mapOptionTree (@fst _ _) tree) as pctx.
set (mapOptionTree ξ' pctx) as passback.
eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
eapply nd_comp; [ apply nd_rlecnac | idtac ].
apply nd_prod; auto.
eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
eapply nd_comp; [ apply nd_rlecnac | idtac ].
apply nd_prod; auto.
Defined.
Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
forall l ξ,
Defined.
Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
forall l ξ,
(unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
) as q.
rewrite <- mapleaves' in q.
(unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
) as q.
rewrite <- mapleaves' in q.
- 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))}}),
match exp as E in Expr Γ Δ ξ τ with
| EGlobal Γ Δ ξ g v lev => let case_EGlobal := tt in _
| EVar Γ Δ ξ ev => let case_EVar := tt in _
match exp as E in Expr Γ Δ ξ τ with
| EGlobal Γ Δ ξ g v lev => let case_EGlobal := tt in _
| EVar Γ Δ ξ ev => let case_EVar := tt in _
| 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 =>
| 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 case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
(branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
(branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
(weakLT' (tbranches@@l)) } })
: ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
match alts as ALTS return ND Rule []
(weakLT' (tbranches@@l)) } })
: ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
match alts as ALTS return ND Rule []
destruct case_ELam; intros.
unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
destruct case_ELam; intros.
unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
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.
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.
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.
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.
rewrite <- (scbwv_coherent scbx l ξ).
rewrite <- vec2list_map_list2vec.
rewrite mapleaves'.
set (@factorContextRightAndWeaken'') as q.
rewrite <- (scbwv_coherent scbx l ξ).
rewrite <- vec2list_map_list2vec.
rewrite mapleaves'.
set (@factorContextRightAndWeaken'') as q.
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.
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.
replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
(stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
apply q.
replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
(stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
apply q.