Module Qcert.NRAEnv.Optim.NRAEnvOptimizer

Require Import Equivalence.
Require Import Morphisms.
Require Import Setoid.
Require Import EquivDec.
Require Import Program.
Require Import String.
Require Import BinNums.
Require Import List.
Require Import ListSet.
Require Import Utils.
Require Import DataSystem.
Require Import cNRAEnvSystem.
Require Import NRAEnvSystem.
Require Import OptimizerStep.
Require Import OptimizerLogger.
Require Import NRAEnvRewrite.
Require Import TNRAEnvRewrite.

Import ListNotations.
Local Open Scope list_scope.

Section NRAEnvOptimizer.
  Open Scope nraenv_scope.
  

  Ltac tcorrectness_prover :=
          simpl; repeat progress (try match goal with
        | [|- context [match ?p with | _ => _ end] ] => destruct p
      end; try reflexivity; try unfold Equivalence.equiv in *; try subst).

  Ltac tprove_correctness p :=
    destruct p;
    tcorrectness_prover.


  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':
    (forall 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)
      | NRAEnvMapProduct op1 op2 => NRAEnvMapProduct (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)
      | NRAEnvNaturalJoin op1 op2 => NRAEnvNaturalJoin (f op1) (f op2)
      | 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))
      | NRAEnvMapProduct op1 op2 => f (NRAEnvMapProduct (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))
      | NRAEnvNaturalJoin op1 op2 => f (NRAEnvNaturalJoin (nraenv_map_deep f op1) (nraenv_map_deep f op2))
      | 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 (nraenv_to_nraenv_core q).

    Fixpoint nodupA_checker {fruntime:foreign_runtime} (p:nraenv) : bool
    := match p with
       | NRAEnvUnop OpDistinct _ => true
       | NRAEnvBinop OpBagDiff 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 OpDistinct 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}:
    forall f: nraenv -> nraenv,
    forall p: nraenv,
      (forall 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}:
    forall f: nraenv -> nraenv,
    forall p: nraenv,
      (forall p', p' ⇒ₓ f p') -> p ⇒ₓ tnraenv_map_deep f p.



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

  Lemma tand_comm_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tand_comm_fun p.
  Local Hint Rewrite @tand_comm_fun_correctness : optim_correct.

  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 OpAnd op1 op2) op =>
        NRAEnvSelect (NRAEnvBinop OpAnd op2 op1) op
      | _ => p
    end.

  Lemma tselect_and_comm_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tselect_and_comm_fun p.
  Local Hint Rewrite @tselect_and_comm_fun_correctness : optim_correct.

  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 OpBagUnion op1 op2) =>
        NRAEnvBinop OpBagUnion (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.
  Local Hint Rewrite @select_union_distr_fun_correctness : optim_correct.

  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 OpAnd op2 op1) op
      | _ => p
    end.

  Lemma tselect_and_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tselect_and_fun p.
  Local Hint Rewrite @tselect_and_fun_correctness : optim_correct.

  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 (OpDot s2)
               (NRAEnvBinop OpRecConcat (NRAEnvUnop (OpRec s1) op1) (NRAEnvUnop (OpRec 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.
  Local Hint Rewrite @tdot_from_duplicate_r_fun_correctness : optim_correct.

  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 (OpDot s1)
               (NRAEnvBinop OpRecConcat (NRAEnvUnop (OpRec s1') op1) (NRAEnvUnop (OpRec 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.
  Local Hint Rewrite @tdot_from_duplicate_l_fun_correctness : optim_correct.

  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 OpFlatten (NRAEnvUnop OpBag p) => p
      | _ => p
    end.

  Lemma tflatten_coll_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tflatten_coll_fun p.
  Local Hint Rewrite @tflatten_coll_fun_correctness : optim_correct.
  
  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 OpRecConcat 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.
  Local Hint Rewrite @tconcat_empty_record_r_fun_correctness : optim_correct.

  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 OpRecConcat (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.
  Local Hint Rewrite @tconcat_empty_record_l_fun_correctness : optim_correct.

    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 (OpDot a₂) (NRAEnvBinop OpRecConcat q₁ (NRAEnvUnop (OpRec a₁) q₂)) =>
       if a₁ == a₂
       then q₂
       else NRAEnvUnop (OpDot a₂) q₁
      | _ => p
    end.

  Lemma tdot_over_concat_r_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tdot_over_concat_r_fun p.
  Local Hint Rewrite @tdot_over_concat_r_fun_correctness : optim_correct.

  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 (OpDot a₂) (NRAEnvBinop OpRecConcat (NRAEnvUnop (OpRec a₁) q₁) q₂) =>
       if a₁ == a₂
       then p
       else NRAEnvUnop (OpDot a₂) q₂
      | _ => p
    end.

  Lemma tdot_over_concat_l_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tdot_over_concat_l_fun p.
  Local Hint Rewrite @tdot_over_concat_l_fun_correctness : optim_correct.

   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 OpRecMerge p (NRAEnvConst (drec [])) =>
         NRAEnvUnop OpBag p
      | _ => p
    end.

  Lemma tmerge_empty_record_r_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tmerge_empty_record_r_fun p.
  Local Hint Rewrite @tmerge_empty_record_r_fun_correctness : optim_correct.

  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 OpRecMerge (NRAEnvConst (drec [])) p =>
         NRAEnvUnop OpBag p
      | _ => p
    end.

  Lemma tmerge_empty_record_l_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tmerge_empty_record_l_fun p.
  Local Hint Rewrite @tmerge_empty_record_l_fun_correctness : optim_correct.

  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.
  Local Hint Rewrite @tmap_into_id_fun_correctness : optim_correct.

  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 OpFlatten (NRAEnvMap (NRAEnvUnop OpBag p1) p2) =>
        NRAEnvMap p1 p2
      | _ => p
    end.

  Lemma tflatten_map_coll_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tflatten_map_coll_fun p.
  Local Hint Rewrite @tflatten_map_coll_fun_correctness : optim_correct.

  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 OpFlatten
                   (NRAEnvUnop OpFlatten (NRAEnvMap (NRAEnvApp (NRAEnvEither p₁ (NRAEnvConst (dcoll nil))) p₂) p₃)) =>
        NRAEnvUnop OpFlatten (NRAEnvMap (NRAEnvApp
                                          (NRAEnvEither (NRAEnvUnop OpFlatten 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.

  Local Hint Rewrite @tflatten_flatten_map_either_nil_fun_correctness : optim_correct.

  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.
  Local Hint Rewrite @tmap_map_compose_fun_correctness : optim_correct.

  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 OpBag p2) => NRAEnvUnop OpBag (NRAEnvApp p1 p2)
      | _ => p
    end.

  Lemma tmap_singleton_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tmap_singleton_fun p.
  Local Hint Rewrite @tmap_singleton_fun_correctness : optim_correct.

  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 nth0_bag_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
        NRAEnvBinop OpBagNth (NRAEnvUnop OpBag p) (NRAEnvConst (dnat Z0)) => NRAEnvUnop OpLeft p
      | _ => p
    end.

  Lemma nth0_bag_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ nth0_bag_fun p.
  Local Hint Rewrite @nth0_bag_fun_correctness : optim_correct.

  Definition nth0_bag_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "nth0bag"
         "Take the element of a bag of one element"
         "nth0_bag_fun"
         nth0_bag_fun .

  Definition nth0_bag_step_correct {model:basic_model}
    := mkOptimizerStepModel nth0_bag_step nth0_bag_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.
  Local Hint Rewrite @tapp_over_id_r_fun_correctness : optim_correct.

  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.
  Local Hint Rewrite @tapp_over_env_fun_correctness : optim_correct.

  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.
  Local Hint Rewrite @tapp_over_id_l_fun_correctness : optim_correct.

  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.
  Local Hint Rewrite @tapp_over_app_fun_correctness : optim_correct.

  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.
  Local Hint Rewrite @tappenv_over_appenv_fun_correctness : optim_correct.

   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.

  Local Hint Rewrite @tappenv_over_app_fun_correctness : optim_correct.

    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.
  Local Hint Rewrite @tapp_over_unop_fun_correctness : optim_correct.

  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.
  Local Hint Rewrite @tapp_over_map_fun_correctness : optim_correct.

  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 (NRAEnvMapProduct p1 p2) p0 =>
        NRAEnvMapProduct p1 (NRAEnvApp p2 p0)
      | _ => p
    end.

  Lemma tapp_over_mapconcat_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tapp_over_mapconcat_fun p.
  Local Hint Rewrite @tapp_over_mapconcat_fun_correctness : optim_correct.

  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.
  Local Hint Rewrite @tapp_over_product_fun_correctness : optim_correct.

  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.
  Local Hint Rewrite @tapp_over_select_fun_correctness : optim_correct.

  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.
  Local Hint Rewrite @tapp_over_binop_fun_correctness : optim_correct.

  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 OpBag (NRAEnvUnop (OpRec s1) p1))
                  (NRAEnvUnop OpBag (NRAEnvUnop (OpRec s2) p2)) =>
        NRAEnvUnop OpBag
               (NRAEnvBinop OpRecConcat (NRAEnvUnop (OpRec s1) p1) (NRAEnvUnop (OpRec s2) p2))
      | _ => p
    end.

  Lemma tproduct_singletons_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tproduct_singletons_fun p.
  Local Hint Rewrite @tproduct_singletons_fun_correctness : optim_correct.

  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 OpBag (NRAEnvConst (drec nil))) => p1
    | _ => p
    end.

  Lemma tproduct_empty_right_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tproduct_empty_right_fun p.
  Local Hint Rewrite @tproduct_empty_right_fun_correctness : optim_correct.

  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 OpBag (NRAEnvConst (drec nil))) p1 => p1
    | _ => p
    end.

  Lemma tproduct_empty_left_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tproduct_empty_left_fun p.
  Local Hint Rewrite @tproduct_empty_left_fun_correctness : optim_correct.

  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 OpFlatten
               (NRAEnvMap (NRAEnvMap (NRAEnvUnop OpBag p3) p1) p2) =>
        NRAEnvMap (NRAEnvUnop OpBag p3)
              (NRAEnvUnop OpFlatten (NRAEnvMap p1 p2))
      | _ => p
    end.

  Lemma tdouble_flatten_map_coll_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ tdouble_flatten_map_coll_fun p.
  Local Hint Rewrite @tdouble_flatten_map_coll_fun_correctness : optim_correct.

    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 OpFlatten
                (NRAEnvMap (NRAEnvMap q₁ (NRAEnvSelect q₂ (NRAEnvUnop OpBag 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.
  Local Hint Rewrite @tflatten_over_double_map_fun_correctness : optim_correct.

  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 OpFlatten
              (NRAEnvMap
                 (NRAEnvMap q₁
                        (NRAEnvSelect q₂
                                  (NRAEnvApp
                                     (NRAEnvEither (NRAEnvUnop OpBag NRAEnvID) (NRAEnvConst (dcoll []))) q₃)))
                 q₄)) =>
      (NRAEnvMap q₁
             (NRAEnvSelect q₂
                       (NRAEnvUnop OpFlatten
                               (NRAEnvMap
                                  (NRAEnvApp
                                     (NRAEnvEither (NRAEnvUnop OpBag 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.
  Local Hint Rewrite @tflatten_over_double_map_with_either_fun_correctness : optim_correct.

  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 OpRecMerge NRAEnvEnv p1) p2 =>
        if (nraenv_ignores_env_fun p1)
        then (NRAEnvBinop OpRecMerge 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 tmap_full_over_select_fun {fruntime:foreign_runtime} (p: nraenv) :=
    match p with
      | NRAEnvMap p0 (NRAEnvSelect p1 (NRAEnvUnop OpBag NRAEnvID)) => p
      | NRAEnvMap p0 (NRAEnvSelect p1 (NRAEnvUnop OpBag p2)) =>
        NRAEnvMap (NRAEnvApp p0 p2) (NRAEnvSelect (NRAEnvApp p1 p2) (NRAEnvUnop OpBag 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 OpFlatten
                   (NRAEnvMapEnv (NRAEnvMap NRAEnvEnv (NRAEnvSelect p1 (NRAEnvUnop OpBag NRAEnvID)))))
           (NRAEnvMap NRAEnvEnv (NRAEnvSelect p2 (NRAEnvUnop OpBag NRAEnvID)))) =>
        (NRAEnvMap NRAEnvEnv (NRAEnvSelect p1 (NRAEnvSelect p2 (NRAEnvUnop OpBag 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 OpFlatten (NRAEnvMapEnv (NRAEnvUnop OpBag 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 OpFlatten (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 OpFlatten (NRAEnvAppEnv p1 p2) =>
        NRAEnvAppEnv (NRAEnvUnop OpFlatten 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 OpFlatten (NRAEnvMapEnv p2))
            (NRAEnvBinop OpRecMerge NRAEnvEnv (NRAEnvUnop (OpRec s) NRAEnvID))) =>
         (NRAEnvUnop OpFlatten
            (NRAEnvMap (NRAEnvAppEnv (NRAEnvApp p2 (NRAEnvUnop (OpDot s) NRAEnvEnv)) NRAEnvID)
                   (NRAEnvBinop OpRecMerge NRAEnvEnv (NRAEnvUnop (OpRec 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.

  Local Hint Rewrite @tselect_over_either_nil_fun_correctness : toptim_correct.

  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.

  Local Hint Rewrite @tselect_over_either_nil_app_fun_correctness : toptim_correct.

  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.

  Local Hint Rewrite @tmap_over_either_nil_fun_correctness : toptim_correct.

  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.

  Local Hint Rewrite @tmap_over_either_nil_app_fun_correctness : toptim_correct.

  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.

  Local Hint Rewrite @tappenv_over_either_nil_fun_correctness : toptim_correct.

    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 OpFlatten p₂) =>
      NRAEnvUnop OpFlatten (NRAEnvMap (NRAEnvSelect p₁ NRAEnvID) p₂)
    | _ => p
    end.

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

  Local Hint Rewrite @tselect_over_flatten_fun_correctness : toptim_correct.

  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 OpFlatten p₂) =>
      NRAEnvUnop OpFlatten (NRAEnvMap (NRAEnvMap p₁ NRAEnvID) p₂)
    | _ => p
    end.

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

  Local Hint Rewrite @tmap_over_flatten_fun_correctness : toptim_correct.

  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 OpFlatten (NRAEnvMap p₂ p₃)) =>
      NRAEnvUnop OpFlatten (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.

  Local Hint Rewrite @tmap_over_flatten_map_fun_correctness : toptim_correct.

  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 OpRecConcat
                 (NRAEnvUnop (OpRec s₁) p₁) (NRAEnvUnop (OpRec s₂) p₂))
        => if string_dec s₁ s₂
           then (NRAEnvUnop (OpRec s₂) p₂)
           else p
      | _ => p
    end.

  Definition tconcat_over_rec_eq_fun_correctness {model:basic_model} p :
    p ⇒ₓ tconcat_over_rec_eq_fun p.
                  
  Local Hint Rewrite @tconcat_over_rec_eq_fun_correctness : toptim_correct.

  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 OpBag NRAEnvID))) q₂ =>
      match q₂ with
      | NRAEnvID => (NRAEnvAppEnv (NRAEnvSelect q₁ (NRAEnvUnop OpBag NRAEnvID)) NRAEnvID)
      | _ =>
        if (nraenv_ignores_env_fun q₁)
        then NRAEnvMap q₂ (NRAEnvSelect q₁ (NRAEnvUnop OpBag 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 OpBag NRAEnvID)) NRAEnvID) =>
      (NRAEnvSelect (NRAEnvAppEnv p NRAEnvID) (NRAEnvUnop OpBag 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 OpBag p2)) =>
      (NRAEnvUnop OpBag (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 OpRecMerge NRAEnvEnv NRAEnvID)
                (NRAEnvSelect p1 (NRAEnvBinop OpRecMerge NRAEnvEnv p2)) =>
      NRAEnvMap (NRAEnvUnop OpBag NRAEnvID)
                (NRAEnvSelect p1 (NRAEnvBinop OpRecMerge 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 OpRecMerge (NRAEnvUnop (OpRec s1) p1) (NRAEnvUnop (OpRec s2) p2) =>
      if (s1 == s2)
      then p
      else NRAEnvUnop OpBag
                      (NRAEnvBinop OpRecConcat
                                   (NRAEnvUnop (OpRec s1) p1)
                                   (NRAEnvUnop (OpRec 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 OpRecMerge (NRAEnvUnop (OpRec s1) p1)
                  (NRAEnvBinop OpRecConcat (NRAEnvUnop (OpRec s1') p1')
                               (NRAEnvUnop (OpRec s2) p2)) =>
        if (s1 == s2)
        then p
        else
          if (s1 == s1')
          then
            if (p1 == p1')
            then NRAEnvUnop OpBag (NRAEnvBinop OpRecConcat
                                               (NRAEnvUnop (OpRec s1) p1)
                                               (NRAEnvUnop (OpRec 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 (OpDot s2)
                 (NRAEnvUnop (OpRec 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 teither_app_over_dleft_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
    | NRAEnvApp (NRAEnvEither p1 p2) (NRAEnvConst (dleft d)) => NRAEnvApp p1 (NRAEnvConst d)
    | _ => p
    end.

  Lemma teither_app_over_dleft_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ teither_app_over_dleft_fun p.

  Definition teither_app_over_dleft_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "either/dleft"
         "Simplifies the application of a either on a left value"
         "teither_app_over_dleft_fun"
         teither_app_over_dleft_fun .

  Definition teither_app_over_dleft_step_correct {model:basic_model}
    := mkOptimizerStepModel teither_app_over_dleft_step teither_app_over_dleft_fun_correctness.


  Definition teither_app_over_dright_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
    | NRAEnvApp (NRAEnvEither p1 p2) (NRAEnvConst (dright d)) => NRAEnvApp p2 (NRAEnvConst d)
    | _ => p
    end.

  Lemma teither_app_over_dright_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ teither_app_over_dright_fun p.

  Definition teither_app_over_dright_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "either/dright"
         "Simplifies the application of a either on a right value"
         "teither_app_over_dright_fun"
         teither_app_over_dright_fun .

  Definition teither_app_over_dright_step_correct {model:basic_model}
    := mkOptimizerStepModel teither_app_over_dright_step teither_app_over_dright_fun_correctness.

  Definition teither_app_over_aleft_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
    | NRAEnvApp (NRAEnvEither p1 p2) (NRAEnvUnop OpLeft p) => NRAEnvApp p1 p
    | _ => p
    end.

  Lemma teither_app_over_aleft_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ teither_app_over_aleft_fun p.

  Definition teither_app_over_aleft_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "either/left"
         "Simplifies the application of a either on a left expression"
         "teither_app_over_aleft_fun"
         teither_app_over_aleft_fun .

  Definition teither_app_over_aleft_step_correct {model:basic_model}
    := mkOptimizerStepModel teither_app_over_aleft_step teither_app_over_aleft_fun_correctness.


  Definition teither_app_over_aright_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
    | NRAEnvApp (NRAEnvEither p1 p2) (NRAEnvUnop OpRight p) => NRAEnvApp p2 p
    | _ => p
    end.

  Lemma teither_app_over_aright_fun_correctness {model:basic_model} (p:nraenv) :
    p ⇒ₓ teither_app_over_aright_fun p.

  Definition teither_app_over_aright_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "either/right"
         "Simplifies the application of a either on a right expression"
         "teither_app_over_aright_fun"
         teither_app_over_aright_fun .

  Definition teither_app_over_aright_step_correct {model:basic_model}
    := mkOptimizerStepModel teither_app_over_aright_step teither_app_over_aright_fun_correctness.


  Definition tnested_map_over_singletons_fun {fruntime:foreign_runtime} (p:nraenv) :=
    match p with
    | NRAEnvUnop OpFlatten
                 (NRAEnvMap (NRAEnvSelect q₁ (NRAEnvUnop OpBag 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 OpRecMerge NRAEnvEnv (NRAEnvUnop (OpRec a) NRAEnvID)) =>
      NRAEnvMap (NRAEnvAppEnv (NRAEnvApp q (NRAEnvUnop (OpDot a) NRAEnvEnv)) NRAEnvID)
                (NRAEnvBinop OpRecMerge NRAEnvEnv (NRAEnvUnop (OpRec 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 (OpRecProject nil) p₁
        => NRAEnvConst (drec nil)
      | _ => p
    end.

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

  Local Hint Rewrite @trproject_nil_fun_correctness : toptim_correct.

  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 (OpRecProject 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.

  Local Hint Rewrite @trproject_over_const_fun_correctness : toptim_correct.

  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 (OpRecProject sl)
          (NRAEnvUnop (OpRec s) p₁)
        => if in_dec string_dec s sl
           then NRAEnvUnop (OpRec s) p₁
           else NRAEnvConst (drec nil)
      | _ => p
    end.

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

  Local Hint Rewrite @trproject_over_rec_fun_correctness : toptim_correct.

  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 (OpRecProject sl)
               (NRAEnvBinop OpRecConcat
                        p₁ (NRAEnvUnop (OpRec s) p₂))
        => if in_dec string_dec s sl
           then NRAEnvBinop OpRecConcat
                        (NRAEnvUnop (OpRecProject (remove string_dec s sl)) p₁)
                        (NRAEnvUnop (OpRec s) p₂)
           else (NRAEnvUnop (OpRecProject sl) p₁)
      | _ => p
    end.

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

  Local Hint Rewrite @trproject_over_concat_r_fun_correctness : toptim_correct.

  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 (OpRecProject sl)
               (NRAEnvBinop OpRecConcat
                        (NRAEnvUnop (OpRec s) p₁) p₂)
        => if in_dec string_dec s sl

           then p
           else (NRAEnvUnop (OpRecProject sl) p₂)
      | _ => p
    end.

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

  Local Hint Rewrite @trproject_over_concat_l_fun_correctness : toptim_correct.

  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 (OpRecProject sl1)
          (NRAEnvUnop (OpRecProject sl2) p1)
        => NRAEnvUnop (OpRecProject (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.

  Local Hint Rewrite @trproject_over_rproject_fun_correctness : toptim_correct.

  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 (OpRecProject sl)
          (NRAEnvEither p₁ p₂)
        => NRAEnvEither (NRAEnvUnop (OpRecProject sl) p₁) (NRAEnvUnop (OpRecProject sl) p₂)
      | _ => p
    end.

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

  Local Hint Rewrite @trproject_over_either_fun_correctness : toptim_correct.

  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 OpCount (NRAEnvMap p₁ p₂) => NRAEnvUnop OpCount p₂
      | _ => p
    end.

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

  Local Hint Rewrite @tcount_over_map_fun_correctness : toptim_correct.

  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 OpCount
                 (NRAEnvUnop OpFlatten
                             (NRAEnvMap (NRAEnvMap p₁ p₂) p₃)) =>
      NRAEnvUnop OpCount (NRAEnvUnop OpFlatten (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.

  Local Hint Rewrite @tcount_over_flat_map_map_fun_correctness : toptim_correct.

  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 OpCount
                 (NRAEnvUnop OpFlatten
                             (NRAEnvMap (NRAEnvEither (NRAEnvMap p₁ p₂)
                                                      (NRAEnvConst (dcoll nil)))
                                        p₃)) =>
      NRAEnvUnop OpCount
                 (NRAEnvUnop OpFlatten
                             (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.

  Local Hint Rewrite @tcount_over_flat_map_either_nil_map_fun_correctness : toptim_correct.

  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 OpCount
                 (NRAEnvUnop OpFlatten
                             (NRAEnvMap (NRAEnvApp (NRAEnvEither (NRAEnvMap p₁ p₂)
                                                                 (NRAEnvConst (dcoll nil))) p₄)
                                        p₃)) =>
      NRAEnvUnop OpCount
                 (NRAEnvUnop OpFlatten
                             (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.

  Local Hint Rewrite @tcount_over_flat_map_either_nil_app_map_fun_correctness : toptim_correct.

  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 OpCount
                 (NRAEnvUnop OpFlatten
                             (NRAEnvMap (NRAEnvApp (NRAEnvEither (NRAEnvUnop OpBag p₁)
                                                                 (NRAEnvConst (dcoll nil))) p₃) p₂)) =>
      NRAEnvUnop OpCount
                 (NRAEnvUnop OpFlatten
                             (NRAEnvMap (NRAEnvApp (NRAEnvEither (NRAEnvUnop OpBag (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.

  Local Hint Rewrite @tcount_over_flat_map_either_nil_app_singleton_fun_correctness : toptim_correct.

  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
      | NRAEnvMapProduct p (NRAEnvUnop OpBag (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.
  Local Hint Rewrite @tmerge_empty_record_r_fun_correctness : optim_correct.

  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.

  Local Hint Rewrite @tdup_elim_fun_correctness : optim_correct.

  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.
  
  Local Open Scope string.

  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
        ; nth0_bag_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
        ; 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
        ; teither_app_over_dleft_step
        ; teither_app_over_dright_step
        ; teither_app_over_aleft_step
        ; teither_app_over_aright_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
        ; nth0_bag_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
        ; 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
        ; teither_app_over_dleft_step_correct
        ; teither_app_over_dright_step_correct
        ; teither_app_over_aleft_step_correct
        ; teither_app_over_aright_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 nraenv_optim_top
             {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 nraenv_optim_top_correctness
        {model:basic_model} {logger:optimizer_logger string nraenv}
        (opc:optim_phases_config)
        (p:nraenv) :
    tnraenv_rewrites_to p (nraenv_optim_top 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 nth0_bag_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 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 teither_app_over_dleft_step
      ; optim_step_name teither_app_over_dright_step
      ; optim_step_name teither_app_over_aleft_step
      ; optim_step_name teither_app_over_aright_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 nth0_bag_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 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 teither_app_over_dleft_step
      ; optim_step_name teither_app_over_dright_step
      ; optim_step_name teither_app_over_aleft_step
      ; optim_step_name teither_app_over_aright_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}
    := nraenv_optim_top (("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}
    := nraenv_optim_top (("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.