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

8 files changed, 76 insertions, 11 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index cbc36bc76..974e9d1ae 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1103,6 +1103,19 @@ Proof.
  intros; apply PX.Sort_NoDupA; auto.
 Qed.
 
+Lemma elements_aux_cardinal :
+ forall m acc, (length acc + cardinal m)%nat = length (elements_aux acc m).
+Proof.
+ simple induction m; simpl; intuition.
+ rewrite <- H; simpl.
+ rewrite <- H0; omega.
+Qed.
+
+Lemma elements_cardinal : forall m, cardinal m = length (elements m).
+Proof.
+ exact (fun m => elements_aux_cardinal m nil).
+Qed.
+
 
 
 (** * Fold *)
@@ -1687,6 +1700,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Definition map2 f m (m':t elt') : t elt'' := 
   Bbst (Raw.map2_bst f m m') (Raw.map2_avl f m m').
  Definition elements m : list (key*elt) := Raw.elements m.(this).
+ Definition cardinal m := Raw.cardinal m.(this).
  Definition fold (A:Type) (f:key->elt->A->A) m i := Raw.fold (A:=A) f m.(this) i.
  Definition equal cmp m m' : bool := Raw.equal cmp m.(this) m'.(this).
 
@@ -1766,6 +1780,9 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Lemma elements_3w : forall m, NoDupA eq_key (elements m).  
  Proof. intros m; exact (@Raw.elements_nodup elt m.(this) m.(is_bst)). Qed.
 
+ Lemma cardinal_1 : forall m, cardinal m = length (elements m).
+ Proof. intro m; exact (@Raw.elements_cardinal elt m.(this)). Qed.
+
  Definition Equal cmp m m' := 
    (forall k, In k m <-> In k m') /\ 
    (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).  
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 3a3698239..64702b687 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -571,8 +571,6 @@ Module WProperties (E:DecidableType)(M:WSfun E).
  Section Elt. 
   Variable elt:Set.
 
-  Definition cardinal (m:t elt) := length (elements m).
-
   Definition Equal (m m':t elt) := forall y, find y m = find y m'.
   Definition Add x (e:elt) m m' := forall y, find y m' = find y (add x e m).
 
@@ -598,6 +596,11 @@ Module WProperties (E:DecidableType)(M:WSfun E).
   rewrite H in H0; destruct H0 as (_,H0); inversion H0.
   Qed.
 
+  Lemma elements_empty : elements (@empty elt) = nil.
+  Proof.
+  rewrite <-elements_Empty; apply empty_1.
+  Qed.
+
   Lemma fold_Empty : forall m (A:Set)(f:key->elt->A->A)(i:A),
    Empty m -> fold f m i = i.
   Proof.
@@ -680,17 +683,18 @@ Module WProperties (E:DecidableType)(M:WSfun E).
   elim n; auto.
   Qed.
 
-  Lemma cardinal_fold : forall m, cardinal m = fold (fun _ _ => S) m 0.
+  Lemma cardinal_fold : forall m : t elt, 
+   cardinal m = fold (fun _ _ => S) m 0.
   Proof.
-  intros; unfold cardinal; rewrite fold_1.
+  intros; rewrite cardinal_1, fold_1.
   symmetry; apply fold_left_length; auto.
   Qed.
 
-  Lemma cardinal_Empty : forall m, Empty m <-> cardinal m = 0.
+  Lemma cardinal_Empty : forall m : t elt, 
+   Empty m <-> cardinal m = 0.
   Proof.
   intros.
-  rewrite elements_Empty.
-  unfold cardinal.
+  rewrite cardinal_1, elements_Empty.
   destruct (elements m); intuition; discriminate.
   Qed.
  
@@ -703,7 +707,7 @@ Module WProperties (E:DecidableType)(M:WSfun E).
   red; auto.
   Qed.
 
-  Lemma cardinal_1 : forall m, Empty m -> cardinal m = 0.
+  Lemma cardinal_1 : forall m : t elt, Empty m -> cardinal m = 0.
   Proof.
   intros; rewrite <- cardinal_Empty; auto.
   Qed.
@@ -719,7 +723,8 @@ Module WProperties (E:DecidableType)(M:WSfun E).
   red; simpl; auto.
   Qed.
 
-  Lemma cardinal_inv_1 : forall m, cardinal m = 0 -> Empty m. 
+  Lemma cardinal_inv_1 : forall m : t elt, 
+   cardinal m = 0 -> Empty m.
   Proof.
   intros; rewrite cardinal_Empty; auto. 
   Qed.
@@ -728,7 +733,7 @@ Module WProperties (E:DecidableType)(M:WSfun E).
   Lemma cardinal_inv_2 :
    forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }.
   Proof. 
-  unfold cardinal; intros.
+  intros; rewrite M.cardinal_1 in *.
   generalize (elements_mapsto_iff m).
   destruct (elements m); try discriminate. 
   exists p; auto.
diff --git a/theories/FSets/FMapIntMap.v b/theories/FSets/FMapIntMap.v
index 761c8d8e6..9673d667d 100644
--- a/theories/FSets/FMapIntMap.v
+++ b/theories/FSets/FMapIntMap.v
@@ -98,6 +98,8 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType.
 
   Definition elements (m : t A) : list (N*A) := alist_of_Map _ m.
 
+  Definition cardinal (m : t A) : nat := MapCard _ m.
+
   Definition MapsTo (x:key)(v:A)(m:t A) := find x m = Some v.
 
   Definition In (x:key)(m:t A) := exists e:A, MapsTo x e m.
@@ -319,6 +321,9 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType.
   inversion H; auto.
   Qed.
 
+  Lemma cardinal_1 : forall m, cardinal m = length (elements m).
+  Proof. exact (@MapCard_as_length _). Qed.
+
   Definition Equal cmp m m' := 
          (forall k, In k m <-> In k m') /\ 
          (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).  
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index a6f90acb7..01362936c 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -43,7 +43,7 @@ Unset Strict Implicit.
     
     - no [iter] function, useless since Coq is purely functional
     - [option] types are used instead of [Not_found] exceptions
-    - more functions are provided: [elements] and [map2]
+    - more functions are provided: [elements] and [cardinal] and [map2]
 
 *)
 
@@ -116,6 +116,9 @@ Module Type WSfun (E : EqualityType).
     (** [elements m] returns an assoc list corresponding to the bindings 
         of [m], in any order. *)
 
+    Parameter cardinal : t elt -> nat. 
+    (** [cardinal m] returns the number of bindings in [m]. *)
+
     Parameter fold : forall A: Type, (key -> elt -> A -> A) -> t elt -> A -> A.
     (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)], 
 	where [k1] ... [kN] are the keys of all bindings in [m] 
@@ -181,6 +184,9 @@ Module Type WSfun (E : EqualityType).
          property that is really weaker: *)
       Parameter elements_3w : NoDupA eq_key (elements m).  
 
+    (** Specification of [cardinal] *)
+      Parameter cardinal_1 : cardinal m = length (elements m).
+
     (** Specification of [fold] *)  
       Parameter fold_1 :
 	forall (A : Type) (i : A) (f : key -> elt -> A -> A),
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index dfe842730..63144afe7 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -1063,6 +1063,7 @@ Section Elt.
  Definition map2 f m (m':t elt') : t elt'' := 
    Build_slist (Raw.map2_sorted f m.(sorted) m'.(sorted)).
  Definition elements m : list (key*elt) := @Raw.elements elt m.(this).
+ Definition cardinal m := length m.(this).
  Definition fold (A:Type)(f:key->elt->A->A) m (i:A) : A := @Raw.fold elt A f m.(this) i.
  Definition equal cmp m m' : bool := @Raw.equal elt cmp m.(this) m'.(this).
 
@@ -1119,6 +1120,9 @@ Section Elt.
  Lemma elements_3w : forall m, NoDupA eq_key (elements m).  
  Proof. intros m; exact (@Raw.elements_3w elt m.(this) m.(sorted)). Qed.
 
+ Lemma cardinal_1 : forall m, cardinal m = length (elements m).
+ Proof. intros; reflexivity. Qed.
+
  Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
  Proof. intros m; exact (@Raw.fold_1 elt m.(this)). Qed.
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.
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 0dcfb05f3..a40e3acf0 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -896,6 +896,7 @@ Section Elt.
  Definition map2 f m (m':t elt') : t elt'' := 
    Build_slist (Raw.map2_NoDup f m.(NoDup) m'.(NoDup)).
  Definition elements m : list (key*elt) := @Raw.elements elt m.(this).
+ Definition cardinal m := length m.(this).
  Definition fold (A:Type)(f:key->elt->A->A) m (i:A) : A := @Raw.fold elt A f m.(this) i.
  Definition equal cmp m m' : bool := @Raw.equal elt cmp m.(this) m'.(this).
 
@@ -948,6 +949,9 @@ Section Elt.
  Proof. intros m; exact (@Raw.elements_2 elt m.(this)). Qed.
  Lemma elements_3w : forall m, NoDupA eq_key (elements m).  
  Proof. intros m; exact (@Raw.elements_3w elt m.(this) m.(NoDup)). Qed.
+ 
+ Lemma cardinal_1 : forall m, cardinal m = length (elements m). 
+ Proof. intros; reflexivity. Qed.
 
  Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index f9bce013c..93adf6790 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -301,6 +301,11 @@ Module WProperties (Import E : DecidableType)(M : WSfun E).
   rewrite H in H0; destruct H0 as (_,H0); inversion H0.
   Qed.
 
+  Lemma elements_empty : elements empty = nil.
+  Proof.
+  rewrite <-elements_Empty; auto with set.
+  Qed.
+
   (** * Alternative (weaker) specifications for [fold] *)
 
   Section Old_Spec_Now_Properties.