Module TNRAEnvRewrite
Section TOptimEnv.
Require Import Equivalence.
Require Import Morphisms.
Require Import Setoid.
Require Import EquivDec.
Require Import Program.
Require Import Bool String List ListSet.
Require Import BasicSystem.
Require Import cNRAEnv cNRAEnvIgnore cNRAEnvEq.
Require Import TcNRAEnv TcNRAEnvIgnore TcNRAEnvEq.
Require Import NRAEnvRewrite.
Local Open Scope nraenv_core_scope.
Context {
m:
basic_model}.
Lemma tand_comm_arrow (
q₁
q₂:
nraenv_core) :
q₁ ∧
q₂ ⇒
q₂ ∧
q₁.
Proof.
Lemma tand_comm {τ
c τ
env τ
in} (
q₁
q₂
ql qr:
m ⊧ τ
in ⇝
Bool ⊣ τ
c;τ
env) :
(`
ql = `
q₂ ∧ `
q₁) ->
(`
qr = `
q₁ ∧ `
q₂) ->
ql ≡τ
qr.
Proof.
Lemma tconcat_empty_record_r_arrow q:
q ⊕ ‵[||] ⇒
q.
Proof.
Lemma tconcat_empty_record_l_arrow q:
‵[||] ⊕
q ⇒
q.
Proof.
Lemma tmerge_empty_record_r_arrow q:
q ⊗ ‵[||] ⇒ ‵{|
q |}.
Proof.
unfold tnraenv_core_rewrites_to;
intros.
nraenv_core_inferer.
simpl in *.
inversion H0;
clear H0;
subst.
rtype_equalizer.
subst.
specialize (
H5 eq_refl);
subst;
clear H4.
assert (‵{|
q|} ▷ τ
in >=>
Coll (
Rec Closed τ₃
pf3) ⊣ τ
c;τ
env /\
q ▷ τ
in >=>
Rec Closed τ₃
pf3 ⊣ τ
c;τ
env ).
-
inversion H6;
clear H6;
subst.
clear pf2 pf'.
rewrite merge_bindings_nil_r in H.
rewrite sort_sorted_is_id in H;
try assumption.
inversion H;
clear H;
subst.
assert (
Rec Closed τ₃
pf1 =
Rec Closed τ₃
pf3).
apply rtype_fequal;
reflexivity.
rewrite H in H7.
clear H pf1.
nraenv_core_inferer.
-
econstructor.
elim H0;
clear H0;
intros.
assumption.
elim H0;
clear H0;
intros.
assert ((
q ⊗ ‵[||]) ▷ τ
in >=>
Coll (
Rec Closed τ₃
pf3) ⊣ τ
c;τ
env).
econstructor;
eauto;
try econstructor;
eauto.
apply dtrec_full;
simpl;
assumption.
input_well_typed.
dependent induction τ
out.
assert (
domain dl =
domain rl0)
by (
apply sorted_forall_same_domain;
assumption).
rewrite merge_bindings_nil_r.
rewrite sort_sorted_is_id.
reflexivity.
rewrite H8.
assumption.
-
assert (‵{|
q|} ▷ τ
in >=>
Coll (
Rec Open τ₃
pf3) ⊣ τ
c;τ
env /\
q ▷ τ
in >=>
Rec Open τ₃
pf3 ⊣ τ
c;τ
env ).
inversion H0.
rtype_equalizer;
subst.
inversion H6;
clear H6;
intros.
subst.
econstructor;
eauto.
econstructor;
eauto.
inversion H4.
subst.
rewrite merge_bindings_nil_r in H.
rewrite sort_sorted_is_id in H;
try assumption.
inversion H;
clear H;
subst.
assert (
Rec Open τ₃
pf1 =
Rec Open τ₃
pf3).
apply rtype_fequal;
reflexivity.
rewrite H in H7.
clear H pf1.
assumption.
inversion H4.
subst.
rewrite merge_bindings_nil_r in H.
rewrite sort_sorted_is_id in H;
try assumption.
inversion H;
clear H;
subst.
assert (
Rec Open τ₃
pf1 =
Rec Open τ₃
pf3).
apply rtype_fequal;
reflexivity.
rewrite H in H7;
assumption.
econstructor.
elim H1;
clear H1;
intros;
assumption;
intros.
intros.
input_well_typed.
dependent induction τ
out.
rtype_equalizer.
subst.
inversion H0;
clear H0;
intros.
rtype_equalizer;
subst.
rewrite merge_bindings_nil_r.
rewrite sort_sorted_is_id.
reflexivity.
assert (
domain dl =
domain rl)
by (
apply sorted_forall_same_domain;
assumption).
rewrite H0;
assumption.
Grab Existential Variables.
eauto.
Qed.
Lemma tmerge_empty_record_l_arrow q:
‵[||] ⊗
q ⇒ ‵{|
q |}.
Proof.
Lemma tdot_over_rec_arrow a q :
(‵[| (
a,
q)|]) ·
a ⇒
q.
Proof.
Lemma tdot_over_concat_eq_r_arrow a (
q₁
q₂:
nraenv_core) :
(
q₁ ⊕ ‵[| (
a,
q₂) |])·
a ⇒
q₂.
Proof.
Lemma tdot_over_concat_neq_r_arrow a₁
a₂ (
q₁
q₂:
nraenv_core) :
a₁ <>
a₂ ->
(
q₁ ⊕ ‵[| (
a₁,
q₂) |])·
a₂ ⇒
q₁·
a₂.
Proof.
Lemma tdot_over_concat_neq_l_arrow a₁
a₂ (
q₁
q₂:
nraenv_core) :
a₁ <>
a₂ ->
(‵[| (
a₁,
q₁) |] ⊕
q₂ )·
a₂ ⇒
q₂·
a₂.
Proof.
Lemma tenvdot_from_duplicate_r_arrow a₁
a₂ (
q₁
q₂:
nraenv_core) :
(‵[| (
a₁,
q₁) |] ⊕ ‵[| (
a₂,
q₂) |])·
a₂ ⇒
q₂.
Proof.
Lemma tenvdot_from_duplicate_l_arrow a₁
a₂ (
q₁
q₂:
nraenv_core) :
a₁ <>
a₂ -> (‵[| (
a₁,
q₁) |] ⊕ ‵[| (
a₂,
q₂) |])·
a₁ ⇒
q₁.
Proof.
Lemma tproduct_singletons_arrow a₁
a₂
q₁
q₂:
‵{|‵[| (
a₁,
q₁) |] |} × ‵{| ‵[| (
a₂,
q₂) |] |} ⇒
‵{|‵[| (
a₁,
q₁) |] ⊕ ‵[| (
a₂,
q₂) |] |}.
Proof.
Lemma tproduct_empty_right_arrow q:
q × ‵{| ‵[||] |} ⇒
q.
Proof.
Lemma tproduct_empty_left_arrow q:
‵{| ‵[||] |} ×
q ⇒
q.
Proof.
Lemma tconcat_over_rec_eq s p₁
p₂ :
‵[| (
s,
p₁) |] ⊕ ‵[| (
s,
p₂) |] ⇒ ‵[| (
s,
p₂) |].
Proof.
Lemma tmerge_concat_to_concat_arrow a₁
a₂
q₁
q₂:
a₁ <>
a₂ ->
‵[| (
a₁,
q₁)|] ⊗ ‵[| (
a₂,
q₂) |] ⇒ ‵{|‵[| (
a₁,
q₁)|] ⊕ ‵[| (
a₂,
q₂)|]|}.
Proof.
Lemma tmerge_with_concat_to_concat_arrow a₁
a₂
q₁
q₂:
a₁ <>
a₂ ->
‵[| (
a₁,
q₁)|] ⊗ (‵[| (
a₁,
q₁) |] ⊕ ‵[| (
a₂,
q₂) |]) ⇒ ‵{|‵[| (
a₁,
q₁)|] ⊕ ‵[| (
a₂,
q₂)|]|}.
Proof.
Lemma tselect_over_nil q : σ⟨
q ⟩(‵{||}) ⇒ ‵{||}.
Proof.
Lemma tselect_and_comm_arrow (
q q₁
q₂:
nraenv_core) :
σ⟨
q₁ ∧
q₂ ⟩(
q) ⇒ σ⟨
q₂ ∧
q₁ ⟩(
q).
Proof.
Lemma tselect_and_comm {τ
c τ
env τ
in τ} (
q ql qr:
m ⊧ τ
in ⇝
Coll τ ⊣ τ
c;τ
env)
(
q₁
q₂:
m ⊧ τ ⇝
Bool ⊣ τ
c;τ
env) :
(`
ql = σ⟨ `
q₂ ∧ `
q₁ ⟩(`
q)) ->
(`
qr = σ⟨ `
q₁ ∧ `
q₂ ⟩(`
q)) ->
ql ≡τ
qr.
Proof.
Lemma tselect_and_arrow (
q q₁
q₂:
nraenv_core) :
σ⟨
q₁ ⟩(σ⟨
q₂ ⟩(
q)) ⇒ σ⟨
q₂ ∧
q₁ ⟩(
q).
Proof.
unfold tnraenv_core_rewrites_to;
intros.
nraenv_core_inferer.
split;[
nraenv_core_inferer|
idtac];
intros.
input_well_typed.
dtype_inverter.
autorewrite with alg.
apply lift_dcoll_inversion.
clear eout.
inversion τ
out;
clear τ
out;
subst.
rtype_equalizer.
subst.
induction dout;
try reflexivity;
simpl in *.
inversion H1;
clear H1;
subst.
specialize (
IHdout H4);
clear H4.
rewrite <-
IHdout;
clear IHdout.
simpl.
input_well_typed.
subst;
simpl.
dtype_inverter.
simpl.
destruct (
lift_filter
(
fun x' :
data =>
match brand_relation_brands ⊢ₑ
q₂ @ₑ
x' ⊣
c;
env with
|
Some (
dbool b0) =>
Some b0
|
_ =>
None
end)
dout).
+
destruct x1;
simpl.
*
input_well_typed.
dtype_inverter.
inversion eout0;
subst.
reflexivity.
*
input_well_typed.
destruct (
lift_filter
(
fun x' :
data =>
match brand_relation_brands ⊢ₑ
q₁ @ₑ
x' ⊣
c;
env with
|
Some (
dbool b0) =>
Some b0
|
_ =>
None
end)
l);
reflexivity.
+
destruct (
brand_relation_brands ⊢ₑ
q₁ @ₑ
a ⊣
c;
env);
try reflexivity.
Qed.
Lemma selection_split_and (
q q₁
q₂:
nraenv_core) :
σ⟨
q₂ ∧
q₁ ⟩(
q) ⇒ σ⟨
q₁ ⟩(σ⟨
q₂ ⟩(
q)).
Proof.
unfold tnraenv_core_rewrites_to;
intros.
nraenv_core_inferer.
split;[
nraenv_core_inferer|
idtac];
intros.
input_well_typed.
dtype_inverter.
autorewrite with alg.
apply lift_dcoll_inversion.
clear eout.
inversion τ
out;
clear τ
out;
subst.
rtype_equalizer.
subst.
induction dout;
try reflexivity;
simpl in *.
inversion H1;
clear H1;
subst.
specialize (
IHdout H3);
clear H3.
rewrite IHdout;
clear IHdout.
simpl.
input_well_typed.
subst;
simpl.
dtype_inverter.
simpl.
destruct (
lift_filter
(
fun x' :
data =>
match brand_relation_brands ⊢ₑ
q₂ @ₑ
x' ⊣
c;
env with
|
Some (
dbool b0) =>
Some b0
|
_ =>
None
end)
dout).
+
destruct x1;
simpl.
*
input_well_typed.
dtype_inverter.
inversion eout0;
subst.
reflexivity.
*
input_well_typed.
destruct (
lift_filter
(
fun x' :
data =>
match brand_relation_brands ⊢ₑ
q₁ @ₑ
x' ⊣
c;
env with
|
Some (
dbool b0) =>
Some b0
|
_ =>
None
end)
l);
reflexivity.
+
destruct (
brand_relation_brands ⊢ₑ
q₁ @ₑ
a ⊣
c;
env);
try reflexivity.
Qed.
Lemma tselect_and {τ
c τ
env τ
in τ} (
q ql qr:
m ⊧ τ
in ⇝ (
Coll τ) ⊣ τ
c;τ
env) (
q₁
q₂:
m ⊧ τ ⇝
Bool ⊣ τ
c;τ
env) :
(`
ql = σ⟨ `
q₁ ⟩(σ⟨ `
q₂ ⟩(`
q))) ->
(`
qr = σ⟨ `
q₂ ∧ `
q₁ ⟩(`
q)) ->
(
ql ≡τ
qr).
Proof.
Lemma tselect_comm_arrow (
q q₁
q₂:
nraenv_core) :
σ⟨
q₁ ⟩(σ⟨
q₂ ⟩(
q )) ⇒ σ⟨
q₂ ⟩(σ⟨
q₁ ⟩(
q )).
Proof.
unfold tnraenv_core_rewrites_to;
intros.
assert (
exists τ, σ⟨
q₁ ⟩(σ⟨
q₂ ⟩(
q )) ▷ τ
in >=>
Coll τ ⊣ τ
c;τ
env)
by nraenv_core_inferer.
split;
try assumption;
intros.
nraenv_core_inferer.
elim H0;
clear H0;
intros τ;
intros.
clear H τ
out.
assert (σ⟨
q₂ ⟩(σ⟨
q₁ ⟩(
q )) ▷ τ
in >=>
Coll τ ⊣ τ
c;τ
env)
by nraenv_core_inferer.
assert (
q ▷ τ
in >=>
Coll τ ⊣ τ
c;τ
env)
by nraenv_core_inferer.
assert (
q₁ ▷ τ >=>
Bool ⊣ τ
c;τ
env)
by nraenv_core_inferer.
assert (
q₂ ▷ τ >=>
Bool ⊣ τ
c;τ
env)
by nraenv_core_inferer.
assert (σ⟨
q₁ ∧
q₂ ⟩(
q ) ▷ τ
in >=>
Coll τ ⊣ τ
c;τ
env)
by eauto.
assert (σ⟨
q₂ ∧
q₁ ⟩(
q ) ▷ τ
in >=>
Coll τ ⊣ τ
c;τ
env)
by eauto.
rewrite (
tselect_and (
exist _ q H1)
(
exist _ (σ⟨
q₁ ⟩( σ⟨
q₂ ⟩(
q )))
H0)
(
exist _ (σ⟨
q₂ ∧
q₁ ⟩(
q ))
H5)
(
exist _ q₁
H2) (
exist _ q₂
H3));
try assumption;
try reflexivity.
rewrite (
tselect_and (
exist _ q H1)
(
exist _ (σ⟨
q₂ ⟩( σ⟨
q₁ ⟩(
q )))
H)
(
exist _ (σ⟨
q₁ ∧
q₂ ⟩(
q ))
H4)
(
exist _ q₂
H3) (
exist _ q₁
H2));
try assumption;
try reflexivity.
assert (
q₁ ∧
q₂ ▷ τ >=>
Bool ⊣ τ
c;τ
env)
by eauto.
assert (
q₂ ∧
q₁ ▷ τ >=>
Bool ⊣ τ
c;τ
env)
by eauto.
rewrite (
tselect_and_comm
(
exist _ q H1)
(
exist _ (σ⟨
q₂ ∧
q₁ ⟩(
q ))
H5)
(
exist _ (σ⟨
q₁ ∧
q₂ ⟩(
q ))
H4)
(
exist _ q₁
H2) (
exist _ q₂
H3)
eq_refl eq_refl);
intros;
try assumption;
reflexivity.
Qed.
Lemma tselect_comm {τ
c τ
env τ
in τ} (
q₁
q₂:
m ⊧ τ ⇝
Bool ⊣ τ
c;τ
env) (
q ql qr:
m ⊧ τ
in ⇝ (
Coll τ) ⊣ τ
c;τ
env) :
(`
ql = σ⟨ `
q₁ ⟩(σ⟨ `
q₂ ⟩(`
q))) ->
(`
qr = σ⟨ `
q₂ ⟩(σ⟨ `
q₁ ⟩(`
q))) ->
ql ≡τ
qr.
Proof.
Lemma tenvflatten_coll {τ
c τ
env τ
in τ
out} (
q:
m ⊧ τ
in ⇝
Coll τ
out ⊣ τ
c;τ
env) (
ql qr:
m ⊧ τ
in ⇝
Coll τ
out ⊣ τ
c;τ
env):
(`
ql = ♯
flatten(‵{| `
q |})) -> (`
qr = `
q) ->
ql ≡τ
qr.
Proof.
Lemma tenvflatten_coll_arrow (
q:
nraenv_core):
♯
flatten(‵{|
q |}) ⇒
q.
Proof.
unfold tnraenv_core_rewrites_to;
intros;
simpl.
nraenv_core_inferer.
split;
try assumption;
intros.
input_well_typed.
dtype_inverter.
rewrite app_nil_r;
reflexivity.
Qed.
Lemma tenvflatten_nil_arrow :
♯
flatten(‵{||}) ⇒ ‵{||}.
Proof.
Lemma tenvflatten_map_coll_arrow q₁
q₂ :
♯
flatten(χ⟨ ‵{|
q₁ |} ⟩(
q₂ )) ⇒ χ⟨
q₁ ⟩(
q₂ ).
Proof.
Lemma tflatten_flatten_map_either_nil p₁
p₂
p₃ :
♯
flatten( ♯
flatten(χ⟨
ANEither p₁ ‵{||} ◯
p₂⟩(
p₃))) ⇒
♯
flatten( χ⟨
ANEither( ♯
flatten(
p₁)) ‵{||} ◯
p₂⟩(
p₃)).
Proof.
Lemma tflatten_mapenv_coll_arrow q₁:
♯
flatten(
ANMapEnv (‵{|
q₁ |})) ⇒
ANMapEnv q₁.
Proof.
Lemma tdouble_flatten_map_coll_arrow q₁
q₂
q₃ :
♯
flatten(χ⟨ χ⟨ ‵{|
q₃ |} ⟩(
q₁ ) ⟩(
q₂ )) ⇒ χ⟨ ‵{|
q₃ |} ⟩(♯
flatten(χ⟨
q₁ ⟩(
q₂ ))).
Proof.
Lemma tnested_map_over_singletons_arrow q₁
q₂
q₃:
♯
flatten(χ⟨ σ⟨
q₁ ⟩(‵{|
q₂|}) ⟩(
q₃)) ⇒ σ⟨
q₁ ⟩(χ⟨
q₂ ⟩(
q₃)).
Proof.
Lemma tflatten_over_double_map_with_either_arrow q₁
q₂
q₃
q₄ :
♯
flatten(χ⟨ χ⟨
q₁ ⟩( σ⟨
q₂ ⟩( (
ANEither (‵{|
ID|}) ‵{||}) ◯
q₃ ) ) ⟩(
q₄ ))
⇒ χ⟨
q₁ ⟩( σ⟨
q₂ ⟩( ♯
flatten( χ⟨ (
ANEither (‵{|
ID|}) ‵{||}) ◯
q₃ ⟩(
q₄ ) ) ) ).
Proof.
Lemma tflatten_over_double_map_arrow q₁
q₂
q₃ :
♯
flatten(χ⟨χ⟨
q₁ ⟩( σ⟨
q₂ ⟩(‵{|
ID|}) ) ⟩(
q₃ )) ⇒ χ⟨
q₁ ⟩( σ⟨
q₂ ⟩(
q₃ ) ).
Proof.
Lemma tselect_over_flatten p₁
p₂ :
σ⟨
p₁⟩(♯
flatten(
p₂)) ⇒ ♯
flatten(χ⟨σ⟨
p₁⟩(
ID)⟩(
p₂)).
Proof.
Lemma tselect_over_flatten_b p₁
p₂ :
♯
flatten(χ⟨σ⟨
p₁⟩(
ID)⟩(
p₂)) ⇒ σ⟨
p₁⟩(♯
flatten(
p₂)).
Proof.
Lemma tmap_over_flatten p₁
p₂ :
χ⟨
p₁⟩(♯
flatten(
p₂)) ⇒ ♯
flatten(χ⟨χ⟨
p₁⟩(
ID)⟩(
p₂)).
Proof.
Lemma tmap_over_flatten_b p₁
p₂ :
♯
flatten(χ⟨χ⟨
p₁⟩(
ID)⟩(
p₂)) ⇒ χ⟨
p₁⟩(♯
flatten(
p₂)).
Proof.
Lemma tselect_over_either p₁
p₂
p₃ :
σ⟨
p₁⟩(
ANEither p₂
p₃) ⇒
ANEither (σ⟨
p₁⟩(
p₂)) (σ⟨
p₁⟩(
p₃)).
Proof.
Lemma tmap_over_nil q : χ⟨
q ⟩(‵{||}) ⇒ ‵{||}.
Proof.
Lemma tenvmap_into_id_arrow q :
χ⟨
ID ⟩(
q ) ⇒
q.
Proof.
unfold tnraenv_core_rewrites_to;
intros.
nraenv_core_inferer.
split;
try assumption;
intros;
simpl.
input_well_typed.
dtype_inverter.
clear eout.
inversion τ
out;
clear τ
out;
subst.
rtype_equalizer.
subst.
induction dout;
try reflexivity.
inversion H1;
clear H1;
subst.
specialize (
IHdout H3);
clear H3.
simpl.
unfold lift in *.
destruct (
rmap (
fun x :
data =>
Some x)
dout);
congruence.
Qed.
Lemma tenvmap_map_compose_arrow q₁
q₂
q:
χ⟨
q₁ ⟩( χ⟨
q₂ ⟩(
q ) ) ⇒ χ⟨
q₁ ◯
q₂ ⟩(
q ).
Proof.
Lemma tenvmap_singleton_arrow q₁
q₂:
χ⟨
q₁ ⟩( ‵{|
q₂ |} ) ⇒ ‵{|
q₁ ◯
q₂ |}.
Proof.
Lemma tmap_full_over_select_arrow q q₁
q₂:
χ⟨
q₂ ⟩(σ⟨
q₁ ⟩(‵{|
q |})) ⇒ χ⟨
q₂ ◯
q ⟩(σ⟨
q₁ ◯
q ⟩(‵{|
ID |})).
Proof.
Lemma tmap_over_map_split p₁
p₂
p₃ :
χ⟨χ⟨
p₁ ⟩(
p₂) ⟩(
p₃) ⇒ χ⟨χ⟨
p₁ ⟩(
ID) ⟩(χ⟨
p₂⟩(
p₃)).
apply (
rewrites_typed_with_untyped _ _ (
map_over_map_split p₁
p₂
p₃)).
intros.
nraenv_core_inferer.
Qed.
Lemma tflip_env6_arrow q₁ q₂:
χ⟨ ENV ⊗ ID ⟩(σ⟨ q₁ ⟩(ENV ⊗ q₂)) ⇒ χ⟨ ‵{|ID|} ⟩(σ⟨ q₁ ⟩(ENV ⊗ q₂)).
Proof.
unfold tnraenv_core_rewrites_to;
intros.
nraenv_core_inferer.
econstructor;
eauto.
-
assert (
merge_bindings τ₁ τ₂2 =
Some τ₂2).
apply (
merge_idem _ τ₂
_ pf1 pf4);
assumption.
rewrite H0 in H;
inversion H.
nraenv_core_inferer.
econstructor;
eauto.
econstructor;
eauto.
assert (
Rec Closed τ₃
pf2 =
Rec Closed τ₃
pf3).
apply rtype_fequal;
reflexivity.
rewrite <-
H1;
assumption.
-
intros.
input_well_typed;
simpl.
dependent induction τ
out.
rtype_equalizer.
subst;
simpl.
case_eq env;
intros;
try reflexivity;
simpl.
subst.
case_eq (
merge_bindings l dl);
intros;
try reflexivity;
simpl.
autorewrite with alg.
destruct (
brand_relation_brands ⊢ₑ
q₁ @ₑ
drec l0 ⊣
c;(
drec l));
try reflexivity;
simpl.
destruct d;
try reflexivity;
simpl.
destruct b;
try reflexivity;
simpl.
rewrite (
merge_idem l dl l0);
try reflexivity;
try assumption.
+
dependent induction dt_env.
rtype_equalizer.
subst.
apply (
sorted_forall_sorted l rl0);
assumption.
+
apply (
sorted_forall_sorted dl rl);
assumption.
-
econstructor;
eauto.
+
assert (
merge_bindings τ₁ τ₂2 =
Some τ₂2).
apply (
merge_idem _ τ₂
_ pf1 pf4);
assumption.
rewrite H0 in H;
inversion H.
nraenv_core_inferer.
econstructor;
eauto.
econstructor;
eauto.
assert (
Rec Open τ₃
pf2 =
Rec Open τ₃
pf3).
apply rtype_fequal;
reflexivity.
rewrite <-
H1;
assumption.
+
intros.
input_well_typed;
simpl.
invcs τ
out.
rtype_equalizer.
subst;
simpl.
case_eq env;
intros;
try reflexivity;
simpl.
subst.
case_eq (
merge_bindings l dl);
intros;
try reflexivity;
simpl.
autorewrite with alg.
destruct (
brand_relation_brands ⊢ₑ
q₁ @ₑ
drec l0 ⊣
c;(
drec l));
try reflexivity;
simpl.
destruct d;
try reflexivity;
simpl.
destruct b;
try reflexivity;
simpl.
rewrite (
merge_idem l dl l0);
try reflexivity;
try assumption.
*
invcs dt_env.
rtype_equalizer.
subst.
apply (
sorted_forall_sorted l rl0);
assumption.
*
apply (
sorted_forall_sorted dl rl);
assumption.
Qed.
Lemma tmap_over_either p₁ p₂ p₃ :
χ⟨p₁⟩( ANEither p₂ p₃) ⇒ ANEither (χ⟨p₁⟩(p₂)) (χ⟨p₁⟩(p₃)).
Proof.
Lemma tmap_over_either_app p₁ p₂ p₃ p₄:
χ⟨p₁⟩( ANEither p₂ p₃ ◯ p₄) ⇒ ANEither (χ⟨p₁⟩(p₂)) (χ⟨p₁⟩(p₃)) ◯ p₄.
Proof.
Lemma tapp_over_const_arrow d q:
(ANConst d) ◯ q ⇒ (ANConst d).
Proof.
unfold tnraenv_core_rewrites_to;
intros;
simpl.
nraenv_core_inferer.
econstructor;
eauto.
intros.
input_well_typed.
reflexivity.
Qed.
Lemma tapp_over_env_arrow q :
ENV ◯ q ⇒ ENV.
Proof.
unfold tnraenv_core_rewrites_to;
intros.
nraenv_core_inferer.
econstructor;
eauto;
intros.
input_well_typed;
reflexivity.
Qed.
Lemma tapp_over_id_r_arrow q:
q ◯ ID ⇒ q.
Proof.
Lemma tapp_over_id_l_arrow q:
ID ◯ q ⇒ q.
Proof.
Lemma tapp_over_unop_arrow u q₁ q₂:
(ANUnop u q₁) ◯ q₂ ⇒ (ANUnop u (q₁ ◯ q₂)).
Proof.
Lemma tapp_over_binop_arrow b q q₁ q₂:
(ANBinop b q₂ q₁) ◯ q ⇒ (ANBinop b (q₂ ◯ q) (q₁ ◯ q)).
Proof.
intros.
unfold tnraenv_core_rewrites_to;
intros.
nraenv_core_inferer.
econstructor;
eauto;
intros.
input_well_typed;
reflexivity.
Qed.
Lemma tapp_over_map_arrow q q₁ q₂:
(χ⟨q₁⟩(q₂)) ◯ q ⇒ χ⟨ q₁ ⟩(q₂ ◯ q).
Proof.
Lemma tapp_over_mapconcat_arrow q q₁ q₂:
⋈ᵈ⟨ q₁ ⟩( q₂ ) ◯ q ⇒ ⋈ᵈ⟨ q₁ ⟩( q₂ ◯ q ).
Proof.
Lemma tapp_over_product_arrow q q₁ q₂:
(q₁ × q₂) ◯ q ⇒ (q₁ ◯ q) × (q₂ ◯ q).
Proof.
Lemma tapp_over_select_arrow q q₁ q₂:
(σ⟨ q₁ ⟩( q₂ )) ◯ q ⇒ (σ⟨ q₁ ⟩( q₂ ◯ q )).
Proof.
Lemma tapp_over_select_back_arrow q q₁ q₂:
(σ⟨ q₁ ⟩( q₂ ◯ q )) ⇒ (σ⟨ q₁ ⟩( q₂ )) ◯ q.
Proof.
Lemma tapp_over_app_arrow q₁ q₂ q₃:
(q₁ ◯ q₂) ◯ q₃ ⇒ q₁ ◯ (q₂ ◯ q₃).
Proof.
Lemma tselect_over_app_either p₁ p₂ p₃ p₄ :
σ⟨p₁⟩( ANEither p₂ p₃ ◯ p₄ ) ⇒ ANEither (σ⟨p₁⟩(p₂)) (σ⟨p₁⟩(p₃)) ◯ p₄.
Proof.
Lemma tappenv_over_const_arrow d q:
(ANConst d) ◯ₑ q ⇒ (ANConst d).
Proof.
unfold tnraenv_core_rewrites_to;
intros;
simpl.
nraenv_core_inferer.
econstructor;
eauto.
intros.
input_well_typed.
reflexivity.
Qed.
Lemma tappenv_over_id_l_arrow q:
ID ◯ₑ q ⇒ ID.
Proof.
unfold tnraenv_core_rewrites_to;
intros.
nraenv_core_inferer.
econstructor;
eauto;
intros.
input_well_typed;
reflexivity.
Qed.
Lemma tapp_over_ignoreid_arrow q₁ q₂:
nraenv_core_ignores_id q₁ -> q₁ ◯ q₂ ⇒ q₁.
Proof.
Lemma tappenv_over_env_l_arrow q:
ENV ◯ₑ q ⇒ q.
Proof.
Lemma tappenv_over_env_r_arrow q:
q ◯ₑ ENV ⇒ q.
Proof.
Lemma tappenv_over_unop_arrow u q₁ q₂:
(ANUnop u q₁) ◯ₑ q₂ ⇒ (ANUnop u (q₁ ◯ₑ q₂)).
Proof.
Lemma tunop_over_either u p₁ p₂ :
ANUnop u (ANEither p₁ p₂) ⇒ ANEither (ANUnop u p₁)(ANUnop u p₂).
Proof.
Lemma tunop_over_either_app u p₁ p₂ p₃:
ANUnop u (ANEither p₁ p₂ ◯ p₃) ⇒ ANEither (ANUnop u p₁)(ANUnop u p₂) ◯ p₃.
Proof.
Lemma tappenv_over_binop b q₁ q₂ q :
(ANBinop b q₁ q₂) ◯ₑ q ⇒ (ANBinop b (q₁ ◯ₑ q) (q₂ ◯ₑ q)).
Proof.
unfold tnraenv_core_rewrites_to;
intros.
nraenv_core_inferer.
econstructor;
eauto;
intros.
input_well_typed.
reflexivity.
Qed.
Lemma tappenv_over_map_arrow q q₁ q₂:
nraenv_core_ignores_id q ->
χ⟨ q₁ ⟩( q₂ ) ◯ₑ q ⇒ χ⟨ q₁ ◯ₑ q ⟩( q₂ ◯ₑ q ).
Proof.
Lemma tappenv_over_map_nraenv_core_ignores_env_arrow q₁ q₂:
nraenv_core_ignores_env q₁ ->
χ⟨ q₁ ⟩( q₂ ) ◯ₑ ANID ⇒ χ⟨ q₁ ◯ₑ ANID ⟩( q₂ ◯ₑ ANID ).
Proof.
Lemma tappenv_over_select_arrow q q₁ q₂:
nraenv_core_ignores_id q ->
σ⟨ q₁ ⟩( q₂ ) ◯ₑ q ⇒ σ⟨ q₁ ◯ₑ q ⟩( q₂ ◯ₑ q ).
Proof.
Lemma tappenv_over_appenv_arrow q q₁ q₂:
(q₁ ◯ₑ q₂) ◯ₑ q ⇒ q₁ ◯ₑ (q₂ ◯ₑ q).
Proof.
unfold tnraenv_core_rewrites_to;
intros.
nraenv_core_inferer.
econstructor;
eauto.
intros.
input_well_typed;
reflexivity.
Qed.
Lemma tappenv_over_app_arrow q q₁ q₂:
nraenv_core_ignores_id q -> (q₁ ◯ q₂) ◯ₑ q ⇒ (q₁ ◯ₑ q) ◯ (q₂ ◯ₑ q).
Proof.
Lemma tappenv_over_app_ie_arrow p1 p2 p3:
nraenv_core_ignores_env p3 ->
((p3 ◯ p2) ◯ₑ p1) ⇒ p3 ◯ (p2 ◯ₑ p1).
Proof.
Lemma tapp_over_appenv_arrow q q₁ q₂:
nraenv_core_ignores_id q₁ -> (q₁ ◯ₑ q₂) ◯ q ⇒ q₁ ◯ₑ (q₂ ◯ q).
Proof.
Lemma tappenv_over_ignoreenv_arrow q₁ q₂:
nraenv_core_ignores_env q₁ -> q₁ ◯ₑ q₂ ⇒ q₁.
Proof.
Lemma tappenv_over_env_merge_l_arrow q₁ q:
nraenv_core_ignores_env q₁ ->
ANAppEnv (ENV ⊗ q₁) q ⇒ q ⊗ q₁.
Proof.
Lemma tflip_env1_arrow q :
(χ⟨ ENV ⟩(σ⟨ q ⟩(‵{|ID|}))) ◯ₑ ID ⇒ σ⟨ q ⟩(‵{|ID|}) ◯ₑ ID.
Proof.
Lemma tflip_env4_arrow q₁ q₂:
nraenv_core_ignores_env q₁ -> (χ⟨ENV⟩( σ⟨ q₁ ⟩(‵{|ID|}))) ◯ₑ q₂ ⇒ χ⟨q₂⟩( σ⟨ q₁ ⟩(‵{|ID|})).
Proof.
Lemma tflip_env2_arrow q :
σ⟨ q ⟩(‵{|ID|}) ◯ₑ ID ⇒ σ⟨ q ◯ₑ ID ⟩(‵{|ID|}).
Proof.
Lemma tflatten_through_appenv_arrow q₁ q₂ :
♯flatten(q₁ ◯ₑ q₂) ⇒ ♯flatten(q₁) ◯ₑ q₂.
Proof.
Lemma tappenv_through_either q₁ q₂ q₃:
nraenv_core_ignores_id q₃ ->
ANEither q₁ q₂ ◯ₑ q₃ ⇒ ANEither (q₁ ◯ₑ q₃) (q₂ ◯ₑ q₃).
Proof.
Lemma tmapenv_to_env_arrow q :
(ANMapEnv (ENV)) ◯ q ⇒ ENV.
Proof.
unfold tnraenv_core_rewrites_to;
intros;
simpl.
nraenv_core_inferer.
econstructor;
eauto.
intros.
input_well_typed;
simpl.
dtype_inverter.
rewrite rmap_id.
reflexivity.
Qed.
Lemma tmapenv_over_singleton_arrow q₁ q₂ :
(ANMapEnv q₁) ◯ₑ (‵{|q₂|}) ⇒ ‵{| q₁ ◯ₑ q₂ |}.
Proof.
Lemma tmapenv_to_map_arrow q₁ q₂:
nraenv_core_ignores_id q₁ ->
(ANMapEnv q₁) ◯ₑ q₂ ⇒ χ⟨ q₁ ◯ₑ ID ⟩(q₂).
Proof.
Lemma tcompose_selects_in_mapenv_arrow q₁ q₂ :
(♯flatten(ANMapEnv (χ⟨ENV⟩(σ⟨ q₁ ⟩( ‵{| ID |}))))) ◯ₑ (χ⟨ENV⟩(σ⟨ q₂ ⟩( ‵{| ID |})))
⇒ (χ⟨ENV⟩(σ⟨ q₁ ⟩(σ⟨ q₂ ⟩( ‵{| ID |})))).
Proof.
Lemma tappenv_mapenv_to_map_arrow q a:
ANAppEnv (ANMapEnv q) (ENV ⊗ ‵[| (a, ID)|]) ⇒
χ⟨(q ◯ (ANUnop (ADot a) ANEnv)) ◯ₑ ID⟩( (ENV ⊗ ‵[| (a, ID)|]) ).
Proof.
Lemma tappenv_flatten_mapenv_to_map_arrow q a:
ANAppEnv (♯flatten(ANMapEnv q)) (ENV ⊗ ‵[| (a, ID)|]) ⇒
♯flatten(χ⟨(q ◯ (ANUnop (ADot a) ANEnv)) ◯ₑ ID⟩( (ENV ⊗ ‵[| (a, ID)|]) )).
Proof.
Lemma ttostring_dstring_arrow s:
(ANUnop AToString (ANConst (dstring s))) ⇒ (ANConst (dstring s)).
Proof.
Lemma ttostring_tostring_arrow q:
(ANUnop AToString (ANUnop AToString q)) ⇒ (ANUnop AToString q).
Proof.
Lemma ttostring_sconcat_arrow q₁ q₂:
(ANUnop AToString (ANBinop ASConcat q₁ q₂)) ⇒ (ANBinop ASConcat q₁ q₂).
Proof.
unfold tnraenv_core_rewrites_to;
intros;
simpl.
nraenv_core_inferer.
econstructor;
eauto.
-
inversion H3;
clear H3;
subst.
inversion H2;
clear H2;
subst.
econstructor;
eauto.
-
intros.
input_well_typed;
simpl.
case_eq (
unsdstring append dout dout0);
intros;
try reflexivity;
simpl.
generalize (
unsdstring_is_string append dout dout0 d H);
intros.
elim H0;
clear H0;
intros.
rewrite H0;
reflexivity.
Qed.
Lemma trproject_nil p :
π[nil](p) ⇒ ‵[||].
Proof.
red;
simpl;
intros.
nraenv_core_inferer.
split.
-
econstructor.
apply dtrec_full.
simpl.
rewrite rproject_nil_r;
trivial.
-
intros.
input_well_typed.
inversion τ
out.
rewrite rproject_nil_r.
trivial.
Qed.
Lemma trproject_over_concat_rec_r_in sl s p₁ p₂ :
In s sl ->
π[sl](p₁ ⊕ ‵[| (s, p₂) |]) ⇒ π[remove string_dec s sl](p₁) ⊕ ‵[| (s, p₂) |] .
Proof.
Lemma trproject_over_const sl l :
π[sl](ANConst (drec l)) ⇒ ANConst (drec (rproject l sl)).
Proof.
Lemma trproject_over_rec_in sl s p :
In s sl ->
π[sl](‵[| (s, p) |]) ⇒ ‵[| (s, p) |].
Proof.
Lemma trproject_over_rec_nin sl s p :
~ In s sl ->
π[sl](‵[| (s, p) |]) ⇒ ‵[||].
Proof.
Lemma trproject_over_concat_rec_r_nin sl s p₁ p₂ :
~ In s sl ->
π[sl](p₁ ⊕ ‵[| (s, p₂) |]) ⇒ π[sl](p₁).
Proof.
Lemma trproject_over_concat_rec_l_nin sl s p₁ p₂ :
~ In s sl ->
π[sl](‵[| (s, p₁) |] ⊕ p₂) ⇒ π[sl](p₂).
Proof.
Lemma trproject_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₂) |].
Proof.
Lemma trproject_over_rproject sl1 sl2 p :
π[sl1](π[sl2](p)) ⇒ π[set_inter string_dec sl2 sl1](p).
Proof.
Lemma trproject_over_either sl p1 p2 :
π[sl](ANEither p1 p2) ⇒ ANEither (π[sl](p1)) (π[sl](p2)).
Proof.
Lemma tcount_over_map p₁ p₂ :
♯count(χ⟨p₁⟩(p₂)) ⇒ ♯count(p₂).
Proof.
red;
intros;
split.
-
nraenv_core_inferer.
inversion H2;
rtype_equalizer;
subst.
nraenv_core_inferer.
-
intros.
nraenv_core_inferer.
input_well_typed.
destruct dout;
simpl;
trivial.
clear eout.
revert l τ
out0.
induction l;
simpl;
trivial.
intros.
inversion τ
out0.
rtype_equalizer;
subst.
inversion H3;
subst.
assert (
typ:
dcoll l ▹
Coll τ₁)
by (
econstructor;
trivial).
specialize (
IHl typ).
input_well_typed.
unfold olift in IHl.
match_case_in IHl; [
intros ?
eqq |
intros eqq];
rewrite eqq in IHl;
simpl in *;
try discriminate.
apply some_lift in eqq.
destruct eqq as [?
eqq ?];
subst.
apply some_lift in IHl.
destruct IHl as [?
IHl ?];
subst.
inversion e;
clear e;
subst.
rewrite eqq;
simpl.
simpl in IHl.
inversion IHl;
clear IHl.
apply of_nat_inv in H0.
congruence.
Qed.
Lemma tcount_over_flat_map_map p₁ p₂ p₃ :
♯count(♯flatten(χ⟨χ⟨p₁⟩(p₂)⟩(p₃))) ⇒
♯count(♯flatten(χ⟨p₂⟩(p₃))).
Proof.
Lemma tmap_over_either_nil_b p₁ p₂ :
ANEither (χ⟨p₁⟩(p₂)) ‵{||} ⇒ χ⟨p₁⟩(ANEither p₂ ‵{||}).
Proof.
Lemma tcount_over_flat_map_either_nil_map p₁ p₂ p₃ :
♯count(♯flatten(χ⟨ANEither (χ⟨p₁⟩(p₂)) ‵{||}⟩(p₃))) ⇒
♯count(♯flatten(χ⟨ANEither p₂ ‵{||}⟩(p₃))).
Proof.
Lemma tcount_over_flat_map_either_nil_app_map p₁ p₂ p₃ p₄:
♯count(♯flatten(χ⟨ANEither (χ⟨p₁⟩(p₂)) ‵{||} ◯ p₄⟩(p₃))) ⇒
♯count(♯flatten(χ⟨ANEither p₂ ‵{||} ◯ p₄⟩(p₃))).
Proof.
Lemma tcount_over_flat_map_either_nil_app_singleton p₁ p₂ p₃:
♯count(♯flatten(χ⟨ANEither (‵{| p₁ |}) ‵{||} ◯ p₃⟩(p₂))) ⇒
♯count(♯flatten(χ⟨ANEither (‵{| ANConst dunit |}) ‵{||} ◯ p₃⟩(p₂))).
Proof.
red;
intros;
split.
-
nraenv_core_inferer.
inversion H2;
rtype_equalizer;
subst.
nraenv_core_inferer.
econstructor.
2: (
repeat econstructor;
simpl;
eauto).
econstructor.
-
intros.
nraenv_core_inferer.
input_well_typed.
destruct dout;
simpl;
trivial.
clear eout.
revert l τ
out0.
induction l;
simpl;
trivial.
intros.
inversion τ
out0.
rtype_equalizer;
subst.
inversion H3;
subst.
assert (
typ:
dcoll l ▹
Coll τ₁)
by (
econstructor;
trivial).
specialize (
IHl typ).
input_well_typed.
case_eq ((
rmap
(
fun x0 :
data =>
olift
(
fun x' :
data =>
match x'
with
|
dleft dl =>
olift (
fun d1 :
data =>
Some (
dcoll [
d1]))
(
brand_relation_brands ⊢ₑ
p₁ @ₑ
dl ⊣
c;
env)
|
dright _ =>
Some (
dcoll [])
|
_ =>
None
end) (
brand_relation_brands ⊢ₑ
p₃ @ₑ
x0 ⊣
c;
env))
l))
; [
intros ?
eqq |
intros eqq];
rewrite eqq in IHl;
simpl in *;
try discriminate.
+
unfold olift in IHl |- *.
case_eq ((
rmap
(
fun x0 :
data =>
match @
brand_relation_brands brand_model_relation ⊢ₑ
p₃ @ₑ
x0 ⊣
c;
env with
|
Some (
dleft _) =>
Some (
dcoll [
dunit])
|
Some (
dright _) =>
Some (
dcoll [])
|
Some _ =>
None
|
None =>
None
end)
l))
; [
intros ?
eqq1 |
intros eqq1];
rewrite eqq1 in IHl;
simpl in *;
try discriminate.
* {
match_case_in IHl; [
intros ?
eqq2 |
intros eqq2];
rewrite eqq2 in IHl;
simpl in *;
try discriminate;
(
match_case_in IHl; [
intros ?
eqq3 |
intros eqq3];
rewrite eqq3 in IHl;
simpl in *;
try discriminate).
-
apply some_lift in eqq2;
destruct eqq2 as [?
eqq2 ?];
subst.
apply some_lift in eqq3;
destruct eqq3 as [?
eqq3 ?];
subst.
simpl in IHl.
inversion IHl;
clear IHl.
apply of_nat_inv in H1.
unfold olift.
destruct dout;
simpl;
trivial.
+
inversion τ
out1;
clear τ
out1.
rtype_equalizer.
subst.
input_well_typed.
rewrite (
rflatten_cons _ _ _ eqq2).
simpl.
rewrite H1.
rewrite (
rflatten_cons _ _ _ eqq3).
simpl.
trivial.
+
rewrite (
rflatten_cons _ _ _ eqq2).
rewrite (
rflatten_cons _ _ _ eqq3).
simpl.
rewrite H1.
trivial.
-
apply some_lift in eqq2;
destruct eqq2 as [?
eqq2 ?];
subst.
apply none_lift in eqq3.
simpl in IHl.
discriminate.
-
apply none_lift in eqq2.
apply some_lift in eqq3;
destruct eqq3 as [?
eqq3 ?];
subst.
destruct eqq3 as [?
eqq3 ?];
subst.
simpl in IHl.
discriminate.
-
apply none_lift in eqq2.
apply none_lift in eqq3.
unfold olift.
destruct dout;
simpl;
trivial.
+
inversion τ
out1;
clear τ
out1;
rtype_equalizer.
subst.
input_well_typed.
rewrite (
rflatten_cons_none _ _ eqq2).
simpl.
rewrite (
rflatten_cons_none _ _ eqq3).
simpl.
trivial.
+
rewrite (
rflatten_cons_none _ _ eqq2).
simpl.
rewrite (
rflatten_cons_none _ _ eqq3).
simpl.
trivial.
}
* {
match_case_in IHl; [
intros ?
eqq2 |
intros eqq2];
rewrite eqq2 in IHl;
simpl in *;
try discriminate.
-
apply some_lift in eqq2;
destruct eqq2 as [?
eqq2 ?];
subst.
simpl in IHl.
discriminate.
-
apply none_lift in eqq2.
unfold olift.
destruct dout;
inversion τ
out1;
clear τ
out1.
+
rtype_equalizer.
subst.
input_well_typed.
rewrite (
rflatten_cons_none _ _ eqq2).
simpl.
trivial.
+
simpl.
rewrite (
rflatten_cons_none _ _ eqq2).
simpl.
trivial.
}
+
unfold olift in IHl.
case_eq ((
rmap
(
fun x0 :
data =>
match @
brand_relation_brands brand_model_relation ⊢ₑ
p₃ @ₑ
x0 ⊣
c;
env with
|
Some (
dleft _) =>
Some (
dcoll [
dunit])
|
Some (
dright _) =>
Some (
dcoll [])
|
Some _ =>
None
|
None =>
None
end)
l))
; [
intros ?
eqq1 |
intros eqq1];
rewrite eqq1 in IHl;
simpl in *;
try discriminate.
* {
match_case_in IHl; [
intros ?
eqq2 |
intros eqq2];
rewrite eqq2 in IHl;
simpl in *;
try discriminate.
-
apply some_lift in eqq2;
destruct eqq2 as [?
eqq2 ?];
subst.
simpl in IHl.
discriminate.
-
apply none_lift in eqq2.
unfold olift.
rewrite eqq1.
destruct dout;
inversion τ
out1;
clear τ
out1.
+
rtype_equalizer.
subst.
input_well_typed.
rewrite (
rflatten_cons_none _ _ eqq2).
simpl.
trivial.
+
simpl.
rewrite (
rflatten_cons_none _ _ eqq2).
simpl.
trivial.
}
*
unfold olift;
rewrite eqq1;
simpl.
{
destruct dout;
inversion τ
out1;
clear τ
out1.
-
rtype_equalizer.
subst.
input_well_typed.
trivial.
-
simpl;
trivial.
}
Qed.
Lemma tmapconcat_over_singleton p₁ :
⋈ᵈ⟨ p₁ ⟩(‵{| ‵[||] |}) ⇒ p₁ ◯ (‵[||]).
Proof.
composite lemmas: these are just composites of previous rewrites.
They are here since the optimizer uses them.
Lemma tmap_over_flatten_map (p₁ p₂ p₃: nraenv_core) :
χ⟨p₁⟩(♯flatten(χ⟨p₂⟩(p₃))) ⇒ ♯flatten(χ⟨χ⟨p₁⟩(p₂)⟩(p₃)).
Proof.
Lemma tdup_elim (q:nraenv_core) :
nodupA q -> ♯distinct(q) ⇒ q.
Proof.
Lemma tselect_union_distr (q₀ q₁ q₂: nraenv_core) :
σ⟨ q₀ ⟩(q₁ ⋃ q₂) ⇒ σ⟨ q₀ ⟩(q₁) ⋃ σ⟨ q₀ ⟩(q₂).
Proof.
End TOptimEnv.
Hint Rewrite @tmerge_empty_record_r_arrow : tnraenv_core_optim.
Hint Rewrite @tmerge_empty_record_l_arrow : tnraenv_core_optim.
Hint Rewrite @tmapenv_to_env_arrow : tnraenv_core_optim.
Hint Rewrite @tselect_and_arrow : tnraenv_core_optim.
Hint Rewrite @tflatten_through_appenv_arrow : tnraenv_core_optim.
Hint Rewrite @tflatten_mapenv_coll_arrow : tnraenv_core_optim.
Hint Rewrite @tflatten_over_double_map_arrow : tnraenv_core_optim.
Hint Rewrite @tflatten_over_double_map_with_either_arrow : tnraenv_core_optim.
Hint Rewrite @tenvflatten_map_coll_arrow : tnraenv_core_optim.
Hint Rewrite @tenvmap_into_id_arrow : tnraenv_core_optim.
Hint Rewrite @tenvmap_map_compose_arrow : tnraenv_core_optim.
Hint Rewrite @tenvmap_singleton_arrow : tnraenv_core_optim.
Hint Rewrite @tenvflatten_coll_arrow : tnraenv_core_optim.
Hint Rewrite @tenvflatten_nil_arrow : tnraenv_core_optim.
Hint Rewrite @tapp_over_const_arrow : tnraenv_core_optim.
Hint Rewrite @tapp_over_env_arrow : tnraenv_core_optim.
Hint Rewrite @tapp_over_id_r_arrow : tnraenv_core_optim.
Hint Rewrite @tapp_over_id_l_arrow : tnraenv_core_optim.
Hint Rewrite @tapp_over_app_arrow : tnraenv_core_optim.
Hint Rewrite @tapp_over_unop_arrow : tnraenv_core_optim.
Hint Rewrite @tapp_over_map_arrow : tnraenv_core_optim.
Hint Rewrite @tapp_over_select_arrow : tnraenv_core_optim.
Hint Rewrite @tproduct_singletons_arrow : tnraenv_core_optim.
Hint Rewrite @tdouble_flatten_map_coll_arrow : tnraenv_core_optim.
Hint Rewrite @ttostring_dstring_arrow : tnraenv_core_optim.
Hint Rewrite @ttostring_tostring_arrow : tnraenv_core_optim.
Hint Rewrite @ttostring_sconcat_arrow : tnraenv_core_optim.
Hint Rewrite @tappenv_over_env_l_arrow : tnraenv_core_optim.
Hint Rewrite @tappenv_over_env_r_arrow : tnraenv_core_optim.
Hint Rewrite @tappenv_over_appenv_arrow : tnraenv_core_optim.
Hint Rewrite @tappenv_over_app_arrow : tnraenv_core_optim.
Hint Rewrite @tappenv_over_app_ie_arrow : tnraenv_core_optim.
Hint Rewrite @tcompose_selects_in_mapenv_arrow : tnraenv_core_optim.
Hint Rewrite @tappenv_flatten_mapenv_to_map_arrow : tnraenv_core_optim.
Hint Rewrite @tappenv_over_const_arrow : tnraenv_core_optim.
Hint Rewrite @tflip_env1_arrow : tnraenv_core_optim.
Hint Rewrite @tflip_env2_arrow : tnraenv_core_optim.
Hint Rewrite @tmapenv_over_singleton_arrow : tnraenv_core_optim.
Hint Rewrite @tflip_env4_arrow : tnraenv_core_optim.
Hint Rewrite @tappenv_over_binop : tnraenv_core_optim.
Hint Rewrite @tflip_env6_arrow : tnraenv_core_optim.
Hint Rewrite @tmapenv_to_map_arrow : tnraenv_core_optim.
Hint Rewrite @tmerge_concat_to_concat_arrow : tnraenv_core_optim.
Hint Rewrite @tmerge_with_concat_to_concat_arrow : tnraenv_core_optim.
Hint Rewrite @tappenv_mapenv_to_map_arrow : tnraenv_core_optim.
Hint Rewrite @tmap_over_nil : tnraenv_core_optim.
Hint Rewrite @tselect_over_nil : tnraenv_core_optim.
Hint Rewrite @tmap_over_either : tnraenv_core_optim.
Hint Rewrite @tmap_over_either_app : tnraenv_core_optim.
Hint Rewrite @tselect_over_either : tnraenv_core_optim.
Hint Rewrite @tselect_over_app_either : tnraenv_core_optim.
Hint Rewrite @tappenv_through_either : tnraenv_core_optim.
Hint Rewrite @tcount_over_map : tnraenv_core_optim.
Hint Rewrite @tcount_over_flat_map_map : tnraenv_core_optim.
Hint Rewrite @tcount_over_flat_map_either_nil_map : tnraenv_core_optim.
Hint Rewrite @tcount_over_flat_map_either_nil_app_map : tnraenv_core_optim.
Hint Rewrite @tunop_over_either : tnraenv_core_optim.
Hint Rewrite @tunop_over_either_app : tnraenv_core_optim.
Hint Rewrite @tflatten_flatten_map_either_nil : tnraenv_core_optim.
Hint Rewrite @tcount_over_flat_map_either_nil_app_singleton : tnraenv_core_optim.