Module NRAEnvRewrite

Section ROptimEnv.

  Require Import List String.
  Require Import ListSet.

  Require Import Utils BasicRuntime.

  Require Import NRARuntime NRAOptim.
  Require Import cNRAEnv cNRAEnvIgnore cNRAEnvEq.


  Local Open Scope nra_scope.
  Local Open Scope nraenv_core_scope.

  Context {fruntime:foreign_runtime}.


  Hint Resolve dnrec_sort_content.
  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 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(χ⟨ANEither p₁ ‵{||} ◯ p₂⟩(p₃))) ≡ₑ
     ♯flatten( χ⟨ANEither( ♯flatten(p₁)) ‵{||} ◯ p₂⟩(p₃)).
      

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


  Lemma rmap_to_map l :
    rmap (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₁⟩(ANConst (dcoll nil)) ≡ₑ ANConst (dcoll nil).

  Lemma map_over_nil p₁ :
    χ⟨p₁⟩(ANConst (dcoll nil)) ≡ₑ ANConst (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₁⟩( ANEither p₂ p₃) ≡ₑ ANEither (σ⟨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₁⟩( ANEither p₂ p₃) ≡ₑ ANEither (χ⟨p₁⟩(p₂)) (χ⟨p₁⟩(p₃)).

  Lemma envmap_over_either_app p₁ p₂ p₃ p₄:
    χ⟨p₁⟩( ANEither p₂ p₃ ◯ p₄) ≡ₑ ANEither (χ⟨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:
    (ANUnop u p1) ◯ p2 ≡ₑ (ANUnop u (p1 ◯ p2)).


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

  Lemma unop_over_either u p₁ p₂ :
    ANUnop u (ANEither p₁ p₂) ≡ₑ ANEither (ANUnop u p₁)(ANUnop u p₂).

  Lemma unop_over_either_app u p₁ p₂ p₃ :
    ANUnop u (ANEither p₁ p₂ ◯ p₃) ≡ₑ ANEither (ANUnop u p₁)(ANUnop u p₂) ◯ p₃.


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

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

  
  Lemma app_over_binop_env b p1 p2 s:
    (ANBinop b p1 p2 ◯ (ANUnop (ADot s) ANEnv))
      ≡ₑ (ANBinop b (p1 ◯ (ANUnop (ADot s) ANEnv)) (p2 ◯ (ANUnop (ADot s) ANEnv))).

  
  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:
    ANAppEnv (ANMapEnv (ANUnop AColl ANEnv)) (ANUnop AFlatten p) ≡ₑ (ANMap (ANUnop AColl ANID) (ANUnop AFlatten p)).


  Lemma appenv_over_mapenv_coll p:
    ANAppEnv (ANMapEnv (ANUnop AColl (ANUnop AColl ANEnv))) (ANUnop AFlatten p) ≡ₑ (ANMap (ANUnop AColl (ANUnop AColl ANID)) (ANUnop AFlatten p)).

  
  Lemma appenv_over_mapenv_merge s:
    ANAppEnv (ANMapEnv (ANUnop AColl ((ENV) · s))) (ENV ⊗ ID)
             ≡ₑ ANMap (ANUnop AColl ((ID) · s)) (ENV ⊗ ID).

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

  
  Lemma appenv_over_mapenv_merge2 s:
    ANAppEnv (ANMapEnv ((ENV) · s)) (ENV ⊗ ID)
             ≡ₑ ANMap ((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 ->
    (ANBinop b ((ID) · a1) ((ID) · a2))
      ◯ (‵[| (a1, p1) |] ⊕ ‵[| (a2, p2) |])
      ≡ₑ (ANBinop b p1 p2).

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

  
  Lemma tostring_dstring s:
    (ANUnop AToString (ANConst (dstring s))) ≡ₑ (ANConst (dstring s)).

  
  Lemma tostring_tostring p:
    (ANUnop AToString (ANUnop AToString p)) ≡ₑ (ANUnop AToString p).

  
  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:
    (((ANMapEnv (‵{|ENV|})) ◯ₑ p1) ◯ p2) ≡ₑ
    (((ANMapEnv (‵{|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(ANMapEnv (χ⟨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₃ ->
    ANEither q₁ q₂ ◯ₑ q₃ ≡ₑ ANEither (q₁ ◯ₑ q₃) (q₂ ◯ₑ q₃).


  
  Lemma flatten_mapenv_coll p1:
    ♯flatten(ANMapEnv (‵{| p1 |})) ≡ₑ ANMapEnv 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 :
     (ANBinop b p1 p2) ◯ₑ ID ≡ₑ (ANBinop b (p1 ◯ₑ ID) (p2 ◯ₑ ID)).

  Lemma flip_env4 p1 p2 s :
     (ANUnop (ADot s) p1) ◯ₑ p2 ≡ₑ (ANUnop (ADot s) (p1 ◯ₑ p2)).

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

  Lemma flip_env7 p1 p2:
    nraenv_core_ignores_id p1 ->
    (ANMapEnv (‵{| 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 :
    (ANEither p₁ p₂) ◯ (ANConst (dleft d)) ≡ₑ p₁ ◯ (ANConst d).

  Lemma either_app_over_dright p₁ p₂ d :
    (ANEither p₁ p₂) ◯ (ANConst (dright d)) ≡ₑ p₂ ◯ (ANConst d).

  Lemma either_app_over_aleft p₁ p₂ p :
    (ANEither p₁ p₂) ◯ (ANUnop ALeft p) ≡ₑ p₁ ◯ p.
  
  Lemma either_app_over_aright p₁ p₂ p :
    (ANEither p₁ p₂) ◯ (ANUnop ARight p) ≡ₑ p₂ ◯ p.

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

  Lemma rproject_over_const sl l :
    π[sl](ANConst (drec l)) ≡ₑ ANConst (drec (RRelation.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](ANEither p1 p2) ≡ₑ ANEither (π[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 -> ANUnop ADistinct q ≡ₑ q.

  
  Fixpoint nraenv_core_split_last (e:nraenv_core) : (nraenv_core*nraenv_core)
    := match e with
         | ANID => (ANID,ANID)
         | ANConst c => (ANID,ANConst c)
         | ANBinop b e1 e2 => (ANBinop b e1 e2,ANID)
         | ANUnop u e1 =>
           match nraenv_core_split_last e1 with
             | (ANID, r) => (ANUnop u r, ANID)
             | (e1last, e1rest) => (e1last, ANUnop u e1rest)
           end
         | ANMap e1 e2 =>
           match nraenv_core_split_last e2 with
             | (ANID, r) => (ANMap e1 e2, ANID)
             | (e2last, e2rest) => (e2last, ANMap e1 e2rest)
           end
         | ANMapConcat e1 e2 =>
           match nraenv_core_split_last e2 with
             | (ANID, r) => (ANMapConcat e1 e2, ANID)
             | (e2last, e2rest) => (e2last, ANMapConcat e1 e2rest)
           end
         | ANProduct e1 e2 => (ANProduct e1 e2,ANID)
         | ANSelect e1 e2 =>
           match nraenv_core_split_last e2 with
             | (ANID, r) => (ANSelect e1 e2, ANID)
             | (e2last, e2rest) => (e2last, ANSelect e1 e2rest)
           end
         | ANDefault e1 e2 => (ANDefault e1 e2,ANID)
         | ANEither l r => (ANEither l r, ANID)
         | ANEitherConcat l r =>
           (ANEitherConcat l r, ANID)
         | ANApp e1 e2 =>
           match nraenv_core_split_last e2 with
             | (ANID, r) => (e1, r)
             | (e2last, e2rest) => (e2last, ANApp e1 e2rest)
           end
         | ANGetConstant s => (ANID,ANGetConstant s)
         | ANEnv => (ANID,ANEnv)
         | ANAppEnv e1 e2 => (ANAppEnv e1 e2, ANID)
         | ANMapEnv e => (ANMapEnv e, ANID)
       end.

  
End ROptimEnv.



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


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


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


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


Hint Rewrite @product_singletons : nraenv_core_optim.
Hint Rewrite @double_flatten_map_coll : nraenv_core_optim.
Hint Rewrite @tostring_dstring : nraenv_core_optim.
Hint Rewrite @tostring_tostring : nraenv_core_optim.


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

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

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