add `assert`

_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

theories/lib/assert.v

+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.