diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 09:11:12 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 09:11:12 +0100 |
| commit | 9cf4ca7760982b40e5721b2d6510eae0ced248a8 (patch) | |
| tree | 78bb00e9705d690f4b567268330c8f47f0a2751d /lib | |
| parent | 33c7fc589ebbbd0ebda9739c479bbd9ee7e526db (diff) | |
| download | compcert-kvx-9cf4ca7760982b40e5721b2d6510eae0ced248a8.tar.gz compcert-kvx-9cf4ca7760982b40e5721b2d6510eae0ced248a8.zip | |
forward_move_l
Diffstat (limited to 'lib')
| -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. |