From fd4ae04ee2eee93c7bcdb3acab6de7c3af0380af Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Tue, 12 Mar 2019 15:31:48 +0100
Subject: [PATCH] add `assert`

---
 _CoqProject           |  1 +
 theories/lib/assert.v | 20 ++++++++++++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 theories/lib/assert.v

diff --git a/_CoqProject b/_CoqProject
index bb31c07..c62d724 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -30,6 +30,7 @@ theories/tests/proofmode_tests.v
 theories/lib/lock.v
 theories/lib/counter.v
 theories/lib/Y.v
+theories/lib/assert.v
 
 theories/examples/bit.v
 theories/examples/or.v
diff --git a/theories/lib/assert.v b/theories/lib/assert.v
new file mode 100644
index 0000000..a6cc2c3
--- /dev/null
+++ b/theories/lib/assert.v
@@ -0,0 +1,20 @@
+From iris.heap_lang Require Export lang.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang.lib Require Export assert.
+From reloc Require Import proofmode.
+Set Default Proof Using "Type".
+
+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.
+
+(* Nested relational specifications *)
+Lemma rel_assert_l `{!relocG Σ} K e t A :
+  (∀ K t A, (REL fill K (of_val #true) << t : A) -∗ REL fill K e << t : A) -∗
+  (▷ REL fill K (of_val #()) << t : A) -∗
+  REL fill K (assert (LamV BAnon e)%V) << t : A.
+Proof.
+  iIntros "H1 H2". rel_rec_l. rel_rec_l.
+  rel_apply_l "H1". by rel_if_l.
+Qed.
-- 
GitLab