Library zoo.iris.base_logic.lib.mono_gmap

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 MonoGmapG Σ K V `{Countable K} :=
  { #[local] mono_gmap ۰ G ۰ mono ۰ G :: AuthMonoG Σ (A := leibnizO (gmap K V)) (subseteq (A := gmap K V))
  }.

Definition mono_gmap ۰ Σ K V `{Countable K} :=
  #[auth_mono ۰ Σ (A := leibnizO (gmap K V)) (subseteq (A := gmap K V))
  ].
#[global] Instance subG ｰ mono_gmap ۰ Σ Σ K V `{Countable K} :
  subG (mono_gmap ۰ Σ K V) Σ →
  MonoGmapG Σ K V.

Section mono_gmap ۰ G.
  Context `{mono_gmap ۰ G : MonoGmapG Σ K V}.

  Implicit Type v : V.
  Implicit Type m : gmap K V.

  #[local] Instance map ｰ subseteq ｰ partialorder :
    PartialOrder (A := gmap K V) subseteq.

  Definition mono_gmap ۰ auth γ dq m :=
    auth_mono ۰ auth subseteq γ dq m.
  Definition mono_gmap ۰ lb γ m :=
    auth_mono ۰ lb subseteq γ m.
  Definition mono_gmap ۰ at γ i v :=
    mono_gmap ۰ lb γ {[i := v ]}.
  Definition mono_gmap ۰ elem γ i : iProp Σ :=
    ∃ v ,
    mono_gmap ۰ at γ i v.

  #[global] Instance mono_gmap ۰ auth ｰ timeless γ dq m :
    Timeless (mono_gmap ۰ auth γ dq m).
  #[global] Instance mono_gmap ۰ lb ｰ timeless γ m :
    Timeless (mono_gmap ۰ lb γ m).
  #[global] Instance mono_gmap ۰ elem ｰ timeless γ i :
    Timeless (mono_gmap ۰ elem γ i).

  #[global] Instance mono_gmap ۰ auth ｰ persistent γ m :
    Persistent (mono_gmap ۰ auth γ DfracDiscarded m).
  #[global] Instance mono_gmap ۰ lb ｰ persistent γ m :
    Persistent (mono_gmap ۰ lb γ m).
  #[global] Instance mono_gmap ۰ elem ｰ persistent γ i :
    Persistent (mono_gmap ۰ elem γ i).

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

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

  Lemma mono_gmap ۰ at ｰ to ｰ elem γ i v :
    mono_gmap ۰ at γ i v ⊢
    mono_gmap ۰ elem γ i.
  Lemma mono_gmap ۰ elem ｰ to ｰ at γ i :
    mono_gmap ۰ elem γ i ⊢
      ∃ v ,
      mono_gmap ۰ at γ i v.

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

  Lemma mono_gmap ۰ lb ｰ get γ dq m :
    mono_gmap ۰ auth γ dq m ⊢
    mono_gmap ۰ lb γ m.
  Lemma mono_gmap ۰ lb ｰ mono {γ m} m' :
    m' ⊆ m →
    mono_gmap ۰ lb γ m ⊢
    mono_gmap ۰ lb γ m'.
  Lemma mono_gmap ۰ at ｰ get {γ dq m} i v :
    m !! i = Some v →
    mono_gmap ۰ auth γ dq m ⊢
    mono_gmap ۰ at γ i v.

  Lemma mono_gmap ۰ lb ｰ valid γ dq m1 m2 :
    mono_gmap ۰ auth γ dq m1 -∗
    mono_gmap ۰ lb γ m2 -∗
    ⌜m2 ⊆ m1 ⌝.
  Lemma mono_gmap ۰ at ｰ valid γ dq m i v :
    mono_gmap ۰ auth γ dq m -∗
    mono_gmap ۰ at γ i v -∗
    ⌜m !! i = Some v ⌝.
  Lemma mono_gmap ۰ elem ｰ valid γ dq m i :
    mono_gmap ۰ auth γ dq m -∗
    mono_gmap ۰ elem γ i -∗
      ∃ v ,
      ⌜m !! i = Some v ⌝.

  Lemma mono_gmap ｰ update {γ m} m' :
    m ⊆ m' →
    mono_gmap ۰ auth γ (DfracOwn 1) m ⊢ |==>
    mono_gmap ۰ auth γ (DfracOwn 1) m'.
  Lemma mono_gmap ｰ insert {γ m} i v :
    m !! i = None →
    mono_gmap ۰ auth γ (DfracOwn 1) m ⊢ |==>
    mono_gmap ۰ auth γ (DfracOwn 1) (<[i := v ]> m).
  Lemma mono_gmap ｰ insert' {γ m} i v :
    m !! i = None →
    mono_gmap ۰ auth γ (DfracOwn 1) m ⊢ |==>
      mono_gmap ۰ auth γ (DfracOwn 1) (<[i := v ]> m) ∗
      mono_gmap ۰ at γ i v.
End mono_gmap ۰ G.

#[global] Opaque mono_gmap ۰ auth.
#[global] Opaque mono_gmap ۰ lb.
#[global] Opaque mono_gmap ۰ elem.