src/HaskStrongToProof.v

   1 (*********************************************************************************************************************************)
   2 (* HaskStrongToProof: convert HaskStrong to HaskProof                                                                            *)
   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 HaskStrongToProof.
  18
  19 Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
  20   RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).
  21
  22 Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) :=
  23   RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _).
  24
  25 Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).
  26   eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ].
  27   eapply RComp; [ idtac | apply RCossa ].
  28   eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
  29   apply RAssoc.
  30   Defined.
  31
  32 Context {VV:Type}{eqd_vv:EqDecidable VV}.
  33
  34 (* maintenance of Xi *)
  35 Fixpoint dropVar (lv:list VV)(v:VV) : ??VV :=
  36   match lv with
  37     | nil     => Some v
  38     | v'::lv' => if eqd_dec v v' then None else dropVar lv' v
  39   end.
  40
  41 Fixpoint mapOptionTree' {a b:Type}(f:a->??b)(t:@Tree ??a) : @Tree ??b :=
  42   match t with
  43     | T_Leaf None     => T_Leaf None
  44     | T_Leaf (Some x) => T_Leaf (f x)
  45     | T_Branch l r    => T_Branch (mapOptionTree' f l) (mapOptionTree' f r)
  46   end.
  47
  48   (* later: use mapOptionTreeAndFlatten *)
  49   Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=
  50     mapOptionTree' (dropVar lv).
  51
  52 Lemma In_both : forall T (l1 l2:list T) a, In a l1 -> In a (app l1 l2).
  53   intros T l1.
  54   induction l1; intros.
  55   inversion H.
  56   simpl.
  57   inversion H; subst.
  58   left; auto.
  59   right.
  60   apply IHl1.
  61   apply H0.
  62   Qed.
  63
  64 Lemma In_both' : forall T (l1 l2:list T) a, In a l2 -> In a (app l1 l2).
  65   intros T l1.
  66   induction l1; intros.
  67   apply H.
  68   rewrite <- app_comm_cons.
  69   simpl.
  70   right.
  71   apply IHl1.
  72   auto.
  73   Qed.
  74
  75 Lemma distinct_app : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l1 /\ distinct l2.
  76   intro T.
  77   intro l1.
  78   induction l1; intros.
  79   split; auto.
  80   apply distinct_nil.
  81   simpl in H.
  82   inversion H.
  83   subst.
  84   set (IHl1 _ H3) as H3'.
  85   destruct H3'.
  86   split; auto.
  87   apply distinct_cons; auto.
  88   intro.
  89   apply H2.
  90   apply In_both; auto.
  91   Qed.
  92
  93 Lemma mapOptionTree'_compose : forall T A B (t:Tree ??T) (f:T->??A)(g:A->??B),
  94   mapOptionTree' g (mapOptionTree' f t)
  95   =
  96   mapOptionTree' (fun x => match f x with None => None | Some x => g x end) t.
  97   intros; induction t.
  98     destruct a; auto.
  99     simpl.
 100     destruct (f t); reflexivity.
 101     simpl.
 102     rewrite <- IHt1.
 103     rewrite <- IHt2.
 104     reflexivity.
 105     Qed.
 106
 107 Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOutVars x t).
 108   unfold stripOutVars.
 109   rewrite mapOptionTree'_compose.
 110   simpl.
 111   induction t.
 112   destruct a0.
 113   simpl.
 114   induction x.
 115   reflexivity.
 116   simpl.
 117   destruct (eqd_dec v a0).
 118     destruct (eqd_dec v a); reflexivity.
 119     apply IHx.
 120   reflexivity.
 121   simpl.
 122   rewrite <- IHt1.
 123   rewrite <- IHt2.
 124   reflexivity.
 125   Qed.
 126
 127 Lemma strip_nil_lemma       t : stripOutVars nil t = t.
 128   induction t; simpl.
 129   unfold stripOutVars.
 130     destruct a; reflexivity.
 131     rewrite <- IHt1 at 2.
 132     rewrite <- IHt2 at 2.
 133     reflexivity.
 134     Qed.
 135
 136 Lemma strip_swap0_lemma : forall a a0 y t,
 137   stripOutVars (a :: a0 :: y) t = stripOutVars (a0 :: a :: y) t.
 138   intros.
 139   unfold stripOutVars.
 140   induction t.
 141   destruct a1; simpl; [ idtac | reflexivity ].
 142   destruct (eqd_dec v a); subst.
 143   destruct (eqd_dec a a0); subst.
 144     reflexivity.
 145     reflexivity.
 146   destruct (eqd_dec v a0); subst.
 147     reflexivity.
 148     reflexivity.
 149     simpl in *.
 150     rewrite IHt1.
 151     rewrite IHt2.
 152     reflexivity.
 153     Qed.
 154
 155 Lemma strip_swap1_lemma : forall a y t,
 156   stripOutVars (a :: nil) (stripOutVars y t) =
 157   stripOutVars y (stripOutVars (a :: nil) t).
 158   intros.
 159   induction y.
 160     rewrite strip_nil_lemma.
 161     rewrite strip_nil_lemma.
 162     reflexivity.
 163   rewrite (strip_lemma a0 y (stripOutVars (a::nil) t)).
 164     rewrite <- IHy.
 165     clear IHy.
 166     rewrite <- (strip_lemma a y t).
 167     rewrite <- strip_lemma.
 168     rewrite <- strip_lemma.
 169     apply strip_swap0_lemma.
 170     Qed.
 171
 172 Lemma strip_swap_lemma : forall  x y t, stripOutVars x (stripOutVars y t) = stripOutVars y (stripOutVars x t).
 173   intros; induction t.
 174     destruct a; simpl.
 175
 176     induction x.
 177       rewrite strip_nil_lemma.
 178         rewrite strip_nil_lemma.
 179         reflexivity.
 180       rewrite strip_lemma.
 181         rewrite (strip_lemma a x [v]).
 182         rewrite IHx.
 183         clear IHx.
 184         apply strip_swap1_lemma.
 185     reflexivity.
 186   unfold stripOutVars in *.
 187     simpl.
 188     rewrite IHt1.
 189     rewrite IHt2.
 190     reflexivity.
 191   Qed.
 192
 193 Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app x y) t.
 194   induction x; simpl.
 195     apply strip_nil_lemma.
 196     rewrite strip_lemma.
 197     rewrite IHx.
 198     clear IHx.
 199     rewrite <- strip_lemma.
 200     reflexivity.
 201     Qed.
 202
 203 Lemma notin_strip_inert a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y.
 204   intros.
 205   induction y.
 206   destruct a0; try reflexivity.
 207   simpl in *.
 208   unfold stripOutVars.
 209   simpl.
 210   destruct (eqd_dec v a).
 211   subst.
 212   assert False.
 213   apply H.
 214   left; auto.
 215   inversion H0.
 216   auto.
 217   rewrite <- IHy1 at 2.
 218   rewrite <- IHy2 at 2.
 219   reflexivity.
 220   unfold not; intro.
 221   apply H.
 222   eapply In_both' in H0.
 223   apply H0.
 224   unfold not; intro.
 225   apply H.
 226   eapply In_both in H0.
 227   apply H0.
 228   Qed.
 229
 230 Lemma drop_distinct x v : (not (In v x)) -> dropVar x v = Some v.
 231   intros.
 232   induction x.
 233   reflexivity.
 234   simpl.
 235   destruct (eqd_dec v a).
 236   subst.
 237   assert False. apply H.
 238   simpl; auto.
 239   inversion H0.
 240   apply IHx.
 241   unfold not.
 242   intro.
 243   apply H.
 244   simpl; auto.
 245   Qed.
 246
 247 Lemma in3 {T}(a b c:list T) q : In q (app a c) -> In q (app (app a b) c).
 248   induction a; intros.
 249   simpl.
 250   simpl in H.
 251   apply In_both'.
 252   auto.
 253   rewrite <- ass_app.
 254   rewrite <- app_comm_cons.
 255   simpl.
 256   rewrite ass_app.
 257   rewrite <- app_comm_cons in H.
 258   inversion H.
 259   left; auto.
 260   right.
 261   apply IHa.
 262   apply H0.
 263   Qed.
 264
 265 Lemma distinct3 {T}(a b c:list T) : distinct (app (app a b) c) -> distinct (app a c).
 266   induction a; intros.
 267   simpl in *.
 268   apply distinct_app in H; auto.
 269   destruct H; auto.
 270   rewrite <- app_comm_cons.
 271   apply distinct_cons.
 272   rewrite <- ass_app in H.
 273   rewrite <- app_comm_cons in H.
 274   inversion H.
 275   subst.
 276   intro q.
 277   apply H2.
 278   rewrite ass_app.
 279   apply in3.
 280   auto.
 281   apply IHa.
 282   rewrite <- ass_app.
 283   rewrite <- ass_app in H.
 284   rewrite <- app_comm_cons in H.
 285   inversion H.
 286   subst.
 287   auto.
 288   Qed.
 289
 290 Lemma notin_strip_inert' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y.
 291   induction x; intros.
 292   simpl in H.
 293   unfold stripOutVars.
 294   simpl.
 295   induction y; try destruct a; auto.
 296   simpl.
 297   rewrite IHy1.
 298   rewrite IHy2.
 299   reflexivity.
 300   simpl in H.
 301   apply distinct_app in H; destruct H; auto.
 302   apply distinct_app in H; destruct H; auto.
 303   rewrite <- app_comm_cons in H.
 304   inversion H; subst.
 305   set (IHx H3) as qq.
 306   rewrite strip_lemma.
 307   rewrite IHx.
 308   apply notin_strip_inert.
 309   unfold not; intros.
 310   apply H2.
 311   apply In_both'.
 312   auto.
 313   auto.
 314   Qed.
 315
 316 Lemma dropvar_lemma v v' y : dropVar y v = Some v' -> v=v'.
 317   intros.
 318   induction y; auto.
 319   simpl in H.
 320   inversion H.
 321   auto.
 322   apply IHy.
 323   simpl in H.
 324   destruct (eqd_dec v a).
 325   inversion H.
 326   auto.
 327   Qed.
 328
 329 Lemma updating_stripped_tree_is_inert'
 330   {Γ} lev
 331   (ξ:VV -> LeveledHaskType Γ ★)
 332   lv tree2 :
 333     mapOptionTree (update_xi ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2)
 334   = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2).
 335
 336   induction tree2.
 337     destruct a; [ idtac | reflexivity ]; simpl.
 338     induction lv; [ reflexivity | idtac ]; simpl.
 339     destruct a; simpl.
 340     set (eqd_dec v v0) as q; destruct q; auto.
 341     set (dropVar (map (@fst _ _) lv) v) as b in *.
 342       assert (dropVar (map (@fst _ _) lv) v=b). reflexivity.
 343       destruct b; [ idtac | reflexivity ].
 344       apply dropvar_lemma in H.
 345       subst.
 346       inversion IHlv.
 347       rewrite H0.
 348       clear H0 IHlv.
 349       destruct (eqd_dec v0 v1).
 350       subst.
 351       assert False. apply n. intros; auto. inversion H.
 352       reflexivity.
 353     unfold stripOutVars in *.
 354       simpl.
 355       rewrite <- IHtree2_1.
 356       rewrite <- IHtree2_2.
 357       reflexivity.
 358     Qed.
 359
 360 Lemma distinct_bogus : forall {T}a0 (a:list T), distinct (a0::(app a (a0::nil))) -> False.
 361   intros; induction a; auto.
 362   simpl in H.
 363   inversion H; subst.
 364   apply H2; auto.
 365   unfold In; simpl.
 366   left; auto.
 367   apply IHa.
 368   clear IHa.
 369   rewrite <- app_comm_cons in H.
 370   inversion H; subst.
 371   inversion H3; subst.
 372   apply distinct_cons; auto.
 373   intros.
 374   apply H2.
 375   simpl.
 376   right; auto.
 377   Qed.
 378
 379 Lemma distinct_swap' : forall {T}a (b:list T), distinct (app b (a::nil)) -> distinct (a::b).
 380   intros.
 381   apply distinct_cons.
 382     induction b; intros; simpl; auto.
 383     rewrite <- app_comm_cons in H.
 384     inversion H; subst.
 385     set (IHb H4) as H4'.
 386     apply H4'.
 387     inversion H0; subst; auto.
 388     apply distinct_bogus in H; inversion H.
 389   induction b; intros; simpl; auto.
 390     apply distinct_nil.
 391     apply distinct_app in H.
 392     destruct H; auto.
 393   Qed.
 394
 395 Lemma in_both : forall {T}(a b:list T) x, In x (app a b) -> In x a \/ In x b.
 396   induction a; intros; simpl; auto.
 397   rewrite <- app_comm_cons in H.
 398   inversion H.
 399   subst.
 400   left; left; auto.
 401   set (IHa _ _ H0) as H'.
 402   destruct H'.
 403   left; right; auto.
 404   right; auto.
 405   Qed.
 406
 407 Lemma distinct_lemma : forall {T} (a b:list T) a0, distinct (app a (a0 :: b)) -> distinct (app a b).
 408   intros.
 409   induction a; simpl; auto.
 410   simpl in H.
 411   inversion H; auto.
 412   assert (distinct (app a1 b)) as Q.
 413   intros.
 414   apply IHa.
 415   clear IHa.
 416   rewrite <- app_comm_cons in H.
 417   inversion H; subst; auto.
 418   apply distinct_cons; [ idtac | apply Q ].
 419   intros.
 420   apply in_both in H0.
 421   destruct H0.
 422   rewrite <- app_comm_cons in H.
 423   inversion H; subst; auto.
 424   apply H3.
 425   apply In_both; auto.
 426   rewrite <- app_comm_cons in H.
 427   inversion H; subst; auto.
 428   apply H3.
 429   apply In_both'; auto.
 430   simpl.
 431   right; auto.
 432   Qed.
 433
 434 Lemma nil_app : forall {T}(a:list T) x, x::a = (app (x::nil) a).
 435   induction a; intros; simpl; auto.
 436   Qed.
 437
 438 Lemma distinct_swap : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a).
 439   intros.
 440   induction b.
 441   rewrite <- app_nil_end in H; auto.
 442   rewrite <- app_comm_cons.
 443   set (distinct_lemma _ _ _ H) as H'.
 444   set (IHb H') as H''.
 445   apply distinct_cons; [ idtac | apply H'' ].
 446   intros.
 447   apply in_both in H0.
 448   clear H'' H'.
 449   destruct H0.
 450   apply distinct_app in H.
 451   destruct H.
 452   inversion H1; auto.
 453   clear IHb.
 454   rewrite nil_app in H.
 455   rewrite ass_app in H.
 456   apply distinct_app in H.
 457   destruct H; auto.
 458   apply distinct_swap' in H.
 459   inversion H; auto.
 460   Qed.
 461
 462 Lemma update_xiv_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) :
 463   forall v1 v2,
 464   distinct (map (@fst _ _) (leaves (v1,,(varstypes,,v2)))) ->
 465   mapOptionTree (update_xi ξ lev (leaves (v1,,(varstypes,,v2)))) (mapOptionTree (@fst _ _) varstypes) =
 466   mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
 467   induction varstypes; intros.
 468   destruct a; simpl; [ idtac | reflexivity ].
 469   destruct p.
 470   simpl.
 471   simpl in H.
 472   induction (leaves v1).
 473     simpl; auto.
 474     destruct (eqd_dec v v); auto.
 475     assert False. apply n. auto. inversion H0.
 476     simpl.
 477     destruct a.
 478       destruct (eqd_dec v0 v); subst; auto.
 479       simpl in H.
 480       rewrite map_app in H.
 481       simpl in H.
 482       rewrite nil_app in H.
 483       apply distinct_swap in H.
 484       rewrite app_ass in H.
 485       apply distinct_app in H.
 486       destruct H.
 487       apply distinct_swap in H0.
 488       simpl in H0.
 489       inversion H0; subst.
 490       assert False.
 491       apply H3.
 492       simpl; left; auto.
 493       inversion H1.
 494     apply IHl.
 495       simpl in H.
 496       inversion H; auto.
 497   set (IHvarstypes1 v1 (varstypes2,,v2)) as i1.
 498     set (IHvarstypes2 (v1,,varstypes1) v2) as i2.
 499     simpl in *.
 500     rewrite <- i1.
 501     rewrite <- i2.
 502     rewrite ass_app.
 503     rewrite ass_app.
 504     rewrite ass_app.
 505     rewrite ass_app.
 506     reflexivity.
 507     clear i1 i2 IHvarstypes1 IHvarstypes2.
 508     repeat rewrite ass_app in *; auto.
 509     clear i1 i2 IHvarstypes1 IHvarstypes2.
 510     repeat rewrite ass_app in *; auto.
 511     Qed.
 512
 513 Lemma update_xiv_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) :
 514   distinct (map (@fst _ _) (leaves varstypes)) ->
 515   mapOptionTree (update_xi ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) =
 516   mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
 517   set (update_xiv_lemma' Γ ξ lev varstypes [] []) as q.
 518   simpl in q.
 519   rewrite <- app_nil_end in q.
 520   apply q.
 521   Qed.
 522
 523 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
 524   match exp as E in Expr Γ Δ ξ τ with
 525   | EGlobal  Γ Δ ξ _ _ _                          => []
 526   | EVar     Γ Δ ξ ev                             => [ev]
 527   | ELit     Γ Δ ξ lit lev                        => []
 528   | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e1),,(expr2antecedent e2)
 529   | ELam     Γ Δ ξ t1 t2 lev v    e               => stripOutVars (v::nil) (expr2antecedent e)
 530   | ELet     Γ Δ ξ tv t  lev v ev ebody           => (expr2antecedent ev),,((stripOutVars (v::nil) (expr2antecedent ebody)))
 531   | EEsc     Γ Δ ξ ec t lev e                     => expr2antecedent e
 532   | EBrak    Γ Δ ξ ec t lev e                     => expr2antecedent e
 533   | ECast    Γ Δ ξ γ t1 t2 lev      e             => expr2antecedent e
 534   | ENote    Γ Δ ξ t n e                          => expr2antecedent e
 535   | ETyLam   Γ Δ ξ κ σ l e                        => expr2antecedent e
 536   | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => expr2antecedent e
 537   | ECoApp   Γ Δ κ γ σ₁ σ₂ σ ξ l      e           => expr2antecedent e
 538   | ETyApp   Γ Δ κ σ τ ξ  l    e                  => expr2antecedent e
 539   | ELetRec  Γ Δ ξ l τ vars _ branches body       =>
 540       let branch_context := eLetRecContext branches
 541    in let all_contexts := branch_context,,(expr2antecedent body)
 542    in     stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
 543   | ECase    Γ Δ ξ l tc tbranches atypes e' alts =>
 544     ((fix varsfromalts (alts:
 545                Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
 546                             & Expr (sac_gamma sac Γ)
 547                                    (sac_delta sac Γ atypes (weakCK'' Δ))
 548                                    (scbwv_xi scb ξ l)
 549                                    (weakLT' (tbranches@@l)) } }
 550       ): Tree ??VV :=
 551       match alts with
 552         | T_Leaf None     => []
 553         | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 (projT2 h)))) (expr2antecedent (projT2 (projT2 h)))
 554         | T_Branch b1 b2  => (varsfromalts b1),,(varsfromalts b2)
 555       end) alts),,(expr2antecedent e')
 556 end
 557 with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
 558 match elrb with
 559   | ELR_nil    Γ Δ ξ lev  => []
 560   | ELR_leaf   Γ Δ ξ lev v t e => expr2antecedent e
 561   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
 562 end.
 563
 564 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
 565 (alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
 566                             & Expr (sac_gamma sac Γ)
 567                                    (sac_delta sac Γ atypes (weakCK'' Δ))
 568                                    (scbwv_xi scb ξ l)
 569                                    (weakLT' (tbranches@@l)) } })
 570   : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }.
 571   destruct alt.
 572   exists x.
 573   exact
 574     {| pcb_freevars := mapOptionTree ξ
 575       (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
 576         (expr2antecedent (projT2 s)))
 577      |}.
 578      Defined.
 579
 580
 581 Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) :=
 582   match elrb with
 583   | ELR_nil    Γ Δ ξ lev  => []
 584   | ELR_leaf   Γ Δ ξ  lev  v t e => [t]
 585   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
 586   end.
 587
 588 Lemma stripping_nothing_is_inert
 589   {Γ:TypeEnv}
 590   (ξ:VV -> LeveledHaskType Γ ★)
 591   tree :
 592   stripOutVars nil tree = tree.
 593   induction tree.
 594     simpl; destruct a; reflexivity.
 595     unfold stripOutVars.
 596     fold stripOutVars.
 597     simpl.
 598     fold (stripOutVars nil).
 599     rewrite <- IHtree1 at 2.
 600     rewrite <- IHtree2 at 2.
 601     reflexivity.
 602     Qed.
 603
 604 Definition factorContextLeft
 605      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 606      v      (* variable to be pivoted, if found *)
 607      ctx    (* initial context *)
 608      (ξ:VV -> LeveledHaskType Γ ★)
 609      :
 610
 611     (* a proof concluding in a context where that variable does not appear *)
 612      sum (Arrange
 613           (mapOptionTree ξ                        ctx                        )
 614           (mapOptionTree ξ ([],,(stripOutVars (v::nil) ctx))                ))
 615
 616     (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
 617         (Arrange
 618           (mapOptionTree ξ                         ctx                       )
 619           (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx))                )).
 620
 621   induction ctx.
 622
 623     refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
 624
 625         (* nonempty leaf *)
 626         destruct case_Some.
 627           unfold stripOutVars in *; simpl.
 628           unfold dropVar.
 629           unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 630
 631           destruct (eqd_dec v' v); subst.
 632
 633             (* where the leaf is v *)
 634             apply inr.
 635               subst.
 636               apply RuCanR.
 637
 638             (* where the leaf is NOT v *)
 639             apply inl.
 640               apply RuCanL.
 641
 642         (* empty leaf *)
 643         destruct case_None.
 644           apply inl; simpl in *.
 645           apply RuCanR.
 646
 647       (* branch *)
 648       refine (
 649         match IHctx1 with
 650           | inr lpf =>
 651             match IHctx2 with
 652               | inr rpf => let case_Both := tt in _
 653               | inl rpf => let case_Left := tt in _
 654             end
 655           | inl lpf =>
 656             match IHctx2 with
 657               | inr rpf => let case_Right   := tt in _
 658               | inl rpf => let case_Neither := tt in _
 659             end
 660         end); clear IHctx1; clear IHctx2.
 661
 662     destruct case_Neither.
 663       apply inl.
 664       simpl.
 665       eapply RComp; [idtac | apply RuCanL ].
 666         exact (RComp
 667           (* order will not matter because these are central as morphisms *)
 668           (RRight _ (RComp lpf (RCanL _)))
 669           (RLeft  _ (RComp rpf (RCanL _)))).
 670
 671     destruct case_Right.
 672       apply inr.
 673       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 674       fold (stripOutVars (v::nil)).
 675       eapply RComp; [ idtac | eapply pivotContext' ].
 676       eapply RComp.
 677       eapply RRight.
 678       eapply RComp.
 679       apply lpf.
 680       apply RCanL.
 681       eapply RLeft.
 682       apply rpf.
 683
 684     destruct case_Left.
 685       apply inr.
 686       fold (stripOutVars (v::nil)).
 687       simpl.
 688       eapply RComp.
 689       eapply RLeft.
 690       eapply RComp.
 691       apply rpf.
 692       simpl.
 693       eapply RCanL.
 694       eapply RComp; [ idtac | eapply RCossa ].
 695       eapply RRight.
 696       apply lpf.
 697
 698     destruct case_Both.
 699       apply inr.
 700       simpl.
 701       eapply RComp; [ idtac | eapply RRight; eapply RCont ].
 702       eapply RComp; [ eapply RRight; eapply lpf | idtac ].
 703       eapply RComp; [ eapply RLeft; eapply rpf | idtac ].
 704       clear lpf rpf.
 705       simpl.
 706       apply arrangeSwapMiddle.
 707       Defined.
 708
 709 Definition factorContextRight
 710      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 711      v      (* variable to be pivoted, if found *)
 712      ctx    (* initial context *)
 713      (ξ:VV -> LeveledHaskType Γ ★)
 714      :
 715
 716     (* a proof concluding in a context where that variable does not appear *)
 717      sum (Arrange
 718           (mapOptionTree ξ                        ctx                        )
 719           (mapOptionTree ξ (stripOutVars (v::nil) ctx),,[]                   ))
 720
 721     (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
 722         (Arrange
 723           (mapOptionTree ξ                         ctx                       )
 724           (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])                )).
 725
 726   induction ctx.
 727
 728     refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
 729
 730         (* nonempty leaf *)
 731         destruct case_Some.
 732           unfold stripOutVars in *; simpl.
 733           unfold dropVar.
 734           unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 735
 736           destruct (eqd_dec v' v); subst.
 737
 738             (* where the leaf is v *)
 739             apply inr.
 740               subst.
 741               apply RuCanL.
 742
 743             (* where the leaf is NOT v *)
 744             apply inl.
 745               apply RuCanR.
 746
 747         (* empty leaf *)
 748         destruct case_None.
 749           apply inl; simpl in *.
 750           apply RuCanR.
 751
 752       (* branch *)
 753       refine (
 754         match IHctx1 with
 755           | inr lpf =>
 756             match IHctx2 with
 757               | inr rpf => let case_Both := tt in _
 758               | inl rpf => let case_Left := tt in _
 759             end
 760           | inl lpf =>
 761             match IHctx2 with
 762               | inr rpf => let case_Right   := tt in _
 763               | inl rpf => let case_Neither := tt in _
 764             end
 765         end); clear IHctx1; clear IHctx2.
 766
 767     destruct case_Neither.
 768       apply inl.
 769       eapply RComp; [idtac | apply RuCanR ].
 770         exact (RComp
 771           (* order will not matter because these are central as morphisms *)
 772           (RRight _ (RComp lpf (RCanR _)))
 773           (RLeft  _ (RComp rpf (RCanR _)))).
 774
 775
 776     destruct case_Right.
 777       apply inr.
 778       fold (stripOutVars (v::nil)).
 779       set (RRight (mapOptionTree ξ ctx2)  (RComp lpf ((RCanR _)))) as q.
 780       simpl in *.
 781       eapply RComp.
 782       apply q.
 783       clear q.
 784       clear lpf.
 785       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 786       eapply RComp; [ idtac | apply RAssoc ].
 787       apply RLeft.
 788       apply rpf.
 789
 790     destruct case_Left.
 791       apply inr.
 792       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 793       fold (stripOutVars (v::nil)).
 794       eapply RComp; [ idtac | eapply pivotContext ].
 795       set (RComp rpf (RCanR _ )) as rpf'.
 796       set (RLeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.
 797       simpl in *.
 798       eapply RComp; [ idtac | apply qq ].
 799       clear qq rpf' rpf.
 800       apply (RRight (mapOptionTree ξ ctx2)).
 801       apply lpf.
 802
 803     destruct case_Both.
 804       apply inr.
 805       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 806       fold (stripOutVars (v::nil)).
 807       eapply RComp; [ idtac | eapply copyAndPivotContext ].
 808         (* order will not matter because these are central as morphisms *)
 809         exact (RComp (RRight _ lpf) (RLeft _ rpf)).
 810
 811     Defined.
 812
 813 (* same as before, but use RWeak if necessary *)
 814 Definition factorContextLeftAndWeaken
 815      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 816      v      (* variable to be pivoted, if found *)
 817      ctx    (* initial context *)
 818      (ξ:VV -> LeveledHaskType Γ ★) :
 819        Arrange
 820           (mapOptionTree ξ                        ctx                )
 821           (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx))        ).
 822   set (factorContextLeft Γ Δ v ctx ξ) as q.
 823   destruct q; auto.
 824   eapply RComp; [ apply a | idtac ].
 825   refine (RRight _ (RWeak _)).
 826   Defined.
 827
 828 Definition factorContextLeftAndWeaken''
 829      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 830      v      (* variable to be pivoted, if found *)
 831      (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
 832   distinct (leaves v) ->
 833   Arrange
 834     ((mapOptionTree ξ ctx)                                       )
 835     ((mapOptionTree ξ v),,(mapOptionTree ξ (stripOutVars (leaves v) ctx))).
 836
 837   induction v; intros.
 838     destruct a.
 839     unfold mapOptionTree in *.
 840     simpl in *.
 841     fold (mapOptionTree ξ) in *.
 842     intros.
 843     set (@factorContextLeftAndWeaken) as q.
 844     simpl in q.
 845     apply q.
 846     apply Δ.
 847
 848   unfold mapOptionTree; simpl in *.
 849     intros.
 850     rewrite (@stripping_nothing_is_inert Γ); auto.
 851     apply RuCanL.
 852     intros.
 853     unfold mapOptionTree in *.
 854     simpl in *.
 855     fold (mapOptionTree ξ) in *.
 856     set (mapOptionTree ξ) as X in *.
 857
 858     set (distinct_app _ _ _ H) as H'.
 859     destruct H' as [H1 H2].
 860
 861     set (IHv1 (v2,,(stripOutVars (leaves v2) ctx))) as IHv1'.
 862
 863     unfold X in *.
 864     simpl in *.
 865       rewrite <- strip_twice_lemma.
 866       set (notin_strip_inert' v2 (leaves v1)) as q.
 867       unfold stripOutVars in q.
 868       rewrite q in IHv1'.
 869       clear q.
 870     eapply RComp; [ idtac | eapply RAssoc ].
 871     eapply RComp; [ idtac | eapply IHv1' ].
 872     clear IHv1'.
 873     apply IHv2; auto.
 874     auto.
 875     auto.
 876     Defined.
 877
 878 (* same as before, but use RWeak if necessary *)
 879 Definition factorContextRightAndWeaken
 880      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 881      v      (* variable to be pivoted, if found *)
 882      ctx    (* initial context *)
 883      (ξ:VV -> LeveledHaskType Γ ★) :
 884        Arrange
 885           (mapOptionTree ξ                        ctx                )
 886           (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])        ).
 887   set (factorContextRight Γ Δ v ctx ξ) as q.
 888   destruct q; auto.
 889   eapply RComp; [ apply a | idtac ].
 890   refine (RLeft _ (RWeak _)).
 891   Defined.
 892
 893 Definition factorContextRightAndWeaken''
 894      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 895      v      (* variable to be pivoted, if found *)
 896      (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
 897   distinct (leaves v) ->
 898   Arrange
 899     ((mapOptionTree ξ ctx)                                       )
 900     ((mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v)).
 901
 902   induction v; intros.
 903     destruct a.
 904     unfold mapOptionTree in *.
 905     simpl in *.
 906     fold (mapOptionTree ξ) in *.
 907     intros.
 908     apply factorContextRightAndWeaken.
 909     apply Δ.
 910
 911   unfold mapOptionTree; simpl in *.
 912     intros.
 913     rewrite (@stripping_nothing_is_inert Γ); auto.
 914     apply RuCanR.
 915     intros.
 916     unfold mapOptionTree in *.
 917     simpl in *.
 918     fold (mapOptionTree ξ) in *.
 919     set (mapOptionTree ξ) as X in *.
 920
 921     set (IHv2 ((stripOutVars (leaves v1) ctx),, v1)) as IHv2'.
 922     unfold stripOutVars in IHv2'.
 923     simpl in IHv2'.
 924     fold (stripOutVars (leaves v2)) in IHv2'.
 925     fold (stripOutVars (leaves v1)) in IHv2'.
 926     unfold X in IHv2'.
 927     unfold mapOptionTree in IHv2'.
 928     simpl in IHv2'.
 929     fold (mapOptionTree ξ) in IHv2'.
 930     fold X in IHv2'.
 931     set (distinct_app _ _ _ H) as H'.
 932     destruct H' as [H1 H2].
 933     set (RComp (IHv1 _ H1) (IHv2' H2)) as qq.
 934     eapply RComp.
 935       apply qq.
 936       clear qq IHv2' IHv2 IHv1.
 937       rewrite strip_swap_lemma.
 938       rewrite strip_twice_lemma.
 939       rewrite (notin_strip_inert' v1 (leaves v2)).
 940         apply RCossa.
 941         apply distinct_swap.
 942         auto.
 943     Defined.
 944
 945 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
 946       mapOptionTree (update_xi ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
 947     = mapOptionTree ξ (stripOutVars (v :: nil) tree).
 948   set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
 949   rewrite p.
 950   simpl.
 951   reflexivity.
 952   Qed.
 953
 954 (* TODO: use multi-conclusion proofs instead *)
 955 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
 956   | lrsp_nil  : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
 957   | lrsp_leaf : forall v t e ,
 958     (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t]@lev]) ->
 959     LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)
 960   | lrsp_cons : forall t1 t2 b1 b2,
 961     LetRecSubproofs Γ Δ ξ lev t1 b1 ->
 962     LetRecSubproofs Γ Δ ξ lev t2 b2 ->
 963     LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
 964
 965 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
 966   LetRecSubproofs Γ Δ ξ lev tree branches ->
 967     ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
 968       |- (mapOptionTree (@snd _ _) tree) @ lev ].
 969   intro X; induction X; intros; simpl in *.
 970     apply nd_rule.
 971       apply RVoid.
 972     set (ξ v) as q in *.
 973       destruct q.
 974       simpl in *.
 975       apply n.
 976     eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
 977     eapply nd_comp; [ apply nd_llecnac | idtac ].
 978     apply nd_prod; auto.
 979   Defined.
 980
 981 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
 982     forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))),
 983     ND Rule [] [Γ > Δ > mapOptionTree (update_xi ξ lev (leaves tree)) (expr2antecedent body) |- [τ ]@ lev] ->
 984     LetRecSubproofs Γ Δ (update_xi ξ lev (leaves tree)) lev tree branches ->
 985     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches body)) |- [τ ]@ lev].
 986
 987   (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
 988   intro branches.
 989   intro body.
 990   intro disti.
 991   intro pf.
 992   intro lrsp.
 993
 994   assert (distinct (leaves (mapOptionTree (@fst _ _) tree))) as disti'.
 995     apply disti.
 996     rewrite mapleaves in disti'.
 997
 998   set (@update_xiv_lemma _ Γ ξ lev tree disti') as ξlemma.
 999     rewrite <- mapOptionTree_compose in ξlemma.
1000
1001   set ((update_xi ξ lev (leaves tree))) as ξ' in *.
1002   set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
1003   set (mapOptionTree (@fst _ _) tree) as pctx.
1004   set (mapOptionTree ξ' pctx) as passback.
1005   set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.
1006   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
1007   clear z.
1008
1009   set (@factorContextRightAndWeaken''  Γ Δ  pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'.
1010   unfold passback in *; clear passback.
1011   unfold pctx in *; clear pctx.
1012   set (q' disti) as q''.
1013
1014   unfold ξ' in *.
1015   set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
1016   rewrite <- mapleaves in zz.
1017   rewrite zz in q''.
1018   clear zz.
1019   clear ξ'.
1020   Opaque stripOutVars.
1021   simpl.
1022   rewrite <- mapOptionTree_compose in q''.
1023   rewrite <- ξlemma.
1024   eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ _ q'') ].
1025   clear q'.
1026   clear q''.
1027   simpl.
1028
1029   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
1030     eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
1031     eapply nd_comp; [ apply nd_rlecnac | idtac ].
1032     apply nd_prod; auto.
1033     Defined.
1034
1035 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
1036   forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
1037     forall l ξ,
1038       vec2list (vec_map (scbwv_xi scb ξ l) (scbwv_exprvars scb)) =
1039       vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)).
1040   intros.
1041   unfold scbwv_xi.
1042   unfold scbwv_varstypes.
1043   set (@update_xiv_lemma _ _ (weakLT' ○ ξ) (weakL' l)
1044     (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
1045     ) as q.
1046   rewrite <- mapleaves' in q.
1047   rewrite <- mapleaves' in q.
1048   rewrite <- mapleaves' in q.
1049   rewrite <- mapleaves' in q.
1050   set (fun z => unleaves_injective _ _ _ (q z)) as q'.
1051   rewrite vec2list_map_list2vec in q'.
1052   rewrite fst_zip in q'.
1053   rewrite vec2list_map_list2vec in q'.
1054   rewrite vec2list_map_list2vec in q'.
1055   rewrite snd_zip in q'.
1056   rewrite leaves_unleaves in q'.
1057   rewrite vec2list_map_list2vec in q'.
1058   rewrite vec2list_map_list2vec in q'.
1059   apply q'.
1060   rewrite fst_zip.
1061   apply scbwv_exprvars_distinct.
1062   Qed.
1063
1064
1065 Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
1066    (alts':Tree
1067             ??{sac : StrongAltCon &
1068               {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
1069               Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ))
1070                 (scbwv_xi scb ξ l) (weakLT' (tbranches @@  l))}}),
1071
1072       (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
1073         (mapOptionTree mkProofCaseBranch alts'))
1074     ,,
1075     mapOptionTree ξ  (expr2antecedent e) =
1076   mapOptionTree ξ
1077         (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).
1078   intros.
1079   simpl.
1080   Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
1081   hack.
1082   induction alts'.
1083   destruct a; simpl.
1084   destruct s; simpl.
1085   unfold mkProofCaseBranch.
1086   reflexivity.
1087   reflexivity.
1088   simpl.
1089   rewrite IHalts'1.
1090   rewrite IHalts'2.
1091   reflexivity.
1092   rewrite H.
1093   reflexivity.
1094   Qed.
1095
1096 Definition expr2proof  :
1097   forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
1098     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [unlev τ] @ getlev τ].
1099
1100   refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
1101     : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [unlev τ'] @ getlev τ'] :=
1102     match exp as E in Expr Γ Δ ξ τ with
1103     | EGlobal  Γ Δ ξ     g v lev                    => let case_EGlobal := tt in _
1104     | EVar     Γ Δ ξ ev                             => let case_EVar := tt in _
1105     | ELit     Γ Δ ξ lit lev                        => let case_ELit := tt in _
1106     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => let case_EApp := tt in
1107                                                         (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
1108     | ELam     Γ Δ ξ t1 t2 lev v    e               => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1109     | ELet     Γ Δ ξ tv t      v lev ev ebody       => let case_ELet := tt in
1110                                                        (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
1111     | ELetRec  Γ Δ ξ lev t tree disti branches ebody =>
1112       let ξ' := update_xi ξ lev (leaves tree) in
1113       let case_ELetRec := tt in  (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
1114         ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
1115         (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
1116         : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
1117         match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
1118           | ELR_nil    Γ Δ ξ lev  => lrsp_nil _ _ _ _
1119           | ELR_leaf   Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ e)
1120           | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
1121         end
1122         ) _ _ _ _ tree branches)
1123     | EEsc     Γ Δ ξ ec t lev e                     => let case_EEsc    := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1124     | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1125     | ECast    Γ Δ ξ γ t1 t2 lev      e             => let case_ECast   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1126     | ENote    Γ Δ ξ t n e                          => let case_ENote   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1127     | ETyLam   Γ Δ ξ κ σ l e                        => let case_ETyLam  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1128     | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1129     | ECoApp   Γ Δ κ σ₁ σ₂ σ γ ξ l      e           => let case_ECoApp  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1130     | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1131     | ECase    Γ Δ ξ l tc tbranches atypes e alts' =>
1132       let dcsp :=
1133         ((fix mkdcsp (alts:
1134                Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
1135                             & Expr (sac_gamma sac Γ)
1136                                    (sac_delta sac Γ atypes (weakCK'' Δ))
1137                                    (scbwv_xi scb ξ l)
1138                                    (weakLT' (tbranches@@l)) } })
1139           : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
1140         match alts as ALTS return ND Rule []
1141           (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
1142           | T_Leaf None      => let case_nil := tt in _
1143           | T_Branch b1 b2   => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
1144           | T_Leaf (Some x)  =>
1145             match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
1146             existT sac (existT scbx ex) =>
1147             (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex)
1148         end
1149         end) alts')
1150         in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1151     end
1152   ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
1153
1154     destruct case_EGlobal.
1155       apply nd_rule.
1156       simpl.
1157       apply (RGlobal _ _ _  g).
1158
1159     destruct case_EVar.
1160       apply nd_rule.
1161       unfold mapOptionTree; simpl.
1162       destruct (ξ ev).
1163       apply RVar.
1164
1165     destruct case_ELit.
1166       apply nd_rule.
1167       apply RLit.
1168
1169     destruct case_EApp.
1170       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
1171       eapply nd_comp; [ idtac
1172         | eapply nd_rule;
1173           apply (@RApp _ _ _ _ t2 t1) ].
1174       eapply nd_comp; [ apply nd_llecnac | idtac ].
1175       apply nd_prod; auto.
1176
1177     destruct case_ELam; intros.
1178       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
1179       eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
1180       set (update_xi ξ lev ((v,t1)::nil)) as ξ'.
1181       set (factorContextRightAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx.
1182         eapply RArrange in pfx.
1183         unfold mapOptionTree in pfx; simpl in pfx.
1184         unfold ξ' in pfx.
1185         rewrite updating_stripped_tree_is_inert in pfx.
1186         unfold update_xi in pfx.
1187         destruct (eqd_dec v v).
1188         eapply nd_comp; [ idtac | apply (nd_rule pfx) ].
1189         clear pfx.
1190         apply e'.
1191         assert False.
1192         apply n.
1193         auto.
1194         inversion H.
1195
1196     destruct case_ELet; intros; simpl in *.
1197       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1198       eapply nd_comp; [ apply nd_rlecnac | idtac ].
1199       apply nd_prod.
1200       apply pf_let.
1201       eapply nd_comp; [ apply pf_body | idtac ].
1202       fold (@mapOptionTree VV).
1203       fold (mapOptionTree ξ).
1204       set (update_xi ξ v ((lev,tv)::nil)) as ξ'.
1205       set (factorContextLeftAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n.
1206       unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
1207       unfold ξ' in n.
1208       rewrite updating_stripped_tree_is_inert in n.
1209       unfold update_xi in n.
1210       destruct (eqd_dec lev lev).
1211       unfold ξ'.
1212       unfold update_xi.
1213       eapply RArrange in n.
1214       apply (nd_rule n).
1215       assert False. apply n0; auto. inversion H.
1216
1217     destruct case_EEsc.
1218       eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
1219       apply e'.
1220
1221     destruct case_EBrak; intros.
1222       eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
1223       apply e'.
1224
1225     destruct case_ECast.
1226       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
1227       apply e'.
1228       auto.
1229
1230     destruct case_ENote.
1231       destruct t.
1232       eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
1233       apply e'.
1234       auto.
1235
1236     destruct case_ETyApp; simpl in *; intros.
1237       eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
1238       apply e'.
1239       auto.
1240
1241     destruct case_ECoLam; simpl in *; intros.
1242       eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
1243       apply e'.
1244
1245     destruct case_ECoApp; simpl in *; intros.
1246       eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
1247       apply e'.
1248       auto.
1249
1250     destruct case_ETyLam; intros.
1251       eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
1252       unfold mapOptionTree in e'.
1253       rewrite mapOptionTree_compose in e'.
1254       unfold mapOptionTree.
1255       apply e'.
1256
1257     destruct case_leaf.
1258       clear o x alts alts' e.
1259       eapply nd_comp; [ apply e' | idtac ].
1260       clear e'.
1261       apply nd_rule.
1262       apply RArrange.
1263       simpl.
1264       rewrite mapleaves'.
1265       simpl.
1266       rewrite <- mapOptionTree_compose.
1267       unfold scbwv_xi.
1268       rewrite <- mapleaves'.
1269       rewrite vec2list_map_list2vec.
1270       unfold sac_gamma.
1271       rewrite <- (scbwv_coherent scbx l ξ).
1272       rewrite <- vec2list_map_list2vec.
1273       rewrite mapleaves'.
1274       set (@factorContextRightAndWeaken'') as q.
1275       unfold scbwv_xi.
1276       set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
1277       unfold scbwv_varstypes in z.
1278       rewrite vec2list_map_list2vec in z.
1279       rewrite fst_zip in z.
1280       rewrite <- z.
1281       clear z.
1282
1283       replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
1284         (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
1285       apply q.
1286       apply (sac_delta sac Γ atypes (weakCK'' Δ)).
1287       rewrite leaves_unleaves.
1288       apply (scbwv_exprvars_distinct scbx).
1289       rewrite leaves_unleaves.
1290       reflexivity.
1291
1292     destruct case_nil.
1293       apply nd_id0.
1294
1295     destruct case_branch.
1296       simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
1297       apply nd_prod.
1298       apply b1'.
1299       apply b2'.
1300
1301     destruct case_ECase.
1302     set (@RCase Γ Δ l tc) as q.
1303       rewrite <- case_lemma.
1304       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
1305       eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
1306       rewrite <- mapOptionTree_compose.
1307       apply dcsp.
1308       apply e'.
1309
1310     destruct case_ELetRec; intros.
1311       unfold ξ'0 in *.
1312       clear ξ'0.
1313       unfold ξ'1 in *.
1314       clear ξ'1.
1315       apply letRecSubproofsToND'.
1316       apply e'.
1317       apply subproofs.
1318
1319   Defined.
1320
1321 End HaskStrongToProof.
1322