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