src/HaskProofToStrong.v

   1 (*********************************************************************************************************************************)
   2 (* HaskProofToStrong: convert HaskProof to HaskStrong                                                                            *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import NaturalDeduction.
   9 Require Import Coq.Strings.String.
  10 Require Import Coq.Lists.List.
  11 Require Import Coq.Init.Specif.
  12 Require Import HaskKinds.
  13 Require Import HaskStrongTypes.
  14 Require Import HaskStrong.
  15 Require Import HaskProof.
  16
  17 Section HaskProofToStrong.
  18
  19   Context {VV:Type} {eqdec_vv:EqDecidable VV} {freshM:FreshMonad VV}.
  20
  21   Definition fresh := FMT_fresh freshM.
  22   Definition FreshM := FMT freshM.
  23   Definition FreshMon := FMT_Monad freshM.
  24   Existing Instance FreshMon.
  25
  26   Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★.
  27
  28   Definition ujudg2exprType {Γ}{Δ}(ξ:ExprVarResolver Γ)(j:UJudg Γ Δ) : Type :=
  29     match j with
  30       mkUJudg Σ τ => forall vars, Σ = mapOptionTree ξ vars ->
  31         FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
  32       end.
  33
  34   Definition judg2exprType (j:Judg) : Type :=
  35     match j with
  36       (Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
  37         FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
  38       end.
  39
  40   Definition justOne Γ Δ ξ τ : ITree _ (fun t => Expr Γ Δ ξ t) [τ] -> Expr Γ Δ ξ τ.
  41     intros.
  42     inversion X; auto.
  43     Defined.
  44
  45   Definition ileaf `(it:ITree X F [t]) : F t.
  46     inversion it.
  47     apply X0.
  48     Defined.
  49
  50   Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q,
  51     update_ξ ξ lev (app l1 l2) q = update_ξ (update_ξ ξ lev l2) lev l1 q.
  52     intros.
  53     induction l1.
  54       reflexivity.
  55       simpl.
  56       destruct a; simpl.
  57       rewrite IHl1.
  58       reflexivity.
  59       Qed.
  60
  61    Lemma quark {T} (l1:list T) l2 vf :
  62       (In vf (app l1 l2)) <->
  63        (In vf l1) \/ (In vf l2).
  64      induction l1.
  65      simpl; auto.
  66      split; intro.
  67      right; auto.
  68      inversion H.
  69      inversion H0.
  70      auto.
  71      split.
  72
  73      destruct IHl1.
  74      simpl in *.
  75      intro.
  76      destruct H1.
  77      left; left; auto.
  78      set (H H1) as q.
  79      destruct q.
  80      left; right; auto.
  81      right; auto.
  82      simpl.
  83
  84      destruct IHl1.
  85      simpl in *.
  86      intro.
  87      destruct H1.
  88      destruct H1.
  89      left; auto.
  90      right; apply H0; auto.
  91      right; apply H0; auto.
  92    Qed.
  93
  94   Lemma splitter {T} (l1:list T) l2 vf :
  95       (In vf (app l1 l2) → False)
  96       -> (In vf l1 → False)  /\ (In vf l2 → False).
  97     intros.
  98     split; intros; apply H; rewrite quark.
  99     auto.
 100     auto.
 101     Qed.
 102
 103   Lemma helper
 104     : forall T Z {eqdt:EqDecidable T}(tl:Tree ??T)(vf:T) ξ (q:Z),
 105       (In vf (leaves tl) -> False) ->
 106       mapOptionTree (fun v' => if eqd_dec vf v' then q else ξ v') tl =
 107       mapOptionTree ξ tl.
 108     intros.
 109     induction tl;
 110       try destruct a;
 111         simpl in *.
 112     set (eqd_dec vf t) as x in *.
 113     destruct x.
 114     subst.
 115       assert False.
 116       apply H.
 117       left; auto.
 118       inversion H0.
 119     auto.
 120     auto.
 121     apply splitter in H.
 122     destruct H.
 123     rewrite (IHtl1 H).
 124     rewrite (IHtl2 H0).
 125     reflexivity.
 126     Qed.
 127
 128   Lemma fresh_lemma' Γ
 129     : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars ->
 130     FreshM { varstypes : _
 131       |  mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
 132       /\ mapOptionTree (update_ξ       ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
 133       /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
 134     induction types.
 135       intros; destruct a.
 136         refine (bind vf = fresh (leaves vars) ; return _).
 137           apply FreshMon.
 138           destruct vf as [ vf vf_pf ].
 139           exists [(vf,h)].
 140           split; auto.
 141           simpl.
 142           set (helper VV _ vars vf ξ (h@@lev) vf_pf) as q.
 143           rewrite q.
 144           symmetry; auto.
 145           simpl.
 146           destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto.
 147           split; auto.
 148           apply distinct_cons.
 149           intro.
 150           inversion H0.
 151           apply distinct_nil.
 152         refine (return _).
 153           exists []; auto.
 154           split.
 155           simpl.
 156           symmetry; auto.
 157           split.
 158           simpl.
 159           reflexivity.
 160           simpl.
 161           apply distinct_nil.
 162         intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _).
 163           apply FreshMon.
 164           destruct x2 as [vt2 [pf21 [pf22 pfdist]]].
 165           refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_ξ ξ lev
 166             (leaves vt2)) _ _; return _).
 167           apply FreshMon.
 168           simpl.
 169           rewrite pf21.
 170           rewrite pf22.
 171           reflexivity.
 172           clear IHtypes1 IHtypes2.
 173           destruct x1 as [vt1 [pf11 pf12]].
 174           exists (vt1,,vt2); split; auto.
 175
 176           set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
 177           set (mapOptionTree_extensional _ _ q) as q'.
 178           rewrite q'.
 179           clear q' q.
 180           inversion pf11.
 181           reflexivity.
 182
 183           simpl.
 184           set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
 185           set (mapOptionTree_extensional _ _ q) as q'.
 186           rewrite q'.
 187           rewrite q'.
 188           clear q' q.
 189           rewrite <- mapOptionTree_compose.
 190           rewrite <- mapOptionTree_compose.
 191           rewrite <- mapOptionTree_compose in *.
 192           split.
 193           destruct pf12.
 194           rewrite H.
 195           inversion pf11.
 196           rewrite <- mapOptionTree_compose.
 197           reflexivity.
 198
 199           admit.
 200         Defined.
 201
 202   Lemma fresh_lemma Γ ξ vars Σ Σ' lev
 203     : Σ = mapOptionTree ξ vars ->
 204     FreshM { vars' : _
 205       |  mapOptionTree (update_ξ(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
 206       /\ mapOptionTree (update_ξ ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
 207     intros.
 208     set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
 209     refine (q >>>= fun q' => return _).
 210     apply FreshMon.
 211     clear q.
 212     destruct q' as [varstypes [pf1 [pf2 pfdist]]].
 213     destruct varstypes; try destruct o; try destruct p; simpl in *.
 214       destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
 215       inversion pf2; subst.
 216       exists v.
 217       destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
 218       split; auto.
 219       inversion pf2.
 220       inversion pf2.
 221     Defined.
 222
 223   Definition urule2expr  : forall Γ Δ h j (r:@URule Γ Δ h j) (ξ:VV -> LeveledHaskType Γ ★),
 224     ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j.
 225
 226       refine (fix urule2expr Γ Δ h j (r:@URule Γ Δ h j) ξ {struct r} :
 227         ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j :=
 228         match r as R in URule H C return ITree _ (ujudg2exprType ξ) H -> ITree _ (ujudg2exprType ξ) C with
 229           | RLeft   h c ctx r => let case_RLeft  := tt in (fun e => _) (urule2expr _ _ _ _ r)
 230           | RRight  h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r)
 231           | RCanL   t a       => let case_RCanL  := tt in _
 232           | RCanR   t a       => let case_RCanR  := tt in _
 233           | RuCanL  t a       => let case_RuCanL := tt in _
 234           | RuCanR  t a       => let case_RuCanR := tt in _
 235           | RAssoc  t a b c   => let case_RAssoc := tt in _
 236           | RCossa  t a b c   => let case_RCossa := tt in _
 237           | RExch   t a b     => let case_RExch  := tt in _
 238           | RWeak   t a       => let case_RWeak  := tt in _
 239           | RCont   t a       => let case_RCont  := tt in _
 240           end); clear urule2expr; intros.
 241
 242       destruct case_RCanL.
 243         apply ILeaf; simpl; intros.
 244         inversion X.
 245         simpl in X0.
 246         apply (X0 ([],,vars)).
 247         simpl; rewrite <- H; auto.
 248
 249       destruct case_RCanR.
 250         apply ILeaf; simpl; intros.
 251         inversion X.
 252         simpl in X0.
 253         apply (X0 (vars,,[])).
 254         simpl; rewrite <- H; auto.
 255
 256       destruct case_RuCanL.
 257         apply ILeaf; simpl; intros.
 258         destruct vars; try destruct o; inversion H.
 259         inversion X.
 260         simpl in X0.
 261         apply (X0 vars2); auto.
 262
 263       destruct case_RuCanR.
 264         apply ILeaf; simpl; intros.
 265         destruct vars; try destruct o; inversion H.
 266         inversion X.
 267         simpl in X0.
 268         apply (X0 vars1); auto.
 269
 270       destruct case_RAssoc.
 271         apply ILeaf; simpl; intros.
 272         inversion X.
 273         simpl in X0.
 274         destruct vars; try destruct o; inversion H.
 275         destruct vars1; try destruct o; inversion H.
 276         apply (X0 (vars1_1,,(vars1_2,,vars2))).
 277         subst; auto.
 278
 279       destruct case_RCossa.
 280         apply ILeaf; simpl; intros.
 281         inversion X.
 282         simpl in X0.
 283         destruct vars; try destruct o; inversion H.
 284         destruct vars2; try destruct o; inversion H.
 285         apply (X0 ((vars1,,vars2_1),,vars2_2)).
 286         subst; auto.
 287
 288       destruct case_RLeft.
 289         destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
 290         destruct o; [ idtac | apply INone ].
 291         destruct u; simpl in *.
 292         apply ILeaf; simpl; intros.
 293         destruct vars; try destruct o; inversion H.
 294         set (fun q => ileaf (e ξ q)) as r'.
 295         simpl in r'.
 296         apply r' with (vars:=vars2).
 297         clear r' e.
 298         clear r0.
 299         induction h0.
 300           destruct a.
 301           destruct u.
 302           simpl in X.
 303           apply ileaf in X.
 304           apply ILeaf.
 305           simpl.
 306           simpl in X.
 307           intros.
 308           apply X with (vars:=vars1,,vars).
 309           simpl.
 310           rewrite H0.
 311           rewrite H1.
 312           reflexivity.
 313           apply INone.
 314           apply IBranch.
 315           apply IHh0_1. inversion X; auto.
 316           apply IHh0_2. inversion X; auto.
 317           auto.
 318
 319       destruct case_RRight.
 320         destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
 321         destruct o; [ idtac | apply INone ].
 322         destruct u; simpl in *.
 323         apply ILeaf; simpl; intros.
 324         destruct vars; try destruct o; inversion H.
 325         set (fun q => ileaf (e ξ q)) as r'.
 326         simpl in r'.
 327         apply r' with (vars:=vars1).
 328         clear r' e.
 329         clear r0.
 330         induction h0.
 331           destruct a.
 332           destruct u.
 333           simpl in X.
 334           apply ileaf in X.
 335           apply ILeaf.
 336           simpl.
 337           simpl in X.
 338           intros.
 339           apply X with (vars:=vars,,vars2).
 340           simpl.
 341           rewrite H0.
 342           rewrite H2.
 343           reflexivity.
 344           apply INone.
 345           apply IBranch.
 346           apply IHh0_1. inversion X; auto.
 347           apply IHh0_2. inversion X; auto.
 348           auto.
 349
 350       destruct case_RExch.
 351         apply ILeaf; simpl; intros.
 352         inversion X.
 353         simpl in X0.
 354         destruct vars; try destruct o; inversion H.
 355         apply (X0 (vars2,,vars1)).
 356         inversion H; subst; auto.
 357
 358       destruct case_RWeak.
 359         apply ILeaf; simpl; intros.
 360         inversion X.
 361         simpl in X0.
 362         apply (X0 []).
 363         auto.
 364
 365       destruct case_RCont.
 366         apply ILeaf; simpl; intros.
 367         inversion X.
 368         simpl in X0.
 369         apply (X0 (vars,,vars)).
 370         simpl.
 371         rewrite <- H.
 372         auto.
 373         Defined.
 374
 375   Definition bridge Γ Δ (c:Tree ??(UJudg Γ Δ)) ξ :
 376     ITree Judg judg2exprType (mapOptionTree UJudg2judg c) -> ITree (UJudg Γ Δ) (ujudg2exprType ξ) c.
 377     intro it.
 378     induction c.
 379     destruct a.
 380       destruct u; simpl in *.
 381       apply ileaf in it.
 382       apply ILeaf.
 383       simpl in *.
 384       intros; apply it with (vars:=vars); auto.
 385     apply INone.
 386     apply IBranch; [ apply IHc1 | apply IHc2 ]; inversion it; auto.
 387     Defined.
 388
 389   Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
 390     ITree (LeveledHaskType Γ ★)
 391          (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
 392          (mapOptionTree (ξ' ○ (@fst _ _)) varstypes)
 393          -> ELetRecBindings Γ Δ ξ' l varstypes.
 394     intros.
 395     induction varstypes.
 396     destruct a; simpl in *.
 397     destruct p.
 398     simpl.
 399     apply ileaf in X. simpl in X.
 400       apply ELR_leaf.
 401       rename h into τ.
 402       destruct (eqd_dec (unlev (ξ' v)) τ).
 403       rewrite <- e.
 404       destruct (ξ' v).
 405       simpl.
 406       destruct (eqd_dec h0 l).
 407         rewrite <- e0.
 408         apply X.
 409       apply (Prelude_error "level mismatch; should never happen").
 410       apply (Prelude_error "letrec type mismatch; should never happen").
 411
 412     apply ELR_nil.
 413     apply ELR_branch.
 414       apply IHvarstypes1; inversion X; auto.
 415       apply IHvarstypes2; inversion X; auto.
 416     Defined.
 417
 418   Definition case_helper tc Γ Δ lev tbranches avars ξ (Σ:Tree ??VV) :
 419     forall pcb : ProofCaseBranch tc Γ Δ lev tbranches avars,
 420     judg2exprType (pcb_judg pcb) ->
 421     (pcb_freevars pcb) = mapOptionTree ξ Σ ->
 422     FreshM
 423     {scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars &
 424     Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars (weakCK'' Δ))
 425     (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@  lev))}.
 426
 427     intros.
 428     simpl in X.
 429     destruct pcb.
 430     simpl in *.
 431     set (sac_types pcb_scb _ avars) as boundvars.
 432     refine (fresh_lemma' _ (unleaves (vec2list boundvars)) Σ (mapOptionTree weakLT' pcb_freevars) (weakLT' ○ ξ) (weakL' lev) _
 433       >>>= fun ξvars => _). apply FreshMon.
 434     rewrite H.
 435     rewrite <- mapOptionTree_compose.
 436     reflexivity.
 437       destruct ξvars as [ exprvars [pf1 [pf2 pfdistinct]]].
 438       set (list2vec (leaves (mapOptionTree (@fst _ _) exprvars))) as exprvars'.
 439
 440    assert (distinct (vec2list exprvars')) as pfdistinct'.
 441      unfold exprvars'.
 442      rewrite vec2list_list2vec.
 443      apply pfdistinct.
 444
 445       assert (sac_numExprVars pcb_scb = Datatypes.length (leaves (mapOptionTree (@fst _ _) exprvars))) as H'.
 446         rewrite <- mapOptionTree_compose in pf2.
 447         simpl in pf2.
 448         rewrite mapleaves.
 449         rewrite <- map_preserves_length.
 450         rewrite map_preserves_length with (f:=
 451           (@update_ξ VV eqdec_vv (@sac_Γ tc pcb_scb Γ)
 452             (@weakLT' Γ (@vec2list (@sac_numExTyVars tc pcb_scb) Kind (@sac_ekinds tc pcb_scb)) ★ ○ ξ)
 453             (@weakL'  Γ (@vec2list (@sac_numExTyVars tc pcb_scb) Kind (@sac_ekinds tc pcb_scb)) lev)
 454             (@leaves (VV * HaskType (@sac_Γ tc pcb_scb Γ) ★) exprvars) ○ @fst VV (HaskType (@sac_Γ tc pcb_scb Γ) ★))).
 455         rewrite <- mapleaves.
 456         rewrite pf2.
 457         rewrite <- mapleaves'.
 458         rewrite leaves_unleaves.
 459         rewrite vec2list_map_list2vec.
 460         rewrite vec2list_len.
 461         reflexivity.
 462
 463         clear pfdistinct'.
 464      rewrite <- H' in exprvars'.
 465        clear H'.
 466    assert (distinct (vec2list exprvars')) as pfdistinct'.
 467      admit.
 468
 469    set (@Build_StrongCaseBranchWithVVs VV _ tc _ avars pcb_scb exprvars' pfdistinct') as scb.
 470       set (scbwv_ξ scb ξ lev) as ξ'.
 471       refine (X ξ' (Σ,,(unleaves (vec2list exprvars'))) _ >>>= fun X' => return _). apply FreshMon.
 472       simpl.
 473       unfold ξ'.
 474       unfold scbwv_ξ.
 475       simpl.
 476       admit.
 477
 478     apply ileaf in X'.
 479       simpl in X'.
 480       exists scb.
 481       unfold weakCK''.
 482       unfold ξ' in X'.
 483       apply X'.
 484     Defined.
 485
 486   Fixpoint treeM {T}(t:Tree ??(FreshM T)) : FreshM (Tree ??T) :=
 487     match t with
 488       | T_Leaf None     => return []
 489       | T_Leaf (Some x) => bind x' = x ; return [x']
 490       | T_Branch b1 b2  => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2')
 491     end.
 492
 493   Lemma itree_mapOptionTree : forall T T' F (f:T->T') t,
 494     ITree _ F (mapOptionTree f t) ->
 495     ITree _ (F ○ f) t.
 496     intros.
 497     induction t; try destruct a; simpl in *.
 498       apply ILeaf.
 499       inversion X; auto.
 500       apply INone.
 501       apply IBranch.
 502         apply IHt1; inversion X; auto.
 503         apply IHt2; inversion X; auto.
 504         Defined.
 505
 506   Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
 507
 508     intros h j r.
 509
 510       refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
 511       | RURule a b c d e              => let case_RURule := tt        in _
 512       | RNote   Γ Δ Σ τ l n           => let case_RNote := tt         in _
 513       | RLit    Γ Δ l     _           => let case_RLit := tt          in _
 514       | RVar    Γ Δ σ         p       => let case_RVar := tt          in _
 515       | RGlobal Γ Δ σ l wev           => let case_RGlobal := tt       in _
 516       | RLam    Γ Δ Σ tx te     x     => let case_RLam := tt          in _
 517       | RCast   Γ Δ Σ σ τ γ     x     => let case_RCast := tt         in _
 518       | RAbsT   Γ Δ Σ κ σ a           => let case_RAbsT := tt         in _
 519       | RAppT   Γ Δ Σ κ σ τ     y     => let case_RAppT := tt         in _
 520       | RAppCo  Γ Δ Σ κ σ₁ σ₂ γ σ l   => let case_RAppCo := tt        in _
 521       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
 522       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
 523       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _
 524       | RBindingGroup Γ p lri m x q   => let case_RBindingGroup := tt in _
 525       | REmptyGroup _ _               => let case_REmptyGroup := tt   in _
 526       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
 527       | REsc    Σ a b c n m           => let case_REsc := tt          in _
 528       | RCase   Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 529       | RLetRec Γ Δ lri x y t         => let case_RLetRec := tt       in _
 530       end); intro X_; try apply ileaf in X_; simpl in X_.
 531
 532   destruct case_RURule.
 533     destruct d; try destruct o.
 534       apply ILeaf; destruct u; simpl; intros.
 535       set (@urule2expr a b _ _ e ξ) as q.
 536       set (fun z => ileaf (q z)) as q'.
 537       simpl in q'.
 538       apply q' with (vars:=vars).
 539       clear q' q.
 540       apply bridge.
 541       apply X_.
 542       auto.
 543       apply no_urules_with_empty_conclusion in e; inversion e; auto.
 544       apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; auto.
 545
 546   destruct case_RBrak.
 547     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 548     apply EBrak.
 549     apply (ileaf X).
 550
 551   destruct case_REsc.
 552     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 553     apply EEsc.
 554     apply (ileaf X).
 555
 556   destruct case_RNote.
 557     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 558     apply ENote; auto.
 559     apply (ileaf X).
 560
 561   destruct case_RLit.
 562     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 563     apply ELit.
 564
 565   destruct case_RVar.
 566     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 567     destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
 568     apply EVar.
 569     inversion H.
 570
 571   destruct case_RGlobal.
 572     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 573     apply EGlobal.
 574     apply wev.
 575
 576   destruct case_RLam.
 577     apply ILeaf.
 578     simpl in *; intros.
 579     refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
 580     apply FreshMon.
 581     destruct pf as [ vnew [ pf1 pf2 ]].
 582     set (update_ξ ξ x ((⟨vnew, tx  ⟩) :: nil)) as ξ' in *.
 583     refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
 584     apply FreshMon.
 585     simpl.
 586     rewrite pf1.
 587     rewrite <- pf2.
 588     simpl.
 589     reflexivity.
 590     intro hyp.
 591     refine (return _).
 592     apply ILeaf.
 593     apply ELam with (ev:=vnew).
 594     apply ileaf in hyp.
 595     simpl in hyp.
 596     unfold ξ' in hyp.
 597     apply hyp.
 598
 599   destruct case_RCast.
 600     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 601     eapply ECast.
 602     apply x.
 603     apply ileaf in X. simpl in X.
 604     apply X.
 605
 606   destruct case_RBindingGroup.
 607     apply ILeaf; simpl; intros.
 608     inversion X_.
 609     apply ileaf in X.
 610     apply ileaf in X0.
 611     simpl in *.
 612     destruct vars; inversion H.
 613     destruct o; inversion H3.
 614     refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
 615     apply FreshMon.
 616     apply FreshMon.
 617     apply IBranch; auto.
 618
 619   destruct case_RApp.
 620     apply ILeaf.
 621     inversion X_.
 622     inversion X.
 623     inversion X0.
 624     simpl in *.
 625     intros.
 626     destruct vars. try destruct o; inversion H.
 627     simpl in H.
 628     inversion H.
 629     set (X1 ξ vars1 H5) as q1.
 630     set (X2 ξ vars2 H6) as q2.
 631     refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
 632     apply FreshMon.
 633     apply FreshMon.
 634     apply ILeaf.
 635     apply ileaf in q1'.
 636     apply ileaf in q2'.
 637     simpl in *.
 638     apply (EApp _ _ _ _ _ _ q1' q2').
 639
 640   destruct case_RLet.
 641     apply ILeaf.
 642     simpl in *; intros.
 643     destruct vars; try destruct o; inversion H.
 644     refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
 645     apply FreshMon.
 646     destruct pf as [ vnew [ pf1 pf2 ]].
 647     set (update_ξ ξ p ((⟨vnew, σ₂  ⟩) :: nil)) as ξ' in *.
 648     inversion X_.
 649     apply ileaf in X.
 650     apply ileaf in X0.
 651     simpl in *.
 652     refine (X0 ξ  vars2 _ >>>= fun X0' => _).
 653     apply FreshMon.
 654     auto.
 655     refine (X  ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
 656     apply FreshMon.
 657     rewrite H1.
 658     simpl.
 659     rewrite pf2.
 660     rewrite pf1.
 661     rewrite H1.
 662     reflexivity.
 663     refine (return _).
 664     apply ILeaf.
 665     apply ileaf in X0'.
 666     apply ileaf in X1'.
 667     simpl in *.
 668     apply ELet with (ev:=vnew)(tv:=σ₂).
 669     apply X0'.
 670     apply X1'.
 671
 672   destruct case_REmptyGroup.
 673     apply ILeaf; simpl; intros.
 674     refine (return _).
 675     apply INone.
 676
 677   destruct case_RAppT.
 678     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 679     apply ETyApp.
 680     apply (ileaf X).
 681
 682   destruct case_RAbsT.
 683     apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 684     rewrite mapOptionTree_compose.
 685     rewrite <- H.
 686     reflexivity.
 687     apply ileaf in X. simpl in *.
 688     apply ETyLam.
 689     apply X.
 690
 691   destruct case_RAppCo.
 692     apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 693     auto.
 694     eapply ECoApp.
 695     apply γ.
 696     apply (ileaf X).
 697
 698   destruct case_RAbsCo.
 699     apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 700     auto.
 701     eapply ECoLam.
 702     apply (ileaf X).
 703
 704   destruct case_RLetRec.
 705     apply ILeaf; simpl; intros.
 706     refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
 707     destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
 708     refine (X_ ((update_ξ ξ t (leaves varstypes)))
 709       (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_.  apply FreshMon.
 710     simpl.
 711     rewrite pf2.
 712     rewrite pf1.
 713     auto.
 714     apply ILeaf.
 715     inversion X; subst; clear X.
 716
 717     apply (@ELetRec _ _ _ _ _ _ _ varstypes).
 718     apply (@letrec_helper Γ Δ t varstypes).
 719     rewrite <- pf2 in X1.
 720     rewrite mapOptionTree_compose.
 721     apply X1.
 722     apply ileaf in X0.
 723     apply X0.
 724
 725   destruct case_RCase.
 726     apply ILeaf; simpl; intros.
 727     inversion X_.
 728     clear X_.
 729     subst.
 730     apply ileaf in X0.
 731     simpl in X0.
 732     set (mapOptionTreeAndFlatten pcb_freevars alts) as Σalts in *.
 733     refine (bind ξvars = fresh_lemma' _ (mapOptionTree unlev (Σalts,,Σ)) _ _ _ lev H ; _).
 734       apply FreshMon.
 735       destruct vars; try destruct o; inversion H; clear H.
 736       rename vars1 into varsalts.
 737       rename vars2 into varsΣ.
 738
 739     refine ( _ >>>= fun Y => X0 ξ varsΣ _ >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
 740       apply FreshMon.
 741       destruct ξvars as [varstypes [pf1 pf2]].
 742
 743       apply treeM.
 744       apply itree_mapOptionTree in X.
 745       refine (itree_to_tree (itmap _ X)).
 746       intros.
 747       eapply case_helper.
 748       apply X1.
 749       instantiate (1:=varsΣ).
 750       rewrite <- H2.
 751       admit.
 752       apply FreshMon.
 753     Defined.
 754
 755   Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
 756     refine ((
 757       fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
 758       match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
 759       | cnd_weak             => let case_nil    := tt in INone _ _
 760       | cnd_rule h c cnd' r  => let case_rule   := tt in rule2expr _ _ r (closed2expr' _ cnd')
 761       | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2)
 762       end)); clear closed2expr'; intros; subst.
 763         Defined.
 764
 765   Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
 766     FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
 767     intros Γ Σ.
 768     induction Σ; intro ξ.
 769     destruct a.
 770     destruct l as [τ l].
 771     set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
 772     refine (q >>>= fun q' => return _).
 773     apply FreshMon.
 774     clear q.
 775     destruct q' as [varstypes [pf1 [pf2 distpf]]].
 776     exists (mapOptionTree (@fst _ _) varstypes).
 777     exists (update_ξ ξ l (leaves varstypes)).
 778     symmetry; auto.
 779     refine (return _).
 780     exists [].
 781     exists ξ; auto.
 782     refine (bind f1 = IHΣ1 ξ ; _).
 783     apply FreshMon.
 784     destruct f1 as [vars1 [ξ1 pf1]].
 785     refine (bind f2 = IHΣ2 ξ1 ; _).
 786     apply FreshMon.
 787     destruct f2 as [vars2 [ξ2 pf22]].
 788     refine (return _).
 789     exists (vars1,,vars2).
 790     exists ξ2.
 791     simpl.
 792     rewrite pf22.
 793     rewrite pf1.
 794     admit.
 795     Defined.
 796
 797   Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
 798     {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
 799     FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
 800     intro pf.
 801     set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
 802     apply closed2expr in cnd.
 803     apply ileaf in cnd.
 804     simpl in *.
 805     clear pf.
 806     refine (bind ξvars = manyFresh _ Σ ξ0; _).
 807     apply FreshMon.
 808     destruct ξvars as [vars ξpf].
 809     destruct ξpf as [ξ pf].
 810     refine (cnd ξ vars _ >>>= fun it => _).
 811     apply FreshMon.
 812     auto.
 813     refine (return OK _).
 814     exists ξ.
 815     apply (ileaf it).
 816     Defined.
 817
 818 End HaskProofToStrong.