Forked from
Iris / Iris
6440 commits behind the upstream repository.
-
Robbert Krebbers authored
We reify to a representation of expressions that includes an explicit constructor for closed terms. Substitution can then be implemented as the identify, which enables us to perform it using computation.
Robbert Krebbers authoredWe reify to a representation of expressions that includes an explicit constructor for closed terms. Substitution can then be implemented as the identify, which enables us to perform it using computation.
assert.v 595 B
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Definition assert : val :=
λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Global Opaque assert.
Lemma wp_assert {Σ} (Φ : val → iProp heap_lang Σ) e `{!Closed [] e} :
WP e {{ v, v = #true ∧ ▷ Φ #() }} ⊢ WP assert: e {{ Φ }}.
Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
iApply wp_wand_r; iFrame "HΦ"; iIntros (v) "[% ?]"; subst.
wp_if. done.
Qed.