cardinal is promoted to the rank of primitive member of the FMap interface

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10605 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 19 insertions, 0 deletions

diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 7bf944b85..b00c6b493 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -276,6 +276,15 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Definition elements (m : t A) := xelements m xH.
 
+  (** [cardinal] *)
+
+  Fixpoint cardinal (m : t A) : nat :=
+    match m with 
+      | Leaf => 0%nat 
+      | Node l None r => (cardinal l + cardinal r)%nat
+      | Node l (Some _) r => S (cardinal l + cardinal r)
+    end.
+
   Section CompcertSpec.
 
   Theorem gempty:
@@ -556,6 +565,16 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     exact (xelements_complete i xH m v H).
   Qed.
 
+  Lemma cardinal_1 : 
+   forall (m: t A), cardinal m = length (elements m).
+  Proof.
+   unfold elements.
+   intros m; set (p:=1); clearbody p; revert m p.
+   induction m; simpl; auto; intros.
+   rewrite (IHm1 (append p 2)), (IHm2 (append p 3)); auto.
+   destruct o; rewrite app_length; simpl; omega.
+  Qed.
+
   End CompcertSpec.
 
   Definition MapsTo (i:positive)(v:A)(m:t A) := find i m = Some v.