Library zoo.program_logic.counter

Require Import iris.base_logic.lib.invariants.

Require Import zoo.prelude.
Require Import zoo.iris.bi.big_op.
Require Import zoo.base.
Require Import zoo.options.

Definition zoo_counter٠incr : val :=
  𝗳𝘂𝗻 ⎽ →
    FAA (#zoo_counter).[contents] 1.

Section zoo۰G.
  Context `{zoo۰G : !ZooG Σ}.

  Lemma zoo_counter٠incrｰspec ids v :
    {{{
      [∗ list] id ∈ ids,
        ∃ v,
        zoo_counter۰at id v
    }}}
      zoo_counter٠incr ()
    {{{
      id
    , RET #id;
      zoo_counter۰at id v ∗
      ⌜Forall (.≠ id) ids⌝
    }}}.
End zoo۰G.