Qcert.NRA.Optim.NRAExtRewrite

Section ROptimExt.




  Context {fruntime:foreign_runtime}.




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


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


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


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


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


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

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



  Lemma eunnest_singleton s1 s2 s3 p1 p2 :
    s1 ≠ s2 ∧ s2 ≠ s3 ∧ s3 ≠ s1 →
    μ[s1 ][ s2 ]( ‵{|‵[| (s3, p1)|] ⊕ ‵[| (s1, ‵{|p2|})|]|})
     ≡ₓ ‵{|‵[| (s3, p1)|] ⊕ ‵[| (s2, p2)|]|}.


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


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


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



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


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


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


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


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


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


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


  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" |}) |].

End ROptimExt.