Library zoo.iris.base_logic.lib.twins

From zoo Require Import
  prelude.
From zoo.iris.algebra Require Import
  lib.twins.
From zoo.iris.base_logic Require Export
  lib.base.
From zoo.iris.base_logic Require Import
  algebra.twins.
From zoo.iris Require Import
  diaframe.
From zoo Require Import
  options.

Class TwinsG Σ F :=
  { #[local] twins_G_inG :: inG Σ (twins_R $ oFunctor_apply F $ iPropO Σ)
  }.

Definition twins_Σ F `{!oFunctorContractive F} :=
  #[GFunctor (twins_RF F)
  ].
#[global] Instance subG_twins_Σ Σ F `{!oFunctorContractive F} :
  subG (twins_Σ F) Σ →
  TwinsG Σ F.

Section twins_G.
  Context `{twins_G : !TwinsG Σ F}.

  Definition twins_twin1 γ dq a :=
    own γ (twins_twin1 dq a).
  Definition twins_twin2 γ a :=
    own γ (twins_twin2 a).

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

  #[global] Instance twins_twin1_timeless γ dq a :
    Discrete a →
    Timeless (twins_twin1 γ dq a).
  #[global] Instance twins_twin2_timeless γ a :
    Discrete a →
    Timeless (twins_twin2 γ a).

  #[global] Instance twins_twin1_persistent γ a :
    Persistent (twins_twin1 γ DfracDiscarded a).

  #[global] Instance twins_twin1_fractional γ a :
    Fractional (λ q, twins_twin1 γ (DfracOwn q) a).
  #[global] Instance twins_twin1_as_fractional γ q a :
    AsFractional (twins_twin1 γ (DfracOwn q) a) (λ q, twins_twin1 γ (DfracOwn q) a) q.

  Lemma twins_alloc a b :
    a ≡ b →
    ⊢ |==>
      ∃ γ,
      twins_twin1 γ (DfracOwn 1) a ∗
      twins_twin2 γ b.
  Lemma twins_alloc' a :
    ⊢ |==>
      ∃ γ,
      twins_twin1 γ (DfracOwn 1) a ∗ twins_twin2 γ a.

  Lemma twins_twin1_valid γ dq a :
    twins_twin1 γ dq a ⊢
    ⌜✓ dq⌝.
  Lemma twins_twin1_combine γ dq1 a1 dq2 a2 :
    twins_twin1 γ dq1 a1 -∗
    twins_twin1 γ dq2 a2 -∗
      a1 ≡ a2 ∗
      twins_twin1 γ (dq1 ⋅ dq2) a1.
  Lemma twins_twin1_valid_2 γ dq1 a1 dq2 a2 :
    twins_twin1 γ dq1 a1 -∗
    twins_twin1 γ dq2 a2 -∗
      ⌜✓ (dq1 ⋅ dq2)⌝ ∗
      a1 ≡ a2.
  Lemma twins_twin1_agree γ dq1 a1 dq2 a2 :
    twins_twin1 γ dq1 a1 -∗
    twins_twin1 γ dq2 a2 -∗
    a1 ≡ a2.
  Lemma twins_twin1_dfrac_ne γ1 dq1 a1 γ2 dq2 a2 :
    ¬ ✓ (dq1 ⋅ dq2) →
    twins_twin1 γ1 dq1 a1 -∗
    twins_twin1 γ2 dq2 a2 -∗
    ⌜γ1 ≠ γ2⌝.
  Lemma twins_twin1_ne γ1 a1 γ2 dq2 a2 :
    twins_twin1 γ1 (DfracOwn 1) a1 -∗
    twins_twin1 γ2 dq2 a2 -∗
    ⌜γ1 ≠ γ2⌝.
  Lemma twins_twin1_exclusive γ a1 dq2 a2 :
    twins_twin1 γ (DfracOwn 1) a1 -∗
    twins_twin1 γ dq2 a2 -∗
    False.
  Lemma twins_twin1_persist γ dq a :
    twins_twin1 γ dq a ⊢ |==>
    twins_twin1 γ DfracDiscarded a.

  Lemma twins_twin2_exclusive γ a1 a2 :
    twins_twin2 γ a1 -∗
    twins_twin2 γ a2 -∗
    False.

  Lemma twins_agree γ dq a b :
    twins_twin1 γ dq a -∗
    twins_twin2 γ b -∗
    a ≡ b.

  Section ofe_discrete.
    Context `{!OfeDiscrete $ oFunctor_apply F $ iPropO Σ}.

    Lemma twins_twin1_combine_discrete γ dq1 a1 dq2 a2 :
      twins_twin1 γ dq1 a1 -∗
      twins_twin1 γ dq2 a2 -∗
        ⌜a1 ≡ a2⌝ ∗
        twins_twin1 γ (dq1 ⋅ dq2) a1.
    Lemma twins_twin1_valid_2_discrete γ dq1 a1 dq2 a2 :
      twins_twin1 γ dq1 a1 -∗
      twins_twin1 γ dq2 a2 -∗
        ⌜✓ (dq1 ⋅ dq2)⌝ ∗
        ⌜a1 ≡ a2⌝.
    Lemma twins_twin1_agree_discrete γ dq1 a1 dq2 a2 :
      twins_twin1 γ dq1 a1 -∗
      twins_twin1 γ dq2 a2 -∗
      ⌜a1 ≡ a2⌝.

    Lemma twins_agree_discrete γ dq a b :
      twins_twin1 γ dq a -∗
      twins_twin2 γ b -∗
      ⌜a ≡ b⌝.

    Section leibniz_equiv.
      Context `{!LeibnizEquiv $ oFunctor_apply F $ iPropO Σ}.

      Lemma twins_twin1_combine_L γ dq1 a1 dq2 a2 :
        twins_twin1 γ dq1 a1 -∗
        twins_twin1 γ dq2 a2 -∗
          ⌜a1 = a2⌝ ∗
          twins_twin1 γ (dq1 ⋅ dq2) a1.
      Lemma twins_twin1_valid_2_L γ dq1 a1 dq2 a2 :
        twins_twin1 γ dq1 a1 -∗
        twins_twin1 γ dq2 a2 -∗
          ⌜✓ (dq1 ⋅ dq2)⌝ ∗
          ⌜a1 = a2⌝.
      Lemma twins_twin1_agree_L γ dq1 a1 dq2 a2 :
        twins_twin1 γ dq1 a1 -∗
        twins_twin1 γ dq2 a2 -∗
        ⌜a1 = a2⌝.

      Lemma twins_agree_L γ dq a b :
        twins_twin1 γ dq a -∗
        twins_twin2 γ b -∗
        ⌜a = b⌝.
    End leibniz_equiv.
  End ofe_discrete.

  Lemma twins_update_equivI {γ a1 b1} a2 b2 :
    twins_twin1 γ (DfracOwn 1) a1 -∗
    twins_twin2 γ b1 -∗
    a2 ≡ b2 ==∗
      twins_twin1 γ (DfracOwn 1) a2 ∗
      twins_twin2 γ b2.
  Lemma twins_update_equiv {γ a1 b1} a2 b2 :
    a2 ≡ b2 →
    twins_twin1 γ (DfracOwn 1) a1 -∗
    twins_twin2 γ b1 ==∗
      twins_twin1 γ (DfracOwn 1) a2 ∗
      twins_twin2 γ b2.
  Lemma twins_update {γ a b} a' :
    twins_twin1 γ (DfracOwn 1) a -∗
    twins_twin2 γ b ==∗
      twins_twin1 γ (DfracOwn 1) a' ∗
      twins_twin2 γ a'.
End twins_G.

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