Defined.
Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q,
- update_ξ ξ lev (app l1 l2) q = update_ξ (update_ξ ξ lev l2) lev l1 q.
+ update_xi ξ lev (app l1 l2) q = update_xi (update_xi ξ lev l2) lev l1 q.
intros.
induction l1.
reflexivity.
Lemma fresh_lemma'' Γ
: forall types ξ lev,
FreshM { varstypes : _
- | mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
+ | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
/\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
admit.
Defined.
Lemma fresh_lemma' Γ
: forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars ->
FreshM { varstypes : _
- | mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
- /\ mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
+ | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
+ /\ mapOptionTree (update_xi ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
/\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
induction types.
intros; destruct a.
intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _).
apply FreshMon.
destruct x2 as [vt2 [pf21 [pf22 pfdist]]].
- refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_ξ ξ lev
+ refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_xi ξ lev
(leaves vt2)) _ _; return _).
apply FreshMon.
simpl.
Lemma fresh_lemma Γ ξ vars Σ Σ' lev
: Σ = mapOptionTree ξ vars ->
FreshM { vars' : _
- | mapOptionTree (update_ξ(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
- /\ mapOptionTree (update_ξ ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
+ | mapOptionTree (update_xi(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
+ /\ mapOptionTree (update_xi ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
intros.
set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
refine (q >>>= fun q' => return _).
with
| RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ r)
| RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ r)
+ | RId a => let case_RId := tt in _
| RCanL a => let case_RCanL := tt in _
| RCanR a => let case_RCanR := tt in _
| RuCanL a => let case_RuCanL := tt in _
| RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g)
end); clear urule2expr; intros.
+ destruct case_RId.
+ apply X.
+
destruct case_RCanL.
simpl; unfold ujudg2exprType; intros.
simpl in X.
prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
((fun sac => FreshM
{ scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
- & Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars (weakCK'' Δ)) (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@ lev)) }) (projT1 pcb)).
+ & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev) (weakLT' (tbranches @@ lev)) }) (projT1 pcb)).
intro pcb.
intro X.
simpl in X.
cut (distinct (vec2list localvars'')). intro H'''.
set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
- refine (bind q = (f (scbwv_ξ scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
+ refine (bind q = (f (scbwv_xi scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
apply FreshMon.
simpl.
- unfold scbwv_ξ.
+ unfold scbwv_xi.
rewrite vars_pf.
rewrite <- mapOptionTree_compose.
clear localvars_pf1.
| RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
| RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
| RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
- | RJoin Γ p lri m x q => let case_RJoin := tt in _
- | RVoid _ _ => let case_RVoid := tt in _
+ | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p => let case_RWhere := tt in _
+ | RJoin Γ p lri m x q => let case_RJoin := tt in _
+ | RVoid _ _ => let case_RVoid := tt in _
| RBrak Σ a b c n m => let case_RBrak := tt in _
| REsc Σ a b c n m => let case_REsc := tt in _
| RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
destruct case_RGlobal.
apply ILeaf; simpl; intros; refine (return ILeaf _ _).
apply EGlobal.
- apply wev.
destruct case_RLam.
apply ILeaf.
refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
apply FreshMon.
destruct pf as [ vnew [ pf1 pf2 ]].
- set (update_ξ ξ x (((vnew, tx )) :: nil)) as ξ' in *.
+ set (update_xi ξ x (((vnew, tx )) :: nil)) as ξ' in *.
refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
apply FreshMon.
simpl.
apply ILeaf.
simpl in *; intros.
destruct vars; try destruct o; inversion H.
- refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
+
+ refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)).
apply FreshMon.
+
destruct pf as [ vnew [ pf1 pf2 ]].
- set (update_ξ ξ p (((vnew, σ₂ )) :: nil)) as ξ' in *.
+ set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
inversion X_.
apply ileaf in X.
apply ileaf in X0.
simpl in *.
- refine (X ξ vars2 _ >>>= fun X0' => _).
+
+ refine (X ξ vars1 _ >>>= fun X0' => _).
apply FreshMon.
+ simpl.
auto.
- refine (X0 ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
+ refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _).
apply FreshMon.
- rewrite H1.
simpl.
rewrite pf2.
rewrite pf1.
- rewrite H1.
reflexivity.
+ apply FreshMon.
- refine (return _).
apply ILeaf.
- apply ileaf in X0'.
apply ileaf in X1'.
+ apply ileaf in X0'.
simpl in *.
- apply ELet with (ev:=vnew)(tv:=σ₂).
+ apply ELet with (ev:=vnew)(tv:=σ₁).
apply X0'.
apply X1'.
+ destruct case_RWhere.
+ apply ILeaf.
+ simpl in *; intros.
+ destruct vars; try destruct o; inversion H.
+ destruct vars2; try destruct o; inversion H2.
+ clear H2.
+
+ assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto.
+ refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)).
+ apply FreshMon.
+
+ destruct pf as [ vnew [ pf1 pf2 ]].
+ set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
+ inversion X_.
+ apply ileaf in X.
+ apply ileaf in X0.
+ simpl in *.
+
+ refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _).
+ apply FreshMon.
+ simpl.
+ inversion pf1.
+ rewrite H3.
+ rewrite H4.
+ rewrite pf2.
+ reflexivity.
+
+ refine (X0 ξ vars2_1 _ >>>= fun X1' => _).
+ apply FreshMon.
+ reflexivity.
+ apply FreshMon.
+
+ apply ILeaf.
+ apply ileaf in X0'.
+ apply ileaf in X1'.
+ simpl in *.
+ apply ELet with (ev:=vnew)(tv:=σ₁).
+ apply X1'.
+ apply X0'.
+
destruct case_RVoid.
apply ILeaf; simpl; intros.
refine (return _).
apply ILeaf; simpl; intros.
refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
- refine (X_ ((update_ξ ξ t (leaves varstypes)))
+ refine (X_ ((update_xi ξ t (leaves varstypes)))
(vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon.
simpl.
rewrite pf2.
inversion X; subst; clear X.
apply (@ELetRec _ _ _ _ _ _ _ varstypes).
+ auto.
apply (@letrec_helper Γ Δ t varstypes).
- rewrite <- pf2 in X1.
+ rewrite <- pf2 in X0.
rewrite mapOptionTree_compose.
- apply X1.
- apply ileaf in X0.
apply X0.
+ apply ileaf in X1.
+ apply X1.
destruct case_RCase.
apply ILeaf; simpl; intros.
apply H2.
Defined.
- Definition closed2expr : forall c (pn:@ClosedSIND _ Rule c), ITree _ judg2exprType c.
- refine ((
- fix closed2expr' j (pn:@ClosedSIND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
- match pn in @ClosedSIND _ _ J return ITree _ judg2exprType J with
- | cnd_weak => let case_nil := tt in INone _ _
- | cnd_rule h c cnd' r => let case_rule := tt in rule2expr _ _ r (closed2expr' _ cnd')
- | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2)
- end)); clear closed2expr'; intros; subst.
- Defined.
+ Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
+ match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
+ | scnd_weak _ => let case_nil := tt in fun _ => INone _ _
+ | scnd_comp x h c cnd' r => let case_rule := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
+ | scnd_branch _ _ _ c1 c2 => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
+ end.
Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
clear q.
destruct q' as [varstypes [pf1 [pf2 distpf]]].
exists (mapOptionTree (@fst _ _) varstypes).
- exists (update_ξ ξ l (leaves varstypes)).
+ exists (update_xi ξ l (leaves varstypes)).
symmetry; auto.
refine (return _).
exists [].
{zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
intro pf.
- set (closedFromSIND _ _ (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
+ set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
apply closed2expr in cnd.
apply ileaf in cnd.
simpl in *.
refine (return OK _).
exists ξ.
apply (ileaf it).
+ apply INone.
Defined.
End HaskProofToStrong.
projects / coq-hetmet.git / blobdiff