Library zoo.iris.bi.big_op.big_sepS

From zoo Require Import
  prelude.
From zoo.iris.bi Require Export
  big_op.big_sepL.
From zoo.iris Require Import
  diaframe.
From zoo Require Import
  options.

Section bi.
  Context {PROP : bi}.

  Section big_sepS.
    Context `{Countable K}.

    Implicit Types s : gset K.
    Implicit Types P : PROP.
    Implicit Types Φ : K → PROP.

    Lemma big_sepS_impl_thread {Φ1} P Φ2 s :
      ([∗ set] x ∈ s, Φ1 x) -∗
      P -∗
      □ (
        ∀ x,
        ⌜x ∈ s⌝ →
        Φ1 x -∗
        P -∗
          Φ2 x ∗
          P
      ) -∗
        ([∗ set] x ∈ s, Φ2 x) ∗
        P.
    Lemma big_sepS_impl_thread_fupd `{!BiFUpd PROP} {Φ1} P Φ2 s E :
      ([∗ set] x ∈ s, Φ1 x) -∗
      P -∗
      □ (
        ∀ x,
        ⌜x ∈ s⌝ →
        Φ1 x -∗
        P -∗
          |={E}=>
          Φ2 x ∗
          P
      ) -∗
        |={E}=>
        ([∗ set] x ∈ s, Φ2 x) ∗
        P.

    Lemma big_sepS_exists `{!BiAffine PROP} {V} (Φ : K → V → PROP) s :
      ([∗ set] x ∈ s, ∃ v, Φ x v) ⊢
        ∃ m,
        ⌜dom m = s⌝ ∗
        [∗ map] x ↦ v ∈ m, Φ x v.
  End big_sepS.
End bi.