Qcert.NNRC.Optim.TNNRCRewrite
Section TNNRCRewrite.
Context {m:basic_model}.
Lemma tunshadow_preserves_arrow sep renamer avoid (e:nnrc) :
tnnrc_ext_rewrites_to e (unshadow sep renamer avoid e).
Lemma tdot_of_rec a (e:nnrc) :
tnnrc_ext_rewrites_to (NNRCUnop (ADot a) (NNRCUnop (ARec a) e)) e.
Lemma tnnrc_dot_of_concat_rec_eq_arrow a (e1 e2:nnrc) :
tnnrc_ext_rewrites_to (NNRCUnop (ADot a) (NNRCBinop AConcat e1 (NNRCUnop (ARec a) e2))) e2.
Lemma tnnrc_dot_of_concat_rec_neq_arrow a1 a2 (e1 e2:nnrc) :
a1 ≠ a2 →
tnnrc_ext_rewrites_to (NNRCUnop (ADot a1) (NNRCBinop AConcat e1 (NNRCUnop (ARec a2) e2))) (NNRCUnop (ADot a1) e1).
Lemma tnnrc_merge_concat_to_concat_arrow a1 a2 p1 p2:
a1 ≠ a2 →
tnnrc_ext_rewrites_to (‵[| (a1, p1)|] ⊗ ‵[| (a2, p2)|]) (‵{|‵[| (a1, p1)|] ⊕ ‵[| (a2, p2)|]|}).
Lemma tfor_nil_arrow x e :
tnnrc_ext_rewrites_to (NNRCFor x ‵{||} e) ‵{||}.
Lemma tfor_singleton_to_let_arrow x e1 e2:
tnnrc_ext_rewrites_to (NNRCFor x (NNRCUnop AColl e1) e2)
(NNRCUnop AColl (NNRCLet x e1 e2)).
Lemma tflatten_nil_nnrc_arrow :
tnnrc_ext_rewrites_to (♯flatten(‵{||})) ‵{||}.
Lemma tflatten_singleton_nnrc_arrow e :
tnnrc_ext_rewrites_to (♯flatten(‵{| e |})) e.
Lemma tmap_sigma_fusion_arrow (v1 v2:var) (e1 e2 e3:nnrc) :
¬ In v1 (nnrc_free_vars e3) →
tnnrc_ext_rewrites_to
(NNRCFor v2
(NNRCUnop AFlatten
(NNRCFor v1 e1
(NNRCIf e2 (NNRCUnop AColl (NNRCVar v1)) (NNRCConst (dcoll nil)))))
e3)
(NNRCUnop AFlatten
(NNRCFor v1 e1
(NNRCIf e2
(NNRCUnop AColl (NNRCLet v2 (NNRCVar v1) e3))
(NNRCConst (dcoll nil))))).
Lemma tmap_sigma_fusion_samevar_arrow (v1:var) (e1 e2 e3:nnrc) :
tnnrc_ext_rewrites_to
(NNRCFor v1
(NNRCUnop AFlatten
(NNRCFor v1 e1
(NNRCIf e2 (NNRCUnop AColl (NNRCVar v1)) (NNRCConst (dcoll nil)))))
e3)
(NNRCUnop AFlatten
(NNRCFor v1 e1
(NNRCIf e2
(NNRCUnop AColl e3)
(NNRCConst (dcoll nil))))).
Lemma tlet_inline_disjoint_arrow x e1 e2 :
disjoint (nnrc_bound_vars e2) (nnrc_free_vars e1) →
tnnrc_ext_rewrites_to
(NNRCLet x e1 e2)
(nnrc_subst e2 x e1).
Lemma tlet_inline_arrow sep renamer x e1 e2 :
tnnrc_ext_rewrites_to
(NNRCLet x e1 e2)
(nnrc_subst (unshadow sep renamer (nnrc_free_vars e1) e2) x e1).
Lemma tfor_over_if_arrow x e1 e2 e3 ebody :
tnnrc_ext_rewrites_to (NNRCFor x (NNRCIf e1 e2 e3) ebody)
(NNRCIf e1 (NNRCFor x e2 ebody)
(NNRCFor x e3 ebody)).
Lemma tfor_over_either_disjoint_arrow x e1 xl el xr er ebody:
disjoint (xl::xr::nil) (nnrc_free_vars ebody) →
tnnrc_ext_rewrites_to (NNRCFor x (NNRCEither e1 xl el xr er) ebody)
(NNRCEither e1
xl (NNRCFor x el ebody)
xr (NNRCFor x er ebody)).
Lemma tnnrceither_rename_l_arrow e1 xl el xr er xl' :
¬ In xl' (nnrc_free_vars el) →
¬ In xl' (nnrc_bound_vars el) →
tnnrc_ext_rewrites_to (NNRCEither e1 xl el xr er)
(NNRCEither e1 xl' (nnrc_subst el xl (NNRCVar xl')) xr er).
Lemma tnnrceither_rename_r_arrow e1 xl el xr er xr' :
¬ In xr' (nnrc_free_vars er) →
¬ In xr' (nnrc_bound_vars er) →
tnnrc_ext_rewrites_to (NNRCEither e1 xl el xr er)
(NNRCEither e1 xl el xr' (nnrc_subst er xr (NNRCVar xr'))).
Lemma tfor_over_either_arrow sep x e1 xl el xr er ebody:
tnnrc_ext_rewrites_to (NNRCFor x (NNRCEither e1 xl el xr er) ebody)
( let xl' := really_fresh_in sep xl (nnrc_free_vars el ++ nnrc_bound_vars el) ebody in
let xr' := really_fresh_in sep xr (nnrc_free_vars er ++ nnrc_bound_vars er) ebody in
(NNRCEither e1
xl' (NNRCFor x (nnrc_subst el xl (NNRCVar xl')) ebody)
xr' (NNRCFor x (nnrc_subst er xr (NNRCVar xr')) ebody))).
Lemma tnnrcunop_over_either_arrow op e1 xl el xr er:
tnnrc_ext_rewrites_to
(NNRCUnop op (NNRCEither e1 xl el xr er))
(NNRCEither e1 xl (NNRCUnop op el) xr (NNRCUnop op er)).
Lemma tnnrcunop_over_if_arrow op e1 e2 e3:
tnnrc_ext_rewrites_to
(NNRCUnop op (NNRCIf e1 e2 e3))
(NNRCIf e1 (NNRCUnop op e2) (NNRCUnop op e3)).
Lemma tsigma_to_if_arrow (e1 e2:nnrc) (v:var) :
tnnrc_ext_rewrites_to
(NNRCUnop AFlatten
(NNRCFor v (NNRCUnop AColl e2)
(NNRCIf e1
(NNRCUnop AColl (NNRCVar v))
(NNRCConst (dcoll nil)))))
(NNRCLet v e2 (NNRCIf e1 (NNRCUnop AColl (NNRCVar v)) (NNRCConst (dcoll nil)))).
Lemma tcount_over_flat_for_either_if_nil_arrow v e1 xl e11 e12 xr ehead :
tnnrc_ext_rewrites_to
(♯count(♯flatten(NNRCFor v
ehead (NNRCEither e1 xl
(NNRCIf e11(‵{| e12|}) ‵{||}) xr ‵{||}))))
(♯count(♯flatten(NNRCFor v
ehead (NNRCEither e1 xl
(NNRCIf e11(‵{| ‵(dunit) |}) ‵{||}) xr ‵{||})))).
Lemma tcount_over_flat_for_either_either_nil_arrow v e1 xl e11 xll e12 xrr xr ehead :
tnnrc_ext_rewrites_to
(♯count(♯flatten(NNRCFor v
ehead (NNRCEither e1 xl
(NNRCEither e11 xll (‵{| e12|}) xrr ‵{||}) xr ‵{||}))))
(♯count(♯flatten(NNRCFor v
ehead (NNRCEither e1 xl
(NNRCEither e11 xll (‵{| ‵(dunit) |}) xrr ‵{||}) xr ‵{||})))).
Lemma tnnrcproject_nil p :
π[nil](p) ⇒ᶜ ‵[||].
Lemma tnnrcproject_over_concat_rec_r_in sl s p₁ p₂ :
In s sl →
π[sl](p₁ ⊕ ‵[| (s, p₂) |]) ⇒ᶜ π[remove string_dec s sl](p₁) ⊕ ‵[| (s, p₂) |] .
Lemma tnnrcproject_over_const sl l :
π[sl](NNRCConst (drec l)) ⇒ᶜ NNRCConst (drec (rproject l sl)).
Lemma tnnrcproject_over_rec_in sl s p :
In s sl →
π[sl](‵[| (s, p) |]) ⇒ᶜ ‵[| (s, p) |].
Lemma tnnrcproject_over_rec_nin sl s p :
¬ In s sl →
π[sl](‵[| (s, p) |]) ⇒ᶜ ‵[||].
Lemma tnnrcproject_over_concat_rec_r_nin sl s p₁ p₂ :
¬ In s sl →
π[sl](p₁ ⊕ ‵[| (s, p₂) |]) ⇒ᶜ π[sl](p₁).
Lemma tnnrcproject_over_concat_rec_l_nin sl s p₁ p₂ :
¬ In s sl →
π[sl](‵[| (s, p₁) |] ⊕ p₂) ⇒ᶜ π[sl](p₂).
Lemma tnnrcproject_over_concat_recs_in_in sl s₁ p₁ s₂ p₂ :
In s₁ sl → In s₂ sl →
π[sl](‵[| (s₁, p₁) |] ⊕ ‵[| (s₂, p₂) |]) ⇒ᶜ ‵[| (s₁, p₁) |] ⊕ ‵[| (s₂, p₂) |].
Lemma tnnrcproject_over_nnrcproject sl1 sl2 p :
π[sl1](π[sl2](p)) ⇒ᶜ π[set_inter string_dec sl2 sl1](p).
Lemma tnnrcproject_over_either sl p xl p1 xr p2 :
π[sl](NNRCEither p xl p1 xr p2) ⇒ᶜ NNRCEither p xl (π[sl](p1)) xr (π[sl](p2)).
End TNNRCRewrite.