Library zoo.iris.base_logic.lib.auth_nat_max

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

Class AuthNatMaxG Σ :=
  { #[local] auth_nat_max ۰ G ۰ mono ۰ G :: AuthMonoiG Σ (≤)
  }.

Definition auth_nat_max ۰ Σ :=
  #[auth_monoi ۰ Σ (≤)
  ].
#[global] Instance subG ｰ auth_nat_max ۰ Σ Σ :
  subG auth_nat_max ۰ Σ Σ →
  AuthNatMaxG Σ.

Section auth_nat_max ۰ G.
  Context `{auth_nat_max ۰ G : !AuthNatMaxG Σ}.

  Implicit Type n m p : nat.

  Definition auth_nat_max ۰ auth γ dq n :=
    auth_monoi ۰ auth (≤) γ dq n.
  Definition auth_nat_max ۰ lb γ n :=
    auth_monoi ۰ lb (≤) γ n.

  #[global] Instance auth_nat_max ۰ auth ｰ timeless γ dq n :
    Timeless (auth_nat_max ۰ auth γ dq n).
  #[global] Instance auth_nat_max ۰ lb ｰ timeless γ n :
    Timeless (auth_nat_max ۰ lb γ n).

  #[global] Instance auth_nat_max ۰ auth ｰ persistent γ n :
    Persistent (auth_nat_max ۰ auth γ DfracDiscarded n).
  #[global] Instance auth_nat_max ۰ lb ｰ persistent γ n :
    Persistent (auth_nat_max ۰ lb γ n).

  #[global] Instance auth_nat_max ۰ auth ｰ fractional γ n :
    Fractional (λ q, auth_nat_max ۰ auth γ (DfracOwn q) n).
  #[global] Instance auth_nat_max ۰ auth ｰ as_fractional γ q n :
    AsFractional (auth_nat_max ۰ auth γ (DfracOwn q) n) (λ q, auth_nat_max ۰ auth γ (DfracOwn q) n) q.

  Lemma auth_nat_max ｰ alloc n :
    ⊢ |==>
      ∃ γ ,
      auth_nat_max ۰ auth γ (DfracOwn 1) n.

  Lemma auth_nat_max ۰ auth ｰ valid γ dq a :
    auth_nat_max ۰ auth γ dq a ⊢
    ⌜✓ dq ⌝.
  Lemma auth_nat_max ۰ auth ｰ combine γ dq1 n1 dq2 n2 :
    auth_nat_max ۰ auth γ dq1 n1 -∗
    auth_nat_max ۰ auth γ dq2 n2 -∗
      ⌜n1 = n2 ⌝ ∗
      auth_nat_max ۰ auth γ (dq1 ⋅ dq2) n1.
  Lemma auth_nat_max ۰ auth ｰ valid ｰ2 γ dq1 n1 dq2 n2 :
    auth_nat_max ۰ auth γ dq1 n1 -∗
    auth_nat_max ۰ auth γ dq2 n2 -∗
      ⌜✓ (dq1 ⋅ dq2 )⌝ ∗
      ⌜n1 = n2 ⌝.
  Lemma auth_nat_max ۰ auth ｰ agree γ dq1 n1 dq2 n2 :
    auth_nat_max ۰ auth γ dq1 n1 -∗
    auth_nat_max ۰ auth γ dq2 n2 -∗
    ⌜n1 = n2 ⌝.
  Lemma auth_nat_max ۰ auth ｰ dfrac ｰ ne γ1 dq1 n1 γ2 dq2 n2 :
    ¬ ✓ (dq1 ⋅ dq2 ) →
    auth_nat_max ۰ auth γ1 dq1 n1 -∗
    auth_nat_max ۰ auth γ2 dq2 n2 -∗
    ⌜γ1 ≠ γ2 ⌝.
  Lemma auth_nat_max ۰ auth ｰ ne γ1 n1 γ2 dq2 n2 :
    auth_nat_max ۰ auth γ1 (DfracOwn 1) n1 -∗
    auth_nat_max ۰ auth γ2 dq2 n2 -∗
    ⌜γ1 ≠ γ2 ⌝.
  Lemma auth_nat_max ۰ auth ｰ exclusive γ n1 dq2 n2 :
    auth_nat_max ۰ auth γ (DfracOwn 1) n1 -∗
    auth_nat_max ۰ auth γ dq2 n2 -∗
    False.
  Lemma auth_nat_max ۰ auth ｰ persist γ dq n :
    auth_nat_max ۰ auth γ dq n ⊢ |==>
    auth_nat_max ۰ auth γ DfracDiscarded n.

  Lemma auth_nat_max ۰ lb ｰ0 γ :
    ⊢ |==>
      auth_nat_max ۰ lb γ 0.
  Lemma auth_nat_max ۰ lb ｰ get γ q n :
    auth_nat_max ۰ auth γ q n ⊢
    auth_nat_max ۰ lb γ n.
  Lemma auth_nat_max ۰ lb ｰ le {γ n} n' :
    n' ≤ n →
    auth_nat_max ۰ lb γ n ⊢
    auth_nat_max ۰ lb γ n'.
  Lemma auth_nat_max ۰ lb ｰ max γ n1 n2 :
    auth_nat_max ۰ lb γ n1 -∗
    auth_nat_max ۰ lb γ n2 -∗
    auth_nat_max ۰ lb γ (n1 `max ` n2).

  Lemma auth_nat_max ۰ lb ｰ valid γ dq n m :
    auth_nat_max ۰ auth γ dq n -∗
    auth_nat_max ۰ lb γ m -∗
    ⌜m ≤ n ⌝.

  Lemma auth_nat_max ｰ update {γ n} n' :
    n ≤ n' →
    auth_nat_max ۰ auth γ (DfracOwn 1) n ⊢ |==>
    auth_nat_max ۰ auth γ (DfracOwn 1) n'.
End auth_nat_max ۰ G.

#[global] Opaque auth_nat_max ۰ auth.
#[global] Opaque auth_nat_max ۰ lb.