Qcert.NRAEnv.Optim.NRAEnvRewrite
Section ROptimEnv.
Context {fruntime:foreign_runtime}.
Lemma pull_nra_opt (p1 p2:cnraenv) :
(nra_of_cnraenv p1) ≡ₐ (nra_of_cnraenv p2) →
p1 ≡ₑ p2.
Lemma envand_comm (p1 p2: cnraenv) :
p2 ∧ p1 ≡ₑ p1 ∧ p2.
Lemma envunion_assoc (p1 p2 p3: cnraenv):
(p1 ⋃ p2) ⋃ p3 ≡ₑ p1 ⋃ (p2 ⋃ p3).
Lemma select_union_distr (q q₁ q₂: cnraenv) :
σ⟨ q ⟩(q₁ ⋃ q₂) ≡ₑ σ⟨ q ⟩(q₁) ⋃ σ⟨ q ⟩(q₂).
Lemma envmap_singleton (p1 p2:cnraenv) :
χ⟨ p1 ⟩( ‵{| p2 |} ) ≡ₑ ‵{| p1 ◯ p2 |}.
Lemma envmap_map_compose (p1 p2 p3:cnraenv) :
χ⟨ 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₃)).
Now has a (better) typed variant for arbitrary p1/p2, see TOptimEnv
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:
cnraenv_ignores_id p0 →
χ⟨ p1 ⟩( p2 ) ◯ₑ p0 ≡ₑ χ⟨ p1 ◯ₑ p0 ⟩( p2 ◯ₑ p0 ).
Lemma appenv_over_select p0 p1 p2:
cnraenv_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:
cnraenv_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:
cnraenv_ignores_id p3 →
((p3 ◯ₑ p2) ◯ p1) ≡ₑ p3 ◯ₑ (p2 ◯ p1).
Lemma appenv_over_app_ie p1 p2 p3:
cnraenv_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₃:
cnraenv_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:
cnraenv_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.
optimizations for record projection
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 : cnraenv → Prop :=
cnraenv_always_ensures
(fun d ⇒ match d with
| dcoll dl ⇒ NoDup dl
| _ ⇒ False
end).
Lemma dup_elim (q:cnraenv) :
nodupA q → ANUnop ADistinct q ≡ₑ q.
π[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 : cnraenv → Prop :=
cnraenv_always_ensures
(fun d ⇒ match d with
| dcoll dl ⇒ NoDup dl
| _ ⇒ False
end).
Lemma dup_elim (q:cnraenv) :
nodupA q → ANUnop ADistinct q ≡ₑ q.
Some optimizations are best seen through outlining -- the
opposite of inlining. This allows sharing of common sub-expressions.
To enable this, we first define the "last" part of a computation.
returns: (last part of the computation, rest of it)
Fixpoint cnraenv_split_last (e:cnraenv) : (cnraenv×cnraenv)
:= match e with
| ANID ⇒ (ANID,ANID)
| ANConst c ⇒ (ANID,ANConst c)
| ANBinop b e1 e2 ⇒ (ANBinop b e1 e2,ANID)
| ANUnop u e1 ⇒
match cnraenv_split_last e1 with
| (ANID, r) ⇒ (ANUnop u r, ANID)
| (e1last, e1rest) ⇒ (e1last, ANUnop u e1rest)
end
| ANMap e1 e2 ⇒
match cnraenv_split_last e2 with
| (ANID, r) ⇒ (ANMap e1 e2, ANID)
| (e2last, e2rest) ⇒ (e2last, ANMap e1 e2rest)
end
| ANMapConcat e1 e2 ⇒
match cnraenv_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 cnraenv_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 cnraenv_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.
:= match e with
| ANID ⇒ (ANID,ANID)
| ANConst c ⇒ (ANID,ANConst c)
| ANBinop b e1 e2 ⇒ (ANBinop b e1 e2,ANID)
| ANUnop u e1 ⇒
match cnraenv_split_last e1 with
| (ANID, r) ⇒ (ANUnop u r, ANID)
| (e1last, e1rest) ⇒ (e1last, ANUnop u e1rest)
end
| ANMap e1 e2 ⇒
match cnraenv_split_last e2 with
| (ANID, r) ⇒ (ANMap e1 e2, ANID)
| (e2last, e2rest) ⇒ (e2last, ANMap e1 e2rest)
end
| ANMapConcat e1 e2 ⇒
match cnraenv_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 cnraenv_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 cnraenv_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.