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