Library zoo.iris.base_logic.lib.mono_gmap

From zoo Require Import
  prelude.
From zoo.common Require Import
  relations.
From zoo.iris.base_logic Require Export
  lib.base.
From zoo.iris.base_logic Require Import
  lib.auth_mono.
From zoo.iris Require Import
  diaframe.
From zoo Require Import
  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 Types v : V.
  Implicit Types 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.