Library zoo_std.assume

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base.
From zoo_std Require Import
  diverge.
From zoo Require Import
  options.

Definition assume : val :=
  fun: "b" ⇒
    if: ¬ "b" then
      diverge ().

Section zoo_G.
  Context `{zoo_G : !ZooG Σ}.

  Lemma assume𑁒spec (b : bool) Φ :
    ▷ (⌜b = true⌝ → Φ ()%V) -∗
    WP assume #b {{ Φ }}.
  Lemma assume𑁒spec' ϕ `{!Decision ϕ} Φ :
    ▷ (⌜ϕ⌝ → Φ ()%V) -∗
    WP assume #(bool_decide ϕ) {{ Φ }}.
End zoo_G.

#[global] Opaque assume.