Library zoo.iris.bi.big_op.big_sepM

Require Import zoo.prelude.
Require Import zoo.common.fin_maps.
Require Import zoo.iris.bi.big_op.base.
Require Import zoo.iris.diaframe.
Require Import zoo.options.

Section bi.
  Context {PROP : bi}.

  Section big_sepM.
    Context `{Countable K} {A : Type}.

    Implicit Type m : gmap K A.
    Implicit Type P : PROP.
    Implicit Type Φ : K → A → PROP.

    Lemma big_sepMｰsingleton₁ Φ k v :
      ([∗ map] k ↦ v ∈ {[k := v]}, Φ k v) ⊢
      Φ k v.
    Lemma big_sepMｰsingleton₂ Φ k v :
      Φ k v ⊢
      [∗ map] k ↦ v ∈ {[k := v]}, Φ k v.

    Lemma big_sepMｰimplｰthread {Φ1} P Φ2 m :
      ([∗ map] k ↦ x ∈ m, Φ1 k x) -∗
      P -∗
      □ (
        ∀ k x,
        ⌜m !! k = Some x⌝ →
        Φ1 k x -∗
        P -∗
          Φ2 k x ∗
          P
      ) -∗
        ([∗ map] k ↦ x ∈ m, Φ2 k x) ∗
        P.
    Lemma big_sepMｰimplｰthreadｰfupd `{!BiFUpd PROP} {Φ1} P Φ2 m E :
      ([∗ map] k ↦ x ∈ m, Φ1 k x) -∗
      P -∗
      □ (
        ∀ k x,
        ⌜m !! k = Some x⌝ →
        Φ1 k x -∗
        P -∗
          |={E}=>
          Φ2 k x ∗
          P
      ) -∗
        |={E}=>
        ([∗ map] k ↦ x ∈ m, Φ2 k x) ∗
        P.

    Lemma big_sepMｰdelete₁ {Φ m} i x :
      m !! i = Some x →
      ([∗ map] k ↦ y ∈ m, Φ k y) ⊢
        Φ i x ∗
        [∗ map] k ↦ y ∈ delete i m, Φ k y.
    Lemma big_sepMｰdelete₂ Φ m i x :
      m !! i = Some x →
      ([∗ map] k ↦ y ∈ delete i m, Φ k y) -∗
      Φ i x -∗
      [∗ map] k ↦ y ∈ m, Φ k y.

    Lemma big_sepMｰinsertｰdelete₂ {Φ m i} x :
      ([∗ map] k ↦ y ∈ delete i m, Φ k y) -∗
      Φ i x -∗
      [∗ map] k ↦ y ∈ <[i := x]> m, Φ k y.

    Lemma big_sepMｰkmap Φ f `{!Inj (=) (=) f} m :
      ([∗ map] k ↦ x ∈ (kmap f m), Φ k x) ⊣⊢
      [∗ map] k ↦ x ∈ m, Φ (f k) x.
  End big_sepM.

  Section big_sepM.
    Context {A : Type}.

    Implicit Type Φ : nat → A → PROP.

    Lemma big_sepMｰmap_seq start l Φ :
      ([∗ map] k ↦ x ∈ map_seq start l, Φ k x) ⊣⊢
      [∗ list] k ↦ x ∈ l, Φ (start + k) x.
    Lemma big_sepMｰmap_seqｰ0 l Φ :
      ([∗ map] k ↦ x ∈ map_seq 0 l, Φ k x) ⊣⊢
      [∗ list] k ↦ x ∈ l, Φ k x.
  End big_sepM.
End bi.