Module Qcert.NRAEnv.Optim.NRAEnvRewrite

Require Import BinNums.
Require Import List.
Require Import String.
Require Import ListSet.
Require Import Utils.
Require Import DataRuntime.
Require Import NRARuntime.
Require Import NRAOptim.
Require Import cNRAEnvRuntime.

Section ROptimEnv.


  Local Open Scope nra_scope.
  Local Open Scope nraenv_core_scope.

  Context {fruntime:foreign_runtime}.


  Local Hint Resolve dnrec_sort_content : qcert.
  Lemma pull_nra_opt (p1 p2:nraenv_core) :
    (nra_of_nraenv_core p1) ≡ₐ (nra_of_nraenv_core p2) ->
    p1 ≡ₑ p2.


  Lemma envand_comm (p1 p2: nraenv_core) :
    p2 ∧ p1 ≡ₑ p1 ∧ p2.


  Lemma envunion_assoc (p1 p2 p3: nraenv_core):
    (p1 ⋃ p2) ⋃ p3 ≡ₑ p1 ⋃ (p2 ⋃ p3).
  
  Lemma select_union_distr (q q₁ q₂: nraenv_core) :
    σ⟨ q ⟩(q₁ ⋃ q₂) ≡ₑ σ⟨ q ⟩(q₁) ⋃ σ⟨ q ⟩(q₂).


  Lemma envmap_singleton (p1 p2:nraenv_core) :
    χ⟨ p1 ⟩( ‵{| p2 |} ) ≡ₑ ‵{| p1 ◯ p2 |}.

  Lemma envnth0_bag (p: nraenv_core) :
    cNRAEnvBinop OpBagNth (‵{| p |}) ‵ (dnat Z0) ≡ₑ
    cNRAEnvUnop OpLeft p.


  Lemma envmap_map_compose (p1 p2 p3:nraenv_core) :
    χ⟨ p1 ⟩( χ⟨ p2 ⟩( p3 ) ) ≡ₑ χ⟨ p1 ◯ p2 ⟩( p3 ).


  Lemma app_over_rec s p1 p2:
    ‵[| (s, p1) |] ◯ p2 ≡ₑ ‵[| (s, p1 ◯ p2) |].

  
  Lemma envflatten_coll_flatten p:
    ♯flatten(‵{| ♯flatten( p ) |}) ≡ₑ ♯flatten( p ).
  
  
  Lemma envflatten_coll_coll p:
    ♯flatten(‵{| ‵{| p |} |}) ≡ₑ ‵{| p |}.

  Lemma envflatten_nil :
    ♯flatten(‵{||}) ≡ₑ ‵{||}.

  
  Lemma envflatten_coll_map p1 p2 :
    ♯flatten(‵{| χ⟨ p1 ⟩( p2 ) |}) ≡ₑ χ⟨ p1 ⟩( p2 ).

  Lemma flatten_flatten_map_either_nil p₁ p₂ p₃ :
    ♯flatten( ♯flatten(χ⟨cNRAEnvEither p₁ ‵{||} ◯ p₂⟩(p₃))) ≡ₑ
     ♯flatten( χ⟨cNRAEnvEither( ♯flatten(p₁)) ‵{||} ◯ p₂⟩(p₃)).
      

  Lemma envflatten_coll_mergeconcat p1 p2:
    ♯flatten( ‵{| p1 ⊗ p2 |} ) ≡ₑ p1 ⊗ p2.


  Lemma lift_map_to_map l :
    lift_map (fun x : data => Some (dcoll (x :: nil))) l =
    Some (map (fun x : data => (dcoll (x :: nil))) l).

  Lemma double_flatten_map_coll p1 p2 :
    ♯flatten(χ⟨ χ⟨ ‵{| ID |} ⟩( ♯flatten( p1 ) ) ⟩( p2 ))
            ≡ₑ χ⟨ ‵{| ID |} ⟩(♯flatten(χ⟨ ♯flatten( p1 ) ⟩( p2 ))).

  
  Lemma envflatten_map_coll p1 p2 :
    ♯flatten(χ⟨ ‵{| p1 |} ⟩( p2 )) ≡ₑ χ⟨ p1 ⟩( p2 ).

  Lemma select_over_nil p₁ :
    σ⟨p₁⟩(cNRAEnvConst (dcoll nil)) ≡ₑ cNRAEnvConst (dcoll nil).

  Lemma map_over_nil p₁ :
    χ⟨p₁⟩(cNRAEnvConst (dcoll nil)) ≡ₑ cNRAEnvConst (dcoll nil).

  Lemma map_over_flatten p₁ p₂ :
    χ⟨p₁⟩(♯flatten(p₂)) ≡ₑ (♯flatten(χ⟨χ⟨p₁⟩(ID)⟩(p₂))).
  
  Lemma select_over_flatten p₁ p₂ :
    σ⟨p₁⟩(♯flatten(p₂)) ≡ₑ (♯flatten(χ⟨σ⟨p₁⟩(ID)⟩(p₂))).

  Lemma select_over_either p₁ p₂ p₃ :
    σ⟨p₁⟩( cNRAEnvEither p₂ p₃) ≡ₑ cNRAEnvEither (σ⟨p₁⟩(p₂)) (σ⟨p₁⟩(p₃)).


  Lemma envdot_from_duplicate_r s1 s2 p1 :
    (‵[| (s1, p1) |] ⊕ ‵[| (s2, p1) |])·s2 ≡ₑ p1.


  Lemma envdot_from_duplicate_l s1 s2 p1 :
    (‵[| (s1, p1) |] ⊕ ‵[| (s2, p1) |])·s1 ≡ₑ p1.

  Lemma envmap_over_either p₁ p₂ p₃ :
    χ⟨p₁⟩( cNRAEnvEither p₂ p₃) ≡ₑ cNRAEnvEither (χ⟨p₁⟩(p₂)) (χ⟨p₁⟩(p₃)).

  Lemma envmap_over_either_app p₁ p₂ p₃ p₄:
    χ⟨p₁⟩( cNRAEnvEither p₂ p₃ ◯ p₄) ≡ₑ cNRAEnvEither (χ⟨p₁⟩(p₂)) (χ⟨p₁⟩(p₃)) ◯ p₄.

  
  Lemma envmap_into_id p :
    χ⟨ ID ⟩(‵{| p |}) ≡ₑ ‵{| p |}.

  

  
  Lemma envmap_into_id_flatten p :
    χ⟨ ID ⟩( ♯flatten(p) ) ≡ₑ ♯flatten(p).


  Lemma product_singletons s1 s2 p1 p2:
    ‵{|‵[| (s1, p1) |] |} × ‵{| ‵[| (s2, p2) |] |} ≡ₑ
     ‵{|‵[| (s1, p1) |] ⊕ ‵[| (s2, p2) |] |}.

  
  Lemma app_over_id p:
    p ◯ ID ≡ₑ p.

  
  Lemma appenv_over_env p:
    ENV ◯ₑ p ≡ₑ p.

  
  Lemma app_over_id_l p:
    ID ◯ p ≡ₑ p.

  
  Lemma app_over_app p1 p2 p3:
    (p1 ◯ p2) ◯ p3 ≡ₑ p1 ◯ (p2 ◯ p3).


  Lemma app_over_unop u p1 p2:
    (cNRAEnvUnop u p1) ◯ p2 ≡ₑ (cNRAEnvUnop u (p1 ◯ p2)).


  Lemma appenv_over_unop u p1 p2:
    (cNRAEnvUnop u p1) ◯ₑ p2 ≡ₑ (cNRAEnvUnop u (p1 ◯ₑ p2)).

  Lemma unop_over_either u p₁ p₂ :
    cNRAEnvUnop u (cNRAEnvEither p₁ p₂) ≡ₑ cNRAEnvEither (cNRAEnvUnop u p₁)(cNRAEnvUnop u p₂).

  Lemma unop_over_either_app u p₁ p₂ p₃ :
    cNRAEnvUnop u (cNRAEnvEither p₁ p₂ ◯ p₃) ≡ₑ cNRAEnvEither (cNRAEnvUnop u p₁)(cNRAEnvUnop u p₂) ◯ p₃.


  Lemma app_over_merge p1 p2:
    (cNRAEnvEnv ⊗ p1) ◯ p2 ≡ₑ cNRAEnvEnv ⊗ (p1 ◯ p2).

  
  Lemma app_over_binop_l b d p1 p2:
    (cNRAEnvBinop b p2 (cNRAEnvConst d) ◯ p1)
      ≡ₑ (cNRAEnvBinop b (p2 ◯ p1) (cNRAEnvConst d)).
 
  
  Lemma app_concat_over_binop b p1 p2 p3 p4:
    (cNRAEnvBinop b p1 p2 ◯ (p3 ⊕ p4) )
      ≡ₑ (cNRAEnvBinop b (p1 ◯ (p3 ⊕ p4)) (p2 ◯ (p3 ⊕ p4))).

  
  Lemma app_over_binop_env b p1 p2 s:
    (cNRAEnvBinop b p1 p2 ◯ (cNRAEnvUnop (OpDot s) cNRAEnvEnv))
      ≡ₑ (cNRAEnvBinop b (p1 ◯ (cNRAEnvUnop (OpDot s) cNRAEnvEnv)) (p2 ◯ (cNRAEnvUnop (OpDot s) cNRAEnvEnv))).

  
  Lemma app_over_select p0 p1 p2:
    σ⟨ p1 ⟩( p2 ) ◯ p0 ≡ₑ σ⟨ p1 ⟩( p2 ◯ p0 ).

  
  Lemma app_over_map p0 p1 p2:
    χ⟨ p1 ⟩( p2 ) ◯ p0 ≡ₑ χ⟨ p1 ⟩( p2 ◯ p0 ).
  
  
  Lemma app_over_mapconcat p0 p1 p2:
    ⋈ᵈ⟨ p1 ⟩( p2 ) ◯ p0 ≡ₑ ⋈ᵈ⟨ p1 ⟩( p2 ◯ p0 ).
  
  
  Lemma app_over_product p0 p1 p2:
    (p1 × p2) ◯ p0 ≡ₑ (p1 ◯ p0) × (p2 ◯ p0).
  
  
  Lemma appenv_over_map p0 p1 p2:
    nraenv_core_ignores_id p0 ->
    χ⟨ p1 ⟩( p2 ) ◯ₑ p0 ≡ₑ χ⟨ p1 ◯ₑ p0 ⟩( p2 ◯ₑ p0 ).

  
  Lemma appenv_over_select p0 p1 p2:
    nraenv_core_ignores_id p0 ->
    σ⟨ p1 ⟩( p2 ) ◯ₑ p0 ≡ₑ σ⟨ p1 ◯ₑ p0 ⟩( p2 ◯ₑ p0 ).

  
  Lemma appenv_over_mapenv p:
    cNRAEnvAppEnv (cNRAEnvMapEnv (cNRAEnvUnop OpBag cNRAEnvEnv)) (cNRAEnvUnop OpFlatten p) ≡ₑ (cNRAEnvMap (cNRAEnvUnop OpBag cNRAEnvID) (cNRAEnvUnop OpFlatten p)).


  Lemma appenv_over_mapenv_coll p:
    cNRAEnvAppEnv (cNRAEnvMapEnv (cNRAEnvUnop OpBag (cNRAEnvUnop OpBag cNRAEnvEnv))) (cNRAEnvUnop OpFlatten p) ≡ₑ (cNRAEnvMap (cNRAEnvUnop OpBag (cNRAEnvUnop OpBag cNRAEnvID)) (cNRAEnvUnop OpFlatten p)).

  
  Lemma appenv_over_mapenv_merge s:
    cNRAEnvAppEnv (cNRAEnvMapEnv (cNRAEnvUnop OpBag ((ENV) · s))) (ENV ⊗ ID)
             ≡ₑ cNRAEnvMap (cNRAEnvUnop OpBag ((ID) · s)) (ENV ⊗ ID).

  
  Lemma appenv_over_env_merge_l p1 p2:
    nraenv_core_ignores_env p1 ->
    cNRAEnvAppEnv (ENV ⊗ p1) p2 ≡ₑ p2 ⊗ p1.

  
  Lemma appenv_over_mapenv_merge2 s:
    cNRAEnvAppEnv (cNRAEnvMapEnv ((ENV) · s)) (ENV ⊗ ID)
             ≡ₑ cNRAEnvMap ((ID) · s) (ENV ⊗ ID).


  Lemma env_appenv p:
    (ENV) ◯ₑ p ≡ₑ p.

  
  
  Lemma envmap_singleton_rec s1 s2 :
    χ⟨‵[| (s1, ID) |] ⟩( ‵{|(ID) · s2 |}) ≡ₑ ‵{|‵[| (s1, (ID) · s2) |] |}.

  
  Lemma envmap_dot_singleton a p :
    χ⟨ ID·a ⟩( ‵{| p |} ) ≡ₑ ‵{| p·a |}.

  
  Lemma envunnest_singleton s1 s2 s3 p1 p2 :
    s1 <> s2 /\ s2 <> s3 /\ s3 <> s1 ->
    χ⟨ ¬π[s1](ID) ⟩(
       ⋈ᵈ⟨ χ⟨‵[| (s2,ID) |] ⟩((ID)·s1) ⟩( ‵{|‵[| (s3,p1) |] ⊕ ‵[| (s1,‵{| p2 |}) |]|} )
     )
     ≡ₑ ‵{|‵[| (s3, p1) |] ⊕ ‵[| (s2, p2) |]|}.


  Lemma binop_over_rec_pair b p1 p2 a1 a2:
    a1 <> a2 ->
    (cNRAEnvBinop b ((ID) · a1) ((ID) · a2))
      ◯ (‵[| (a1, p1) |] ⊕ ‵[| (a2, p2) |])
      ≡ₑ (cNRAEnvBinop b p1 p2).

  
  Lemma concat_id_left p1 p2 s1 s2 d:
    (‵[| (s1, p1) |] ⊕ ‵[| (s2, cNRAEnvConst d) |])
      ◯ p2
     ≡ₑ (‵[| (s1, p1 ◯ p2) |] ⊕ ‵[| (s2, cNRAEnvConst d) |]).

  
  Lemma app_over_env_dot s:
    (ENV ◯ (ENV) · s) · s ≡ₑ (ENV) · s.

  Lemma app_over_appenv p1 p2 p3:
    nraenv_core_ignores_id p3 ->
    ((p3 ◯ₑ p2) ◯ p1) ≡ₑ p3 ◯ₑ (p2 ◯ p1).

  Lemma appenv_over_app_ie p1 p2 p3:
    nraenv_core_ignores_env p3 ->
    ((p3 ◯ p2) ◯ₑ p1) ≡ₑ p3 ◯ (p2 ◯ₑ p1).

  Lemma app_over_appenv_over_mapenv p1 p2:
    (((cNRAEnvMapEnv (‵{|ENV|})) ◯ₑ p1) ◯ p2) ≡ₑ
    (((cNRAEnvMapEnv (‵{|ENV|})) ◯ₑ (p1 ◯ p2) )).

  Lemma map_full_over_select_id p0 p1 p2:
    χ⟨ p0 ⟩(σ⟨ p1 ⟩(‵{| p2 |})) ≡ₑ χ⟨ p0 ◯ p2 ⟩(σ⟨ p1 ◯ p2 ⟩(‵{| ID |})).

  Lemma compose_selects_in_mapenv p1 p2 :
    (♯flatten(cNRAEnvMapEnv (χ⟨ENV⟩(σ⟨p1⟩( ‵{| ID |}))))) ◯ₑ (χ⟨ENV⟩(σ⟨p2⟩( ‵{| ID |})))
            ≡ₑ (χ⟨ENV⟩(σ⟨p1⟩(σ⟨p2⟩( ‵{| ID |})))).

  
  Lemma flatten_through_appenv p1 p2 :
    ♯flatten(p1 ◯ₑ p2) ≡ₑ ♯flatten(p1) ◯ₑ p2.

  Lemma appenv_through_either q₁ q₂ q₃:
    nraenv_core_ignores_id q₃ ->
    cNRAEnvEither q₁ q₂ ◯ₑ q₃ ≡ₑ cNRAEnvEither (q₁ ◯ₑ q₃) (q₂ ◯ₑ q₃).


  
  Lemma flatten_mapenv_coll p1:
    ♯flatten(cNRAEnvMapEnv (‵{| p1 |})) ≡ₑ cNRAEnvMapEnv p1.

  Lemma flip_env1 p :
    χ⟨ENV⟩(σ⟨ p ⟩(‵{|ID|})) ◯ₑ ID ≡ₑ (σ⟨ p ⟩(‵{|ID|})) ◯ₑ ID.

  Lemma flip_env2 p :
    (σ⟨ p ⟩(‵{|ID|}) ◯ₑ ID) ≡ₑ σ⟨ p ◯ₑ ID ⟩(‵{|ID|}).

  Lemma flip_env3 b p1 p2 :
     (cNRAEnvBinop b p1 p2) ◯ₑ ID ≡ₑ (cNRAEnvBinop b (p1 ◯ₑ ID) (p2 ◯ₑ ID)).

  Lemma flip_env4 p1 p2 s :
     (cNRAEnvUnop (OpDot s) p1) ◯ₑ p2 ≡ₑ (cNRAEnvUnop (OpDot s) (p1 ◯ₑ p2)).

  Lemma flip_env5 p1 p2:
    ♯flatten(χ⟨σ⟨p1⟩(‵{|ID|})⟩(p2)) ≡ₑ σ⟨p1⟩(p2).

  Lemma flip_env7 p1 p2:
    nraenv_core_ignores_id p1 ->
    (cNRAEnvMapEnv (‵{| p1 |})) ◯ₑ p2 ≡ₑ χ⟨‵{| p1 ◯ₑ ID |}⟩(p2).

  
  Lemma merge_concat_to_concat s1 s2 p1 p2:
    s1 <> s2 ->
    ‵[| (s1, p1)|] ⊗ ‵[| (s2, p2)|] ≡ₑ ‵{|‵[| (s1, p1)|] ⊕ ‵[| (s2, p2)|]|}.


  Lemma dot_over_rec s p :
    (‵[| (s, p)|]) · s ≡ₑ p.

  Lemma either_app_over_dleft p₁ p₂ d :
    (cNRAEnvEither p₁ p₂) ◯ (cNRAEnvConst (dleft d)) ≡ₑ p₁ ◯ (cNRAEnvConst d).

  Lemma either_app_over_dright p₁ p₂ d :
    (cNRAEnvEither p₁ p₂) ◯ (cNRAEnvConst (dright d)) ≡ₑ p₂ ◯ (cNRAEnvConst d).

  Lemma either_app_over_aleft p₁ p₂ p :
    (cNRAEnvEither p₁ p₂) ◯ (cNRAEnvUnop OpLeft p) ≡ₑ p₁ ◯ p.
  
  Lemma either_app_over_aright p₁ p₂ p :
    (cNRAEnvEither p₁ p₂) ◯ (cNRAEnvUnop OpRight p) ≡ₑ p₂ ◯ p.

  Lemma rproject_over_concat sl p1 p2 :
    π[sl](p1 ⊕ p2)
          ≡ₑ π[sl](p1) ⊕ π[sl](p2).

  Lemma rproject_over_const sl l :
    π[sl](cNRAEnvConst (drec l)) ≡ₑ cNRAEnvConst (drec (Bindings.rproject l sl)).
  
  Lemma rproject_over_rec_in sl s p :
    In s sl ->
    π[sl](‵[| (s, p) |]) ≡ₑ ‵[| (s, p) |].

  Lemma rproject_over_rec_nin sl s p :
    ~ In s sl ->
    π[sl](‵[| (s, p) |]) ≡ₑ ‵[||] ◯ p .
  
  Lemma rproject_over_rproject sl1 sl2 p :
    π[sl1](π[sl2](p)) ≡ₑ π[set_inter string_dec sl2 sl1](p).

  Lemma rproject_over_either sl p1 p2 :
    π[sl](cNRAEnvEither p1 p2) ≡ₑ cNRAEnvEither (π[sl](p1)) (π[sl](p2)).

  Lemma map_over_map_split p₁ p₂ p₃ :
    χ⟨χ⟨p₁ ⟩( p₂) ⟩( p₃) ≡ₑ χ⟨χ⟨p₁ ⟩( ID) ⟩(χ⟨p₂⟩(p₃)).
  
  Definition nodupA : nraenv_core -> Prop :=
    nraenv_core_always_ensures
      (fun d => match d with
                | dcoll dl => NoDup dl
                | _ => False
                end).
  
  Lemma dup_elim (q:nraenv_core) :
    nodupA q -> cNRAEnvUnop OpDistinct q ≡ₑ q.

  
  Fixpoint nraenv_core_split_last (e:nraenv_core) : (nraenv_core*nraenv_core)
    := match e with
         | cNRAEnvID => (cNRAEnvID,cNRAEnvID)
         | cNRAEnvConst c => (cNRAEnvID,cNRAEnvConst c)
         | cNRAEnvBinop b e1 e2 => (cNRAEnvBinop b e1 e2,cNRAEnvID)
         | cNRAEnvUnop u e1 =>
           match nraenv_core_split_last e1 with
             | (cNRAEnvID, r) => (cNRAEnvUnop u r, cNRAEnvID)
             | (e1last, e1rest) => (e1last, cNRAEnvUnop u e1rest)
           end
         | cNRAEnvMap e1 e2 =>
           match nraenv_core_split_last e2 with
             | (cNRAEnvID, r) => (cNRAEnvMap e1 e2, cNRAEnvID)
             | (e2last, e2rest) => (e2last, cNRAEnvMap e1 e2rest)
           end
         | cNRAEnvMapProduct e1 e2 =>
           match nraenv_core_split_last e2 with
             | (cNRAEnvID, r) => (cNRAEnvMapProduct e1 e2, cNRAEnvID)
             | (e2last, e2rest) => (e2last, cNRAEnvMapProduct e1 e2rest)
           end
         | cNRAEnvProduct e1 e2 => (cNRAEnvProduct e1 e2,cNRAEnvID)
         | cNRAEnvSelect e1 e2 =>
           match nraenv_core_split_last e2 with
             | (cNRAEnvID, r) => (cNRAEnvSelect e1 e2, cNRAEnvID)
             | (e2last, e2rest) => (e2last, cNRAEnvSelect e1 e2rest)
           end
         | cNRAEnvDefault e1 e2 => (cNRAEnvDefault e1 e2,cNRAEnvID)
         | cNRAEnvEither l r => (cNRAEnvEither l r, cNRAEnvID)
         | cNRAEnvEitherConcat l r =>
           (cNRAEnvEitherConcat l r, cNRAEnvID)
         | cNRAEnvApp e1 e2 =>
           match nraenv_core_split_last e2 with
             | (cNRAEnvID, r) => (e1, r)
             | (e2last, e2rest) => (e2last, cNRAEnvApp e1 e2rest)
           end
         | cNRAEnvGetConstant s => (cNRAEnvID,cNRAEnvGetConstant s)
         | cNRAEnvEnv => (cNRAEnvID,cNRAEnvEnv)
         | cNRAEnvAppEnv e1 e2 => (cNRAEnvAppEnv e1 e2, cNRAEnvID)
         | cNRAEnvMapEnv e => (cNRAEnvMapEnv e, cNRAEnvID)
       end.

  
End ROptimEnv.



Global Hint Rewrite @envflatten_map_coll : nraenv_core_optim.
Global Hint Rewrite @envmap_into_id : nraenv_core_optim.
Global Hint Rewrite @envmap_into_id_flatten : nraenv_core_optim.


Global Hint Rewrite @envmap_map_compose : nraenv_core_optim.
Global Hint Rewrite @envmap_singleton : nraenv_core_optim.


Global Hint Rewrite @envnth0_bag : nraenv_core_optim.



Global Hint Rewrite @envflatten_coll_mergeconcat : nraenv_core_optim.
Global Hint Rewrite @envflatten_coll_map : nraenv_core_optim.
Global Hint Rewrite @envflatten_coll_flatten : nraenv_core_optim.
Global Hint Rewrite @envflatten_coll_coll : nraenv_core_optim.


Global Hint Rewrite @app_over_id : nraenv_core_optim.
Global Hint Rewrite @app_over_id_l : nraenv_core_optim.
Global Hint Rewrite @app_over_app : nraenv_core_optim.
Global Hint Rewrite @app_over_map : nraenv_core_optim.
Global Hint Rewrite @app_over_select : nraenv_core_optim.
Global Hint Rewrite @app_over_unop : nraenv_core_optim.
Global Hint Rewrite @app_over_binop_l : nraenv_core_optim.
Global Hint Rewrite @app_over_merge : nraenv_core_optim.
Global Hint Rewrite @app_over_rec : nraenv_core_optim.
Global Hint Rewrite @binop_over_rec_pair : nraenv_core_optim.
Global Hint Rewrite @concat_id_left : nraenv_core_optim.
Global Hint Rewrite @app_over_env_dot : nraenv_core_optim.
Global Hint Rewrite @app_over_appenv_over_mapenv : nraenv_core_optim.


Global Hint Rewrite @product_singletons : nraenv_core_optim.
Global Hint Rewrite @double_flatten_map_coll : nraenv_core_optim.


Global Hint Rewrite @env_appenv : nraenv_core_optim.
Global Hint Rewrite @appenv_over_mapenv : nraenv_core_optim.
Global Hint Rewrite @appenv_over_mapenv_coll : nraenv_core_optim.
Global Hint Rewrite @appenv_over_mapenv_merge : nraenv_core_optim.
Global Hint Rewrite @appenv_over_mapenv_merge2 : nraenv_core_optim.
Global Hint Rewrite @compose_selects_in_mapenv : nraenv_core_optim.
Global Hint Rewrite @flatten_through_appenv : nraenv_core_optim.
Global Hint Rewrite @flatten_mapenv_coll : nraenv_core_optim.

Global Hint Rewrite @either_app_over_dleft : nraenv_core_optim.
Global Hint Rewrite @either_app_over_dright : nraenv_core_optim.
Global Hint Rewrite @either_app_over_aleft : nraenv_core_optim.
Global Hint Rewrite @either_app_over_aright : nraenv_core_optim.

Global Hint Rewrite @rproject_over_concat : nraenv_core_optim.
Global Hint Rewrite @rproject_over_rec_in : nraenv_core_optim.
Global Hint Rewrite @rproject_over_rec_nin : nraenv_core_optim.
Global Hint Rewrite @rproject_over_rproject : nraenv_core_optim.
Global Hint Rewrite @rproject_over_either : nraenv_core_optim.