Module Qcert.NNRC.Lang.NNRCStratify

Require Import String.
Require Import List.
Require Import Bool.
Require Import BinInt.
Require Import Arith.
Require Import EquivDec.
Require Import Morphisms.
Require Import Permutation.
Require Import Eqdep_dec.
Require Import Program.Basics.
Require Import Utils.
Require Import DataRuntime.
Require Import cNNRC.
Require Import cNNRCNorm.
Require Import cNNRCVars.
Require Import cNNRCEq.
Require Import cNNRCShadow.
Require Import NNRC.
Require Import NNRCEq.
Require Import NNRCShadow.


Section Stratify.
  
  Context {fruntime:foreign_runtime}.

  Section Stratified.
    
    Inductive nnrcKind :=
    | nnrcExpr
    | nnrcStmt.

    Global Instance nnrcKind_eqdec : EqDec nnrcKind eq.
    
    Inductive stratifiedLevel_spec : nnrcKind -> nnrc -> Prop
      :=
      | StratifiedGetConstant_level c : stratifiedLevel_spec nnrcExpr (NNRCGetConstant c)
      | StratifiedVar_level v : stratifiedLevel_spec nnrcExpr (NNRCVar v)
      | StratifiedConst_level c : stratifiedLevel_spec nnrcExpr (NNRCConst c)
      | StratifiedBinop_level b e1 e2 :
          stratifiedLevel_spec nnrcExpr e1 ->
          stratifiedLevel_spec nnrcExpr e2 ->
          stratifiedLevel_spec nnrcExpr (NNRCBinop b e1 e2)
      | StratifiedUnop_level u e :
          stratifiedLevel_spec nnrcExpr e ->
          stratifiedLevel_spec nnrcExpr (NNRCUnop u e)
      | StratifiedLet_level v s1 s2 :
          stratifiedLevel_spec nnrcStmt s1 ->
          stratifiedLevel_spec nnrcStmt s2 ->
          stratifiedLevel_spec nnrcStmt (NNRCLet v s1 s2)
      | StratifiedFor_level v e s :
          stratifiedLevel_spec nnrcExpr e ->
          stratifiedLevel_spec nnrcStmt s ->
          stratifiedLevel_spec nnrcStmt (NNRCFor v e s)
      | StratifiedIf_level e s1 s2 :
          stratifiedLevel_spec nnrcExpr e ->
          stratifiedLevel_spec nnrcStmt s1 ->
          stratifiedLevel_spec nnrcStmt s2 ->
          stratifiedLevel_spec nnrcStmt (NNRCIf e s1 s2)
      | StratifiedEither_level e x1 s1 x2 s2 :
          stratifiedLevel_spec nnrcExpr e ->
          stratifiedLevel_spec nnrcStmt s1 ->
          stratifiedLevel_spec nnrcStmt s2 ->
          stratifiedLevel_spec nnrcStmt (NNRCEither e x1 s1 x2 s2)
      | StratifiedGroupBy_level s ls e :
          stratifiedLevel_spec nnrcExpr e ->
          stratifiedLevel_spec nnrcStmt (NNRCGroupBy s ls e)
      | StratifiedLift_level e : stratifiedLevel_spec nnrcExpr e -> stratifiedLevel_spec nnrcStmt e
    .

    Fixpoint stratifiedLevel (kind:nnrcKind) (e:nnrc) : Prop
      := match e with
         | NNRCGetConstant _ => True
         | NNRCVar _ => True
         | NNRCConst _ => True
         | NNRCBinop _ e1 e2 =>
           stratifiedLevel nnrcExpr e1
           /\ stratifiedLevel nnrcExpr e2
         | NNRCUnop _ e1 => stratifiedLevel nnrcExpr e1
         | NNRCLet _ e1 e2 =>
           kind = nnrcStmt
           /\ stratifiedLevel nnrcStmt e1
           /\ stratifiedLevel nnrcStmt e2
         | NNRCFor _ e1 e2 =>
           kind = nnrcStmt
           /\ stratifiedLevel nnrcExpr e1
           /\ stratifiedLevel nnrcStmt e2
         | NNRCIf e1 e2 e3 =>
           kind = nnrcStmt
           /\ stratifiedLevel nnrcExpr e1
           /\ stratifiedLevel nnrcStmt e2
           /\ stratifiedLevel nnrcStmt e3
         | NNRCEither e1 _ e2 _ e3 =>
           kind = nnrcStmt
           /\ stratifiedLevel nnrcExpr e1
           /\ stratifiedLevel nnrcStmt e2
           /\ stratifiedLevel nnrcStmt e3
         | NNRCGroupBy _ _ e =>
           kind = nnrcStmt
           /\ stratifiedLevel nnrcExpr e
         end.

    Definition stratified := stratifiedLevel nnrcStmt.
    Definition stratified_spec := stratifiedLevel_spec nnrcStmt.

    Lemma stratifiedLevel_lift k e :
      stratifiedLevel k e -> stratifiedLevel nnrcStmt e.

    Lemma stratifiedLevel_stratified k (e:nnrc) :
      stratifiedLevel k e -> stratified e.

    Lemma stratifiedLevel_spec_lifts k e :
      stratifiedLevel_spec k e -> stratifiedLevel_spec nnrcStmt e.

    Lemma stratifiedLevel_spec_lifte k e :
      stratifiedLevel_spec nnrcExpr e -> stratifiedLevel_spec k e.

    Lemma stratifiedLevel_spec_stratified k (e:nnrc) :
      stratifiedLevel_spec k e -> stratified_spec e.

    Lemma stratifiedLevel_correct k e:
      stratifiedLevel k e <-> stratifiedLevel_spec k e.

    Corollary stratified_correct e:
      stratified e <-> stratified_spec e.

    Section dec.
      Lemma stratifiedLevel_dec k (e:nnrc):
        {stratifiedLevel k e} + {~ stratifiedLevel k e}.

      Lemma stratifiedLevel_spec_dec k (e:nnrc):
        {stratifiedLevel_spec k e} + {~ stratifiedLevel_spec k e}.

      Theorem stratified_dec (e:nnrc) :
        {stratified e} + {~ stratified e}.

      Theorem stratified_spec_dec (e:nnrc) :
        {stratified_spec e} + {~ stratified_spec e}.

    End dec.

  End Stratified.
  

  Section stratify.

    Definition nnrc_with_substs : Type := nnrc*list (var*nnrc).

    Definition mk_expr_from_vars (nws:nnrc_with_substs) : nnrc
      := fold_right (fun sdef accum => NNRCLet (fst sdef) (snd sdef) accum) (fst nws) (snd nws).

    Lemma mk_expr_from_vars_eq e sdefs :
      fold_right (fun sdef accum => NNRCLet (fst sdef) (snd sdef) accum) e sdefs = mk_expr_from_vars (e, sdefs).
    
    Definition stratify1_aux
               (body:nnrc)
               (required_kind:nnrcKind)
               (bound_vars:list var)
               (sdefs:list (var*nnrc))
      : nnrc_with_substs
      := match required_kind with
         | nnrcExpr =>
           let fvar := fresh_var "stratify" bound_vars in
           (NNRCVar fvar, sdefs++((fvar, body)::nil))
         | _ => (body, sdefs)
         end.

    Fixpoint stratify_aux (e: nnrc) (required_kind:nnrcKind) (bound_vars:list var): nnrc_with_substs
      := match e with
         | NNRCGetConstant c => (e, nil)
         | NNRCVar _ => (e, nil)
         | NNRCConst _ => (e, nil)
         | NNRCBinop b e1 e2 =>
           let (e1', sdefs1) := stratify_aux e1 nnrcExpr bound_vars in
           let bound_vars2 := (domain sdefs1) ++ bound_vars in
           let (e2', sdefs2) := stratify_aux e2 nnrcExpr (bound_vars2) in
           ((NNRCBinop b e1' e2'), sdefs1++sdefs2)
         | NNRCUnop u e1 =>
           let (e1', sdefs1) := stratify_aux e1 nnrcExpr bound_vars in
           ((NNRCUnop u e1'), sdefs1)
         | NNRCLet x e1 e2 =>
           let e1'ws := stratify_aux e1 nnrcStmt bound_vars in
           let e1' := mk_expr_from_vars e1'ws in
           let e2'ws := stratify_aux e2 nnrcStmt (x::bound_vars) in
           let e2' := mk_expr_from_vars e2'ws in
           stratify1_aux (NNRCLet x e1' e2') required_kind bound_vars nil
         | NNRCFor x e1 e2 =>
           let (e1', sdefs1) := stratify_aux e1 nnrcExpr bound_vars in
           let bound_vars2 := (domain sdefs1) ++ x::bound_vars in
           let e2'ws := stratify_aux e2 nnrcStmt (x::bound_vars) in
           let e2' := mk_expr_from_vars e2'ws in
           stratify1_aux (NNRCFor x e1' e2') required_kind bound_vars2 sdefs1
         | NNRCIf e1 e2 e3 =>
           let (e1', sdefs1) := stratify_aux e1 nnrcExpr bound_vars in
           let bound_vars2 := (domain sdefs1) ++ bound_vars in
           let e2'ws := stratify_aux e2 nnrcStmt bound_vars in
           let e2' := mk_expr_from_vars e2'ws in
           let e3'ws := stratify_aux e3 nnrcStmt bound_vars in
           let e3' := mk_expr_from_vars e3'ws in
           stratify1_aux (NNRCIf e1' e2' e3') required_kind bound_vars2 sdefs1
         | NNRCEither e1 x2 e2 x3 e3 =>
           let (e1', sdefs1) := stratify_aux e1 nnrcExpr bound_vars in
           let bound_vars2 := (domain sdefs1) ++ bound_vars in
           let e2'ws := stratify_aux e2 nnrcStmt (x2::bound_vars) in
           let e2' := mk_expr_from_vars e2'ws in
           let e3'ws := stratify_aux e3 nnrcStmt (x3::bound_vars) in
           let e3' := mk_expr_from_vars e3'ws in
           stratify1_aux (NNRCEither e1' x2 e2' x3 e3') required_kind (x2::x3::bound_vars2) sdefs1
         | NNRCGroupBy s ls e1 =>
           let (e1', sdefs1) := stratify_aux e1 nnrcExpr bound_vars in
           stratify1_aux (NNRCGroupBy s ls e1') required_kind bound_vars sdefs1
         end.

    Definition stratify (e: nnrc) : nnrc
      := mk_expr_from_vars (stratify_aux e nnrcStmt (nnrc_free_vars e)).

  End stratify.
  
  Section tests.
    Local Open Scope nnrc_scope.
    Local Open Scope string_scope.


    Example nnrc1 := ((‵abs ‵ (dnat 3) ‵+ ‵(dnat 5)) ‵+ ((‵(dnat 4) ‵+ ‵(dnat 7)) ‵+‵`(dnat 3))).

    Example nnrc2 := NNRCLet "x" nnrc1 (NNRCVar "x").

    Example nnrc3 := (‵abs (NNRCLet "x" ((‵(dnat 1) ‵+ ‵(dnat 2))) (((NNRCVar "x" ‵+ ‵(dnat 8)))) ‵+ ‵(dnat 5)) ‵+ ((‵(dnat 4) ‵+ ‵(dnat 7)) ‵+‵`(dnat 3))).

    Example nnrc4 := (‵abs (NNRCFor "x" ((‵(dnat 1) ‵+ ‵(dnat 2))) (((NNRCVar "x" ‵+ ‵(dnat 8)))) ‵+ ‵(dnat 5)) ‵+ ((‵(dnat 4) ‵+ ‵(dnat 7)) ‵+‵`(dnat 3))).

    Example nnrc5 := (‵abs (NNRCLet "z" (NNRCFor "x" ((‵(dnat 1) ‵+ ‵(dnat 2))) (((NNRCVar "x" ‵+ ‵(dnat 8)))) ‵+ ‵(dnat 5)) (NNRCVar "z")) ‵+ ((‵(dnat 4) ‵+ ‵(dnat 7)) ‵+‵`(dnat 3))).

    Example nnrc6 := (‵abs (NNRCLet "z" (NNRCFor "x" ((‵(dnat 1) ‵+ ‵(dnat 2))) (((NNRCVar "x" ‵+ ‵(dnat 8))))) (NNRCVar "z")) ‵+ ((‵(dnat 4) ‵+ ‵(dnat 7)) ‵+‵`(dnat 3))).

    Example nnrc7 := NNRCLet "x" (NNRCLet "y" ‵(dnat 3) (‵(dnat 8) ‵+ (NNRCVar "y"))) (NNRCVar "x").
    

    Example nnrc8 := NNRCLet "x" (NNRCLet "x" ‵(dnat 3) (‵(dnat 8) ‵+ (NNRCVar "x"))) (NNRCVar "x").
    

  End tests.

  Lemma Forall_app_iff {A} (P:A->Prop) l1 l2 :
      Forall P (l1 ++ l2) <-> Forall P l1 /\ Forall P l2.

  Ltac list_simpler :=
    repeat progress (
             try match goal with
                 | [H: ?l = ?l ++ _ |- _ ] => apply app_inv_self_l in H; try subst
                 | [H: ?l = _ ++ ?l |- _ ] => apply app_inv_self_r in H; try subst
                 | [H: ?l ++ _ = ?l ++ _ |- _ ] => apply app_inv_head in H; try subst
                 | [H: _ ++ ?l = _ ++ ?l |- _ ] => apply app_inv_tail in H; try subst
                 | [H: In _ (remove _ _ _) |- _] => apply remove_inv in H; destruct H
                 | [H: ?a <> ?v |- context [In ?a (remove _ ?v _)]] => rewrite <- (remove_in_neq _ _ _ H)
                 | [H: ?v <> ?a |- context [In ?a (remove _ ?v _)]] => rewrite <- (remove_in_neq _ a v ) by congruence
                 | [H: ?a = ?v -> False |- context [In ?a (remove _ ?v _)]] => rewrite <- (remove_in_neq _ _ _ H)
                 | [H: ?v = ?a -> False |- context [In ?a (remove _ ?v _)]] => rewrite <- (remove_in_neq _ a v) by congruence
                 end
             ; repeat rewrite domain_app in *
             ; repeat rewrite codomain_app in *
             ; repeat rewrite map_app in *
             ; repeat rewrite concat_app in *
             ; repeat rewrite in_app_iff in *
             ; repeat rewrite Forall_app_iff in *
           ).
  Section Effective.

    Lemma stratify1_aux_stratified {body required_level bv sdefs1 n sdefs2} :
      stratify1_aux body required_level bv sdefs1 = (n,sdefs2) ->
      stratifiedLevel nnrcStmt body ->
      Forall (stratifiedLevel nnrcStmt) (codomain sdefs1) ->
      stratifiedLevel required_level n /\
      Forall (stratifiedLevel nnrcStmt) (codomain sdefs2).

    Lemma mk_expr_from_vars_stratified {e sdefs} :
      stratifiedLevel nnrcStmt e ->
      Forall (stratifiedLevel nnrcStmt) (codomain sdefs) ->
      stratifiedLevel nnrcStmt (mk_expr_from_vars (e, sdefs)).
    
    Lemma stratify_aux_stratified {e required_level bound_vars n sdefs} :
      stratify_aux e required_level bound_vars = (n, sdefs) ->
      stratifiedLevel required_level n /\
      Forall (stratifiedLevel nnrcStmt) (codomain sdefs).

    Theorem stratify_stratified (e: nnrc) : stratified (stratify e).

    Corollary stratify_stratified_spec (e: nnrc) : stratified_spec (stratify e).

  End Effective.

  Section Idempotent.

    Lemma mk_expr_from_vars_nil e :
      mk_expr_from_vars (e, nil) = e.
    
    Lemma stratify_aux_stratify_id
          (e: nnrc)
          (required_level:nnrcKind)
          (bound_vars:list var) :
      stratifiedLevel required_level e ->
      stratify_aux e required_level bound_vars = (e, nil).

    Theorem stratify_stratify_id (e: nnrc) :
      stratified e ->
      stratify e = e.

    Corollary stratify_idem (e: nnrc) :
      stratify (stratify e) = stratify e.

  End Idempotent.

  Section BoundVars.

    Lemma stratify1_aux_nbound_vars {e required_kind bound_vars n l sdefs} :
      stratify1_aux e required_kind bound_vars sdefs = (n,l) ->
      forall x, In x (domain l) -> In x bound_vars -> In x (domain sdefs).

    Lemma stratify_aux_nbound_vars {e required_kind bound_vars n sdefs} :
      stratify_aux e required_kind bound_vars = (n,sdefs) ->
      disjoint (domain sdefs) bound_vars.

  End BoundVars.

  Section FreeVars.

    Fixpoint growing_fv_ctxt (l:list (var*nnrc)) (ctxt:list var) : Prop
      := match l with
         | nil => True
         | (v,e)::lx =>
           incl (nnrc_free_vars e) ctxt
           /\ growing_fv_ctxt lx (v::ctxt)
         end.

    Global Instance growing_fv_ctxt_incl :
      Proper (eq ==> (@incl var) ==> impl) growing_fv_ctxt.

    Global Instance growing_fv_ctxt_equiv :
      Proper (eq ==> (@equivlist var) ==> iff) growing_fv_ctxt.

    Lemma growing_fv_ctxt_app sdefs1 sdefs2 ctxt :
      growing_fv_ctxt (sdefs1 ++ sdefs2) ctxt <->
      (growing_fv_ctxt sdefs1 ctxt /\ growing_fv_ctxt sdefs2 (ctxt ++ domain sdefs1)).

    Lemma mk_expr_from_vars_growing_fv_free_fw {sdefs ctxt} :
      growing_fv_ctxt sdefs ctxt ->
      forall e x,
        In x (nnrc_free_vars (mk_expr_from_vars (e, sdefs))) ->
        ((In x (nnrc_free_vars e) /\ ~ In x (domain sdefs)) \/ In x ctxt).

    Lemma mk_expr_from_vars_growing_fv_free_fw_codomain {sdefs e x} :
      In x (nnrc_free_vars (mk_expr_from_vars (e, sdefs))) ->
      ((In x (nnrc_free_vars e) \/ In x (concat (map nnrc_free_vars (codomain sdefs))))).

    Lemma mk_expr_from_vars_growing_fv_free_bk e sdefs x :
      ((In x (nnrc_free_vars e) \/ In x (concat (map nnrc_free_vars (codomain sdefs)))) /\ ~ In x (domain sdefs)) ->
      In x (nnrc_free_vars (mk_expr_from_vars (e, sdefs))).

    Lemma stratify1_aux_free_vars_incl {e required_level bound_vars n sdefs1 sdefs2} :
      stratify1_aux e required_level bound_vars sdefs1 = (n, sdefs2) ->
      incl (nnrc_free_vars n) (nnrc_free_vars e ++ (domain sdefs2)).

    Lemma stratify1_aux_sdefs_app {e required_level bound_vars n sdefs1 sdefs2} :
      stratify1_aux e required_level bound_vars sdefs1 = (n, sdefs2) ->
      { l | sdefs2 = sdefs1++l}.

    Lemma stratify1_aux_gfc {e required_level bound_vars n sdefs1 sdefs2} :
      stratify1_aux e required_level bound_vars sdefs1 = (n, sdefs2) ->
      forall ctxt,
        growing_fv_ctxt sdefs1 ctxt ->
        growing_fv_ctxt sdefs2 (ctxt++nnrc_free_vars e).

    Lemma stratify1_aux_gfc_weak {e required_level bound_vars n sdefs1 sdefs2} :
      stratify1_aux e required_level bound_vars sdefs1 = (n, sdefs2) ->
      growing_fv_ctxt sdefs1 (nnrc_free_vars e) ->
      growing_fv_ctxt sdefs2 (nnrc_free_vars e).

    Lemma stratify1_aux_gfc_app {e required_level bound_vars n sdefs1 sdefs2} :
      stratify1_aux e required_level bound_vars sdefs1 = (n, sdefs1++sdefs2) ->
      forall ctxt,
        growing_fv_ctxt sdefs1 ctxt ->
        growing_fv_ctxt sdefs2 (ctxt++nnrc_free_vars e).

    Lemma stratify1_aux_gfc_app_weak {e required_level bound_vars n sdefs1 sdefs2} :
      stratify1_aux e required_level bound_vars sdefs1 = (n, sdefs1++sdefs2) ->
      growing_fv_ctxt sdefs1 (nnrc_free_vars e) ->
      growing_fv_ctxt sdefs2 (nnrc_free_vars e).

    Lemma mk_expr_from_vars_has_codomain_vars a l n :
      In a (concat (map nnrc_free_vars (codomain l))) ->
      ~ In a (domain l) ->
      In a (nnrc_free_vars (mk_expr_from_vars (n, l))).

    Lemma stratify1_aux_free_vars {e required_level bound_vars n}
          {sdefs1 sdefs2:list (var*nnrc)} :
      stratify1_aux e required_level bound_vars sdefs1 = (n, sdefs1++sdefs2) ->
      equivlist (nnrc_free_vars n ++ (concat (map nnrc_free_vars (codomain sdefs2)))) (nnrc_free_vars e ++ (domain sdefs2)).

    Lemma stratify_aux_free_vars_and_growing
          {e required_level bound_vars n sdefs} :
      stratify_aux e required_level bound_vars = (n,sdefs) ->
      incl (nnrc_free_vars e) bound_vars ->
      equivlist (nnrc_free_vars n ++ (concat (map nnrc_free_vars (codomain sdefs)))) (nnrc_free_vars e ++ domain sdefs)
      /\ growing_fv_ctxt sdefs (nnrc_free_vars e).

    Corollary stratify_aux_free_vars
              {e required_level bound_vars n sdefs} :
      stratify_aux e required_level bound_vars = (n,sdefs) ->
      incl (nnrc_free_vars e) bound_vars ->
      equivlist (nnrc_free_vars n ++ (concat (map nnrc_free_vars (codomain sdefs)))) (nnrc_free_vars e ++ domain sdefs).

    Corollary stratify_aux_free_vars_gfc
              {e required_level bound_vars n sdefs} :
      stratify_aux e required_level bound_vars = (n,sdefs) ->
      incl (nnrc_free_vars e) bound_vars ->
      growing_fv_ctxt sdefs (nnrc_free_vars e).

    Lemma mk_expr_stratify_aux_free_vars e required_kind bound_vars :
      incl (nnrc_free_vars e) bound_vars ->
      equivlist (nnrc_free_vars (mk_expr_from_vars (stratify_aux e required_kind bound_vars))) (nnrc_free_vars e).
    
    Theorem stratify_free_vars e :
      equivlist (nnrc_free_vars (stratify e)) (nnrc_free_vars e).

  End FreeVars.

  Section Eval_substs.

    Fixpoint eval_substs h cenv (sdefs:list (var*nnrc)) (env:bindings): option bindings
      := match sdefs with
         | nil => Some env
         | (v,n)::sdefs' =>
           olift (fun d => eval_substs h cenv sdefs' ((v,d)::env))
                 (@nnrc_eval _ h cenv env n)
         end.

    Definition eval_nnrc_with_substs h cenv env nws :=
      olift (fun env' => @nnrc_eval _ h cenv env' (fst nws))
            (eval_substs h cenv (snd nws) env).

    Lemma eval_nnrc_with_substs_eq h cenv env a b :
      olift (fun env' => @nnrc_eval _ h cenv env' a)
            (eval_substs h cenv b env) = eval_nnrc_with_substs h cenv env (a,b).

    Lemma eval_nnrc_with_substs_eq_core h cenv env a b :
      olift (fun env' => @nnrc_core_eval _ h cenv env' (nnrc_to_nnrc_base a))
            (eval_substs h cenv b env) = eval_nnrc_with_substs h cenv env (a,b).

    Lemma mk_expr_from_vars_eval h cenv env nws :
      @nnrc_eval _ h cenv env
                 (mk_expr_from_vars nws) =
      eval_nnrc_with_substs h cenv env nws.

    Lemma eval_substs_app h cenv (sdefs1 sdefs2:list (var*nnrc)) (env:bindings) :
      eval_substs h cenv (sdefs1++sdefs2) env = olift (eval_substs h cenv sdefs2) (eval_substs h cenv sdefs1 env).

    Lemma eval_substs_applies {h cenv sdefs env res} :
      eval_substs h cenv sdefs env = Some res ->
      {x | res = x++env & domain x = rev (domain sdefs)}.

    Lemma eval_substs_lookup_equiv_on_env
          h cenv sdefs {l env1 env2}:
      lookup_equiv_on l env1 env2 ->
      incl (concat (map nnrc_free_vars (codomain sdefs))) l ->
      match eval_substs h cenv sdefs env1, eval_substs h cenv sdefs env2 with
      | Some e1, Some e2 => lookup_equiv_on l e1 e2
      | None, None => True
      | _, _ => False
      end.

    Lemma eval_substs_lookup_equiv_env {h cenv sdefs env1 env2}:
      lookup_equiv env1 env2 ->
      match eval_substs h cenv sdefs env1, eval_substs h cenv sdefs env2 with
      | Some e1, Some e2 => lookup_equiv e1 e2
      | None, None => True
      | _, _ => False
      end.

    Lemma eval_substs_disjoint_swap_env
          h cenv sdefs env₁ env₂ x₁ d₁ x₂ d₂ :
      x₁ <> x₂ ->
      match eval_substs h cenv sdefs (env₁++(x₁,d₁)::(x₂,d₂)::env₂)
            , eval_substs h cenv sdefs (env₁++(x₂,d₂)::(x₁,d₁)::env₂) with
      | Some res₁, Some res₂ =>
        {env' | res₁ = env' ++ env₁++((x₁,d₁)::(x₂,d₂)::env₂) & res₂ = env' ++ env₁ ++ ((x₂,d₂)::(x₁,d₁)::env₂)}
      | None, None => True
      | _, _ => False
      end.

    Lemma eval_substs_disjoint_cons_env h cenv sdefs x d :
      ~ In x (domain sdefs) ->
      ~ In x (concat (map nnrc_free_vars (codomain sdefs))) ->
      forall env,
        match eval_substs h cenv sdefs env
              , eval_substs h cenv sdefs ((x,d)::env) with
        | Some res₁, Some res₂ => {env' | res₁ = env' ++ env & res₂ = env' ++ (x,d)::env}
        | None, None => True
        | _, _ => False
        end.
    
    Lemma eval_substs_disjoint_middle_some h cenv sdefs env' :
      disjoint (domain sdefs) (domain env') ->
      disjoint (concat (map nnrc_free_vars (codomain sdefs))) (domain env') ->
      forall env,
        match eval_substs h cenv sdefs env
              , eval_substs h cenv sdefs (env' ++ env) with
        | Some res₁, Some res₂ => {env'' | res₁ = env'' ++ env & res₂ = env'' ++ env' ++ env}
        | None, None => True
        | _, _ => False
        end.

    Lemma mk_expr_from_vars_eq_expr {n1 n2} :
      nnrc_eq n1 n2 ->
      forall sdefs,
        nnrc_eq (mk_expr_from_vars (n1, sdefs)) (mk_expr_from_vars (n2, sdefs)).

  End Eval_substs.

  Section Correct.

    Opaque fresh_var.
    Lemma stratify1_aux_correct h cenv env e bound_vars required_kind sdefs :
      eval_nnrc_with_substs h cenv env (stratify1_aux e required_kind bound_vars sdefs) =
      eval_nnrc_with_substs h cenv env (e,sdefs).

    Lemma eval_substs_normalized {h cenv env sdefs env'} :
      eval_substs h cenv sdefs env = Some env' ->
      Forall (data_normalized h) (map snd cenv) ->
      Forall (data_normalized h) (map snd env) ->
      Forall (data_normalized h) (map snd env').
    
    Lemma stratify_aux_correct h cenv env e bound_vars required_kind :
      incl (nnrc_free_vars e) bound_vars ->
      @nnrc_eval _ h cenv env (mk_expr_from_vars (stratify_aux e required_kind bound_vars)) =
      @nnrc_eval _ h cenv env e.

    Theorem stratify_correct h cenv env e :
      @nnrc_eval _ h cenv env (stratify e) =
      @nnrc_eval _ h cenv env e.

    Theorem stratify_correct_eq e :
      nnrc_eq (stratify e) e.

  End Correct.

  Section Core.

    Lemma stratify1_aux_preserves_core
          {e required_level bound_vars n}
          {sdefs1 sdefs2:list (var*nnrc)} :
      stratify1_aux e required_level bound_vars sdefs1 = (n, sdefs2) ->
      nnrcIsCore e /\ Forall nnrcIsCore (codomain sdefs1) <->
      nnrcIsCore n /\ Forall nnrcIsCore (codomain sdefs2).

    Lemma mk_expr_from_vars_preserves_core nws :
      (nnrcIsCore (fst nws) /\ Forall nnrcIsCore (codomain (snd nws))) <->
      nnrcIsCore (mk_expr_from_vars nws).
    
    Lemma stratify_aux_preserves_core
          {e required_level bound_vars n sdefs} :
      stratify_aux e required_level bound_vars = (n,sdefs) ->
      nnrcIsCore e <->
      nnrcIsCore n /\ Forall nnrcIsCore (codomain sdefs).

    Theorem stratify_preserves_core e :
      nnrcIsCore e <-> nnrcIsCore (stratify e).

    Definition stratified_core (e:nnrc_core) : Prop
      := stratified (proj1_sig e).
    
    Definition stratify_core (e:nnrc_core) : nnrc_core
      := exist _ _ (proj1 (stratify_preserves_core _) (proj2_sig e)).

    Theorem stratify_stratified_core (e: nnrc_core) : stratified_core (stratify_core e).
    
    Theorem stratify_stratify_id_core (e: nnrc_core) :
      stratified_core e ->
      stratify_core e = e.

    Corollary stratify_idem_core (e: nnrc_core) :
      stratify_core (stratify_core e) = stratify_core e.
    
  End Core.
  
End Stratify.