src/HaskProofToStrong.v

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