Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★.
- Definition ujudg2exprType {Γ}{Δ}(ξ:ExprVarResolver Γ)(j:UJudg Γ Δ) : Type :=
- match j with
- mkUJudg Σ τ => forall vars, Σ = mapOptionTree ξ vars ->
- FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
- end.
-
Definition judg2exprType (j:Judg) : Type :=
match j with
(Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
inversion pf2.
Defined.
+ Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ : Type :=
+ forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ).
+
Definition urule2expr : forall Γ Δ h j t (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
- ujudg2exprType ξ (Γ >> Δ > h |- t) ->
- ujudg2exprType ξ (Γ >> Δ > j |- t)
+ ujudg2exprType Γ ξ Δ h t ->
+ ujudg2exprType Γ ξ Δ j t
.
intros Γ Δ.
refine (fix urule2expr h j t (r:@Arrange _ h j) ξ {struct r} :
- ujudg2exprType ξ (Γ >> Δ > h |- t) ->
- ujudg2exprType ξ (Γ >> Δ > j |- t) :=
- match r as R in Arrange H C return ujudg2exprType ξ (Γ >> Δ > H |- t) ->
- ujudg2exprType ξ (Γ >> Δ > C |- t) with
+ ujudg2exprType Γ ξ Δ h t ->
+ ujudg2exprType Γ ξ Δ j t :=
+ match r as R in Arrange H C return
+ ujudg2exprType Γ ξ Δ H t ->
+ ujudg2exprType Γ ξ Δ C t
+ 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; intros.
+ simpl; unfold ujudg2exprType; intros.
simpl in X.
apply (X ([],,vars)).
simpl; rewrite <- H; auto.
destruct case_RCanR.
- simpl; intros.
+ simpl; unfold ujudg2exprType; intros.
simpl in X.
apply (X (vars,,[])).
simpl; rewrite <- H; auto.
destruct case_RuCanL.
- simpl; intros.
+ simpl; unfold ujudg2exprType; intros.
destruct vars; try destruct o; inversion H.
simpl in X.
apply (X vars2); auto.
destruct case_RuCanR.
- simpl; intros.
+ simpl; unfold ujudg2exprType; intros.
destruct vars; try destruct o; inversion H.
simpl in X.
apply (X vars1); auto.
destruct case_RAssoc.
- simpl; intros.
+ simpl; unfold ujudg2exprType; intros.
simpl in X.
destruct vars; try destruct o; inversion H.
destruct vars1; try destruct o; inversion H.
subst; auto.
destruct case_RCossa.
- simpl; intros.
+ simpl; unfold ujudg2exprType; intros.
simpl in X.
destruct vars; try destruct o; inversion H.
destruct vars2; try destruct o; inversion H.
subst; auto.
destruct case_RExch.
- simpl; intros.
+ simpl; unfold ujudg2exprType ; intros.
simpl in X.
destruct vars; try destruct o; inversion H.
apply (X (vars2,,vars1)).
inversion H; subst; auto.
destruct case_RWeak.
- simpl; intros.
+ simpl; unfold ujudg2exprType; intros.
simpl in X.
apply (X []).
auto.
destruct case_RCont.
- simpl; intros.
+ simpl; unfold ujudg2exprType ; intros.
simpl in X.
apply (X (vars,,vars)).
simpl.
auto.
destruct case_RLeft.
- intro vars; intro H.
+ intro vars; unfold ujudg2exprType; intro H.
destruct vars; try destruct o; inversion H.
apply (fun q => e ξ q vars2 H2).
clear r0 e H2.
simpl in X.
simpl.
+ unfold ujudg2exprType.
intros.
apply X with (vars:=vars1,,vars).
rewrite H0.
reflexivity.
destruct case_RRight.
- intro vars; intro H.
+ intro vars; unfold ujudg2exprType; intro H.
destruct vars; try destruct o; inversion H.
apply (fun q => e ξ q vars1 H1).
clear r0 e H2.
simpl in X.
simpl.
+ unfold ujudg2exprType.
intros.
apply X with (vars:=vars,,vars2).
rewrite H0.
| RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
| RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
| RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
- | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
- | REmptyGroup _ _ => let case_REmptyGroup := 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 _
simpl in q'.
apply q' with (vars:=vars).
clear q' q.
+ unfold ujudg2exprType.
intros.
apply X_ with (vars:=vars0).
auto.
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_ξ ξ x (((vnew, tx )) :: nil)) as ξ' in *.
refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
apply FreshMon.
simpl.
apply ileaf in X. simpl in X.
apply X.
- destruct case_RBindingGroup.
+ destruct case_RJoin.
apply ILeaf; simpl; intros.
inversion X_.
apply ileaf in X.
apply ileaf in q1'.
apply ileaf in q2'.
simpl in *.
- apply (EApp _ _ _ _ _ _ q1' q2').
+ apply (EApp _ _ _ _ _ _ q2' q1').
destruct case_RLet.
apply ILeaf.
refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
apply FreshMon.
destruct pf as [ vnew [ pf1 pf2 ]].
- set (update_ξ ξ p ((⟨vnew, σ₂ ⟩) :: nil)) as ξ' in *.
+ set (update_ξ ξ p (((vnew, σ₂ )) :: nil)) as ξ' in *.
inversion X_.
apply ileaf in X.
apply ileaf in X0.
simpl in *.
- refine (X0 ξ vars2 _ >>>= fun X0' => _).
+ refine (X ξ vars2 _ >>>= fun X0' => _).
apply FreshMon.
auto.
- refine (X ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
+
+ refine (X0 ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
apply FreshMon.
rewrite H1.
simpl.
rewrite pf1.
rewrite H1.
reflexivity.
+
refine (return _).
apply ILeaf.
apply ileaf in X0'.
apply X0'.
apply X1'.
- destruct case_REmptyGroup.
+ destruct case_RVoid.
apply ILeaf; simpl; intros.
refine (return _).
apply INone.
inversion X; subst; clear X.
apply (@ELetRec _ _ _ _ _ _ _ varstypes).
+ auto.
apply (@letrec_helper Γ Δ t varstypes).
rewrite <- pf2 in X1.
rewrite mapOptionTree_compose.
apply H2.
Defined.
- Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
- refine ((
- fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
- match pn in @ClosedND _ _ 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 } }.
{zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
intro pf.
- set (closedFromSCND _ _ (mkSCND 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