Qcert.NRAEnv.Optim.NRAEnvOptimizer

Section NRAEnvOptimizer.









  Lemma tnraenv_rewrites_to_trans {model:basic_model} p1 p2 p3:
    p1 ⇒ₓ p2 → p2 ⇒ₓ p3 → p1 ⇒ₓ p3.

  Lemma AUX {model:basic_model} f p p':
    (∀ p, p ⇒ₓ f p) → p ⇒ₓ p' → p ⇒ₓ f p'.

  Section rewriter.
    Context {fruntime:foreign_runtime}.

    Definition nraenv_map (f: nraenv → nraenv) (p: nraenv) :=
      match p with
      | NRAEnvID ⇒ NRAEnvID
      | NRAEnvConst rd ⇒ NRAEnvConst rd
      | NRAEnvBinop bop op1 op2 ⇒ NRAEnvBinop bop (f op1) (f op2)
      | NRAEnvUnop uop op1 ⇒ NRAEnvUnop uop (f op1)
      | NRAEnvMap op1 op2 ⇒ NRAEnvMap (f op1) (f op2)
      | NRAEnvMapConcat op1 op2 ⇒ NRAEnvMapConcat (f op1) (f op2)
      | NRAEnvProduct op1 op2 ⇒ NRAEnvProduct (f op1) (f op2)
      | NRAEnvSelect op1 op2 ⇒ NRAEnvSelect (f op1) (f op2)
      | NRAEnvEither op1 op2 ⇒ NRAEnvEither (f op1) (f op2)
      | NRAEnvEitherConcat op1 op2 ⇒ NRAEnvEitherConcat (f op1) (f op2)
      | NRAEnvDefault op1 op2 ⇒ NRAEnvDefault (f op1) (f op2)
      | NRAEnvApp op1 op2 ⇒ NRAEnvApp (f op1) (f op2)
      | NRAEnvGetConstant s ⇒ NRAEnvGetConstant s
      | NRAEnvEnv ⇒ NRAEnvEnv
      | NRAEnvAppEnv op1 op2 ⇒ NRAEnvAppEnv (f op1) (f op2)
      | NRAEnvMapEnv op1 ⇒ NRAEnvMapEnv (f op1)
      | NRAEnvFlatMap op1 op2 ⇒ NRAEnvFlatMap (f op1) (f op2)
      | NRAEnvJoin op1 op2 op3 ⇒ NRAEnvJoin (f op1) (f op2) (f op3)
      | NRAEnvProject sl op1 ⇒ NRAEnvProject sl (f op1)
      | NRAEnvGroupBy s sl op1 ⇒ NRAEnvGroupBy s sl (f op1)
      | NRAEnvUnnest a b op1 ⇒ NRAEnvUnnest a b (f op1)
      end.

    Fixpoint nraenv_map_deep (f: nraenv → nraenv) (p: nraenv) :=
      match p with
      | NRAEnvID ⇒ f NRAEnvID
      | NRAEnvConst rd ⇒ f (NRAEnvConst rd)
      | NRAEnvBinop bop op1 op2 ⇒ f (NRAEnvBinop bop (nraenv_map_deep f op1) (nraenv_map_deep f op2))
      | NRAEnvUnop uop op1 ⇒ f (NRAEnvUnop uop (nraenv_map_deep f op1))
      | NRAEnvMap op1 op2 ⇒ f (NRAEnvMap (nraenv_map_deep f op1) (nraenv_map_deep f op2))
      | NRAEnvMapConcat op1 op2 ⇒ f (NRAEnvMapConcat (nraenv_map_deep f op1) (nraenv_map_deep f op2))
      | NRAEnvProduct op1 op2 ⇒ f (NRAEnvProduct (nraenv_map_deep f op1) (nraenv_map_deep f op2))
      | NRAEnvSelect op1 op2 ⇒ f (NRAEnvSelect (nraenv_map_deep f op1) (nraenv_map_deep f op2))
      | NRAEnvDefault op1 op2 ⇒ f (NRAEnvDefault (nraenv_map_deep f op1) (nraenv_map_deep f op2))
      | NRAEnvEither op1 op2 ⇒ f (NRAEnvEither (nraenv_map_deep f op1) (nraenv_map_deep f op2))
      | NRAEnvEitherConcat op1 op2 ⇒ f (NRAEnvEitherConcat (nraenv_map_deep f op1) (nraenv_map_deep f op2))
      | NRAEnvApp op1 op2 ⇒ f (NRAEnvApp (nraenv_map_deep f op1) (nraenv_map_deep f op2))
      | NRAEnvGetConstant s ⇒ f (NRAEnvGetConstant s)
      | NRAEnvEnv ⇒ f NRAEnvEnv
      | NRAEnvAppEnv op1 op2 ⇒ f (NRAEnvAppEnv (nraenv_map_deep f op1) (nraenv_map_deep f op2))
      | NRAEnvMapEnv op1 ⇒ f (NRAEnvMapEnv (nraenv_map_deep f op1))
      | NRAEnvFlatMap op1 op2 ⇒ f (NRAEnvFlatMap (nraenv_map_deep f op1) (nraenv_map_deep f op2))
      | NRAEnvJoin op1 op2 op3 ⇒ f (NRAEnvJoin (nraenv_map_deep f op1) (nraenv_map_deep f op2) (nraenv_map_deep f op3))
      | NRAEnvProject sl op1 ⇒ f (NRAEnvProject sl (nraenv_map_deep f op1))
      | NRAEnvGroupBy s sl op1 ⇒ f (NRAEnvGroupBy s sl (nraenv_map_deep f op1))
      | NRAEnvUnnest a b op1 ⇒ f (NRAEnvUnnest a b (nraenv_map_deep f op1))
    end.
  End rewriter.

  Section dup.
    Definition nraenv_nodupA {fruntime:foreign_runtime} (q:nraenv) : Prop :=
      nodupA (cnraenv_of_nraenv q).

    Fixpoint nodupA_checker {fruntime:foreign_runtime} (p:nraenv) : bool
    := match p with
       | NRAEnvUnop ADistinct _ ⇒ true
       | NRAEnvBinop AMinus p₁ p₂ ⇒ nodupA_checker p₂
       | _ ⇒ false
       end.

    Lemma nodupA_checker_correct {bm:basic_model} (p:nraenv) :
      nodupA_checker p = true → nraenv_nodupA p.

    Definition dup_elim_fun {fruntime:foreign_runtime} (p:nraenv) :=
      match p with
      | NRAEnvUnop ADistinct q ⇒
        if nodupA_checker q then q else p
      | _ ⇒ p
      end.

    Lemma dup_elim_fun_correctness {bm:basic_model} (p:nraenv) :
      dup_elim_fun p ≡ₓ p.

  End dup.

  Definition tnraenv_map {fruntime:foreign_runtime} := nraenv_map.

  Lemma tnraenv_map_correctness {model:basic_model}:
    ∀ f: nraenv → nraenv,
    ∀ p: nraenv,
      (∀ p', p' ⇒ₓ f p') → p ⇒ₓ tnraenv_map f p.

  Definition tnraenv_map_deep {fruntime:foreign_runtime} := nraenv_map_deep.

  Lemma nraenv_map_deep_correctness {model:basic_model}:
    ∀ f: nraenv → nraenv,
    ∀ p: nraenv,
      (∀ p', p' ⇒ₓ f p') → p ⇒ₓ tnraenv_map_deep f p.



  Definition tand_comm_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvBinop AAnd op1 op2 ⇒ NRAEnvBinop AAnd op2 op1
      | _ ⇒ p
    end.

  Lemma tand_comm_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tand_comm_fun p.

  Definition tand_comm_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "and commute"
         "Swap the arguments to the boolean and operator"
         "tand_comm_fun"
         tand_comm_fun .

  Definition tand_comm_step_correct {model:basic_model}
    := mkOptimizerStepModel tand_comm_step tand_comm_fun_correctness.


  Definition tselect_and_comm_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvSelect (NRAEnvBinop AAnd op1 op2) op ⇒
        NRAEnvSelect (NRAEnvBinop AAnd op2 op1) op
      | _ ⇒ p
    end.

  Lemma tselect_and_comm_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tselect_and_comm_fun p.

  Definition tselect_and_comm_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "select/and swap"
         "Swap the arguments to the boolean operator when it is used in a selection"
         "tselect_and_comm_fun"
         tselect_and_comm_fun .

  Definition tselect_and_comm_step_correct {model:basic_model}
    := mkOptimizerStepModel tselect_and_comm_step tselect_and_comm_fun_correctness.

  Definition select_union_distr_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvSelect op (NRAEnvBinop AUnion op1 op2) ⇒
        NRAEnvBinop AUnion (NRAEnvSelect op op1) (NRAEnvSelect op op2)
      | _ ⇒ p
    end.

  Lemma select_union_distr_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ select_union_distr_fun p.

  Definition select_union_distr_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "select/union distr"
         "Pushes selection through union"
         "select_union_distr_fun"
         select_union_distr_fun .

  Definition select_union_distr_step_correct {model:basic_model}
    := mkOptimizerStepModel select_union_distr_step select_union_distr_fun_correctness.


  Definition tselect_and_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvSelect op1 (NRAEnvSelect op2 op) ⇒
        NRAEnvSelect (NRAEnvBinop AAnd op2 op1) op
      | _ ⇒ p
    end.

  Lemma tselect_and_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tselect_and_fun p.

  Definition tselect_and_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "select/select fusion"
         "Fuse nested selections into a single selection using a conjunction"
         "tselect_and_fun"
         tselect_and_fun .

  Definition tselect_and_step_correct {model:basic_model}
    := mkOptimizerStepModel tselect_and_step tselect_and_fun_correctness.


  Definition tdot_from_duplicate_r_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvUnop (ADot s2)
               (NRAEnvBinop AConcat (NRAEnvUnop (ARec s1) op1) (NRAEnvUnop (ARec s2') op2)) ⇒
        if s2 == s2' then
          op2
        else
          p
      | _ ⇒ p
    end.

  Lemma tdot_from_duplicate_r_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tdot_from_duplicate_r_fun p.

  Definition tdot_from_duplicate_r_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "dot/concat/rec right dup"
         "Simplifies field lookup of a concatenation with a record creation of that field"
         "tdot_from_duplicate_r_fun"
         tdot_from_duplicate_r_fun .

  Definition tdot_from_duplicate_r_step_correct {model:basic_model}
    := mkOptimizerStepModel tdot_from_duplicate_r_step tdot_from_duplicate_r_fun_correctness.


  Definition tdot_from_duplicate_l_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvUnop (ADot s1)
               (NRAEnvBinop AConcat (NRAEnvUnop (ARec s1') op1) (NRAEnvUnop (ARec s2) op2)) ⇒
        if (s1 ≠ s2) then
          if s1 == s1' then op1
          else p
        else p
      | _ ⇒ p
    end.

  Lemma tdot_from_duplicate_l_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tdot_from_duplicate_l_fun p.

  Definition tdot_from_duplicate_l_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "dot/concat/rec left dup"
         "Simplifies field lookup of a concatenation with a record creation of that field"
         "tdot_from_duplicate_l_fun"
         tdot_from_duplicate_l_fun .

  Definition tdot_from_duplicate_l_step_correct {model:basic_model}
    := mkOptimizerStepModel tdot_from_duplicate_l_step tdot_from_duplicate_l_fun_correctness.

  Definition tflatten_coll_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvUnop AFlatten (NRAEnvUnop AColl p) ⇒ p
      | _ ⇒ p
    end.

  Lemma tflatten_coll_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tflatten_coll_fun p.

  Definition tflatten_coll_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "flatten/coll"
         "Simplify flatten of a bag constructor"
         "tflatten_coll_fun"
         tflatten_coll_fun .

  Definition tflatten_coll_step_correct {model:basic_model}
    := mkOptimizerStepModel tflatten_coll_step tflatten_coll_fun_correctness.

  Definition tconcat_empty_record_r_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvBinop AConcat p (NRAEnvConst (drec [])) ⇒
        p
      | _ ⇒ p
    end.

  Lemma tconcat_empty_record_r_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tconcat_empty_record_r_fun p.

  Definition tconcat_empty_record_r_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "concat/nil right"
         "Remove concatenation with an empty record"
         "tconcat_empty_record_r_fun"
         tconcat_empty_record_r_fun .

  Definition tconcat_empty_record_r_step_correct {model:basic_model}
    := mkOptimizerStepModel tconcat_empty_record_r_step tconcat_empty_record_r_fun_correctness.

  Definition tconcat_empty_record_l_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvBinop AConcat (NRAEnvConst (drec [])) p ⇒
         p
      | _ ⇒ p
    end.

  Lemma tconcat_empty_record_l_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tconcat_empty_record_l_fun p.

    Definition tconcat_empty_record_l_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "concat/nil left"
         "Remove concatenation with an empty record"
         "tconcat_empty_record_l_fun"
         tconcat_empty_record_l_fun .

  Definition tconcat_empty_record_l_step_correct {model:basic_model}
    := mkOptimizerStepModel tconcat_empty_record_l_step tconcat_empty_record_l_fun_correctness.

  Definition tdot_over_concat_r_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
    | NRAEnvUnop (ADot a₂) (NRAEnvBinop AConcat q₁ (NRAEnvUnop (ARec a₁) q₂)) ⇒
       if a₁ == a₂
       then q₂
       else NRAEnvUnop (ADot a₂) q₁
      | _ ⇒ p
    end.

  Lemma tdot_over_concat_r_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tdot_over_concat_r_fun p.

  Definition tdot_over_concat_r_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "dot/concat/rec right"
         "Simplify field lookup of a concatenation of a record construction"
         "tdot_over_concat_r_fun"
         tdot_over_concat_r_fun .

  Definition tdot_over_concat_r_step_correct {model:basic_model}
    := mkOptimizerStepModel tdot_over_concat_r_step tdot_over_concat_r_fun_correctness.

  Definition tdot_over_concat_l_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
    | NRAEnvUnop (ADot a₂) (NRAEnvBinop AConcat (NRAEnvUnop (ARec a₁) q₁) q₂) ⇒
       if a₁ == a₂
       then p
       else NRAEnvUnop (ADot a₂) q₂
      | _ ⇒ p
    end.

  Lemma tdot_over_concat_l_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tdot_over_concat_l_fun p.

   Definition tdot_over_concat_l_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "dot/concat/rec left"
         "Simplify field lookup of a concatenation of a record construction"
         "tdot_over_concat_l_fun"
         tdot_over_concat_l_fun .

  Definition tdot_over_concat_l_step_correct {model:basic_model}
    := mkOptimizerStepModel tdot_over_concat_l_step tdot_over_concat_l_fun_correctness.

  Definition tmerge_empty_record_r_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvBinop AMergeConcat p (NRAEnvConst (drec [])) ⇒
         NRAEnvUnop AColl p
      | _ ⇒ p
    end.

  Lemma tmerge_empty_record_r_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tmerge_empty_record_r_fun p.

  Definition tmerge_empty_record_r_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "merge-concat/nil right"
         "Simplify merge concat of an empty record"
         "tmerge_empty_record_r_fun"
         tmerge_empty_record_r_fun .

  Definition tmerge_empty_record_r_step_correct {model:basic_model}
    := mkOptimizerStepModel tmerge_empty_record_r_step tmerge_empty_record_r_fun_correctness.

  Definition tmerge_empty_record_l_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvBinop AMergeConcat (NRAEnvConst (drec [])) p ⇒
         NRAEnvUnop AColl p
      | _ ⇒ p
    end.

  Lemma tmerge_empty_record_l_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tmerge_empty_record_l_fun p.

  Definition tmerge_empty_record_l_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "merge-concat/nil left"
         "Simplify merge concat of an empty record"
         "tmerge_empty_record_l_fun"
         tmerge_empty_record_l_fun .

  Definition tmerge_empty_lecord_l_step_correct {model:basic_model}
    := mkOptimizerStepModel tmerge_empty_record_l_step tmerge_empty_record_l_fun_correctness.

  Definition tmap_into_id_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvMap NRAEnvID p ⇒ p
      | _ ⇒ p
    end.

  Lemma tmap_into_id_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tmap_into_id_fun p.

  Definition tmap_into_id_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "map/id"
         "Simplify map of ID"
         "tmap_into_id_fun"
         tmap_into_id_fun .

  Definition tmap_into_id_step_correct {model:basic_model}
    := mkOptimizerStepModel tmap_into_id_step tmap_into_id_fun_correctness.

  Definition tflatten_map_coll_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvUnop AFlatten (NRAEnvMap (NRAEnvUnop AColl p1) p2) ⇒
        NRAEnvMap p1 p2
      | _ ⇒ p
    end.

  Lemma tflatten_map_coll_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tflatten_map_coll_fun p.

  Definition tflatten_map_coll_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "flatten/map/coll"
         "Simplify flatten of the map of a bag constructor"
         "tflatten_map_coll_fun"
         tflatten_map_coll_fun .

  Definition tflatten_map_coll_step_correct {model:basic_model}
    := mkOptimizerStepModel tflatten_map_coll_step tflatten_map_coll_fun_correctness.

  Definition tflatten_flatten_map_either_nil_fun {fruntime:foreign_runtime} (p: nraenv) :=
      match p with
        NRAEnvUnop AFlatten
                   (NRAEnvUnop AFlatten (NRAEnvMap (NRAEnvApp (NRAEnvEither p₁ (NRAEnvConst (dcoll nil))) p₂) p₃)) ⇒
        NRAEnvUnop AFlatten (NRAEnvMap (NRAEnvApp
                                          (NRAEnvEither (NRAEnvUnop AFlatten p₁)
                                                        (NRAEnvConst (dcoll nil))) p₂) p₃)
      | _ ⇒ p
    end.

  Lemma tflatten_flatten_map_either_nil_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tflatten_flatten_map_either_nil_fun p.


  Definition tflatten_flatten_map_either_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "flatten/flatten/map/app/either/nil right"
         "Simplify nested flatten of an either nil (under an application)"
         "tflatten_flatten_map_either_nil_fun"
         tflatten_flatten_map_either_nil_fun .

  Definition tflatten_flatten_map_either_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tflatten_flatten_map_either_nil_step tflatten_flatten_map_either_nil_fun_correctness.

  Definition tmap_map_compose_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvMap p1 (NRAEnvMap p2 p3) ⇒ NRAEnvMap (NRAEnvApp p1 p2) p3
      | _ ⇒ p
    end.

  Lemma tmap_map_compose_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tmap_map_compose_fun p.

  Definition tmap_map_compose_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "map/map"
         "Fuses nested maps together"
         "tmap_map_compose_fun"
         tmap_map_compose_fun .

  Definition tmap_map_compose_step_correct {model:basic_model}
    := mkOptimizerStepModel tmap_map_compose_step tmap_map_compose_fun_correctness.

  Definition tmap_singleton_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvMap p1 (NRAEnvUnop AColl p2) ⇒ NRAEnvUnop AColl (NRAEnvApp p1 p2)
      | _ ⇒ p
    end.

  Lemma tmap_singleton_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tmap_singleton_fun p.

  Definition tmap_singleton_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "map/coll"
         "Lowers a map over a bag constructor"
         "tmap_singleton_fun"
         tmap_singleton_fun .

  Definition tmap_singleton_step_correct {model:basic_model}
    := mkOptimizerStepModel tmap_singleton_step tmap_singleton_fun_correctness.

  Definition tapp_over_id_r_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvApp p NRAEnvID ⇒ p
      | _ ⇒ p
    end.

  Lemma tapp_over_id_r_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tapp_over_id_r_fun p.

  Definition tapp_over_id_r_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app/id arg"
         "Simplifies application to ID"
         "tapp_over_id_r_fun"
         tapp_over_id_r_fun .

  Definition tapp_over_id_r_step_correct {model:basic_model}
    := mkOptimizerStepModel tapp_over_id_r_step tapp_over_id_r_fun_correctness.

  Definition tapp_over_env_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvApp NRAEnvEnv p ⇒ NRAEnvEnv
      | _ ⇒ p
    end.

  Lemma tapp_over_env_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tapp_over_env_fun p.

  Definition tapp_over_env_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app/env body"
         "Simplify applications of ENV"
         "tapp_over_env_fun"
         tapp_over_env_fun .

  Definition tapp_over_env_step_correct {model:basic_model}
    := mkOptimizerStepModel tapp_over_env_step tapp_over_env_fun_correctness.

  Definition tapp_over_id_l_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvApp NRAEnvID p ⇒ p
      | _ ⇒ p
    end.

  Lemma tapp_over_id_l_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tapp_over_id_l_fun p.

  Definition tapp_over_id_l_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app/id body"
         "Simplify applications of ID"
         "tapp_over_id_l_fun"
         tapp_over_id_l_fun .

  Definition tapp_over_id_l_step_correct {model:basic_model}
    := mkOptimizerStepModel tapp_over_id_l_step tapp_over_id_l_fun_correctness.

  Definition tapp_over_ignoreid_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
    | NRAEnvApp p1 p2 ⇒
      if (nraenv_ignores_id_fun p1)
      then p1 else p
    | _ ⇒ p
    end.

  Lemma tapp_over_ignoreid_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tapp_over_ignoreid_fun p.

  Definition tapp_over_ignoreid_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app/ignore-id body"
         "Simplify application of expressions that ignore ID"
         "tapp_over_ignoreid_fun"
         tapp_over_ignoreid_fun .

  Definition tapp_over_ignoreid_step_correct {model:basic_model}
    := mkOptimizerStepModel tapp_over_ignoreid_step tapp_over_ignoreid_fun_correctness.

  Definition tappenv_over_env_l_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvAppEnv NRAEnvEnv p ⇒ p
      | _ ⇒ p
    end.

  Lemma tappenv_over_env_l_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tappenv_over_env_l_fun p.

  Definition tappenv_over_env_l_step {fruntime:foreign_runtime}
      := mkOptimizerStep
         "app-env/env body"
         "Simplify environment applications of the environment"
         "tappenv_over_env_l_fun"
         tappenv_over_env_l_fun .

  Definition tappenv_over_env_l_step_correct {model:basic_model}
    := mkOptimizerStepModel tappenv_over_env_l_step tappenv_over_env_l_fun_correctness.

  Definition tappenv_over_env_r_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvAppEnv p NRAEnvEnv ⇒ p
      | _ ⇒ p
    end.

  Lemma tappenv_over_env_r_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tappenv_over_env_r_fun p.

  Definition tappenv_over_env_r_step {fruntime:foreign_runtime}
      := mkOptimizerStep
         "app-env/env arg"
         "Simplify environment applications to the environment"
         "tappenv_over_env_r_fun"
         tappenv_over_env_r_fun .

  Definition tappenv_over_env_r_step_correct {model:basic_model}
    := mkOptimizerStepModel tappenv_over_env_r_step tappenv_over_env_r_fun_correctness.

  Definition tappenv_over_ignoreenv_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
    | NRAEnvAppEnv p1 p2 ⇒
      if (nraenv_ignores_env_fun p1)
      then p1 else p
    | _ ⇒ p
    end.

  Lemma tappenv_over_ignoreenv_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tappenv_over_ignoreenv_fun p.

  Definition tappenv_over_ignoreenv_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/ignore-env arg"
         "Simplify environment applications that ignore the environment"
         "tappenv_over_ignoreenv_fun"
         tappenv_over_ignoreenv_fun .

  Definition tappenv_over_ignoreenv_step_correct {model:basic_model}
    := mkOptimizerStepModel tappenv_over_ignoreenv_step tappenv_over_ignoreenv_fun_correctness.

  Definition tapp_over_app_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvApp (NRAEnvApp p1 p2) p3 ⇒
        NRAEnvApp p1 (NRAEnvApp p2 p3)
      | _ ⇒ p
    end.

  Lemma tapp_over_app_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tapp_over_app_fun p.

  Definition tapp_over_app_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app/app"
         "Reorder nested applications"
         "tapp_over_app_fun"
         tapp_over_app_fun .

  Definition tapp_over_app_step_correct {model:basic_model}
    := mkOptimizerStepModel tapp_over_app_step tapp_over_app_fun_correctness.

  Definition tappenv_over_appenv_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvAppEnv (NRAEnvAppEnv p1 p2) p3 ⇒
        NRAEnvAppEnv p1 (NRAEnvAppEnv p2 p3)
      | _ ⇒ p
    end.

  Lemma tappenv_over_appenv_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tappenv_over_appenv_fun p.

   Definition tappenv_over_appenv_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/app-env"
         "Reorder nested environment applications"
         "tappenv_over_appenv_fun"
         tappenv_over_appenv_fun .

  Definition tappenv_over_appenv_step_correct {model:basic_model}
    := mkOptimizerStepModel tappenv_over_appenv_step tappenv_over_appenv_fun_correctness.

  Definition tappenv_over_app_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvAppEnv (NRAEnvApp p1 p2) p3 ⇒
        if (nraenv_ignores_env_fun p1) then
          NRAEnvApp p1(NRAEnvAppEnv p2 p3)
        else if (nraenv_ignores_id_fun p3) then
        NRAEnvApp (NRAEnvAppEnv p1 p3) (NRAEnvAppEnv p2 p3)
      else p
    | _ ⇒ p
    end.

  Lemma tappenv_over_app_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tappenv_over_app_fun p.


    Definition tappenv_over_app_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/app body"
         "Push environment application through application"
         "tappenv_over_app_fun"
         tappenv_over_app_fun .

  Definition tappenv_over_app_step_correct {model:basic_model}
    := mkOptimizerStepModel tappenv_over_app_step tappenv_over_app_fun_correctness.

  Definition tapp_over_appenv_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
    | NRAEnvApp (NRAEnvAppEnv p1 p2) p3 ⇒
      if (nraenv_ignores_id_fun p1) then
        NRAEnvAppEnv p1 (NRAEnvApp p2 p3)
      else p
    | _ ⇒ p
    end.

  Lemma tapp_over_appenv_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tapp_over_appenv_fun p.

  Definition tapp_over_appenv_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app/app-env body"
         "Push application through environment application"
         "tapp_over_appenv_fun"
         tapp_over_appenv_fun .

  Definition tapp_over_appenv_step_correct {model:basic_model}
    := mkOptimizerStepModel tapp_over_appenv_step tapp_over_appenv_fun_correctness.

  Definition tapp_over_unop_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvApp (NRAEnvUnop u p1) p2 ⇒
        NRAEnvUnop u (NRAEnvApp p1 p2)
      | _ ⇒ p
    end.

  Lemma tapp_over_unop_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tapp_over_unop_fun p.

  Definition tapp_over_unop_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app/unop"
         "Push application through unary operations"
         "tapp_over_unop_fun"
         tapp_over_unop_fun .

  Definition tapp_over_unop_step_correct {model:basic_model}
    := mkOptimizerStepModel tapp_over_unop_step tapp_over_unop_fun_correctness.

  Definition tappenv_over_unop_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvAppEnv (NRAEnvUnop u p1) p2 ⇒
        NRAEnvUnop u (NRAEnvAppEnv p1 p2)
      | _ ⇒ p
    end.

  Lemma tappenv_over_unop_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tappenv_over_unop_fun p.

  Definition tappenv_over_unop_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/unop"
         "Push environment application through unary operations"
         "tappenv_over_unop_fun"
         tappenv_over_unop_fun .

  Definition tappenv_over_unop_step_correct {model:basic_model}
    := mkOptimizerStepModel tappenv_over_unop_step tappenv_over_unop_fun_correctness.

  Definition tunop_over_either_const_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvUnop u (NRAEnvEither p₁ (NRAEnvConst d)) ⇒ NRAEnvEither (NRAEnvUnop u p₁) (NRAEnvUnop u (NRAEnvConst d))
      | _ ⇒ p
    end.

  Lemma tunop_over_either_const_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tunop_over_either_const_fun p.

  Definition tunop_over_either_const_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "unop/either/const right"
         "Push a unary operation through an either construct with a right branch that builds a constant"
         "tunop_over_either_const_fun"
         tunop_over_either_const_fun .

  Definition tunop_over_either_const_step_correct {model:basic_model}
    := mkOptimizerStepModel tunop_over_either_const_step tunop_over_either_const_fun_correctness.

  Definition tunop_over_either_const_app_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
    | NRAEnvUnop u (NRAEnvApp (NRAEnvEither p₁ (NRAEnvConst d)) p₃) ⇒
      NRAEnvApp (NRAEnvEither (NRAEnvUnop u p₁) (NRAEnvUnop u (NRAEnvConst d))) p₃
    | _ ⇒ p
    end.

  Lemma tunop_over_either_const_app_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tunop_over_either_const_app_fun p.

  Definition tunop_over_either_const_app_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "unop/app/either/const right"
         "Push a unary operation through an application of an either construct with a right branch that builds a constant"
         "tunop_over_either_const_app_fun"
         tunop_over_either_const_app_fun .

  Definition tunop_over_either_const_app_step_correct {model:basic_model}
    := mkOptimizerStepModel tunop_over_either_const_app_step tunop_over_either_const_app_fun_correctness.

  Definition tapp_over_map_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvApp (NRAEnvMap p1 p2) p0 ⇒
        NRAEnvMap p1 (NRAEnvApp p2 p0)
      | _ ⇒ p
    end.

  Lemma tapp_over_map_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tapp_over_map_fun p.

  Definition tapp_over_map_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app/map"
         "Push applications through map a body"
         "tapp_over_map_fun"
         tapp_over_map_fun .

  Definition tapp_over_map_step_correct {model:basic_model}
    := mkOptimizerStepModel tapp_over_map_step tapp_over_map_fun_correctness.


  Definition tapp_over_mapconcat_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvApp (NRAEnvMapConcat p1 p2) p0 ⇒
        NRAEnvMapConcat p1 (NRAEnvApp p2 p0)
      | _ ⇒ p
    end.

  Lemma tapp_over_mapconcat_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tapp_over_mapconcat_fun p.

  Definition tapp_over_mapconcat_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app/map-concat"
         "Push application through a map-concat body"
         "tapp_over_mapconcat_fun"
         tapp_over_mapconcat_fun .

  Definition tapp_over_mapconcat_step_correct {model:basic_model}
    := mkOptimizerStepModel tapp_over_mapconcat_step tapp_over_mapconcat_fun_correctness.


  Definition tapp_over_product_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvApp (NRAEnvProduct p1 p2) p0 ⇒
        NRAEnvProduct (NRAEnvApp p1 p0) (NRAEnvApp p2 p0)
      | _ ⇒ p
    end.

  Lemma tapp_over_product_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tapp_over_product_fun p.

  Definition tapp_over_product_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app/product"
         "Push application through a product body"
         "tapp_over_product_fun"
         tapp_over_product_fun .

  Definition tapp_over_product_step_correct {model:basic_model}
    := mkOptimizerStepModel tapp_over_product_step tapp_over_product_fun_correctness.


  Definition tappenv_over_map_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvAppEnv (NRAEnvMap p1 p2) p0 ⇒
        if (nraenv_ignores_id_fun p0)
        then NRAEnvMap (NRAEnvAppEnv p1 p0) (NRAEnvAppEnv p2 p0)
        else p
      | _ ⇒ p
    end.

  Lemma tappenv_over_map_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tappenv_over_map_fun p.

  Definition tappenv_over_map_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/map"
         "Push environment application through a map body"
         "tappenv_over_map_fun"
         tappenv_over_map_fun .

  Definition tappenv_over_map_step_correct {model:basic_model}
    := mkOptimizerStepModel tappenv_over_map_step tappenv_over_map_fun_correctness.


  Definition tappenv_over_select_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvAppEnv (NRAEnvSelect p1 p2) p0 ⇒
        if (nraenv_ignores_id_fun p0)
        then NRAEnvSelect (NRAEnvAppEnv p1 p0) (NRAEnvAppEnv p2 p0)
        else p
      | _ ⇒ p
    end.

  Lemma tappenv_over_select_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tappenv_over_select_fun p.

  Definition tappenv_over_select_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/select"
         "Push environment application through a selection body"
         "tappenv_over_select_fun"
         tappenv_over_select_fun .

  Definition tappenv_over_select_step_correct {model:basic_model}
    := mkOptimizerStepModel tappenv_over_select_step tappenv_over_select_fun_correctness.


  Definition tapp_over_select_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvApp (NRAEnvSelect p1 p2) p0 ⇒
        NRAEnvSelect p1 (NRAEnvApp p2 p0)
      | _ ⇒ p
    end.

  Lemma tapp_over_select_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tapp_over_select_fun p.

  Definition tapp_over_select_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app/slect"
         "Push application through a selection body"
         "tapp_over_select_fun"
         tapp_over_select_fun .

  Definition tapp_over_select_step_correct {model:basic_model}
    := mkOptimizerStepModel tapp_over_select_step tapp_over_select_fun_correctness.

  Definition tapp_over_binop_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvApp (NRAEnvBinop b p2 p3) p1 ⇒
        NRAEnvBinop b (NRAEnvApp p2 p1) (NRAEnvApp p3 p1)
      | _ ⇒ p
    end.

  Lemma tapp_over_binop_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tapp_over_binop_fun p.

  Definition tapp_over_binop_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app/binop"
         "Push application through binary operations"
         "tapp_over_binop_fun"
         tapp_over_binop_fun .

  Definition tapp_over_binop_step_correct {model:basic_model}
    := mkOptimizerStepModel tapp_over_binop_step tapp_over_binop_fun_correctness.

  Definition tproduct_singletons_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvProduct (NRAEnvUnop AColl (NRAEnvUnop (ARec s1) p1))
                  (NRAEnvUnop AColl (NRAEnvUnop (ARec s2) p2)) ⇒
        NRAEnvUnop AColl
               (NRAEnvBinop AConcat (NRAEnvUnop (ARec s1) p1) (NRAEnvUnop (ARec s2) p2))
      | _ ⇒ p
    end.

  Lemma tproduct_singletons_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tproduct_singletons_fun p.

  Definition tproduct_singletons_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "product/singleton singleton"
         "Simplify the product of two singRemove loop comprehensions over empty loops"
         "tproduct_singletons_fun"
         tproduct_singletons_fun .

  Definition tproduct_singletons_step_correct {model:basic_model}
    := mkOptimizerStepModel tproduct_singletons_step tproduct_singletons_fun_correctness.

  Definition tproduct_empty_right_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
    | NRAEnvProduct p1 (NRAEnvUnop AColl (NRAEnvConst (drec nil))) ⇒ p1
    | _ ⇒ p
    end.

  Lemma tproduct_empty_right_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tproduct_empty_right_fun p.

  Definition tproduct_empty_right_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "product singleton right"
         "Eliminates empty table on the right of a Cartesian product"
         "tproduct_empty_right_fun"
         tproduct_empty_right_fun .

  Definition tproduct_empty_right_step_correct {model:basic_model}
    := mkOptimizerStepModel tproduct_empty_right_step tproduct_empty_right_fun_correctness.

  Definition tproduct_empty_left_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
    | NRAEnvProduct (NRAEnvUnop AColl (NRAEnvConst (drec nil))) p1 ⇒ p1
    | _ ⇒ p
    end.

  Lemma tproduct_empty_left_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tproduct_empty_left_fun p.

  Definition tproduct_empty_left_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "product singleton left"
         "Eliminates empty table on the left of a Cartesian product"
         "tproduct_empty_left_fun"
         tproduct_empty_left_fun .

  Definition tproduct_empty_left_step_correct {model:basic_model}
    := mkOptimizerStepModel tproduct_empty_left_step tproduct_empty_left_fun_correctness.

  Definition tdouble_flatten_map_coll_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvUnop AFlatten
               (NRAEnvMap (NRAEnvMap (NRAEnvUnop AColl p3) p1) p2) ⇒
        NRAEnvMap (NRAEnvUnop AColl p3)
              (NRAEnvUnop AFlatten (NRAEnvMap p1 p2))
      | _ ⇒ p
    end.

  Lemma tdouble_flatten_map_coll_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tdouble_flatten_map_coll_fun p.

    Definition tdouble_flatten_map_coll_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "flatten/map/map/coll"
         "Simplify flattenging the map of the map of a bag constructor"
         "tdouble_flatten_map_coll_fun"
         tdouble_flatten_map_coll_fun .

  Definition tdouble_flatten_map_coll_step_correct {model:basic_model}
    := mkOptimizerStepModel tdouble_flatten_map_coll_step tdouble_flatten_map_coll_fun_correctness.

  Definition tflatten_over_double_map_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | (NRAEnvUnop AFlatten
                (NRAEnvMap (NRAEnvMap q₁ (NRAEnvSelect q₂ (NRAEnvUnop AColl NRAEnvID))) q₃))
        ⇒ (NRAEnvMap q₁ (NRAEnvSelect q₂ q₃))
      | _ ⇒ p
    end.

  Lemma tflatten_over_double_map_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tflatten_over_double_map_fun p.

  Definition tflatten_over_double_map_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "flatten/map/map/select"
         "Simplify flatten of a map over a map of a selection applied to a bag constructor of the input"
         "tflatten_over_double_map_fun"
         tflatten_over_double_map_fun .

  Definition tflatten_over_double_map_step_correct {model:basic_model}
    := mkOptimizerStepModel tflatten_over_double_map_step tflatten_over_double_map_fun_correctness.

  Definition tflatten_over_double_map_with_either_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
    | (NRAEnvUnop AFlatten
              (NRAEnvMap
                 (NRAEnvMap q₁
                        (NRAEnvSelect q₂
                                  (NRAEnvApp
                                     (NRAEnvEither (NRAEnvUnop AColl NRAEnvID) (NRAEnvConst (dcoll []))) q₃)))
                 q₄)) ⇒
      (NRAEnvMap q₁
             (NRAEnvSelect q₂
                       (NRAEnvUnop AFlatten
                               (NRAEnvMap
                                  (NRAEnvApp
                                     (NRAEnvEither (NRAEnvUnop AColl NRAEnvID) (NRAEnvConst (dcoll []))) q₃)
                                  q₄))))
    | _ ⇒ p
    end.

  Lemma tflatten_over_double_map_with_either_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tflatten_over_double_map_with_either_fun p.

  Definition tflatten_over_double_map_with_either_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "flatten/map/map/select/app/either"
         "???"
         "tflatten_over_double_map_with_either_fun"
         tflatten_over_double_map_with_either_fun .

  Definition tflatten_over_double_map_with_either_step_correct {model:basic_model}
    := mkOptimizerStepModel tflatten_over_double_map_with_either_step tflatten_over_double_map_with_either_fun_correctness.

  Definition tappenv_over_env_merge_l_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvAppEnv (NRAEnvBinop AMergeConcat NRAEnvEnv p1) p2 ⇒
        if (nraenv_ignores_env_fun p1)
        then (NRAEnvBinop AMergeConcat p2 p1)
        else p
      | _ ⇒ p
    end.

  Lemma tappenv_over_env_merge_l_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tappenv_over_env_merge_l_fun p.

  Definition tappenv_over_env_merge_l_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/merge-concat/env left"
         "Simplify environment application of a merge-concat where the left part is ENV and the right part ignores the environment"
         "tappenv_over_env_merge_l_fun"
         tappenv_over_env_merge_l_fun .

  Definition tappenv_over_env_merge_l_step_correct {model:basic_model}
    := mkOptimizerStepModel tappenv_over_env_merge_l_step tappenv_over_env_merge_l_fun_correctness.

  Definition ttostring_on_string_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvUnop AToString (NRAEnvConst (dstring s)) ⇒
        NRAEnvConst (dstring s)
      | NRAEnvUnop AToString (NRAEnvUnop AToString p) ⇒
        NRAEnvUnop AToString p
      | NRAEnvUnop AToString (NRAEnvBinop ASConcat p1 p2) ⇒
        (NRAEnvBinop ASConcat p1 p2)
      | _ ⇒ p
    end.

  Lemma ttostring_on_string_fun_correctness {model:basic_model} (p: nraenv) :
    p ⇒ₓ ttostring_on_string_fun p.

  Definition ttostring_on_string_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "to-string/string"
         "Remove ToString operations where the argument is statically known to already be a string"
         "ttostring_on_string_fun"
         ttostring_on_string_fun .

  Definition ttostring_on_string_step_correct {model:basic_model}
    := mkOptimizerStepModel ttostring_on_string_step ttostring_on_string_fun_correctness.

  Definition tmap_full_over_select_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvMap p0 (NRAEnvSelect p1 (NRAEnvUnop AColl NRAEnvID)) ⇒ p
      | NRAEnvMap p0 (NRAEnvSelect p1 (NRAEnvUnop AColl p2)) ⇒
        NRAEnvMap (NRAEnvApp p0 p2) (NRAEnvSelect (NRAEnvApp p1 p2) (NRAEnvUnop AColl NRAEnvID))
      | _ ⇒ p
    end.

  Lemma tmap_full_over_select_fun_correctness {model:basic_model} (p: nraenv) :
    p ⇒ₓ tmap_full_over_select_fun p.

  Definition tmap_full_over_select_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "map/select/coll"
         "???"
         "tmap_full_over_select_fun"
         tmap_full_over_select_fun .

  Definition tmap_full_over_select_step_correct {model:basic_model}
    := mkOptimizerStepModel tmap_full_over_select_step tmap_full_over_select_fun_correctness.

  Definition tcompose_selects_in_mapenv_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | (NRAEnvAppEnv
           (NRAEnvUnop AFlatten
                   (NRAEnvMapEnv (NRAEnvMap NRAEnvEnv (NRAEnvSelect p1 (NRAEnvUnop AColl NRAEnvID)))))
           (NRAEnvMap NRAEnvEnv (NRAEnvSelect p2 (NRAEnvUnop AColl NRAEnvID)))) ⇒
        (NRAEnvMap NRAEnvEnv (NRAEnvSelect p1 (NRAEnvSelect p2 (NRAEnvUnop AColl NRAEnvID))))
      | _ ⇒ p
    end.

  Lemma tcompose_selects_in_mapenv_fun_correctness {model:basic_model} (p: nraenv) :
    p ⇒ₓ tcompose_selects_in_mapenv_fun p.

  Definition tcompose_selects_in_mapenv_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/flatten/map-env/map/select/coll/id"
         "???"
         "tcompose_selects_in_mapenv_fun"
         tcompose_selects_in_mapenv_fun .

  Definition tcompose_selects_in_mapenv_step_correct {model:basic_model}
    := mkOptimizerStepModel tcompose_selects_in_mapenv_step tcompose_selects_in_mapenv_fun_correctness.

  Definition tmapenv_to_env_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
      | (NRAEnvApp (NRAEnvMapEnv NRAEnvEnv) p1) ⇒ NRAEnvEnv
      | _ ⇒ p
    end.

  Lemma tmapenv_to_env_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tmapenv_to_env_fun p.

  Definition tmapenv_to_env_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app/map-env/env"
         "Simplify applications with body that map-environments over the environment"
         "tmapenv_to_env_fun"
         tmapenv_to_env_fun .

  Definition tmapenv_to_env_step_correct {model:basic_model}
    := mkOptimizerStepModel tmapenv_to_env_step tmapenv_to_env_fun_correctness.

  Definition tenv_appenv_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvAppEnv NRAEnvEnv p1 ⇒ p1
      | _ ⇒ p
    end.

  Lemma tenv_appenv_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tenv_appenv_fun p.

  Definition tenv_appenv_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/env"
         "Simplifies environment applications of the environment"
         "tenv_appenv_fun"
         tenv_appenv_fun .

  Definition tenv_appenv_step_correct {model:basic_model}
    := mkOptimizerStepModel tenv_appenv_step tenv_appenv_fun_correctness.

  Definition tflatten_mapenv_coll_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
      | NRAEnvUnop AFlatten (NRAEnvMapEnv (NRAEnvUnop AColl p1)) ⇒
        NRAEnvMapEnv p1
      | _ ⇒ p
    end.

  Lemma tflatten_mapenv_coll_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tflatten_mapenv_coll_fun p.

  Definition tflatten_mapenv_coll_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "flatten/map-env/coll"
         "Simplify flattening a map environment of a bag constructor"
         "tflatten_mapenv_coll_fun"
         tflatten_mapenv_coll_fun .

  Definition tflatten_mapenv_coll_step_correct {model:basic_model}
    := mkOptimizerStepModel tflatten_mapenv_coll_step tflatten_mapenv_coll_fun_correctness.

  Definition tflatten_nil_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
      | NRAEnvUnop AFlatten (NRAEnvConst (dcoll nil)) ⇒
        NRAEnvConst (dcoll nil)
      | _ ⇒ p
    end.

  Lemma tflatten_nil_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tflatten_nil_fun p.

  Definition tflatten_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "flatten/nil"
         "Remove flatten over empty records"
         "tflatten_nil_fun"
         tflatten_nil_fun .

  Definition tflatten_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tflatten_nil_step tflatten_nil_fun_correctness.

  Definition tflatten_through_appenv_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvUnop AFlatten (NRAEnvAppEnv p1 p2) ⇒
        NRAEnvAppEnv (NRAEnvUnop AFlatten p1) p2
      | _ ⇒ p
    end.

  Lemma tflatten_through_appenv_fun_correctness {model:basic_model} (p: nraenv) :
    p ⇒ₓ tflatten_through_appenv_fun p.

  Definition tflatten_through_appenv_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "flatten/app-env"
         "Push flatten operations through environment applications"
         "tflatten_through_appenv_fun"
         tflatten_through_appenv_fun .

  Definition tflatten_through_appenv_step_correct {model:basic_model}
    := mkOptimizerStepModel tflatten_through_appenv_step tflatten_through_appenv_fun_correctness.

  Definition tappenv_flatten_mapenv_to_map_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | (NRAEnvAppEnv (NRAEnvUnop AFlatten (NRAEnvMapEnv p2))
            (NRAEnvBinop AMergeConcat NRAEnvEnv (NRAEnvUnop (ARec s) NRAEnvID))) ⇒
         (NRAEnvUnop AFlatten
            (NRAEnvMap (NRAEnvAppEnv (NRAEnvApp p2 (NRAEnvUnop (ADot s) NRAEnvEnv)) NRAEnvID)
                   (NRAEnvBinop AMergeConcat NRAEnvEnv (NRAEnvUnop (ARec s) NRAEnvID))))
      | _ ⇒ p
    end.

  Lemma tappenv_flatten_mapenv_to_map_fun_correctness {model:basic_model} (p: nraenv) :
    p ⇒ₓ tappenv_flatten_mapenv_to_map_fun p.

  Definition tappenv_flatten_mapenv_to_map_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/(flatten/map-env)(merge-concat/(env)(rec/id))"
         "Simplify environment application of a flattened environment map to a merge-concat of the environment with a record constructor"
         "tappenv_flatten_mapenv_to_map_fun"
         tappenv_flatten_mapenv_to_map_fun .

  Definition tappenv_flatten_mapenv_to_map_step_correct {model:basic_model}
    := mkOptimizerStepModel tappenv_flatten_mapenv_to_map_step tappenv_flatten_mapenv_to_map_fun_correctness.

  Definition tselect_over_either_nil_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
    | NRAEnvSelect p₁ (NRAEnvEither p₂ (NRAEnvConst (dcoll nil))) ⇒
      NRAEnvEither (NRAEnvSelect p₁ (p₂)) (NRAEnvConst (dcoll nil))
    | _ ⇒ p
    end.

  Lemma tselect_over_either_nil_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tselect_over_either_nil_fun p.


  Definition tselect_over_either_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "select/either/nil right"
         "Push selection through an either whose right side returns an empty bag"
         "tselect_over_either_nil_fun"
         tselect_over_either_nil_fun .

  Definition tselect_over_either_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tselect_over_either_nil_step tselect_over_either_nil_fun_correctness.

  Definition tselect_over_either_nil_app_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
    | NRAEnvSelect p₁ (NRAEnvApp (NRAEnvEither p₂ (NRAEnvConst (dcoll nil))) p₄) ⇒
      NRAEnvApp (NRAEnvEither (NRAEnvSelect p₁ p₂) ((NRAEnvConst (dcoll nil)))) p₄
    | _ ⇒ p
    end.

  Lemma tselect_over_either_nil_app_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tselect_over_either_nil_app_fun p.


  Definition tselect_over_either_nil_app_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "select/app/either/nil right"
         "Push selection through an application of an either whose right side returns an empty bag"
         "tselect_over_either_nil_app_fun"
         tselect_over_either_nil_app_fun .

  Definition tselect_over_either_nil_app_step_correct {model:basic_model}
    := mkOptimizerStepModel tselect_over_either_nil_app_step tselect_over_either_nil_app_fun_correctness.

  Definition tmap_over_either_nil_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
    | NRAEnvMap p₁ (NRAEnvEither p₂ (NRAEnvConst (dcoll nil))) ⇒
      NRAEnvEither (NRAEnvMap p₁ p₂) ((NRAEnvConst (dcoll nil)))
    | _ ⇒ p
    end.

  Lemma tmap_over_either_nil_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tmap_over_either_nil_fun p.


  Definition tmap_over_either_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "map/either/nil right"
         "Push map through an either whose right side returns an empty bag"
         "tmap_over_either_nil_fun"
         tmap_over_either_nil_fun .

  Definition tmap_over_either_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tmap_over_either_nil_step tmap_over_either_nil_fun_correctness.

  Definition tmap_over_either_nil_app_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
    | NRAEnvMap p₁ (NRAEnvApp (NRAEnvEither p₂ (NRAEnvConst (dcoll nil))) p₄) ⇒
      NRAEnvApp (NRAEnvEither (NRAEnvMap p₁ p₂) (NRAEnvConst (dcoll nil))) p₄
    | _ ⇒ p
    end.

  Lemma tmap_over_either_nil_app_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tmap_over_either_nil_app_fun p.


  Definition tmap_over_either_nil_app_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "map/app/either/nil right"
         "Push map through an application of an either whose right side returns an empty bag"
         "tmap_over_either_nil_app_fun"
         tmap_over_either_nil_app_fun .

  Definition tmap_over_either_nil_app_step_correct {model:basic_model}
    := mkOptimizerStepModel tmap_over_either_nil_app_step tmap_over_either_nil_app_fun_correctness.

  Definition tappenv_over_either_nil_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
      | NRAEnvAppEnv (NRAEnvEither p₂ (NRAEnvConst (dcoll nil))) p₃ ⇒
        if nraenv_ignores_id_fun p₃
        then NRAEnvEither (NRAEnvAppEnv p₂ p₃) ((NRAEnvConst (dcoll nil)))
        else p
      | _ ⇒ p
    end.

  Lemma tappenv_over_either_nil_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tappenv_over_either_nil_fun p.


    Definition tappenv_over_either_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/either/nil right"
         "Pushes environment application through an either with a right branch that builds an empty bag"
         "tappenv_over_either_nil_fun"
         tappenv_over_either_nil_fun .

  Definition tappenv_over_either_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tappenv_over_either_nil_step tappenv_over_either_nil_fun_correctness.

  Definition tselect_over_flatten_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
    | NRAEnvSelect p₁ (NRAEnvUnop AFlatten p₂) ⇒
      NRAEnvUnop AFlatten (NRAEnvMap (NRAEnvSelect p₁ NRAEnvID) p₂)
    | _ ⇒ p
    end.

  Lemma tselect_over_flatten_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tselect_over_flatten_fun p.


  Definition tselect_over_flatten_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "select/flatten"
         "Pushes selection through a flatten operation"
         "tselect_over_flatten_fun"
         tselect_over_flatten_fun .

  Definition tselect_over_flatten_step_correct {model:basic_model}
    := mkOptimizerStepModel tselect_over_flatten_step tselect_over_flatten_fun_correctness.

  Definition tmap_over_flatten_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
    | NRAEnvMap p₁ (NRAEnvUnop AFlatten p₂) ⇒
      NRAEnvUnop AFlatten (NRAEnvMap (NRAEnvMap p₁ NRAEnvID) p₂)
    | _ ⇒ p
    end.

  Lemma tmap_over_flatten_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tmap_over_flatten_fun p.


  Definition tmap_over_flatten_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "map/flatten"
         "Pushes map through a flatten operation"
         "tmap_over_flatten_fun"
         tmap_over_flatten_fun .

  Definition tmap_over_flatten_step_correct {model:basic_model}
    := mkOptimizerStepModel tmap_over_flatten_step tmap_over_flatten_fun_correctness.

  Definition tmap_over_flatten_map_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
    | NRAEnvMap p₁ (NRAEnvUnop AFlatten (NRAEnvMap p₂ p₃)) ⇒
      NRAEnvUnop AFlatten (NRAEnvMap (NRAEnvMap p₁ p₂) p₃)
      | _ ⇒ p
    end.

  Lemma tmap_over_flatten_map_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tmap_over_flatten_map_fun p.


  Definition tmap_over_flatten_map_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "map/flatten/map"
         "Pushes map through a flatten of a map"
         "tmap_over_flatten_map_fun"
         tmap_over_flatten_map_fun .

  Definition tmap_over_flatten_map_step_correct {model:basic_model}
    := mkOptimizerStepModel tmap_over_flatten_map_step tmap_over_flatten_map_fun_correctness.

  Definition tconcat_over_rec_eq_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
      | (NRAEnvBinop AConcat
                 (NRAEnvUnop (ARec s₁) p₁) (NRAEnvUnop (ARec s₂) p₂))
        ⇒ if string_dec s₁ s₂
           then (NRAEnvUnop (ARec s₂) p₂)
           else p
      | _ ⇒ p
    end.

  Definition tconcat_over_rec_eq_fun_correctness {model:basic_model} p :
    p ⇒ₓ tconcat_over_rec_eq_fun p.


  Definition tconcat_over_rec_eq_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "concat/(rec)(rec)"
         "Simplifies a concatentation of two record constructors"
         "tconcat_over_rec_eq_fun"
         tconcat_over_rec_eq_fun .

  Definition tconcat_over_rec_eq_step_correct {model:basic_model}
    := mkOptimizerStepModel tconcat_over_rec_eq_step tconcat_over_rec_eq_fun_correctness.

  Definition tapp_over_const_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        (NRAEnvApp (NRAEnvConst d) p1) ⇒ (NRAEnvConst d)
      | _ ⇒ p
    end.

  Lemma tapp_over_const_fun_correctness {model:basic_model} (p: nraenv) :
    p ⇒ₓ tapp_over_const_fun p.

  Definition tapp_over_const_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app/const"
         "Simplifies application of a constant"
         "tapp_over_const_fun"
         tapp_over_const_fun .

  Definition tapp_over_const_step_correct {model:basic_model}
    := mkOptimizerStepModel tapp_over_const_step tapp_over_const_fun_correctness.

  Definition tappenv_over_const_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        (NRAEnvAppEnv (NRAEnvConst d) p1) ⇒ (NRAEnvConst d)
      | _ ⇒ p
    end.

  Lemma tappenv_over_const_fun_correctness {model:basic_model} (p: nraenv) :
    p ⇒ₓ tappenv_over_const_fun p.

  Definition tappenv_over_const_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/const"
         "Simplifies environment application of a constant"
         "tappenv_over_const_fun"
         tappenv_over_const_fun .

  Definition tappenv_over_const_step_correct {model:basic_model}
    := mkOptimizerStepModel tappenv_over_const_step tappenv_over_const_fun_correctness.

  Definition tflip_env1_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
    | NRAEnvAppEnv (NRAEnvMap NRAEnvEnv (NRAEnvSelect q₁ (NRAEnvUnop AColl NRAEnvID))) q₂ ⇒
      match q₂ with
      | NRAEnvID ⇒ (NRAEnvAppEnv (NRAEnvSelect q₁ (NRAEnvUnop AColl NRAEnvID)) NRAEnvID)
      | _ ⇒
        if (nraenv_ignores_env_fun q₁)
        then NRAEnvMap q₂ (NRAEnvSelect q₁ (NRAEnvUnop AColl NRAEnvID))
        else p
      end
    | _ ⇒ p
    end.

  Lemma tflip_env1_fun_correctness {model:basic_model} (p: nraenv) :
    p ⇒ₓ tflip_env1_fun p.

  Definition tflip_env1_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "env flip1"
         "???"
         "tflip_env1_fun"
         tflip_env1_fun .

  Definition tflip_env1_step_correct {model:basic_model}
    := mkOptimizerStepModel tflip_env1_step tflip_env1_fun_correctness.

  Definition tflip_env2_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      (NRAEnvAppEnv (NRAEnvSelect p (NRAEnvUnop AColl NRAEnvID)) NRAEnvID) ⇒
      (NRAEnvSelect (NRAEnvAppEnv p NRAEnvID) (NRAEnvUnop AColl NRAEnvID))
    | _ ⇒ p
    end.

  Lemma tflip_env2_fun_correctness {model:basic_model} (p: nraenv) :
    p ⇒ₓ tflip_env2_fun p.

  Definition tflip_env2_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/select/coll/id"
         "Pushes environment application through selection of a bag constructor over the input"
         "tflip_env2_fun"
         tflip_env2_fun .

  Definition tflip_env2_step_correct {model:basic_model}
    := mkOptimizerStepModel tflip_env2_step tflip_env2_fun_correctness.

  Definition tmapenv_over_singleton_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      (NRAEnvAppEnv (NRAEnvMapEnv p1) (NRAEnvUnop AColl p2)) ⇒
      (NRAEnvUnop AColl (NRAEnvAppEnv p1 p2))
    | _ ⇒ p
    end.

  Lemma tmapenv_over_singleton_fun_correctness {model:basic_model} (p: nraenv) :
    p ⇒ₓ tmapenv_over_singleton_fun p.

    Definition tmapenv_over_singleton_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/(map-env)(coll)"
         "Simplifies the environment application of a map environment over a bag constructor"
         "tmapenv_over_singleton_fun"
         tmapenv_over_singleton_fun .

  Definition tmapenv_over_singleton_step_correct {model:basic_model}
    := mkOptimizerStepModel tmapenv_over_singleton_step tmapenv_over_singleton_fun_correctness.

  Definition tappenv_over_binop_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        (NRAEnvAppEnv (NRAEnvBinop b p1 p2) p0) ⇒
         (NRAEnvBinop b (NRAEnvAppEnv p1 p0) (NRAEnvAppEnv p2 p0))
      | _ ⇒ p
    end.

  Lemma tappenv_over_binop_fun_correctness {model:basic_model} (p: nraenv) :
    p ⇒ₓ tappenv_over_binop_fun p.

  Definition tappenv_over_binop_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/binop"
         "Pushes an environment application through a binary operation"
         "tappenv_over_binop_fun"
         tappenv_over_binop_fun .

  Definition tappenv_over_binop_step_correct {model:basic_model}
    := mkOptimizerStepModel tappenv_over_binop_step tappenv_over_binop_fun_correctness.

  Definition tflip_env6_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
    | NRAEnvMap (NRAEnvBinop AMergeConcat NRAEnvEnv NRAEnvID)
                (NRAEnvSelect p1 (NRAEnvBinop AMergeConcat NRAEnvEnv p2)) ⇒
      NRAEnvMap (NRAEnvUnop AColl NRAEnvID)
                (NRAEnvSelect p1 (NRAEnvBinop AMergeConcat NRAEnvEnv p2))
    | _ ⇒ p
    end.

  Lemma tflip_env6_fun_correctness {model:basic_model} (p: nraenv) :
    p ⇒ₓ tflip_env6_fun p.

  Definition tflip_env6_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "env flip6"
         "???"
         "tflip_env6_fun"
         tflip_env6_fun .

  Definition tflip_env6_step_correct {model:basic_model}
    := mkOptimizerStepModel tflip_env6_step tflip_env6_fun_correctness.

  Definition tmapenv_to_map_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | (NRAEnvAppEnv (NRAEnvMapEnv p1) p2) ⇒
        if (nraenv_ignores_id_fun p1)
        then (NRAEnvMap (NRAEnvAppEnv p1 NRAEnvID) p2)
        else p
      | _ ⇒ p
    end.

  Lemma tmapenv_to_map_fun_correctness {model:basic_model} (p: nraenv) :
    p ⇒ₓ tmapenv_to_map_fun p.

  Definition tmapenv_to_map_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/map-env"
         "Push environment application through map environment"
         "tmapenv_to_map_fun"
         tmapenv_to_map_fun .

  Definition tmapenv_to_map_step_correct {model:basic_model}
    := mkOptimizerStepModel tmapenv_to_map_step tmapenv_to_map_fun_correctness.

  Definition tmerge_concat_to_concat_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
    | NRAEnvBinop AMergeConcat (NRAEnvUnop (ARec s1) p1) (NRAEnvUnop (ARec s2) p2) ⇒
      if (s1 == s2)
      then p
      else NRAEnvUnop AColl
                      (NRAEnvBinop AConcat
                                   (NRAEnvUnop (ARec s1) p1)
                                   (NRAEnvUnop (ARec s2) p2))
    | _ ⇒ p
    end.

  Lemma tmerge_concat_to_concat_fun_correctness {model:basic_model} (p: nraenv) :
    p ⇒ₓ tmerge_concat_to_concat_fun p.

  Definition tmerge_concat_to_concat_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "merge-concat/(rec)(rec)"
         "Simplifies a merge-concat of two record constructors into a simpler concatentation"
         "tmerge_concat_to_concat_fun"
         tmerge_concat_to_concat_fun .

  Definition tmerge_concat_to_concat_step_correct {model:basic_model}
    := mkOptimizerStepModel tmerge_concat_to_concat_step tmerge_concat_to_concat_fun_correctness.

  Definition tmerge_with_concat_to_concat_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
    | NRAEnvBinop AMergeConcat (NRAEnvUnop (ARec s1) p1)
                  (NRAEnvBinop AConcat (NRAEnvUnop (ARec s1') p1')
                               (NRAEnvUnop (ARec s2) p2)) ⇒
        if (s1 == s2)
        then p
        else
          if (s1 == s1')
          then
            if (p1 == p1')
            then NRAEnvUnop AColl (NRAEnvBinop AConcat
                                               (NRAEnvUnop (ARec s1) p1)
                                               (NRAEnvUnop (ARec s2) p2))
            else p
          else p
      | _ ⇒ p
    end.

  Lemma tmerge_with_concat_to_concat_fun_correctness {model:basic_model} (p: nraenv) :
    p ⇒ₓ tmerge_with_concat_to_concat_fun p.

  Definition tmerge_with_concat_to_concat_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "merge-concat/(rec)(concat(rec)(rec))"
         "Simplifies a merge concatenation of a record constructor and a concatenation of record constructors into a simpler concatenation"
         "tmerge_with_concat_to_concat_fun"
         tmerge_with_concat_to_concat_fun .

  Definition tmerge_with_concat_to_concat_step_correct {model:basic_model}
    := mkOptimizerStepModel tmerge_with_concat_to_concat_step tmerge_with_concat_to_concat_fun_correctness.

  Definition tdot_over_rec_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
    | NRAEnvUnop (ADot s2)
                 (NRAEnvUnop (ARec s1) p1) ⇒
      if (s1 == s2) then p1
      else p
    | _ ⇒ p
    end.

  Lemma tdot_over_rec_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tdot_over_rec_fun p.

  Definition tdot_over_rec_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "dot/rec"
         "Simplifies field lookup of a record construction"
         "tdot_over_rec_fun"
         tdot_over_rec_fun .

  Definition tdot_over_rec_step_correct {model:basic_model}
    := mkOptimizerStepModel tdot_over_rec_step tdot_over_rec_fun_correctness.

  Definition tnested_map_over_singletons_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
    | NRAEnvUnop AFlatten
                 (NRAEnvMap (NRAEnvSelect q₁ (NRAEnvUnop AColl q₂)) q₃) ⇒
      NRAEnvSelect q₁ (NRAEnvMap q₂ q₃)
    | _ ⇒ p
    end.

  Lemma tnested_map_over_singletons_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tnested_map_over_singletons_fun p.

  Definition tnested_map_over_singletons_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "flatten/map/select/coll"
         "Simplifies a flatten of a map of a select over a bag constructor"
         "tnested_map_over_singletons_fun"
         tnested_map_over_singletons_fun .

  Definition tnested_map_over_singletons_step_correct {model:basic_model}
    := mkOptimizerStepModel tnested_map_over_singletons_step tnested_map_over_singletons_fun_correctness.

  Definition tappenv_mapenv_to_map_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
    | NRAEnvAppEnv (NRAEnvMapEnv q)
                   (NRAEnvBinop AMergeConcat NRAEnvEnv (NRAEnvUnop (ARec a) NRAEnvID)) ⇒
      NRAEnvMap (NRAEnvAppEnv (NRAEnvApp q (NRAEnvUnop (ADot a) NRAEnvEnv)) NRAEnvID)
                (NRAEnvBinop AMergeConcat NRAEnvEnv (NRAEnvUnop (ARec a) NRAEnvID))
    | _ ⇒ p
    end.

  Lemma tappenv_mapenv_to_map_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tappenv_mapenv_to_map_fun p.

  Definition tappenv_mapenv_to_map_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "app-env/(map-env)(merge-concat(env)(rec/id))"
         "???"
         "tappenv_mapenv_to_map_fun"
         tappenv_mapenv_to_map_fun .

  Definition tappenv_mapenv_to_map_step_correct {model:basic_model}
    := mkOptimizerStepModel tappenv_mapenv_to_map_step tappenv_mapenv_to_map_fun_correctness.


   Definition trproject_nil_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
      | NRAEnvUnop (ARecProject nil) p₁
        ⇒ NRAEnvConst (drec nil)
      | _ ⇒ p
    end.

  Definition trproject_nil_fun_correctness {model:basic_model} p :
    p ⇒ₓ trproject_nil_fun p.


  Definition trproject_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "rproject/nil"
         "Remove record projection of an empty record"
         "trproject_nil_fun"
         trproject_nil_fun .

  Definition trproject_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel trproject_nil_step trproject_nil_fun_correctness.

  Definition trproject_over_const_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
      | NRAEnvUnop (ARecProject sl)
          (NRAEnvConst (drec l))
        ⇒ NRAEnvConst (drec (rproject l sl))
      | _ ⇒ p
    end.

  Definition trproject_over_const_fun_correctness {model:basic_model} p :
    p ⇒ₓ trproject_over_const_fun p.


  Definition trproject_over_const_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "rproject/const"
         "Simplify record projection of a constant record"
         "trproject_over_const_fun"
         trproject_over_const_fun .

  Definition trproject_over_const_step_correct {model:basic_model}
    := mkOptimizerStepModel trproject_over_const_step trproject_over_const_fun_correctness.

  Definition trproject_over_rec_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
      | NRAEnvUnop (ARecProject sl)
          (NRAEnvUnop (ARec s) p₁)
        ⇒ if in_dec string_dec s sl
           then NRAEnvUnop (ARec s) p₁
           else NRAEnvConst (drec nil)
      | _ ⇒ p
    end.

  Definition trproject_over_rec_fun_correctness {model:basic_model} p :
    p ⇒ₓ trproject_over_rec_fun p.


  Definition trproject_over_rec_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "rproject/rec"
         "Simplify record projection of a record construction"
         "trproject_over_rec_fun"
         trproject_over_rec_fun .

  Definition trproject_over_rec_step_correct {model:basic_model}
    := mkOptimizerStepModel trproject_over_rec_step trproject_over_rec_fun_correctness.

  Definition trproject_over_concat_r_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
      | NRAEnvUnop (ARecProject sl)
               (NRAEnvBinop AConcat
                        p₁ (NRAEnvUnop (ARec s) p₂))
        ⇒ if in_dec string_dec s sl
           then NRAEnvBinop AConcat
                        (NRAEnvUnop (ARecProject (remove string_dec s sl)) p₁)
                        (NRAEnvUnop (ARec s) p₂)
           else (NRAEnvUnop (ARecProject sl) p₁)
      | _ ⇒ p
    end.

  Definition trproject_over_concat_r_fun_correctness {model:basic_model} p :
    p ⇒ₓ trproject_over_concat_r_fun p.


  Definition trproject_over_concat_r_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "rproject/concat/rec right"
         "Simplify record projection of a concatenation with a record constructor"
         "trproject_over_concat_r_fun"
         trproject_over_concat_r_fun .

  Definition trproject_over_concat_r_step_correct {model:basic_model}
    := mkOptimizerStepModel trproject_over_concat_r_step trproject_over_concat_r_fun_correctness.

  Definition trproject_over_concat_l_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
      | NRAEnvUnop (ARecProject sl)
               (NRAEnvBinop AConcat
                        (NRAEnvUnop (ARec s) p₁) p₂)
        ⇒ if in_dec string_dec s sl
                     

           then p
           else (NRAEnvUnop (ARecProject sl) p₂)
      | _ ⇒ p
    end.

  Definition trproject_over_concat_l_fun_correctness {model:basic_model} p :
    p ⇒ₓ trproject_over_concat_l_fun p.


  Definition trproject_over_concat_l_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "rproject/concat/rec left"
         "Simplify record projection of a concatenation with a record constructor"
         "trproject_over_concat_l_fun"
         trproject_over_concat_l_fun .

  Definition trproject_over_concat_l_step_correct {model:basic_model}
    := mkOptimizerStepModel trproject_over_concat_l_step trproject_over_concat_l_fun_correctness.

  Definition trproject_over_rproject_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
      | NRAEnvUnop (ARecProject sl1)
          (NRAEnvUnop (ARecProject sl2) p1)
        ⇒ NRAEnvUnop (ARecProject (set_inter string_dec sl2 sl1)) p1
      | _ ⇒ p
    end.

  Definition trproject_over_rproject_fun_correctness {model:basic_model} p :
    p ⇒ₓ trproject_over_rproject_fun p.


  Definition trproject_over_rproject_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "rproject/rproject"
         "Fuse nested record projections"
         "trproject_over_rproject_fun"
         trproject_over_rproject_fun .

  Definition trproject_over_rproject_step_correct {model:basic_model}
    := mkOptimizerStepModel trproject_over_rproject_step trproject_over_rproject_fun_correctness.

  Definition trproject_over_either_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
      | NRAEnvUnop (ARecProject sl)
          (NRAEnvEither p₁ p₂)
        ⇒ NRAEnvEither (NRAEnvUnop (ARecProject sl) p₁) (NRAEnvUnop (ARecProject sl) p₂)
      | _ ⇒ p
    end.

  Definition trproject_over_either_fun_correctness {model:basic_model} p :
    p ⇒ₓ trproject_over_either_fun p.


  Definition trproject_over_either_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "rproject/either"
         "Push record projection through an either"
         "trproject_over_either_fun"
         trproject_over_either_fun .

  Definition trproject_over_either_step_correct {model:basic_model}
    := mkOptimizerStepModel trproject_over_either_step trproject_over_either_fun_correctness.

  Definition tcount_over_map_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
      | NRAEnvUnop ACount (NRAEnvMap p₁ p₂) ⇒ NRAEnvUnop ACount p₂
      | _ ⇒ p
    end.

  Definition tcount_over_map_fun_correctness {model:basic_model} p :
    p ⇒ₓ tcount_over_map_fun p.


  Definition tcount_over_map_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "count/map"
         "Simplify count of a map (by removing the map)"
         "tcount_over_map_fun"
         tcount_over_map_fun .

  Definition tcount_over_map_step_correct {model:basic_model}
    := mkOptimizerStepModel tcount_over_map_step tcount_over_map_fun_correctness.

  Definition tcount_over_flat_map_map_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
    | NRAEnvUnop ACount
                 (NRAEnvUnop AFlatten
                             (NRAEnvMap (NRAEnvMap p₁ p₂) p₃)) ⇒
      NRAEnvUnop ACount (NRAEnvUnop AFlatten (NRAEnvMap p₂ p₃))
    | _ ⇒ p
    end.

  Definition tcount_over_flat_map_map_fun_correctness {model:basic_model} p :
    p ⇒ₓ tcount_over_flat_map_map_fun p.


  Definition tcount_over_flat_map_map_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "count/flatten/map/map"
         "Simplify the count of a flatten of a map'ed map"
         "tcount_over_flat_map_map_fun"
         tcount_over_flat_map_map_fun .

  Definition tcount_over_flat_map_map_step_correct {model:basic_model}
    := mkOptimizerStepModel tcount_over_flat_map_map_step tcount_over_flat_map_map_fun_correctness.

  Definition tcount_over_flat_map_either_nil_map_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
    | NRAEnvUnop ACount
                 (NRAEnvUnop AFlatten
                             (NRAEnvMap (NRAEnvEither (NRAEnvMap p₁ p₂)
                                                      (NRAEnvConst (dcoll nil)))
                                        p₃)) ⇒
      NRAEnvUnop ACount
                 (NRAEnvUnop AFlatten
                             (NRAEnvMap (NRAEnvEither p₂
                                                      (NRAEnvConst (dcoll nil))) p₃))
    | _ ⇒ p
    end.

  Definition tcount_over_flat_map_either_nil_map_fun_correctness {model:basic_model} p :
    p ⇒ₓ tcount_over_flat_map_either_nil_map_fun p.


  Definition tcount_over_flat_map_either_nil_map_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "count/flatten/map/either(map)(nil)"
         "Simplify count of a flatten of a map over an either where the right part builds an empty bag"
         "tcount_over_flat_map_either_nil_map_fun"
         tcount_over_flat_map_either_nil_map_fun .

  Definition tcount_over_flat_map_either_nil_map_step_correct {model:basic_model}
    := mkOptimizerStepModel tcount_over_flat_map_either_nil_map_step tcount_over_flat_map_either_nil_map_fun_correctness.

  Definition tcount_over_flat_map_either_nil_app_map_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
    | NRAEnvUnop ACount
                 (NRAEnvUnop AFlatten
                             (NRAEnvMap (NRAEnvApp (NRAEnvEither (NRAEnvMap p₁ p₂)
                                                                 (NRAEnvConst (dcoll nil))) p₄)
                                        p₃)) ⇒
      NRAEnvUnop ACount
                 (NRAEnvUnop AFlatten
                             (NRAEnvMap (NRAEnvApp
                                           (NRAEnvEither p₂ (NRAEnvConst (dcoll nil)))
                                           p₄)
                                        p₃))
      | _ ⇒ p
    end.

  Definition tcount_over_flat_map_either_nil_app_map_fun_correctness {model:basic_model} p :
    p ⇒ₓ tcount_over_flat_map_either_nil_app_map_fun p.


  Definition tcount_over_flat_map_either_nil_app_map_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "count/flatten/map/app/either(map)(nil)"
         "Simplify count of a flatten of a map over an application of an either where the right part builds an empty bag"
         "tcount_over_flat_map_either_nil_app_map_fun"
         tcount_over_flat_map_either_nil_app_map_fun .

  Definition tcount_over_flat_map_either_nil_app_map_step_correct {model:basic_model}
    := mkOptimizerStepModel tcount_over_flat_map_either_nil_app_map_step tcount_over_flat_map_either_nil_app_map_fun_correctness.

  Definition tcount_over_flat_map_either_nil_app_singleton_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
    | NRAEnvUnop ACount
                 (NRAEnvUnop AFlatten
                             (NRAEnvMap (NRAEnvApp (NRAEnvEither (NRAEnvUnop AColl p₁)
                                                                 (NRAEnvConst (dcoll nil))) p₃) p₂)) ⇒
      NRAEnvUnop ACount
                 (NRAEnvUnop AFlatten
                             (NRAEnvMap (NRAEnvApp (NRAEnvEither (NRAEnvUnop AColl (NRAEnvConst dunit))
                                                                 (NRAEnvConst (dcoll nil))) p₃) p₂))
    | _ ⇒ p
    end.

  Definition tcount_over_flat_map_either_nil_app_singleton_fun_correctness {model:basic_model} p :
    p ⇒ₓ tcount_over_flat_map_either_nil_app_singleton_fun p.


  Definition tcount_over_flat_map_either_nil_app_singleton_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "count/flatten/map/app/either(coll)(nil)"
         "Simplify count of a flatten of a map over an application of an either where the left side builds a bag and the right part builds an empty bag"
         "tcount_over_flat_map_either_nil_app_singleton_fun"
         tcount_over_flat_map_either_nil_app_singleton_fun .

  Definition tcount_over_flat_map_either_nil_app_singleton_step_correct {model:basic_model}
    := mkOptimizerStepModel tcount_over_flat_map_either_nil_app_singleton_step tcount_over_flat_map_either_nil_app_singleton_fun_correctness.


  Definition tmapconcat_over_singleton_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvMapConcat p (NRAEnvUnop AColl (NRAEnvConst (drec []))) ⇒
         NRAEnvApp p (NRAEnvConst (drec []))
      | _ ⇒ p
    end.

  Lemma tmapconcat_over_singleton_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tmapconcat_over_singleton_fun p.

  Definition tmapconcat_over_singleton_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "map-concat/coll right/nil"
         "Simplufy map concat with a bag with an empty record"
         "tmapconcat_over_singleton_fun"
         tmapconcat_over_singleton_fun .

  Definition tmapconcat_over_singleton_step_correct {model:basic_model}
    := mkOptimizerStepModel tmapconcat_over_singleton_step tmapconcat_over_singleton_fun_correctness.

  Definition tdup_elim_fun {fruntime:foreign_runtime} (p:nraenv) :=
    dup_elim_fun p.

  Lemma tdup_elim_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tdup_elim_fun p.


  Definition tdup_elim_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "distinct/nodup"
         "Removes applications of the distinct operator to bags statically known to already be duplicate free"
         "tdup_elim_fun"
         tdup_elim_fun .

  Definition tdup_elim_step_correct {model:basic_model}
    := mkOptimizerStepModel tdup_elim_step tdup_elim_fun_correctness.


  Definition tnraenv_optim_list {fruntime:foreign_runtime} : list (@OptimizerStep nraenv)
    := [
        tand_comm_step
        ; tselect_and_comm_step
        ; tselect_and_step
        ; select_union_distr_step
        ; tdot_from_duplicate_r_step
        ; tdot_from_duplicate_l_step
        ; tflatten_coll_step
        ; tconcat_empty_record_r_step
        ; tconcat_empty_record_l_step
        ; tdot_over_concat_r_step
        ; tdot_over_concat_l_step
        ; tmerge_empty_record_r_step
        ; tmerge_empty_record_l_step
        ; tmap_into_id_step
        ; tflatten_map_coll_step
        ; tflatten_flatten_map_either_nil_step
        ; tmap_map_compose_step
        ; tmap_singleton_step
        ; tapp_over_id_r_step
        ; tapp_over_env_step
        ; tapp_over_id_l_step
        ; tapp_over_ignoreid_step
        ; tappenv_over_env_l_step
        ; tappenv_over_env_r_step
        ; tappenv_over_ignoreenv_step
        ; tapp_over_app_step
        ; tappenv_over_appenv_step
        ; tappenv_over_app_step
        ; tapp_over_appenv_step
        ; tapp_over_unop_step
        ; tappenv_over_unop_step
        ; tunop_over_either_const_step
        ; tunop_over_either_const_app_step
        ; tapp_over_map_step
        ; tapp_over_mapconcat_step
        ; tapp_over_product_step
        ; tappenv_over_map_step
        ; tappenv_over_select_step
        ; tapp_over_select_step
        ; tapp_over_binop_step
        ; tproduct_singletons_step
        ; tproduct_empty_right_step
        ; tproduct_empty_left_step
        ; tdouble_flatten_map_coll_step
        ; tflatten_over_double_map_step
        ; tflatten_over_double_map_with_either_step
        ; tappenv_over_env_merge_l_step
        ; ttostring_on_string_step
        ; tmap_full_over_select_step
        ; tcompose_selects_in_mapenv_step
        ; tmapenv_to_env_step
        ; tenv_appenv_step
        ; tflatten_mapenv_coll_step
        ; tflatten_nil_step
        ; tflatten_through_appenv_step
        ; tappenv_flatten_mapenv_to_map_step
        ; tselect_over_either_nil_step
        ; tselect_over_either_nil_app_step
        ; tmap_over_either_nil_step
        ; tmap_over_either_nil_app_step
        ; tappenv_over_either_nil_step
        ; tselect_over_flatten_step
        ; tmap_over_flatten_step
        ; tmap_over_flatten_map_step
        ; tconcat_over_rec_eq_step
        ; tapp_over_const_step
        ; tappenv_over_const_step
        ; tflip_env1_step
        ; tflip_env2_step
        ; tmapenv_over_singleton_step
        ; tappenv_over_binop_step
        ; tflip_env6_step
        ; tmapenv_to_map_step
        ; tmerge_concat_to_concat_step
        ; tmerge_with_concat_to_concat_step
        ; tdot_over_rec_step
        ; tnested_map_over_singletons_step
        ; tappenv_mapenv_to_map_step
        ; trproject_nil_step
        ; trproject_over_const_step
        ; trproject_over_rec_step
        ; trproject_over_concat_r_step
        ; trproject_over_concat_l_step
        ; trproject_over_rproject_step
        ; trproject_over_either_step
        ; tcount_over_map_step
        ; tcount_over_flat_map_map_step
        ; tcount_over_flat_map_either_nil_map_step
        ; tcount_over_flat_map_either_nil_app_map_step
        ; tcount_over_flat_map_either_nil_app_singleton_step
        ; tmapconcat_over_singleton_step
        ; tdup_elim_step
      ].

  Definition tnraenv_optim_model_list {model:basic_model} : list (OptimizerStepModel tnraenv_rewrites_to)
    := [
        tand_comm_step_correct
        ; tselect_and_comm_step_correct
        ; tselect_and_step_correct
        ; select_union_distr_step_correct
        ; tdot_from_duplicate_r_step_correct
        ; tdot_from_duplicate_l_step_correct
        ; tflatten_coll_step_correct
        ; tconcat_empty_record_r_step_correct
        ; tconcat_empty_record_l_step_correct
        ; tdot_over_concat_r_step_correct
        ; tdot_over_concat_l_step_correct
        ; tmerge_empty_record_r_step_correct
        ; tmerge_empty_lecord_l_step_correct
        ; tmap_into_id_step_correct
        ; tflatten_map_coll_step_correct
        ; tflatten_flatten_map_either_nil_step_correct
        ; tmap_map_compose_step_correct
        ; tmap_singleton_step_correct
        ; tapp_over_id_r_step_correct
        ; tapp_over_env_step_correct
        ; tapp_over_id_l_step_correct
        ; tapp_over_ignoreid_step_correct
        ; tappenv_over_env_l_step_correct
        ; tappenv_over_env_r_step_correct
        ; tappenv_over_ignoreenv_step_correct
        ; tapp_over_app_step_correct
        ; tappenv_over_appenv_step_correct
        ; tappenv_over_app_step_correct
        ; tapp_over_appenv_step_correct
        ; tapp_over_unop_step_correct
        ; tappenv_over_unop_step_correct
        ; tunop_over_either_const_step_correct
        ; tunop_over_either_const_app_step_correct
        ; tapp_over_map_step_correct
        ; tapp_over_mapconcat_step_correct
        ; tapp_over_product_step_correct
        ; tappenv_over_map_step_correct
        ; tappenv_over_select_step_correct
        ; tapp_over_select_step_correct
        ; tapp_over_binop_step_correct
        ; tproduct_singletons_step_correct
        ; tproduct_empty_right_step_correct
        ; tproduct_empty_left_step_correct
        ; tdouble_flatten_map_coll_step_correct
        ; tflatten_over_double_map_step_correct
        ; tflatten_over_double_map_with_either_step_correct
        ; tappenv_over_env_merge_l_step_correct
        ; ttostring_on_string_step_correct
        ; tmap_full_over_select_step_correct
        ; tcompose_selects_in_mapenv_step_correct
        ; tmapenv_to_env_step_correct
        ; tenv_appenv_step_correct
        ; tflatten_mapenv_coll_step_correct
        ; tflatten_nil_step_correct
        ; tflatten_through_appenv_step_correct
        ; tappenv_flatten_mapenv_to_map_step_correct
        ; tselect_over_either_nil_step_correct
        ; tselect_over_either_nil_app_step_correct
        ; tmap_over_either_nil_step_correct
        ; tmap_over_either_nil_app_step_correct
        ; tappenv_over_either_nil_step_correct
        ; tselect_over_flatten_step_correct
        ; tmap_over_flatten_step_correct
        ; tmap_over_flatten_map_step_correct
        ; tconcat_over_rec_eq_step_correct
        ; tapp_over_const_step_correct
        ; tappenv_over_const_step_correct
        ; tflip_env1_step_correct
        ; tflip_env2_step_correct
        ; tmapenv_over_singleton_step_correct
        ; tappenv_over_binop_step_correct
        ; tflip_env6_step_correct
        ; tmapenv_to_map_step_correct
        ; tmerge_concat_to_concat_step_correct
        ; tmerge_with_concat_to_concat_step_correct
        ; tdot_over_rec_step_correct
        ; tnested_map_over_singletons_step_correct
        ; tappenv_mapenv_to_map_step_correct
        ; trproject_nil_step_correct
        ; trproject_over_const_step_correct
        ; trproject_over_rec_step_correct
        ; trproject_over_concat_r_step_correct
        ; trproject_over_concat_l_step_correct
        ; trproject_over_rproject_step_correct
        ; trproject_over_either_step_correct
        ; tcount_over_map_step_correct
        ; tcount_over_flat_map_map_step_correct
        ; tcount_over_flat_map_either_nil_map_step_correct
        ; tcount_over_flat_map_either_nil_app_map_step_correct
        ; tcount_over_flat_map_either_nil_app_singleton_step_correct
        ; tmapconcat_over_singleton_step_correct
        ; tdup_elim_step_correct
      ].

  Lemma tnraenv_optim_model_list_complete {model:basic_model}
    : optim_model_list_complete tnraenv_optim_list tnraenv_optim_model_list.

  Definition tnraenv_optim_list_correct {model:basic_model}
    : optim_list_correct tnraenv_rewrites_to tnraenv_optim_list
    := optim_list_correct_from_model tnraenv_optim_model_list_complete.

  Lemma tnraenv_optim_list_distinct {fruntime:foreign_runtime}:
    optim_list_distinct tnraenv_optim_list.

  Definition run_nraenv_optims
             {fruntime:foreign_runtime}
             {logger:optimizer_logger string nraenv}
             (opc:optim_phases_config)
    : nraenv → nraenv :=
    run_phases tnraenv_map_deep nraenv_size tnraenv_optim_list opc.

  Lemma run_nraenv_optims_correctness
        {model:basic_model} {logger:optimizer_logger string nraenv}
        (opc:optim_phases_config)
        (p:nraenv) :
    tnraenv_rewrites_to p ( run_nraenv_optims opc p).

  Section default.

  Definition nraenv_default_head_optim_list {fruntime:foreign_runtime} : list string :=
    [
      optim_step_name tapp_over_app_step
      ; optim_step_name tappenv_over_appenv_step
      ; optim_step_name tappenv_over_app_step
      ; optim_step_name tapp_over_appenv_step
      ; optim_step_name tmap_into_id_step
      ; optim_step_name tproduct_singletons_step
      ; optim_step_name tproduct_empty_right_step
      ; optim_step_name tproduct_empty_left_step
      ; optim_step_name tmap_singleton_step
      ; optim_step_name tmap_map_compose_step
      ; optim_step_name tflatten_coll_step
      
      
      ; optim_step_name tflatten_map_coll_step
      ; optim_step_name tapp_over_id_r_step
      ; optim_step_name tapp_over_id_l_step
      ; optim_step_name tapp_over_unop_step
      ; optim_step_name tapp_over_binop_step
      ; optim_step_name tapp_over_select_step
      ; optim_step_name tapp_over_map_step
      ; optim_step_name tapp_over_mapconcat_step
      ; optim_step_name tapp_over_product_step
      ; optim_step_name tappenv_over_unop_step
      ; optim_step_name tcompose_selects_in_mapenv_step
      ; optim_step_name tmap_full_over_select_step
      ; optim_step_name ttostring_on_string_step
      ; optim_step_name tmerge_empty_record_r_step
      ; optim_step_name tselect_and_step
      ; optim_step_name select_union_distr_step
      ; optim_step_name tdot_from_duplicate_r_step
      ; optim_step_name tdot_from_duplicate_l_step
      ; optim_step_name tconcat_empty_record_r_step
      ; optim_step_name tconcat_empty_record_l_step
      ; optim_step_name tdot_over_concat_r_step
      ; optim_step_name tdot_over_concat_l_step
      ; optim_step_name tmerge_empty_record_r_step
      ; optim_step_name tmerge_empty_record_l_step
      ; optim_step_name tmapenv_to_env_step
      ; optim_step_name tenv_appenv_step
      ; optim_step_name tflatten_mapenv_coll_step
      ; optim_step_name tflatten_nil_step
      
      ; optim_step_name tflatten_through_appenv_step
      
      ; optim_step_name tappenv_flatten_mapenv_to_map_step
      ; optim_step_name tapp_over_const_step
      ; optim_step_name tappenv_over_const_step
      ; optim_step_name tflip_env1_step
      ; optim_step_name tflip_env2_step
      ; optim_step_name tmapenv_over_singleton_step
      ; optim_step_name tappenv_over_binop_step
      ; optim_step_name tflip_env6_step
      ; optim_step_name tmapenv_to_map_step
      ; optim_step_name tappenv_over_map_step
      ; optim_step_name tapp_over_ignoreid_step
      ; optim_step_name tappenv_over_ignoreenv_step
      ; optim_step_name tappenv_over_env_r_step
      ; optim_step_name tappenv_over_env_l_step
      ; optim_step_name tappenv_over_env_merge_l_step
      ; optim_step_name tappenv_over_select_step
      ; optim_step_name tmerge_concat_to_concat_step
      ; optim_step_name tmerge_with_concat_to_concat_step
      ; optim_step_name tdot_over_rec_step
      ; optim_step_name tnested_map_over_singletons_step
      ; optim_step_name tapp_over_env_step
      ; optim_step_name tselect_over_either_nil_step
      ; optim_step_name tselect_over_either_nil_app_step
      ; optim_step_name tmap_over_either_nil_step
      ; optim_step_name tmap_over_either_nil_app_step
      ; optim_step_name tappenv_over_either_nil_step
      ; optim_step_name tselect_over_flatten_step
      
      ; optim_step_name tconcat_over_rec_eq_step
      ; optim_step_name trproject_nil_step
      ; optim_step_name trproject_over_const_step
      ; optim_step_name trproject_over_rec_step
      ; optim_step_name trproject_over_concat_r_step
      ; optim_step_name trproject_over_concat_l_step
      ; optim_step_name trproject_over_rproject_step
      ; optim_step_name trproject_over_either_step
      ; optim_step_name tcount_over_map_step
      ; optim_step_name tcount_over_flat_map_map_step
      ; optim_step_name tcount_over_flat_map_either_nil_map_step
      ; optim_step_name tcount_over_flat_map_either_nil_app_map_step
      ; optim_step_name tcount_over_flat_map_either_nil_app_singleton_step
      ; optim_step_name tunop_over_either_const_app_step
      ; optim_step_name tunop_over_either_const_step
      ; optim_step_name tmapconcat_over_singleton_step
    ].

  Remark nraenv_default_head_optim_list_valid {fruntime:foreign_runtime}
    : valid_optims tnraenv_optim_list nraenv_default_head_optim_list = (nraenv_default_head_optim_list,nil).

  Definition nraenv_default_tail_optim_list {fruntime:foreign_runtime} : list string :=
    [ optim_step_name tflatten_flatten_map_either_nil_step
      ; optim_step_name tmap_over_flatten_map_step
      ; optim_step_name tapp_over_app_step
      ; optim_step_name tappenv_over_appenv_step
      ; optim_step_name tappenv_over_app_step
      ; optim_step_name tapp_over_appenv_step
      ; optim_step_name tmap_into_id_step
      ; optim_step_name tproduct_singletons_step
      ; optim_step_name tproduct_empty_right_step
      ; optim_step_name tproduct_empty_left_step
      ; optim_step_name tmap_singleton_step
      ; optim_step_name tmap_map_compose_step
      ; optim_step_name tflatten_coll_step
      
      ; optim_step_name tdouble_flatten_map_coll_step
      ; optim_step_name tflatten_over_double_map_step
      ; optim_step_name tflatten_over_double_map_with_either_step
      ; optim_step_name tflatten_map_coll_step
      ; optim_step_name tapp_over_id_r_step
      ; optim_step_name tapp_over_id_l_step
      ; optim_step_name tapp_over_unop_step
      ; optim_step_name tapp_over_binop_step
      ; optim_step_name tapp_over_select_step
      ; optim_step_name tapp_over_map_step
      ; optim_step_name tapp_over_mapconcat_step
      ; optim_step_name tapp_over_product_step
      ; optim_step_name tappenv_over_unop_step
      ; optim_step_name tcompose_selects_in_mapenv_step
      ; optim_step_name tmap_full_over_select_step
      ; optim_step_name ttostring_on_string_step
      ; optim_step_name tmerge_empty_record_r_step
      ; optim_step_name tselect_and_step
      ; optim_step_name select_union_distr_step
      ; optim_step_name tdot_from_duplicate_r_step
      ; optim_step_name tdot_from_duplicate_l_step
      ; optim_step_name tconcat_empty_record_r_step
      ; optim_step_name tconcat_empty_record_l_step
      ; optim_step_name tdot_over_concat_r_step
      ; optim_step_name tdot_over_concat_l_step
      ; optim_step_name tmerge_empty_record_r_step
      ; optim_step_name tmerge_empty_record_l_step
      ; optim_step_name tmapenv_to_env_step
      ; optim_step_name tenv_appenv_step
      ; optim_step_name tflatten_mapenv_coll_step
      ; optim_step_name tflatten_nil_step
      ; optim_step_name tapp_over_const_step
      ; optim_step_name tappenv_over_const_step
      ; optim_step_name tflip_env1_step
      ; optim_step_name tflip_env2_step
      ; optim_step_name tmapenv_over_singleton_step
      ; optim_step_name tappenv_over_binop_step
      ; optim_step_name tflip_env6_step
      ; optim_step_name tmapenv_to_map_step
      ; optim_step_name tappenv_over_map_step
      ; optim_step_name tapp_over_ignoreid_step
      ; optim_step_name tappenv_over_ignoreenv_step
      ; optim_step_name tappenv_over_env_r_step
      ; optim_step_name tappenv_over_env_l_step
      ; optim_step_name tappenv_over_env_merge_l_step
      ; optim_step_name tappenv_over_select_step
      ; optim_step_name tmerge_concat_to_concat_step
      ; optim_step_name tmerge_with_concat_to_concat_step
      ; optim_step_name tdot_over_rec_step
      ; optim_step_name tnested_map_over_singletons_step
      ; optim_step_name tapp_over_env_step
      ; optim_step_name tappenv_mapenv_to_map_step
      ; optim_step_name tselect_over_either_nil_step
      ; optim_step_name tselect_over_either_nil_app_step
      ; optim_step_name tmap_over_either_nil_step
      ; optim_step_name tmap_over_either_nil_app_step
      ; optim_step_name tappenv_over_either_nil_step
      ; optim_step_name tselect_over_flatten_step
      ; optim_step_name tmap_over_flatten_step
      ; optim_step_name tconcat_over_rec_eq_step
      ; optim_step_name trproject_nil_step
      ; optim_step_name trproject_over_const_step
      ; optim_step_name trproject_over_rec_step
      ; optim_step_name trproject_over_concat_r_step
      ; optim_step_name trproject_over_concat_l_step
      ; optim_step_name trproject_over_rproject_step
      ; optim_step_name trproject_over_either_step
      ; optim_step_name tcount_over_map_step
      ; optim_step_name tcount_over_flat_map_map_step
      ; optim_step_name tcount_over_flat_map_either_nil_map_step
      ; optim_step_name tcount_over_flat_map_either_nil_app_map_step
      ; optim_step_name tcount_over_flat_map_either_nil_app_singleton_step
      ; optim_step_name tunop_over_either_const_app_step
      ; optim_step_name tunop_over_either_const_step
      ; optim_step_name tmapconcat_over_singleton_step
    ].

    Remark nraenv_default_tail_optim_list_valid {fruntime:foreign_runtime}
    : valid_optims tnraenv_optim_list nraenv_default_tail_optim_list = (nraenv_default_tail_optim_list,nil).

    Definition default_nraenv_optim_phases {fruntime:foreign_runtime} :=
      ("[nraenv] head"%string,nraenv_default_head_optim_list,5)
        :: ("[nraenv] tail"%string,nraenv_default_tail_optim_list,15)
        :: nil.

  End default.

  Definition toptim_old_nraenv_head {fruntime:foreign_runtime} {logger:optimizer_logger string nraenv}
    := run_nraenv_optims (("head",nraenv_default_head_optim_list,5)::nil).

  Lemma toptim_old_nraenv_head_correctness {model:basic_model} {logger:optimizer_logger string nraenv} p:
    p ⇒ₓ toptim_old_nraenv_head p.

  Definition toptim_old_nraenv_tail {fruntime:foreign_runtime} {logger:optimizer_logger string nraenv}
    := run_nraenv_optims (("tail",nraenv_default_head_optim_list,15)::nil).

  Lemma toptim_old_nraenv_tail_correctness {model:basic_model} {logger:optimizer_logger string nraenv} p:
    p ⇒ₓ toptim_old_nraenv_tail p.

  Definition toptim_old_nraenv {fruntime:foreign_runtime} {logger:optimizer_logger string nraenv} :=
    compose toptim_old_nraenv_tail toptim_old_nraenv_head.

  Lemma compose_transitivity {A:Type} {R:relation A} {trans:Transitive R}
        (x y:A) (f g :A→A):
    R x (g y) →
    R (g y) (f (g y)) →
    R x ((compose f g) y).

  Lemma toptim_old_nraenv_correctness {model:basic_model} {logger:optimizer_logger string nraenv} p:
    p ⇒ₓ toptim_old_nraenv p.

End NRAEnvOptimizer.