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   Definition dropVar (lv:list VV)(v:VV) : ??VV :=
  60     if fold_left
  61       (fun a b:bool => if a then true else if b then true else false)
  62       (map (fun lvv => if eqd_dec lvv v then true else false) lv)
  63       false
  64       then None
  65       else Some v.
  66   (* later: use mapOptionTreeAndFlatten *)
  67   Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=
  68     mapTree (fun x => match x with None => None | Some vt => dropVar lv vt end).
  69
  70 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
  71   match exp as E in Expr Γ Δ ξ τ with
  72   | EGlobal  Γ Δ ξ _ _                            => []
  73   | EVar     Γ Δ ξ ev                             => [ev]
  74   | ELit     Γ Δ ξ lit lev                        => []
  75   | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e1),,(expr2antecedent e2)
  76   | ELam     Γ Δ ξ t1 t2 lev v    e               => stripOutVars (v::nil) (expr2antecedent e)
  77   | ELet     Γ Δ ξ tv t  lev v ev ebody           => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
  78   | EEsc     Γ Δ ξ ec t lev e                     => expr2antecedent e
  79   | EBrak    Γ Δ ξ ec t lev e                     => expr2antecedent e
  80   | ECast    Γ Δ ξ γ t1 t2 lev      e             => expr2antecedent e
  81   | ENote    Γ Δ ξ t n e                          => expr2antecedent e
  82   | ETyLam   Γ Δ ξ κ σ l e                        => expr2antecedent e
  83   | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => expr2antecedent e
  84   | ECoApp   Γ Δ κ γ σ₁ σ₂ σ ξ l      e           => expr2antecedent e
  85   | ETyApp   Γ Δ κ σ τ ξ  l    e                  => expr2antecedent e
  86   | ELetRec  Γ Δ ξ l τ vars branches body         =>
  87       let branch_context := eLetRecContext branches
  88    in let all_contexts := (expr2antecedent body),,branch_context
  89    in     stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
  90   | ECase    Γ Δ ξ l tc tbranches atypes e' alts =>
  91     ((fix varsfromalts (alts:
  92                Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
  93                             & Expr (sac_Γ scb Γ)
  94                                    (sac_Δ scb Γ atypes (weakCK'' Δ))
  95                                    (scbwv_ξ scb ξ l)
  96                                    (weakLT' (tbranches@@l)) }
  97       ): Tree ??VV :=
  98       match alts with
  99         | T_Leaf None     => []
 100         | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 h))) (expr2antecedent (projT2 h))
 101         | T_Branch b1 b2  => (varsfromalts b1),,(varsfromalts b2)
 102       end) alts),,(expr2antecedent e')
 103 end
 104 with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
 105 match elrb with
 106   | ELR_nil    Γ Δ ξ lev  => []
 107   | ELR_leaf   Γ Δ ξ lev v e => expr2antecedent e
 108   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
 109 end.
 110
 111 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
 112   (alt: { scb : StrongCaseBranchWithVVs _ _ tc atypes
 113                             & Expr (sac_Γ scb Γ)
 114                                    (sac_Δ scb Γ atypes (weakCK'' Δ))
 115                                    (scbwv_ξ scb ξ l)
 116                                    (weakLT' (tbranches@@l)) })
 117   : ProofCaseBranch tc Γ Δ l tbranches atypes.
 118   exact
 119     {| pcb_scb := projT1 alt
 120      ; pcb_freevars := mapOptionTree ξ (stripOutVars (vec2list (scbwv_exprvars (projT1 alt))) (expr2antecedent (projT2 alt)))
 121      |}.
 122      Defined.
 123
 124 Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(LeveledHaskType Γ ★) :=
 125   match elrb with
 126   | ELR_nil    Γ Δ ξ lev  => []
 127   | ELR_leaf   Γ Δ ξ  lev  v e => [ξ v]
 128   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
 129   end.
 130
 131 Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV :=
 132   match elrb with
 133   | ELR_nil    Γ Δ ξ lev  => []
 134   | ELR_leaf   Γ Δ ξ  lev  v e => [v]
 135   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2)
 136   end.
 137
 138 Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * LeveledHaskType Γ ★):=
 139   match elrb with
 140   | ELR_nil    Γ Δ ξ lev  => []
 141   | ELR_leaf   Γ Δ ξ  lev  v e => [(v, ξ v)]
 142   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2)
 143   end.
 144
 145
 146 Lemma stripping_nothing_is_inert
 147   {Γ:TypeEnv}
 148   (ξ:VV -> LeveledHaskType Γ ★)
 149   tree :
 150   stripOutVars nil tree = tree.
 151   induction tree.
 152     simpl; destruct a; reflexivity.
 153     unfold stripOutVars.
 154     fold stripOutVars.
 155     simpl.
 156     fold (stripOutVars nil).
 157     rewrite IHtree1.
 158     rewrite IHtree2.
 159     reflexivity.
 160     Qed.
 161
 162
 163
 164 Definition arrangeContext
 165      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
 166      v      (* variable to be pivoted, if found *)
 167      ctx    (* initial context *)
 168      τ      (* type of succedent *)
 169      (ξ:VV -> LeveledHaskType Γ ★)
 170      :
 171
 172     (* a proof concluding in a context where that variable does not appear *)
 173     sum (ND (@URule Γ Δ)
 174           [Γ >> Δ > mapOptionTree ξ                        ctx                        |- τ]
 175           [Γ >> Δ > mapOptionTree ξ (stripOutVars (v::nil) ctx),,[]                   |- τ])
 176
 177     (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
 178         (ND (@URule Γ Δ)
 179           [Γ >> Δ > mapOptionTree ξ                         ctx                       |- τ]
 180           [Γ >> Δ > mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])                |- τ]).
 181
 182   induction ctx; simpl in *.
 183
 184     refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end); simpl in *.
 185
 186         (* nonempty leaf *)
 187         destruct case_Some.
 188           unfold stripOutVars in *; simpl.
 189           unfold dropVar.
 190           unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 191           destruct (eqd_dec v v'); simpl in *.
 192
 193             (* where the leaf is v *)
 194             apply inr.
 195               subst.
 196               apply nd_rule.
 197               apply RuCanL.
 198
 199             (* where the leaf is NOT v *)
 200             apply inl.
 201               apply nd_rule.
 202               apply RuCanR.
 203
 204         (* empty leaf *)
 205         destruct case_None.
 206           apply inl; simpl in *.
 207           apply nd_rule.
 208           apply RuCanR.
 209
 210       (* branch *)
 211       refine (
 212         match IHctx1 with
 213           | inr lpf =>
 214             match IHctx2 with
 215               | inr rpf => let case_Both := tt in _
 216               | inl rpf => let case_Left := tt in _
 217             end
 218           | inl lpf =>
 219             match IHctx2 with
 220               | inr rpf => let case_Right   := tt in _
 221               | inl rpf => let case_Neither := tt in _
 222             end
 223         end); clear IHctx1; clear IHctx2.
 224
 225     destruct case_Neither.
 226       apply inl.
 227       eapply nd_comp; [idtac | eapply nd_rule; apply RuCanR ].
 228         exact (nd_comp
 229           (* order will not matter because these are central as morphisms *)
 230           (ext_right _ _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _))))
 231           (ext_left  _ _ _ (nd_comp rpf (nd_rule (@RCanR _ _ _ _))))).
 232
 233
 234     destruct case_Right.
 235       apply inr.
 236       fold (stripOutVars (v::nil)).
 237       set (ext_right (mapOptionTree ξ ctx2) _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _)))) as q.
 238       simpl in *.
 239       eapply nd_comp.
 240       apply q.
 241       clear q.
 242       clear lpf.
 243       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 244       eapply nd_comp; [ idtac | eapply nd_rule; apply RAssoc ].
 245       set (ext_left (mapOptionTree ξ (stripOutVars (v :: nil) ctx1)) [Γ >> Δ>mapOptionTree ξ ctx2 |- τ]
 246                                                             [Γ >> Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx2),,[ξ v])  |- τ]) as qq.
 247       apply qq.
 248       clear qq.
 249       apply rpf.
 250
 251     destruct case_Left.
 252       apply inr.
 253       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 254       fold (stripOutVars (v::nil)).
 255       eapply nd_comp; [ idtac | eapply pivotContext ].
 256       set (nd_comp rpf (nd_rule (@RCanR _ _ _ _ ) ) ) as rpf'.
 257       set (ext_left ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) _ _ rpf') as qq.
 258       simpl in *.
 259       eapply nd_comp; [ idtac | apply qq ].
 260       clear qq rpf' rpf.
 261       set (ext_right (mapOptionTree ξ ctx2) [Γ >>Δ> mapOptionTree ξ ctx1 |- τ] [Γ >>Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v]) |- τ]) as q.
 262       apply q.
 263       clear q.
 264       apply lpf.
 265
 266     destruct case_Both.
 267       apply inr.
 268       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 269       fold (stripOutVars (v::nil)).
 270       eapply nd_comp; [ idtac | eapply copyAndPivotContext ].
 271         exact (nd_comp
 272           (* order will not matter because these are central as morphisms *)
 273           (ext_right _ _ _ lpf)
 274           (ext_left  _ _ _ rpf)).
 275
 276     Defined.
 277
 278 (* same as before, but use RWeak if necessary *)
 279 Definition arrangeContextAndWeaken v ctx Γ Δ τ ξ :
 280        ND (@URule Γ Δ)
 281           [Γ >> Δ>mapOptionTree ξ                        ctx                |- τ]
 282           [Γ >> Δ>mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])        |- τ].
 283   set (arrangeContext Γ Δ v ctx τ ξ) as q.
 284   destruct q; auto.
 285   eapply nd_comp; [ apply n | idtac ].
 286   clear n.
 287   refine (ext_left _ _ _ (nd_rule (RWeak _ _))).
 288   Defined.
 289
 290 Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
 291   ND (@URule Γ Δ)
 292     [Γ >> Δ>(mapOptionTree ξ ctx)                                       |-  z]
 293     [Γ >> Δ>(mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v) |-  z].
 294
 295   induction v.
 296     destruct a.
 297     unfold mapOptionTree in *.
 298     simpl in *.
 299     fold (mapOptionTree ξ) in *.
 300     intros.
 301     apply arrangeContextAndWeaken.
 302
 303   unfold mapOptionTree; simpl in *.
 304     intros.
 305     rewrite (@stripping_nothing_is_inert Γ); auto.
 306     apply nd_rule.
 307     apply RuCanR.
 308     intros.
 309     unfold mapOptionTree in *.
 310     simpl in *.
 311     fold (mapOptionTree ξ) in *.
 312     set (mapOptionTree ξ) as X in *.
 313
 314     set (IHv2 ((stripOutVars (leaves v1) ctx),, v1) z) as IHv2'.
 315     unfold stripOutVars in IHv2'.
 316     simpl in IHv2'.
 317     fold (stripOutVars (leaves v2)) in IHv2'.
 318     fold (stripOutVars (leaves v1)) in IHv2'.
 319     unfold X in IHv2'.
 320     unfold mapOptionTree in IHv2'.
 321     simpl in IHv2'.
 322     fold (mapOptionTree ξ) in IHv2'.
 323     fold X in IHv2'.
 324     set (nd_comp (IHv1 _ _) IHv2') as qq.
 325     eapply nd_comp.
 326       apply qq.
 327       clear qq IHv2' IHv2 IHv1.
 328
 329       assert ((stripOutVars (leaves v2) (stripOutVars (leaves v1) ctx))=(stripOutVars (app (leaves v1) (leaves v2)) ctx)).
 330         admit.
 331         rewrite H.
 332         clear H.
 333
 334       (* FIXME: this only works because the variables are all distinct, but I need to prove that *)
 335       assert ((stripOutVars (leaves v2) v1) = v1).
 336         admit.
 337         rewrite H.
 338         clear H.
 339
 340         apply nd_rule.
 341         apply RCossa.
 342     Defined.
 343
 344 Definition update_ξ'' {Γ} ξ tree lev :=
 345 (update_ξ ξ
 346                   (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@  lev ⟩)
 347                      (leaves tree))).
 348
 349 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree lev :
 350       mapOptionTree (update_ξ ξ ((v,lev)::nil)) (stripOutVars (v :: nil) tree)
 351     = mapOptionTree ξ (stripOutVars (v :: nil) tree).
 352   induction tree; simpl in *; try reflexivity; auto.
 353
 354   unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *; fold (mapOptionTree (update_ξ ξ ((v,lev)::nil))) in *.
 355   destruct a; simpl; try reflexivity.
 356   unfold update_ξ.
 357   simpl.
 358   unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
 359   unfold update_ξ.
 360   unfold dropVar.
 361   simpl.
 362   set (eqd_dec v v0) as q.
 363   assert (q=eqd_dec v v0).
 364     reflexivity.
 365   destruct q.
 366   reflexivity.
 367   rewrite <- H.
 368   reflexivity.
 369   auto.
 370   unfold mapOptionTree.
 371   unfold mapOptionTree in IHtree1.
 372   unfold mapOptionTree in IHtree2.
 373   simpl in *.
 374   simpl in IHtree1.
 375   fold (stripOutVars (v::nil)).
 376   rewrite <- IHtree1.
 377   rewrite <- IHtree2.
 378   reflexivity.
 379   Qed.
 380
 381
 382
 383 Lemma updating_stripped_tree_is_inert'
 384   {Γ} lev
 385   (ξ:VV -> LeveledHaskType Γ ★)
 386   tree tree2 :
 387     mapOptionTree (update_ξ'' ξ tree lev) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2)
 388   = mapOptionTree ξ (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2).
 389 admit.
 390   Qed.
 391
 392 Lemma updating_stripped_tree_is_inert''
 393   {Γ}
 394   (ξ:VV -> LeveledHaskType Γ ★)
 395   v tree lev :
 396     mapOptionTree   (update_ξ'' ξ (unleaves v) lev) (stripOutVars (map (@fst _ _) v) tree)
 397   = mapOptionTree ξ (stripOutVars  (map (@fst _ _) v) tree).
 398 admit.
 399   Qed.
 400
 401 (*
 402 Lemma updating_stripped_tree_is_inert'''
 403   {Γ}
 404   (ξ:VV -> LeveledHaskType Γ)
 405 {T}
 406   (idx:Tree ??T) (types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx) tree
 407 :
 408     mapOptionTree   (update_ξ''' ξ types vars) (stripOutVars (leaves (unshape vars)) tree)
 409   = mapOptionTree ξ (stripOutVars (leaves (unshape vars)) tree).
 410 admit.
 411   Qed.
 412 *)
 413
 414 (* IDEA: use multi-conclusion proofs instead *)
 415 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
 416   | lrsp_nil  : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
 417   | lrsp_leaf : forall v  e,
 418     (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [unlev (ξ v) @@ lev]]) ->
 419     LetRecSubproofs Γ Δ ξ lev [(v, unlev (ξ v))] (ELR_leaf _ _ _ _ _ e)
 420   | lrsp_cons : forall t1 t2 b1 b2,
 421     LetRecSubproofs Γ Δ ξ lev t1 b1 ->
 422     LetRecSubproofs Γ Δ ξ lev t2 b2 ->
 423     LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
 424
 425 Lemma cheat1 : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree),
 426   eLetRecTypes branches =
 427     mapOptionTree  (update_ξ'' ξ tree lev)
 428     (mapOptionTree (@fst _ _) tree).
 429   intros.
 430   induction branches.
 431   reflexivity.
 432   simpl.
 433   unfold update_ξ.
 434   unfold mapOptionTree; simpl.
 435 admit.
 436 admit.
 437   Qed.
 438 Lemma cheat2 : forall Γ Δ ξ l tc tbranches atypes e alts',
 439 mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
 440 =
 441 (*
 442 ((mapOptionTreeAndFlatten
 443 (fun h => stripOutVars (vec2list (scbwv_exprvars (projT1 h)))
 444                   (expr2antecedent (projT2 h))) alts'),,(expr2antecedent e)).
 445 *)
 446 ((mapOptionTreeAndFlatten pcb_freevars
 447            (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ  (expr2antecedent e)).
 448 admit.
 449 Qed.
 450 Lemma cheat3 : forall {A}{B}{f:A->B} l, unleaves (map f l) = mapOptionTree f (unleaves l).
 451   admit.
 452   Qed.
 453 Lemma cheat4 : forall {A}(t:list A), leaves (unleaves t) = t.
 454 admit.
 455 Qed.
 456
 457 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches
 458     : LetRecSubproofs Γ Δ ξ lev tree branches ->
 459     ND Rule []
 460     [ Γ > Δ >
 461       mapOptionTree ξ (eLetRecContext branches)
 462       |-
 463   eLetRecTypes branches
 464     ].
 465   intro X.
 466   induction X; intros; simpl in *.
 467     apply nd_rule.
 468       apply REmptyGroup.
 469     set (ξ v) as q in *.
 470       destruct q.
 471       simpl in *.
 472       assert (h0=lev).
 473         admit.
 474         rewrite H.
 475       apply n.
 476     eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
 477     eapply nd_comp; [ apply nd_llecnac | idtac ].
 478     apply nd_prod; auto.
 479   Defined.
 480
 481
 482 Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ ★) tree z lev,
 483   mapOptionTree (@update_ξ'' Γ ξ tree lev) z = mapOptionTree (update_ξ'' (update_ξ'' ξ tree lev) tree lev) z.
 484 admit.
 485   Qed.
 486
 487
 488
 489 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
 490     forall branches body,
 491     ND Rule [] [Γ > Δ > mapOptionTree (update_ξ'' ξ tree lev) (expr2antecedent body) |- [τ @@ lev]] ->
 492     LetRecSubproofs Γ Δ (update_ξ'' ξ tree lev) lev tree branches ->
 493     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]].
 494
 495   (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
 496   simpl.
 497   intro branches.
 498   intro body.
 499   intro pf.
 500   intro lrsp.
 501   set ((update_ξ ξ
 502            (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@  lev ⟩)
 503               (leaves tree)))) as ξ' in *.
 504   set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
 505   set (mapOptionTree (@fst _ _) tree) as pctx.
 506   set (mapOptionTree ξ' pctx) as passback.
 507   set (fun a b => @RLetRec Γ Δ a b passback) as z.
 508   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
 509   clear z.
 510
 511   set (@arrangeContextAndWeaken''  Γ Δ ξ' pctx (expr2antecedent body,,eLetRecContext branches)) as q'.
 512   unfold passback in *; clear passback.
 513   unfold pctx in *; clear pctx.
 514   eapply UND_to_ND in q'.
 515
 516   unfold ξ' in *.
 517   set (@updating_stripped_tree_is_inert') as zz.
 518   unfold update_ξ'' in *.
 519   rewrite zz in q'.
 520   clear zz.
 521   clear ξ'.
 522   simpl in q'.
 523
 524   eapply nd_comp; [ idtac | apply q' ].
 525   clear q'.
 526   unfold mapOptionTree. simpl. fold (mapOptionTree (update_ξ'' ξ tree lev)).
 527
 528   simpl.
 529
 530   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
 531
 532     eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
 533     eapply nd_comp; [ apply nd_llecnac | idtac ].
 534     apply nd_prod; auto.
 535     rewrite cheat1 in q.
 536     set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz.
 537     unfold update_ξ'' in *.
 538     rewrite <- zz in q.
 539     apply q.
 540   Defined.
 541
 542
 543 Lemma updating_stripped_tree_is_inert''' : forall Γ tc ξ l t atypes x,
 544          mapOptionTree (scbwv_ξ(Γ:=Γ)(tc:=tc)(atypes:=atypes) x ξ l)
 545            (stripOutVars (vec2list (scbwv_exprvars x)) t)
 546              =
 547          mapOptionTree (weakLT' ○ ξ)
 548            (stripOutVars (vec2list (scbwv_exprvars x)) t).
 549   admit.
 550   Qed.
 551
 552
 553 Lemma updating_stripped_tree_is_inert'''' : forall Γ Δ ξ l tc atypes tbranches
 554 (x:StrongCaseBranchWithVVs(Γ:=Γ) VV eqd_vv tc atypes)
 555 (e0:Expr (sac_Γ x Γ) (sac_Δ x Γ atypes (weakCK'' Δ))
 556     (scbwv_ξ x ξ l) (weakT' tbranches @@  weakL' l)) ,
 557 mapOptionTree (weakLT' ○ ξ)
 558         (stripOutVars (vec2list (scbwv_exprvars x)) (expr2antecedent e0)),,
 559 unleaves (vec2list (sac_types x Γ atypes)) @@@ weakL' l
 560 =
 561 mapOptionTree (weakLT' ○ ξ)
 562         (stripOutVars (vec2list (scbwv_exprvars x)) (expr2antecedent e0)),,
 563          mapOptionTree
 564            (update_ξ (weakLT' ○ ξ)
 565               (vec2list
 566                  (vec_map
 567                     (fun
 568                        x0 : VV *
 569                             HaskType
 570                               (app (vec2list (sac_ekinds x)) Γ)
 571                               ★ => ⟨fst x0, snd x0 @@  weakL' l ⟩)
 572                     (vec_zip (scbwv_exprvars x)
 573                        (sac_types x Γ atypes)))))
 574            (unleaves (vec2list (scbwv_exprvars x)))
 575 .
 576 admit.
 577 Qed.
 578
 579
 580
 581
 582 Definition expr2proof  :
 583   forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
 584     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
 585
 586   refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
 587     : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
 588     match exp as E in Expr Γ Δ ξ τ with
 589     | EGlobal  Γ Δ ξ t wev                          => let case_EGlobal := tt in _
 590     | EVar     Γ Δ ξ ev                             => let case_EVar := tt in _
 591     | ELit     Γ Δ ξ lit lev                        => let case_ELit := tt in _
 592     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => let case_EApp := tt in
 593                                                         (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
 594     | ELam     Γ Δ ξ t1 t2 lev v    e               => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 595     | ELet     Γ Δ ξ tv t      v lev ev ebody       => let case_ELet := tt in
 596                                                        (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
 597     | ELetRec  Γ Δ ξ lev t tree branches ebody      =>
 598       let ξ' := update_ξ'' ξ tree lev in
 599       let case_ELetRec := tt in  (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
 600 ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
 601         (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
 602         : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
 603         match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
 604           | ELR_nil    Γ Δ ξ lev  => lrsp_nil _ _ _ _
 605           | ELR_leaf   Γ Δ ξ l v e => lrsp_leaf Γ Δ ξ l v e (expr2proof _ _ _ _ e)
 606           | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
 607         end
 608         ) _ _ _ _ tree branches)
 609     | EEsc     Γ Δ ξ ec t lev e                     => let case_EEsc    := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 610     | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 611     | ECast    Γ Δ ξ γ t1 t2 lev      e             => let case_ECast   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 612     | ENote    Γ Δ ξ t n e                          => let case_ENote   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 613     | ETyLam   Γ Δ ξ κ σ l e                        => let case_ETyLam  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 614     | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 615     | ECoApp   Γ Δ κ σ₁ σ₂ σ γ ξ l      e           => let case_ECoApp  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 616     | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 617     | ECase    Γ Δ ξ l tc tbranches atypes e alts' =>
 618       let dcsp :=
 619         ((fix mkdcsp (alts:
 620                Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
 621                             & Expr (sac_Γ scb Γ)
 622                                    (sac_Δ scb Γ atypes (weakCK'' Δ))
 623                                    (scbwv_ξ scb ξ l)
 624                                    (weakLT' (tbranches@@l)) })
 625           : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) :=
 626         match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with
 627           | T_Leaf None       => let case_nil := tt in _
 628           | T_Leaf (Some x)   => (fun ecb' => let case_leaf := tt in _) (expr2proof _ _ _ _ (projT2 x))
 629           | T_Branch b1 b2   => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
 630         end) alts')
 631         in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 632     end
 633 ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
 634
 635     destruct case_EGlobal.
 636       apply nd_rule.
 637       simpl.
 638       destruct t as [t lev].
 639       apply (RGlobal _ _ _ _ wev).
 640
 641     destruct case_EVar.
 642       apply nd_rule.
 643       unfold mapOptionTree; simpl.
 644       destruct (ξ ev).
 645       apply RVar.
 646
 647     destruct case_ELit.
 648       apply nd_rule.
 649       apply RLit.
 650
 651     destruct case_EApp.
 652       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
 653       eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
 654       eapply nd_comp; [ apply nd_llecnac | idtac ].
 655       apply nd_prod; auto.
 656       apply e1'.
 657       apply e2'.
 658
 659     destruct case_ELam; intros.
 660       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
 661       eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
 662       set (update_ξ ξ ((v,t1@@lev)::nil)) as ξ'.
 663       set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx.
 664         apply UND_to_ND in pfx.
 665         unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx.
 666         unfold ξ' in pfx.
 667         fold (mapOptionTree (update_ξ ξ ((v,(t1@@lev))::nil))) in pfx.
 668         rewrite updating_stripped_tree_is_inert in pfx.
 669         unfold update_ξ in pfx.
 670         destruct (eqd_dec v v).
 671         eapply nd_comp; [ idtac | apply pfx ].
 672         clear pfx.
 673         apply e'.
 674         assert False.
 675         apply n.
 676         auto.
 677         inversion H.
 678
 679     destruct case_ELet; intros; simpl in *.
 680       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 681       eapply nd_comp; [ apply nd_llecnac | idtac ].
 682       apply nd_prod; [ idtac | apply pf_let].
 683       clear pf_let.
 684       eapply nd_comp; [ apply pf_body | idtac ].
 685       clear pf_body.
 686       fold (@mapOptionTree VV).
 687       fold (mapOptionTree ξ).
 688       set (update_ξ ξ ((lev,(tv @@ v))::nil)) as ξ'.
 689       set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
 690       unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
 691       unfold ξ' in n.
 692       rewrite updating_stripped_tree_is_inert in n.
 693       unfold update_ξ in n.
 694       destruct (eqd_dec lev lev).
 695       unfold ξ'.
 696       unfold update_ξ.
 697       apply UND_to_ND in n.
 698       apply n.
 699       assert False. apply n0; auto. inversion H.
 700
 701     destruct case_EEsc.
 702       eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
 703       apply e'.
 704
 705     destruct case_EBrak; intros.
 706       eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
 707       apply e'.
 708
 709     destruct case_ECast.
 710       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
 711       apply e'.
 712       auto.
 713
 714     destruct case_ENote.
 715       destruct t.
 716       eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
 717       apply e'.
 718       auto.
 719
 720     destruct case_ETyApp; simpl in *; intros.
 721       eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
 722       apply e'.
 723       auto.
 724
 725     destruct case_ECoLam; simpl in *; intros.
 726       eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
 727       apply e'.
 728
 729     destruct case_ECoApp; simpl in *; intros.
 730       eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
 731       apply e'.
 732       auto.
 733
 734     destruct case_ETyLam; intros.
 735       eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
 736       unfold mapOptionTree in e'.
 737       rewrite mapOptionTree_compose in e'.
 738       unfold mapOptionTree.
 739       apply e'.
 740
 741     destruct case_leaf.
 742       unfold pcb_judg.
 743       simpl.
 744       repeat rewrite <- mapOptionTree_compose in *.
 745       set (nd_comp ecb' (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _
 746         (unleaves (vec2list (scbwv_exprvars (projT1 x))))
 747       (*(unleaves (vec2list (sac_types (projT1 x) Γ atypes)))*)
 748         _ _
 749       ))) as q.
 750       rewrite cheat4 in q.
 751       rewrite cheat3.
 752       unfold weakCK'' in q.
 753       simpl in q.
 754       rewrite (updating_stripped_tree_is_inert''' Γ tc ξ l _ atypes  (projT1 x)) in q.
 755       Ltac cheater Q :=
 756        match goal with
 757         [ Q:?Y |- ?Z ] =>
 758          assert (Y=Z) end.
 759       cheater q.
 760       admit.
 761       rewrite <- H.
 762       clear H.
 763       apply q.
 764
 765     destruct case_nil.
 766       apply nd_id0.
 767
 768     destruct case_branch.
 769       simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
 770       apply nd_prod.
 771       apply b1'.
 772       apply b2'.
 773
 774     destruct case_ECase.
 775       rewrite cheat2.
 776       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
 777       eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
 778       rewrite <- mapOptionTree_compose.
 779       apply dcsp.
 780       apply e'.
 781
 782     destruct case_ELetRec; simpl in *; intros.
 783       set (@letRecSubproofsToND') as q.
 784       simpl in q.
 785       apply q.
 786       clear q.
 787       apply e'.
 788       apply subproofs.
 789
 790   Defined.
 791
 792 End HaskStrongToProof.
 793