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    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      e             => expr2antecedent e
  83   | ENote    Γ Δ ξ t n e                          => expr2antecedent e
  84   | ETyLam   Γ Δ ξ κ σ l e                        => expr2antecedent e
  85   | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => expr2antecedent e
  86   | ECoApp   Γ Δ κ γ σ₁ σ₂ σ ξ l      e           => expr2antecedent e
  87   | ETyApp   Γ Δ κ σ τ ξ  l    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    Γ Δ ξ l tc tbranches sac atypes e' alts =>
  93     ((fix varsfromalts (alts:
  94                Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc sac atypes
  95                             & Expr (sac_Γ scb Γ)
  96                                    (sac_Δ scb Γ atypes (weakCK'' Δ))
  97                                    (scbwv_ξ scb ξ l)
  98                                    (weakLT' (tbranches@@l)) }
  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    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      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             e      => let case_ECoLam  := tt in let e' := expr2proof _ _ _ _ e in _
 576     | ECoApp   Γ Δ κ σ₁ σ₂ σ γ ξ l      e           => let case_ECoApp  := tt in let e' := expr2proof _ _ _ _ e in _
 577     | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in let e' := expr2proof _ _ _ _ e in _
 578     | ECase    Γ Δ ξ l tc tbranches sac atypes 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
 633     destruct case_ELet; intros.
 634       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 635       eapply nd_comp; [ apply nd_llecnac | idtac ].
 636       apply nd_prod; [ idtac | apply pf_let].
 637       clear pf_let.
 638       eapply nd_comp; [ apply pf_body | idtac ].
 639       clear pf_body.
 640       fold (@mapOptionTree VV).
 641       fold (mapOptionTree ξ).
 642       set (update_ξ ξ ((lev,(tv @@ v))::nil)) as ξ'.
 643       set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
 644       unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
 645       unfold ξ' in n.
 646       rewrite updating_stripped_tree_is_inert in n.
 647       unfold update_ξ in n.
 648       destruct (eqd_dec lev lev).
 649       unfold ξ'.
 650       unfold update_ξ.
 651       apply UND_to_ND in n.
 652       apply n.
 653       assert False. apply n0; auto. inversion H.
 654
 655     destruct case_EEsc.
 656       eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
 657       apply e'.
 658
 659     destruct case_EBrak; intros.
 660       eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
 661       apply e'.
 662
 663     destruct case_ECast.
 664       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
 665       apply e'.
 666       auto.
 667
 668     destruct case_ENote.
 669       eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
 670       apply e'.
 671       auto.
 672
 673     destruct case_ETyApp; intros.
 674       eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
 675       apply e'.
 676       auto.
 677
 678     destruct case_ECoLam; intros.
 679       eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
 680       apply e'.
 681
 682     destruct case_ECoApp; intros.
 683       eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
 684       apply e'.
 685       auto.
 686
 687     destruct case_ETyLam; intros.
 688       eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
 689       unfold mapOptionTree in e'.
 690       rewrite mapOptionTree_compose in e'.
 691       unfold mapOptionTree.
 692       apply e'.
 693
 694     destruct case_ECase.
 695       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
 696       apply (fail "ECase not implemented").
 697       (*
 698       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
 699       eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
 700       rewrite <- mapOptionTree_compose.
 701       apply dcsp.
 702       apply e'.
 703       *)
 704
 705     destruct case_elr_leaf; intros.
 706       assert (unlev (ξ0 v) = t0).
 707         apply cheat.
 708         set (@lrsp_leaf Γ0 Δ0 ξ0 l v) as q.
 709         rewrite H in q.
 710         apply q.
 711       apply e'0.
 712
 713     destruct case_ELetRec; intros.
 714       set (@letRecSubproofsToND') as q.
 715       simpl in q.
 716       apply q.
 717       clear q.
 718       apply e'.
 719       apply subproofs.
 720
 721       (*
 722     destruct case_leaf.
 723       unfold pcb_judg.
 724       simpl.
 725       clear mkdcsp alts0 o ecb Γ Δ ξ lev  tc avars e alts u.
 726       repeat rewrite <- mapOptionTree_compose in *.
 727       set (nd_comp ecb'
 728       (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _ (unshape corevars) _ _))) as q.
 729       idtac.
 730       assert (unshape (scb_types alt) = (mapOptionTree (update_ξ''' (weakenX' ξ0) (scb_types alt) corevars) (unshape corevars))).
 731       apply update_ξ_and_reapply.
 732       rewrite H.
 733       simpl in q.
 734       unfold mapOptionTree in q; simpl in q.
 735       set (@updating_stripped_tree_is_inert''') as u.
 736       unfold mapOptionTree in u.
 737       rewrite u in q.
 738       clear u H.
 739       unfold weakenX' in *.
 740       admit.
 741       unfold mapOptionTree in *.
 742       replace
 743         (@weakenT' _ (sac_ekinds alt) (coreTypeToType φ tbranches0))
 744         with
 745         (coreTypeToType (updatePhi φ (sac_evars alt)) tbranches0).
 746       apply q.
 747       apply cheat.
 748
 749     destruct case_branch.
 750       simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
 751       apply nd_prod.
 752       apply (mkdcsp b1).
 753       apply (mkdcsp b2).
 754     *)
 755
 756   Defined.
 757
 758 End HaskStrongToProof.
 759
 760 (*
 761
 762 (* Figure 7, production "decl"; actually not used in this formalization *)
 763 Inductive Decl :=.
 764 | DeclDataType     : forall tc:TyCon,      (forall dc:DataCon tc, DataConDecl dc)      -> Decl
 765 | DeclTypeFunction : forall n t l,         TypeFunctionDecl n t l                      -> Decl
 766 | DeclAxiom        : forall n ccon vk TV,  @AxiomDecl        n ccon vk  TV             -> Decl.
 767
 768 (* Figure 1, production "pgm" *)
 769 Inductive Pgm Γ Δ :=
 770   mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ.
 771 *)