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