Library zoo.iris.base_logic.lib.auth_frac

From iris.algebra Require Import
  lib.frac_auth.

From zoo Require Import
  prelude.
From zoo.common Require Import
  math.
From zoo.iris.base_logic Require Export
  lib.base.
From zoo.iris Require Import
  diaframe.
From zoo Require Import
  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 Types q : frac.
  Implicit Types 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 Types q : frac.
  Implicit Types 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.