src/HaskStrongToProof.v

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