Library zoo.iris.base_logic.lib.auth_twins

From zoo Require Import
  prelude.
From zoo.common Require Import
  countable.
From zoo.iris.base_logic Require Export
  lib.base.
From zoo.iris.base_logic Require Import
  lib.ghost_var
  lib.auth_mono
  lib.twins.
From zoo.iris Require Import
  diaframe.
From zoo Require Import
  options.

Class AuthTwinsG Σ (A : ofe) (R : relation A) :=
  { #[local] auth_twins_G_var_G :: GhostVarG Σ (leibnizO gname)
  ; #[local] auth_twins_G_mono_G :: AuthMonoG Σ R
  ; #[local] auth_twins_G_twins_G :: TwinsG Σ A
  }.

Definition auth_twins_Σ (A : ofe) (R : relation A) :=
  #[ghost_var_Σ (leibnizO gname)
  ; auth_mono_Σ R
  ; twins_Σ A
  ].
#[global] Instance subG_auth_twins_Σ Σ (A : ofe) (R : relation A) :
  subG (auth_twins_Σ A R) Σ →
  AuthTwinsG Σ A R.

Section auth_twins_G.
  Context {A : ofe} (R : relation A).
  Context `{auth_twins_G : !AuthTwinsG Σ A R}.

  Notation Rs := (
    rtc R
  ).

  Implicit Types a b : A.

  Record auth_twins_name :=
    { auth_twins_name_var : gname
    ; auth_twins_name_twins : gname
    }.
  Implicit Types γ : auth_twins_name.

  #[global] Instance auth_twins_name_eq_dec : EqDecision auth_twins_name :=
    ltac:(solve_decision).
  #[global] Instance auth_twins_name_countable :
    Countable auth_twins_name.

  Definition auth_twins_auth γ a : iProp Σ :=
    ∃ η,
    ghost_var γ.(auth_twins_name_var) (DfracOwn (1/3)) η ∗
    auth_mono_auth R η (DfracOwn 1) a.
  #[local] Instance : CustomIpat "auth" :=
    " ( %{{pref}_}η & Hvar{} & {{pref}_}Hauth ) ".
  Definition auth_twins_twin1 γ a : iProp Σ :=
    ∃ η,
    ghost_var γ.(auth_twins_name_var) (DfracOwn (1/3)) η ∗
    auth_mono_lb R η a ∗
    twins_twin1 γ.(auth_twins_name_twins) (DfracOwn 1) a.
  #[local] Instance : CustomIpat "twin1" :=
    " ( %{{pref}_}η & Hvar{} & #Hlb{} & Htwin1{_{suff}} ) ".
  Definition auth_twins_twin2 γ a : iProp Σ :=
    ∃ η,
    ghost_var γ.(auth_twins_name_var) (DfracOwn (1/3)) η ∗
    auth_mono_lb R η a ∗
    twins_twin2 γ.(auth_twins_name_twins) a.
  #[local] Instance : CustomIpat "twin2" :=
    " ( %{{pref}_}η & Hvar{} & #Hlb{} & Htwin2{_{suff}} ) ".

  #[global] Instance auth_twins_auth_timeless γ a :
    Timeless (auth_twins_auth γ a).
  #[global] Instance auth_twins_twin1_timeless γ a :
    Discrete a →
    Timeless (auth_twins_twin1 γ a).
  #[global] Instance auth_twins_twin2_timeless γ a :
    Discrete a →
    Timeless (auth_twins_twin2 γ a).

  Lemma auth_twins_alloc a :
    ⊢ |==>
      ∃ γ,
      auth_twins_auth γ a ∗
      auth_twins_twin1 γ a ∗
      auth_twins_twin2 γ a.

  Lemma auth_twins_auth_exclusive `{!AntiSymm (≡) Rs} γ a1 a2 :
    auth_twins_auth γ a1 -∗
    auth_twins_auth γ a2 -∗
    False.
  Lemma auth_twins_auth_exclusive_L `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} γ a1 a2 :
    auth_twins_auth γ a1 -∗
    auth_twins_auth γ a2 -∗
    False.

  Lemma auth_twins_twin1_exclusive γ a1 a2 :
    auth_twins_twin1 γ a1 -∗
    auth_twins_twin1 γ a2 -∗
    False.

  Lemma auth_twins_twin2_exclusive γ a1 a2 :
    auth_twins_twin2 γ a1 -∗
    auth_twins_twin2 γ a2 -∗
    False.

  Lemma auth_twins_valid_1 γ a1 a2 :
    auth_twins_auth γ a1 -∗
    auth_twins_twin1 γ a2 -∗
    ⌜Rs a2 a1⌝.
  Lemma auth_twins_valid_2 γ a1 a2 :
    auth_twins_auth γ a1 -∗
    auth_twins_twin2 γ a2 -∗
    ⌜Rs a2 a1⌝.

  Lemma auth_twins_agree γ a1 a2 :
    auth_twins_twin1 γ a1 -∗
    auth_twins_twin2 γ a2 -∗
    a1 ≡ a2.
  Lemma auth_twins_agree_discrete `{!OfeDiscrete A} γ a1 a2 :
    auth_twins_twin1 γ a1 -∗
    auth_twins_twin2 γ a2 -∗
    ⌜a1 ≡ a2⌝.
  Lemma auth_twins_agree_L `{!OfeDiscrete A} `{!LeibnizEquiv A} γ a1 a2 :
    auth_twins_twin1 γ a1 -∗
    auth_twins_twin2 γ a2 -∗
    ⌜a1 = a2⌝.

  Lemma auth_twins_update_auth {γ a a1 a2} a' :
    auth_twins_auth γ a -∗
    auth_twins_twin1 γ a1 -∗
    auth_twins_twin2 γ a2 ==∗
      auth_twins_auth γ a' ∗
      auth_twins_twin1 γ a' ∗
      auth_twins_twin2 γ a'.
  Lemma auth_twins_update_twins {γ a1 a2} a :
    Rs a a1 →
    Rs a a2 →
    auth_twins_twin1 γ a1 -∗
    auth_twins_twin2 γ a2 ==∗
      auth_twins_twin1 γ a ∗
      auth_twins_twin2 γ a.
  Lemma auth_twins_update_twins_L `{!OfeDiscrete A} `{!LeibnizEquiv A} {γ a1 a2} a :
    Rs a a1 →
    auth_twins_twin1 γ a1 -∗
    auth_twins_twin2 γ a2 ==∗
      auth_twins_twin1 γ a ∗
      auth_twins_twin2 γ a.
End auth_twins_G.

#[global] Opaque auth_twins_auth.
#[global] Opaque auth_twins_twin1.
#[global] Opaque auth_twins_twin2.