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 NaturalDeductionContext.
  10 Require Import Coq.Strings.String.
  11 Require Import Coq.Lists.List.
  12 Require Import Coq.Init.Specif.
  13 Require Import HaskKinds.
  14 Require Import HaskStrongTypes.
  15 Require Import HaskStrong.
  16 Require Import HaskProof.
  17
  18 Section HaskProofToStrong.
  19
  20   Context {VV:Type} {eqdec_vv:EqDecidable VV} {freshM:FreshMonad VV}.
  21
  22   Definition fresh := FMT_fresh freshM.
  23   Definition FreshM := FMT freshM.
  24   Definition FreshMon := FMT_Monad freshM.
  25   Existing Instance FreshMon.
  26
  27   Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★.
  28
  29   Definition judg2exprType (j:Judg) : Type :=
  30     match j with
  31       (Γ > Δ > Σ |- τ @ l) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
  32         FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ)
  33       end.
  34
  35   Definition justOne Γ Δ ξ τ l : ITree _ (fun t => Expr Γ Δ ξ t l) [τ] -> Expr Γ Δ ξ τ l.
  36     intros.
  37     inversion X; auto.
  38     Defined.
  39
  40   Definition ileaf `(it:ITree X F [t]) : F t.
  41     inversion it.
  42     apply X0.
  43     Defined.
  44
  45   Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q,
  46     update_xi ξ lev (app l1 l2) q = update_xi (update_xi ξ lev l2) lev l1 q.
  47     intros.
  48     induction l1.
  49       reflexivity.
  50       simpl.
  51       destruct a; simpl.
  52       rewrite IHl1.
  53       reflexivity.
  54       Qed.
  55
  56    Lemma quark {T} (l1:list T) l2 vf :
  57       (In vf (app l1 l2)) <->
  58        (In vf l1) \/ (In vf l2).
  59      induction l1.
  60      simpl; auto.
  61      split; intro.
  62      right; auto.
  63      inversion H.
  64      inversion H0.
  65      auto.
  66      split.
  67
  68      destruct IHl1.
  69      simpl in *.
  70      intro.
  71      destruct H1.
  72      left; left; auto.
  73      set (H H1) as q.
  74      destruct q.
  75      left; right; auto.
  76      right; auto.
  77      simpl.
  78
  79      destruct IHl1.
  80      simpl in *.
  81      intro.
  82      destruct H1.
  83      destruct H1.
  84      left; auto.
  85      right; apply H0; auto.
  86      right; apply H0; auto.
  87    Qed.
  88
  89   Lemma splitter {T} (l1:list T) l2 vf :
  90       (In vf (app l1 l2) → False)
  91       -> (In vf l1 → False)  /\ (In vf l2 → False).
  92     intros.
  93     split; intros; apply H; rewrite quark.
  94     auto.
  95     auto.
  96     Qed.
  97
  98   Lemma helper
  99     : forall T Z {eqdt:EqDecidable T}(tl:Tree ??T)(vf:T) ξ (q:Z),
 100       (In vf (leaves tl) -> False) ->
 101       mapOptionTree (fun v' => if eqd_dec vf v' then q else ξ v') tl =
 102       mapOptionTree ξ tl.
 103     intros.
 104     induction tl;
 105       try destruct a;
 106         simpl in *.
 107     set (eqd_dec vf t) as x in *.
 108     destruct x.
 109     subst.
 110       assert False.
 111       apply H.
 112       left; auto.
 113       inversion H0.
 114     auto.
 115     auto.
 116     apply splitter in H.
 117     destruct H.
 118     rewrite (IHtl1 H).
 119     rewrite (IHtl2 H0).
 120     reflexivity.
 121     Qed.
 122
 123   Lemma fresh_lemma'' Γ
 124     : forall types ξ lev,
 125     FreshM { varstypes : _
 126       |  mapOptionTree (update_xi(Γ:=Γ)   ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
 127       /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
 128   admit.
 129   Defined.
 130
 131   Lemma fresh_lemma' Γ
 132     : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars ->
 133     FreshM { varstypes : _
 134       |  mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
 135       /\ mapOptionTree (update_xi       ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
 136       /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
 137     induction types.
 138       intros; destruct a.
 139         refine (bind vf = fresh (leaves vars) ; return _).
 140           apply FreshMon.
 141           destruct vf as [ vf vf_pf ].
 142           exists [(vf,h)].
 143           split; auto.
 144           simpl.
 145           set (helper VV _ vars vf ξ (h@@lev) vf_pf) as q.
 146           rewrite q.
 147           symmetry; auto.
 148           simpl.
 149           destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto.
 150           split; auto.
 151           apply distinct_cons.
 152           intro.
 153           inversion H0.
 154           apply distinct_nil.
 155         refine (return _).
 156           exists []; auto.
 157           split.
 158           simpl.
 159           symmetry; auto.
 160           split.
 161           simpl.
 162           reflexivity.
 163           simpl.
 164           apply distinct_nil.
 165         intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _).
 166           apply FreshMon.
 167           destruct x2 as [vt2 [pf21 [pf22 pfdist]]].
 168           refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_xi ξ lev
 169             (leaves vt2)) _ _; return _).
 170           apply FreshMon.
 171           simpl.
 172           rewrite pf21.
 173           rewrite pf22.
 174           reflexivity.
 175           clear IHtypes1 IHtypes2.
 176           destruct x1 as [vt1 [pf11 pf12]].
 177           exists (vt1,,vt2); split; auto.
 178
 179           set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
 180           set (mapOptionTree_extensional _ _ q) as q'.
 181           rewrite q'.
 182           clear q' q.
 183           inversion pf11.
 184           reflexivity.
 185
 186           simpl.
 187           set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
 188           set (mapOptionTree_extensional _ _ q) as q'.
 189           rewrite q'.
 190           rewrite q'.
 191           clear q' q.
 192           rewrite <- mapOptionTree_compose.
 193           rewrite <- mapOptionTree_compose.
 194           rewrite <- mapOptionTree_compose in *.
 195           split.
 196           destruct pf12.
 197           rewrite H.
 198           inversion pf11.
 199           rewrite <- mapOptionTree_compose.
 200           reflexivity.
 201
 202           admit.
 203         Defined.
 204
 205   Lemma fresh_lemma Γ ξ vars Σ Σ' lev
 206     : Σ = mapOptionTree ξ vars ->
 207     FreshM { vars' : _
 208       |  mapOptionTree (update_xi(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
 209       /\ mapOptionTree (update_xi ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
 210     intros.
 211     set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
 212     refine (q >>>= fun q' => return _).
 213     apply FreshMon.
 214     clear q.
 215     destruct q' as [varstypes [pf1 [pf2 pfdist]]].
 216     destruct varstypes; try destruct o; try destruct p; simpl in *.
 217       destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
 218       inversion pf2; subst.
 219       exists v.
 220       destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
 221       split; auto.
 222       inversion pf2.
 223       inversion pf2.
 224     Defined.
 225
 226   Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ l : Type :=
 227     forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ).
 228
 229   Definition urule2expr  : forall Γ Δ h j t l (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
 230     ujudg2exprType Γ ξ Δ h t l ->
 231     ujudg2exprType Γ ξ Δ j t l
 232     .
 233     intros Γ Δ.
 234       refine (fix urule2expr h j t l (r:@Arrange _ h j) ξ {struct r} :
 235     ujudg2exprType Γ ξ Δ h t l ->
 236     ujudg2exprType Γ ξ Δ j t l :=
 237         match r as R in Arrange H C return
 238     ujudg2exprType Γ ξ Δ H t l ->
 239     ujudg2exprType Γ ξ Δ C t l
 240  with
 241           | ALeft   h c ctx r => let case_ALeft  := tt in (fun e => _) (urule2expr _ _ _ _ r)
 242           | ARight  h c ctx r => let case_ARight := tt in (fun e => _) (urule2expr _ _ _ _ r)
 243           | AId     a       => let case_AId    := tt in _
 244           | ACanL   a       => let case_ACanL  := tt in _
 245           | ACanR   a       => let case_ACanR  := tt in _
 246           | AuCanL  a       => let case_AuCanL := tt in _
 247           | AuCanR  a       => let case_AuCanR := tt in _
 248           | AAssoc  a b c   => let case_AAssoc := tt in _
 249           | AuAssoc  a b c   => let case_AuAssoc := tt in _
 250           | AExch   a b     => let case_AExch  := tt in _
 251           | AWeak   a       => let case_AWeak  := tt in _
 252           | ACont   a       => let case_ACont  := tt in _
 253           | AComp   a b c f g => let case_AComp  := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g)
 254           end); clear urule2expr; intros.
 255
 256       destruct case_AId.
 257         apply X.
 258
 259       destruct case_ACanL.
 260         simpl; unfold ujudg2exprType; intros.
 261         simpl in X.
 262         apply (X ([],,vars)).
 263         simpl; rewrite <- H; auto.
 264
 265       destruct case_ACanR.
 266         simpl; unfold ujudg2exprType; intros.
 267         simpl in X.
 268         apply (X (vars,,[])).
 269         simpl; rewrite <- H; auto.
 270
 271       destruct case_AuCanL.
 272         simpl; unfold ujudg2exprType; intros.
 273         destruct vars; try destruct o; inversion H.
 274         simpl in X.
 275         apply (X vars2); auto.
 276
 277       destruct case_AuCanR.
 278         simpl; unfold ujudg2exprType; intros.
 279         destruct vars; try destruct o; inversion H.
 280         simpl in X.
 281         apply (X vars1); auto.
 282
 283       destruct case_AAssoc.
 284         simpl; unfold ujudg2exprType; intros.
 285         simpl in X.
 286         destruct vars; try destruct o; inversion H.
 287         destruct vars1; try destruct o; inversion H.
 288         apply (X (vars1_1,,(vars1_2,,vars2))).
 289         subst; auto.
 290
 291       destruct case_AuAssoc.
 292         simpl; unfold ujudg2exprType; intros.
 293         simpl in X.
 294         destruct vars; try destruct o; inversion H.
 295         destruct vars2; try destruct o; inversion H.
 296         apply (X ((vars1,,vars2_1),,vars2_2)).
 297         subst; auto.
 298
 299       destruct case_AExch.
 300         simpl; unfold ujudg2exprType ; intros.
 301         simpl in X.
 302         destruct vars; try destruct o; inversion H.
 303         apply (X (vars2,,vars1)).
 304         inversion H; subst; auto.
 305
 306       destruct case_AWeak.
 307         simpl; unfold ujudg2exprType; intros.
 308         simpl in X.
 309         apply (X []).
 310         auto.
 311
 312       destruct case_ACont.
 313         simpl; unfold ujudg2exprType ; intros.
 314         simpl in X.
 315         apply (X (vars,,vars)).
 316         simpl.
 317         rewrite <- H.
 318         auto.
 319
 320       destruct case_ALeft.
 321         intro vars; unfold ujudg2exprType; intro H.
 322         destruct vars; try destruct o; inversion H.
 323         apply (fun q => e ξ q vars2 H2).
 324         clear r0 e H2.
 325           simpl in X.
 326           simpl.
 327           unfold ujudg2exprType.
 328           intros.
 329           apply X with (vars:=vars1,,vars).
 330           rewrite H0.
 331           rewrite H1.
 332           simpl.
 333           reflexivity.
 334
 335       destruct case_ARight.
 336         intro vars; unfold ujudg2exprType; intro H.
 337         destruct vars; try destruct o; inversion H.
 338         apply (fun q => e ξ q vars1 H1).
 339         clear r0 e H2.
 340           simpl in X.
 341           simpl.
 342           unfold ujudg2exprType.
 343           intros.
 344           apply X with (vars:=vars,,vars2).
 345           rewrite H0.
 346           inversion H.
 347           simpl.
 348           reflexivity.
 349
 350       destruct case_AComp.
 351         apply e2.
 352         apply e1.
 353         apply X.
 354         Defined.
 355
 356   Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
 357     ITree (HaskType Γ ★)
 358          (fun t : HaskType Γ ★ => Expr Γ Δ ξ' t l)
 359          (mapOptionTree (unlev ○ ξ' ○ (@fst _ _)) varstypes)
 360          -> ELetRecBindings Γ Δ ξ' l varstypes.
 361     intros.
 362     induction varstypes.
 363     destruct a; simpl in *.
 364     destruct p.
 365     simpl.
 366     apply ileaf in X. simpl in X.
 367       apply ELR_leaf.
 368       rename h into τ.
 369       destruct (eqd_dec (unlev (ξ' v)) τ).
 370       rewrite <- e.
 371       destruct (ξ' v).
 372       simpl.
 373       destruct (eqd_dec h0 l).
 374         rewrite <- e0.
 375         simpl in X.
 376         subst.
 377         apply X.
 378       apply (Prelude_error "level mismatch; should never happen").
 379       apply (Prelude_error "letrec type mismatch; should never happen").
 380
 381     apply ELR_nil.
 382     apply ELR_branch.
 383       apply IHvarstypes1; inversion X; auto.
 384       apply IHvarstypes2; inversion X; auto.
 385     Defined.
 386
 387   Definition unindex_tree {V}{F} : forall {t:Tree ??V}, ITree V F t -> Tree ??{ v:V & F v }.
 388     refine (fix rec t it := match it as IT return Tree ??{ v:V & F v } with
 389       | INone => T_Leaf None
 390       | ILeaf x y => T_Leaf (Some _)
 391       | IBranch _ _ b1 b2 => (rec _ b1),,(rec _ b2)
 392             end).
 393     exists x; auto.
 394     Defined.
 395
 396   Definition fix_indexing X Y (J:X->Type)(t:Tree ??(X*Y))
 397     :  ITree (X * Y) (fun x => J (fst x))                                t
 398     -> ITree X       (fun x:X => J x)   (mapOptionTree (@fst _ _) t).
 399     intro it.
 400     induction it; simpl in *.
 401     apply INone.
 402     apply ILeaf.
 403     apply f.
 404     simpl; apply IBranch; auto.
 405     Defined.
 406
 407   Definition fix2 {X}{F} : Tree ??{ x:X & FreshM (F x) } -> Tree ??(FreshM { x:X & F x }).
 408     refine (fix rec t := match t with
 409       | T_Leaf None => T_Leaf None
 410       | T_Leaf (Some x) => T_Leaf (Some _)
 411       | T_Branch b1 b2 => T_Branch (rec b1) (rec b2)
 412             end).
 413     destruct x as [x fx].
 414     refine (bind fx' = fx ; return _).
 415     apply FreshMon.
 416     exists x.
 417     apply fx'.
 418     Defined.
 419
 420   Definition case_helper tc Γ Δ lev tbranches avars ξ :
 421     forall pcb:(StrongAltCon * Tree ??(LeveledHaskType Γ ★)),
 422      prod (judg2exprType (@pcb_judg tc Γ Δ lev tbranches avars (fst pcb) (snd pcb)))
 423      {vars' : Tree ??VV & (snd pcb) = mapOptionTree ξ vars'} ->
 424      ((fun sac => FreshM
 425        { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
 426          & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev)
 427          (weakT' tbranches) (weakL' lev) }) (fst pcb)).
 428     intro pcb.
 429     intro X.
 430     simpl in X.
 431     simpl.
 432     destruct pcb as [sac pcb].
 433     simpl in *.
 434
 435     destruct X.
 436     destruct s as [vars vars_pf].
 437
 438     refine (bind localvars = fresh_lemma' _ (unleaves  (vec2list (sac_types sac _ avars))) vars
 439       (mapOptionTree weakLT' pcb) (weakLT' ○ ξ) (weakL' lev) _  ; _).
 440       apply FreshMon.
 441       rewrite vars_pf.
 442       rewrite <- mapOptionTree_compose.
 443       reflexivity.
 444       destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]].
 445       set (mapOptionTree (@fst _ _) localvars) as localvars'.
 446
 447     set (list2vec (leaves localvars')) as localvars''.
 448     cut (length (leaves localvars') = sac_numExprVars sac). intro H''.
 449       rewrite H'' in localvars''.
 450     cut (distinct (vec2list localvars'')). intro H'''.
 451     set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
 452
 453     refine (bind q = (f (scbwv_xi scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
 454       apply FreshMon.
 455       simpl.
 456       unfold scbwv_xi.
 457       rewrite vars_pf.
 458       rewrite <- mapOptionTree_compose.
 459       clear localvars_pf1.
 460       simpl.
 461       rewrite mapleaves'.
 462
 463     admit.
 464
 465     exists scb.
 466     apply ileaf in q.
 467     apply q.
 468
 469     admit.
 470     admit.
 471     Defined.
 472
 473   Definition gather_branch_variables
 474     Γ Δ
 475     (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev
 476     (alts:Tree ??(@StrongAltCon tc * Tree ??(LeveledHaskType Γ ★)))
 477     :
 478     forall vars,
 479     mapOptionTreeAndFlatten (fun x => snd x) alts = mapOptionTree ξ vars
 480     -> ITree Judg judg2exprType (mapOptionTree (fun x => @pcb_judg tc Γ Δ lev avars tbranches (fst x) (snd x)) alts)
 481     -> ITree _ (fun q => prod (judg2exprType (@pcb_judg tc Γ Δ lev avars tbranches (fst q) (snd q)))
 482       { vars' : _ & (snd q) = mapOptionTree ξ vars' })
 483   alts.
 484     induction alts;
 485     intro vars;
 486     intro pf;
 487     intro source.
 488     destruct a; [ idtac | apply INone ].
 489     simpl in *.
 490     apply ileaf in source.
 491     apply ILeaf.
 492     destruct p as [sac pcb].
 493     simpl in *.
 494     split.
 495     intros.
 496     eapply source.
 497     apply H.
 498     clear source.
 499
 500     exists vars.
 501     auto.
 502
 503     simpl in pf.
 504     destruct vars; try destruct o; simpl in pf; inversion pf.
 505     simpl in source.
 506     inversion source.
 507     subst.
 508     apply IBranch.
 509     apply (IHalts1 vars1 H0 X); auto.
 510     apply (IHalts2 vars2 H1 X0); auto.
 511
 512     Defined.
 513
 514   Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
 515     FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
 516     intros Γ Σ.
 517     induction Σ; intro ξ.
 518     destruct a.
 519     destruct l as [τ l].
 520     set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
 521     refine (q >>>= fun q' => return _).
 522     apply FreshMon.
 523     clear q.
 524     destruct q' as [varstypes [pf1 [pf2 distpf]]].
 525     exists (mapOptionTree (@fst _ _) varstypes).
 526     exists (update_xi ξ l (leaves varstypes)).
 527     symmetry; auto.
 528     refine (return _).
 529     exists [].
 530     exists ξ; auto.
 531     refine (bind f1 = IHΣ1 ξ ; _).
 532     apply FreshMon.
 533     destruct f1 as [vars1 [ξ1 pf1]].
 534     refine (bind f2 = IHΣ2 ξ1 ; _).
 535     apply FreshMon.
 536     destruct f2 as [vars2 [ξ2 pf22]].
 537     refine (return _).
 538     exists (vars1,,vars2).
 539     exists ξ2.
 540     simpl.
 541     rewrite pf22.
 542     rewrite pf1.
 543     admit.         (* freshness assumption *)
 544     Defined.
 545
 546   Definition rlet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p :
 547     forall (X_ : ITree Judg judg2exprType
 548          ([Γ > Δ > Σ₁ |- [σ₁] @ p],, [Γ > Δ > [σ₁ @@  p],, Σ₂ |- [σ₂] @ p])),
 549    ITree Judg judg2exprType [Γ > Δ > Σ₁,, Σ₂ |- [σ₂] @ p].
 550     intros.
 551     apply ILeaf.
 552     simpl in *; intros.
 553     destruct vars; try destruct o; inversion H.
 554
 555     refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)).
 556     apply FreshMon.
 557
 558     destruct pf as [ vnew [ pf1 pf2 ]].
 559     set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
 560     inversion X_.
 561     apply ileaf in X.
 562     apply ileaf in X0.
 563     simpl in *.
 564
 565     refine (X ξ vars1 _ >>>= fun X0' => _).
 566     apply FreshMon.
 567     simpl.
 568     auto.
 569
 570     refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _).
 571     apply FreshMon.
 572     simpl.
 573     rewrite pf2.
 574     rewrite pf1.
 575     reflexivity.
 576     apply FreshMon.
 577
 578     apply ILeaf.
 579     apply ileaf in X1'.
 580     apply ileaf in X0'.
 581     simpl in *.
 582     apply ELet with (ev:=vnew)(tv:=σ₁).
 583     apply X0'.
 584     apply X1'.
 585     Defined.
 586
 587   Definition vartree Γ Δ Σ lev ξ :
 588     forall vars, Σ @@@ lev = mapOptionTree ξ vars ->
 589     ITree (HaskType Γ ★) (fun t : HaskType Γ ★ => Expr Γ Δ ξ t lev) Σ.
 590     induction Σ; intros.
 591     destruct a.
 592     intros; simpl in *.
 593     apply ILeaf.
 594     destruct vars; try destruct o; inversion H.
 595     set (EVar Γ Δ ξ v) as q.
 596     rewrite <- H1 in q.
 597     apply q.
 598     intros.
 599     apply INone.
 600     intros.
 601     destruct vars; try destruct o; inversion H.
 602     apply IBranch.
 603     eapply IHΣ1.
 604     apply H1.
 605     eapply IHΣ2.
 606     apply H2.
 607     Defined.
 608
 609
 610   Definition rdrop  Γ Δ Σ₁ Σ₁₂ a lev :
 611     ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a,,Σ₁₂ @ lev] ->
 612     ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
 613     intros.
 614     apply ileaf in X.
 615     apply ILeaf.
 616     simpl in *.
 617     intros.
 618     set (X ξ vars H) as q.
 619     simpl in q.
 620     refine (q >>>= fun q' => return _).
 621     apply FreshMon.
 622     inversion q'.
 623     apply X0.
 624     Defined.
 625
 626   Definition rdrop'  Γ Δ Σ₁ Σ₁₂ a lev :
 627     ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂,,a @ lev] ->
 628     ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
 629     intros.
 630     apply ileaf in X.
 631     apply ILeaf.
 632     simpl in *.
 633     intros.
 634     set (X ξ vars H) as q.
 635     simpl in q.
 636     refine (q >>>= fun q' => return _).
 637     apply FreshMon.
 638     inversion q'.
 639     auto.
 640     Defined.
 641
 642   Definition rdrop''  Γ Δ Σ₁ Σ₁₂ lev :
 643     ITree Judg judg2exprType [Γ > Δ > [],,Σ₁ |- Σ₁₂ @ lev] ->
 644     ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev].
 645     intros.
 646     apply ileaf in X.
 647     apply ILeaf.
 648     simpl in *; intros.
 649     eapply X with (vars:=[],,vars).
 650     rewrite H; reflexivity.
 651     Defined.
 652
 653   Definition rdrop'''  Γ Δ a Σ₁ Σ₁₂ lev :
 654     ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] ->
 655     ITree Judg judg2exprType [Γ > Δ > a,,Σ₁ |- Σ₁₂ @ lev].
 656     intros.
 657     apply ileaf in X.
 658     apply ILeaf.
 659     simpl in *; intros.
 660     destruct vars; try destruct o; inversion H.
 661     eapply X with (vars:=vars2).
 662     auto.
 663     Defined.
 664
 665   Definition rassoc  Γ Δ Σ₁ a b c lev :
 666     ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
 667     ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev].
 668     intros.
 669     apply ileaf in X.
 670     apply ILeaf.
 671     simpl in *; intros.
 672     destruct vars; try destruct o; inversion H.
 673     destruct vars2; try destruct o; inversion H2.
 674     apply X with (vars:=(vars1,,vars2_1),,vars2_2).
 675     subst; reflexivity.
 676     Defined.
 677
 678   Definition rassoc'  Γ Δ Σ₁ a b c lev :
 679     ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev] ->
 680     ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev].
 681     intros.
 682     apply ileaf in X.
 683     apply ILeaf.
 684     simpl in *; intros.
 685     destruct vars; try destruct o; inversion H.
 686     destruct vars1; try destruct o; inversion H1.
 687     apply X with (vars:=vars1_1,,(vars1_2,,vars2)).
 688     subst; reflexivity.
 689     Defined.
 690
 691   Definition swapr  Γ Δ Σ₁ a b c lev :
 692     ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
 693     ITree Judg judg2exprType [Γ > Δ > ((b,,a),,c) |- Σ₁ @ lev].
 694     intros.
 695     apply ileaf in X.
 696     apply ILeaf.
 697     simpl in *; intros.
 698     destruct vars; try destruct o; inversion H.
 699     destruct vars1; try destruct o; inversion H1.
 700     apply X with (vars:=(vars1_2,,vars1_1),,vars2).
 701     subst; reflexivity.
 702     Defined.
 703
 704   Definition rdup  Γ Δ Σ₁ a  c lev :
 705     ITree Judg judg2exprType [Γ > Δ > ((a,,a),,c) |- Σ₁ @ lev] ->
 706     ITree Judg judg2exprType [Γ > Δ > (a,,c) |- Σ₁ @ lev].
 707     intros.
 708     apply ileaf in X.
 709     apply ILeaf.
 710     simpl in *; intros.
 711     destruct vars; try destruct o; inversion H.
 712     apply X with (vars:=(vars1,,vars1),,vars2).    (* is this allowed? *)
 713     subst; reflexivity.
 714     Defined.
 715
 716   (* holy cow this is ugly *)
 717   Definition rcut Γ Δ  Σ₃ lev  Σ₁₂  :
 718     forall Σ₁ Σ₂,
 719     ITree Judg judg2exprType [Γ > Δ > Σ₁ |-  Σ₁₂ @ lev] ->
 720     ITree Judg judg2exprType [Γ > Δ >  Σ₁₂ @@@ lev,,Σ₂ |- [Σ₃] @ lev] ->
 721     ITree Judg judg2exprType [Γ > Δ > Σ₁,,Σ₂ |- [Σ₃] @ lev].
 722
 723     induction Σ₁₂.
 724     intros.
 725     destruct a.
 726
 727     eapply rlet.
 728     apply IBranch.
 729     apply X.
 730     apply X0.
 731
 732     simpl in X0.
 733     apply rdrop'' in X0.
 734     apply rdrop'''.
 735     apply X0.
 736
 737     intros.
 738     simpl in X0.
 739     apply rassoc in X0.
 740     set (IHΣ₁₂1 _ _ (rdrop  _ _ _ _ _ _ X) X0) as q.
 741     set (IHΣ₁₂2 _ (Σ₁,,Σ₂) (rdrop' _ _ _ _ _ _ X)) as q'.
 742     apply rassoc' in q.
 743     apply swapr in q.
 744     apply rassoc in q.
 745     set (q' q) as q''.
 746     apply rassoc' in q''.
 747     apply rdup in q''.
 748     apply q''.
 749     Defined.
 750
 751   Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
 752
 753     intros h j r.
 754
 755       refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
 756       | RArrange a b c d e l r        => let case_RURule := tt        in _
 757       | RNote   Γ Δ Σ τ l n           => let case_RNote := tt         in _
 758       | RLit    Γ Δ l     _           => let case_RLit := tt          in _
 759       | RVar    Γ Δ σ         p       => let case_RVar := tt          in _
 760       | RGlobal Γ Δ σ l wev           => let case_RGlobal := tt       in _
 761       | RLam    Γ Δ Σ tx te     x     => let case_RLam := tt          in _
 762       | RCast   Γ Δ Σ σ τ γ     x     => let case_RCast := tt         in _
 763       | RAbsT   Γ Δ Σ κ σ a           => let case_RAbsT := tt         in _
 764       | RAppT   Γ Δ Σ κ σ τ     y     => let case_RAppT := tt         in _
 765       | RAppCo  Γ Δ Σ κ σ₁ σ₂ γ σ l   => let case_RAppCo := tt        in _
 766       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
 767       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
 768       | RCut    Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l  => let case_RCut := tt          in _
 769       | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
 770       | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
 771       | RVoid   _ _ l                 => let case_RVoid := tt   in _
 772       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
 773       | REsc    Σ a b c n m           => let case_REsc := tt          in _
 774       | RCase   Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 775       | RLetRec Γ Δ lri x y t         => let case_RLetRec := tt       in _
 776       end); intro X_; try apply ileaf in X_; simpl in X_.
 777
 778     destruct case_RURule.
 779       apply ILeaf. simpl. intros.
 780       set (@urule2expr a b _ _ e l r0 ξ) as q.
 781       unfold ujudg2exprType.
 782       unfold ujudg2exprType in q.
 783       apply q with (vars:=vars).
 784       intros.
 785       apply X_ with (vars:=vars0).
 786       auto.
 787       auto.
 788
 789   destruct case_RBrak.
 790     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 791     apply EBrak.
 792     apply (ileaf X).
 793
 794   destruct case_REsc.
 795     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 796     apply EEsc.
 797     apply (ileaf X).
 798
 799   destruct case_RNote.
 800     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 801     apply ENote; auto.
 802     apply (ileaf X).
 803
 804   destruct case_RLit.
 805     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 806     apply ELit.
 807
 808   destruct case_RVar.
 809     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 810     destruct vars; simpl in H; inversion H; destruct o. inversion H1.
 811     set (@EVar _ _ _ Δ ξ v) as q.
 812     rewrite <- H2 in q.
 813     simpl in q.
 814     apply q.
 815     inversion H.
 816
 817   destruct case_RGlobal.
 818     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 819     apply EGlobal.
 820
 821   destruct case_RLam.
 822     apply ILeaf.
 823     simpl in *; intros.
 824     refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
 825     apply FreshMon.
 826     destruct pf as [ vnew [ pf1 pf2 ]].
 827     set (update_xi ξ x (((vnew, tx  )) :: nil)) as ξ' in *.
 828     refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
 829     apply FreshMon.
 830     simpl.
 831     rewrite pf1.
 832     rewrite <- pf2.
 833     simpl.
 834     reflexivity.
 835     intro hyp.
 836     refine (return _).
 837     apply ILeaf.
 838     apply ELam with (ev:=vnew).
 839     apply ileaf in hyp.
 840     simpl in hyp.
 841     unfold ξ' in hyp.
 842     apply hyp.
 843
 844   destruct case_RCast.
 845     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 846     eapply ECast.
 847     apply x.
 848     apply ileaf in X. simpl in X.
 849     apply X.
 850
 851   destruct case_RApp.
 852     apply ILeaf.
 853     inversion X_.
 854     inversion X.
 855     inversion X0.
 856     simpl in *.
 857     intros.
 858     destruct vars. try destruct o; inversion H.
 859     simpl in H.
 860     inversion H.
 861     set (X1 ξ vars1 H5) as q1.
 862     set (X2 ξ vars2 H6) as q2.
 863     refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
 864     apply FreshMon.
 865     apply FreshMon.
 866     apply ILeaf.
 867     apply ileaf in q1'.
 868     apply ileaf in q2'.
 869     simpl in *.
 870     apply (EApp _ _ _ _ _ _ q1' q2').
 871
 872   destruct case_RCut.
 873     apply rassoc.
 874     apply swapr.
 875     apply rassoc'.
 876
 877     inversion X_.
 878     subst.
 879     clear X_.
 880
 881     apply rassoc' in X0.
 882     apply swapr in X0.
 883     apply rassoc in X0.
 884
 885     induction Σ₃.
 886     destruct a.
 887     subst.
 888     eapply rcut.
 889     apply X.
 890     apply X0.
 891
 892     apply ILeaf.
 893     simpl.
 894     intros.
 895     refine (return _).
 896     apply INone.
 897     set (IHΣ₃1 (rdrop  _ _ _ _ _ _ X0)) as q1.
 898     set (IHΣ₃2 (rdrop' _ _ _ _ _ _ X0)) as q2.
 899     apply ileaf in q1.
 900     apply ileaf in q2.
 901     simpl in *.
 902     apply ILeaf.
 903     simpl.
 904     intros.
 905     refine (q1 _ _ H >>>= fun q1' => q2 _ _ H >>>= fun q2' => return _).
 906     apply FreshMon.
 907     apply FreshMon.
 908     apply IBranch; auto.
 909
 910   destruct case_RLeft.
 911     apply ILeaf.
 912     simpl; intros.
 913     destruct vars; try destruct o; inversion H.
 914     refine (X_ _ _ H2 >>>= fun X' => return _).
 915     apply FreshMon.
 916     apply IBranch.
 917     eapply vartree.
 918     apply H1.
 919     apply X'.
 920
 921   destruct case_RRight.
 922     apply ILeaf.
 923     simpl; intros.
 924     destruct vars; try destruct o; inversion H.
 925     refine (X_ _ _ H1 >>>= fun X' => return _).
 926     apply FreshMon.
 927     apply IBranch.
 928     apply X'.
 929     eapply vartree.
 930     apply H2.
 931
 932   destruct case_RVoid.
 933     apply ILeaf; simpl; intros.
 934     refine (return _).
 935     apply INone.
 936
 937   destruct case_RAppT.
 938     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 939     apply ETyApp.
 940     apply (ileaf X).
 941
 942   destruct case_RAbsT.
 943     apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 944     rewrite mapOptionTree_compose.
 945     rewrite <- H.
 946     reflexivity.
 947     apply ileaf in X. simpl in *.
 948     apply ETyLam.
 949     apply X.
 950
 951   destruct case_RAppCo.
 952     apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 953     auto.
 954     eapply ECoApp.
 955     apply γ.
 956     apply (ileaf X).
 957
 958   destruct case_RAbsCo.
 959     apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 960     auto.
 961     eapply ECoLam.
 962     apply (ileaf X).
 963
 964   destruct case_RLetRec.
 965     apply ILeaf; simpl; intros.
 966     refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
 967     destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
 968     refine (X_ ((update_xi ξ t (leaves varstypes)))
 969       ((mapOptionTree (@fst _ _) varstypes),,vars) _ >>>= fun X => return _); clear X_.  apply FreshMon.
 970     simpl.
 971     rewrite pf2.
 972     rewrite pf1.
 973     auto.
 974     apply ILeaf.
 975     inversion X; subst; clear X.
 976
 977     apply (@ELetRec _ _ _ _ _ _ _ varstypes).
 978     auto.
 979     apply (@letrec_helper Γ Δ t varstypes).
 980     rewrite mapOptionTree_compose.
 981     rewrite mapOptionTree_compose.
 982     rewrite pf2.
 983     replace ((mapOptionTree unlev (y @@@ t))) with y.
 984       apply X0.
 985       clear pf1 X0 X1 pfdist pf2 vars varstypes.
 986       induction y; try destruct a; auto.
 987       rewrite IHy1 at 1.
 988       rewrite IHy2 at 1.
 989       reflexivity.
 990     apply ileaf in X1.
 991     simpl in X1.
 992     apply X1.
 993
 994   destruct case_RCase.
 995     apply ILeaf; simpl; intros.
 996     inversion X_.
 997     clear X_.
 998     subst.
 999     apply ileaf in X0.
1000     simpl in X0.
1001
1002     (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
1003      * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
1004     rename Σ into body_freevars_types.
1005     rename vars into all_freevars.
1006     rename X0 into body_expr.
1007     rename X  into alts_exprs.
1008
1009     destruct all_freevars; try destruct o; inversion H.
1010     rename all_freevars2 into body_freevars.
1011     rename all_freevars1 into alts_freevars.
1012
1013     set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
1014     set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
1015     apply fix_indexing in alts_exprs'.
1016     simpl in alts_exprs'.
1017     apply unindex_tree in alts_exprs'.
1018     simpl in alts_exprs'.
1019     apply fix2 in alts_exprs'.
1020     apply treeM in alts_exprs'.
1021
1022     refine ( alts_exprs' >>>= fun Y =>
1023       body_expr ξ _ _
1024       >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
1025       apply FreshMon.
1026       apply FreshMon.
1027       apply H2.
1028     Defined.
1029
1030   Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
1031     match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
1032     | scnd_weak   _             => let case_nil    := tt in fun _ => INone _ _
1033     | scnd_comp   x h c cnd' r  => let case_rule   := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
1034     | scnd_branch _ _ _ c1 c2   => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
1035     end.
1036
1037   Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
1038     {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
1039     FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).
1040     intro pf.
1041     set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
1042     apply closed2expr in cnd.
1043     apply ileaf in cnd.
1044     simpl in *.
1045     clear pf.
1046     refine (bind ξvars = manyFresh _ Σ ξ0; _).
1047     apply FreshMon.
1048     destruct ξvars as [vars ξpf].
1049     destruct ξpf as [ξ pf].
1050     refine (cnd ξ vars _ >>>= fun it => _).
1051     apply FreshMon.
1052     auto.
1053     refine (return OK _).
1054     exists ξ.
1055     apply ileaf in it.
1056     simpl in it.
1057     apply it.
1058     apply INone.
1059     Defined.
1060
1061 End HaskProofToStrong.