Library zoo.iris.base_logic.lib.subpreds

Require Import iris.base_logic.lib.fancy_updates.

Require Import zoo.prelude.
Require Import zoo.iris.base_logic.lib.auth_dgset.
Require Import zoo.iris.base_logic.lib.saved_pred.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.diaframe.
Require Import zoo.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 Type state : option A.
  Implicit Type η : gname.
  Implicit Type Ψ Χ : 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.