Library zoo.iris.base_logic.lib.subpreds

From iris.base_logic Require Import
  lib.fancy_updates.

From zoo Require Import
  prelude.
From zoo.iris.base_logic Require Import
  lib.auth_dgset
  lib.saved_pred.
From zoo.iris.base_logic Require Export
  lib.base.
From zoo.iris Require Import
  diaframe.
From zoo Require Import
  options.

Class SubpredsG Σ A :=
  { #[local] subpreds_G_auth_dgset_G :: AuthDgsetG Σ gname
  ; #[local] subpreds_G_saved_pred_G :: SavedPredG Σ A
  }.

Definition subpreds_Σ A :=
  #[auth_dgset_Σ gname
  ; saved_pred_Σ A
  ].
#[global] Instance subG_subpreds_Σ Σ A :
  subG (subpreds_Σ A) Σ →
  SubpredsG Σ A.

Section subpreds_G.
  Context `{subpreds_G : !SubpredsG Σ A}.

  Implicit Types state : option A.
  Implicit Types η : gname.
  Implicit Types Ψ Χ : A → iProp Σ.

  Definition subpreds_auth γ Ψ state : iProp Σ :=
    ∃ ηs,
    auth_dgset_auth γ (DfracOwn 1) ηs ∗
      ∀ x,
      (if state is Some y then ⌜x = y⌝ else Ψ x) -∗
      [∗ set] η ∈ ηs,
        ∃ Χ,
        saved_pred η Χ ∗
        ▷ Χ x.
  #[local] Instance : CustomIpat "auth" :=
    " ( %ηs & {>;}Hauth & Hηs ) ".

  Definition subpreds_frag γ Χ : iProp Σ :=
    ∃ η,
    auth_dgset_frag γ {[η]} ∗
    saved_pred η Χ.
  #[local] Instance : CustomIpat "frag" :=
    " ( %η{} & Hfrag{_{}} & #Hη{} ) ".

  #[global] Instance subpreds_auth_ne γ n :
    Proper (
      (pointwise_relation _ (≡{n}≡)) ==>
      (=) ==>
      (≡{n}≡)
    ) (subpreds_auth γ).
  #[global] Instance subpreds_auth_proper γ :
    Proper (
      (pointwise_relation _ (≡)) ==>
      (=) ==>
      (≡)
    ) (subpreds_auth γ).
  #[global] Instance subpreds_frag_contractive γ n :
    Proper (
      (pointwise_relation _ (dist_later n)) ==>
      (≡{n}≡)
    ) (subpreds_frag γ).
  #[global] Instance subpreds_frag_proper γ :
    Proper (
      (pointwise_relation _ (≡)) ==>
      (≡)
    ) (subpreds_frag γ).

  Lemma subpreds_alloc Ψ :
    ⊢ |==>
      ∃ γ,
      subpreds_auth γ Ψ None ∗
      subpreds_frag γ Ψ.

  Lemma subpreds_split_wand `{inv_G : !invGS Σ} {γ Ψ state Χ} Χ1 Χ2 E :
    ▷ subpreds_auth γ Ψ state -∗
    subpreds_frag γ Χ -∗
    (∀ x, Χ x -∗ Χ1 x ∗ Χ2 x) ={E}=∗
      ▷ subpreds_auth γ Ψ state ∗
      subpreds_frag γ Χ1 ∗
      subpreds_frag γ Χ2.
  Lemma subpreds_wand `{inv_G : !invGS Σ} {γ Ψ state Χ1} Χ2 E :
    ▷ subpreds_auth γ Ψ state -∗
    subpreds_frag γ Χ1 -∗
    (∀ x, Χ1 x -∗ Χ2 x) ={E}=∗
      ▷ subpreds_auth γ Ψ state ∗
      subpreds_frag γ Χ2.
  Lemma subpreds_split `{inv_G : !invGS Σ} {γ Ψ state} Χ1 Χ2 E :
    ▷ subpreds_auth γ Ψ state -∗
    subpreds_frag γ (λ x, Χ1 x ∗ Χ2 x)%I ={E}=∗
      ▷ subpreds_auth γ Ψ state ∗
      subpreds_frag γ Χ1 ∗
      subpreds_frag γ Χ2.
  Lemma subpreds_divide `{inv_G : !invGS Σ} {γ Ψ state} Χs E :
    ▷ subpreds_auth γ Ψ state -∗
    subpreds_frag γ (λ x, [∗ list] Χ ∈ Χs, Χ x) ={E}=∗
      ▷ subpreds_auth γ Ψ state ∗
      [∗ list] Χ ∈ Χs, subpreds_frag γ Χ.

  Lemma subpreds_produce {γ Ψ} x :
    subpreds_auth γ Ψ None -∗
    Ψ x -∗
    subpreds_auth γ Ψ (Some x).

  Lemma subpreds_consume `{inv_G : !invGS Σ} γ Ψ x Χ E :
    ▷ subpreds_auth γ Ψ (Some x) -∗
    subpreds_frag γ Χ ={E}=∗
      ▷ subpreds_auth γ Ψ (Some x) ∗
      ▷^2 Χ x.
End subpreds_G.

#[global] Opaque subpreds_auth.
#[global] Opaque subpreds_frag.