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