From 9cf4ca7760982b40e5721b2d6510eae0ced248a8 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 10 Mar 2020 09:11:12 +0100
Subject: forward_move_l

---
 lib/HashedSet.v | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'lib/HashedSet.v')

diff --git a/lib/HashedSet.v b/lib/HashedSet.v
index bd9cd9c0..00e01612 100644
--- a/lib/HashedSet.v
+++ b/lib/HashedSet.v
@@ -1058,6 +1058,10 @@ Axiom elements_complete:
   forall (m: t) (i: positive),
     In i (elements m) -> contains m i = true.
 
+Axiom elements_spec:
+  forall (m: t) (i: positive),
+    In i (elements m) <-> contains m i = true.
+
 Parameter fold:
   forall {B : Type},
     (B -> positive -> B) -> t -> B -> B.
@@ -1304,7 +1308,6 @@ Proof.
   apply PSet_internals.elements_correct.
 Qed.
 
-
 Theorem elements_complete:
   forall (m: pset) (i: positive),
     In i (elements m) -> contains m i = true.
@@ -1314,6 +1317,15 @@ Proof.
 Qed.
 
 
+Theorem elements_spec:
+  forall (m: pset) (i: positive),
+    In i (elements m) <-> contains m i = true.
+Proof.
+  intros. split.
+  - apply elements_complete.
+  - apply elements_correct.
+Qed.
+
 Definition fold {B : Type} (f : B -> positive -> B) (m : t) (v : B) : B :=
   PSet_internals.fold f (pset_x m) v.
 
-- 
cgit