Library zoo.iris.base_logic.lib.mono_gset

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

Class MonoGsetG Σ A `{Countable A} :=
  { #[local] mono_gset ۰ G ۰ mono ۰ G :: AuthMonoG Σ (A := leibnizO (gset A)) subseteq
  }.

Definition mono_gset ۰ Σ A `{Countable A} :=
  #[auth_mono ۰ Σ (A := leibnizO (gset A)) subseteq
  ].
#[global] Instance subG ｰ mono_gset ۰ Σ Σ V `{Countable V} :
  subG (mono_gset ۰ Σ V) Σ →
  MonoGsetG Σ V.

Section mono_gset ۰ G.
  Context `{mono_gset ۰ G : MonoGsetG Σ A}.

  Implicit Type a : A.
  Implicit Type s : gset A.

  Definition mono_gset ۰ auth γ dq s :=
    auth_mono ۰ auth subseteq γ dq s.
  Definition mono_gset ۰ lb γ s :=
    auth_mono ۰ lb subseteq γ s.
  Definition mono_gset ۰ elem γ a :=
    mono_gset ۰ lb γ {[a ]}.

  #[global] Instance mono_gset ۰ auth ｰ proper γ dq :
    Proper ((≡) ==> (≡)) (mono_gset ۰ auth γ dq).
  #[global] Instance mono_gset ۰ lb ｰ proper γ :
    Proper ((≡) ==> (≡)) (mono_gset ۰ lb γ).

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

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

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

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

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

  Lemma mono_gset ۰ lb ｰ get γ dq s :
    mono_gset ۰ auth γ dq s ⊢
    mono_gset ۰ lb γ s.
  Lemma mono_gset ۰ lb ｰ mono {γ s} s' :
    s' ⊆ s →
    mono_gset ۰ lb γ s ⊢
    mono_gset ۰ lb γ s'.
  Lemma mono_gset ۰ elem ｰ get {γ dq s} a :
    a ∈ s →
    mono_gset ۰ auth γ dq s ⊢
    mono_gset ۰ elem γ a.

  Lemma mono_gset ۰ lb ｰ valid γ dq s1 s2 :
    mono_gset ۰ auth γ dq s1 -∗
    mono_gset ۰ lb γ s2 -∗
    ⌜s2 ⊆ s1 ⌝.
  Lemma mono_gset ۰ elem ｰ valid γ dq s a :
    mono_gset ۰ auth γ dq s -∗
    mono_gset ۰ elem γ a -∗
    ⌜a ∈ s ⌝.

  Lemma mono_gset ｰ update {γ s} s' :
    s ⊆ s' →
    mono_gset ۰ auth γ (DfracOwn 1) s ⊢ |==>
    mono_gset ۰ auth γ (DfracOwn 1) s'.
  Lemma mono_gset ｰ insert {γ s} a :
    mono_gset ۰ auth γ (DfracOwn 1) s ⊢ |==>
    mono_gset ۰ auth γ (DfracOwn 1) ({[a ]} ∪ s).
  Lemma mono_gset ｰ insert' {γ s} a :
    mono_gset ۰ auth γ (DfracOwn 1) s ⊢ |==>
      mono_gset ۰ auth γ (DfracOwn 1) ({[a ]} ∪ s) ∗
      mono_gset ۰ elem γ a.
End mono_gset ۰ G.

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