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