Library zoo.iris.base_logic.lib.auth_frac

Require Import iris.algebra.lib.frac_auth.

Require Import zoo.prelude.
Require Import zoo.common.math.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.diaframe.
Require Import zoo.options.

Class AuthFracG Σ A :=
  { #[local] auth_frac۰G۰inG :: inG Σ (frac_authUR A)
  }.

Definition auth_frac۰Σ A :=
  #[GFunctor (frac_authUR A)
  ].
#[global] Instance subGｰauth_frac۰Σ Σ A :
  subG (auth_frac۰Σ A) Σ →
  AuthFracG Σ A.

Section auth_frac۰G.
  Context `{auth_frac۰G : !AuthFracG Σ A}.

  Implicit Type q : frac.
  Implicit Type x y : A.

  Definition auth_frac۰auth γ x :=
    own γ (frac_auth_auth (DfracOwn 1) x).
  Definition auth_frac۰frag γ q y :=
    own γ (frac_auth_frag q y).

  #[global] Instance auth_frac۰authｰproper γ :
    Proper ((≡) ==> (≡)) (auth_frac۰auth γ).
  #[global] Instance auth_frac۰fragｰproper γ q :
    Proper ((≡) ==> (≡)) (auth_frac۰frag γ q).

  #[global] Instance auth_frac۰authｰtimeless γ x :
    Discrete x →
    Timeless (auth_frac۰auth γ x).
  #[global] Instance auth_frac۰fragｰtimeless γ q y :
    Discrete y →
    Timeless (auth_frac۰frag γ q y).

  Lemma auth_fracｰalloc x :
    ✓ x →
    ⊢ |==>
      ∃ γ,
      auth_frac۰auth γ x ∗
      auth_frac۰frag γ 1 x.

  Lemma auth_frac۰authｰvalid `{!CmraDiscrete A} γ x :
    auth_frac۰auth γ x ⊢
    ⌜✓ x⌝.

  Lemma auth_frac۰fragｰvalid `{!CmraDiscrete A} γ q y :
    auth_frac۰frag γ q y ⊢
      ⌜q ≤ 1⌝%Qp ∗
      ⌜✓ y⌝.
  Lemma auth_frac۰fragｰsplit {γ q y} q1 y1 q2 y2 :
    q = (q1 + q2)%Qp →
    y = y1 ⋅ y2 →
    auth_frac۰frag γ q y ⊢
      auth_frac۰frag γ q1 y1 ∗
      auth_frac۰frag γ q2 y2.
  Lemma auth_frac۰fragｰcombine γ q1 y1 q2 y2 :
    auth_frac۰frag γ q1 y1 -∗
    auth_frac۰frag γ q2 y2 -∗
    auth_frac۰frag γ (q1 ⋅ q2) (y1 ⋅ y2).
  Lemma auth_frac۰fragｰvalidｰ2 `{!CmraDiscrete A} γ q1 y1 q2 y2 :
    auth_frac۰frag γ q1 y1 -∗
    auth_frac۰frag γ q2 y2 -∗
      ⌜q1 ⋅ q2 ≤ 1⌝%Qp ∗
      ⌜✓ (y1 ⋅ y2)⌝.
  Lemma auth_frac۰fragｰfracｰne `{!CmraDiscrete A} γ1 q1 y1 γ2 q2 y2 :
    ¬ (q1 + q2 ≤ 1)%Qp →
    auth_frac۰frag γ1 q1 y1 -∗
    auth_frac۰frag γ2 q2 y2 -∗
    ⌜γ1 ≠ γ2⌝.
  Lemma auth_frac۰fragｰne `{!CmraDiscrete A} γ1 y1 γ2 q2 y2 :
    auth_frac۰frag γ1 1 y1 -∗
    auth_frac۰frag γ2 q2 y2 -∗
    ⌜γ1 ≠ γ2⌝.
  Lemma auth_frac۰fragｰexclusive `{!CmraDiscrete A} γ y1 q2 y2 :
    auth_frac۰frag γ 1 y1 -∗
    auth_frac۰frag γ q2 y2 -∗
    False.

  Lemma auth_fracｰauthｰfragｰagree `{!CmraDiscrete A} γ x y :
    auth_frac۰auth γ x -∗
    auth_frac۰frag γ 1 y -∗
    ⌜x ≡ y⌝.
  Lemma auth_fracｰauthｰfragｰagreeｰL `{!CmraDiscrete A, !LeibnizEquiv A} γ x y :
    auth_frac۰auth γ x -∗
    auth_frac۰frag γ 1 y -∗
    ⌜x = y⌝.

  Lemma auth_fracｰauthｰfragｰincluded `{!CmraDiscrete A, !CmraTotal A} γ x q y :
    auth_frac۰auth γ x -∗
    auth_frac۰frag γ q y -∗
    ⌜y ≼ x⌝.

  Lemma auth_fracｰupdate {γ x q y} x' y' :
    (x, y) ¬l~> (x', y') →
    auth_frac۰auth γ x -∗
    auth_frac۰frag γ q y ==∗
      auth_frac۰auth γ x' ∗
      auth_frac۰frag γ q y'.
  Lemma auth_fracｰupdateｰ1 {γ x y} x' :
    ✓ x' →
    auth_frac۰auth γ x -∗
    auth_frac۰frag γ 1 y ==∗
      auth_frac۰auth γ x' ∗
      auth_frac۰frag γ 1 x'.
End auth_frac۰G.

#[global] Opaque auth_frac۰auth.
#[global] Opaque auth_frac۰frag.

Section auth_frac۰G.
  Context {A : ucmra}.
  Context `{auth_frac۰G : !AuthFracG Σ A}.

  Implicit Type q : frac.
  Implicit Type x y : A.

  Lemma auth_frac۰fragｰdivide {γ q y} ys :
    y = foldr (⋅) ε ys →
    auth_frac۰frag γ q y ⊢
    [∗ list] y ∈ ys, auth_frac۰frag γ (q / Qp۰of_nat (length ys)) y.
  Lemma auth_frac۰fragｰdivide' {γ q y} q' ys :
    q = (Qp۰of_nat (length ys) × q')%Qp →
    y = foldr (⋅) ε ys →
    auth_frac۰frag γ q y ⊢
    [∗ list] y ∈ ys, auth_frac۰frag γ q' y.
  Lemma auth_frac۰fragｰgather γ q ys :
    0 < length ys →
    ([∗ list] y ∈ ys, auth_frac۰frag γ q y) ⊢
    auth_frac۰frag γ (Qp۰of_nat (length ys) × q) (foldr (⋅) ε ys).
End auth_frac۰G.