Library zoo.iris.algebra.lib.twins

From iris.algebra Require Import
  excl
  proofmode_classes.

From zoo Require Import
  prelude.
From zoo.iris.algebra Require Export
  base.
From zoo.iris.algebra Require Import
  lib.auth_option.
From zoo Require Import
  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 Types a b : A.

  Definition twins_twin1 dq a : twins_UR A :=
    ●O{dq} (Excl a).
  Definition twins_twin2 a : twins_UR A :=
    ◯O (Excl a).

  #[global] Instance twins_twin1_ne dq :
    NonExpansive (twins_twin1 dq).
  #[global] Instance twins_twin1_proper dq :
    Proper ((≡) ==> (≡)) (twins_twin1 dq).
  #[global] Instance twins_twin2_ne :
    NonExpansive twins_twin2.
  #[global] Instance twins_twin2_proper :
    Proper ((≡) ==> (≡)) twins_twin2.

  #[global] Instance twins_twin1_dist_inj n :
    Inj2 (=) (≡{n}≡) (≡{n}≡) twins_twin1.
  #[global] Instance twins_twin1_inj :
    Inj2 (=) (≡) (≡) twins_twin1.
  #[global] Instance twins_twin2_dist_inj n :
    Inj (≡{n}≡) (≡{n}≡) twins_twin2.
  #[global] Instance twins_twin2_inj :
    Inj (≡) (≡) twins_twin2.

  #[global] Instance twins_twin1_discrete dq a :
    Discrete a →
    Discrete (twins_twin1 dq a).
  #[global] Instance twins_twin2_discrete a :
    Discrete a →
    Discrete (twins_twin2 a).
  #[global] Instance twins_cmra_discrete :
    OfeDiscrete A →
    CmraDiscrete (twins_R A).

  Lemma twins_twin1_dfrac_op dq1 dq2 a :
    twins_twin1 (dq1 ⋅ dq2) a ≡ twins_twin1 dq1 a ⋅ twins_twin1 dq2 a.
  #[global] Instance twins_twin1_dfrac_is_op dq dq1 dq2 a :
    IsOp dq dq1 dq2 →
    IsOp' (twins_twin1 dq a) (twins_twin1 dq1 a) (twins_twin1 dq2 a).

  #[global] Instance twins_twin1_core_id a :
    CoreId (twins_twin1 DfracDiscarded a).

  Lemma twins_twin1_dfrac_validN n dq a :
    ✓{n} (twins_twin1 dq a) ↔
    ✓ dq.
  Lemma twins_twin1_dfrac_valid dq a :
    ✓ (twins_twin1 dq a) ↔
    ✓ dq.
  Lemma twins_twin1_validN n a :
    ✓{n} (twins_twin1 (DfracOwn 1) a).
  Lemma twins_twin1_valid a :
    ✓ (twins_twin1 (DfracOwn 1) a).

  Lemma twins_twin1_dfrac_op_validN n dq1 a1 dq2 a2 :
    ✓{n} (twins_twin1 dq1 a1 ⋅ twins_twin1 dq2 a2) ↔
    ✓ (dq1 ⋅ dq2) ∧ a1 ≡{n}≡ a2.
  Lemma twins_twin1_dfrac_op_valid dq1 a1 dq2 a2 :
    ✓ (twins_twin1 dq1 a1 ⋅ twins_twin1 dq2 a2) ↔
    ✓ (dq1 ⋅ dq2) ∧ a1 ≡ a2.
  Lemma twins_twin1_op_validN n a1 a2 :
    ✓{n} (twins_twin1 (DfracOwn 1) a1 ⋅ twins_twin1 (DfracOwn 1) a2) ↔
    False.
  Lemma twins_twin1_op_valid a b :
    ✓ (twins_twin1 (DfracOwn 1) a ⋅ twins_twin1 (DfracOwn 1) b) ↔
    False.

  Lemma twins_twin2_validN n a :
    ✓{n} (twins_twin2 a).
  Lemma twins_twin2_valid a :
    ✓ (twins_twin2 a).

  Lemma twins_twin2_op_validN n a b :
    ✓{n} (twins_twin2 a ⋅ twins_twin2 b) ↔
    False.
  Lemma twins_twin2_op_valid a b :
    ✓ (twins_twin2 a ⋅ twins_twin2 b) ↔
    False.

  Lemma twins_both_dfrac_validN n dq a b :
    ✓{n} (twins_twin1 dq a ⋅ twins_twin2 b) ↔
    ✓ dq ∧ a ≡{n}≡ b.
  Lemma twins_both_dfrac_valid dq a b :
    ✓ (twins_twin1 dq a ⋅ twins_twin2 b) ↔
    ✓ dq ∧ a ≡ b.
  Lemma twins_both_validN n a b :
    ✓{n} (twins_twin1 (DfracOwn 1) a ⋅ twins_twin2 b) ↔
    a ≡{n}≡ b.
  Lemma twins_both_valid a b :
    ✓ (twins_twin1 (DfracOwn 1) a ⋅ twins_twin2 b) ↔
    a ≡ b.

  Lemma twins_twin1_persist dq a :
    twins_twin1 dq a ~~> twins_twin1 DfracDiscarded a.
  Lemma twins_both_update a1 b1 a2 b2 :
    a2 ≡ b2 →
    twins_twin1 (DfracOwn 1) a1 ⋅ twins_twin2 b1 ~~> twins_twin1 (DfracOwn 1) a2 ⋅ twins_twin2 b2.
End ofe.

#[global] Opaque twins_twin1.
#[global] Opaque twins_twin2.

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).