assert.v 1002 Bytes
Newer Older
1
From iris.proofmode Require Import tactics.
2 3
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
4
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
(* just below ;; *)
10 11
Notation "'assert:' e" := (assert (λ: <>, e)%E) (at level 99) : expr_scope.
Notation "'assert:' e" := (assert (λ: <>, e)%V) (at level 99) : val_scope.
12

13
Lemma twp_assert `{!heapG Σ} E (Φ : val  iProp Σ) e :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
14
  WP e @ E [{ v, v = #true  Φ #() }] -
15
  WP (assert: e)%V @ E [{ Φ }].
16
Proof.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
17
  iIntros "HΦ". wp_lam.
18 19 20
  wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.

21
Lemma wp_assert `{!heapG Σ} E (Φ : val  iProp Σ) e :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
22
  WP e @ E {{ v, v = #true   Φ #() }} -
23
  WP (assert: e)%V @ E {{ Φ }}.
24
Proof.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
25
  iIntros "HΦ". wp_lam.
26
  wp_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
27
Qed.