Library zoo.iris.bi.big_op.big_sepM

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

Section bi.
  Context {PROP : bi}.

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

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

    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_1 {Φ 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_2 Φ 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_2 {Φ 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 Types Φ : 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.