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 cheat9 : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree),
 426
 427   eLetRecTypes branches =
 428     mapOptionTree  (update_ξ'' ξ tree lev)
 429     (mapOptionTree (@fst _ _) tree).
 430   intros.
 431   induction branches.
 432   reflexivity.
 433   simpl.
 434   unfold update_ξ.
 435   unfold mapOptionTree; simpl.
 436 admit.
 437 admit.
 438   Qed.
 439
 440 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches
 441     : LetRecSubproofs Γ Δ ξ lev tree branches ->
 442     ND Rule []
 443     [ Γ > Δ >
 444       mapOptionTree ξ (eLetRecContext branches)
 445       |-
 446   eLetRecTypes branches
 447     ].
 448   intro X.
 449   induction X; intros; simpl in *.
 450     apply nd_rule.
 451       apply REmptyGroup.
 452     unfold mapOptionTree.
 453       simpl.
 454 admit.
 455 (*      apply n.*)
 456     eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
 457     eapply nd_comp; [ apply nd_llecnac | idtac ].
 458     apply nd_prod; auto.
 459   Defined.
 460
 461
 462 Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ ★) tree z lev,
 463   mapOptionTree (@update_ξ'' Γ ξ tree lev) z = mapOptionTree (update_ξ'' (update_ξ'' ξ tree lev) tree lev) z.
 464 admit.
 465   Qed.
 466
 467
 468
 469 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
 470     forall branches body,
 471     ND Rule [] [Γ > Δ > mapOptionTree (update_ξ'' ξ tree lev) (expr2antecedent body) |- [τ @@ lev]] ->
 472     LetRecSubproofs Γ Δ (update_ξ'' ξ tree lev) lev tree branches ->
 473     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]].
 474
 475   (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
 476   simpl.
 477   intro branches.
 478   intro body.
 479   intro pf.
 480   intro lrsp.
 481   set ((update_ξ ξ
 482            (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@  lev ⟩)
 483               (leaves tree)))) as ξ' in *.
 484   set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
 485   set (mapOptionTree (@fst _ _) tree) as pctx.
 486   set (mapOptionTree ξ' pctx) as passback.
 487   set (fun a b => @RLetRec Γ Δ a b passback) as z.
 488   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
 489   clear z.
 490
 491   set (@arrangeContextAndWeaken''  Γ Δ ξ' pctx (expr2antecedent body,,eLetRecContext branches)) as q'.
 492   unfold passback in *; clear passback.
 493   unfold pctx in *; clear pctx.
 494   eapply UND_to_ND in q'.
 495
 496   unfold ξ' in *.
 497   set (@updating_stripped_tree_is_inert') as zz.
 498   unfold update_ξ'' in *.
 499   rewrite zz in q'.
 500   clear zz.
 501   clear ξ'.
 502   simpl in q'.
 503
 504   eapply nd_comp; [ idtac | apply q' ].
 505   clear q'.
 506   unfold mapOptionTree. simpl. fold (mapOptionTree (update_ξ'' ξ tree lev)).
 507
 508   simpl.
 509
 510   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
 511
 512     eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
 513     eapply nd_comp; [ apply nd_llecnac | idtac ].
 514     apply nd_prod; auto.
 515     rewrite cheat9 in q.
 516     set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz.
 517     unfold update_ξ'' in *.
 518     rewrite <- zz in q.
 519     apply q.
 520   Defined.
 521
 522 (*
 523 Lemma update_ξ_and_reapply : forall Γ ξ {T}(idx:Tree ??T)(types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx),
 524   unshape types = mapOptionTree (update_ξ''' ξ types vars) (unshape vars).
 525 admit.
 526   Qed.
 527 *)
 528
 529 Lemma cheat0 : forall Γ Δ ξ l tc tbranches atypes e alts',
 530 mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
 531 =
 532 (*
 533 ((mapOptionTreeAndFlatten
 534 (fun h => stripOutVars (vec2list (scbwv_exprvars (projT1 h)))
 535                   (expr2antecedent (projT2 h))) alts'),,(expr2antecedent e)).
 536 *)
 537 ((mapOptionTreeAndFlatten pcb_freevars
 538            (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ  (expr2antecedent e)).
 539 admit.
 540 Defined.
 541
 542 Lemma cheat1 : forall {A}{B}{f:A->B} l, unleaves (map f l) = mapOptionTree f (unleaves l).
 543   admit.
 544   Defined.
 545 Lemma cheat2 : forall {A}(t:list A), leaves (unleaves t) = t.
 546 admit.
 547 Defined.
 548
 549 Definition expr2proof  :
 550   forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
 551     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
 552
 553   refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
 554     : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
 555     match exp as E in Expr Γ Δ ξ τ with
 556     | EVar     Γ Δ ξ ev                             => let case_EVar := tt in _
 557     | ELit     Γ Δ ξ lit lev                        => let case_ELit := tt in _
 558     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => let case_EApp := tt in
 559       let e1' := expr2proof _ _ _ _ e1 in
 560       let e2' := expr2proof _ _ _ _ e2 in _
 561     | ELam     Γ Δ ξ t1 t2 lev v    e               => let case_ELam := tt in
 562       let e' := expr2proof _ _ _ _ e in _
 563     | ELet     Γ Δ ξ tv t      v lev ev ebody       => let case_ELet := tt in
 564       let pf_let := (expr2proof _ _ _ _ ev) in
 565       let pf_body := (expr2proof _ _ _ _ ebody) in _
 566     | ELetRec  Γ Δ ξ lev t tree branches ebody      =>
 567       let e' := expr2proof _ _ _ _ ebody in
 568       let ξ' := update_ξ'' ξ tree lev in
 569       let subproofs := ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
 570         (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
 571         : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
 572         match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
 573   | ELR_nil    Γ Δ ξ lev  => lrsp_nil _ _ _ _
 574   | ELR_leaf   Γ Δ ξ l v e => lrsp_leaf Γ Δ ξ l v e (expr2proof _ _ _ _ e)
 575   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
 576         end
 577         ) _ _ _ _ tree branches) in
 578       let case_ELetRec := tt in  _
 579     | EEsc     Γ Δ ξ ec t lev e                     => let case_EEsc    := tt in let e' := expr2proof _ _ _ _ e in _
 580     | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in let e' := expr2proof _ _ _ _ e in _
 581     | ECast    Γ Δ ξ γ t1 t2 lev      e             => let case_ECast   := tt in let e' := expr2proof _ _ _ _ e in _
 582     | ENote    Γ Δ ξ t n e                          => let case_ENote   := tt in let e' := expr2proof _ _ _ _ e in _
 583     | ETyLam   Γ Δ ξ κ σ l e                        => let case_ETyLam  := tt in let e' := expr2proof _ _ _ _ e in _
 584     | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in let e' := expr2proof _ _ _ _ e in _
 585     | ECoApp   Γ Δ κ σ₁ σ₂ σ γ ξ l      e           => let case_ECoApp  := tt in let e' := expr2proof _ _ _ _ e in _
 586     | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in let e' := expr2proof _ _ _ _ e in _
 587     | ECase    Γ Δ ξ l tc tbranches atypes e alts' =>
 588       let dcsp :=
 589         ((fix mkdcsp (alts:
 590                Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
 591                             & Expr (sac_Γ scb Γ)
 592                                    (sac_Δ scb Γ atypes (weakCK'' Δ))
 593                                    (scbwv_ξ scb ξ l)
 594                                    (weakLT' (tbranches@@l)) })
 595           : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) :=
 596         match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with
 597           | T_Leaf None       => let case_nil := tt in _
 598           | T_Leaf (Some x)   => (fun ecb' => let case_leaf := tt in _) (expr2proof _ _ _ _ (projT2 x))
 599           | T_Branch b1 b2   => let case_branch := tt in _
 600         end) alts')
 601         in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
 602     end
 603 ); clear exp ξ' τ' Γ' Δ'.
 604
 605     destruct case_EVar.
 606       apply nd_rule.
 607       unfold mapOptionTree; simpl.
 608       destruct (ξ ev).
 609       apply RVar.
 610
 611     destruct case_ELit.
 612       apply nd_rule.
 613       apply RLit.
 614
 615     destruct case_EApp.
 616       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
 617       eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
 618       eapply nd_comp; [ apply nd_llecnac | idtac ].
 619       apply nd_prod; auto.
 620
 621     destruct case_ELam; intros.
 622       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
 623       eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
 624       set (update_ξ ξ ((v,t1@@lev)::nil)) as ξ'.
 625       set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx.
 626         apply UND_to_ND in pfx.
 627         unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx.
 628         unfold ξ' in pfx.
 629         fold (mapOptionTree (update_ξ ξ ((v,(t1@@lev))::nil))) in pfx.
 630         rewrite updating_stripped_tree_is_inert in pfx.
 631         unfold update_ξ in pfx.
 632         destruct (eqd_dec v v).
 633         eapply nd_comp; [ idtac | apply pfx ].
 634         clear pfx.
 635         apply e'.
 636         assert False.
 637         apply n.
 638         auto.
 639         inversion H.
 640
 641     destruct case_ELet; intros; simpl in *.
 642       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 643       eapply nd_comp; [ apply nd_llecnac | idtac ].
 644       apply nd_prod; [ idtac | apply pf_let].
 645       clear pf_let.
 646       eapply nd_comp; [ apply pf_body | idtac ].
 647       clear pf_body.
 648       fold (@mapOptionTree VV).
 649       fold (mapOptionTree ξ).
 650       set (update_ξ ξ ((lev,(tv @@ v))::nil)) as ξ'.
 651       set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
 652       unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
 653       unfold ξ' in n.
 654       rewrite updating_stripped_tree_is_inert in n.
 655       unfold update_ξ in n.
 656       destruct (eqd_dec lev lev).
 657       unfold ξ'.
 658       unfold update_ξ.
 659       apply UND_to_ND in n.
 660       apply n.
 661       assert False. apply n0; auto. inversion H.
 662
 663     destruct case_EEsc.
 664       eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
 665       apply e'.
 666
 667     destruct case_EBrak; intros.
 668       eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
 669       apply e'.
 670
 671     destruct case_ECast.
 672       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
 673       apply e'.
 674       auto.
 675
 676     destruct case_ENote.
 677       eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
 678       apply e'.
 679       auto.
 680
 681     destruct case_ETyApp; simpl in *; intros.
 682       eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
 683       apply e'.
 684       auto.
 685
 686     destruct case_ECoApp; simpl in *; intros.
 687       eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
 688       apply e'.
 689       auto.
 690
 691     destruct case_leaf.
 692       unfold pcb_judg.
 693       simpl.
 694       repeat rewrite <- mapOptionTree_compose in *.
 695       set (nd_comp ecb' (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _
 696         (unleaves (vec2list (scbwv_exprvars (projT1 x))))
 697       (*(unleaves (vec2list (sac_types (projT1 x) Γ atypes)))*)
 698         _ _
 699       ))) as q.
 700
 701 rewrite cheat2 in q.
 702 rewrite cheat1.
 703 unfold weakCK'' in q.
 704 simpl in q.
 705 admit.
 706 (*
 707 replace (mapOptionTree ((@weakLT' Γ (tyConKind tc) _) ○ ξ)
 708         (stripOutVars (vec2list (scbwv_exprvars (projT1 x)))
 709            (expr2antecedent (projT2 x))))
 710 with (mapOptionTree (scbwv_ξ (projT1 x) ξ l)
 711               (stripOutVars (vec2list (scbwv_exprvars (projT1 x)))
 712                  (expr2antecedent (projT2 x)))).
 713 rewrite <- cheat1 in q.
 714 rewrite vec2list_map_list2vec in q.
 715 unfold mapOptionTree.
 716 fold (@mapOptionTree (HaskType (app (tyConKind tc) Γ) ★)
 717  (LeveledHaskType (app (tyConKind tc) Γ) ★) (fun t' => t' @@ weakL' l)).
 718 admit.
 719 *)
 720 admit.
 721
 722 (*
 723 assert (
 724
 725 unleaves (vec2list (vec_map (scbwv_ξ (projT1 x) ξ l) (scbwv_exprvars (projT1 x))))
 726 =
 727 unleaves (vec2list (sac_types (projT1 x) Γ atypes)) @@@ weakL'(κ:=tyConKind tc) l).
 728 admit.
 729 Set Printing Implicit.
 730 idtac.
 731 rewrite <- H.
 732
 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
 753     destruct case_branch.
 754       simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
 755       apply nd_prod.
 756       apply (mkdcsp b1).
 757       apply (mkdcsp b2).
 758
 759     destruct case_ECase.
 760       rewrite cheat0.
 761       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
 762       eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
 763       rewrite <- mapOptionTree_compose.
 764       apply dcsp.
 765       apply e'.
 766
 767     destruct case_ELetRec; simpl in *; intros.
 768       set (@letRecSubproofsToND') as q.
 769       simpl in q.
 770       apply q.
 771       clear q.
 772       apply e'.
 773       apply subproofs.
 774
 775     (*
 776     destruct case_ECoLam; simpl in *; intros.
 777       eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
 778       apply e'.
 779
 780     destruct case_ETyLam; intros.
 781       eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
 782       unfold mapOptionTree in e'.
 783       rewrite mapOptionTree_compose in e'.
 784       unfold mapOptionTree.
 785       apply e'.
 786      *)
 787   Admitted.
 788
 789 End HaskStrongToProof.
 790
 791 (*
 792
 793 (* Figure 7, production "decl"; actually not used in this formalization *)
 794 Inductive Decl :=.
 795 | DeclDataType     : forall tc:TyCon,      (forall dc:DataCon tc, DataConDecl dc)      -> Decl
 796 | DeclTypeFunction : forall n t l,         TypeFunctionDecl n t l                      -> Decl
 797 | DeclAxiom        : forall n ccon vk TV,  @AxiomDecl        n ccon vk  TV             -> Decl.
 798
 799 (* Figure 1, production "pgm" *)
 800 Inductive Pgm Γ Δ :=
 801   mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ.
 802 *)
 803