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       (Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
  31         FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
  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_ξ ξ lev (app l1 l2) q = update_ξ (update_ξ ξ 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_ξ(Γ:=Γ)   ξ 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_ξ(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
 134       /\ mapOptionTree (update_ξ       ξ 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_ξ ξ 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_ξ(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
 208       /\ mapOptionTree (update_ξ ξ 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 Γ) Σ τ : Type :=
 226     forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ).
 227
 228   Definition urule2expr  : forall Γ Δ h j t (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
 229     ujudg2exprType Γ ξ Δ h t ->
 230     ujudg2exprType Γ ξ Δ j t
 231     .
 232     intros Γ Δ.
 233       refine (fix urule2expr h j t (r:@Arrange _ h j) ξ {struct r} :
 234     ujudg2exprType Γ ξ Δ h t ->
 235     ujudg2exprType Γ ξ Δ j t :=
 236         match r as R in Arrange H C return
 237     ujudg2exprType Γ ξ Δ H t ->
 238     ujudg2exprType Γ ξ Δ C t
 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 (LeveledHaskType Γ ★)
 357          (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
 358          (mapOptionTree (ξ' ○ (@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         apply X.
 375       apply (Prelude_error "level mismatch; should never happen").
 376       apply (Prelude_error "letrec type mismatch; should never happen").
 377
 378     apply ELR_nil.
 379     apply ELR_branch.
 380       apply IHvarstypes1; inversion X; auto.
 381       apply IHvarstypes2; inversion X; auto.
 382     Defined.
 383
 384   Definition unindex_tree {V}{F} : forall {t:Tree ??V}, ITree V F t -> Tree ??{ v:V & F v }.
 385     refine (fix rec t it := match it as IT return Tree ??{ v:V & F v } with
 386       | INone => T_Leaf None
 387       | ILeaf x y => T_Leaf (Some _)
 388       | IBranch _ _ b1 b2 => (rec _ b1),,(rec _ b2)
 389             end).
 390     exists x; auto.
 391     Defined.
 392
 393   Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x })
 394     :  ITree { x:X & F x } (fun x => J (projT1 x))                                t
 395     -> ITree X             (fun x:X => J x)   (mapOptionTree (@projT1 _ _) t).
 396     intro it.
 397     induction it; simpl in *.
 398     apply INone.
 399     apply ILeaf.
 400     apply f.
 401     simpl; apply IBranch; auto.
 402     Defined.
 403
 404   Definition fix2 {X}{F} : Tree ??{ x:X & FreshM (F x) } -> Tree ??(FreshM { x:X & F x }).
 405     refine (fix rec t := match t with
 406       | T_Leaf None => T_Leaf None
 407       | T_Leaf (Some x) => T_Leaf (Some _)
 408       | T_Branch b1 b2 => T_Branch (rec b1) (rec b2)
 409             end).
 410     destruct x as [x fx].
 411     refine (bind fx' = fx ; return _).
 412     apply FreshMon.
 413     exists x.
 414     apply fx'.
 415     Defined.
 416
 417   Definition case_helper tc Γ Δ lev tbranches avars ξ :
 418     forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac},
 419      prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
 420      ((fun sac => FreshM
 421        { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
 422          & Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars (weakCK'' Δ)) (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@  lev)) }) (projT1 pcb)).
 423     intro pcb.
 424     intro X.
 425     simpl in X.
 426     simpl.
 427     destruct pcb as [sac pcb].
 428     simpl in *.
 429
 430     destruct X.
 431     destruct s as [vars vars_pf].
 432
 433     refine (bind localvars = fresh_lemma' _ (unleaves  (vec2list (sac_types sac _ avars))) vars
 434       (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _  ; _).
 435       apply FreshMon.
 436       rewrite vars_pf.
 437       rewrite <- mapOptionTree_compose.
 438       reflexivity.
 439       destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]].
 440       set (mapOptionTree (@fst _ _) localvars) as localvars'.
 441
 442     set (list2vec (leaves localvars')) as localvars''.
 443     cut (length (leaves localvars') = sac_numExprVars sac). intro H''.
 444       rewrite H'' in localvars''.
 445     cut (distinct (vec2list localvars'')). intro H'''.
 446     set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
 447
 448     refine (bind q = (f (scbwv_ξ scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
 449       apply FreshMon.
 450       simpl.
 451       unfold scbwv_ξ.
 452       rewrite vars_pf.
 453       rewrite <- mapOptionTree_compose.
 454       clear localvars_pf1.
 455       simpl.
 456       rewrite mapleaves'.
 457
 458     admit.
 459
 460     exists scb.
 461     apply ileaf in q.
 462     apply q.
 463
 464     admit.
 465     admit.
 466     Defined.
 467
 468   Definition gather_branch_variables
 469     Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
 470                 ProofCaseBranch tc Γ Δ lev tbranches avars sac})
 471     :
 472     forall vars,
 473     mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
 474     -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
 475     -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q)))
 476       { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
 477   alts.
 478     induction alts;
 479     intro vars;
 480     intro pf;
 481     intro source.
 482     destruct a; [ idtac | apply INone ].
 483     simpl in *.
 484     apply ileaf in source.
 485     apply ILeaf.
 486     destruct s as [sac pcb].
 487     simpl in *.
 488     split.
 489     intros.
 490     eapply source.
 491     apply H.
 492     clear source.
 493
 494     exists vars.
 495     auto.
 496
 497     simpl in pf.
 498     destruct vars; try destruct o; simpl in pf; inversion pf.
 499     simpl in source.
 500     inversion source.
 501     subst.
 502     apply IBranch.
 503     apply (IHalts1 vars1 H0 X); auto.
 504     apply (IHalts2 vars2 H1 X0); auto.
 505
 506     Defined.
 507
 508
 509   Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
 510
 511     intros h j r.
 512
 513       refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
 514       | RArrange a b c d e  r         => let case_RURule := tt        in _
 515       | RNote   Γ Δ Σ τ l n           => let case_RNote := tt         in _
 516       | RLit    Γ Δ l     _           => let case_RLit := tt          in _
 517       | RVar    Γ Δ σ         p       => let case_RVar := tt          in _
 518       | RGlobal Γ Δ σ l wev           => let case_RGlobal := tt       in _
 519       | RLam    Γ Δ Σ tx te     x     => let case_RLam := tt          in _
 520       | RCast   Γ Δ Σ σ τ γ     x     => let case_RCast := tt         in _
 521       | RAbsT   Γ Δ Σ κ σ a           => let case_RAbsT := tt         in _
 522       | RAppT   Γ Δ Σ κ σ τ     y     => let case_RAppT := tt         in _
 523       | RAppCo  Γ Δ Σ κ σ₁ σ₂ γ σ l   => let case_RAppCo := tt        in _
 524       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
 525       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
 526       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _
 527       | RJoin Γ p lri m x q   => let case_RJoin := tt in _
 528       | RVoid _ _               => let case_RVoid := tt   in _
 529       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
 530       | REsc    Σ a b c n m           => let case_REsc := tt          in _
 531       | RCase   Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 532       | RLetRec Γ Δ lri x y t         => let case_RLetRec := tt       in _
 533       end); intro X_; try apply ileaf in X_; simpl in X_.
 534
 535     destruct case_RURule.
 536       apply ILeaf. simpl. intros.
 537       set (@urule2expr a b _ _ e r0 ξ) as q.
 538       set (fun z => q z) as q'.
 539       simpl in q'.
 540       apply q' with (vars:=vars).
 541       clear q' q.
 542       unfold ujudg2exprType.
 543       intros.
 544       apply X_ with (vars:=vars0).
 545       auto.
 546       auto.
 547
 548   destruct case_RBrak.
 549     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 550     apply EBrak.
 551     apply (ileaf X).
 552
 553   destruct case_REsc.
 554     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 555     apply EEsc.
 556     apply (ileaf X).
 557
 558   destruct case_RNote.
 559     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 560     apply ENote; auto.
 561     apply (ileaf X).
 562
 563   destruct case_RLit.
 564     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 565     apply ELit.
 566
 567   destruct case_RVar.
 568     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 569     destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
 570     apply EVar.
 571     inversion H.
 572
 573   destruct case_RGlobal.
 574     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 575     apply EGlobal.
 576
 577   destruct case_RLam.
 578     apply ILeaf.
 579     simpl in *; intros.
 580     refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
 581     apply FreshMon.
 582     destruct pf as [ vnew [ pf1 pf2 ]].
 583     set (update_ξ ξ x (((vnew, tx  )) :: nil)) as ξ' in *.
 584     refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
 585     apply FreshMon.
 586     simpl.
 587     rewrite pf1.
 588     rewrite <- pf2.
 589     simpl.
 590     reflexivity.
 591     intro hyp.
 592     refine (return _).
 593     apply ILeaf.
 594     apply ELam with (ev:=vnew).
 595     apply ileaf in hyp.
 596     simpl in hyp.
 597     unfold ξ' in hyp.
 598     apply hyp.
 599
 600   destruct case_RCast.
 601     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 602     eapply ECast.
 603     apply x.
 604     apply ileaf in X. simpl in X.
 605     apply X.
 606
 607   destruct case_RJoin.
 608     apply ILeaf; simpl; intros.
 609     inversion X_.
 610     apply ileaf in X.
 611     apply ileaf in X0.
 612     simpl in *.
 613     destruct vars; inversion H.
 614     destruct o; inversion H3.
 615     refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
 616     apply FreshMon.
 617     apply FreshMon.
 618     apply IBranch; auto.
 619
 620   destruct case_RApp.
 621     apply ILeaf.
 622     inversion X_.
 623     inversion X.
 624     inversion X0.
 625     simpl in *.
 626     intros.
 627     destruct vars. try destruct o; inversion H.
 628     simpl in H.
 629     inversion H.
 630     set (X1 ξ vars1 H5) as q1.
 631     set (X2 ξ vars2 H6) as q2.
 632     refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
 633     apply FreshMon.
 634     apply FreshMon.
 635     apply ILeaf.
 636     apply ileaf in q1'.
 637     apply ileaf in q2'.
 638     simpl in *.
 639     apply (EApp _ _ _ _ _ _ q2' q1').
 640
 641   destruct case_RLet.
 642     apply ILeaf.
 643     simpl in *; intros.
 644     destruct vars; try destruct o; inversion H.
 645     refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
 646     apply FreshMon.
 647     destruct pf as [ vnew [ pf1 pf2 ]].
 648     set (update_ξ ξ p (((vnew, σ₂ )) :: nil)) as ξ' in *.
 649     inversion X_.
 650     apply ileaf in X.
 651     apply ileaf in X0.
 652     simpl in *.
 653     refine (X ξ  vars2 _ >>>= fun X0' => _).
 654     apply FreshMon.
 655     auto.
 656
 657     refine (X0 ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
 658     apply FreshMon.
 659     rewrite H1.
 660     simpl.
 661     rewrite pf2.
 662     rewrite pf1.
 663     rewrite H1.
 664     reflexivity.
 665
 666     refine (return _).
 667     apply ILeaf.
 668     apply ileaf in X0'.
 669     apply ileaf in X1'.
 670     simpl in *.
 671     apply ELet with (ev:=vnew)(tv:=σ₂).
 672     apply X0'.
 673     apply X1'.
 674
 675   destruct case_RVoid.
 676     apply ILeaf; simpl; intros.
 677     refine (return _).
 678     apply INone.
 679
 680   destruct case_RAppT.
 681     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 682     apply ETyApp.
 683     apply (ileaf X).
 684
 685   destruct case_RAbsT.
 686     apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 687     rewrite mapOptionTree_compose.
 688     rewrite <- H.
 689     reflexivity.
 690     apply ileaf in X. simpl in *.
 691     apply ETyLam.
 692     apply X.
 693
 694   destruct case_RAppCo.
 695     apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 696     auto.
 697     eapply ECoApp.
 698     apply γ.
 699     apply (ileaf X).
 700
 701   destruct case_RAbsCo.
 702     apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 703     auto.
 704     eapply ECoLam.
 705     apply (ileaf X).
 706
 707   destruct case_RLetRec.
 708     apply ILeaf; simpl; intros.
 709     refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
 710     destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
 711     refine (X_ ((update_ξ ξ t (leaves varstypes)))
 712       (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_.  apply FreshMon.
 713     simpl.
 714     rewrite pf2.
 715     rewrite pf1.
 716     auto.
 717     apply ILeaf.
 718     inversion X; subst; clear X.
 719
 720     apply (@ELetRec _ _ _ _ _ _ _ varstypes).
 721     auto.
 722     apply (@letrec_helper Γ Δ t varstypes).
 723     rewrite <- pf2 in X1.
 724     rewrite mapOptionTree_compose.
 725     apply X1.
 726     apply ileaf in X0.
 727     apply X0.
 728
 729   destruct case_RCase.
 730     apply ILeaf; simpl; intros.
 731     inversion X_.
 732     clear X_.
 733     subst.
 734     apply ileaf in X0.
 735     simpl in X0.
 736
 737     (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
 738      * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
 739     rename Σ into body_freevars_types.
 740     rename vars into all_freevars.
 741     rename X0 into body_expr.
 742     rename X  into alts_exprs.
 743
 744     destruct all_freevars; try destruct o; inversion H.
 745     rename all_freevars2 into body_freevars.
 746     rename all_freevars1 into alts_freevars.
 747
 748     set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
 749     set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
 750     apply fix_indexing in alts_exprs'.
 751     simpl in alts_exprs'.
 752     apply unindex_tree in alts_exprs'.
 753     simpl in alts_exprs'.
 754     apply fix2 in alts_exprs'.
 755     apply treeM in alts_exprs'.
 756
 757     refine ( alts_exprs' >>>= fun Y =>
 758       body_expr ξ _ _
 759       >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
 760       apply FreshMon.
 761       apply FreshMon.
 762       apply H2.
 763     Defined.
 764
 765   Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
 766     match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
 767     | scnd_weak   _             => let case_nil    := tt in fun _ => INone _ _
 768     | scnd_comp   x h c cnd' r  => let case_rule   := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
 769     | scnd_branch _ _ _ c1 c2   => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
 770     end.
 771
 772   Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
 773     FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
 774     intros Γ Σ.
 775     induction Σ; intro ξ.
 776     destruct a.
 777     destruct l as [τ l].
 778     set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
 779     refine (q >>>= fun q' => return _).
 780     apply FreshMon.
 781     clear q.
 782     destruct q' as [varstypes [pf1 [pf2 distpf]]].
 783     exists (mapOptionTree (@fst _ _) varstypes).
 784     exists (update_ξ ξ l (leaves varstypes)).
 785     symmetry; auto.
 786     refine (return _).
 787     exists [].
 788     exists ξ; auto.
 789     refine (bind f1 = IHΣ1 ξ ; _).
 790     apply FreshMon.
 791     destruct f1 as [vars1 [ξ1 pf1]].
 792     refine (bind f2 = IHΣ2 ξ1 ; _).
 793     apply FreshMon.
 794     destruct f2 as [vars2 [ξ2 pf22]].
 795     refine (return _).
 796     exists (vars1,,vars2).
 797     exists ξ2.
 798     simpl.
 799     rewrite pf22.
 800     rewrite pf1.
 801     admit.
 802     Defined.
 803
 804   Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
 805     {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
 806     FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
 807     intro pf.
 808     set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
 809     apply closed2expr in cnd.
 810     apply ileaf in cnd.
 811     simpl in *.
 812     clear pf.
 813     refine (bind ξvars = manyFresh _ Σ ξ0; _).
 814     apply FreshMon.
 815     destruct ξvars as [vars ξpf].
 816     destruct ξpf as [ξ pf].
 817     refine (cnd ξ vars _ >>>= fun it => _).
 818     apply FreshMon.
 819     auto.
 820     refine (return OK _).
 821     exists ξ.
 822     apply (ileaf it).
 823     apply INone.
 824     Defined.
 825
 826 End HaskProofToStrong.