Library zoo.iris.base_logic.lib.subprops

Require Import iris.base_logic.lib.fancy_updates.

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

Implicit Type 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 Type 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.