assert.v 946 Bytes
Newer Older
1 2 3 4 5 6
From iris.heap_lang Require Export derived.
From iris.heap_lang Require Import wp_tactics substitution notation.

Definition Assert {X} (e : expr X) : expr X :=
  if: e then #() else #0 #0. (* #0 #0 is unsafe *)

7 8
Instance do_wexpr_assert {X Y} (H : X `included` Y) e er :
  WExpr H e er  WExpr H (Assert e) (Assert er) := _.
9
Instance do_wsubst_assert {X Y} x es (H : X `included` x :: Y) e er :
10
  WSubst x es H e er  WSubst x es H (Assert e) (Assert er).
11
Proof. intros; red. by rewrite /Assert /wsubst -/wsubst; f_equal/=. Qed.
12
Typeclasses Opaque Assert.
13 14 15 16 17 18

Lemma wp_assert {Σ} (Φ : val  iProp heap_lang Σ) :
   Φ #()  WP Assert #true {{ Φ }}.
Proof. by rewrite -wp_if_true -wp_value. Qed.

Lemma wp_assert' {Σ} (Φ : val  iProp heap_lang Σ) e :
19
  WP e {{ v, v = #true   Φ #() }}  WP Assert e {{ Φ }}.
20 21 22 23
Proof.
  rewrite /Assert. wp_focus e; apply wp_mono=>v.
  apply uPred.const_elim_l=>->. apply wp_assert.
Qed.