Library zoo.iris.base_logic.lib.subprops

From iris.base_logic Require Import
  lib.fancy_updates.

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

Implicit Types state : bool.

Class SubpropsG Σ :=
  { #[local] subprops_G_subpreds_G :: SubpredsG Σ ()
  }.

Definition subprops_Σ :=
  #[subpreds_Σ ()
  ].
#[global] Instance subG_subprops_Σ Σ :
  subG subprops_Σ Σ →
  SubpropsG Σ.

Section subprops_G.
  Context `{subprops_G : !SubpropsG Σ}.

  Implicit Types P Q : iProp Σ.

  Definition subprops_auth γ P state :=
    subpreds_auth γ (λ _, P) (if state then Some () else None).

  Definition subprops_frag γ Q :=
    subpreds_frag γ (λ _, Q).

  #[global] Instance subprops_auth_ne γ n :
    Proper ((≡{n}≡) ==> (=) ==> (≡{n}≡)) (subprops_auth γ).
  #[global] Instance subprops_auth_proper γ :
    Proper ((≡) ==> (=) ==> (≡)) (subprops_auth γ).
  #[global] Instance subprops_frag_contractive γ :
    Contractive (subprops_frag γ).
  #[global] Instance subprops_frag_proper γ :
    Proper ((≡) ==> (≡)) (subprops_frag γ).

  Lemma subprops_alloc P :
    ⊢ |==>
      ∃ γ,
      subprops_auth γ P false ∗
      subprops_frag γ P.

  Lemma subprops_wand `{inv_G : !invGS Σ} {γ P state Q1} Q2 E :
    ▷ subprops_auth γ P state -∗
    subprops_frag γ Q1 -∗
    (Q1 -∗ Q2) ={E}=∗
      ▷ subprops_auth γ P state ∗
      subprops_frag γ Q2.
  Lemma subprops_split `{inv_G : !invGS Σ} {γ P state} Q1 Q2 E :
    ▷ subprops_auth γ P state -∗
    subprops_frag γ (Q1 ∗ Q2) ={E}=∗
      ▷ subprops_auth γ P state ∗
      subprops_frag γ Q1 ∗
      subprops_frag γ Q2.
  Lemma subprops_divide `{inv_G : !invGS Σ} {γ P state} Qs E :
    ▷ subprops_auth γ P state -∗
    subprops_frag γ ([∗ list] Q ∈ Qs, Q) ={E}=∗
      ▷ subprops_auth γ P state ∗
      [∗ list] Q ∈ Qs, subprops_frag γ Q.

  Lemma subprops_produce γ P :
    subprops_auth γ P false -∗
    P -∗
    subprops_auth γ P true.

  Lemma subprops_consume `{inv_G : !invGS Σ} γ P Q E :
    ▷ subprops_auth γ P true -∗
    subprops_frag γ Q ={E}=∗
      ▷ subprops_auth γ P true ∗
      ▷^2 Q.
End subprops_G.

#[global] Opaque subprops_auth.
#[global] Opaque subprops_frag.