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       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _
 767       | RCut    Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l    => let case_RCut := tt          in _
 768       | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
 769       | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
 770       | RWhere  Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p  => let case_RWhere := tt          in _
 771       | RJoin   Γ p lri m x q l       => let case_RJoin := tt in _
 772       | RVoid   _ _ l                 => let case_RVoid := tt   in _
 773       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
 774       | REsc    Σ a b c n m           => let case_REsc := tt          in _
 775       | RCase   Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 776       | RLetRec Γ Δ lri x y t         => let case_RLetRec := tt       in _
 777       end); intro X_; try apply ileaf in X_; simpl in X_.
 778
 779     destruct case_RURule.
 780       apply ILeaf. simpl. intros.
 781       set (@urule2expr a b _ _ e l r0 ξ) as q.
 782       unfold ujudg2exprType.
 783       unfold ujudg2exprType in q.
 784       apply q with (vars:=vars).
 785       intros.
 786       apply X_ with (vars:=vars0).
 787       auto.
 788       auto.
 789
 790   destruct case_RBrak.
 791     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 792     apply EBrak.
 793     apply (ileaf X).
 794
 795   destruct case_REsc.
 796     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 797     apply EEsc.
 798     apply (ileaf X).
 799
 800   destruct case_RNote.
 801     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 802     apply ENote; auto.
 803     apply (ileaf X).
 804
 805   destruct case_RLit.
 806     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 807     apply ELit.
 808
 809   destruct case_RVar.
 810     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 811     destruct vars; simpl in H; inversion H; destruct o. inversion H1.
 812     set (@EVar _ _ _ Δ ξ v) as q.
 813     rewrite <- H2 in q.
 814     simpl in q.
 815     apply q.
 816     inversion H.
 817
 818   destruct case_RGlobal.
 819     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 820     apply EGlobal.
 821
 822   destruct case_RLam.
 823     apply ILeaf.
 824     simpl in *; intros.
 825     refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
 826     apply FreshMon.
 827     destruct pf as [ vnew [ pf1 pf2 ]].
 828     set (update_xi ξ x (((vnew, tx  )) :: nil)) as ξ' in *.
 829     refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
 830     apply FreshMon.
 831     simpl.
 832     rewrite pf1.
 833     rewrite <- pf2.
 834     simpl.
 835     reflexivity.
 836     intro hyp.
 837     refine (return _).
 838     apply ILeaf.
 839     apply ELam with (ev:=vnew).
 840     apply ileaf in hyp.
 841     simpl in hyp.
 842     unfold ξ' in hyp.
 843     apply hyp.
 844
 845   destruct case_RCast.
 846     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 847     eapply ECast.
 848     apply x.
 849     apply ileaf in X. simpl in X.
 850     apply X.
 851
 852   destruct case_RJoin.
 853     apply ILeaf; simpl; intros.
 854     inversion X_.
 855     apply ileaf in X.
 856     apply ileaf in X0.
 857     simpl in *.
 858     destruct vars; inversion H.
 859     destruct o; inversion H3.
 860     refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
 861     apply FreshMon.
 862     apply FreshMon.
 863     apply IBranch; auto.
 864
 865   destruct case_RApp.
 866     apply ILeaf.
 867     inversion X_.
 868     inversion X.
 869     inversion X0.
 870     simpl in *.
 871     intros.
 872     destruct vars. try destruct o; inversion H.
 873     simpl in H.
 874     inversion H.
 875     set (X1 ξ vars1 H5) as q1.
 876     set (X2 ξ vars2 H6) as q2.
 877     refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
 878     apply FreshMon.
 879     apply FreshMon.
 880     apply ILeaf.
 881     apply ileaf in q1'.
 882     apply ileaf in q2'.
 883     simpl in *.
 884     apply (EApp _ _ _ _ _ _ q1' q2').
 885
 886   destruct case_RLet.
 887     eapply rlet.
 888     apply X_.
 889
 890   destruct case_RWhere.
 891     apply ILeaf.
 892     simpl in *; intros.
 893     destruct vars;  try destruct o; inversion H.
 894     destruct vars2; try destruct o; inversion H2.
 895     clear H2.
 896
 897     assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto.
 898     refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)).
 899     apply FreshMon.
 900
 901     destruct pf as [ vnew [ pf1 pf2 ]].
 902     set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
 903     inversion X_.
 904     apply ileaf in X.
 905     apply ileaf in X0.
 906     simpl in *.
 907
 908     refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _).
 909     apply FreshMon.
 910     simpl.
 911     inversion pf1.
 912     rewrite H3.
 913     rewrite H4.
 914     rewrite pf2.
 915     reflexivity.
 916
 917     refine (X0 ξ vars2_1 _ >>>= fun X1' => _).
 918     apply FreshMon.
 919     reflexivity.
 920     apply FreshMon.
 921
 922     apply ILeaf.
 923     apply ileaf in X0'.
 924     apply ileaf in X1'.
 925     simpl in *.
 926     apply ELet with (ev:=vnew)(tv:=σ₁).
 927     apply X1'.
 928     apply X0'.
 929
 930   destruct case_RCut.
 931     inversion X_.
 932     subst.
 933     clear X_.
 934     induction Σ₃.
 935     destruct a.
 936     subst.
 937     eapply rcut.
 938     apply X.
 939     apply X0.
 940
 941     apply ILeaf.
 942     simpl.
 943     intros.
 944     refine (return _).
 945     apply INone.
 946     set (IHΣ₃1 (rdrop  _ _ _ _ _ _ X0)) as q1.
 947     set (IHΣ₃2 (rdrop' _ _ _ _ _ _ X0)) as q2.
 948     apply ileaf in q1.
 949     apply ileaf in q2.
 950     simpl in *.
 951     apply ILeaf.
 952     simpl.
 953     intros.
 954     refine (q1 _ _ H >>>= fun q1' => q2 _ _ H >>>= fun q2' => return _).
 955     apply FreshMon.
 956     apply FreshMon.
 957     apply IBranch; auto.
 958
 959   destruct case_RLeft.
 960     apply ILeaf.
 961     simpl; intros.
 962     destruct vars; try destruct o; inversion H.
 963     refine (X_ _ _ H2 >>>= fun X' => return _).
 964     apply FreshMon.
 965     apply IBranch.
 966     eapply vartree.
 967     apply H1.
 968     apply X'.
 969
 970   destruct case_RRight.
 971     apply ILeaf.
 972     simpl; intros.
 973     destruct vars; try destruct o; inversion H.
 974     refine (X_ _ _ H1 >>>= fun X' => return _).
 975     apply FreshMon.
 976     apply IBranch.
 977     apply X'.
 978     eapply vartree.
 979     apply H2.
 980
 981   destruct case_RVoid.
 982     apply ILeaf; simpl; intros.
 983     refine (return _).
 984     apply INone.
 985
 986   destruct case_RAppT.
 987     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 988     apply ETyApp.
 989     apply (ileaf X).
 990
 991   destruct case_RAbsT.
 992     apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 993     rewrite mapOptionTree_compose.
 994     rewrite <- H.
 995     reflexivity.
 996     apply ileaf in X. simpl in *.
 997     apply ETyLam.
 998     apply X.
 999
1000   destruct case_RAppCo.
1001     apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
1002     auto.
1003     eapply ECoApp.
1004     apply γ.
1005     apply (ileaf X).
1006
1007   destruct case_RAbsCo.
1008     apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
1009     auto.
1010     eapply ECoLam.
1011     apply (ileaf X).
1012
1013   destruct case_RLetRec.
1014     apply ILeaf; simpl; intros.
1015     refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
1016     destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
1017     refine (X_ ((update_xi ξ t (leaves varstypes)))
1018       (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_.  apply FreshMon.
1019     simpl.
1020     rewrite pf2.
1021     rewrite pf1.
1022     auto.
1023     apply ILeaf.
1024     inversion X; subst; clear X.
1025
1026     apply (@ELetRec _ _ _ _ _ _ _ varstypes).
1027     auto.
1028     apply (@letrec_helper Γ Δ t varstypes).
1029     rewrite mapOptionTree_compose.
1030     rewrite mapOptionTree_compose.
1031     rewrite pf2.
1032     replace ((mapOptionTree unlev (y @@@ t))) with y.
1033       apply X0.
1034       clear pf1 X0 X1 pfdist pf2 vars varstypes.
1035       induction y; try destruct a; auto.
1036       rewrite IHy1 at 1.
1037       rewrite IHy2 at 1.
1038       reflexivity.
1039     apply ileaf in X1.
1040     simpl in X1.
1041     apply X1.
1042
1043   destruct case_RCase.
1044     apply ILeaf; simpl; intros.
1045     inversion X_.
1046     clear X_.
1047     subst.
1048     apply ileaf in X0.
1049     simpl in X0.
1050
1051     (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
1052      * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
1053     rename Σ into body_freevars_types.
1054     rename vars into all_freevars.
1055     rename X0 into body_expr.
1056     rename X  into alts_exprs.
1057
1058     destruct all_freevars; try destruct o; inversion H.
1059     rename all_freevars2 into body_freevars.
1060     rename all_freevars1 into alts_freevars.
1061
1062     set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
1063     set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
1064     apply fix_indexing in alts_exprs'.
1065     simpl in alts_exprs'.
1066     apply unindex_tree in alts_exprs'.
1067     simpl in alts_exprs'.
1068     apply fix2 in alts_exprs'.
1069     apply treeM in alts_exprs'.
1070
1071     refine ( alts_exprs' >>>= fun Y =>
1072       body_expr ξ _ _
1073       >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
1074       apply FreshMon.
1075       apply FreshMon.
1076       apply H2.
1077     Defined.
1078
1079   Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
1080     match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
1081     | scnd_weak   _             => let case_nil    := tt in fun _ => INone _ _
1082     | scnd_comp   x h c cnd' r  => let case_rule   := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
1083     | scnd_branch _ _ _ c1 c2   => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
1084     end.
1085
1086   Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
1087     {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
1088     FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).
1089     intro pf.
1090     set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
1091     apply closed2expr in cnd.
1092     apply ileaf in cnd.
1093     simpl in *.
1094     clear pf.
1095     refine (bind ξvars = manyFresh _ Σ ξ0; _).
1096     apply FreshMon.
1097     destruct ξvars as [vars ξpf].
1098     destruct ξpf as [ξ pf].
1099     refine (cnd ξ vars _ >>>= fun it => _).
1100     apply FreshMon.
1101     auto.
1102     refine (return OK _).
1103     exists ξ.
1104     apply ileaf in it.
1105     simpl in it.
1106     apply it.
1107     apply INone.
1108     Defined.
1109
1110 End HaskProofToStrong.