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 HaskWeakVars.
  16 Require Import HaskProof.
  17
  18 Section HaskStrongToProof.
  19
  20 (* Whereas RLeft/RRight perform left and right context expansion on a single uniform rule, these functions perform
  21  * expansion on an entire uniform proof *)
  22 Definition ext_left  {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★))
  23   := @nd_map' _ _ _ _ (ext_tree_left ctx)  (fun h c r => nd_rule (@RLeft Γ Δ h c ctx r)).
  24 Definition ext_right {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★))
  25   := @nd_map' _ _ _ _ (ext_tree_right ctx) (fun h c r => nd_rule (@RRight Γ Δ h c ctx r)).
  26
  27 Definition pivotContext {Γ}{Δ} a b c τ :
  28   @ND _ (@URule Γ Δ)
  29     [ Γ >> Δ > (a,,b),,c |- τ]
  30     [ Γ >> Δ > (a,,c),,b |- τ].
  31   set (ext_left a _ _ (nd_rule (@RExch Γ Δ τ c b))) as q.
  32   simpl in *.
  33   eapply nd_comp ; [ eapply nd_rule; apply RCossa | idtac ].
  34   eapply nd_comp ; [ idtac | eapply nd_rule; apply RAssoc ].
  35   apply q.
  36   Defined.
  37
  38 Definition copyAndPivotContext {Γ}{Δ} a b c τ :
  39   @ND _ (@URule Γ Δ)
  40     [ Γ >> Δ > (a,,b),,(c,,b) |- τ]
  41     [ Γ >> Δ > (a,,c),,b |- τ].
  42     set (ext_left (a,,c) _ _ (nd_rule (@RCont Γ Δ τ b))) as q.
  43     simpl in *.
  44     eapply nd_comp; [ idtac | apply q ].
  45     clear q.
  46     eapply nd_comp ; [ idtac | eapply nd_rule; apply RCossa ].
  47     set (ext_right b _ _ (@pivotContext _ Δ a b c τ)) as q.
  48     simpl in *.
  49     eapply nd_comp ; [ idtac | apply q ].
  50     clear q.
  51     apply nd_rule.
  52     apply RAssoc.
  53     Defined.
  54
  55
  56
  57 Context {VV:Type}{eqd_vv:EqDecidable VV}.
  58
  59   (* maintenance of Xi *)
  60   Definition dropVar (lv:list VV)(v:VV) : ??VV :=
  61     if fold_left
  62       (fun a b:bool => if a then true else if b then true else false)
  63       (map (fun lvv => if eqd_dec lvv v then true else false) lv)
  64       false
  65       then None
  66       else Some v.
  67   (* later: use mapOptionTreeAndFlatten *)
  68   Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=
  69     mapTree (fun x => match x with None => None | Some vt => dropVar lv vt end).
  70
  71 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
  72   match exp as E in Expr Γ Δ ξ τ with
  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     | EVar     Γ Δ ξ ev                             => let case_EVar := tt in _
 590     | ELit     Γ Δ ξ lit lev                        => let case_ELit := tt in _
 591     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => let case_EApp := tt in
 592                                                         (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
 593     | ELam     Γ Δ ξ t1 t2 lev v    e               => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 594     | ELet     Γ Δ ξ tv t      v lev ev ebody       => let case_ELet := tt in
 595                                                        (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
 596     | ELetRec  Γ Δ ξ lev t tree branches ebody      =>
 597       let ξ' := update_ξ'' ξ tree lev in
 598       let case_ELetRec := tt in  (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
 599 ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
 600         (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
 601         : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
 602         match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
 603           | ELR_nil    Γ Δ ξ lev  => lrsp_nil _ _ _ _
 604           | ELR_leaf   Γ Δ ξ l v e => lrsp_leaf Γ Δ ξ l v e (expr2proof _ _ _ _ e)
 605           | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
 606         end
 607         ) _ _ _ _ tree branches)
 608     | EEsc     Γ Δ ξ ec t lev e                     => let case_EEsc    := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 609     | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 610     | ECast    Γ Δ ξ γ t1 t2 lev      e             => let case_ECast   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 611     | ENote    Γ Δ ξ t n e                          => let case_ENote   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 612     | ETyLam   Γ Δ ξ κ σ l e                        => let case_ETyLam  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 613     | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 614     | ECoApp   Γ Δ κ σ₁ σ₂ σ γ ξ l      e           => let case_ECoApp  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 615     | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 616     | ECase    Γ Δ ξ l tc tbranches atypes e alts' =>
 617       let dcsp :=
 618         ((fix mkdcsp (alts:
 619                Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
 620                             & Expr (sac_Γ scb Γ)
 621                                    (sac_Δ scb Γ atypes (weakCK'' Δ))
 622                                    (scbwv_ξ scb ξ l)
 623                                    (weakLT' (tbranches@@l)) })
 624           : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) :=
 625         match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with
 626           | T_Leaf None       => let case_nil := tt in _
 627           | T_Leaf (Some x)   => (fun ecb' => let case_leaf := tt in _) (expr2proof _ _ _ _ (projT2 x))
 628           | T_Branch b1 b2   => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
 629         end) alts')
 630         in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 631     end
 632 ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
 633
 634     destruct case_EVar.
 635       apply nd_rule.
 636       unfold mapOptionTree; simpl.
 637       destruct (ξ ev).
 638       apply RVar.
 639
 640     destruct case_ELit.
 641       apply nd_rule.
 642       apply RLit.
 643
 644     destruct case_EApp.
 645       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
 646       eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
 647       eapply nd_comp; [ apply nd_llecnac | idtac ].
 648       apply nd_prod; auto.
 649       apply e1'.
 650       apply e2'.
 651
 652     destruct case_ELam; intros.
 653       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
 654       eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
 655       set (update_ξ ξ ((v,t1@@lev)::nil)) as ξ'.
 656       set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx.
 657         apply UND_to_ND in pfx.
 658         unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx.
 659         unfold ξ' in pfx.
 660         fold (mapOptionTree (update_ξ ξ ((v,(t1@@lev))::nil))) in pfx.
 661         rewrite updating_stripped_tree_is_inert in pfx.
 662         unfold update_ξ in pfx.
 663         destruct (eqd_dec v v).
 664         eapply nd_comp; [ idtac | apply pfx ].
 665         clear pfx.
 666         apply e'.
 667         assert False.
 668         apply n.
 669         auto.
 670         inversion H.
 671
 672     destruct case_ELet; intros; simpl in *.
 673       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 674       eapply nd_comp; [ apply nd_llecnac | idtac ].
 675       apply nd_prod; [ idtac | apply pf_let].
 676       clear pf_let.
 677       eapply nd_comp; [ apply pf_body | idtac ].
 678       clear pf_body.
 679       fold (@mapOptionTree VV).
 680       fold (mapOptionTree ξ).
 681       set (update_ξ ξ ((lev,(tv @@ v))::nil)) as ξ'.
 682       set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
 683       unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
 684       unfold ξ' in n.
 685       rewrite updating_stripped_tree_is_inert in n.
 686       unfold update_ξ in n.
 687       destruct (eqd_dec lev lev).
 688       unfold ξ'.
 689       unfold update_ξ.
 690       apply UND_to_ND in n.
 691       apply n.
 692       assert False. apply n0; auto. inversion H.
 693
 694     destruct case_EEsc.
 695       eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
 696       apply e'.
 697
 698     destruct case_EBrak; intros.
 699       eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
 700       apply e'.
 701
 702     destruct case_ECast.
 703       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
 704       apply e'.
 705       auto.
 706
 707     destruct case_ENote.
 708       eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
 709       apply e'.
 710       auto.
 711
 712     destruct case_ETyApp; simpl in *; intros.
 713       eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
 714       apply e'.
 715       auto.
 716
 717     destruct case_ECoLam; simpl in *; intros.
 718       eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
 719       apply e'.
 720
 721     destruct case_ECoApp; simpl in *; intros.
 722       eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
 723       apply e'.
 724       auto.
 725
 726     destruct case_ETyLam; intros.
 727       eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
 728       unfold mapOptionTree in e'.
 729       rewrite mapOptionTree_compose in e'.
 730       unfold mapOptionTree.
 731       apply e'.
 732
 733     destruct case_leaf.
 734       unfold pcb_judg.
 735       simpl.
 736       repeat rewrite <- mapOptionTree_compose in *.
 737       set (nd_comp ecb' (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _
 738         (unleaves (vec2list (scbwv_exprvars (projT1 x))))
 739       (*(unleaves (vec2list (sac_types (projT1 x) Γ atypes)))*)
 740         _ _
 741       ))) as q.
 742       rewrite cheat4 in q.
 743       rewrite cheat3.
 744       unfold weakCK'' in q.
 745       simpl in q.
 746       rewrite (updating_stripped_tree_is_inert''' Γ tc ξ l _ atypes  (projT1 x)) in q.
 747       Ltac cheater Q :=
 748        match goal with
 749         [ Q:?Y |- ?Z ] =>
 750          assert (Y=Z) end.
 751       cheater q.
 752       admit.
 753       rewrite <- H.
 754       clear H.
 755       apply q.
 756
 757     destruct case_nil.
 758       apply nd_id0.
 759
 760     destruct case_branch.
 761       simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
 762       apply nd_prod.
 763       apply b1'.
 764       apply b2'.
 765
 766     destruct case_ECase.
 767       rewrite cheat2.
 768       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
 769       eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
 770       rewrite <- mapOptionTree_compose.
 771       apply dcsp.
 772       apply e'.
 773
 774     destruct case_ELetRec; simpl in *; intros.
 775       set (@letRecSubproofsToND') as q.
 776       simpl in q.
 777       apply q.
 778       clear q.
 779       apply e'.
 780       apply subproofs.
 781
 782   Defined.
 783
 784 End HaskStrongToProof.
 785
 786 (*
 787
 788 (* Figure 7, production "decl"; actually not used in this formalization *)
 789 Inductive Decl :=.
 790 | DeclDataType     : forall tc:TyCon,      (forall dc:DataCon tc, DataConDecl dc)      -> Decl
 791 | DeclTypeFunction : forall n t l,         TypeFunctionDecl n t l                      -> Decl
 792 | DeclAxiom        : forall n ccon vk TV,  @AxiomDecl        n ccon vk  TV             -> Decl.
 793
 794 (* Figure 1, production "pgm" *)
 795 Inductive Pgm Γ Δ :=
 796   mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ.
 797 *)
 798