Module Qcert.NRA.Optim.NRAExtRewrite


Section NRAExtRewrite.
  Require Import List.
  Require Import CommonRuntime.
  Require Import NRA.
  Require Import NRAEq.
  Require Import NRAExt.
  Require Import 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) :
    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.