Library zoo.iris.base_logic.lib.auth_nat_min

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

Class AuthNatMinG Σ :=
  { #[local] auth_nat_min ۰ G ۰ mono ۰ G :: AuthMonoG Σ ge
  }.

Definition auth_nat_min ۰ Σ :=
  #[auth_mono ۰ Σ ge
  ].
#[global] Instance subG ｰ auth_nat_min ۰ Σ Σ :
  subG auth_nat_min ۰ Σ Σ →
  AuthNatMinG Σ.

Section auth_nat_min ۰ G.
  Context `{auth_nat_min ۰ G : !AuthNatMinG Σ}.

  Implicit Type n m p : nat.

  Definition auth_nat_min ۰ auth γ dq n :=
    auth_mono ۰ auth ge γ dq n.
  Definition auth_nat_min ۰ ub γ n :=
    auth_mono ۰ lb ge γ n.

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

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

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

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

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

  Lemma auth_nat_min ۰ ub ｰ get γ q n :
    auth_nat_min ۰ auth γ q n ⊢
    auth_nat_min ۰ ub γ n.
  Lemma auth_nat_min ۰ ub ｰ le {γ n} n' :
    n ≤ n' →
    auth_nat_min ۰ ub γ n ⊢
    auth_nat_min ۰ ub γ n'.

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

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

#[global] Opaque auth_nat_min ۰ auth.
#[global] Opaque auth_nat_min ۰ ub.