Library zoo.iris.algebra.view

Require Export iris.algebra.view.

Require Import zoo.prelude.
Require Export zoo.iris.algebra.base.
Require Import zoo.options.

Section cmra.
  Context {SI : sidx}.
  Context `(rel : view_rel A B).

  Implicit Type a : A.
  Implicit Type b : B.

  Lemma viewｰauthｰfragｰdfracｰop dq1 a1 b1 dq2 a2 b2 :
    ●V{dq1} a1 ⋅ ◯V b1 ≡@{view rel} ●V{dq2} a2 ⋅ ◯V b2 ↔
    dq1 = dq2 ∧ a1 ≡ a2 ∧ b1 ≡ b2.
  Lemma viewｰauthｰfragｰop a1 b1 a2 b2 :
    ●V a1 ⋅ ◯V b1 ≡@{view rel} ●V a2 ⋅ ◯V b2 ↔
    a1 ≡ a2 ∧ b1 ≡ b2.
End cmra.