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.
    unfold nra_eq, nraext_eq; intros.
    unfold nraext_eval.
    rewrite H; trivial.
  Qed.


  Lemma eand_comm (p1 p2: nraext) :
    p2p1 ≡ₓ p1p2.
Proof.
    apply pull_nra_opt.
    apply and_comm.
  Qed.


  Lemma eunion_assoc (p1 p2 p3: nraext):
    (p1p2) ⋃ p3 ≡ₓ p1 ⋃ (p2p3).
Proof.
    apply pull_nra_opt.
    apply union_assoc.
  Qed.
  

  Lemma eunion_select_distr (p p1 p2: nraext) :
    σ⟨ p ⟩(p1p2) ≡ₓ σ⟨ p ⟩(p1) ⋃ σ⟨ p ⟩(p2).
Proof.
    apply pull_nra_opt.
    apply union_select_distr.
  Qed.


  Lemma emap_singleton (p1 p2:nraext) :
    χ⟨ p1 ⟩( ‵{| p2 |} ) ≡ₓ ‵{| p1p2 |}.
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 :
    χ⟨ (IDs ⟩( ‵{| 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 NRAExtRewrite.