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 n 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 Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) :=
 553   match elrb with
 554   | ELR_nil    Γ Δ ξ lev  => []
 555   | ELR_leaf   Γ Δ ξ  lev  v t e => [t]
 556   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
 557   end.
 558
 559 Lemma stripping_nothing_is_inert
 560   {Γ:TypeEnv}
 561   (ξ:VV -> LeveledHaskType Γ ★)
 562   tree :
 563   stripOutVars nil tree = tree.
 564   induction tree.
 565     simpl; destruct a; reflexivity.
 566     unfold stripOutVars.
 567     fold stripOutVars.
 568     simpl.
 569     fold (stripOutVars nil).
 570     rewrite <- IHtree1 at 2.
 571     rewrite <- IHtree2 at 2.
 572     reflexivity.
 573     Qed.
 574
 575 Definition factorContextLeft
 576      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 577      v      (* variable to be pivoted, if found *)
 578      ctx    (* initial context *)
 579      (ξ:VV -> LeveledHaskType Γ ★)
 580      :
 581
 582     (* a proof concluding in a context where that variable does not appear *)
 583      sum (Arrange
 584           (mapOptionTree ξ                        ctx                        )
 585           (mapOptionTree ξ ([],,(stripOutVars (v::nil) ctx))                ))
 586
 587     (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
 588         (Arrange
 589           (mapOptionTree ξ                         ctx                       )
 590           (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx))                )).
 591
 592   induction ctx.
 593
 594     refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
 595
 596         (* nonempty leaf *)
 597         destruct case_Some.
 598           unfold stripOutVars in *; simpl.
 599           unfold dropVar.
 600           unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 601
 602           destruct (eqd_dec v' v); subst.
 603
 604             (* where the leaf is v *)
 605             apply inr.
 606               subst.
 607               apply AuCanR.
 608
 609             (* where the leaf is NOT v *)
 610             apply inl.
 611               apply AuCanL.
 612
 613         (* empty leaf *)
 614         destruct case_None.
 615           apply inl; simpl in *.
 616           apply AuCanR.
 617
 618       (* branch *)
 619       refine (
 620         match IHctx1 with
 621           | inr lpf =>
 622             match IHctx2 with
 623               | inr rpf => let case_Both := tt in _
 624               | inl rpf => let case_Left := tt in _
 625             end
 626           | inl lpf =>
 627             match IHctx2 with
 628               | inr rpf => let case_Right   := tt in _
 629               | inl rpf => let case_Neither := tt in _
 630             end
 631         end); clear IHctx1; clear IHctx2.
 632
 633     destruct case_Neither.
 634       apply inl.
 635       simpl.
 636       eapply AComp; [idtac | apply AuCanL ].
 637         exact (AComp
 638           (* order will not matter because these are central as morphisms *)
 639           (ARight _ (AComp lpf (ACanL _)))
 640           (ALeft  _ (AComp rpf (ACanL _)))).
 641
 642     destruct case_Right.
 643       apply inr.
 644       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 645       fold (stripOutVars (v::nil)).
 646       eapply AComp; [ idtac | eapply pivotContext' ].
 647       eapply AComp.
 648       eapply ARight.
 649       eapply AComp.
 650       apply lpf.
 651       apply ACanL.
 652       eapply ALeft.
 653       apply rpf.
 654
 655     destruct case_Left.
 656       apply inr.
 657       fold (stripOutVars (v::nil)).
 658       simpl.
 659       eapply AComp.
 660       eapply ALeft.
 661       eapply AComp.
 662       apply rpf.
 663       simpl.
 664       eapply ACanL.
 665       eapply AComp; [ idtac | eapply AuAssoc ].
 666       eapply ARight.
 667       apply lpf.
 668
 669     destruct case_Both.
 670       apply inr.
 671       simpl.
 672       eapply AComp; [ idtac | eapply ARight; eapply ACont ].
 673       eapply AComp; [ eapply ARight; eapply lpf | idtac ].
 674       eapply AComp; [ eapply ALeft; eapply rpf | idtac ].
 675       clear lpf rpf.
 676       simpl.
 677       apply arrangeSwapMiddle.
 678       Defined.
 679
 680 Definition factorContextRight
 681      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 682      v      (* variable to be pivoted, if found *)
 683      ctx    (* initial context *)
 684      (ξ:VV -> LeveledHaskType Γ ★)
 685      :
 686
 687     (* a proof concluding in a context where that variable does not appear *)
 688      sum (Arrange
 689           (mapOptionTree ξ                        ctx                        )
 690           (mapOptionTree ξ (stripOutVars (v::nil) ctx),,[]                   ))
 691
 692     (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
 693         (Arrange
 694           (mapOptionTree ξ                         ctx                       )
 695           (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])                )).
 696
 697   induction ctx.
 698
 699     refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
 700
 701         (* nonempty leaf *)
 702         destruct case_Some.
 703           unfold stripOutVars in *; simpl.
 704           unfold dropVar.
 705           unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 706
 707           destruct (eqd_dec v' v); subst.
 708
 709             (* where the leaf is v *)
 710             apply inr.
 711               subst.
 712               apply AuCanL.
 713
 714             (* where the leaf is NOT v *)
 715             apply inl.
 716               apply AuCanR.
 717
 718         (* empty leaf *)
 719         destruct case_None.
 720           apply inl; simpl in *.
 721           apply AuCanR.
 722
 723       (* branch *)
 724       refine (
 725         match IHctx1 with
 726           | inr lpf =>
 727             match IHctx2 with
 728               | inr rpf => let case_Both := tt in _
 729               | inl rpf => let case_Left := tt in _
 730             end
 731           | inl lpf =>
 732             match IHctx2 with
 733               | inr rpf => let case_Right   := tt in _
 734               | inl rpf => let case_Neither := tt in _
 735             end
 736         end); clear IHctx1; clear IHctx2.
 737
 738     destruct case_Neither.
 739       apply inl.
 740       eapply AComp; [idtac | apply AuCanR ].
 741         exact (AComp
 742           (* order will not matter because these are central as morphisms *)
 743           (ARight _ (AComp lpf (ACanR _)))
 744           (ALeft  _ (AComp rpf (ACanR _)))).
 745
 746
 747     destruct case_Right.
 748       apply inr.
 749       fold (stripOutVars (v::nil)).
 750       set (ARight (mapOptionTree ξ ctx2)  (AComp lpf ((ACanR _)))) as q.
 751       simpl in *.
 752       eapply AComp.
 753       apply q.
 754       clear q.
 755       clear lpf.
 756       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 757       eapply AComp; [ idtac | apply AAssoc ].
 758       apply ALeft.
 759       apply rpf.
 760
 761     destruct case_Left.
 762       apply inr.
 763       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 764       fold (stripOutVars (v::nil)).
 765       eapply AComp; [ idtac | eapply pivotContext ].
 766       set (AComp rpf (ACanR _ )) as rpf'.
 767       set (ALeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.
 768       simpl in *.
 769       eapply AComp; [ idtac | apply qq ].
 770       clear qq rpf' rpf.
 771       apply (ARight (mapOptionTree ξ ctx2)).
 772       apply lpf.
 773
 774     destruct case_Both.
 775       apply inr.
 776       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 777       fold (stripOutVars (v::nil)).
 778       eapply AComp; [ idtac | eapply copyAndPivotContext ].
 779         (* order will not matter because these are central as morphisms *)
 780         exact (AComp (ARight _ lpf) (ALeft _ rpf)).
 781
 782     Defined.
 783
 784 (* same as before, but use AWeak if necessary *)
 785 Definition factorContextLeftAndWeaken
 786      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 787      v      (* variable to be pivoted, if found *)
 788      ctx    (* initial context *)
 789      (ξ:VV -> LeveledHaskType Γ ★) :
 790        Arrange
 791           (mapOptionTree ξ                        ctx                )
 792           (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx))        ).
 793   set (factorContextLeft Γ Δ v ctx ξ) as q.
 794   destruct q; auto.
 795   eapply AComp; [ apply a | idtac ].
 796   refine (ARight _ (AWeak _)).
 797   Defined.
 798
 799 Definition factorContextLeftAndWeaken''
 800      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 801      v      (* variable to be pivoted, if found *)
 802      (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
 803   distinct (leaves v) ->
 804   Arrange
 805     ((mapOptionTree ξ ctx)                                       )
 806     ((mapOptionTree ξ v),,(mapOptionTree ξ (stripOutVars (leaves v) ctx))).
 807
 808   induction v; intros.
 809     destruct a.
 810     unfold mapOptionTree in *.
 811     simpl in *.
 812     fold (mapOptionTree ξ) in *.
 813     intros.
 814     set (@factorContextLeftAndWeaken) as q.
 815     simpl in q.
 816     apply q.
 817     apply Δ.
 818
 819   unfold mapOptionTree; simpl in *.
 820     intros.
 821     rewrite (@stripping_nothing_is_inert Γ); auto.
 822     apply AuCanL.
 823     intros.
 824     unfold mapOptionTree in *.
 825     simpl in *.
 826     fold (mapOptionTree ξ) in *.
 827     set (mapOptionTree ξ) as X in *.
 828
 829     set (distinct_app _ _ _ H) as H'.
 830     destruct H' as [H1 H2].
 831
 832     set (IHv1 (v2,,(stripOutVars (leaves v2) ctx))) as IHv1'.
 833
 834     unfold X in *.
 835     simpl in *.
 836       rewrite <- strip_twice_lemma.
 837       set (notin_strip_inert' v2 (leaves v1)) as q.
 838       unfold stripOutVars in q.
 839       rewrite q in IHv1'.
 840       clear q.
 841     eapply AComp; [ idtac | eapply AAssoc ].
 842     eapply AComp; [ idtac | eapply IHv1' ].
 843     clear IHv1'.
 844     apply IHv2; auto.
 845     auto.
 846     auto.
 847     Defined.
 848
 849 (* same as before, but use AWeak if necessary *)
 850 Definition factorContextRightAndWeaken
 851      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 852      v      (* variable to be pivoted, if found *)
 853      ctx    (* initial context *)
 854      (ξ:VV -> LeveledHaskType Γ ★) :
 855        Arrange
 856           (mapOptionTree ξ                        ctx                )
 857           (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])        ).
 858   set (factorContextRight Γ Δ v ctx ξ) as q.
 859   destruct q; auto.
 860   eapply AComp; [ apply a | idtac ].
 861   refine (ALeft _ (AWeak _)).
 862   Defined.
 863
 864 Definition factorContextRightAndWeaken''
 865      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 866      v      (* variable to be pivoted, if found *)
 867      (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
 868   distinct (leaves v) ->
 869   Arrange
 870     ((mapOptionTree ξ ctx)                                       )
 871     ((mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v)).
 872
 873   induction v; intros.
 874     destruct a.
 875     unfold mapOptionTree in *.
 876     simpl in *.
 877     fold (mapOptionTree ξ) in *.
 878     intros.
 879     apply factorContextRightAndWeaken.
 880     apply Δ.
 881
 882   unfold mapOptionTree; simpl in *.
 883     intros.
 884     rewrite (@stripping_nothing_is_inert Γ); auto.
 885     apply AuCanR.
 886     intros.
 887     unfold mapOptionTree in *.
 888     simpl in *.
 889     fold (mapOptionTree ξ) in *.
 890     set (mapOptionTree ξ) as X in *.
 891
 892     set (IHv2 ((stripOutVars (leaves v1) ctx),, v1)) as IHv2'.
 893     unfold stripOutVars in IHv2'.
 894     simpl in IHv2'.
 895     fold (stripOutVars (leaves v2)) in IHv2'.
 896     fold (stripOutVars (leaves v1)) in IHv2'.
 897     unfold X in IHv2'.
 898     unfold mapOptionTree in IHv2'.
 899     simpl in IHv2'.
 900     fold (mapOptionTree ξ) in IHv2'.
 901     fold X in IHv2'.
 902     set (distinct_app _ _ _ H) as H'.
 903     destruct H' as [H1 H2].
 904     set (AComp (IHv1 _ H1) (IHv2' H2)) as qq.
 905     eapply AComp.
 906       apply qq.
 907       clear qq IHv2' IHv2 IHv1.
 908       rewrite strip_swap_lemma.
 909       rewrite strip_twice_lemma.
 910       rewrite (notin_strip_inert' v1 (leaves v2)).
 911         apply AuAssoc.
 912         apply distinct_swap.
 913         auto.
 914     Defined.
 915
 916 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
 917       mapOptionTree (update_xi ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
 918     = mapOptionTree ξ (stripOutVars (v :: nil) tree).
 919   set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
 920   rewrite p.
 921   simpl.
 922   reflexivity.
 923   Qed.
 924
 925 (* TODO: use multi-conclusion proofs instead *)
 926 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
 927   | lrsp_nil  : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
 928   | lrsp_leaf : forall v t e ,
 929     (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t]@lev]) ->
 930     LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)
 931   | lrsp_cons : forall t1 t2 b1 b2,
 932     LetRecSubproofs Γ Δ ξ lev t1 b1 ->
 933     LetRecSubproofs Γ Δ ξ lev t2 b2 ->
 934     LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
 935
 936 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
 937   LetRecSubproofs Γ Δ ξ lev tree branches ->
 938     ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
 939       |- (mapOptionTree (@snd _ _) tree) @ lev ].
 940   intro X; induction X; intros; simpl in *.
 941     apply nd_rule.
 942       apply RVoid.
 943     set (ξ v) as q in *.
 944       destruct q.
 945       simpl in *.
 946       apply n.
 947     eapply nd_comp; [ idtac | eapply RCut' ].
 948       eapply nd_comp; [ apply nd_llecnac | idtac ].
 949       apply nd_prod.
 950       apply IHX1.
 951       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ].
 952       apply IHX2.
 953       Defined.
 954
 955 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
 956     forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))),
 957     ND Rule [] [Γ > Δ > mapOptionTree (update_xi ξ lev (leaves tree)) (expr2antecedent body) |- [τ ]@ lev] ->
 958     LetRecSubproofs Γ Δ (update_xi ξ lev (leaves tree)) lev tree branches ->
 959     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches body)) |- [τ ]@ lev].
 960
 961   (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
 962   intro branches.
 963   intro body.
 964   intro disti.
 965   intro pf.
 966   intro lrsp.
 967
 968   assert (distinct (leaves (mapOptionTree (@fst _ _) tree))) as disti'.
 969     apply disti.
 970     rewrite mapleaves in disti'.
 971
 972   set (@update_xiv_lemma _ Γ ξ lev tree disti') as ξlemma.
 973     rewrite <- mapOptionTree_compose in ξlemma.
 974
 975   set ((update_xi ξ lev (leaves tree))) as ξ' in *.
 976   set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
 977   set (mapOptionTree (@fst _ _) tree) as pctx.
 978   set (mapOptionTree ξ' pctx) as passback.
 979   set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.
 980   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
 981   clear z.
 982
 983   set (@factorContextLeftAndWeaken''  Γ Δ  pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'.
 984   unfold passback in *; clear passback.
 985   unfold pctx in *; clear pctx.
 986   set (q' disti) as q''.
 987
 988   unfold ξ' in *.
 989   set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
 990   rewrite <- mapleaves in zz.
 991   rewrite zz in q''.
 992   clear zz.
 993   clear ξ'.
 994   Opaque stripOutVars.
 995   simpl.
 996   rewrite <- mapOptionTree_compose in q''.
 997   rewrite <- ξlemma.
 998   eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ _ q'') ].
 999   clear q'.
1000   clear q''.
1001   simpl.
1002
1003   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
1004
1005     eapply nd_comp; [ idtac | eapply RCut' ].
1006       eapply nd_comp; [ apply nd_llecnac | idtac ].
1007       apply nd_prod.
1008       apply q.
1009       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ].
1010       apply pf.
1011       Defined.
1012
1013 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
1014   forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
1015     forall l ξ,
1016       vec2list (vec_map (scbwv_xi scb ξ l) (scbwv_exprvars scb)) =
1017       vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)).
1018   intros.
1019   unfold scbwv_xi.
1020   unfold scbwv_varstypes.
1021   set (@update_xiv_lemma _ _ (weakLT' ○ ξ) (weakL' l)
1022     (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
1023     ) as q.
1024   rewrite <- mapleaves' in q.
1025   rewrite <- mapleaves' in q.
1026   rewrite <- mapleaves' in q.
1027   rewrite <- mapleaves' in q.
1028   set (fun z => unleaves_injective _ _ _ (q z)) as q'.
1029   rewrite vec2list_map_list2vec in q'.
1030   rewrite fst_zip in q'.
1031   rewrite vec2list_map_list2vec in q'.
1032   rewrite vec2list_map_list2vec in q'.
1033   rewrite snd_zip in q'.
1034   rewrite leaves_unleaves in q'.
1035   rewrite vec2list_map_list2vec in q'.
1036   rewrite vec2list_map_list2vec in q'.
1037   apply q'.
1038   rewrite fst_zip.
1039   apply scbwv_exprvars_distinct.
1040   Qed.
1041
1042
1043 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
1044 (alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
1045                             & Expr (sac_gamma sac Γ)
1046                                    (sac_delta sac Γ atypes (weakCK'' Δ))
1047                                    (scbwv_xi scb ξ l)
1048                                    (weakT' tbranches) (weakL' l) } })
1049   : @StrongAltCon tc * Tree ??(LeveledHaskType Γ ★).
1050   destruct alt.
1051   split.
1052   apply x.
1053   apply (mapOptionTree ξ
1054       (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
1055         (expr2antecedent (projT2 s)))).
1056      Defined.
1057
1058 Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
1059    (alts':Tree
1060             ??{sac : StrongAltCon &
1061               {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
1062               Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ))
1063                 (scbwv_xi scb ξ l) (weakT' tbranches) (weakL' l)}}),
1064
1065       (mapOptionTreeAndFlatten (fun x => snd x)
1066         (mapOptionTree mkProofCaseBranch alts'))
1067     ,,
1068     mapOptionTree ξ  (expr2antecedent e) =
1069   mapOptionTree ξ
1070         (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).
1071   intros.
1072   simpl.
1073   Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
1074   hack.
1075   induction alts'.
1076   destruct a; simpl.
1077   destruct s; simpl.
1078   unfold mkProofCaseBranch.
1079   reflexivity.
1080   reflexivity.
1081   simpl.
1082   rewrite IHalts'1.
1083   rewrite IHalts'2.
1084   reflexivity.
1085   rewrite H.
1086   reflexivity.
1087   Qed.
1088
1089 Definition expr2proof  :
1090   forall Γ Δ ξ τ l (e:Expr Γ Δ ξ τ l),
1091     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ] @ l].
1092
1093   refine (fix expr2proof Γ' Δ' ξ' τ' l' (exp:Expr Γ' Δ' ξ' τ' l') {struct exp}
1094     : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ'] @ l'] :=
1095     match exp as E in Expr Γ Δ ξ τ l with
1096     | EGlobal  Γ Δ ξ     g v lev                    => let case_EGlobal := tt in _
1097     | EVar     Γ Δ ξ ev                             => let case_EVar := tt in _
1098     | ELit     Γ Δ ξ lit lev                        => let case_ELit := tt in _
1099     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => let case_EApp := tt in
1100                                                         (fun e1' e2' => _) (expr2proof _ _ _ _ _ e1) (expr2proof _ _ _ _ _ e2)
1101     | ELam     Γ Δ ξ t1 t2 lev v    e               => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1102     | ELet     Γ Δ ξ tv t      v lev ev ebody       => let case_ELet := tt in
1103                                                        (fun pf_let pf_body => _) (expr2proof _ _ _ _ _ ev) (expr2proof _ _ _ _ _ ebody)
1104     | ELetRec  Γ Δ ξ lev t tree disti branches ebody =>
1105       let ξ' := update_xi ξ lev (leaves tree) in
1106       let case_ELetRec := tt in  (fun e' subproofs => _) (expr2proof _ _ _ _ _ ebody)
1107         ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
1108         (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
1109         : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
1110         match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
1111           | ELR_nil    Γ Δ ξ lev  => lrsp_nil _ _ _ _
1112           | ELR_leaf   Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ _ e)
1113           | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
1114         end
1115         ) _ _ _ _ tree branches)
1116     | EEsc     Γ Δ ξ ec t lev e                     => let case_EEsc    := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1117     | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1118     | ECast    Γ Δ ξ γ t1 t2 lev      e             => let case_ECast   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1119     | ENote    Γ Δ ξ t _ n e                        => let case_ENote   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1120     | ETyLam   Γ Δ ξ κ σ l n e                      => let case_ETyLam  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1121     | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1122     | ECoApp   Γ Δ κ σ₁ σ₂ σ γ ξ l      e           => let case_ECoApp  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1123     | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1124     | ECase    Γ Δ ξ l tc tbranches atypes e alts' =>
1125       let dcsp :=
1126         ((fix mkdcsp (alts:
1127                Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
1128                             & Expr (sac_gamma sac Γ)
1129                                    (sac_delta sac Γ atypes (weakCK'' Δ))
1130                                    (scbwv_xi scb ξ l)
1131                                    (weakT' tbranches) (weakL' l) } })
1132           : ND Rule [] (mapOptionTree (fun x => pcb_judg (snd (mkProofCaseBranch x))) alts) :=
1133         match alts as ALTS return ND Rule []
1134           (mapOptionTree (fun x => pcb_judg (snd (mkProofCaseBranch x))) ALTS) with
1135           | T_Leaf None      => let case_nil := tt in _
1136           | T_Branch b1 b2   => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
1137           | T_Leaf (Some x)  =>
1138             match x as X return ND Rule [] [@pcb_judg tc Γ Δ l tbranches atypes
1139               (fst (mkProofCaseBranch X))
1140               (snd (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       simpl.
1254       apply (fun x => nd_comp e' x).
1255       clear e'.
1256       unfold pcb_judg.
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 <- vec2list_map_list2vec.
1266       rewrite mapleaves'.
1267       set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
1268       unfold scbwv_varstypes in z.
1269       rewrite vec2list_map_list2vec in z.
1270       rewrite fst_zip in z.
1271       rewrite <- z.
1272       clear z.
1273       unfold sac_gamma in *.
1274       simpl in *.
1275       Unset Printing Implicit.
1276       idtac.
1277       apply nd_rule.
1278       apply RArrange.
1279       set (scbwv_exprvars_distinct scbx) as q'.
1280       rewrite <- leaves_unleaves in q'.
1281       apply (AComp (@factorContextRightAndWeaken'' _ (weakCE' Δ) _ _ (expr2antecedent ex) q')).
1282       clear q'.
1283
1284       set (scbwv_coherent scbx l ξ) as H.
1285       rewrite leaves_unleaves.
1286       unfold scbwv_varstypes.
1287       apply ALeft.
1288       rewrite <- mapleaves'.
1289       rewrite <- mapleaves'.
1290       rewrite mapleaves'.
1291       rewrite vec2list_map_list2vec.
1292       rewrite <- H.
1293       clear H.
1294       rewrite <- mapleaves'.
1295       rewrite vec2list_map_list2vec.
1296       unfold scbwv_xi.
1297       unfold scbwv_varstypes.
1298       apply AId.
1299
1300     destruct case_nil.
1301       apply nd_id0.
1302
1303     destruct case_branch.
1304       simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
1305       apply nd_prod.
1306       apply b1'.
1307       apply b2'.
1308
1309     destruct case_ECase.
1310     set (@RCase Γ Δ l tc) as q.
1311       rewrite <- case_lemma.
1312       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
1313       eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
1314       rewrite <- mapOptionTree_compose.
1315       apply dcsp.
1316       apply e'.
1317
1318     destruct case_ELetRec; intros.
1319       unfold ξ'0 in *.
1320       clear ξ'0.
1321       unfold ξ'1 in *.
1322       clear ξ'1.
1323       apply letRecSubproofsToND'.
1324       apply e'.
1325       apply subproofs.
1326
1327   Defined.
1328
1329 End HaskStrongToProof.
1330