diff options
Diffstat (limited to 'lib/HashedSet.v')
| -rw-r--r-- | lib/HashedSet.v | 14 |
1 files changed, 13 insertions, 1 deletions
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. |