Library zoo.iris.base_logic.algebra.twins

Require Import iris.bi.bi.
Require Import iris.base_logic.bi.

Require Import zoo.prelude.
Require Import zoo.iris.algebra.lib.twins.
Require Import zoo.options.

Section upred.
  Context {M : ucmra}.

  Notation "P ⊢ Q" := (
    bi_entails (PROP := uPredI M) P Q
  ).
  Notation "P ⊣⊢ Q" := (
    equiv (A := uPredI M) P%I Q%I
  ).
  Notation "⊢ Q" := (
    bi_entails (PROP := uPredI M) True Q
  ).

  Section ofe.
    Context {A : ofe}.

    Implicit Type a b : A.

    Lemma twins۰twin₁ｰdfracｰvalidI dq a :
      ✓ (twins۰twin₁ dq a) ⊣⊢
      ⌜✓ dq⌝.
    Lemma twins۰twin₁ｰvalidI a :
      ⊢ ✓ (twins۰twin₁ (DfracOwn 1) a).

    Lemma twins۰twin₁ｰdfracｰopｰvalidI dq1 a1 dq2 a2 :
      ✓ (twins۰twin₁ dq1 a1 ⋅ twins۰twin₁ dq2 a2) ⊣⊢
        ⌜✓ (dq1 ⋅ dq2)⌝ ∧
        a1 ≡ a2.
    Lemma twins۰twin₁ｰopｰvalidI a b :
      ✓ (twins۰twin₁ (DfracOwn 1) a ⋅ twins۰twin₁ (DfracOwn 1) b) ⊣⊢
      False.

    Lemma twins۰twin₂ｰvalidI a :
      ⊢ ✓ (twins۰twin₂ a).

    Lemma twins۰twin₂ｰopｰvalidI a b :
      ✓ (twins۰twin₂ a ⋅ twins۰twin₂ b) ⊣⊢
      False.

    Lemma twinsｰbothｰdfracｰvalidI dq a b :
      ✓ (twins۰twin₁ dq a ⋅ twins۰twin₂ b) ⊣⊢
        ⌜✓ dq⌝ ∧
        a ≡ b.
    Lemma twinsｰbothｰvalidI a b :
      ✓ (twins۰twin₁ (DfracOwn 1) a ⋅ twins۰twin₂ b) ⊣⊢
      a ≡ b.
  End ofe.
End upred.