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