Module NRARewrite
Section ROptim.
Require Import List String.
Require Import Utils BasicRuntime.
Require Import NRA NRAEq.
Local Open Scope nra_scope.
Context {
fruntime:
foreign_runtime}.
Lemma and_comm (
p1 p2:
nra) :
p2 ∧
p1 ≡ₐ
p1 ∧
p2.
Proof.
unfold nra_eq;
intros;
simpl.
generalize (
h ⊢
p1 @ₐ
x ⊣
c);
generalize (
h ⊢
p2 @ₐ
x ⊣
c);
intros.
destruct o;
destruct o0;
try reflexivity.
unfold unbdbool.
destruct d;
destruct d0;
try reflexivity;
simpl.
rewrite Bool.andb_comm;
reflexivity.
Qed.
Lemma union_assoc (
p1 p2 p3:
nra):
(
p1 ⋃
p2) ⋃
p3 ≡ₐ
p1 ⋃ (
p2 ⋃
p3).
Proof.
unfold nra_eq;
intros;
simpl.
generalize (
h ⊢
p1 @ₐ
x ⊣
c)
as d1.
generalize (
h ⊢
p2 @ₐ
x ⊣
c)
as d2.
generalize (
h ⊢
p3 @ₐ
x ⊣
c)
as d3.
intros.
destruct d1;
destruct d2;
destruct d3;
try reflexivity.
destruct d;
destruct d0;
destruct d1;
try reflexivity.
simpl.
autorewrite with alg.
rewrite bunion_assoc.
reflexivity.
destruct (
rondcoll2 bunion d d0);
autorewrite with alg;
reflexivity.
Qed.
Lemma union_select_distr (
p p1 p2:
nra) :
σ⟨
p ⟩(
p1 ⋃
p2) ≡ₐ σ⟨
p ⟩(
p1) ⋃ σ⟨
p ⟩(
p2).
Proof.
unfold nra_eq;
intros.
simpl.
generalize (
h ⊢
p1 @ₐ
x ⊣
c)
as d1.
generalize (
h ⊢
p2 @ₐ
x ⊣
c)
as d2.
intros.
destruct d1;
destruct d2;
try (
autorewrite with alg;
reflexivity).
-
destruct d;
try reflexivity.
destruct d0;
simpl;
try (
destruct (
lift_filter
(
fun x' :
data =>
match h ⊢
p @ₐ
x' ⊣
c with
|
Some (
dbool b) =>
Some b
|
_ =>
None
end)
l);
reflexivity).
induction l;
simpl.
destruct (
lift_filter
(
fun x' :
data =>
match h ⊢
p @ₐ
x' ⊣
c with
|
Some (
dbool b) =>
Some b
|
_ =>
None
end)
l0);
reflexivity.
generalize(
h ⊢
p @ₐ
a ⊣
c);
intros.
unfold bunion.
rewrite lift_app_filter.
destruct o;
try reflexivity.
destruct d;
try reflexivity.
revert IHl.
generalize ((
lift_filter
(
fun x' :
data =>
match h ⊢
p @ₐ
x' ⊣
c with
|
Some (
dbool b0) =>
Some b0
|
_ =>
None
end)
l)).
generalize (
lift_filter
(
fun x' :
data =>
match h ⊢
p @ₐ
x' ⊣
c with
|
Some (
dbool b0) =>
Some b0
|
_ =>
None
end)
l0).
intros.
destruct o0;
try reflexivity.
simpl.
destruct o;
try reflexivity.
+
destruct b;
autorewrite with alg;
reflexivity.
+
autorewrite with alg.
reflexivity.
Qed.
Lemma map_singleton (
p1 p2:
nra) :
χ⟨
p1 ⟩( ‵{|
p2 |} ) ≡ₐ ‵{|
p1 ◯
p2 |}.
Proof.
unfold nra_eq;
intros;
simpl.
generalize (
h ⊢
p2 @ₐ
x ⊣
c);
intros.
destruct o;
try reflexivity;
simpl.
generalize (
h ⊢
p1 @ₐ
d ⊣
c);
intros;
simpl.
destruct o;
reflexivity.
Qed.
Lemma compose_rec_id s p:
‵[| (
s,
ID) |] ◯
p ≡ₐ ‵[| (
s,
p) |].
Proof.
unfold nra_eq;
intros;
simpl.
generalize (
h ⊢
p @ₐ
x ⊣
c);
intros.
destruct o;
reflexivity.
Qed.
Lemma flatten_map_coll p1 p2 :
♯
flatten(χ⟨ ‵{|
p1 |} ⟩(
p2 )) ≡ₐ χ⟨
p1 ⟩(
p2 ).
Proof.
unfold nra_eq;
intros h c _ x _;
simpl.
generalize (
h ⊢
p2 @ₐ
x ⊣
c);
clear x p2;
intros.
destruct o;
try reflexivity.
destruct d;
try reflexivity;
simpl.
induction l;
try reflexivity;
simpl.
generalize (
h ⊢
p1 @ₐ
a ⊣
c);
clear a;
intros;
simpl.
destruct o;
try reflexivity;
simpl.
unfold olift in *.
revert IHl.
generalize (
rmap
(
fun x :
data =>
match h ⊢
p1 @ₐ
x ⊣
c with
|
Some x' =>
Some (
dcoll (
x' ::
nil))
|
None =>
None
end)
l);
generalize (
rmap (
nra_eval h c p1)
l);
intros.
unfold lift in *;
simpl.
destruct o;
destruct o0;
simpl;
try reflexivity;
try congruence.
-
simpl in *.
unfold rflatten in *;
simpl in *.
revert IHl.
generalize ((
oflat_map
(
fun x :
data =>
match x with
|
dcoll y =>
Some y
|
_ =>
None
end)
l1));
intros;
simpl in *.
destruct o;
try congruence.
inversion IHl;
clear IHl H0;
reflexivity.
-
simpl in *.
unfold rflatten in *;
simpl.
revert IHl.
generalize ((
oflat_map
(
fun x :
data =>
match x with
|
dcoll y =>
Some y
|
_ =>
None
end)
l0));
intros;
simpl in *.
destruct o;
try congruence;
reflexivity.
Qed.
Lemma dot_from_duplicate_r s1 s2 p1 :
(‵[| (
s1,
p1) |] ⊕ ‵[| (
s2,
p1) |])·
s2 ≡ₐ
p1.
Proof.
Lemma dot_from_duplicate_l s1 s2 p1 :
(‵[| (
s1,
p1) |] ⊕ ‵[| (
s2,
p1) |])·
s1 ≡ₐ
p1.
Proof.
Lemma map_into_singleton p :
χ⟨ ‵{|
ID |} ⟩(‵{|
p |}) ≡ₐ ‵{|‵{|
p |}|}.
Proof.
unfold nra_eq;
intros ? ?
_ x _;
simpl.
generalize (
h ⊢
p @ₐ
x ⊣
c);
clear x p;
intros.
destruct o;
reflexivity.
Qed.
Lemma flatten_over_map_into_singleton p1 p2:
♯
flatten( χ⟨ ‵{|‵{|
p1 |}|} ⟩(
p2 ) ) ≡ₐ χ⟨ ‵{|
p1 |} ⟩(
p2 ).
Proof.
unfold nra_eq;
intros ? ?
_ ?
_;
simpl.
generalize (
h ⊢
p2 @ₐ
x ⊣
c);
clear p2 x;
intros.
destruct o;
try reflexivity;
simpl.
destruct d;
try reflexivity;
simpl.
induction l;
try reflexivity;
simpl.
unfold olift,
lift in *;
simpl.
generalize (
h ⊢
p1 @ₐ
a ⊣
c);
clear a;
intros;
simpl.
destruct o;
try reflexivity;
simpl.
revert IHl.
generalize (
rmap
(
fun x :
data =>
match
match h ⊢
p1 @ₐ
x ⊣
c with
|
Some x' =>
Some (
dcoll (
x'::
nil))
|
None =>
None
end
with
|
Some x' =>
Some (
dcoll (
x'::
nil))
|
None =>
None
end)
l);
generalize (
rmap
(
fun x :
data =>
match h ⊢
p1 @ₐ
x ⊣
c with
|
Some x' =>
Some (
dcoll (
x'::
nil))
|
None =>
None
end)
l);
intros.
destruct o;
destruct o0;
try reflexivity;
simpl;
unfold lift_oncoll in *;
simpl;
try congruence.
-
unfold rflatten in *;
simpl in *.
revert IHl;
generalize (
oflat_map
(
fun x :
data =>
match x with
|
dcoll y =>
Some y
|
_ =>
None
end)
l1);
intros.
destruct o;
try reflexivity;
simpl.
inversion IHl;
reflexivity.
congruence.
-
unfold rflatten in *;
simpl.
revert IHl;
generalize (
oflat_map
(
fun x :
data =>
match x with
|
dcoll y =>
Some y
|
_ =>
None
end)
l0);
intros.
destruct o;
try reflexivity;
simpl.
congruence.
Qed.
Lemma map_singleton_rec s1 s2 :
χ⟨‵[| (
s1,
ID) |] ⟩( ‵{|(
ID) ·
s2 |}) ≡ₐ ‵{|‵[| (
s1, (
ID) ·
s2) |] |}.
Proof.
Lemma map_dot_singleton s p :
χ⟨ (
ID)·
s ⟩( ‵{|
p |} ) ≡ₐ ‵{|
p·
s |}.
Proof.
Lemma unnest_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) |]|}.
Proof.
Lemma substitute_in_bindings (
p:
nra) :
χ⟨ (‵[| ("
PBIND",
ID·"
PBIND") |] ⊕ ‵[| ("
PDATA",
ID·"
PDATA"·"
WORLD") |])·"
PDATA" ⟩( ‵{|
p |} )
≡ₐ ‵{|(‵[| ("
PBIND",
p·"
PBIND") |] ⊕ ‵[| ("
PDATA",
p·"
PDATA"·"
WORLD") |])·"
PDATA" |}.
Proof.
unfold nra_eq,
olift;
intros ? ?
_ ?
_;
simpl.
generalize (
h ⊢
p @ₐ
x ⊣
c);
simpl;
intros;
clear p x.
destruct o;
try reflexivity.
destruct d;
try reflexivity.
unfold olift,
lift;
simpl.
generalize (
edot l "
PBIND");
generalize (
edot l "
PDATA");
intros;
clear l;
simpl.
destruct o;
destruct o0;
try reflexivity;
simpl.
generalize (
match
match d with
|
drec r =>
edot r "
WORLD"
|
_ =>
None
end
with
|
Some x' =>
Some (
drec (("
PDATA"%
string,
x') ::
nil))
|
None =>
None
end
);
intros;
simpl.
destruct (
match o with
|
Some (
drec r2) =>
Some
(
drec
(
RSort.insertion_sort_insert rec_field_lt_dec
("
PBIND"%
string,
d0) (
rec_sort r2)))
|
_ =>
None
end
);
intros;
simpl.
destruct d1;
try reflexivity.
generalize (
edot l "
PDATA");
clear l;
intros.
destruct o0;
try reflexivity;
simpl.
reflexivity.
Qed.
Lemma dot_from_duplicate_bind_r :
(‵[| ("
PBIND", (
AUnop (
ADot "
PBIND")
AID)) |] ⊕ ‵[| ("
PDATA", (
AUnop (
ADot "
PBIND")
AID)) |])·"
PDATA" ≡ₐ (
AUnop (
ADot "
PBIND")
AID).
Proof.
Lemma dot_from_duplicate_bind_l :
(‵[| ("
PBIND", (
AUnop (
ADot "
PBIND")
AID)) |] ⊕ ‵[| ("
PDATA", (
AUnop (
ADot "
PBIND")
AID)) |])·"
PBIND" ≡ₐ (
AUnop (
ADot "
PBIND")
AID).
Proof.
Lemma dot_dot_from_duplicate_bind :
(‵[| ("
PBIND",
ID·"
PBIND") |] ⊕ ‵[| ("
PDATA",
ID·"
PBIND"·"
WORLD") |])·"
PDATA"
≡ₐ
ID·"
PBIND"·"
WORLD".
Proof.
unfold nra_eq;
intros ? ?
_ ?
_;
simpl.
destruct x;
try reflexivity;
simpl.
generalize (
edot l "
PBIND");
clear l;
intros.
destruct o;
try reflexivity;
simpl.
destruct d;
try reflexivity;
simpl.
generalize (
edot l "
WORLD");
intros;
simpl.
destruct o;
reflexivity.
Qed.
Lemma big_nested_bind_simplify_one :
‵[| ("
PBIND",
ID·"
PBIND") |]
⊕ ‵[| ("
a1",
χ⟨(‵[| ("
PBIND",
ID·"
PBIND") |] ⊕ ‵[| ("
PDATA",
ID·"
PDATA"·"
e") |])·"
PDATA"
⟩( ‵{|‵[| ("
PBIND",
ID·"
PBIND") |] ⊕ ‵[| ("
PDATA",
ID· "
PBIND") |] |}))|]
≡ₐ ‵[| ("
PBIND",
ID·"
PBIND") |] ⊕ ‵[| ("
a1", ‵{|
ID·"
PBIND"·"
e" |}) |].
Proof.
unfold nra_eq;
intros ? ?
_;
simpl.
destruct x;
try reflexivity;
simpl.
generalize (
edot l "
PBIND");
intros.
destruct o;
try reflexivity;
simpl.
unfold olift2,
olift;
simpl.
destruct d;
try reflexivity;
simpl.
generalize (
edot l0 "
e");
intros.
destruct o;
try reflexivity;
simpl.
Qed.
End ROptim.