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 nd_rule; apply RJoin ].
 965     eapply nd_comp; [ apply nd_llecnac | idtac ].
 966     apply nd_prod; auto.
 967   Defined.
 968
 969 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
 970     forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))),
 971     ND Rule [] [Γ > Δ > mapOptionTree (update_xi ξ lev (leaves tree)) (expr2antecedent body) |- [τ ]@ lev] ->
 972     LetRecSubproofs Γ Δ (update_xi ξ lev (leaves tree)) lev tree branches ->
 973     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches body)) |- [τ ]@ lev].
 974
 975   (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
 976   intro branches.
 977   intro body.
 978   intro disti.
 979   intro pf.
 980   intro lrsp.
 981
 982   assert (distinct (leaves (mapOptionTree (@fst _ _) tree))) as disti'.
 983     apply disti.
 984     rewrite mapleaves in disti'.
 985
 986   set (@update_xiv_lemma _ Γ ξ lev tree disti') as ξlemma.
 987     rewrite <- mapOptionTree_compose in ξlemma.
 988
 989   set ((update_xi ξ lev (leaves tree))) as ξ' in *.
 990   set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
 991   set (mapOptionTree (@fst _ _) tree) as pctx.
 992   set (mapOptionTree ξ' pctx) as passback.
 993   set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.
 994   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
 995   clear z.
 996
 997   set (@factorContextRightAndWeaken''  Γ Δ  pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'.
 998   unfold passback in *; clear passback.
 999   unfold pctx in *; clear pctx.
1000   set (q' disti) as q''.
1001
1002   unfold ξ' in *.
1003   set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
1004   rewrite <- mapleaves in zz.
1005   rewrite zz in q''.
1006   clear zz.
1007   clear ξ'.
1008   Opaque stripOutVars.
1009   simpl.
1010   rewrite <- mapOptionTree_compose in q''.
1011   rewrite <- ξlemma.
1012   eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ _ q'') ].
1013   clear q'.
1014   clear q''.
1015   simpl.
1016
1017   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
1018     eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
1019     eapply nd_comp; [ apply nd_rlecnac | idtac ].
1020     apply nd_prod; auto.
1021     Defined.
1022
1023 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
1024   forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
1025     forall l ξ,
1026       vec2list (vec_map (scbwv_xi scb ξ l) (scbwv_exprvars scb)) =
1027       vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)).
1028   intros.
1029   unfold scbwv_xi.
1030   unfold scbwv_varstypes.
1031   set (@update_xiv_lemma _ _ (weakLT' ○ ξ) (weakL' l)
1032     (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
1033     ) as q.
1034   rewrite <- mapleaves' in q.
1035   rewrite <- mapleaves' in q.
1036   rewrite <- mapleaves' in q.
1037   rewrite <- mapleaves' in q.
1038   set (fun z => unleaves_injective _ _ _ (q z)) as q'.
1039   rewrite vec2list_map_list2vec in q'.
1040   rewrite fst_zip in q'.
1041   rewrite vec2list_map_list2vec in q'.
1042   rewrite vec2list_map_list2vec in q'.
1043   rewrite snd_zip in q'.
1044   rewrite leaves_unleaves in q'.
1045   rewrite vec2list_map_list2vec in q'.
1046   rewrite vec2list_map_list2vec in q'.
1047   apply q'.
1048   rewrite fst_zip.
1049   apply scbwv_exprvars_distinct.
1050   Qed.
1051
1052
1053 Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
1054    (alts':Tree
1055             ??{sac : StrongAltCon &
1056               {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
1057               Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ))
1058                 (scbwv_xi scb ξ l) (weakT' tbranches) (weakL' l)}}),
1059
1060       (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
1061         (mapOptionTree mkProofCaseBranch alts'))
1062     ,,
1063     mapOptionTree ξ  (expr2antecedent e) =
1064   mapOptionTree ξ
1065         (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).
1066   intros.
1067   simpl.
1068   Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
1069   hack.
1070   induction alts'.
1071   destruct a; simpl.
1072   destruct s; simpl.
1073   unfold mkProofCaseBranch.
1074   reflexivity.
1075   reflexivity.
1076   simpl.
1077   rewrite IHalts'1.
1078   rewrite IHalts'2.
1079   reflexivity.
1080   rewrite H.
1081   reflexivity.
1082   Qed.
1083
1084 Definition expr2proof  :
1085   forall Γ Δ ξ τ l (e:Expr Γ Δ ξ τ l),
1086     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ] @ l].
1087
1088   refine (fix expr2proof Γ' Δ' ξ' τ' l' (exp:Expr Γ' Δ' ξ' τ' l') {struct exp}
1089     : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ'] @ l'] :=
1090     match exp as E in Expr Γ Δ ξ τ l with
1091     | EGlobal  Γ Δ ξ     g v lev                    => let case_EGlobal := tt in _
1092     | EVar     Γ Δ ξ ev                             => let case_EVar := tt in _
1093     | ELit     Γ Δ ξ lit lev                        => let case_ELit := tt in _
1094     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => let case_EApp := tt in
1095                                                         (fun e1' e2' => _) (expr2proof _ _ _ _ _ e1) (expr2proof _ _ _ _ _ e2)
1096     | ELam     Γ Δ ξ t1 t2 lev v    e               => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1097     | ELet     Γ Δ ξ tv t      v lev ev ebody       => let case_ELet := tt in
1098                                                        (fun pf_let pf_body => _) (expr2proof _ _ _ _ _ ev) (expr2proof _ _ _ _ _ ebody)
1099     | ELetRec  Γ Δ ξ lev t tree disti branches ebody =>
1100       let ξ' := update_xi ξ lev (leaves tree) in
1101       let case_ELetRec := tt in  (fun e' subproofs => _) (expr2proof _ _ _ _ _ ebody)
1102         ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
1103         (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
1104         : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
1105         match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
1106           | ELR_nil    Γ Δ ξ lev  => lrsp_nil _ _ _ _
1107           | ELR_leaf   Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ _ e)
1108           | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
1109         end
1110         ) _ _ _ _ tree branches)
1111     | EEsc     Γ Δ ξ ec t lev e                     => let case_EEsc    := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1112     | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1113     | ECast    Γ Δ ξ γ t1 t2 lev      e             => let case_ECast   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1114     | ENote    Γ Δ ξ t _ n e                        => let case_ENote   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1115     | ETyLam   Γ Δ ξ κ σ l e                        => let case_ETyLam  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1116     | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1117     | ECoApp   Γ Δ κ σ₁ σ₂ σ γ ξ l      e           => let case_ECoApp  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1118     | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1119     | ECase    Γ Δ ξ l tc tbranches atypes e alts' =>
1120       let dcsp :=
1121         ((fix mkdcsp (alts:
1122                Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
1123                             & Expr (sac_gamma sac Γ)
1124                                    (sac_delta sac Γ atypes (weakCK'' Δ))
1125                                    (scbwv_xi scb ξ l)
1126                                    (weakT' tbranches) (weakL' l) } })
1127           : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
1128         match alts as ALTS return ND Rule []
1129           (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
1130           | T_Leaf None      => let case_nil := tt in _
1131           | T_Branch b1 b2   => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
1132           | T_Leaf (Some x)  =>
1133             match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
1134             existT sac (existT scbx ex) =>
1135             (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ _ ex)
1136         end
1137         end) alts')
1138         in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1139     end
1140   ); clear exp ξ' τ' Γ' Δ' l' expr2proof; try clear mkdcsp.
1141
1142     destruct case_EGlobal.
1143       apply nd_rule.
1144       simpl.
1145       apply (RGlobal _ _ _  g).
1146
1147     destruct case_EVar.
1148       apply nd_rule.
1149       unfold mapOptionTree; simpl.
1150       destruct (ξ ev).
1151       apply RVar.
1152
1153     destruct case_ELit.
1154       apply nd_rule.
1155       apply RLit.
1156
1157     destruct case_EApp.
1158       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
1159       eapply nd_comp; [ idtac
1160         | eapply nd_rule;
1161           apply (@RApp _ _ _ _ t2 t1) ].
1162       eapply nd_comp; [ apply nd_llecnac | idtac ].
1163       apply nd_prod; auto.
1164
1165     destruct case_ELam; intros.
1166       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
1167       eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
1168       set (update_xi ξ lev ((v,t1)::nil)) as ξ'.
1169       set (factorContextRightAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx.
1170         eapply RArrange in pfx.
1171         unfold mapOptionTree in pfx; simpl in pfx.
1172         unfold ξ' in pfx.
1173         rewrite updating_stripped_tree_is_inert in pfx.
1174         unfold update_xi in pfx.
1175         destruct (eqd_dec v v).
1176         eapply nd_comp; [ idtac | apply (nd_rule pfx) ].
1177         clear pfx.
1178         apply e'.
1179         assert False.
1180         apply n.
1181         auto.
1182         inversion H.
1183
1184     destruct case_ELet; intros; simpl in *.
1185       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1186       eapply nd_comp; [ apply nd_rlecnac | idtac ].
1187       apply nd_prod.
1188       apply pf_let.
1189       eapply nd_comp; [ apply pf_body | idtac ].
1190       fold (@mapOptionTree VV).
1191       fold (mapOptionTree ξ).
1192       set (update_xi ξ v ((lev,tv)::nil)) as ξ'.
1193       set (factorContextLeftAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n.
1194       unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
1195       unfold ξ' in n.
1196       rewrite updating_stripped_tree_is_inert in n.
1197       unfold update_xi in n.
1198       destruct (eqd_dec lev lev).
1199       unfold ξ'.
1200       unfold update_xi.
1201       eapply RArrange in n.
1202       apply (nd_rule n).
1203       assert False. apply n0; auto. inversion H.
1204
1205     destruct case_EEsc.
1206       eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
1207       apply e'.
1208
1209     destruct case_EBrak; intros.
1210       eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
1211       apply e'.
1212
1213     destruct case_ECast.
1214       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
1215       apply e'.
1216       auto.
1217
1218     destruct case_ENote.
1219       eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
1220       apply e'.
1221       auto.
1222
1223     destruct case_ETyApp; simpl in *; intros.
1224       eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
1225       apply e'.
1226       auto.
1227
1228     destruct case_ECoLam; simpl in *; intros.
1229       eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
1230       apply e'.
1231
1232     destruct case_ECoApp; simpl in *; intros.
1233       eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
1234       apply e'.
1235       auto.
1236
1237     destruct case_ETyLam; intros.
1238       eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
1239       unfold mapOptionTree in e'.
1240       rewrite mapOptionTree_compose in e'.
1241       unfold mapOptionTree.
1242       apply e'.
1243
1244     destruct case_leaf.
1245       clear o x alts alts' e.
1246       eapply nd_comp; [ apply e' | idtac ].
1247       clear e'.
1248       apply nd_rule.
1249       apply RArrange.
1250       simpl.
1251       rewrite mapleaves'.
1252       simpl.
1253       rewrite <- mapOptionTree_compose.
1254       unfold scbwv_xi.
1255       rewrite <- mapleaves'.
1256       rewrite vec2list_map_list2vec.
1257       unfold sac_gamma.
1258       rewrite <- (scbwv_coherent scbx l ξ).
1259       rewrite <- vec2list_map_list2vec.
1260       rewrite mapleaves'.
1261       set (@factorContextRightAndWeaken'') as q.
1262       unfold scbwv_xi.
1263       set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
1264       unfold scbwv_varstypes in z.
1265       rewrite vec2list_map_list2vec in z.
1266       rewrite fst_zip in z.
1267       rewrite <- z.
1268       clear z.
1269
1270       replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
1271         (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
1272       apply q.
1273       apply (sac_delta sac Γ atypes (weakCK'' Δ)).
1274       rewrite leaves_unleaves.
1275       apply (scbwv_exprvars_distinct scbx).
1276       rewrite leaves_unleaves.
1277       reflexivity.
1278
1279     destruct case_nil.
1280       apply nd_id0.
1281
1282     destruct case_branch.
1283       simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
1284       apply nd_prod.
1285       apply b1'.
1286       apply b2'.
1287
1288     destruct case_ECase.
1289     set (@RCase Γ Δ l tc) as q.
1290       rewrite <- case_lemma.
1291       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
1292       eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
1293       rewrite <- mapOptionTree_compose.
1294       apply dcsp.
1295       apply e'.
1296
1297     destruct case_ELetRec; intros.
1298       unfold ξ'0 in *.
1299       clear ξ'0.
1300       unfold ξ'1 in *.
1301       clear ξ'1.
1302       apply letRecSubproofsToND'.
1303       apply e'.
1304       apply subproofs.
1305
1306   Defined.
1307
1308 End HaskStrongToProof.
1309