assert.v 986 Bytes
Newer Older
1
2
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
3
4
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
5
Set Default Proof Using "Type".
6

7
Definition assert : val :=
8
  λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
9
10
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
11

12
Lemma twp_assert `{heapG Σ} E (Φ : val  iProp Σ) e :
13
14
  WP e @ E [{ v, v = #true  Φ #() }] - WP assert: e @ E [{ Φ }].
Proof.
15
  iIntros "HΦ". rewrite /assert. wp_closure. wp_lam. wp_lam.
16
17
18
  wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.

19
Lemma wp_assert `{heapG Σ} E (Φ : val  iProp Σ) e :
20
  WP e @ E {{ v, v = #true   Φ #() }} - WP assert: e @ E {{ Φ }}.
21
Proof.
22
  iIntros "HΦ". rewrite /assert. wp_closure. wp_lam. wp_lam.
23
  wp_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
24
Qed.