Library zoo.iris.bi.big_op.big_sepS

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

Section bi.
  Context {PROP : bi}.

  Section big_sepS.
    Context `{Countable K}.

    Implicit Type s : gset K.
    Implicit Type P : PROP.
    Implicit Type Φ : 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ｰ∃ `{!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.