src/HaskStrongToProof.v

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