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 Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV :=
 368   match elrb with
 369   | ELR_nil    Γ Δ ξ lev  => []
 370   | ELR_leaf   Γ Δ ξ  lev  v _ _ e => [v]
 371   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2)
 372   end.
 373
 374 Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * HaskType Γ ★):=
 375   match elrb with
 376   | ELR_nil    Γ Δ ξ lev  => []
 377   | ELR_leaf   Γ Δ ξ  lev  v t _ e => [(v, t)]
 378   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2)
 379   end.
 380 *)
 381
 382 Lemma stripping_nothing_is_inert
 383   {Γ:TypeEnv}
 384   (ξ:VV -> LeveledHaskType Γ ★)
 385   tree :
 386   stripOutVars nil tree = tree.
 387   induction tree.
 388     simpl; destruct a; reflexivity.
 389     unfold stripOutVars.
 390     fold stripOutVars.
 391     simpl.
 392     fold (stripOutVars nil).
 393     rewrite <- IHtree1 at 2.
 394     rewrite <- IHtree2 at 2.
 395     reflexivity.
 396     Qed.
 397
 398 Definition arrangeContext
 399      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 400      v      (* variable to be pivoted, if found *)
 401      ctx    (* initial context *)
 402      (ξ:VV -> LeveledHaskType Γ ★)
 403      :
 404
 405     (* a proof concluding in a context where that variable does not appear *)
 406      sum (Arrange
 407           (mapOptionTree ξ                        ctx                        )
 408           (mapOptionTree ξ (stripOutVars (v::nil) ctx),,[]                   ))
 409
 410     (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
 411         (Arrange
 412           (mapOptionTree ξ                         ctx                       )
 413           (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])                )).
 414
 415   induction ctx.
 416
 417     refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
 418
 419         (* nonempty leaf *)
 420         destruct case_Some.
 421           unfold stripOutVars in *; simpl.
 422           unfold dropVar.
 423           unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 424
 425           destruct (eqd_dec v' v); subst.
 426
 427             (* where the leaf is v *)
 428             apply inr.
 429               subst.
 430               apply RuCanL.
 431
 432             (* where the leaf is NOT v *)
 433             apply inl.
 434               apply RuCanR.
 435
 436         (* empty leaf *)
 437         destruct case_None.
 438           apply inl; simpl in *.
 439           apply RuCanR.
 440
 441       (* branch *)
 442       refine (
 443         match IHctx1 with
 444           | inr lpf =>
 445             match IHctx2 with
 446               | inr rpf => let case_Both := tt in _
 447               | inl rpf => let case_Left := tt in _
 448             end
 449           | inl lpf =>
 450             match IHctx2 with
 451               | inr rpf => let case_Right   := tt in _
 452               | inl rpf => let case_Neither := tt in _
 453             end
 454         end); clear IHctx1; clear IHctx2.
 455
 456     destruct case_Neither.
 457       apply inl.
 458       eapply RComp; [idtac | apply RuCanR ].
 459         exact (RComp
 460           (* order will not matter because these are central as morphisms *)
 461           (RRight _ (RComp lpf (RCanR _)))
 462           (RLeft  _ (RComp rpf (RCanR _)))).
 463
 464
 465     destruct case_Right.
 466       apply inr.
 467       fold (stripOutVars (v::nil)).
 468       set (RRight (mapOptionTree ξ ctx2)  (RComp lpf ((RCanR _)))) as q.
 469       simpl in *.
 470       eapply RComp.
 471       apply q.
 472       clear q.
 473       clear lpf.
 474       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 475       eapply RComp; [ idtac | apply RAssoc ].
 476       apply RLeft.
 477       apply rpf.
 478
 479     destruct case_Left.
 480       apply inr.
 481       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 482       fold (stripOutVars (v::nil)).
 483       eapply RComp; [ idtac | eapply pivotContext ].
 484       set (RComp rpf (RCanR _ )) as rpf'.
 485       set (RLeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.
 486       simpl in *.
 487       eapply RComp; [ idtac | apply qq ].
 488       clear qq rpf' rpf.
 489       apply (RRight (mapOptionTree ξ ctx2)).
 490       apply lpf.
 491
 492     destruct case_Both.
 493       apply inr.
 494       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 495       fold (stripOutVars (v::nil)).
 496       eapply RComp; [ idtac | eapply copyAndPivotContext ].
 497         (* order will not matter because these are central as morphisms *)
 498         exact (RComp (RRight _ lpf) (RLeft _ rpf)).
 499
 500     Defined.
 501
 502 (* same as before, but use RWeak if necessary *)
 503 Definition arrangeContextAndWeaken
 504      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 505      v      (* variable to be pivoted, if found *)
 506      ctx    (* initial context *)
 507      (ξ:VV -> LeveledHaskType Γ ★) :
 508        Arrange
 509           (mapOptionTree ξ                        ctx                )
 510           (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])        ).
 511   set (arrangeContext Γ Δ v ctx ξ) as q.
 512   destruct q; auto.
 513   eapply RComp; [ apply a | idtac ].
 514   refine (RLeft _ (RWeak _)).
 515   Defined.
 516
 517 Lemma cheat : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a).
 518   admit.
 519   Qed.
 520
 521 Definition arrangeContextAndWeaken''
 522      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 523      v      (* variable to be pivoted, if found *)
 524      (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
 525   distinct (leaves v) ->
 526   Arrange
 527     ((mapOptionTree ξ ctx)                                       )
 528     ((mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v)).
 529
 530   induction v; intros.
 531     destruct a.
 532     unfold mapOptionTree in *.
 533     simpl in *.
 534     fold (mapOptionTree ξ) in *.
 535     intros.
 536     apply arrangeContextAndWeaken.
 537     apply Δ.
 538
 539   unfold mapOptionTree; simpl in *.
 540     intros.
 541     rewrite (@stripping_nothing_is_inert Γ); auto.
 542     apply RuCanR.
 543     intros.
 544     unfold mapOptionTree in *.
 545     simpl in *.
 546     fold (mapOptionTree ξ) in *.
 547     set (mapOptionTree ξ) as X in *.
 548
 549     set (IHv2 ((stripOutVars (leaves v1) ctx),, v1)) as IHv2'.
 550     unfold stripOutVars in IHv2'.
 551     simpl in IHv2'.
 552     fold (stripOutVars (leaves v2)) in IHv2'.
 553     fold (stripOutVars (leaves v1)) in IHv2'.
 554     unfold X in IHv2'.
 555     unfold mapOptionTree in IHv2'.
 556     simpl in IHv2'.
 557     fold (mapOptionTree ξ) in IHv2'.
 558     fold X in IHv2'.
 559     set (distinct_app _ _ _ H) as H'.
 560     destruct H' as [H1 H2].
 561     set (RComp (IHv1 _ H1) (IHv2' H2)) as qq.
 562     eapply RComp.
 563       apply qq.
 564       clear qq IHv2' IHv2 IHv1.
 565       rewrite strip_twice_lemma.
 566
 567       rewrite (strip_distinct' v1 (leaves v2)).
 568         apply RCossa.
 569         apply cheat.
 570         auto.
 571     Defined.
 572
 573 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
 574       mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
 575     = mapOptionTree ξ (stripOutVars (v :: nil) tree).
 576   set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
 577   rewrite p.
 578   simpl.
 579   reflexivity.
 580   Qed.
 581
 582 (* IDEA: use multi-conclusion proofs instead *)
 583 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
 584   | lrsp_nil  : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
 585   | lrsp_leaf : forall v t e ,
 586     (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t@@lev]]) ->
 587     LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)
 588   | lrsp_cons : forall t1 t2 b1 b2,
 589     LetRecSubproofs Γ Δ ξ lev t1 b1 ->
 590     LetRecSubproofs Γ Δ ξ lev t2 b2 ->
 591     LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
 592
 593 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
 594   LetRecSubproofs Γ Δ ξ lev tree branches ->
 595     ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
 596       |- (mapOptionTree (@snd _ _) tree) @@@ lev ].
 597   intro X; induction X; intros; simpl in *.
 598     apply nd_rule.
 599       apply REmptyGroup.
 600     set (ξ v) as q in *.
 601       destruct q.
 602       simpl in *.
 603       apply n.
 604     eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
 605     eapply nd_comp; [ apply nd_llecnac | idtac ].
 606     apply nd_prod; auto.
 607   Defined.
 608
 609 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
 610     forall branches body,
 611     distinct (leaves (mapOptionTree (@fst _ _) tree)) ->
 612     ND Rule [] [Γ > Δ > mapOptionTree (update_ξ ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] ->
 613     LetRecSubproofs Γ Δ (update_ξ ξ lev (leaves tree)) lev tree branches ->
 614     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]].
 615
 616   (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
 617   intro branches.
 618   intro body.
 619   intro disti.
 620   intro pf.
 621   intro lrsp.
 622
 623   rewrite mapleaves in disti.
 624   set (@update_ξ_lemma _ Γ ξ lev tree disti) as ξlemma.
 625     rewrite <- mapOptionTree_compose in ξlemma.
 626
 627   set ((update_ξ ξ lev (leaves tree))) as ξ' in *.
 628   set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
 629   set (mapOptionTree (@fst _ _) tree) as pctx.
 630   set (mapOptionTree ξ' pctx) as passback.
 631   set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.
 632   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
 633   clear z.
 634
 635   set (@arrangeContextAndWeaken''  Γ Δ  pctx ξ' (expr2antecedent body,,eLetRecContext branches)) as q'.
 636   unfold passback in *; clear passback.
 637   unfold pctx in *; clear pctx.
 638   rewrite <- mapleaves in disti.
 639   set (q' disti) as q''.
 640
 641   unfold ξ' in *.
 642   set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
 643   rewrite <- mapleaves in zz.
 644   rewrite zz in q''.
 645   clear zz.
 646   clear ξ'.
 647   Opaque stripOutVars.
 648   simpl.
 649   rewrite <- mapOptionTree_compose in q''.
 650   rewrite <- ξlemma.
 651   eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ q'') ].
 652   clear q'.
 653   clear q''.
 654   simpl.
 655
 656   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
 657     eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
 658     eapply nd_comp; [ apply nd_llecnac | idtac ].
 659     apply nd_prod; auto.
 660     rewrite ξlemma.
 661     apply q.
 662     Defined.
 663
 664 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
 665   forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
 666     forall l ξ,
 667       vec2list (vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb)) =
 668       vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)).
 669   intros.
 670   unfold scbwv_ξ.
 671   unfold scbwv_varstypes.
 672   set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l)
 673     (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
 674     ) as q.
 675   rewrite <- mapleaves' in q.
 676   rewrite <- mapleaves' in q.
 677   rewrite <- mapleaves' in q.
 678   rewrite <- mapleaves' in q.
 679   set (fun z => unleaves_injective _ _ _ (q z)) as q'.
 680   rewrite vec2list_map_list2vec in q'.
 681   rewrite fst_zip in q'.
 682   rewrite vec2list_map_list2vec in q'.
 683   rewrite vec2list_map_list2vec in q'.
 684   rewrite snd_zip in q'.
 685   rewrite leaves_unleaves in q'.
 686   rewrite vec2list_map_list2vec in q'.
 687   rewrite vec2list_map_list2vec in q'.
 688   apply q'.
 689   rewrite fst_zip.
 690   apply scbwv_exprvars_distinct.
 691   Qed.
 692
 693
 694 Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
 695    (alts':Tree
 696             ??{sac : StrongAltCon &
 697               {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
 698               Expr (sac_Γ sac Γ) (sac_Δ sac Γ atypes (weakCK'' Δ))
 699                 (scbwv_ξ scb ξ l) (weakLT' (tbranches @@  l))}}),
 700
 701       (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
 702         (mapOptionTree mkProofCaseBranch alts'))
 703     ,,
 704     mapOptionTree ξ  (expr2antecedent e) =
 705   mapOptionTree ξ
 706         (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).
 707   intros.
 708   simpl.
 709   Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
 710   hack.
 711   induction alts'.
 712   destruct a; simpl.
 713   destruct s; simpl.
 714   unfold mkProofCaseBranch.
 715   reflexivity.
 716   reflexivity.
 717   simpl.
 718   rewrite IHalts'1.
 719   rewrite IHalts'2.
 720   reflexivity.
 721   rewrite H.
 722   reflexivity.
 723   Qed.
 724
 725 Definition expr2proof  :
 726   forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
 727     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
 728
 729   refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
 730     : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
 731     match exp as E in Expr Γ Δ ξ τ with
 732     | EGlobal  Γ Δ ξ t wev                          => let case_EGlobal := tt in _
 733     | EVar     Γ Δ ξ ev                             => let case_EVar := tt in _
 734     | ELit     Γ Δ ξ lit lev                        => let case_ELit := tt in _
 735     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => let case_EApp := tt in
 736                                                         (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
 737     | ELam     Γ Δ ξ t1 t2 lev v    e               => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 738     | ELet     Γ Δ ξ tv t      v lev ev ebody       => let case_ELet := tt in
 739                                                        (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
 740     | ELetRec  Γ Δ ξ lev t tree branches ebody      =>
 741       let ξ' := update_ξ ξ lev (leaves tree) in
 742       let case_ELetRec := tt in  (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
 743         ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
 744         (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
 745         : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
 746         match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
 747           | ELR_nil    Γ Δ ξ lev  => lrsp_nil _ _ _ _
 748           | ELR_leaf   Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ e)
 749           | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
 750         end
 751         ) _ _ _ _ tree branches)
 752     | EEsc     Γ Δ ξ ec t lev e                     => let case_EEsc    := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 753     | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 754     | ECast    Γ Δ ξ γ t1 t2 lev      e             => let case_ECast   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 755     | ENote    Γ Δ ξ t n e                          => let case_ENote   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 756     | ETyLam   Γ Δ ξ κ σ l e                        => let case_ETyLam  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 757     | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 758     | ECoApp   Γ Δ κ σ₁ σ₂ σ γ ξ l      e           => let case_ECoApp  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 759     | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 760     | ECase    Γ Δ ξ l tc tbranches atypes e alts' =>
 761       let dcsp :=
 762         ((fix mkdcsp (alts:
 763                Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
 764                             & Expr (sac_Γ sac Γ)
 765                                    (sac_Δ sac Γ atypes (weakCK'' Δ))
 766                                    (scbwv_ξ scb ξ l)
 767                                    (weakLT' (tbranches@@l)) } })
 768           : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
 769         match alts as ALTS return ND Rule []
 770           (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
 771           | T_Leaf None      => let case_nil := tt in _
 772           | T_Branch b1 b2   => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
 773           | T_Leaf (Some x)  =>
 774             match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
 775             existT sac (existT scbx ex) =>
 776             (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex)
 777         end
 778         end) alts')
 779         in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 780     end
 781   ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
 782
 783     destruct case_EGlobal.
 784       apply nd_rule.
 785       simpl.
 786       destruct t as [t lev].
 787       apply (RGlobal _ _ _ _ wev).
 788
 789     destruct case_EVar.
 790       apply nd_rule.
 791       unfold mapOptionTree; simpl.
 792       destruct (ξ ev).
 793       apply RVar.
 794
 795     destruct case_ELit.
 796       apply nd_rule.
 797       apply RLit.
 798
 799     destruct case_EApp.
 800       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
 801       eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
 802       eapply nd_comp; [ apply nd_llecnac | idtac ].
 803       apply nd_prod; auto.
 804       apply e1'.
 805       apply e2'.
 806
 807     destruct case_ELam; intros.
 808       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
 809       eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
 810       set (update_ξ ξ lev ((v,t1)::nil)) as ξ'.
 811       set (arrangeContextAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx.
 812         eapply RArrange in pfx.
 813         unfold mapOptionTree in pfx; simpl in pfx.
 814         unfold ξ' in pfx.
 815         rewrite updating_stripped_tree_is_inert in pfx.
 816         unfold update_ξ in pfx.
 817         destruct (eqd_dec v v).
 818         eapply nd_comp; [ idtac | apply (nd_rule pfx) ].
 819         clear pfx.
 820         apply e'.
 821         assert False.
 822         apply n.
 823         auto.
 824         inversion H.
 825
 826     destruct case_ELet; intros; simpl in *.
 827       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 828       eapply nd_comp; [ apply nd_llecnac | idtac ].
 829       apply nd_prod; [ idtac | apply pf_let].
 830       clear pf_let.
 831       eapply nd_comp; [ apply pf_body | idtac ].
 832       clear pf_body.
 833       fold (@mapOptionTree VV).
 834       fold (mapOptionTree ξ).
 835       set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.
 836       set (arrangeContextAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n.
 837       unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
 838       unfold ξ' in n.
 839       rewrite updating_stripped_tree_is_inert in n.
 840       unfold update_ξ in n.
 841       destruct (eqd_dec lev lev).
 842       unfold ξ'.
 843       unfold update_ξ.
 844       eapply RArrange in n.
 845       apply (nd_rule n).
 846       assert False. apply n0; auto. inversion H.
 847
 848     destruct case_EEsc.
 849       eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
 850       apply e'.
 851
 852     destruct case_EBrak; intros.
 853       eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
 854       apply e'.
 855
 856     destruct case_ECast.
 857       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
 858       apply e'.
 859       auto.
 860
 861     destruct case_ENote.
 862       destruct t.
 863       eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
 864       apply e'.
 865       auto.
 866
 867     destruct case_ETyApp; simpl in *; intros.
 868       eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
 869       apply e'.
 870       auto.
 871
 872     destruct case_ECoLam; simpl in *; intros.
 873       eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
 874       apply e'.
 875
 876     destruct case_ECoApp; simpl in *; intros.
 877       eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
 878       apply e'.
 879       auto.
 880
 881     destruct case_ETyLam; intros.
 882       eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
 883       unfold mapOptionTree in e'.
 884       rewrite mapOptionTree_compose in e'.
 885       unfold mapOptionTree.
 886       apply e'.
 887
 888     destruct case_leaf.
 889       clear o x alts alts' e.
 890       eapply nd_comp; [ apply e' | idtac ].
 891       clear e'.
 892       apply nd_rule.
 893       apply RArrange.
 894       simpl.
 895       rewrite mapleaves'.
 896       simpl.
 897       rewrite <- mapOptionTree_compose.
 898       unfold scbwv_ξ.
 899       rewrite <- mapleaves'.
 900       rewrite vec2list_map_list2vec.
 901       unfold sac_Γ.
 902       rewrite <- (scbwv_coherent scbx l ξ).
 903       rewrite <- vec2list_map_list2vec.
 904       rewrite mapleaves'.
 905       set (@arrangeContextAndWeaken'') as q.
 906       unfold scbwv_ξ.
 907       set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
 908       unfold scbwv_varstypes in z.
 909       rewrite vec2list_map_list2vec in z.
 910       rewrite fst_zip in z.
 911       rewrite <- z.
 912       clear z.
 913       replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
 914         (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
 915       apply q.
 916       apply (sac_Δ sac Γ atypes (weakCK'' Δ)).
 917       rewrite leaves_unleaves.
 918       apply (scbwv_exprvars_distinct scbx).
 919       rewrite leaves_unleaves.
 920       reflexivity.
 921
 922     destruct case_nil.
 923       apply nd_id0.
 924
 925     destruct case_branch.
 926       simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
 927       apply nd_prod.
 928       apply b1'.
 929       apply b2'.
 930
 931     destruct case_ECase.
 932     set (@RCase Γ Δ l tc) as q.
 933       rewrite <- case_lemma.
 934       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
 935       eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
 936       rewrite <- mapOptionTree_compose.
 937       apply dcsp.
 938       apply e'.
 939
 940     destruct case_ELetRec; intros.
 941       unfold ξ'0 in *.
 942       clear ξ'0.
 943       unfold ξ'1 in *.
 944       clear ξ'1.
 945       apply letRecSubproofsToND'.
 946       admit.
 947       apply e'.
 948       apply subproofs.
 949
 950   Defined.
 951
 952 End HaskStrongToProof.
 953