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 (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x })
 397     :  ITree { x:X & F x } (fun x => J (projT1 x))                                t
 398     -> ITree X             (fun x:X => J x)   (mapOptionTree (@projT1 _ _) 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:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac},
 422      prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
 423      ((fun sac => FreshM
 424        { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
 425          & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev)
 426          (weakT' tbranches) (weakL' lev) }) (projT1 pcb)).
 427     intro pcb.
 428     intro X.
 429     simpl in X.
 430     simpl.
 431     destruct pcb as [sac pcb].
 432     simpl in *.
 433
 434     destruct X.
 435     destruct s as [vars vars_pf].
 436
 437     refine (bind localvars = fresh_lemma' _ (unleaves  (vec2list (sac_types sac _ avars))) vars
 438       (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _  ; _).
 439       apply FreshMon.
 440       rewrite vars_pf.
 441       rewrite <- mapOptionTree_compose.
 442       reflexivity.
 443       destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]].
 444       set (mapOptionTree (@fst _ _) localvars) as localvars'.
 445
 446     set (list2vec (leaves localvars')) as localvars''.
 447     cut (length (leaves localvars') = sac_numExprVars sac). intro H''.
 448       rewrite H'' in localvars''.
 449     cut (distinct (vec2list localvars'')). intro H'''.
 450     set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
 451
 452     refine (bind q = (f (scbwv_xi scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
 453       apply FreshMon.
 454       simpl.
 455       unfold scbwv_xi.
 456       rewrite vars_pf.
 457       rewrite <- mapOptionTree_compose.
 458       clear localvars_pf1.
 459       simpl.
 460       rewrite mapleaves'.
 461
 462     admit.
 463
 464     exists scb.
 465     apply ileaf in q.
 466     apply q.
 467
 468     admit.
 469     admit.
 470     Defined.
 471
 472   Definition gather_branch_variables
 473     Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
 474                 ProofCaseBranch tc Γ Δ lev tbranches avars sac})
 475     :
 476     forall vars,
 477     mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
 478     -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
 479     -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q)))
 480       { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
 481   alts.
 482     induction alts;
 483     intro vars;
 484     intro pf;
 485     intro source.
 486     destruct a; [ idtac | apply INone ].
 487     simpl in *.
 488     apply ileaf in source.
 489     apply ILeaf.
 490     destruct s as [sac pcb].
 491     simpl in *.
 492     split.
 493     intros.
 494     eapply source.
 495     apply H.
 496     clear source.
 497
 498     exists vars.
 499     auto.
 500
 501     simpl in pf.
 502     destruct vars; try destruct o; simpl in pf; inversion pf.
 503     simpl in source.
 504     inversion source.
 505     subst.
 506     apply IBranch.
 507     apply (IHalts1 vars1 H0 X); auto.
 508     apply (IHalts2 vars2 H1 X0); auto.
 509
 510     Defined.
 511
 512   Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
 513     FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
 514     intros Γ Σ.
 515     induction Σ; intro ξ.
 516     destruct a.
 517     destruct l as [τ l].
 518     set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
 519     refine (q >>>= fun q' => return _).
 520     apply FreshMon.
 521     clear q.
 522     destruct q' as [varstypes [pf1 [pf2 distpf]]].
 523     exists (mapOptionTree (@fst _ _) varstypes).
 524     exists (update_xi ξ l (leaves varstypes)).
 525     symmetry; auto.
 526     refine (return _).
 527     exists [].
 528     exists ξ; auto.
 529     refine (bind f1 = IHΣ1 ξ ; _).
 530     apply FreshMon.
 531     destruct f1 as [vars1 [ξ1 pf1]].
 532     refine (bind f2 = IHΣ2 ξ1 ; _).
 533     apply FreshMon.
 534     destruct f2 as [vars2 [ξ2 pf22]].
 535     refine (return _).
 536     exists (vars1,,vars2).
 537     exists ξ2.
 538     simpl.
 539     rewrite pf22.
 540     rewrite pf1.
 541     admit.         (* freshness assumption *)
 542     Defined.
 543
 544   Definition rlet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p :
 545     forall (X_ : ITree Judg judg2exprType
 546          ([Γ > Δ > Σ₁ |- [σ₁] @ p],, [Γ > Δ > [σ₁ @@  p],, Σ₂ |- [σ₂] @ p])),
 547    ITree Judg judg2exprType [Γ > Δ > Σ₁,, Σ₂ |- [σ₂] @ p].
 548     intros.
 549     apply ILeaf.
 550     simpl in *; intros.
 551     destruct vars; try destruct o; inversion H.
 552
 553     refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)).
 554     apply FreshMon.
 555
 556     destruct pf as [ vnew [ pf1 pf2 ]].
 557     set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
 558     inversion X_.
 559     apply ileaf in X.
 560     apply ileaf in X0.
 561     simpl in *.
 562
 563     refine (X ξ vars1 _ >>>= fun X0' => _).
 564     apply FreshMon.
 565     simpl.
 566     auto.
 567
 568     refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _).
 569     apply FreshMon.
 570     simpl.
 571     rewrite pf2.
 572     rewrite pf1.
 573     reflexivity.
 574     apply FreshMon.
 575
 576     apply ILeaf.
 577     apply ileaf in X1'.
 578     apply ileaf in X0'.
 579     simpl in *.
 580     apply ELet with (ev:=vnew)(tv:=σ₁).
 581     apply X0'.
 582     apply X1'.
 583     Defined.
 584
 585   Definition vartree Γ Δ Σ lev ξ :
 586     forall vars, Σ @@@ lev = mapOptionTree ξ vars ->
 587     ITree (HaskType Γ ★) (fun t : HaskType Γ ★ => Expr Γ Δ ξ t lev) Σ.
 588     induction Σ; intros.
 589     destruct a.
 590     intros; simpl in *.
 591     apply ILeaf.
 592     destruct vars; try destruct o; inversion H.
 593     set (EVar Γ Δ ξ v) as q.
 594     rewrite <- H1 in q.
 595     apply q.
 596     intros.
 597     apply INone.
 598     intros.
 599     destruct vars; try destruct o; inversion H.
 600     apply IBranch.
 601     eapply IHΣ1.
 602     apply H1.
 603     eapply IHΣ2.
 604     apply H2.
 605     Defined.
 606
 607
 608   Definition rdrop  Γ Δ Σ₁ Σ₁₂ a lev :
 609     ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a,,Σ₁₂ @ lev] ->
 610     ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
 611     intros.
 612     apply ileaf in X.
 613     apply ILeaf.
 614     simpl in *.
 615     intros.
 616     set (X ξ vars H) as q.
 617     simpl in q.
 618     refine (q >>>= fun q' => return _).
 619     apply FreshMon.
 620     inversion q'.
 621     apply X0.
 622     Defined.
 623
 624   Definition rdrop'  Γ Δ Σ₁ Σ₁₂ a lev :
 625     ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂,,a @ lev] ->
 626     ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
 627     intros.
 628     apply ileaf in X.
 629     apply ILeaf.
 630     simpl in *.
 631     intros.
 632     set (X ξ vars H) as q.
 633     simpl in q.
 634     refine (q >>>= fun q' => return _).
 635     apply FreshMon.
 636     inversion q'.
 637     auto.
 638     Defined.
 639
 640   Definition rdrop''  Γ Δ Σ₁ Σ₁₂ lev :
 641     ITree Judg judg2exprType [Γ > Δ > [],,Σ₁ |- Σ₁₂ @ lev] ->
 642     ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev].
 643     intros.
 644     apply ileaf in X.
 645     apply ILeaf.
 646     simpl in *; intros.
 647     eapply X with (vars:=[],,vars).
 648     rewrite H; reflexivity.
 649     Defined.
 650
 651   Definition rdrop'''  Γ Δ a Σ₁ Σ₁₂ lev :
 652     ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] ->
 653     ITree Judg judg2exprType [Γ > Δ > a,,Σ₁ |- Σ₁₂ @ lev].
 654     intros.
 655     apply ileaf in X.
 656     apply ILeaf.
 657     simpl in *; intros.
 658     destruct vars; try destruct o; inversion H.
 659     eapply X with (vars:=vars2).
 660     auto.
 661     Defined.
 662
 663   Definition rassoc  Γ Δ Σ₁ a b c lev :
 664     ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
 665     ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev].
 666     intros.
 667     apply ileaf in X.
 668     apply ILeaf.
 669     simpl in *; intros.
 670     destruct vars; try destruct o; inversion H.
 671     destruct vars2; try destruct o; inversion H2.
 672     apply X with (vars:=(vars1,,vars2_1),,vars2_2).
 673     subst; reflexivity.
 674     Defined.
 675
 676   Definition rassoc'  Γ Δ Σ₁ a b c lev :
 677     ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev] ->
 678     ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev].
 679     intros.
 680     apply ileaf in X.
 681     apply ILeaf.
 682     simpl in *; intros.
 683     destruct vars; try destruct o; inversion H.
 684     destruct vars1; try destruct o; inversion H1.
 685     apply X with (vars:=vars1_1,,(vars1_2,,vars2)).
 686     subst; reflexivity.
 687     Defined.
 688
 689   Definition swapr  Γ Δ Σ₁ a b c lev :
 690     ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
 691     ITree Judg judg2exprType [Γ > Δ > ((b,,a),,c) |- Σ₁ @ lev].
 692     intros.
 693     apply ileaf in X.
 694     apply ILeaf.
 695     simpl in *; intros.
 696     destruct vars; try destruct o; inversion H.
 697     destruct vars1; try destruct o; inversion H1.
 698     apply X with (vars:=(vars1_2,,vars1_1),,vars2).
 699     subst; reflexivity.
 700     Defined.
 701
 702   Definition rdup  Γ Δ Σ₁ a  c lev :
 703     ITree Judg judg2exprType [Γ > Δ > ((a,,a),,c) |- Σ₁ @ lev] ->
 704     ITree Judg judg2exprType [Γ > Δ > (a,,c) |- Σ₁ @ lev].
 705     intros.
 706     apply ileaf in X.
 707     apply ILeaf.
 708     simpl in *; intros.
 709     destruct vars; try destruct o; inversion H.
 710     apply X with (vars:=(vars1,,vars1),,vars2).    (* is this allowed? *)
 711     subst; reflexivity.
 712     Defined.
 713
 714   (* holy cow this is ugly *)
 715   Definition rcut Γ Δ  Σ₃ lev  Σ₁₂  :
 716     forall Σ₁ Σ₂,
 717     ITree Judg judg2exprType [Γ > Δ > Σ₁ |-  Σ₁₂ @ lev] ->
 718     ITree Judg judg2exprType [Γ > Δ >  Σ₁₂ @@@ lev,,Σ₂ |- [Σ₃] @ lev] ->
 719     ITree Judg judg2exprType [Γ > Δ > Σ₁,,Σ₂ |- [Σ₃] @ lev].
 720
 721     induction Σ₁₂.
 722     intros.
 723     destruct a.
 724
 725     eapply rlet.
 726     apply IBranch.
 727     apply X.
 728     apply X0.
 729
 730     simpl in X0.
 731     apply rdrop'' in X0.
 732     apply rdrop'''.
 733     apply X0.
 734
 735     intros.
 736     simpl in X0.
 737     apply rassoc in X0.
 738     set (IHΣ₁₂1 _ _ (rdrop  _ _ _ _ _ _ X) X0) as q.
 739     set (IHΣ₁₂2 _ (Σ₁,,Σ₂) (rdrop' _ _ _ _ _ _ X)) as q'.
 740     apply rassoc' in q.
 741     apply swapr in q.
 742     apply rassoc in q.
 743     set (q' q) as q''.
 744     apply rassoc' in q''.
 745     apply rdup in q''.
 746     apply q''.
 747     Defined.
 748
 749   Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
 750
 751     intros h j r.
 752
 753       refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
 754       | RArrange a b c d e l r        => let case_RURule := tt        in _
 755       | RNote   Γ Δ Σ τ l n           => let case_RNote := tt         in _
 756       | RLit    Γ Δ l     _           => let case_RLit := tt          in _
 757       | RVar    Γ Δ σ         p       => let case_RVar := tt          in _
 758       | RGlobal Γ Δ σ l wev           => let case_RGlobal := tt       in _
 759       | RLam    Γ Δ Σ tx te     x     => let case_RLam := tt          in _
 760       | RCast   Γ Δ Σ σ τ γ     x     => let case_RCast := tt         in _
 761       | RAbsT   Γ Δ Σ κ σ a           => let case_RAbsT := tt         in _
 762       | RAppT   Γ Δ Σ κ σ τ     y     => let case_RAppT := tt         in _
 763       | RAppCo  Γ Δ Σ κ σ₁ σ₂ γ σ l   => let case_RAppCo := tt        in _
 764       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
 765       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
 766       | RCut    Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l  => let case_RCut := tt          in _
 767       | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
 768       | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
 769       | RVoid   _ _ l                 => let case_RVoid := tt   in _
 770       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
 771       | REsc    Σ a b c n m           => let case_REsc := tt          in _
 772       | RCase   Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 773       | RLetRec Γ Δ lri x y t         => let case_RLetRec := tt       in _
 774       end); intro X_; try apply ileaf in X_; simpl in X_.
 775
 776     destruct case_RURule.
 777       apply ILeaf. simpl. intros.
 778       set (@urule2expr a b _ _ e l r0 ξ) as q.
 779       unfold ujudg2exprType.
 780       unfold ujudg2exprType in q.
 781       apply q with (vars:=vars).
 782       intros.
 783       apply X_ with (vars:=vars0).
 784       auto.
 785       auto.
 786
 787   destruct case_RBrak.
 788     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 789     apply EBrak.
 790     apply (ileaf X).
 791
 792   destruct case_REsc.
 793     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 794     apply EEsc.
 795     apply (ileaf X).
 796
 797   destruct case_RNote.
 798     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 799     apply ENote; auto.
 800     apply (ileaf X).
 801
 802   destruct case_RLit.
 803     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 804     apply ELit.
 805
 806   destruct case_RVar.
 807     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 808     destruct vars; simpl in H; inversion H; destruct o. inversion H1.
 809     set (@EVar _ _ _ Δ ξ v) as q.
 810     rewrite <- H2 in q.
 811     simpl in q.
 812     apply q.
 813     inversion H.
 814
 815   destruct case_RGlobal.
 816     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 817     apply EGlobal.
 818
 819   destruct case_RLam.
 820     apply ILeaf.
 821     simpl in *; intros.
 822     refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
 823     apply FreshMon.
 824     destruct pf as [ vnew [ pf1 pf2 ]].
 825     set (update_xi ξ x (((vnew, tx  )) :: nil)) as ξ' in *.
 826     refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
 827     apply FreshMon.
 828     simpl.
 829     rewrite pf1.
 830     rewrite <- pf2.
 831     simpl.
 832     reflexivity.
 833     intro hyp.
 834     refine (return _).
 835     apply ILeaf.
 836     apply ELam with (ev:=vnew).
 837     apply ileaf in hyp.
 838     simpl in hyp.
 839     unfold ξ' in hyp.
 840     apply hyp.
 841
 842   destruct case_RCast.
 843     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 844     eapply ECast.
 845     apply x.
 846     apply ileaf in X. simpl in X.
 847     apply X.
 848
 849   destruct case_RApp.
 850     apply ILeaf.
 851     inversion X_.
 852     inversion X.
 853     inversion X0.
 854     simpl in *.
 855     intros.
 856     destruct vars. try destruct o; inversion H.
 857     simpl in H.
 858     inversion H.
 859     set (X1 ξ vars1 H5) as q1.
 860     set (X2 ξ vars2 H6) as q2.
 861     refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
 862     apply FreshMon.
 863     apply FreshMon.
 864     apply ILeaf.
 865     apply ileaf in q1'.
 866     apply ileaf in q2'.
 867     simpl in *.
 868     apply (EApp _ _ _ _ _ _ q1' q2').
 869
 870   destruct case_RCut.
 871     apply rassoc.
 872     apply swapr.
 873     apply rassoc'.
 874
 875     inversion X_.
 876     subst.
 877     clear X_.
 878
 879     apply rassoc' in X0.
 880     apply swapr in X0.
 881     apply rassoc in X0.
 882
 883     induction Σ₃.
 884     destruct a.
 885     subst.
 886     eapply rcut.
 887     apply X.
 888     apply X0.
 889
 890     apply ILeaf.
 891     simpl.
 892     intros.
 893     refine (return _).
 894     apply INone.
 895     set (IHΣ₃1 (rdrop  _ _ _ _ _ _ X0)) as q1.
 896     set (IHΣ₃2 (rdrop' _ _ _ _ _ _ X0)) as q2.
 897     apply ileaf in q1.
 898     apply ileaf in q2.
 899     simpl in *.
 900     apply ILeaf.
 901     simpl.
 902     intros.
 903     refine (q1 _ _ H >>>= fun q1' => q2 _ _ H >>>= fun q2' => return _).
 904     apply FreshMon.
 905     apply FreshMon.
 906     apply IBranch; auto.
 907
 908   destruct case_RLeft.
 909     apply ILeaf.
 910     simpl; intros.
 911     destruct vars; try destruct o; inversion H.
 912     refine (X_ _ _ H2 >>>= fun X' => return _).
 913     apply FreshMon.
 914     apply IBranch.
 915     eapply vartree.
 916     apply H1.
 917     apply X'.
 918
 919   destruct case_RRight.
 920     apply ILeaf.
 921     simpl; intros.
 922     destruct vars; try destruct o; inversion H.
 923     refine (X_ _ _ H1 >>>= fun X' => return _).
 924     apply FreshMon.
 925     apply IBranch.
 926     apply X'.
 927     eapply vartree.
 928     apply H2.
 929
 930   destruct case_RVoid.
 931     apply ILeaf; simpl; intros.
 932     refine (return _).
 933     apply INone.
 934
 935   destruct case_RAppT.
 936     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 937     apply ETyApp.
 938     apply (ileaf X).
 939
 940   destruct case_RAbsT.
 941     apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 942     rewrite mapOptionTree_compose.
 943     rewrite <- H.
 944     reflexivity.
 945     apply ileaf in X. simpl in *.
 946     apply ETyLam.
 947     apply X.
 948
 949   destruct case_RAppCo.
 950     apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 951     auto.
 952     eapply ECoApp.
 953     apply γ.
 954     apply (ileaf X).
 955
 956   destruct case_RAbsCo.
 957     apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 958     auto.
 959     eapply ECoLam.
 960     apply (ileaf X).
 961
 962   destruct case_RLetRec.
 963     apply ILeaf; simpl; intros.
 964     refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
 965     destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
 966     refine (X_ ((update_xi ξ t (leaves varstypes)))
 967       ((mapOptionTree (@fst _ _) varstypes),,vars) _ >>>= fun X => return _); clear X_.  apply FreshMon.
 968     simpl.
 969     rewrite pf2.
 970     rewrite pf1.
 971     auto.
 972     apply ILeaf.
 973     inversion X; subst; clear X.
 974
 975     apply (@ELetRec _ _ _ _ _ _ _ varstypes).
 976     auto.
 977     apply (@letrec_helper Γ Δ t varstypes).
 978     rewrite mapOptionTree_compose.
 979     rewrite mapOptionTree_compose.
 980     rewrite pf2.
 981     replace ((mapOptionTree unlev (y @@@ t))) with y.
 982       apply X0.
 983       clear pf1 X0 X1 pfdist pf2 vars varstypes.
 984       induction y; try destruct a; auto.
 985       rewrite IHy1 at 1.
 986       rewrite IHy2 at 1.
 987       reflexivity.
 988     apply ileaf in X1.
 989     simpl in X1.
 990     apply X1.
 991
 992   destruct case_RCase.
 993     apply ILeaf; simpl; intros.
 994     inversion X_.
 995     clear X_.
 996     subst.
 997     apply ileaf in X0.
 998     simpl in X0.
 999
1000     (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
1001      * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
1002     rename Σ into body_freevars_types.
1003     rename vars into all_freevars.
1004     rename X0 into body_expr.
1005     rename X  into alts_exprs.
1006
1007     destruct all_freevars; try destruct o; inversion H.
1008     rename all_freevars2 into body_freevars.
1009     rename all_freevars1 into alts_freevars.
1010
1011     set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
1012     set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
1013     apply fix_indexing in alts_exprs'.
1014     simpl in alts_exprs'.
1015     apply unindex_tree in alts_exprs'.
1016     simpl in alts_exprs'.
1017     apply fix2 in alts_exprs'.
1018     apply treeM in alts_exprs'.
1019
1020     refine ( alts_exprs' >>>= fun Y =>
1021       body_expr ξ _ _
1022       >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
1023       apply FreshMon.
1024       apply FreshMon.
1025       apply H2.
1026     Defined.
1027
1028   Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
1029     match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
1030     | scnd_weak   _             => let case_nil    := tt in fun _ => INone _ _
1031     | scnd_comp   x h c cnd' r  => let case_rule   := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
1032     | scnd_branch _ _ _ c1 c2   => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
1033     end.
1034
1035   Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
1036     {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
1037     FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).
1038     intro pf.
1039     set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
1040     apply closed2expr in cnd.
1041     apply ileaf in cnd.
1042     simpl in *.
1043     clear pf.
1044     refine (bind ξvars = manyFresh _ Σ ξ0; _).
1045     apply FreshMon.
1046     destruct ξvars as [vars ξpf].
1047     destruct ξpf as [ξ pf].
1048     refine (cnd ξ vars _ >>>= fun it => _).
1049     apply FreshMon.
1050     auto.
1051     refine (return OK _).
1052     exists ξ.
1053     apply ileaf in it.
1054     simpl in it.
1055     apply it.
1056     apply INone.
1057     Defined.
1058
1059 End HaskProofToStrong.