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