Module NRAExtRewrite

Section ROptimExt.

  Require Import List.

  Require Import Utils BasicRuntime.
  Require Import NRA NRAEq NRAExt NRAExtEq.
  Require Import NRARewrite.

  Local Open Scope nra_scope.
  Local Open Scope nraext_scope.

  Context {fruntime:foreign_runtime}.

  Lemma pull_nra_opt (p1 p2:nraext) :
    (nra_of_nraext p1) ≡ₐ (nra_of_nraext p2) ->
    p1 ≡ₓ p2.

Proof.

    unfold nra_eq, nraext_eq; intros.
    unfold nraext_eval.
    rewrite H; trivial.
  Qed.

Lemma eand_comm (p1 p2: nraext) :
p2 ∧ p1 ≡ₓ p1 ∧ p2.

Proof.

    apply pull_nra_opt.
    apply and_comm.
  Qed.

Lemma eunion_assoc (p1 p2 p3: nraext):
(p1 ⋃ p2) ⋃ p3 ≡ₓ p1 ⋃ (p2 ⋃ p3).

Proof.

    apply pull_nra_opt.
    apply union_assoc.
  Qed.

  Lemma eunion_select_distr (p p1 p2: nraext) :
    σ⟨ p ⟩(p1 ⋃ p2) ≡ₓ σ⟨ p ⟩(p1) ⋃ σ⟨ p ⟩(p2).

Proof.

    apply pull_nra_opt.
    apply union_select_distr.
  Qed.

Lemma emap_singleton (p1 p2:nraext) :
χ⟨ p1 ⟩( ‵{| p2 |} ) ≡ₓ ‵{| p1 ◯ p2 |}.

Proof.

    apply pull_nra_opt.
    apply map_singleton.
  Qed.

Lemma ecompose_rec_id s p:
‵[| (s, ID) |] ◯ p ≡ₓ ‵[| (s, p) |].

Proof.

    apply pull_nra_opt.
    apply compose_rec_id.
  Qed.

Lemma eflatten_map_coll p1 p2 :
♯flatten(χ⟨ ‵{| p1 |} ⟩( p2 )) ≡ₓ χ⟨ p1 ⟩( p2 ).

Proof.

    apply pull_nra_opt.
    apply flatten_map_coll.
  Qed.

  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.

    intros.
    apply pull_nra_opt.
    apply unnest_singleton; assumption.
  Qed.

  Lemma emap_into_singleton p :
    χ⟨ ‵{| ID |} ⟩(‵{| p |}) ≡ₓ ‵{|‵{| p |}|}.

Proof.

    apply pull_nra_opt.
    apply map_into_singleton.
  Qed.

  Lemma eflatten_over_map_into_singleton p1 p2 :
    ♯flatten( χ⟨ ‵{|‵{| p1 |}|} ⟩( p2 ) ) ≡ₓ χ⟨ ‵{| p1 |} ⟩( p2 ).

Proof.

    apply pull_nra_opt.
    apply flatten_over_map_into_singleton.
  Qed.

Lemma join_intro p1 p2 p3 :
σ⟨ p1 ⟩( p2 × p3 ) ≡ₓ ⋈⟨ p1 ⟩(p2, p3).

Proof.

    apply pull_nra_opt.
    simpl; unfold join.
    unfold nra_eq; intros ? ? _.
    reflexivity.
  Qed.

  Lemma emap_singleton_rec s1 s2 :
    χ⟨‵[| (s1, ID) |] ⟩( ‵{|(ID) · s2 |}) ≡ₓ ‵{|‵[| (s1, (ID) · s2) |] |}.

Proof.

    apply pull_nra_opt.
    apply map_singleton_rec.
  Qed.

  Lemma emap_dot_singleton s p :
    χ⟨ (ID)·s ⟩( ‵{| p |} ) ≡ₓ ‵{| p·s |}.

Proof.

    apply pull_nra_opt.
    apply map_dot_singleton.
  Qed.

  Lemma eunnest_singleton_context p1 p2 :
    μ["a1"]["PDATA"]( ‵{|‵[| ("PBIND", p1)|] ⊕ ‵[| ("a1", ‵{|p2|})|]|})
     ≡ₓ ‵{|‵[| ("PBIND", p1)|] ⊕ ‵[| ("PDATA", p2)|]|}.

Proof.

    apply eunnest_singleton.
    split; try congruence.
    split; try congruence.
  Qed.

  Lemma esubstitute_in_bindings (p:nraext) :
    χ⟨ (‵[| ("PBIND", ID·"PBIND") |] ⊕ ‵[| ("PDATA", ID·"PDATA"·"WORLD") |])·"PDATA" ⟩( ‵{| p |} )
     ≡ₓ ‵{|(‵[| ("PBIND", p·"PBIND") |] ⊕ ‵[| ("PDATA", p·"PDATA"·"WORLD") |])·"PDATA" |}.

Proof.

    apply pull_nra_opt.
    apply substitute_in_bindings.
  Qed.

Lemma edot_from_duplicate_bind_r :
(‵[| ("PBIND", ID·"PBIND") |] ⊕ ‵[| ("PDATA", ID·"PBIND") |])·"PDATA" ≡ₓ ID·"PBIND".

Proof.

    apply pull_nra_opt.
    apply dot_from_duplicate_bind_r.
  Qed.

  Lemma edot_from_duplicate_bind_l :
    (‵[| ("PBIND", ID·"PBIND") |] ⊕ ‵[| ("PDATA", ID·"PBIND") |])·"PBIND" ≡ₓ ID·"PBIND".

Proof.

    apply pull_nra_opt.
    apply dot_from_duplicate_bind_l.
  Qed.

  Lemma edot_dot_from_duplicate_bind :
    (‵[| ("PBIND", ID·"PBIND") |] ⊕ ‵[| ("PDATA", ID·"PBIND"·"WORLD") |])·"PDATA"
     ≡ₓ ID·"PBIND"·"WORLD".

Proof.

    apply pull_nra_opt.
    apply dot_dot_from_duplicate_bind.
  Qed.

  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.

    apply pull_nra_opt.
    apply big_nested_bind_simplify_one.
  Qed.

End ROptimExt.