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