Qcert.NRA.Optim.NRARewrite

Section ROptim.




  Context {fruntime:foreign_runtime}.



  Lemma and_comm (p1 p2: nra) :
    p2 ∧ p1 ≡ₐ p1 ∧ p2.


  Lemma union_assoc (p1 p2 p3: nra):
    (p1 ⋃ p2) ⋃ p3 ≡ₐ p1 ⋃ (p2 ⋃ p3).


  Lemma union_select_distr (p p1 p2: nra) :
    σ⟨ p ⟩(p1 ⋃ p2) ≡ₐ σ⟨ p ⟩(p1) ⋃ σ⟨ p ⟩(p2).


  Lemma map_singleton (p1 p2:nra) :
    χ⟨ p1 ⟩( ‵{| p2 |} ) ≡ₐ ‵{| p1 ◯ p2 |}.


  Lemma compose_rec_id s p:
    ‵[| (s, ID) |] ◯ p ≡ₐ ‵[| (s, p) |].

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


  Lemma dot_from_duplicate_r s1 s2 p1 :
    (‵[| (s1, p1) |] ⊕ ‵[| (s2, p1) |])·s2 ≡ₐ p1.


  Lemma dot_from_duplicate_l s1 s2 p1 :
    (‵[| (s1, p1) |] ⊕ ‵[| (s2, p1) |])·s1 ≡ₐ p1.


  Lemma map_into_singleton p :
    χ⟨ ‵{| ID |} ⟩(‵{| p |}) ≡ₐ ‵{|‵{| p |}|}.


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



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


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


  Lemma unnest_singleton s1 s2 s3 p1 p2 :
    s1 ≠ s2 ∧ s2 ≠ s3 ∧ s3 ≠ s1 →
    χ⟨ ¬π[s1](ID) ⟩(
       ⋈ᵈ⟨ χ⟨ ‵[| (s2,ID) |] ⟩((ID)·s1) ⟩( ‵{|‵[| (s3,p1) |] ⊕ ‵[| (s1,‵{| p2 |}) |]|} )
     )
     ≡ₐ ‵{|‵[| (s3, p1) |] ⊕ ‵[| (s2, p2) |]|}.


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


  Lemma dot_from_duplicate_bind_r :
    (‵[| ("PBIND", (AUnop (ADot "PBIND") AID)) |] ⊕ ‵[| ("PDATA", (AUnop (ADot "PBIND") AID)) |])·"PDATA" ≡ₐ (AUnop (ADot "PBIND") AID).


  Lemma dot_from_duplicate_bind_l :
    (‵[| ("PBIND", (AUnop (ADot "PBIND") AID)) |] ⊕ ‵[| ("PDATA", (AUnop (ADot "PBIND") AID)) |])·"PBIND" ≡ₐ (AUnop (ADot "PBIND") AID).


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


  Lemma big_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 ROptim.