From 53741bf7c82c6e50dd47515ce5bfc12073209c49 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Mar 2016 02:36:42 +0100
Subject: [PATCH] Define Assert for heap_lang.

---
 _CoqProject        |  1 +
 heap_lang/assert.v | 23 +++++++++++++++++++++++
 2 files changed, 24 insertions(+)
 create mode 100644 heap_lang/assert.v

diff --git a/_CoqProject b/_CoqProject
index 861ba66eb..a26b5ebab 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -87,6 +87,7 @@ heap_lang/spawn.v
 heap_lang/par.v
 heap_lang/tests.v
 heap_lang/substitution.v
+heap_lang/assert.v
 barrier/barrier.v
 barrier/specification.v
 barrier/protocol.v
diff --git a/heap_lang/assert.v b/heap_lang/assert.v
new file mode 100644
index 000000000..705282b5d
--- /dev/null
+++ b/heap_lang/assert.v
@@ -0,0 +1,23 @@
+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 *)
+
+Instance do_wsubst_assert {X Y} x es (H : X `included` x :: Y) e er :
+  WSubst x es H e er → WSubst x es H (Assert e) (Assert er) | 1.
+Proof. intros; red. by rewrite /Assert /wsubst -/wsubst; f_equal/=. Qed.
+Instance do_wexpr_assert {X Y} (H : X `included` Y) e er :
+  WExpr H e er → WExpr H (Assert e) (Assert er) | 1.
+Proof. intros; red. by rewrite /Assert /wexpr -/wexpr; f_equal/=. Qed.
+
+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 :
+  WP e {{ λ v, v = #true ∧ ▷ Φ #() }} ⊢ WP Assert e {{ Φ }}.
+Proof.
+  rewrite /Assert. wp_focus e; apply wp_mono=>v.
+  apply uPred.const_elim_l=>->. apply wp_assert.
+Qed.
-- 
GitLab