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 Γ ★) l1 l2 q,
  51     update_ξ ξ (app l1 l2) q = update_ξ (update_ξ ξ l2) 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 mapOptionTree_extensional {A}{B}(f g:A->B) : (forall a, f a = g a) -> (forall t, mapOptionTree f t = mapOptionTree g t).
  62     intros.
  63     induction t.
  64     destruct a; auto.
  65     simpl; rewrite H; auto.
  66     simpl; rewrite IHt1; rewrite IHt2; auto.
  67     Qed.
  68
  69    Lemma quark {T} (l1:list T) l2 vf :
  70       (In vf (app l1 l2)) <->
  71        (In vf l1) \/ (In vf l2).
  72      induction l1.
  73      simpl; auto.
  74      split; intro.
  75      right; auto.
  76      inversion H.
  77      inversion H0.
  78      auto.
  79      split.
  80
  81      destruct IHl1.
  82      simpl in *.
  83      intro.
  84      destruct H1.
  85      left; left; auto.
  86      set (H H1) as q.
  87      destruct q.
  88      left; right; auto.
  89      right; auto.
  90      simpl.
  91
  92      destruct IHl1.
  93      simpl in *.
  94      intro.
  95      destruct H1.
  96      destruct H1.
  97      left; auto.
  98      right; apply H0; auto.
  99      right; apply H0; auto.
 100    Qed.
 101
 102   Lemma splitter {T} (l1:list T) l2 vf :
 103       (In vf (app l1 l2) → False)
 104       -> (In vf l1 → False)  /\ (In vf l2 → False).
 105     intros.
 106     split; intros; apply H; rewrite quark.
 107     auto.
 108     auto.
 109     Qed.
 110
 111   Lemma helper
 112     : forall T Z {eqdt:EqDecidable T}(tl:Tree ??T)(vf:T) ξ (q:Z),
 113       (In vf (leaves tl) -> False) ->
 114       mapOptionTree (fun v' => if eqd_dec vf v' then q else ξ v') tl =
 115       mapOptionTree ξ tl.
 116     intros.
 117     induction tl;
 118       try destruct a;
 119         simpl in *.
 120     set (eqd_dec vf t) as x in *.
 121     destruct x.
 122     subst.
 123       assert False.
 124       apply H.
 125       left; auto.
 126       inversion H0.
 127     auto.
 128     auto.
 129     apply splitter in H.
 130     destruct H.
 131     rewrite (IHtl1 H).
 132     rewrite (IHtl2 H0).
 133     reflexivity.
 134     Qed.
 135
 136   Lemma fresh_lemma' Γ
 137     : forall types vars Σ ξ, Σ = mapOptionTree ξ vars ->
 138     FreshM { varstypes : _
 139       |  mapOptionTree (update_ξ(Γ:=Γ) ξ (leaves varstypes)) vars = Σ
 140       /\ mapOptionTree (update_ξ       ξ (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = types }.
 141     induction types.
 142       intros; destruct a.
 143         refine (bind vf = fresh (leaves vars) ; return _).
 144           apply FreshMon.
 145           destruct vf as [ vf vf_pf ].
 146           exists [(vf,l)].
 147           split; auto.
 148           simpl.
 149           set (helper VV _ vars vf ξ l vf_pf) as q.
 150           rewrite q.
 151           symmetry; auto.
 152           simpl.
 153           destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto.
 154         refine (return _).
 155           exists []; auto.
 156         intros vars Σ ξ pf; refine (bind x2 = IHtypes2 vars Σ ξ pf; _).
 157           apply FreshMon.
 158           destruct x2 as [vt2 [pf21 pf22]].
 159           refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,types2) (update_ξ ξ (leaves vt2)) _; return _).
 160           apply FreshMon.
 161           simpl.
 162           rewrite pf21.
 163           rewrite pf22.
 164           reflexivity.
 165           clear IHtypes1 IHtypes2.
 166           destruct x1 as [vt1 [pf11 pf12]].
 167           exists (vt1,,vt2); split; auto.
 168
 169           set (update_branches Γ ξ (leaves vt1) (leaves vt2)) as q.
 170           set (mapOptionTree_extensional _ _ q) as q'.
 171           rewrite q'.
 172           clear q' q.
 173           inversion pf11.
 174           reflexivity.
 175
 176           simpl.
 177           set (update_branches Γ ξ (leaves vt1) (leaves vt2)) as q.
 178           set (mapOptionTree_extensional _ _ q) as q'.
 179           rewrite q'.
 180           rewrite q'.
 181           clear q' q.
 182           rewrite <- mapOptionTree_compose.
 183           rewrite <- mapOptionTree_compose.
 184           rewrite <- mapOptionTree_compose in *.
 185           rewrite pf12.
 186           inversion pf11.
 187           rewrite <- mapOptionTree_compose.
 188           reflexivity.
 189         Defined.
 190
 191   Lemma fresh_lemma Γ ξ vars Σ Σ'
 192     : Σ = mapOptionTree ξ vars ->
 193     FreshM { vars' : _
 194       |  mapOptionTree (update_ξ(Γ:=Γ) ξ ((vars',Σ')::nil)) vars = Σ
 195       /\ mapOptionTree (update_ξ ξ ((vars',Σ')::nil)) [vars'] = [Σ'] }.
 196     intros.
 197     set (fresh_lemma' Γ [Σ'] vars Σ ξ H) as q.
 198     refine (q >>>= fun q' => return _).
 199     apply FreshMon.
 200     clear q.
 201     destruct q' as [varstypes [pf1 pf2]].
 202     destruct varstypes; try destruct o; try destruct p; simpl in *.
 203       destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
 204       inversion pf2; subst.
 205       exists v.
 206       destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
 207       split; auto.
 208       inversion pf2.
 209       inversion pf2.
 210     Defined.
 211
 212   Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
 213     FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
 214     intros.
 215     set (fresh_lemma' Γ Σ []  []  ξ0 (refl_equal _)) as q.
 216     refine (q >>>= fun q' => return _).
 217     apply FreshMon.
 218     clear q.
 219     destruct q' as [varstypes [pf1 pf2]].
 220     exists (mapOptionTree (@fst _ _) varstypes).
 221     exists (update_ξ ξ0 (leaves varstypes)).
 222     symmetry; auto.
 223     Defined.
 224
 225   Definition urule2expr  : forall Γ Δ h j (r:@URule Γ Δ h j) (ξ:VV -> LeveledHaskType Γ ★),
 226     ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j.
 227
 228       refine (fix urule2expr Γ Δ h j (r:@URule Γ Δ h j) ξ {struct r} :
 229         ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j :=
 230         match r as R in URule H C return ITree _ (ujudg2exprType ξ) H -> ITree _ (ujudg2exprType ξ) C with
 231           | RLeft   h c ctx r => let case_RLeft  := tt in (fun e => _) (urule2expr _ _ _ _ r)
 232           | RRight  h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r)
 233           | RCanL   t a       => let case_RCanL  := tt in _
 234           | RCanR   t a       => let case_RCanR  := tt in _
 235           | RuCanL  t a       => let case_RuCanL := tt in _
 236           | RuCanR  t a       => let case_RuCanR := tt in _
 237           | RAssoc  t a b c   => let case_RAssoc := tt in _
 238           | RCossa  t a b c   => let case_RCossa := tt in _
 239           | RExch   t a b     => let case_RExch  := tt in _
 240           | RWeak   t a       => let case_RWeak  := tt in _
 241           | RCont   t a       => let case_RCont  := tt in _
 242           end); clear urule2expr; intros.
 243
 244       destruct case_RCanL.
 245         apply ILeaf; simpl; intros.
 246         inversion X.
 247         simpl in X0.
 248         apply (X0 ([],,vars)).
 249         simpl; rewrite <- H; auto.
 250
 251       destruct case_RCanR.
 252         apply ILeaf; simpl; intros.
 253         inversion X.
 254         simpl in X0.
 255         apply (X0 (vars,,[])).
 256         simpl; rewrite <- H; auto.
 257
 258       destruct case_RuCanL.
 259         apply ILeaf; simpl; intros.
 260         destruct vars; try destruct o; inversion H.
 261         inversion X.
 262         simpl in X0.
 263         apply (X0 vars2); auto.
 264
 265       destruct case_RuCanR.
 266         apply ILeaf; simpl; intros.
 267         destruct vars; try destruct o; inversion H.
 268         inversion X.
 269         simpl in X0.
 270         apply (X0 vars1); auto.
 271
 272       destruct case_RAssoc.
 273         apply ILeaf; simpl; intros.
 274         inversion X.
 275         simpl in X0.
 276         destruct vars; try destruct o; inversion H.
 277         destruct vars1; try destruct o; inversion H.
 278         apply (X0 (vars1_1,,(vars1_2,,vars2))).
 279         subst; auto.
 280
 281       destruct case_RCossa.
 282         apply ILeaf; simpl; intros.
 283         inversion X.
 284         simpl in X0.
 285         destruct vars; try destruct o; inversion H.
 286         destruct vars2; try destruct o; inversion H.
 287         apply (X0 ((vars1,,vars2_1),,vars2_2)).
 288         subst; auto.
 289
 290       destruct case_RLeft.
 291         destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
 292         destruct o; [ idtac | apply INone ].
 293         destruct u; simpl in *.
 294         apply ILeaf; simpl; intros.
 295         destruct vars; try destruct o; inversion H.
 296         set (fun q => ileaf (e ξ q)) as r'.
 297         simpl in r'.
 298         apply r' with (vars:=vars2).
 299         clear r' e.
 300         clear r0.
 301         induction h0.
 302           destruct a.
 303           destruct u.
 304           simpl in X.
 305           apply ileaf in X.
 306           apply ILeaf.
 307           simpl.
 308           simpl in X.
 309           intros.
 310           apply X with (vars:=vars1,,vars).
 311           simpl.
 312           rewrite H0.
 313           rewrite H1.
 314           reflexivity.
 315           apply INone.
 316           apply IBranch.
 317           apply IHh0_1. inversion X; auto.
 318           apply IHh0_2. inversion X; auto.
 319           auto.
 320
 321       destruct case_RRight.
 322         destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
 323         destruct o; [ idtac | apply INone ].
 324         destruct u; simpl in *.
 325         apply ILeaf; simpl; intros.
 326         destruct vars; try destruct o; inversion H.
 327         set (fun q => ileaf (e ξ q)) as r'.
 328         simpl in r'.
 329         apply r' with (vars:=vars1).
 330         clear r' e.
 331         clear r0.
 332         induction h0.
 333           destruct a.
 334           destruct u.
 335           simpl in X.
 336           apply ileaf in X.
 337           apply ILeaf.
 338           simpl.
 339           simpl in X.
 340           intros.
 341           apply X with (vars:=vars,,vars2).
 342           simpl.
 343           rewrite H0.
 344           rewrite H2.
 345           reflexivity.
 346           apply INone.
 347           apply IBranch.
 348           apply IHh0_1. inversion X; auto.
 349           apply IHh0_2. inversion X; auto.
 350           auto.
 351
 352       destruct case_RExch.
 353         apply ILeaf; simpl; intros.
 354         inversion X.
 355         simpl in X0.
 356         destruct vars; try destruct o; inversion H.
 357         apply (X0 (vars2,,vars1)).
 358         inversion H; subst; auto.
 359
 360       destruct case_RWeak.
 361         apply ILeaf; simpl; intros.
 362         inversion X.
 363         simpl in X0.
 364         apply (X0 []).
 365         auto.
 366
 367       destruct case_RCont.
 368         apply ILeaf; simpl; intros.
 369         inversion X.
 370         simpl in X0.
 371         apply (X0 (vars,,vars)).
 372         simpl.
 373         rewrite <- H.
 374         auto.
 375         Defined.
 376
 377   Definition bridge Γ Δ (c:Tree ??(UJudg Γ Δ)) ξ :
 378     ITree Judg judg2exprType (mapOptionTree UJudg2judg c) -> ITree (UJudg Γ Δ) (ujudg2exprType ξ) c.
 379     intro it.
 380     induction c.
 381     destruct a.
 382       destruct u; simpl in *.
 383       apply ileaf in it.
 384       apply ILeaf.
 385       simpl in *.
 386       intros; apply it with (vars:=vars); auto.
 387     apply INone.
 388     apply IBranch; [ apply IHc1 | apply IHc2 ]; inversion it; auto.
 389     Defined.
 390
 391   Definition letrec_helper Γ Δ l varstypes ξ' :
 392     ITree (LeveledHaskType Γ ★)
 393          (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
 394          (mapOptionTree (ξ' ○ (@fst _ _)) varstypes)
 395          -> ELetRecBindings Γ Δ ξ' l
 396          (mapOptionTree (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) ⟩) varstypes).
 397     intros.
 398     induction varstypes.
 399     destruct a; simpl in *.
 400     destruct p.
 401     destruct l0 as [τ l'].
 402     simpl.
 403     apply ileaf in X. simpl in X.
 404     assert (unlev (ξ' v) = τ).
 405       admit.
 406       rewrite <- H.
 407       apply ELR_leaf.
 408       rewrite H.
 409       destruct (ξ' v).
 410       rewrite <- H.
 411       simpl.
 412       assert (h0=l). admit.
 413         rewrite H0 in X.
 414         apply X.
 415
 416     apply ELR_nil.
 417
 418     simpl; apply ELR_branch.
 419       apply IHvarstypes1.
 420       simpl in X.
 421       inversion X; auto.
 422       apply IHvarstypes2.
 423       simpl in X.
 424       inversion X; auto.
 425
 426     Defined.
 427
 428
 429 (*
 430   Definition case_helper tc Γ Δ lev tbranches avars ξ (Σ:Tree ??VV) tys :
 431     forall pcb : ProofCaseBranch tc Γ Δ lev tbranches avars,
 432   judg2exprType (pcb_judg pcb) -> FreshM
 433   {scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars &
 434     Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars (weakCK'' Δ))
 435     (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@  lev))}.
 436     intros.
 437     simpl in X.
 438     destruct pcb.
 439     simpl in *.
 440     refine (bind ξvars = fresh_lemma' Γ pcb_freevars Σ [] ξ _ ; _). apply FreshMon.
 441     destruct ξvars as [vars [ξ'
 442   Defined.
 443 *)
 444
 445   Lemma itree_mapOptionTree : forall T T' F (f:T->T') t,
 446     ITree _ F (mapOptionTree f t) ->
 447     ITree _ (F ○ f) t.
 448     intros.
 449     induction t; try destruct a; simpl in *.
 450       apply ILeaf.
 451       inversion X; auto.
 452       apply INone.
 453       apply IBranch.
 454         apply IHt1; inversion X; auto.
 455         apply IHt2; inversion X; auto.
 456         Defined.
 457
 458   Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
 459
 460     intros h j r.
 461
 462       refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
 463       | RURule a b c d e              => let case_RURule := tt        in _
 464       | RNote   Γ Δ Σ τ l n           => let case_RNote := tt         in _
 465       | RLit    Γ Δ l     _           => let case_RLit := tt          in _
 466       | RVar    Γ Δ σ         p       => let case_RVar := tt          in _
 467       | RGlobal Γ Δ σ l wev           => let case_RGlobal := tt       in _
 468       | RLam    Γ Δ Σ tx te     x     => let case_RLam := tt          in _
 469       | RCast   Γ Δ Σ σ τ γ     x     => let case_RCast := tt         in _
 470       | RAbsT   Γ Δ Σ κ σ a           => let case_RAbsT := tt         in _
 471       | RAppT   Γ Δ Σ κ σ τ     y     => let case_RAppT := tt         in _
 472       | RAppCo  Γ Δ Σ κ σ₁ σ₂ γ σ l   => let case_RAppCo := tt        in _
 473       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
 474       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
 475       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _
 476       | RBindingGroup Γ p lri m x q   => let case_RBindingGroup := tt in _
 477       | REmptyGroup _ _               => let case_REmptyGroup := tt   in _
 478       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
 479       | REsc    Σ a b c n m           => let case_REsc := tt          in _
 480       | RCase   Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 481       | RLetRec Γ Δ lri x y           => let case_RLetRec := tt       in _
 482       end); intro X_; try apply ileaf in X_; simpl in X_.
 483
 484   destruct case_RURule.
 485     destruct d; try destruct o.
 486       apply ILeaf; destruct u; simpl; intros.
 487       set (@urule2expr a b _ _ e ξ) as q.
 488       set (fun z => ileaf (q z)) as q'.
 489       simpl in q'.
 490       apply q' with (vars:=vars).
 491       clear q' q.
 492       apply bridge.
 493       apply X_.
 494       auto.
 495       apply no_urules_with_empty_conclusion in e; inversion e; auto.
 496       apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; auto.
 497
 498   destruct case_RBrak.
 499     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 500     apply EBrak.
 501     apply (ileaf X).
 502
 503   destruct case_REsc.
 504     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 505     apply EEsc.
 506     apply (ileaf X).
 507
 508   destruct case_RNote.
 509     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 510     apply ENote; auto.
 511     apply (ileaf X).
 512
 513   destruct case_RLit.
 514     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 515     apply ELit.
 516
 517   destruct case_RVar.
 518     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 519     destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
 520     apply EVar.
 521     inversion H.
 522
 523   destruct case_RGlobal.
 524     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 525     apply EGlobal.
 526     apply wev.
 527
 528   destruct case_RLam.
 529     apply ILeaf.
 530     simpl in *; intros.
 531     refine (fresh_lemma _ ξ vars _ (tx@@x) H >>>= (fun pf => _)).
 532     apply FreshMon.
 533     destruct pf as [ vnew [ pf1 pf2 ]].
 534     set (update_ξ ξ ((⟨vnew, tx @@  x ⟩) :: nil)) as ξ' in *.
 535     refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
 536     apply FreshMon.
 537     simpl.
 538     rewrite pf1.
 539     rewrite <- pf2.
 540     simpl.
 541     reflexivity.
 542     intro hyp.
 543     refine (return _).
 544     apply ILeaf.
 545     apply ELam with (ev:=vnew).
 546     apply ileaf in hyp.
 547     simpl in hyp.
 548     unfold ξ' in hyp.
 549     apply hyp.
 550
 551   destruct case_RCast.
 552     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 553     eapply ECast.
 554     apply x.
 555     apply ileaf in X. simpl in X.
 556     apply X.
 557
 558   destruct case_RBindingGroup.
 559     apply ILeaf; simpl; intros.
 560     inversion X_.
 561     apply ileaf in X.
 562     apply ileaf in X0.
 563     simpl in *.
 564     destruct vars; inversion H.
 565     destruct o; inversion H3.
 566     refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
 567     apply FreshMon.
 568     apply FreshMon.
 569     apply IBranch; auto.
 570
 571   destruct case_RApp.
 572     apply ILeaf.
 573     inversion X_.
 574     inversion X.
 575     inversion X0.
 576     simpl in *.
 577     intros.
 578     destruct vars. try destruct o; inversion H.
 579     simpl in H.
 580     inversion H.
 581     set (X1 ξ vars1 H5) as q1.
 582     set (X2 ξ vars2 H6) as q2.
 583     refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
 584     apply FreshMon.
 585     apply FreshMon.
 586     apply ILeaf.
 587     apply ileaf in q1'.
 588     apply ileaf in q2'.
 589     simpl in *.
 590     apply (EApp _ _ _ _ _ _ q1' q2').
 591
 592   destruct case_RLet.
 593     apply ILeaf.
 594     simpl in *; intros.
 595     destruct vars; try destruct o; inversion H.
 596     refine (fresh_lemma _ ξ vars1 _ (σ₂@@p) H1 >>>= (fun pf => _)).
 597     apply FreshMon.
 598     destruct pf as [ vnew [ pf1 pf2 ]].
 599     set (update_ξ ξ ((⟨vnew, σ₂ @@  p ⟩) :: nil)) as ξ' in *.
 600     inversion X_.
 601     apply ileaf in X.
 602     apply ileaf in X0.
 603     simpl in *.
 604     refine (X0 ξ  vars2 _ >>>= fun X0' => _).
 605     apply FreshMon.
 606     auto.
 607     refine (X  ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
 608     apply FreshMon.
 609     rewrite H1.
 610     simpl.
 611     rewrite pf2.
 612     rewrite pf1.
 613     rewrite H1.
 614     reflexivity.
 615     refine (return _).
 616     apply ILeaf.
 617     apply ileaf in X0'.
 618     apply ileaf in X1'.
 619     simpl in *.
 620     apply ELet with (ev:=vnew)(tv:=σ₂).
 621     apply X0'.
 622     apply X1'.
 623
 624   destruct case_REmptyGroup.
 625     apply ILeaf; simpl; intros.
 626     refine (return _).
 627     apply INone.
 628
 629   destruct case_RAppT.
 630     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 631     apply ETyApp.
 632     apply (ileaf X).
 633
 634   destruct case_RAbsT.
 635     apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 636     rewrite mapOptionTree_compose.
 637     rewrite <- H.
 638     reflexivity.
 639     apply ileaf in X. simpl in *.
 640     apply ETyLam.
 641     apply X.
 642
 643   destruct case_RAppCo.
 644     apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 645     auto.
 646     eapply ECoApp.
 647     apply γ.
 648     apply (ileaf X).
 649
 650   destruct case_RAbsCo.
 651     apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 652     auto.
 653     eapply ECoLam.
 654     apply (ileaf X).
 655
 656   destruct case_RLetRec.
 657     apply ILeaf; simpl; intros.
 658     refine (bind ξvars = fresh_lemma' _ y _ _ _ H; _). apply FreshMon.
 659     destruct ξvars as [ varstypes [ pf1 pf2 ]].
 660     refine (X_ ((update_ξ ξ (leaves varstypes)))
 661       (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_.  apply FreshMon.
 662     simpl.
 663     rewrite pf2.
 664     rewrite pf1.
 665     auto.
 666     apply ILeaf.
 667     destruct x as [τ l].
 668     inversion X; subst; clear X.
 669
 670     (* getting rid of this will require strengthening RLetRec *)
 671     assert ((mapOptionTree (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) @@  l ⟩) varstypes) = varstypes) as HHH.
 672       admit.
 673
 674     apply (@ELetRec _ _ _ _ _ _ _ (mapOptionTree (fun x => ((fst x),unlev (snd x))) varstypes));
 675       rewrite mapleaves; rewrite <- map_compose; simpl;
 676       [ idtac
 677       | rewrite <- mapleaves; rewrite HHH; apply (ileaf X0) ].
 678
 679     clear X0.
 680     rewrite <- mapOptionTree_compose in X1.
 681     set (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) @@  l ⟩) as ξ' in *.
 682     rewrite <- mapleaves.
 683     rewrite HHH.
 684
 685     apply (letrec_helper _ _ _ _ _ X1).
 686
 687   destruct case_RCase.
 688   apply ILeaf.
 689 simpl.
 690 intros.
 691 apply (Prelude_error "FIXME").
 692
 693
 694 (*
 695     apply ILeaf; simpl; intros.
 696     inversion X_.
 697     clear X_.
 698     subst.
 699     apply ileaf in X0.
 700     simpl in X0.
 701     set (mapOptionTreeAndFlatten pcb_freevars alts) as Σalts in *.
 702     refine (bind ξvars = fresh_lemma' _ (Σalts,,Σ) _ _ _ H ; _).
 703       apply FreshMon.
 704       destruct vars; try destruct o; inversion H; clear H.
 705       rename vars1 into varsalts.
 706       rename vars2 into varsΣ.
 707
 708     refine (X0 ξ varsΣ _ >>>= fun X => return ILeaf _ _); auto. apply FreshMon.
 709       clear X0.
 710       eapply (ECase _ _ _ _ _ _ _ (ileaf X1)).
 711       clear X1.
 712
 713       destruct ξvars as [varstypes [pf1 pf2]].
 714
 715       apply itree_mapOptionTree in X.
 716       refine (itree_to_tree (itmap _ X)).
 717       apply case_helper.
 718 *)
 719     Defined.
 720
 721   Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
 722     refine ((
 723       fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
 724       match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
 725       | cnd_weak             => let case_nil    := tt in INone _ _
 726       | cnd_rule h c cnd' r  => let case_rule   := tt in rule2expr _ _ r (closed2expr' _ cnd')
 727       | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2)
 728       end)); clear closed2expr'; intros; subst.
 729         Defined.
 730
 731   Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
 732     {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
 733     FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
 734     intro pf.
 735     set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
 736     apply closed2expr in cnd.
 737     apply ileaf in cnd.
 738     simpl in *.
 739     clear pf.
 740     refine (bind ξvars = manyFresh _ Σ ξ0; _).
 741     apply FreshMon.
 742     destruct ξvars as [vars ξpf].
 743     destruct ξpf as [ξ pf].
 744     refine (cnd ξ vars _ >>>= fun it => _).
 745     apply FreshMon.
 746     auto.
 747     refine (return OK _).
 748     exists ξ.
 749     apply (ileaf it).
 750     Defined.
 751
 752 End HaskProofToStrong.