Library iris.heap_lang.lib.assert

From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.

Definition assert : val :=
  λ: "v", if: "v" #() then #() else #0 #0. Notation "'assert:' e" := (assert (λ: ≠, e))%E (at level 99) : expr_scope.
Global Opaque assert.

Lemma wp_assert {Σ} E (Φ : val → iProp heap_lang Σ) e `{!Closed [] e} :
  (|={E}=>> |={E}=>> WP e @ E {{ v, ⧆(v = #true) ★ ▷ |={E}=>> Φ #() }}) ⊢ WP assert: e @ E {{ Φ }}.
Proof.
  iIntros "HΦ". rewrite /assert. wp_let. iPsvs "HΦ". iPvsIntro.
  wp_seq. iPsvs "HΦ". iPvsIntro.
  iApply wp_wand_r; iFrame "HΦ". iIntros "@". iIntros (v) "[% HΦ']"; subst.
  wp_if. iPsvs "HΦ'". iPvsIntro. wp_value. done.
Qed.