- destruct case_RURule.
- destruct d; [ destruct o | idtac ]; inversion H; subst.
- clear H.
- destruct u.
- refine (match e as R in URule H C return C=[a >> b > t1 |- t2] -> _ with
- | RLeft h c ctx r => let case_RLeft := tt in _
- | RRight h c ctx r => let case_RRight := tt in _
- | RCanL t a => let case_RCanL := tt in _
- | RCanR t a => let case_RCanR := tt in _
- | RuCanL t a => let case_RuCanL := tt in _
- | RuCanR t a => let case_RuCanR := tt in _
- | RAssoc t a b c => let case_RAssoc := tt in _
- | RCossa t a b c => let case_RCossa := tt in _
- | RExch t a b => let case_RExch := tt in _
- | RWeak t a => let case_RWeak := tt in _
- | RCont t a => let case_RCont := tt in _
- end (refl_equal _) ); intros.
-
- destruct case_RCanL. admit.
- destruct case_RCanR. admit.
- destruct case_RuCanL. admit.
- destruct case_RuCanR. admit.
- destruct case_RAssoc. admit.
- destruct case_RCossa. admit.
- destruct case_RLeft. admit.
- destruct case_RRight. admit.
- destruct case_RExch. admit.
- destruct case_RWeak. admit.
- destruct case_RCont. admit.
- destruct case_RBrak. admit.
- destruct case_REsc. admit.
- destruct case_RNote. admit.
- destruct case_RLit. admit.
- destruct case_RVar. admit.
- destruct case_RLam. admit.
- destruct case_RCast. admit.
- destruct case_RBindingGroup. admit.
- destruct case_RApp. admit.
- destruct case_RLet. admit.
- destruct case_REmptyGroup. admit.
- destruct case_RAppT. admit.
- destruct case_RAbsT. admit.
- destruct case_RAppCo. admit.
- destruct case_RAbsCo. admit.
- destruct case_RLetRec. admit.
- destruct case_RCase. admit.
- 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 _
- | cnd_rule h c cnd' r => let case_rule := tt in (fun rest => _) (closed2expr' _ cnd')
- | cnd_branch _ _ c1 c2 => let case_branch := tt in (fun rest1 rest2 => _) (closed2expr' _ c1) (closed2expr' _ c2)
- end)); clear closed2expr'; intros; subst.
-
- destruct case_nil.
- apply INone.
-
- destruct case_rule.
- set (@rule2expr h) as q.
- destruct c.
- destruct o.
- apply ILeaf.
- eapply rule2expr.
- apply r.
- apply rest.
-
- apply no_rules_with_empty_conclusion in r.
- inversion r.
- auto.
+ Definition ileaf `(it:ITree X F [t]) : F t.
+ inversion it.
+ apply X0.
+ Defined.
+
+ Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q,
+ update_ξ ξ lev (app l1 l2) q = update_ξ (update_ξ ξ lev l2) lev l1 q.
+ intros.
+ induction l1.
+ reflexivity.
+ simpl.
+ destruct a; simpl.
+ rewrite IHl1.
+ reflexivity.
+ Qed.
+
+ Lemma quark {T} (l1:list T) l2 vf :
+ (In vf (app l1 l2)) <->
+ (In vf l1) \/ (In vf l2).
+ induction l1.
+ simpl; auto.
+ split; intro.
+ right; auto.
+ inversion H.
+ inversion H0.
+ auto.
+ split.
+
+ destruct IHl1.
+ simpl in *.
+ intro.
+ destruct H1.
+ left; left; auto.
+ set (H H1) as q.
+ destruct q.
+ left; right; auto.
+ right; auto.
+ simpl.
+
+ destruct IHl1.
+ simpl in *.
+ intro.
+ destruct H1.
+ destruct H1.
+ left; auto.
+ right; apply H0; auto.
+ right; apply H0; auto.
+ Qed.
+
+ Lemma splitter {T} (l1:list T) l2 vf :
+ (In vf (app l1 l2) → False)
+ -> (In vf l1 → False) /\ (In vf l2 → False).
+ intros.
+ split; intros; apply H; rewrite quark.
+ auto.
+ auto.
+ Qed.
+
+ Lemma helper
+ : forall T Z {eqdt:EqDecidable T}(tl:Tree ??T)(vf:T) ξ (q:Z),
+ (In vf (leaves tl) -> False) ->
+ mapOptionTree (fun v' => if eqd_dec vf v' then q else ξ v') tl =
+ mapOptionTree ξ tl.
+ intros.
+ induction tl;
+ try destruct a;
+ simpl in *.
+ set (eqd_dec vf t) as x in *.
+ destruct x.
+ subst.
+ assert False.
+ apply H.
+ left; auto.
+ inversion H0.
+ auto.
+ auto.
+ apply splitter in H.
+ destruct H.
+ rewrite (IHtl1 H).
+ rewrite (IHtl2 H0).
+ reflexivity.
+ Qed.
+
+ Lemma fresh_lemma'' Γ
+ : forall types ξ lev,
+ FreshM { varstypes : _
+ | mapOptionTree (update_ξ(Γ:=Γ) ξ 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)
+ /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
+ induction types.
+ intros; destruct a.
+ refine (bind vf = fresh (leaves vars) ; return _).
+ apply FreshMon.
+ destruct vf as [ vf vf_pf ].
+ exists [(vf,h)].
+ split; auto.
+ simpl.
+ set (helper VV _ vars vf ξ (h@@lev) vf_pf) as q.
+ rewrite q.
+ symmetry; auto.
+ simpl.
+ destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto.
+ split; auto.
+ apply distinct_cons.
+ intro.
+ inversion H0.
+ apply distinct_nil.
+ refine (return _).
+ exists []; auto.
+ split.
+ simpl.
+ symmetry; auto.
+ split.
+ simpl.
+ reflexivity.
+ simpl.
+ apply distinct_nil.
+ 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
+ (leaves vt2)) _ _; return _).
+ apply FreshMon.
+ simpl.
+ rewrite pf21.
+ rewrite pf22.
+ reflexivity.
+ clear IHtypes1 IHtypes2.
+ destruct x1 as [vt1 [pf11 pf12]].
+ exists (vt1,,vt2); split; auto.
+
+ set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
+ set (mapOptionTree_extensional _ _ q) as q'.
+ rewrite q'.
+ clear q' q.
+ inversion pf11.
+ reflexivity.
+
+ simpl.
+ set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
+ set (mapOptionTree_extensional _ _ q) as q'.
+ rewrite q'.
+ rewrite q'.
+ clear q' q.
+ rewrite <- mapOptionTree_compose.
+ rewrite <- mapOptionTree_compose.
+ rewrite <- mapOptionTree_compose in *.
+ split.
+ destruct pf12.
+ rewrite H.
+ inversion pf11.
+ rewrite <- mapOptionTree_compose.
+ reflexivity.
+
+ admit.
+ Defined.
+
+ Lemma fresh_lemma Γ ξ vars Σ Σ' lev
+ : Σ = mapOptionTree ξ vars ->
+ FreshM { vars' : _
+ | mapOptionTree (update_ξ(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
+ /\ mapOptionTree (update_ξ ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
+ intros.
+ set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
+ refine (q >>>= fun q' => return _).
+ apply FreshMon.
+ clear q.
+ destruct q' as [varstypes [pf1 [pf2 pfdist]]].
+ destruct varstypes; try destruct o; try destruct p; simpl in *.
+ destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
+ inversion pf2; subst.
+ exists v.
+ destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
+ split; auto.
+ inversion pf2.
+ 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
+ .
+ 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
+ | 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 _
+ | RuCanR a => let case_RuCanR := tt in _
+ | RAssoc a b c => let case_RAssoc := tt in _
+ | RCossa a b c => let case_RCossa := tt in _
+ | RExch a b => let case_RExch := tt in _
+ | RWeak a => let case_RWeak := tt in _
+ | RCont a => let case_RCont := 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.
+ apply (X ([],,vars)).
+ simpl; rewrite <- H; auto.
+
+ destruct case_RCanR.
+ simpl; unfold ujudg2exprType; intros.
+ simpl in X.
+ apply (X (vars,,[])).
+ simpl; rewrite <- H; auto.