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_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app y x) t.
 125 (*
 126   induction x.
 127   simpl.
 128   unfold stripOutVars.
 129   simpl.
 130   rewrite mapOptionTree'_compose.
 131   induction t.
 132   destruct a; try reflexivity.
 133   simpl.
 134   destruct (dropVar y v); reflexivity.
 135   simpl.
 136   rewrite IHt1.
 137   rewrite IHt2.
 138   reflexivity.
 139   rewrite strip_lemma.
 140   rewrite IHx.
 141   rewrite <- strip_lemma.
 142   rewrite app_comm_cons.
 143   reflexivity.
 144 *)
 145   admit.
 146   Qed.
 147
 148 Lemma strip_distinct a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y.
 149   intros.
 150   induction y.
 151   destruct a0; try reflexivity.
 152   simpl in *.
 153   unfold stripOutVars.
 154   simpl.
 155   destruct (eqd_dec v a).
 156   subst.
 157   assert False.
 158   apply H.
 159   left; auto.
 160   inversion H0.
 161   auto.
 162   rewrite <- IHy1 at 2.
 163   rewrite <- IHy2 at 2.
 164   reflexivity.
 165   unfold not; intro.
 166   apply H.
 167   eapply In_both' in H0.
 168   apply H0.
 169   unfold not; intro.
 170   apply H.
 171   eapply In_both in H0.
 172   apply H0.
 173   Qed.
 174
 175 Lemma drop_distinct x v : (not (In v x)) -> dropVar x v = Some v.
 176   intros.
 177   induction x.
 178   reflexivity.
 179   simpl.
 180   destruct (eqd_dec v a).
 181   subst.
 182   assert False. apply H.
 183   simpl; auto.
 184   inversion H0.
 185   apply IHx.
 186   unfold not.
 187   intro.
 188   apply H.
 189   simpl; auto.
 190   Qed.
 191
 192 Lemma in3 {T}(a b c:list T) q : In q (app a c) -> In q (app (app a b) c).
 193   induction a; intros.
 194   simpl.
 195   simpl in H.
 196   apply In_both'.
 197   auto.
 198   rewrite <- ass_app.
 199   rewrite <- app_comm_cons.
 200   simpl.
 201   rewrite ass_app.
 202   rewrite <- app_comm_cons in H.
 203   inversion H.
 204   left; auto.
 205   right.
 206   apply IHa.
 207   apply H0.
 208   Qed.
 209
 210 Lemma distinct3 {T}(a b c:list T) : distinct (app (app a b) c) -> distinct (app a c).
 211   induction a; intros.
 212   simpl in *.
 213   apply distinct_app in H; auto.
 214   destruct H; auto.
 215   rewrite <- app_comm_cons.
 216   apply distinct_cons.
 217   rewrite <- ass_app in H.
 218   rewrite <- app_comm_cons in H.
 219   inversion H.
 220   subst.
 221   intro q.
 222   apply H2.
 223   rewrite ass_app.
 224   apply in3.
 225   auto.
 226   apply IHa.
 227   rewrite <- ass_app.
 228   rewrite <- ass_app in H.
 229   rewrite <- app_comm_cons in H.
 230   inversion H.
 231   subst.
 232   auto.
 233   Qed.
 234
 235 Lemma strip_distinct' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y.
 236   induction x; intros.
 237   simpl in H.
 238   unfold stripOutVars.
 239   simpl.
 240   induction y; try destruct a; auto.
 241   simpl.
 242   rewrite IHy1.
 243   rewrite IHy2.
 244   reflexivity.
 245   simpl in H.
 246   apply distinct_app in H; destruct H; auto.
 247   apply distinct_app in H; destruct H; auto.
 248   rewrite <- app_comm_cons in H.
 249   inversion H; subst.
 250   set (IHx H3) as qq.
 251   rewrite strip_lemma.
 252   rewrite IHx.
 253   apply strip_distinct.
 254   unfold not; intros.
 255   apply H2.
 256   apply In_both'.
 257   auto.
 258   auto.
 259   Qed.
 260
 261 Lemma updating_stripped_tree_is_inert'
 262   {Γ} lev
 263   (ξ:VV -> LeveledHaskType Γ ★)
 264   lv tree2 :
 265     mapOptionTree (update_ξ ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2)
 266   = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2).
 267   induction tree2.
 268   destruct a.
 269   simpl.
 270   induction lv.
 271   reflexivity.
 272   simpl.
 273   destruct a.
 274   simpl.
 275   set (eqd_dec v v0) as q.
 276   destruct q.
 277   auto.
 278   set (dropVar (map (@fst _ _) lv) v) as b in *.
 279   destruct b.
 280   inversion IHlv.
 281   admit.
 282   auto.
 283   reflexivity.
 284   simpl.
 285   unfold stripOutVars in *.
 286   rewrite <- IHtree2_1.
 287   rewrite <- IHtree2_2.
 288   reflexivity.
 289   Qed.
 290
 291 Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)),
 292   distinct (map (@fst _ _) (leaves varstypes)) ->
 293   mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) =
 294   mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
 295   admit.
 296   Qed.
 297
 298
 299
 300
 301
 302 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
 303   match exp as E in Expr Γ Δ ξ τ with
 304   | EGlobal  Γ Δ ξ _ _                            => []
 305   | EVar     Γ Δ ξ ev                             => [ev]
 306   | ELit     Γ Δ ξ lit lev                        => []
 307   | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e1),,(expr2antecedent e2)
 308   | ELam     Γ Δ ξ t1 t2 lev v    e               => stripOutVars (v::nil) (expr2antecedent e)
 309   | ELet     Γ Δ ξ tv t  lev v ev ebody           => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
 310   | EEsc     Γ Δ ξ ec t lev e                     => expr2antecedent e
 311   | EBrak    Γ Δ ξ ec t lev e                     => expr2antecedent e
 312   | ECast    Γ Δ ξ γ t1 t2 lev      e             => expr2antecedent e
 313   | ENote    Γ Δ ξ t n e                          => expr2antecedent e
 314   | ETyLam   Γ Δ ξ κ σ l e                        => expr2antecedent e
 315   | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => expr2antecedent e
 316   | ECoApp   Γ Δ κ γ σ₁ σ₂ σ ξ l      e           => expr2antecedent e
 317   | ETyApp   Γ Δ κ σ τ ξ  l    e                  => expr2antecedent e
 318   | ELetRec  Γ Δ ξ l τ vars branches body         =>
 319       let branch_context := eLetRecContext branches
 320    in let all_contexts := (expr2antecedent body),,branch_context
 321    in     stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
 322   | ECase    Γ Δ ξ l tc tbranches atypes e' alts =>
 323     ((fix varsfromalts (alts:
 324                Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
 325                             & Expr (sac_Γ sac Γ)
 326                                    (sac_Δ sac Γ atypes (weakCK'' Δ))
 327                                    (scbwv_ξ scb ξ l)
 328                                    (weakLT' (tbranches@@l)) } }
 329       ): Tree ??VV :=
 330       match alts with
 331         | T_Leaf None     => []
 332         | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 (projT2 h)))) (expr2antecedent (projT2 (projT2 h)))
 333         | T_Branch b1 b2  => (varsfromalts b1),,(varsfromalts b2)
 334       end) alts),,(expr2antecedent e')
 335 end
 336 with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
 337 match elrb with
 338   | ELR_nil    Γ Δ ξ lev  => []
 339   | ELR_leaf   Γ Δ ξ lev v t e => expr2antecedent e
 340   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
 341 end.
 342
 343 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
 344 (alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
 345                             & Expr (sac_Γ sac Γ)
 346                                    (sac_Δ sac Γ atypes (weakCK'' Δ))
 347                                    (scbwv_ξ scb ξ l)
 348                                    (weakLT' (tbranches@@l)) } })
 349   : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }.
 350   destruct alt.
 351   exists x.
 352   exact
 353     {| pcb_freevars := mapOptionTree ξ
 354       (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
 355         (expr2antecedent (projT2 s)))
 356      |}.
 357      Defined.
 358
 359
 360 Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) :=
 361   match elrb with
 362   | ELR_nil    Γ Δ ξ lev  => []
 363   | ELR_leaf   Γ Δ ξ  lev  v t e => [t]
 364   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
 365   end.
 366
 367 Lemma stripping_nothing_is_inert
 368   {Γ:TypeEnv}
 369   (ξ:VV -> LeveledHaskType Γ ★)
 370   tree :
 371   stripOutVars nil tree = tree.
 372   induction tree.
 373     simpl; destruct a; reflexivity.
 374     unfold stripOutVars.
 375     fold stripOutVars.
 376     simpl.
 377     fold (stripOutVars nil).
 378     rewrite <- IHtree1 at 2.
 379     rewrite <- IHtree2 at 2.
 380     reflexivity.
 381     Qed.
 382
 383 Definition arrangeContext
 384      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 385      v      (* variable to be pivoted, if found *)
 386      ctx    (* initial context *)
 387      (ξ:VV -> LeveledHaskType Γ ★)
 388      :
 389
 390     (* a proof concluding in a context where that variable does not appear *)
 391      sum (Arrange
 392           (mapOptionTree ξ                        ctx                        )
 393           (mapOptionTree ξ (stripOutVars (v::nil) ctx),,[]                   ))
 394
 395     (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
 396         (Arrange
 397           (mapOptionTree ξ                         ctx                       )
 398           (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])                )).
 399
 400   induction ctx.
 401
 402     refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
 403
 404         (* nonempty leaf *)
 405         destruct case_Some.
 406           unfold stripOutVars in *; simpl.
 407           unfold dropVar.
 408           unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 409
 410           destruct (eqd_dec v' v); subst.
 411
 412             (* where the leaf is v *)
 413             apply inr.
 414               subst.
 415               apply RuCanL.
 416
 417             (* where the leaf is NOT v *)
 418             apply inl.
 419               apply RuCanR.
 420
 421         (* empty leaf *)
 422         destruct case_None.
 423           apply inl; simpl in *.
 424           apply RuCanR.
 425
 426       (* branch *)
 427       refine (
 428         match IHctx1 with
 429           | inr lpf =>
 430             match IHctx2 with
 431               | inr rpf => let case_Both := tt in _
 432               | inl rpf => let case_Left := tt in _
 433             end
 434           | inl lpf =>
 435             match IHctx2 with
 436               | inr rpf => let case_Right   := tt in _
 437               | inl rpf => let case_Neither := tt in _
 438             end
 439         end); clear IHctx1; clear IHctx2.
 440
 441     destruct case_Neither.
 442       apply inl.
 443       eapply RComp; [idtac | apply RuCanR ].
 444         exact (RComp
 445           (* order will not matter because these are central as morphisms *)
 446           (RRight _ (RComp lpf (RCanR _)))
 447           (RLeft  _ (RComp rpf (RCanR _)))).
 448
 449
 450     destruct case_Right.
 451       apply inr.
 452       fold (stripOutVars (v::nil)).
 453       set (RRight (mapOptionTree ξ ctx2)  (RComp lpf ((RCanR _)))) as q.
 454       simpl in *.
 455       eapply RComp.
 456       apply q.
 457       clear q.
 458       clear lpf.
 459       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 460       eapply RComp; [ idtac | apply RAssoc ].
 461       apply RLeft.
 462       apply rpf.
 463
 464     destruct case_Left.
 465       apply inr.
 466       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 467       fold (stripOutVars (v::nil)).
 468       eapply RComp; [ idtac | eapply pivotContext ].
 469       set (RComp rpf (RCanR _ )) as rpf'.
 470       set (RLeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.
 471       simpl in *.
 472       eapply RComp; [ idtac | apply qq ].
 473       clear qq rpf' rpf.
 474       apply (RRight (mapOptionTree ξ ctx2)).
 475       apply lpf.
 476
 477     destruct case_Both.
 478       apply inr.
 479       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 480       fold (stripOutVars (v::nil)).
 481       eapply RComp; [ idtac | eapply copyAndPivotContext ].
 482         (* order will not matter because these are central as morphisms *)
 483         exact (RComp (RRight _ lpf) (RLeft _ rpf)).
 484
 485     Defined.
 486
 487 (* same as before, but use RWeak if necessary *)
 488 Definition arrangeContextAndWeaken
 489      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 490      v      (* variable to be pivoted, if found *)
 491      ctx    (* initial context *)
 492      (ξ:VV -> LeveledHaskType Γ ★) :
 493        Arrange
 494           (mapOptionTree ξ                        ctx                )
 495           (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])        ).
 496   set (arrangeContext Γ Δ v ctx ξ) as q.
 497   destruct q; auto.
 498   eapply RComp; [ apply a | idtac ].
 499   refine (RLeft _ (RWeak _)).
 500   Defined.
 501
 502 Lemma cheat : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a).
 503   admit.
 504   Qed.
 505
 506 Definition arrangeContextAndWeaken''
 507      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 508      v      (* variable to be pivoted, if found *)
 509      (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
 510   distinct (leaves v) ->
 511   Arrange
 512     ((mapOptionTree ξ ctx)                                       )
 513     ((mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v)).
 514
 515   induction v; intros.
 516     destruct a.
 517     unfold mapOptionTree in *.
 518     simpl in *.
 519     fold (mapOptionTree ξ) in *.
 520     intros.
 521     apply arrangeContextAndWeaken.
 522     apply Δ.
 523
 524   unfold mapOptionTree; simpl in *.
 525     intros.
 526     rewrite (@stripping_nothing_is_inert Γ); auto.
 527     apply RuCanR.
 528     intros.
 529     unfold mapOptionTree in *.
 530     simpl in *.
 531     fold (mapOptionTree ξ) in *.
 532     set (mapOptionTree ξ) as X in *.
 533
 534     set (IHv2 ((stripOutVars (leaves v1) ctx),, v1)) as IHv2'.
 535     unfold stripOutVars in IHv2'.
 536     simpl in IHv2'.
 537     fold (stripOutVars (leaves v2)) in IHv2'.
 538     fold (stripOutVars (leaves v1)) in IHv2'.
 539     unfold X in IHv2'.
 540     unfold mapOptionTree in IHv2'.
 541     simpl in IHv2'.
 542     fold (mapOptionTree ξ) in IHv2'.
 543     fold X in IHv2'.
 544     set (distinct_app _ _ _ H) as H'.
 545     destruct H' as [H1 H2].
 546     set (RComp (IHv1 _ H1) (IHv2' H2)) as qq.
 547     eapply RComp.
 548       apply qq.
 549       clear qq IHv2' IHv2 IHv1.
 550       rewrite strip_twice_lemma.
 551
 552       rewrite (strip_distinct' v1 (leaves v2)).
 553         apply RCossa.
 554         apply cheat.
 555         auto.
 556     Defined.
 557
 558 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
 559       mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
 560     = mapOptionTree ξ (stripOutVars (v :: nil) tree).
 561   set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
 562   rewrite p.
 563   simpl.
 564   reflexivity.
 565   Qed.
 566
 567 (* TODO: use multi-conclusion proofs instead *)
 568 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
 569   | lrsp_nil  : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
 570   | lrsp_leaf : forall v t e ,
 571     (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t@@lev]]) ->
 572     LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)
 573   | lrsp_cons : forall t1 t2 b1 b2,
 574     LetRecSubproofs Γ Δ ξ lev t1 b1 ->
 575     LetRecSubproofs Γ Δ ξ lev t2 b2 ->
 576     LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
 577
 578 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
 579   LetRecSubproofs Γ Δ ξ lev tree branches ->
 580     ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
 581       |- (mapOptionTree (@snd _ _) tree) @@@ lev ].
 582   intro X; induction X; intros; simpl in *.
 583     apply nd_rule.
 584       apply REmptyGroup.
 585     set (ξ v) as q in *.
 586       destruct q.
 587       simpl in *.
 588       apply n.
 589     eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
 590     eapply nd_comp; [ apply nd_llecnac | idtac ].
 591     apply nd_prod; auto.
 592   Defined.
 593
 594 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
 595     forall branches body,
 596     distinct (leaves (mapOptionTree (@fst _ _) tree)) ->
 597     ND Rule [] [Γ > Δ > mapOptionTree (update_ξ ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] ->
 598     LetRecSubproofs Γ Δ (update_ξ ξ lev (leaves tree)) lev tree branches ->
 599     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]].
 600
 601   (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
 602   intro branches.
 603   intro body.
 604   intro disti.
 605   intro pf.
 606   intro lrsp.
 607
 608   rewrite mapleaves in disti.
 609   set (@update_ξ_lemma _ Γ ξ lev tree disti) as ξlemma.
 610     rewrite <- mapOptionTree_compose in ξlemma.
 611
 612   set ((update_ξ ξ lev (leaves tree))) as ξ' in *.
 613   set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
 614   set (mapOptionTree (@fst _ _) tree) as pctx.
 615   set (mapOptionTree ξ' pctx) as passback.
 616   set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.
 617   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
 618   clear z.
 619
 620   set (@arrangeContextAndWeaken''  Γ Δ  pctx ξ' (expr2antecedent body,,eLetRecContext branches)) as q'.
 621   unfold passback in *; clear passback.
 622   unfold pctx in *; clear pctx.
 623   rewrite <- mapleaves in disti.
 624   set (q' disti) as q''.
 625
 626   unfold ξ' in *.
 627   set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
 628   rewrite <- mapleaves in zz.
 629   rewrite zz in q''.
 630   clear zz.
 631   clear ξ'.
 632   Opaque stripOutVars.
 633   simpl.
 634   rewrite <- mapOptionTree_compose in q''.
 635   rewrite <- ξlemma.
 636   eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ q'') ].
 637   clear q'.
 638   clear q''.
 639   simpl.
 640
 641   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
 642     eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
 643     eapply nd_comp; [ apply nd_llecnac | idtac ].
 644     apply nd_prod; auto.
 645     rewrite ξlemma.
 646     apply q.
 647     Defined.
 648
 649 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
 650   forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
 651     forall l ξ,
 652       vec2list (vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb)) =
 653       vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)).
 654   intros.
 655   unfold scbwv_ξ.
 656   unfold scbwv_varstypes.
 657   set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l)
 658     (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
 659     ) as q.
 660   rewrite <- mapleaves' in q.
 661   rewrite <- mapleaves' in q.
 662   rewrite <- mapleaves' in q.
 663   rewrite <- mapleaves' in q.
 664   set (fun z => unleaves_injective _ _ _ (q z)) as q'.
 665   rewrite vec2list_map_list2vec in q'.
 666   rewrite fst_zip in q'.
 667   rewrite vec2list_map_list2vec in q'.
 668   rewrite vec2list_map_list2vec in q'.
 669   rewrite snd_zip in q'.
 670   rewrite leaves_unleaves in q'.
 671   rewrite vec2list_map_list2vec in q'.
 672   rewrite vec2list_map_list2vec in q'.
 673   apply q'.
 674   rewrite fst_zip.
 675   apply scbwv_exprvars_distinct.
 676   Qed.
 677
 678
 679 Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
 680    (alts':Tree
 681             ??{sac : StrongAltCon &
 682               {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
 683               Expr (sac_Γ sac Γ) (sac_Δ sac Γ atypes (weakCK'' Δ))
 684                 (scbwv_ξ scb ξ l) (weakLT' (tbranches @@  l))}}),
 685
 686       (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
 687         (mapOptionTree mkProofCaseBranch alts'))
 688     ,,
 689     mapOptionTree ξ  (expr2antecedent e) =
 690   mapOptionTree ξ
 691         (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).
 692   intros.
 693   simpl.
 694   Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
 695   hack.
 696   induction alts'.
 697   destruct a; simpl.
 698   destruct s; simpl.
 699   unfold mkProofCaseBranch.
 700   reflexivity.
 701   reflexivity.
 702   simpl.
 703   rewrite IHalts'1.
 704   rewrite IHalts'2.
 705   reflexivity.
 706   rewrite H.
 707   reflexivity.
 708   Qed.
 709
 710 Definition expr2proof  :
 711   forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
 712     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
 713
 714   refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
 715     : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
 716     match exp as E in Expr Γ Δ ξ τ with
 717     | EGlobal  Γ Δ ξ t wev                          => let case_EGlobal := tt in _
 718     | EVar     Γ Δ ξ ev                             => let case_EVar := tt in _
 719     | ELit     Γ Δ ξ lit lev                        => let case_ELit := tt in _
 720     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => let case_EApp := tt in
 721                                                         (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
 722     | ELam     Γ Δ ξ t1 t2 lev v    e               => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 723     | ELet     Γ Δ ξ tv t      v lev ev ebody       => let case_ELet := tt in
 724                                                        (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
 725     | ELetRec  Γ Δ ξ lev t tree branches ebody      =>
 726       let ξ' := update_ξ ξ lev (leaves tree) in
 727       let case_ELetRec := tt in  (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
 728         ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
 729         (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
 730         : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
 731         match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
 732           | ELR_nil    Γ Δ ξ lev  => lrsp_nil _ _ _ _
 733           | ELR_leaf   Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ e)
 734           | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
 735         end
 736         ) _ _ _ _ tree branches)
 737     | EEsc     Γ Δ ξ ec t lev e                     => let case_EEsc    := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 738     | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 739     | ECast    Γ Δ ξ γ t1 t2 lev      e             => let case_ECast   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 740     | ENote    Γ Δ ξ t n e                          => let case_ENote   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 741     | ETyLam   Γ Δ ξ κ σ l e                        => let case_ETyLam  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 742     | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 743     | ECoApp   Γ Δ κ σ₁ σ₂ σ γ ξ l      e           => let case_ECoApp  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 744     | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 745     | ECase    Γ Δ ξ l tc tbranches atypes e alts' =>
 746       let dcsp :=
 747         ((fix mkdcsp (alts:
 748                Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
 749                             & Expr (sac_Γ sac Γ)
 750                                    (sac_Δ sac Γ atypes (weakCK'' Δ))
 751                                    (scbwv_ξ scb ξ l)
 752                                    (weakLT' (tbranches@@l)) } })
 753           : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
 754         match alts as ALTS return ND Rule []
 755           (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
 756           | T_Leaf None      => let case_nil := tt in _
 757           | T_Branch b1 b2   => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
 758           | T_Leaf (Some x)  =>
 759             match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
 760             existT sac (existT scbx ex) =>
 761             (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex)
 762         end
 763         end) alts')
 764         in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 765     end
 766   ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
 767
 768     destruct case_EGlobal.
 769       apply nd_rule.
 770       simpl.
 771       destruct t as [t lev].
 772       apply (RGlobal _ _ _ _ wev).
 773
 774     destruct case_EVar.
 775       apply nd_rule.
 776       unfold mapOptionTree; simpl.
 777       destruct (ξ ev).
 778       apply RVar.
 779
 780     destruct case_ELit.
 781       apply nd_rule.
 782       apply RLit.
 783
 784     destruct case_EApp.
 785       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
 786       eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
 787       eapply nd_comp; [ apply nd_llecnac | idtac ].
 788       apply nd_prod; auto.
 789       apply e1'.
 790       apply e2'.
 791
 792     destruct case_ELam; intros.
 793       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
 794       eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
 795       set (update_ξ ξ lev ((v,t1)::nil)) as ξ'.
 796       set (arrangeContextAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx.
 797         eapply RArrange in pfx.
 798         unfold mapOptionTree in pfx; simpl in pfx.
 799         unfold ξ' in pfx.
 800         rewrite updating_stripped_tree_is_inert in pfx.
 801         unfold update_ξ in pfx.
 802         destruct (eqd_dec v v).
 803         eapply nd_comp; [ idtac | apply (nd_rule pfx) ].
 804         clear pfx.
 805         apply e'.
 806         assert False.
 807         apply n.
 808         auto.
 809         inversion H.
 810
 811     destruct case_ELet; intros; simpl in *.
 812       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 813       eapply nd_comp; [ apply nd_llecnac | idtac ].
 814       apply nd_prod.
 815         apply pf_let.
 816         clear pf_let.
 817         eapply nd_comp; [ apply pf_body | idtac ].
 818         clear pf_body.
 819       fold (@mapOptionTree VV).
 820       fold (mapOptionTree ξ).
 821       set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.
 822       set (arrangeContextAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n.
 823       unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
 824       unfold ξ' in n.
 825       rewrite updating_stripped_tree_is_inert in n.
 826       unfold update_ξ in n.
 827       destruct (eqd_dec lev lev).
 828       unfold ξ'.
 829       unfold update_ξ.
 830       eapply RArrange in n.
 831       apply (nd_rule n).
 832       assert False. apply n0; auto. inversion H.
 833
 834     destruct case_EEsc.
 835       eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
 836       apply e'.
 837
 838     destruct case_EBrak; intros.
 839       eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
 840       apply e'.
 841
 842     destruct case_ECast.
 843       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
 844       apply e'.
 845       auto.
 846
 847     destruct case_ENote.
 848       destruct t.
 849       eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
 850       apply e'.
 851       auto.
 852
 853     destruct case_ETyApp; simpl in *; intros.
 854       eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
 855       apply e'.
 856       auto.
 857
 858     destruct case_ECoLam; simpl in *; intros.
 859       eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
 860       apply e'.
 861
 862     destruct case_ECoApp; simpl in *; intros.
 863       eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
 864       apply e'.
 865       auto.
 866
 867     destruct case_ETyLam; intros.
 868       eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
 869       unfold mapOptionTree in e'.
 870       rewrite mapOptionTree_compose in e'.
 871       unfold mapOptionTree.
 872       apply e'.
 873
 874     destruct case_leaf.
 875       clear o x alts alts' e.
 876       eapply nd_comp; [ apply e' | idtac ].
 877       clear e'.
 878       apply nd_rule.
 879       apply RArrange.
 880       simpl.
 881       rewrite mapleaves'.
 882       simpl.
 883       rewrite <- mapOptionTree_compose.
 884       unfold scbwv_ξ.
 885       rewrite <- mapleaves'.
 886       rewrite vec2list_map_list2vec.
 887       unfold sac_Γ.
 888       rewrite <- (scbwv_coherent scbx l ξ).
 889       rewrite <- vec2list_map_list2vec.
 890       rewrite mapleaves'.
 891       set (@arrangeContextAndWeaken'') as q.
 892       unfold scbwv_ξ.
 893       set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
 894       unfold scbwv_varstypes in z.
 895       rewrite vec2list_map_list2vec in z.
 896       rewrite fst_zip in z.
 897       rewrite <- z.
 898       clear z.
 899       replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
 900         (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
 901       apply q.
 902       apply (sac_Δ sac Γ atypes (weakCK'' Δ)).
 903       rewrite leaves_unleaves.
 904       apply (scbwv_exprvars_distinct scbx).
 905       rewrite leaves_unleaves.
 906       reflexivity.
 907
 908     destruct case_nil.
 909       apply nd_id0.
 910
 911     destruct case_branch.
 912       simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
 913       apply nd_prod.
 914       apply b1'.
 915       apply b2'.
 916
 917     destruct case_ECase.
 918     set (@RCase Γ Δ l tc) as q.
 919       rewrite <- case_lemma.
 920       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
 921       eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
 922       rewrite <- mapOptionTree_compose.
 923       apply dcsp.
 924       apply e'.
 925
 926     destruct case_ELetRec; intros.
 927       unfold ξ'0 in *.
 928       clear ξ'0.
 929       unfold ξ'1 in *.
 930       clear ξ'1.
 931       apply letRecSubproofsToND'.
 932       admit.
 933       apply e'.
 934       apply subproofs.
 935
 936   Defined.
 937
 938 End HaskStrongToProof.
 939