Library zoo.iris.algebra.lib.twins

Require Import iris.algebra.excl.
Require Import iris.algebra.proofmode_classes.

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

Definition twins {SI : sidx} A :=
  auth_option (exclR A).
Definition twins۰R {SI : sidx} A :=
  auth_option۰R (exclR A).
Definition twins۰UR {SI : sidx} A :=
  auth_option۰UR (exclR A).

Section ofe.
  Context {SI : sidx}.
  Context {A : ofe}.

  Implicit Type a b : A.

  Definition twins۰twin₁ dq a : twins۰UR A :=
    ●O{dq} (Excl a).
  Definition twins۰twin₂ a : twins۰UR A :=
    ◯O (Excl a).

  #[global] Instance twins۰twin₁ｰne dq :
    NonExpansive (twins۰twin₁ dq).
  #[global] Instance twins۰twin₁ｰproper dq :
    Proper ((≡) ==> (≡)) (twins۰twin₁ dq).
  #[global] Instance twins۰twin₂ｰne :
    NonExpansive twins۰twin₂.
  #[global] Instance twins۰twin₂ｰproper :
    Proper ((≡) ==> (≡)) twins۰twin₂.

  #[global] Instance twins۰twin₁ｰdistｰinj n :
    Inj2 (=) (≡{n}≡) (≡{n}≡) twins۰twin₁.
  #[global] Instance twins۰twin₁ｰinj :
    Inj2 (=) (≡) (≡) twins۰twin₁.
  #[global] Instance twins۰twin₂ｰdistｰinj n :
    Inj (≡{n}≡) (≡{n}≡) twins۰twin₂.
  #[global] Instance twins۰twin₂ｰinj :
    Inj (≡) (≡) twins۰twin₂.

  #[global] Instance twins۰twin₁ｰdiscrete dq a :
    Discrete a →
    Discrete (twins۰twin₁ dq a).
  #[global] Instance twins۰twin₂ｰdiscrete a :
    Discrete a →
    Discrete (twins۰twin₂ a).
  #[global] Instance twins۰cmra_discrete :
    OfeDiscrete A →
    CmraDiscrete (twins۰R A).

  Lemma twins۰twin₁ｰdfracｰop dq1 dq2 a :
    twins۰twin₁ (dq1 ⋅ dq2) a ≡ twins۰twin₁ dq1 a ⋅ twins۰twin₁ dq2 a.
  #[global] Instance twins۰twin₁ｰdfracｰis_op dq dq1 dq2 a :
    IsOp dq dq1 dq2 →
    IsOp' (twins۰twin₁ dq a) (twins۰twin₁ dq1 a) (twins۰twin₁ dq2 a).

  #[global] Instance twins۰twin₁ｰcore_id a :
    CoreId (twins۰twin₁ DfracDiscarded a).

  Lemma twins۰twin₁ｰdfracｰvalidN n dq a :
    ✓{n} (twins۰twin₁ dq a) ↔
    ✓ dq.
  Lemma twins۰twin₁ｰdfracｰvalid dq a :
    ✓ (twins۰twin₁ dq a) ↔
    ✓ dq.
  Lemma twins۰twin₁ｰvalidN n a :
    ✓{n} (twins۰twin₁ (DfracOwn 1) a).
  Lemma twins۰twin₁ｰvalid a :
    ✓ (twins۰twin₁ (DfracOwn 1) a).

  Lemma twins۰twin₁ｰdfracｰopｰvalidN n dq1 a1 dq2 a2 :
    ✓{n} (twins۰twin₁ dq1 a1 ⋅ twins۰twin₁ dq2 a2) ↔
    ✓ (dq1 ⋅ dq2) ∧ a1 ≡{n}≡ a2.
  Lemma twins۰twin₁ｰdfracｰopｰvalid dq1 a1 dq2 a2 :
    ✓ (twins۰twin₁ dq1 a1 ⋅ twins۰twin₁ dq2 a2) ↔
    ✓ (dq1 ⋅ dq2) ∧ a1 ≡ a2.
  Lemma twins۰twin₁ｰopｰvalidN n a1 a2 :
    ✓{n} (twins۰twin₁ (DfracOwn 1) a1 ⋅ twins۰twin₁ (DfracOwn 1) a2) ↔
    False.
  Lemma twins۰twin₁ｰopｰvalid a b :
    ✓ (twins۰twin₁ (DfracOwn 1) a ⋅ twins۰twin₁ (DfracOwn 1) b) ↔
    False.

  Lemma twins۰twin₂ｰvalidN n a :
    ✓{n} (twins۰twin₂ a).
  Lemma twins۰twin₂ｰvalid a :
    ✓ (twins۰twin₂ a).

  Lemma twins۰twin₂ｰopｰvalidN n a b :
    ✓{n} (twins۰twin₂ a ⋅ twins۰twin₂ b) ↔
    False.
  Lemma twins۰twin₂ｰopｰvalid a b :
    ✓ (twins۰twin₂ a ⋅ twins۰twin₂ b) ↔
    False.

  Lemma twinsｰbothｰdfracｰvalidN n dq a b :
    ✓{n} (twins۰twin₁ dq a ⋅ twins۰twin₂ b) ↔
    ✓ dq ∧ a ≡{n}≡ b.
  Lemma twinsｰbothｰdfracｰvalid dq a b :
    ✓ (twins۰twin₁ dq a ⋅ twins۰twin₂ b) ↔
    ✓ dq ∧ a ≡ b.
  Lemma twinsｰbothｰvalidN n a b :
    ✓{n} (twins۰twin₁ (DfracOwn 1) a ⋅ twins۰twin₂ b) ↔
    a ≡{n}≡ b.
  Lemma twinsｰbothｰvalid a b :
    ✓ (twins۰twin₁ (DfracOwn 1) a ⋅ twins۰twin₂ b) ↔
    a ≡ b.

  Lemma twins۰twin₁ｰpersist dq a :
    twins۰twin₁ dq a ~~> twins۰twin₁ DfracDiscarded a.
  Lemma twinsｰbothｰupdate a1 b1 a2 b2 :
    a2 ≡ b2 →
    twins۰twin₁ (DfracOwn 1) a1 ⋅ twins۰twin₂ b1 ~~> twins۰twin₁ (DfracOwn 1) a2 ⋅ twins۰twin₂ b2.
End ofe.

#[global] Opaque twins۰twin₁.
#[global] Opaque twins۰twin₂.

Definition twins۰URF {SI : sidx} F :=
  auth_option۰URF $ exclRF F.
#[global] Instance twins۰URFｰcontractive {SI : sidx} F :
  oFunctorContractive F →
  urFunctorContractive (twins۰URF F).

Definition twins۰RF {SI : sidx} F :=
  auth_option۰RF $ exclRF F.
#[global] Instance twins۰RFｰcontractive {SI : sidx} F :
  oFunctorContractive F →
  rFunctorContractive (twins۰RF F).