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     destruct (eqd_dec (unlev (ξ' v)) τ).
 405       rewrite <- e.
 406       apply ELR_leaf.
 407       destruct (ξ' v).
 408       simpl.
 409       destruct (eqd_dec h0 l).
 410         rewrite <- e0.
 411         apply X.
 412     apply (Prelude_error "level mismatch; should never happen").
 413     apply (Prelude_error "letrec type mismatch; should never happen").
 414
 415     apply ELR_nil.
 416
 417     simpl; apply ELR_branch.
 418       apply IHvarstypes1.
 419       simpl in X.
 420       inversion X; auto.
 421       apply IHvarstypes2.
 422       simpl in X.
 423       inversion X; auto.
 424
 425     Defined.
 426
 427   Lemma leaves_unleaves {T}(t:list T) : leaves (unleaves t) = t.
 428     induction t; auto.
 429     simpl.
 430     rewrite IHt; auto.
 431     Qed.
 432
 433   Definition case_helper tc Γ Δ lev tbranches avars ξ (Σ:Tree ??VV) :
 434     forall pcb : ProofCaseBranch tc Γ Δ lev tbranches avars,
 435   judg2exprType (pcb_judg pcb) ->
 436   (pcb_freevars pcb) = mapOptionTree ξ Σ ->
 437   FreshM
 438   {scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars &
 439     Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars (weakCK'' Δ))
 440     (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@  lev))}.
 441     intros.
 442     simpl in X.
 443     destruct pcb.
 444     simpl in *.
 445     set (sac_types pcb_scb _ avars) as boundvars.
 446     refine (fresh_lemma' _ (unleaves (map (fun x => x@@(weakL' lev)) (vec2list boundvars))) Σ
 447       (mapOptionTree weakLT' pcb_freevars)
 448         (weakLT' ○ ξ) _
 449       >>>= fun ξvars => _). apply FreshMon.
 450     rewrite H.
 451     rewrite <- mapOptionTree_compose.
 452     reflexivity.
 453       destruct ξvars as [ exprvars [pf1 pf2 ]].
 454       set (list2vec (leaves (mapOptionTree (@fst _ _) exprvars))) as exprvars'.
 455       assert (sac_numExprVars pcb_scb = Datatypes.length (leaves (mapOptionTree (@fst _ _) exprvars))) as H'.
 456         rewrite <- mapOptionTree_compose in pf2.
 457         simpl in pf2.
 458         rewrite mapleaves.
 459         rewrite <- map_preserves_length.
 460         rewrite map_preserves_length with (f:=update_ξ (weakLT' ○ ξ) (leaves exprvars) ○ (@fst _ _)).
 461         rewrite <- mapleaves.
 462         rewrite pf2.
 463         rewrite leaves_unleaves.
 464         rewrite vec2list_map_list2vec.
 465         rewrite vec2list_len.
 466         reflexivity.
 467       rewrite <- H' in exprvars'.
 468         clear H'.
 469
 470     set (@Build_StrongCaseBranchWithVVs VV _ tc _ avars pcb_scb exprvars') as scb.
 471     set (scbwv_ξ scb ξ lev) as ξ'.
 472     refine (X ξ' (Σ,,(unleaves (vec2list exprvars'))) _ >>>= fun X' => return _). apply FreshMon.
 473       simpl.
 474       unfold ξ'.
 475       unfold scbwv_ξ.
 476       simpl.
 477       rewrite <- vec2list_map_list2vec.
 478       rewrite <- pf1.
 479       admit.
 480
 481     apply ileaf in X'.
 482       simpl in X'.
 483       exists scb.
 484       unfold weakCK''.
 485       unfold ξ' in X'.
 486       apply X'.
 487     Defined.
 488
 489   Fixpoint treeM {T}(t:Tree ??(FreshM T)) : FreshM (Tree ??T) :=
 490     match t with
 491       | T_Leaf None     => return []
 492       | T_Leaf (Some x) => bind x' = x ; return [x']
 493       | T_Branch b1 b2  => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2')
 494     end.
 495
 496   Lemma itree_mapOptionTree : forall T T' F (f:T->T') t,
 497     ITree _ F (mapOptionTree f t) ->
 498     ITree _ (F ○ f) t.
 499     intros.
 500     induction t; try destruct a; simpl in *.
 501       apply ILeaf.
 502       inversion X; auto.
 503       apply INone.
 504       apply IBranch.
 505         apply IHt1; inversion X; auto.
 506         apply IHt2; inversion X; auto.
 507         Defined.
 508
 509   Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
 510
 511     intros h j r.
 512
 513       refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
 514       | RURule a b c d e              => let case_RURule := tt        in _
 515       | RNote   Γ Δ Σ τ l n           => let case_RNote := tt         in _
 516       | RLit    Γ Δ l     _           => let case_RLit := tt          in _
 517       | RVar    Γ Δ σ         p       => let case_RVar := tt          in _
 518       | RGlobal Γ Δ σ l wev           => let case_RGlobal := tt       in _
 519       | RLam    Γ Δ Σ tx te     x     => let case_RLam := tt          in _
 520       | RCast   Γ Δ Σ σ τ γ     x     => let case_RCast := tt         in _
 521       | RAbsT   Γ Δ Σ κ σ a           => let case_RAbsT := tt         in _
 522       | RAppT   Γ Δ Σ κ σ τ     y     => let case_RAppT := tt         in _
 523       | RAppCo  Γ Δ Σ κ σ₁ σ₂ γ σ l   => let case_RAppCo := tt        in _
 524       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
 525       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
 526       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _
 527       | RBindingGroup Γ p lri m x q   => let case_RBindingGroup := tt in _
 528       | REmptyGroup _ _               => let case_REmptyGroup := tt   in _
 529       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
 530       | REsc    Σ a b c n m           => let case_REsc := tt          in _
 531       | RCase   Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 532       | RLetRec Γ Δ lri x y           => let case_RLetRec := tt       in _
 533       end); intro X_; try apply ileaf in X_; simpl in X_.
 534
 535   destruct case_RURule.
 536     destruct d; try destruct o.
 537       apply ILeaf; destruct u; simpl; intros.
 538       set (@urule2expr a b _ _ e ξ) as q.
 539       set (fun z => ileaf (q z)) as q'.
 540       simpl in q'.
 541       apply q' with (vars:=vars).
 542       clear q' q.
 543       apply bridge.
 544       apply X_.
 545       auto.
 546       apply no_urules_with_empty_conclusion in e; inversion e; auto.
 547       apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; auto.
 548
 549   destruct case_RBrak.
 550     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 551     apply EBrak.
 552     apply (ileaf X).
 553
 554   destruct case_REsc.
 555     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 556     apply EEsc.
 557     apply (ileaf X).
 558
 559   destruct case_RNote.
 560     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 561     apply ENote; auto.
 562     apply (ileaf X).
 563
 564   destruct case_RLit.
 565     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 566     apply ELit.
 567
 568   destruct case_RVar.
 569     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 570     destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
 571     apply EVar.
 572     inversion H.
 573
 574   destruct case_RGlobal.
 575     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 576     apply EGlobal.
 577     apply wev.
 578
 579   destruct case_RLam.
 580     apply ILeaf.
 581     simpl in *; intros.
 582     refine (fresh_lemma _ ξ vars _ (tx@@x) H >>>= (fun pf => _)).
 583     apply FreshMon.
 584     destruct pf as [ vnew [ pf1 pf2 ]].
 585     set (update_ξ ξ ((⟨vnew, tx @@  x ⟩) :: nil)) as ξ' in *.
 586     refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
 587     apply FreshMon.
 588     simpl.
 589     rewrite pf1.
 590     rewrite <- pf2.
 591     simpl.
 592     reflexivity.
 593     intro hyp.
 594     refine (return _).
 595     apply ILeaf.
 596     apply ELam with (ev:=vnew).
 597     apply ileaf in hyp.
 598     simpl in hyp.
 599     unfold ξ' in hyp.
 600     apply hyp.
 601
 602   destruct case_RCast.
 603     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 604     eapply ECast.
 605     apply x.
 606     apply ileaf in X. simpl in X.
 607     apply X.
 608
 609   destruct case_RBindingGroup.
 610     apply ILeaf; simpl; intros.
 611     inversion X_.
 612     apply ileaf in X.
 613     apply ileaf in X0.
 614     simpl in *.
 615     destruct vars; inversion H.
 616     destruct o; inversion H3.
 617     refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
 618     apply FreshMon.
 619     apply FreshMon.
 620     apply IBranch; auto.
 621
 622   destruct case_RApp.
 623     apply ILeaf.
 624     inversion X_.
 625     inversion X.
 626     inversion X0.
 627     simpl in *.
 628     intros.
 629     destruct vars. try destruct o; inversion H.
 630     simpl in H.
 631     inversion H.
 632     set (X1 ξ vars1 H5) as q1.
 633     set (X2 ξ vars2 H6) as q2.
 634     refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
 635     apply FreshMon.
 636     apply FreshMon.
 637     apply ILeaf.
 638     apply ileaf in q1'.
 639     apply ileaf in q2'.
 640     simpl in *.
 641     apply (EApp _ _ _ _ _ _ q1' q2').
 642
 643   destruct case_RLet.
 644     apply ILeaf.
 645     simpl in *; intros.
 646     destruct vars; try destruct o; inversion H.
 647     refine (fresh_lemma _ ξ vars1 _ (σ₂@@p) H1 >>>= (fun pf => _)).
 648     apply FreshMon.
 649     destruct pf as [ vnew [ pf1 pf2 ]].
 650     set (update_ξ ξ ((⟨vnew, σ₂ @@  p ⟩) :: nil)) as ξ' in *.
 651     inversion X_.
 652     apply ileaf in X.
 653     apply ileaf in X0.
 654     simpl in *.
 655     refine (X0 ξ  vars2 _ >>>= fun X0' => _).
 656     apply FreshMon.
 657     auto.
 658     refine (X  ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
 659     apply FreshMon.
 660     rewrite H1.
 661     simpl.
 662     rewrite pf2.
 663     rewrite pf1.
 664     rewrite H1.
 665     reflexivity.
 666     refine (return _).
 667     apply ILeaf.
 668     apply ileaf in X0'.
 669     apply ileaf in X1'.
 670     simpl in *.
 671     apply ELet with (ev:=vnew)(tv:=σ₂).
 672     apply X0'.
 673     apply X1'.
 674
 675   destruct case_REmptyGroup.
 676     apply ILeaf; simpl; intros.
 677     refine (return _).
 678     apply INone.
 679
 680   destruct case_RAppT.
 681     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 682     apply ETyApp.
 683     apply (ileaf X).
 684
 685   destruct case_RAbsT.
 686     apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 687     rewrite mapOptionTree_compose.
 688     rewrite <- H.
 689     reflexivity.
 690     apply ileaf in X. simpl in *.
 691     apply ETyLam.
 692     apply X.
 693
 694   destruct case_RAppCo.
 695     apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 696     auto.
 697     eapply ECoApp.
 698     apply γ.
 699     apply (ileaf X).
 700
 701   destruct case_RAbsCo.
 702     apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 703     auto.
 704     eapply ECoLam.
 705     apply (ileaf X).
 706
 707   destruct case_RLetRec.
 708     apply ILeaf; simpl; intros.
 709     refine (bind ξvars = fresh_lemma' _ y _ _ _ H; _). apply FreshMon.
 710     destruct ξvars as [ varstypes [ pf1 pf2 ]].
 711     refine (X_ ((update_ξ ξ (leaves varstypes)))
 712       (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_.  apply FreshMon.
 713     simpl.
 714     rewrite pf2.
 715     rewrite pf1.
 716     auto.
 717     apply ILeaf.
 718     destruct x as [τ l].
 719     inversion X; subst; clear X.
 720
 721     (* getting rid of this will require strengthening RLetRec *)
 722     assert ((mapOptionTree (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) @@  l ⟩) varstypes) = varstypes) as HHH.
 723       admit.
 724
 725     apply (@ELetRec _ _ _ _ _ _ _ (mapOptionTree (fun x => ((fst x),unlev (snd x))) varstypes));
 726       rewrite mapleaves; rewrite <- map_compose; simpl;
 727       [ idtac
 728       | rewrite <- mapleaves; rewrite HHH; apply (ileaf X0) ].
 729
 730     clear X0.
 731     rewrite <- mapOptionTree_compose in X1.
 732     set (fun x : VV * LeveledHaskType Γ ★ => ⟨fst x, unlev (snd x) @@  l ⟩) as ξ' in *.
 733     rewrite <- mapleaves.
 734     rewrite HHH.
 735
 736     apply (letrec_helper _ _ _ _ _ X1).
 737
 738   destruct case_RCase.
 739     apply ILeaf; simpl; intros.
 740     inversion X_.
 741     clear X_.
 742     subst.
 743     apply ileaf in X0.
 744     simpl in X0.
 745     set (mapOptionTreeAndFlatten pcb_freevars alts) as Σalts in *.
 746     refine (bind ξvars = fresh_lemma' _ (Σalts,,Σ) _ _ _ H ; _).
 747       apply FreshMon.
 748       destruct vars; try destruct o; inversion H; clear H.
 749       rename vars1 into varsalts.
 750       rename vars2 into varsΣ.
 751
 752
 753     refine ( _ >>>= fun Y => X0 ξ varsΣ _ >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
 754       apply FreshMon.
 755       destruct ξvars as [varstypes [pf1 pf2]].
 756
 757       apply treeM.
 758       apply itree_mapOptionTree in X.
 759       refine (itree_to_tree (itmap _ X)).
 760       intros.
 761       eapply case_helper.
 762       apply X1.
 763       instantiate (1:=varsΣ).
 764       rewrite <- H2.
 765       admit.
 766       apply FreshMon.
 767     Defined.
 768
 769   Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
 770     refine ((
 771       fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
 772       match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
 773       | cnd_weak             => let case_nil    := tt in INone _ _
 774       | cnd_rule h c cnd' r  => let case_rule   := tt in rule2expr _ _ r (closed2expr' _ cnd')
 775       | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2)
 776       end)); clear closed2expr'; intros; subst.
 777         Defined.
 778
 779   Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
 780     {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
 781     FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
 782     intro pf.
 783     set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
 784     apply closed2expr in cnd.
 785     apply ileaf in cnd.
 786     simpl in *.
 787     clear pf.
 788     refine (bind ξvars = manyFresh _ Σ ξ0; _).
 789     apply FreshMon.
 790     destruct ξvars as [vars ξpf].
 791     destruct ξpf as [ξ pf].
 792     refine (cnd ξ vars _ >>>= fun it => _).
 793     apply FreshMon.
 794     auto.
 795     refine (return OK _).
 796     exists ξ.
 797     apply (ileaf it).
 798     Defined.
 799
 800 End HaskProofToStrong.