src/HaskProofToStrong.v

   1 (*********************************************************************************************************************************)
   2 (* HaskProofToStrong: convert HaskProof to HaskStrong                                                                            *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import NaturalDeduction.
   9 Require Import Coq.Strings.String.
  10 Require Import Coq.Lists.List.
  11 Require Import Coq.Init.Specif.
  12 Require Import HaskKinds.
  13 Require Import HaskStrongTypes.
  14 Require Import HaskStrong.
  15 Require Import HaskProof.
  16
  17 Section HaskProofToStrong.
  18
  19   Context {VV:Type} {eqdec_vv:EqDecidable VV} {freshM:FreshMonad VV}.
  20
  21   Definition fresh := FMT_fresh freshM.
  22   Definition FreshM := FMT freshM.
  23   Definition FreshMon := FMT_Monad freshM.
  24   Existing Instance FreshMon.
  25
  26   Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★.
  27
  28   Definition ujudg2exprType {Γ}{Δ}(ξ:ExprVarResolver Γ)(j:UJudg Γ Δ) : Type :=
  29     match j with
  30       mkUJudg Σ τ => forall vars, Σ = mapOptionTree ξ vars ->
  31         FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
  32       end.
  33
  34   Definition judg2exprType (j:Judg) : Type :=
  35     match j with
  36       (Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
  37         FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
  38       end.
  39
  40   Definition justOne Γ Δ ξ τ : ITree _ (fun t => Expr Γ Δ ξ t) [τ] -> Expr Γ Δ ξ τ.
  41     intros.
  42     inversion X; auto.
  43     Defined.
  44
  45   Definition ileaf `(it:ITree X F [t]) : F t.
  46     inversion it.
  47     apply X0.
  48     Defined.
  49
  50   Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q,
  51     update_ξ ξ lev (app l1 l2) q = update_ξ (update_ξ ξ lev l2) lev l1 q.
  52     intros.
  53     induction l1.
  54       reflexivity.
  55       simpl.
  56       destruct a; simpl.
  57       rewrite IHl1.
  58       reflexivity.
  59       Qed.
  60
  61    Lemma quark {T} (l1:list T) l2 vf :
  62       (In vf (app l1 l2)) <->
  63        (In vf l1) \/ (In vf l2).
  64      induction l1.
  65      simpl; auto.
  66      split; intro.
  67      right; auto.
  68      inversion H.
  69      inversion H0.
  70      auto.
  71      split.
  72
  73      destruct IHl1.
  74      simpl in *.
  75      intro.
  76      destruct H1.
  77      left; left; auto.
  78      set (H H1) as q.
  79      destruct q.
  80      left; right; auto.
  81      right; auto.
  82      simpl.
  83
  84      destruct IHl1.
  85      simpl in *.
  86      intro.
  87      destruct H1.
  88      destruct H1.
  89      left; auto.
  90      right; apply H0; auto.
  91      right; apply H0; auto.
  92    Qed.
  93
  94   Lemma splitter {T} (l1:list T) l2 vf :
  95       (In vf (app l1 l2) → False)
  96       -> (In vf l1 → False)  /\ (In vf l2 → False).
  97     intros.
  98     split; intros; apply H; rewrite quark.
  99     auto.
 100     auto.
 101     Qed.
 102
 103   Lemma helper
 104     : forall T Z {eqdt:EqDecidable T}(tl:Tree ??T)(vf:T) ξ (q:Z),
 105       (In vf (leaves tl) -> False) ->
 106       mapOptionTree (fun v' => if eqd_dec vf v' then q else ξ v') tl =
 107       mapOptionTree ξ tl.
 108     intros.
 109     induction tl;
 110       try destruct a;
 111         simpl in *.
 112     set (eqd_dec vf t) as x in *.
 113     destruct x.
 114     subst.
 115       assert False.
 116       apply H.
 117       left; auto.
 118       inversion H0.
 119     auto.
 120     auto.
 121     apply splitter in H.
 122     destruct H.
 123     rewrite (IHtl1 H).
 124     rewrite (IHtl2 H0).
 125     reflexivity.
 126     Qed.
 127
 128   Lemma fresh_lemma'' Γ
 129     : forall types ξ lev,
 130     FreshM { varstypes : _
 131       |  mapOptionTree (update_ξ(Γ:=Γ)   ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
 132       /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
 133   admit.
 134   Defined.
 135
 136   Lemma fresh_lemma' Γ
 137     : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars ->
 138     FreshM { varstypes : _
 139       |  mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
 140       /\ mapOptionTree (update_ξ       ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
 141       /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
 142     induction types.
 143       intros; destruct a.
 144         refine (bind vf = fresh (leaves vars) ; return _).
 145           apply FreshMon.
 146           destruct vf as [ vf vf_pf ].
 147           exists [(vf,h)].
 148           split; auto.
 149           simpl.
 150           set (helper VV _ vars vf ξ (h@@lev) vf_pf) as q.
 151           rewrite q.
 152           symmetry; auto.
 153           simpl.
 154           destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto.
 155           split; auto.
 156           apply distinct_cons.
 157           intro.
 158           inversion H0.
 159           apply distinct_nil.
 160         refine (return _).
 161           exists []; auto.
 162           split.
 163           simpl.
 164           symmetry; auto.
 165           split.
 166           simpl.
 167           reflexivity.
 168           simpl.
 169           apply distinct_nil.
 170         intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _).
 171           apply FreshMon.
 172           destruct x2 as [vt2 [pf21 [pf22 pfdist]]].
 173           refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_ξ ξ lev
 174             (leaves vt2)) _ _; return _).
 175           apply FreshMon.
 176           simpl.
 177           rewrite pf21.
 178           rewrite pf22.
 179           reflexivity.
 180           clear IHtypes1 IHtypes2.
 181           destruct x1 as [vt1 [pf11 pf12]].
 182           exists (vt1,,vt2); split; auto.
 183
 184           set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
 185           set (mapOptionTree_extensional _ _ q) as q'.
 186           rewrite q'.
 187           clear q' q.
 188           inversion pf11.
 189           reflexivity.
 190
 191           simpl.
 192           set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
 193           set (mapOptionTree_extensional _ _ q) as q'.
 194           rewrite q'.
 195           rewrite q'.
 196           clear q' q.
 197           rewrite <- mapOptionTree_compose.
 198           rewrite <- mapOptionTree_compose.
 199           rewrite <- mapOptionTree_compose in *.
 200           split.
 201           destruct pf12.
 202           rewrite H.
 203           inversion pf11.
 204           rewrite <- mapOptionTree_compose.
 205           reflexivity.
 206
 207           admit.
 208         Defined.
 209
 210   Lemma fresh_lemma Γ ξ vars Σ Σ' lev
 211     : Σ = mapOptionTree ξ vars ->
 212     FreshM { vars' : _
 213       |  mapOptionTree (update_ξ(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
 214       /\ mapOptionTree (update_ξ ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
 215     intros.
 216     set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
 217     refine (q >>>= fun q' => return _).
 218     apply FreshMon.
 219     clear q.
 220     destruct q' as [varstypes [pf1 [pf2 pfdist]]].
 221     destruct varstypes; try destruct o; try destruct p; simpl in *.
 222       destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
 223       inversion pf2; subst.
 224       exists v.
 225       destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
 226       split; auto.
 227       inversion pf2.
 228       inversion pf2.
 229     Defined.
 230
 231   Definition urule2expr  : forall Γ Δ h j (r:@URule Γ Δ h j) (ξ:VV -> LeveledHaskType Γ ★),
 232     ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j.
 233
 234       refine (fix urule2expr Γ Δ h j (r:@URule Γ Δ h j) ξ {struct r} :
 235         ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j :=
 236         match r as R in URule H C return ITree _ (ujudg2exprType ξ) H -> ITree _ (ujudg2exprType ξ) C with
 237           | RLeft   h c ctx r => let case_RLeft  := tt in (fun e => _) (urule2expr _ _ _ _ r)
 238           | RRight  h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r)
 239           | RCanL   t a       => let case_RCanL  := tt in _
 240           | RCanR   t a       => let case_RCanR  := tt in _
 241           | RuCanL  t a       => let case_RuCanL := tt in _
 242           | RuCanR  t a       => let case_RuCanR := tt in _
 243           | RAssoc  t a b c   => let case_RAssoc := tt in _
 244           | RCossa  t a b c   => let case_RCossa := tt in _
 245           | RExch   t a b     => let case_RExch  := tt in _
 246           | RWeak   t a       => let case_RWeak  := tt in _
 247           | RCont   t a       => let case_RCont  := tt in _
 248           end); clear urule2expr; intros.
 249
 250       destruct case_RCanL.
 251         apply ILeaf; simpl; intros.
 252         inversion X.
 253         simpl in X0.
 254         apply (X0 ([],,vars)).
 255         simpl; rewrite <- H; auto.
 256
 257       destruct case_RCanR.
 258         apply ILeaf; simpl; intros.
 259         inversion X.
 260         simpl in X0.
 261         apply (X0 (vars,,[])).
 262         simpl; rewrite <- H; auto.
 263
 264       destruct case_RuCanL.
 265         apply ILeaf; simpl; intros.
 266         destruct vars; try destruct o; inversion H.
 267         inversion X.
 268         simpl in X0.
 269         apply (X0 vars2); auto.
 270
 271       destruct case_RuCanR.
 272         apply ILeaf; simpl; intros.
 273         destruct vars; try destruct o; inversion H.
 274         inversion X.
 275         simpl in X0.
 276         apply (X0 vars1); auto.
 277
 278       destruct case_RAssoc.
 279         apply ILeaf; simpl; intros.
 280         inversion X.
 281         simpl in X0.
 282         destruct vars; try destruct o; inversion H.
 283         destruct vars1; try destruct o; inversion H.
 284         apply (X0 (vars1_1,,(vars1_2,,vars2))).
 285         subst; auto.
 286
 287       destruct case_RCossa.
 288         apply ILeaf; simpl; intros.
 289         inversion X.
 290         simpl in X0.
 291         destruct vars; try destruct o; inversion H.
 292         destruct vars2; try destruct o; inversion H.
 293         apply (X0 ((vars1,,vars2_1),,vars2_2)).
 294         subst; auto.
 295
 296       destruct case_RLeft.
 297         destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
 298         destruct o; [ idtac | apply INone ].
 299         destruct u; simpl in *.
 300         apply ILeaf; simpl; intros.
 301         destruct vars; try destruct o; inversion H.
 302         set (fun q => ileaf (e ξ q)) as r'.
 303         simpl in r'.
 304         apply r' with (vars:=vars2).
 305         clear r' e.
 306         clear r0.
 307         induction h0.
 308           destruct a.
 309           destruct u.
 310           simpl in X.
 311           apply ileaf in X.
 312           apply ILeaf.
 313           simpl.
 314           simpl in X.
 315           intros.
 316           apply X with (vars:=vars1,,vars).
 317           simpl.
 318           rewrite H0.
 319           rewrite H1.
 320           reflexivity.
 321           apply INone.
 322           apply IBranch.
 323           apply IHh0_1. inversion X; auto.
 324           apply IHh0_2. inversion X; auto.
 325           auto.
 326
 327       destruct case_RRight.
 328         destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
 329         destruct o; [ idtac | apply INone ].
 330         destruct u; simpl in *.
 331         apply ILeaf; simpl; intros.
 332         destruct vars; try destruct o; inversion H.
 333         set (fun q => ileaf (e ξ q)) as r'.
 334         simpl in r'.
 335         apply r' with (vars:=vars1).
 336         clear r' e.
 337         clear r0.
 338         induction h0.
 339           destruct a.
 340           destruct u.
 341           simpl in X.
 342           apply ileaf in X.
 343           apply ILeaf.
 344           simpl.
 345           simpl in X.
 346           intros.
 347           apply X with (vars:=vars,,vars2).
 348           simpl.
 349           rewrite H0.
 350           rewrite H2.
 351           reflexivity.
 352           apply INone.
 353           apply IBranch.
 354           apply IHh0_1. inversion X; auto.
 355           apply IHh0_2. inversion X; auto.
 356           auto.
 357
 358       destruct case_RExch.
 359         apply ILeaf; simpl; intros.
 360         inversion X.
 361         simpl in X0.
 362         destruct vars; try destruct o; inversion H.
 363         apply (X0 (vars2,,vars1)).
 364         inversion H; subst; auto.
 365
 366       destruct case_RWeak.
 367         apply ILeaf; simpl; intros.
 368         inversion X.
 369         simpl in X0.
 370         apply (X0 []).
 371         auto.
 372
 373       destruct case_RCont.
 374         apply ILeaf; simpl; intros.
 375         inversion X.
 376         simpl in X0.
 377         apply (X0 (vars,,vars)).
 378         simpl.
 379         rewrite <- H.
 380         auto.
 381         Defined.
 382
 383   Definition bridge Γ Δ (c:Tree ??(UJudg Γ Δ)) ξ :
 384     ITree Judg judg2exprType (mapOptionTree UJudg2judg c) -> ITree (UJudg Γ Δ) (ujudg2exprType ξ) c.
 385     intro it.
 386     induction c.
 387     destruct a.
 388       destruct u; simpl in *.
 389       apply ileaf in it.
 390       apply ILeaf.
 391       simpl in *.
 392       intros; apply it with (vars:=vars); auto.
 393     apply INone.
 394     apply IBranch; [ apply IHc1 | apply IHc2 ]; inversion it; auto.
 395     Defined.
 396
 397   Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
 398     ITree (LeveledHaskType Γ ★)
 399          (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
 400          (mapOptionTree (ξ' ○ (@fst _ _)) varstypes)
 401          -> ELetRecBindings Γ Δ ξ' l varstypes.
 402     intros.
 403     induction varstypes.
 404     destruct a; simpl in *.
 405     destruct p.
 406     simpl.
 407     apply ileaf in X. simpl in X.
 408       apply ELR_leaf.
 409       rename h into τ.
 410       destruct (eqd_dec (unlev (ξ' v)) τ).
 411       rewrite <- e.
 412       destruct (ξ' v).
 413       simpl.
 414       destruct (eqd_dec h0 l).
 415         rewrite <- e0.
 416         apply X.
 417       apply (Prelude_error "level mismatch; should never happen").
 418       apply (Prelude_error "letrec type mismatch; should never happen").
 419
 420     apply ELR_nil.
 421     apply ELR_branch.
 422       apply IHvarstypes1; inversion X; auto.
 423       apply IHvarstypes2; inversion X; auto.
 424     Defined.
 425
 426   Definition unindex_tree {V}{F} : forall {t:Tree ??V}, ITree V F t -> Tree ??{ v:V & F v }.
 427     refine (fix rec t it := match it as IT return Tree ??{ v:V & F v } with
 428       | INone => T_Leaf None
 429       | ILeaf x y => T_Leaf (Some _)
 430       | IBranch _ _ b1 b2 => (rec _ b1),,(rec _ b2)
 431             end).
 432     exists x; auto.
 433     Defined.
 434
 435   Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x })
 436     :  ITree { x:X & F x } (fun x => J (projT1 x))                                t
 437     -> ITree X             (fun x:X => J x)   (mapOptionTree (@projT1 _ _) t).
 438     intro it.
 439     induction it; simpl in *.
 440     apply INone.
 441     apply ILeaf.
 442     apply f.
 443     simpl; apply IBranch; auto.
 444     Defined.
 445
 446   Definition fix2 {X}{F} : Tree ??{ x:X & FreshM (F x) } -> Tree ??(FreshM { x:X & F x }).
 447     refine (fix rec t := match t with
 448       | T_Leaf None => T_Leaf None
 449       | T_Leaf (Some x) => T_Leaf (Some _)
 450       | T_Branch b1 b2 => T_Branch (rec b1) (rec b2)
 451             end).
 452     destruct x as [x fx].
 453     refine (bind fx' = fx ; return _).
 454     apply FreshMon.
 455     exists x.
 456     apply fx'.
 457     Defined.
 458
 459   Definition case_helper tc Γ Δ lev tbranches avars ξ :
 460     forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac},
 461      prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
 462      ((fun sac => FreshM
 463        { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
 464          & Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars (weakCK'' Δ)) (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@  lev)) }) (projT1 pcb)).
 465     intro pcb.
 466     intro X.
 467     simpl in X.
 468     simpl.
 469     destruct pcb as [sac pcb].
 470     simpl in *.
 471
 472     destruct X.
 473     destruct s as [vars vars_pf].
 474
 475     refine (bind localvars = fresh_lemma' _ (unleaves  (vec2list (sac_types sac _ avars))) vars
 476       (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _  ; _).
 477       apply FreshMon.
 478       rewrite vars_pf.
 479       rewrite <- mapOptionTree_compose.
 480       reflexivity.
 481       destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]].
 482       set (mapOptionTree (@fst _ _) localvars) as localvars'.
 483
 484     set (list2vec (leaves localvars')) as localvars''.
 485     cut (length (leaves localvars') = sac_numExprVars sac). intro H''.
 486       rewrite H'' in localvars''.
 487     cut (distinct (vec2list localvars'')). intro H'''.
 488     set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
 489
 490     refine (bind q = (f (scbwv_ξ scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
 491       apply FreshMon.
 492       simpl.
 493       unfold scbwv_ξ.
 494       rewrite vars_pf.
 495       rewrite <- mapOptionTree_compose.
 496       clear localvars_pf1.
 497       simpl.
 498       rewrite mapleaves'.
 499
 500     admit.
 501
 502     exists scb.
 503     apply ileaf in q.
 504     apply q.
 505
 506     admit.
 507     admit.
 508     Defined.
 509
 510   Fixpoint treeM {T}(t:Tree ??(FreshM T)) : FreshM (Tree ??T) :=
 511     match t with
 512       | T_Leaf None     => return []
 513       | T_Leaf (Some x) => bind x' = x ; return [x']
 514       | T_Branch b1 b2  => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2')
 515     end.
 516
 517   Definition gather_branch_variables
 518     Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
 519                 ProofCaseBranch tc Γ Δ lev tbranches avars sac})
 520     :
 521     forall vars,
 522     mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
 523     -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
 524     -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q)))
 525       { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
 526   alts.
 527     induction alts;
 528     intro vars;
 529     intro pf;
 530     intro source.
 531     destruct a; [ idtac | apply INone ].
 532     simpl in *.
 533     apply ileaf in source.
 534     apply ILeaf.
 535     destruct s as [sac pcb].
 536     simpl in *.
 537     split.
 538     intros.
 539     eapply source.
 540     apply H.
 541     clear source.
 542
 543     exists vars.
 544     auto.
 545
 546     simpl in pf.
 547     destruct vars; try destruct o; simpl in pf; inversion pf.
 548     simpl in source.
 549     inversion source.
 550     subst.
 551     apply IBranch.
 552     apply (IHalts1 vars1 H0 X); auto.
 553     apply (IHalts2 vars2 H1 X0); auto.
 554
 555     Defined.
 556
 557
 558   Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
 559
 560     intros h j r.
 561
 562       refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
 563       | RURule a b c d e              => let case_RURule := tt        in _
 564       | RNote   Γ Δ Σ τ l n           => let case_RNote := tt         in _
 565       | RLit    Γ Δ l     _           => let case_RLit := tt          in _
 566       | RVar    Γ Δ σ         p       => let case_RVar := tt          in _
 567       | RGlobal Γ Δ σ l wev           => let case_RGlobal := tt       in _
 568       | RLam    Γ Δ Σ tx te     x     => let case_RLam := tt          in _
 569       | RCast   Γ Δ Σ σ τ γ     x     => let case_RCast := tt         in _
 570       | RAbsT   Γ Δ Σ κ σ a           => let case_RAbsT := tt         in _
 571       | RAppT   Γ Δ Σ κ σ τ     y     => let case_RAppT := tt         in _
 572       | RAppCo  Γ Δ Σ κ σ₁ σ₂ γ σ l   => let case_RAppCo := tt        in _
 573       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
 574       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
 575       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _
 576       | RBindingGroup Γ p lri m x q   => let case_RBindingGroup := tt in _
 577       | REmptyGroup _ _               => let case_REmptyGroup := tt   in _
 578       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
 579       | REsc    Σ a b c n m           => let case_REsc := tt          in _
 580       | RCase   Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 581       | RLetRec Γ Δ lri x y t         => let case_RLetRec := tt       in _
 582       end); intro X_; try apply ileaf in X_; simpl in X_.
 583
 584   destruct case_RURule.
 585     destruct d; try destruct o.
 586       apply ILeaf; destruct u; simpl; intros.
 587       set (@urule2expr a b _ _ e ξ) as q.
 588       set (fun z => ileaf (q z)) as q'.
 589       simpl in q'.
 590       apply q' with (vars:=vars).
 591       clear q' q.
 592       apply bridge.
 593       apply X_.
 594       auto.
 595       apply no_urules_with_empty_conclusion in e; inversion e; auto.
 596       apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; auto.
 597
 598   destruct case_RBrak.
 599     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 600     apply EBrak.
 601     apply (ileaf X).
 602
 603   destruct case_REsc.
 604     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 605     apply EEsc.
 606     apply (ileaf X).
 607
 608   destruct case_RNote.
 609     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 610     apply ENote; auto.
 611     apply (ileaf X).
 612
 613   destruct case_RLit.
 614     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 615     apply ELit.
 616
 617   destruct case_RVar.
 618     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 619     destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
 620     apply EVar.
 621     inversion H.
 622
 623   destruct case_RGlobal.
 624     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
 625     apply EGlobal.
 626     apply wev.
 627
 628   destruct case_RLam.
 629     apply ILeaf.
 630     simpl in *; intros.
 631     refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
 632     apply FreshMon.
 633     destruct pf as [ vnew [ pf1 pf2 ]].
 634     set (update_ξ ξ x ((⟨vnew, tx  ⟩) :: nil)) as ξ' in *.
 635     refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
 636     apply FreshMon.
 637     simpl.
 638     rewrite pf1.
 639     rewrite <- pf2.
 640     simpl.
 641     reflexivity.
 642     intro hyp.
 643     refine (return _).
 644     apply ILeaf.
 645     apply ELam with (ev:=vnew).
 646     apply ileaf in hyp.
 647     simpl in hyp.
 648     unfold ξ' in hyp.
 649     apply hyp.
 650
 651   destruct case_RCast.
 652     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 653     eapply ECast.
 654     apply x.
 655     apply ileaf in X. simpl in X.
 656     apply X.
 657
 658   destruct case_RBindingGroup.
 659     apply ILeaf; simpl; intros.
 660     inversion X_.
 661     apply ileaf in X.
 662     apply ileaf in X0.
 663     simpl in *.
 664     destruct vars; inversion H.
 665     destruct o; inversion H3.
 666     refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
 667     apply FreshMon.
 668     apply FreshMon.
 669     apply IBranch; auto.
 670
 671   destruct case_RApp.
 672     apply ILeaf.
 673     inversion X_.
 674     inversion X.
 675     inversion X0.
 676     simpl in *.
 677     intros.
 678     destruct vars. try destruct o; inversion H.
 679     simpl in H.
 680     inversion H.
 681     set (X1 ξ vars1 H5) as q1.
 682     set (X2 ξ vars2 H6) as q2.
 683     refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
 684     apply FreshMon.
 685     apply FreshMon.
 686     apply ILeaf.
 687     apply ileaf in q1'.
 688     apply ileaf in q2'.
 689     simpl in *.
 690     apply (EApp _ _ _ _ _ _ q1' q2').
 691
 692   destruct case_RLet.
 693     apply ILeaf.
 694     simpl in *; intros.
 695     destruct vars; try destruct o; inversion H.
 696     refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
 697     apply FreshMon.
 698     destruct pf as [ vnew [ pf1 pf2 ]].
 699     set (update_ξ ξ p ((⟨vnew, σ₂  ⟩) :: nil)) as ξ' in *.
 700     inversion X_.
 701     apply ileaf in X.
 702     apply ileaf in X0.
 703     simpl in *.
 704     refine (X0 ξ  vars2 _ >>>= fun X0' => _).
 705     apply FreshMon.
 706     auto.
 707     refine (X  ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
 708     apply FreshMon.
 709     rewrite H1.
 710     simpl.
 711     rewrite pf2.
 712     rewrite pf1.
 713     rewrite H1.
 714     reflexivity.
 715     refine (return _).
 716     apply ILeaf.
 717     apply ileaf in X0'.
 718     apply ileaf in X1'.
 719     simpl in *.
 720     apply ELet with (ev:=vnew)(tv:=σ₂).
 721     apply X0'.
 722     apply X1'.
 723
 724   destruct case_REmptyGroup.
 725     apply ILeaf; simpl; intros.
 726     refine (return _).
 727     apply INone.
 728
 729   destruct case_RAppT.
 730     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
 731     apply ETyApp.
 732     apply (ileaf X).
 733
 734   destruct case_RAbsT.
 735     apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 736     rewrite mapOptionTree_compose.
 737     rewrite <- H.
 738     reflexivity.
 739     apply ileaf in X. simpl in *.
 740     apply ETyLam.
 741     apply X.
 742
 743   destruct case_RAppCo.
 744     apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 745     auto.
 746     eapply ECoApp.
 747     apply γ.
 748     apply (ileaf X).
 749
 750   destruct case_RAbsCo.
 751     apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
 752     auto.
 753     eapply ECoLam.
 754     apply (ileaf X).
 755
 756   destruct case_RLetRec.
 757     apply ILeaf; simpl; intros.
 758     refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
 759     destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
 760     refine (X_ ((update_ξ ξ t (leaves varstypes)))
 761       (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_.  apply FreshMon.
 762     simpl.
 763     rewrite pf2.
 764     rewrite pf1.
 765     auto.
 766     apply ILeaf.
 767     inversion X; subst; clear X.
 768
 769     apply (@ELetRec _ _ _ _ _ _ _ varstypes).
 770     apply (@letrec_helper Γ Δ t varstypes).
 771     rewrite <- pf2 in X1.
 772     rewrite mapOptionTree_compose.
 773     apply X1.
 774     apply ileaf in X0.
 775     apply X0.
 776
 777   destruct case_RCase.
 778     apply ILeaf; simpl; intros.
 779     inversion X_.
 780     clear X_.
 781     subst.
 782     apply ileaf in X0.
 783     simpl in X0.
 784
 785     (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
 786      * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
 787     rename Σ into body_freevars_types.
 788     rename vars into all_freevars.
 789     rename X0 into body_expr.
 790     rename X  into alts_exprs.
 791
 792     destruct all_freevars; try destruct o; inversion H.
 793     rename all_freevars2 into body_freevars.
 794     rename all_freevars1 into alts_freevars.
 795
 796     set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
 797     set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
 798     apply fix_indexing in alts_exprs'.
 799     simpl in alts_exprs'.
 800     apply unindex_tree in alts_exprs'.
 801     simpl in alts_exprs'.
 802     apply fix2 in alts_exprs'.
 803     apply treeM in alts_exprs'.
 804
 805     refine ( alts_exprs' >>>= fun Y =>
 806       body_expr ξ _ _
 807       >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
 808       apply FreshMon.
 809       apply FreshMon.
 810       apply H2.
 811     Defined.
 812
 813   Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
 814     refine ((
 815       fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
 816       match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
 817       | cnd_weak             => let case_nil    := tt in INone _ _
 818       | cnd_rule h c cnd' r  => let case_rule   := tt in rule2expr _ _ r (closed2expr' _ cnd')
 819       | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2)
 820       end)); clear closed2expr'; intros; subst.
 821         Defined.
 822
 823   Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
 824     FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
 825     intros Γ Σ.
 826     induction Σ; intro ξ.
 827     destruct a.
 828     destruct l as [τ l].
 829     set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
 830     refine (q >>>= fun q' => return _).
 831     apply FreshMon.
 832     clear q.
 833     destruct q' as [varstypes [pf1 [pf2 distpf]]].
 834     exists (mapOptionTree (@fst _ _) varstypes).
 835     exists (update_ξ ξ l (leaves varstypes)).
 836     symmetry; auto.
 837     refine (return _).
 838     exists [].
 839     exists ξ; auto.
 840     refine (bind f1 = IHΣ1 ξ ; _).
 841     apply FreshMon.
 842     destruct f1 as [vars1 [ξ1 pf1]].
 843     refine (bind f2 = IHΣ2 ξ1 ; _).
 844     apply FreshMon.
 845     destruct f2 as [vars2 [ξ2 pf22]].
 846     refine (return _).
 847     exists (vars1,,vars2).
 848     exists ξ2.
 849     simpl.
 850     rewrite pf22.
 851     rewrite pf1.
 852     admit.
 853     Defined.
 854
 855   Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
 856     {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
 857     FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
 858     intro pf.
 859     set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
 860     apply closed2expr in cnd.
 861     apply ileaf in cnd.
 862     simpl in *.
 863     clear pf.
 864     refine (bind ξvars = manyFresh _ Σ ξ0; _).
 865     apply FreshMon.
 866     destruct ξvars as [vars ξpf].
 867     destruct ξpf as [ξ pf].
 868     refine (cnd ξ vars _ >>>= fun it => _).
 869     apply FreshMon.
 870     auto.
 871     refine (return OK _).
 872     exists ξ.
 873     apply (ileaf it).
 874     Defined.
 875
 876 End HaskProofToStrong.