Module Qcert.NRA.Optim.NRAExtRewrite
Require Import List.
Require Import DataRuntime.
Require Import NRA.
Require Import NRAEq.
Require Import NRAExt.
Require Import NRAExtEq.
Require Import NRARewrite.
Require Import String.
Section NRAExtRewrite.
Local Open Scope nra_scope.
Local Open Scope nraext_scope.
Local Open Scope string.
Context {
fruntime:
foreign_runtime}.
Lemma pull_nra_opt (
p1 p2:
nraext) :
(
nra_of_nraext p1) ≡ₐ (
nra_of_nraext p2) ->
p1 ≡ₓ
p2.
Proof.
Lemma eand_comm (
p1 p2:
nraext) :
p2 ∧
p1 ≡ₓ
p1 ∧
p2.
Proof.
Lemma eunion_assoc (
p1 p2 p3:
nraext):
(
p1 ⋃
p2) ⋃
p3 ≡ₓ
p1 ⋃ (
p2 ⋃
p3).
Proof.
Lemma eunion_select_distr (
p p1 p2:
nraext) :
σ⟨
p ⟩(
p1 ⋃
p2) ≡ₓ σ⟨
p ⟩(
p1) ⋃ σ⟨
p ⟩(
p2).
Proof.
Lemma emap_singleton (
p1 p2:
nraext) :
χ⟨
p1 ⟩( ‵{|
p2 |} ) ≡ₓ ‵{|
p1 ◯
p2 |}.
Proof.
Lemma ecompose_rec_id s p:
‵[| (
s,
ID) |] ◯
p ≡ₓ ‵[| (
s,
p) |].
Proof.
Lemma eflatten_map_coll p1 p2 :
♯
flatten(χ⟨ ‵{|
p1 |} ⟩(
p2 )) ≡ₓ χ⟨
p1 ⟩(
p2 ).
Proof.
Lemma eunnest_singleton s1 s2 s3 p1 p2 :
s1 <>
s2 /\
s2 <>
s3 /\
s3 <>
s1 ->
μ[
s1 ][
s2 ]( ‵{|‵[| (
s3,
p1)|] ⊕ ‵[| (
s1, ‵{|
p2|})|]|})
≡ₓ ‵{|‵[| (
s3,
p1)|] ⊕ ‵[| (
s2,
p2)|]|}.
Proof.
Lemma emap_into_singleton p :
χ⟨ ‵{|
ID |} ⟩(‵{|
p |}) ≡ₓ ‵{|‵{|
p |}|}.
Proof.
Lemma eflatten_over_map_into_singleton p1 p2 :
♯
flatten( χ⟨ ‵{|‵{|
p1 |}|} ⟩(
p2 ) ) ≡ₓ χ⟨ ‵{|
p1 |} ⟩(
p2 ).
Proof.
Lemma join_intro p1 p2 p3 :
σ⟨
p1 ⟩(
p2 ×
p3 ) ≡ₓ ⋈⟨
p1 ⟩(
p2,
p3).
Proof.
Lemma emap_singleton_rec s1 s2 :
χ⟨‵[| (
s1,
ID) |] ⟩( ‵{|(
ID) ·
s2 |}) ≡ₓ ‵{|‵[| (
s1, (
ID) ·
s2) |] |}.
Proof.
Lemma emap_dot_singleton s p :
χ⟨ (
ID)·
s ⟩( ‵{|
p |} ) ≡ₓ ‵{|
p·
s |}.
Proof.
Lemma eunnest_singleton_context p1 p2 :
μ["
a1"]["
PDATA"]( ‵{|‵[| ("
PBIND",
p1)|] ⊕ ‵[| ("
a1", ‵{|
p2|})|]|})
≡ₓ ‵{|‵[| ("
PBIND",
p1)|] ⊕ ‵[| ("
PDATA",
p2)|]|}.
Proof.
Lemma esubstitute_in_bindings (
p:
nraext) :
χ⟨ (‵[| ("
PBIND",
ID·"
PBIND") |] ⊕ ‵[| ("
PDATA",
ID·"
PDATA"·"
WORLD") |])·"
PDATA" ⟩( ‵{|
p |} )
≡ₓ ‵{|(‵[| ("
PBIND",
p·"
PBIND") |] ⊕ ‵[| ("
PDATA",
p·"
PDATA"·"
WORLD") |])·"
PDATA" |}.
Proof.
Lemma edot_from_duplicate_bind_r :
(‵[| ("
PBIND",
ID·"
PBIND") |] ⊕ ‵[| ("
PDATA",
ID·"
PBIND") |])·"
PDATA" ≡ₓ
ID·"
PBIND".
Proof.
Lemma edot_from_duplicate_bind_l :
(‵[| ("
PBIND",
ID·"
PBIND") |] ⊕ ‵[| ("
PDATA",
ID·"
PBIND") |])·"
PBIND" ≡ₓ
ID·"
PBIND".
Proof.
Lemma edot_dot_from_duplicate_bind :
(‵[| ("
PBIND",
ID·"
PBIND") |] ⊕ ‵[| ("
PDATA",
ID·"
PBIND"·"
WORLD") |])·"
PDATA"
≡ₓ
ID·"
PBIND"·"
WORLD".
Proof.
Lemma ebig_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.
End NRAExtRewrite.