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