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