Réparation de FSet (back to 8628)

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

1 files changed, 151 insertions, 151 deletions

diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index 2adc17ff4..2abc20799 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(* $Id: FSetEqProperties.v,v 1.10 2006/03/14 23:52:28 letouzey Exp $ *)
 
 (** * Finite sets library *)
 
@@ -23,118 +23,118 @@ Require Import Zerob.
 Require Import Sumbool.
 Require Import Omega.
 
-Module EqProperties (MS).
+Module EqProperties (M:S).
 Import M.
 Import Logic. (* to unmask [eq] *)  
 Import Peano. (* to unmask [lt] *)
   
-Module ME = OrderedTypeFacts E.  
-Module MP = Properties M.
+Module ME := OrderedTypeFacts E.  
+Module MP := Properties M.
 Import MP.
 Import MP.FM.
 
-Definition Add = MP.Add.
+Definition Add := MP.Add.
 
 Section BasicProperties. 
 
 (** Some old specifications written with boolean equalities. *) 
 
-Variable s s' s'' t.
-Variable x y z  elt.
+Variable s s' s'': t.
+Variable x y z : elt.
 
-Lemma mem_eq 
+Lemma mem_eq: 
   E.eq x y -> mem x s=mem y s.
 Proof. 
 intro H; rewrite H; auto.
 Qed.
 
-Lemma equal_mem_1 
+Lemma equal_mem_1: 
   (forall a, mem a s=mem a s') -> equal s s'=true.
 Proof. 
 intros; apply equal_1; unfold Equal; intros.
 do 2 rewrite mem_iff; rewrite H; tauto.
 Qed.
 
-Lemma equal_mem_2 
+Lemma equal_mem_2: 
   equal s s'=true -> forall a, mem a s=mem a s'.
 Proof. 
 intros; rewrite (equal_2 H); auto.
 Qed.
 
-Lemma subset_mem_1 
+Lemma subset_mem_1: 
   (forall a, mem a s=true->mem a s'=true) -> subset s s'=true.
 Proof. 
 intros; apply subset_1; unfold Subset; intros a.
 do 2 rewrite mem_iff; auto.
 Qed.
 
-Lemma subset_mem_2 
+Lemma subset_mem_2: 
   subset s s'=true -> forall a, mem a s=true -> mem a s'=true.
 Proof. 
 intros H a; do 2 rewrite <- mem_iff; apply subset_2; auto.
 Qed.
   
-Lemma empty_mem mem x empty=false.
+Lemma empty_mem: mem x empty=false.
 Proof. 
 rewrite <- not_mem_iff; auto.
 Qed.
 
-Lemma is_empty_equal_empty is_empty s = equal s empty.
+Lemma is_empty_equal_empty: is_empty s = equal s empty.
 Proof. 
 apply bool_1; split; intros.
-rewrite <- (empty_is_empty_1 (s=empty)); auto with set.
+rewrite <- (empty_is_empty_1 (s:=empty)); auto with set.
 rewrite <- is_empty_iff; auto with set.
 Qed.
   
-Lemma choose_mem_1 choose s=Some x -> mem x s=true.
+Lemma choose_mem_1: choose s=Some x -> mem x s=true.
 Proof.  
 auto.
 Qed.
 
-Lemma choose_mem_2 choose s=None -> is_empty s=true.
+Lemma choose_mem_2: choose s=None -> is_empty s=true.
 Proof.
 auto.
 Qed.
 
-Lemma add_mem_1 mem x (add x s)=true.
+Lemma add_mem_1: mem x (add x s)=true.
 Proof.
 auto.
 Qed.  
  
-Lemma add_mem_2 ~E.eq x y -> mem y (add x s)=mem y s.
+Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s.
 Proof. 
 apply add_neq_b.
 Qed.
 
-Lemma remove_mem_1 mem x (remove x s)=false.
+Lemma remove_mem_1: mem x (remove x s)=false.
 Proof. 
 rewrite <- not_mem_iff; auto.
 Qed. 
  
-Lemma remove_mem_2 ~E.eq x y -> mem y (remove x s)=mem y s.
+Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s.
 Proof. 
 apply remove_neq_b.
 Qed.
 
-Lemma singleton_equal_add 
+Lemma singleton_equal_add: 
   equal (singleton x) (add x empty)=true.
 Proof.
 rewrite (singleton_equal_add x); auto with set.
 Qed.  
 
-Lemma union_mem 
+Lemma union_mem: 
   mem x (union s s')=mem x s || mem x s'.
 Proof. 
 apply union_b.
 Qed.
 
-Lemma inter_mem 
+Lemma inter_mem: 
   mem x (inter s s')=mem x s && mem x s'.
 Proof. 
 apply inter_b.
 Qed.
 
-Lemma diff_mem 
+Lemma diff_mem: 
   mem x (diff s s')=mem x s && negb (mem x s').
 Proof. 
 apply diff_b.
@@ -142,41 +142,41 @@ Qed.
 
 (** properties of [mem] *)
 
-Lemma mem_3  ~In x s -> mem x s=false.
+Lemma mem_3 : ~In x s -> mem x s=false.
 Proof.
 intros; rewrite <- not_mem_iff; auto.
 Qed.
 
-Lemma mem_4  mem x s=false -> ~In x s.
+Lemma mem_4 : mem x s=false -> ~In x s.
 Proof.
 intros; rewrite not_mem_iff; auto.
 Qed.
 
 (** Properties of [equal] *) 
 
-Lemma equal_refl equal s s=true.
+Lemma equal_refl: equal s s=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma equal_sym equal s s'=equal s' s.
+Lemma equal_sym: equal s s'=equal s' s.
 Proof.
 intros; apply bool_1; do 2 rewrite <- equal_iff; intuition.
 Qed.
 
-Lemma equal_trans 
+Lemma equal_trans: 
  equal s s'=true -> equal s' s''=true -> equal s s''=true.
 Proof.
 intros; rewrite (equal_2 H); auto.
 Qed.
 
-Lemma equal_equal 
+Lemma equal_equal: 
  equal s s'=true -> equal s s''=equal s' s''.
 Proof.
 intros; rewrite (equal_2 H); auto.
 Qed.
 
-Lemma equal_cardinal 
+Lemma equal_cardinal: 
  equal s s'=true -> cardinal s=cardinal s'.
 Proof.
 auto with set.
@@ -184,25 +184,25 @@ Qed.
 
 (* Properties of [subset] *)
 
-Lemma subset_refl subset s s=true. 
+Lemma subset_refl: subset s s=true. 
 Proof.
 auto with set.
 Qed.
 
-Lemma subset_antisym 
+Lemma subset_antisym: 
  subset s s'=true -> subset s' s=true -> equal s s'=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma subset_trans 
+Lemma subset_trans: 
  subset s s'=true -> subset s' s''=true -> subset s s''=true.
 Proof.
 do 3 rewrite <- subset_iff; intros.
 apply subset_trans with s'; auto.
 Qed.
 
-Lemma subset_equal 
+Lemma subset_equal: 
  equal s s'=true -> subset s s'=true.
 Proof.
 auto with set.
@@ -210,8 +210,8 @@ Qed.
 
 (** Properties of [choose] *)
 
-Lemma choose_mem_3 
- is_empty s=false -> {xelt|choose s=Some x /\ mem x s=true}.
+Lemma choose_mem_3: 
+ is_empty s=false -> {x:elt|choose s=Some x /\ mem x s=true}.
 Proof.
 intros.
 generalize (@choose_1 s) (@choose_2 s).
@@ -221,7 +221,7 @@ generalize (H1 (refl_equal None)); clear H1.
 intros; rewrite (is_empty_1 H1) in H; discriminate.
 Qed.
 
-Lemma choose_mem_4 choose empty=None.
+Lemma choose_mem_4: choose empty=None.
 Proof.
 generalize (@choose_1 empty).
 case (@choose empty);intros;auto.
@@ -230,13 +230,13 @@ Qed.
 
 (** Properties of [add] *)
 
-Lemma add_mem_3 
+Lemma add_mem_3: 
  mem y s=true -> mem y (add x s)=true.
 Proof.
 auto.
 Qed.
 
-Lemma add_equal 
+Lemma add_equal: 
  mem x s=true -> equal (add x s) s=true.
 Proof.
 auto with set.
@@ -244,26 +244,26 @@ Qed.
 
 (** Properties of [remove] *)
 
-Lemma remove_mem_3 
+Lemma remove_mem_3: 
  mem y (remove x s)=true -> mem y s=true.
 Proof.
 rewrite remove_b; intros H;destruct (andb_prop _ _ H); auto.
 Qed.
 
-Lemma remove_equal 
+Lemma remove_equal: 
  mem x s=false -> equal (remove x s) s=true.
 Proof.
 intros; apply equal_1; apply remove_equal.
 rewrite not_mem_iff; auto.
 Qed.
 
-Lemma add_remove 
+Lemma add_remove: 
  mem x s=true -> equal (add x (remove x s)) s=true.
 Proof.
 intros; apply equal_1; apply add_remove; auto.
 Qed.
 
-Lemma remove_add 
+Lemma remove_add: 
  mem x s=false -> equal (remove x (add x s)) s=true.
 Proof.
 intros; apply equal_1; apply remove_add; auto.
@@ -272,7 +272,7 @@ Qed.
 
 (** Properties of [is_empty] *)
 
-Lemma is_empty_cardinal is_empty s = zerob (cardinal s).
+Lemma is_empty_cardinal: is_empty s = zerob (cardinal s).
 Proof.
 intros; apply bool_1; split; intros.
 rewrite cardinal_1; simpl; auto.
@@ -282,61 +282,61 @@ Qed.
 
 (** Properties of [singleton] *)
 
-Lemma singleton_mem_1 mem x (singleton x)=true.
+Lemma singleton_mem_1: mem x (singleton x)=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma singleton_mem_2 ~E.eq x y -> mem y (singleton x)=false.
+Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false.
 Proof.
 intros; rewrite singleton_b.
 unfold ME.eqb; destruct (ME.eq_dec x y); intuition.
 Qed.
 
-Lemma singleton_mem_3 mem y (singleton x)=true -> E.eq x y.
+Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y.
 Proof.
 auto.
 Qed.
 
 (** Properties of [union] *)
 
-Lemma union_sym
+Lemma union_sym:
  equal (union s s') (union s' s)=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma union_subset_equal 
+Lemma union_subset_equal: 
  subset s s'=true -> equal (union s s') s'=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma union_equal_1 
+Lemma union_equal_1: 
  equal s s'=true-> equal (union s s'') (union s' s'')=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma union_equal_2 
+Lemma union_equal_2: 
  equal s' s''=true-> equal (union s s') (union s s'')=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma union_assoc 
+Lemma union_assoc: 
  equal (union (union s s') s'') (union s (union s' s''))=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma add_union_singleton 
+Lemma add_union_singleton: 
  equal (add x s) (union (singleton x) s)=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma union_add 
+Lemma union_add: 
  equal (union (add x s) s') (add x (union s s'))=true.
 Proof.
 auto with set.
@@ -344,17 +344,17 @@ Qed.
 
 (* caracterisation of [union] via [subset] *)
 
-Lemma union_subset_1 subset s (union s s')=true.
+Lemma union_subset_1: subset s (union s s')=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma union_subset_2 subset s' (union s s')=true.
+Lemma union_subset_2: subset s' (union s s')=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma union_subset_3
+Lemma union_subset_3:
  subset s s''=true -> subset s' s''=true -> 
   subset (union s s') s''=true.
 Proof.
@@ -363,54 +363,54 @@ Qed.
 
 (** Properties of [inter] *) 
 
-Lemma inter_sym equal (inter s s') (inter s' s)=true.
+Lemma inter_sym: equal (inter s s') (inter s' s)=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma inter_subset_equal 
+Lemma inter_subset_equal: 
  subset s s'=true -> equal (inter s s') s=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma inter_equal_1 
+Lemma inter_equal_1: 
  equal s s'=true -> equal (inter s s'') (inter s' s'')=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma inter_equal_2 
+Lemma inter_equal_2: 
  equal s' s''=true -> equal (inter s s') (inter s s'')=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma inter_assoc 
+Lemma inter_assoc: 
  equal (inter (inter s s') s'') (inter s (inter s' s''))=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma union_inter_1 
+Lemma union_inter_1: 
  equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma union_inter_2 
+Lemma union_inter_2: 
  equal (union (inter s s') s'') (inter (union s s'') (union s' s''))=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma inter_add_1 mem x s'=true -> 
+Lemma inter_add_1: mem x s'=true -> 
  equal (inter (add x s) s') (add x (inter s s'))=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma inter_add_2 mem x s'=false -> 
+Lemma inter_add_2: mem x s'=false -> 
  equal (inter (add x s) s') (inter s s')=true.
 Proof.
 intros; apply equal_1; apply inter_add_2.
@@ -419,17 +419,17 @@ Qed.
 
 (* caracterisation of [union] via [subset] *)
 
-Lemma inter_subset_1 subset (inter s s') s=true.
+Lemma inter_subset_1: subset (inter s s') s=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma inter_subset_2 subset (inter s s') s'=true.
+Lemma inter_subset_2: subset (inter s s') s'=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma inter_subset_3
+Lemma inter_subset_3:
  subset s'' s=true -> subset s'' s'=true -> 
   subset s'' (inter s s')=true.
 Proof.
@@ -438,30 +438,30 @@ Qed.
 
 (** Properties of [diff] *)
 
-Lemma diff_subset subset (diff s s') s=true.
+Lemma diff_subset: subset (diff s s') s=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma diff_subset_equal
+Lemma diff_subset_equal:
  subset s s'=true -> equal (diff s s') empty=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma remove_inter_singleton 
+Lemma remove_inter_singleton: 
  equal (remove x s) (diff s (singleton x))=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma diff_inter_empty
+Lemma diff_inter_empty:
  equal (inter (diff s s') (inter s s')) empty=true. 
 Proof.
 auto with set.
 Qed.
 
-Lemma diff_inter_all 
+Lemma diff_inter_all: 
  equal (union (diff s s') (inter s s')) s=true.
 Proof.
 auto with set.
@@ -471,16 +471,16 @@ End BasicProperties.
 
 Hint Immediate empty_mem is_empty_equal_empty add_mem_1
    remove_mem_1 singleton_equal_add union_mem inter_mem
-   diff_mem equal_sym add_remove remove_add  set. 
+   diff_mem equal_sym add_remove remove_add : set. 
 Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
    choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal
    subset_refl subset_equal subset_antisym
-   add_mem_3 add_equal remove_mem_3 remove_equal  set.
+   add_mem_3 add_equal remove_mem_3 remove_equal : set.
 
 
 (** General recursion principes based on [cardinal] *)
 
-Lemma cardinal_set_rec  forall (P:t->Type),
+Lemma cardinal_set_rec:  forall (P:t->Type),
  (forall s s', equal s s'=true -> P s -> P s') -> 
  (forall s x, mem x s=false -> P s -> P (add x s)) -> 
  P empty -> forall n s, cardinal s=n -> P s.
@@ -493,7 +493,7 @@ apply equal_1; intro a; rewrite add_iff; rewrite (H1 a); tauto.
 apply X0; auto with set; apply mem_3; auto.
 Qed.
 
-Lemma set_rec  forall (P:t->Type),
+Lemma set_rec:  forall (P:t->Type),
  (forall s s', equal s s'=true -> P s -> P s') ->
  (forall s x, mem x s=false -> P s -> P (add x s)) -> 
  P empty -> forall s, P s.
@@ -503,7 +503,7 @@ Qed.
 
 (** Properties of [fold] *)
 
-Lemma exclusive_set  forall s s' x,
+Lemma exclusive_set : forall s s' x,
  ~In x s\/~In x s' <-> mem x s && mem x s'=false.
 Proof.
 intros; do 2 rewrite not_mem_iff.
@@ -511,53 +511,53 @@ destruct (mem x s); destruct (mem x s'); intuition.
 Qed.
 
 Section Fold. 
-Variables (ASet)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA).
-Variables (felt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
-Variables (iA).
-Variables (s s't)(x:elt).
+Variables (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA).
+Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
+Variables (i:A).
+Variables (s s':t)(x:elt).
  
-Lemma fold_empty eqA (fold f empty i) i.
+Lemma fold_empty: eqA (fold f empty i) i.
 Proof. 
 apply fold_empty; auto.
 Qed.
 
-Lemma fold_equal 
+Lemma fold_equal: 
  equal s s'=true -> eqA (fold f s i) (fold f s' i).
 Proof. 
-intros; apply fold_equal with (eqA=eqA); auto.
+intros; apply fold_equal with (eqA:=eqA); auto.
 Qed.
    
-Lemma fold_add 
+Lemma fold_add: 
  mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)).
 Proof. 
-intros; apply fold_add with (eqA=eqA); auto.
+intros; apply fold_add with (eqA:=eqA); auto.
 rewrite not_mem_iff; auto.
 Qed.
 
-Lemma add_fold 
+Lemma add_fold: 
   mem x s=true -> eqA (fold f (add x s) i) (fold f s i).
 Proof.
-intros; apply add_fold with (eqA=eqA); auto.
+intros; apply add_fold with (eqA:=eqA); auto.
 Qed.
 
-Lemma remove_fold_1 
+Lemma remove_fold_1: 
  mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i).
 Proof.
-intros; apply remove_fold_1 with (eqA=eqA); auto.
+intros; apply remove_fold_1 with (eqA:=eqA); auto.
 Qed.
 
-Lemma remove_fold_2 
+Lemma remove_fold_2: 
  mem x s=false -> eqA (fold f (remove x s) i) (fold f s i).
 Proof.
-intros; apply remove_fold_2 with (eqA=eqA); auto.
+intros; apply remove_fold_2 with (eqA:=eqA); auto.
 rewrite not_mem_iff; auto.
 Qed.
 
-Lemma fold_union 
+Lemma fold_union: 
  (forall x, mem x s && mem x s'=false) -> 
  eqA (fold f (union s s') i) (fold f s (fold f s' i)).
 Proof.
-intros; apply fold_union with (eqA=eqA); auto.
+intros; apply fold_union with (eqA:=eqA); auto.
 intros; rewrite exclusive_set; auto.
 Qed.
 
@@ -565,32 +565,32 @@ End Fold.
 
 (** Properties of [cardinal] *)
 
-Lemma add_cardinal_1 
+Lemma add_cardinal_1: 
  forall s x, mem x s=true -> cardinal (add x s)=cardinal s.
 Proof.
 auto with set.
 Qed.
 
-Lemma add_cardinal_2 
+Lemma add_cardinal_2: 
  forall s x, mem x s=false -> cardinal (add x s)=S (cardinal s).
 Proof.
 intros; apply add_cardinal_2; auto.
 rewrite not_mem_iff; auto.
 Qed.
 
-Lemma remove_cardinal_1 
+Lemma remove_cardinal_1: 
  forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s.
 Proof.
 intros; apply remove_cardinal_1; auto.
 Qed.
 
-Lemma remove_cardinal_2 
+Lemma remove_cardinal_2: 
  forall s x, mem x s=false -> cardinal (remove x s)=cardinal s.
 Proof.
 auto with set.
 Qed.
 
-Lemma union_cardinal 
+Lemma union_cardinal: 
  forall s s', (forall x, mem x s && mem x s'=false) -> 
  cardinal (union s s')=cardinal s+cardinal s'.
 Proof.
@@ -598,7 +598,7 @@ intros; apply union_cardinal; auto; intros.
 rewrite exclusive_set; auto.
 Qed.
 
-Lemma subset_cardinal 
+Lemma subset_cardinal: 
  forall s s', subset s s'=true -> cardinal s<=cardinal s'.
 Proof.
 intros; apply subset_cardinal; auto.
@@ -608,20 +608,20 @@ Section Bool.
 
 (** Properties of [filter] *)
 
-Variable felt->bool.
-Variable Comp compat_bool E.eq f.
+Variable f:elt->bool.
+Variable Comp: compat_bool E.eq f.
 
-Let Comp'  compat_bool E.eq (fun x =>negb (f x)).
+Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
 Proof.
 unfold compat_bool in *; intros; f_equal; auto.
 Qed.
 
-Lemma filter_mem forall s x, mem x (filter f s)=mem x s && f x.
+Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x.
 Proof. 
 intros; apply filter_b; auto.
 Qed.
 
-Lemma for_all_filter 
+Lemma for_all_filter: 
  forall s, for_all f s=is_empty (filter (fun x => negb (f x)) s).
 Proof. 
 intros; apply bool_1; split; intros.
@@ -638,7 +638,7 @@ rewrite filter_iff; auto.
 destruct (f x); auto.
 Qed.
 
-Lemma exists_filter  
+Lemma exists_filter : 
  forall s, exists_ f s=negb (is_empty (filter f s)).
 Proof. 
 intros; apply bool_1; split; intros. 
@@ -653,19 +653,19 @@ intros _ H0.
 rewrite (is_empty_1 (H0 (refl_equal None))) in H; auto; discriminate.
 Qed.
 
-Lemma partition_filter_1 
+Lemma partition_filter_1: 
  forall s, equal (fst (partition f s)) (filter f s)=true.
 Proof. 
 auto.
 Qed.
 
-Lemma partition_filter_2 
+Lemma partition_filter_2: 
  forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true.
 Proof. 
 auto.
 Qed.
 
-Lemma add_filter_1  forall s s' x, 
+Lemma add_filter_1 : forall s s' x, 
  f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')).
 Proof.
 unfold Add, MP.Add; intros.
@@ -676,7 +676,7 @@ assert (E.eq x y -> f y = true) by
 tauto.
 Qed.
 
-Lemma add_filter_2  forall s s' x, 
+Lemma add_filter_2 : forall s s' x, 
  f x=false -> (Add x s s') -> filter f s [=] filter f s'.
 Proof.
 unfold Add, MP.Add, Equal; intros.
@@ -689,7 +689,7 @@ assert (f a = true -> ~E.eq x a).
 tauto. 
 Qed.
 
-Lemma union_filter forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) ->
+Lemma union_filter: forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) ->
   forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s.
 Proof.
 clear Comp' Comp f.
@@ -706,7 +706,7 @@ Qed.
 
 (** Properties of [for_all] *)
 
-Lemma for_all_mem_1 forall s, 
+Lemma for_all_mem_1: forall s, 
  (forall x, (mem x s)=true->(f x)=true) -> (for_all f s)=true.
 Proof.
 intros.
@@ -719,7 +719,7 @@ generalize (H a); case (mem a s);intros;auto.
 rewrite H0;auto.
 Qed.
 
-Lemma for_all_mem_2 forall s, 
+Lemma for_all_mem_2: forall s, 
  (for_all f s)=true -> forall x,(mem x s)=true -> (f x)=true. 
 Proof.
 intros.
@@ -732,7 +732,7 @@ rewrite H0; simpl;intros.
 replace true with (negb false);auto;apply negb_sym;auto.
 Qed.
 
-Lemma for_all_mem_3 
+Lemma for_all_mem_3: 
  forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false.
 Proof.
 intros.
@@ -747,8 +747,8 @@ rewrite H0.
 simpl;auto.
 Qed.
 
-Lemma for_all_mem_4 
- forall s, for_all f s=false -> {xelt | mem x s=true /\ f x=false}.
+Lemma for_all_mem_4: 
+ forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false}.
 Proof.
 intros.
 rewrite for_all_filter in H; auto.
@@ -762,7 +762,7 @@ Qed.
 
 (** Properties of [exists] *)
 
-Lemma for_all_exists 
+Lemma for_all_exists: 
  forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s).
 Proof.
 intros.
@@ -775,15 +775,15 @@ Qed.
 End Bool.
 Section Bool'.
 
-Variable felt->bool.
-Variable Comp compat_bool E.eq f.
+Variable f:elt->bool.
+Variable Comp: compat_bool E.eq f.
 
-Let Comp'  compat_bool E.eq (fun x =>negb (f x)).
+Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
 Proof.
 unfold compat_bool in *; intros; f_equal; auto.
 Qed.
 
-Lemma exists_mem_1 
+Lemma exists_mem_1: 
  forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false.
 Proof.
 intros.
@@ -793,7 +793,7 @@ intros;generalize (H x H0);intros.
 symmetry;apply negb_sym;simpl;auto.
 Qed.
 
-Lemma exists_mem_2 
+Lemma exists_mem_2: 
  forall s, exists_ f s=false -> forall x, mem x s=true -> f x=false. 
 Proof.
 intros.
@@ -803,7 +803,7 @@ rewrite (for_all_mem_2 (fun x => negb (f x)) Comp' s);simpl;auto.
 replace true with (negb false);auto;apply negb_sym;auto.
 Qed.
 
-Lemma exists_mem_3 
+Lemma exists_mem_3: 
  forall s x, mem x s=true -> f x=true -> exists_ f s=true.
 Proof.
 intros.
@@ -813,8 +813,8 @@ apply for_all_mem_3 with x;auto.
 rewrite H0;auto.
 Qed.
 
-Lemma exists_mem_4 
- forall s, exists_ f s=true -> {xelt | (mem x s)=true /\ (f x)=true}.
+Lemma exists_mem_4: 
+ forall s, exists_ f s=true -> {x:elt | (mem x s)=true /\ (f x)=true}.
 Proof.
 intros.
 rewrite for_all_exists in H; auto.
@@ -831,21 +831,21 @@ Section Sum.
 
 (** Adding a valuation function on all elements of a set. *)
 
-Definition sum (felt -> nat)(s:t) := fold (fun x => plus (f x)) s 0. 
+Definition sum (f:elt -> nat)(s:t) := fold (fun x => plus (f x)) s 0. 
 
-Lemma sum_plus  
+Lemma sum_plus : 
   forall f g, compat_nat E.eq f -> compat_nat E.eq g -> 
     forall s, sum (fun x =>f x+g x) s = sum f s + sum g s.
 Proof.
 unfold sum.
 intros f g Hf Hg.
-assert (fc  compat_op E.eq (@eq _) (fun x:elt =>plus (f x))).  auto.
-assert (ft  transpose (@eq _) (fun x:elt =>plus (f x))). red; intros; omega.
-assert (gc  compat_op E.eq (@eq _) (fun x:elt => plus (g x))). auto.
-assert (gt  transpose (@eq _) (fun x:elt =>plus (g x))). red; intros; omega.
-assert (fgc  compat_op E.eq (@eq _) (fun x:elt =>plus ((f x)+(g x)))). auto.
-assert (fgt  transpose (@eq _) (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega.
-assert (st = gen_st nat).
+assert (fc : compat_op E.eq (@eq _) (fun x:elt =>plus (f x))).  auto.
+assert (ft : transpose (@eq _) (fun x:elt =>plus (f x))). red; intros; omega.
+assert (gc : compat_op E.eq (@eq _) (fun x:elt => plus (g x))). auto.
+assert (gt : transpose (@eq _) (fun x:elt =>plus (g x))). red; intros; omega.
+assert (fgc : compat_op E.eq (@eq _) (fun x:elt =>plus ((f x)+(g x)))). auto.
+assert (fgt : transpose (@eq _) (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega.
+assert (st := gen_st nat).
 intros s;pattern s; apply set_rec.
 intros.
 rewrite <- (fold_equal _ _ st _ fc ft 0 _ _ H).
@@ -856,15 +856,15 @@ rewrite H0;simpl;omega.
 intros; do 3 rewrite (fold_empty _ _ st);auto.
 Qed.
 
-Lemma sum_filter  forall f, (compat_bool E.eq f) -> 
+Lemma sum_filter : forall f, (compat_bool E.eq f) -> 
   forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)).
 Proof.
 unfold sum; intros f Hf.
-assert (st = gen_st nat).
-assert (cc  compat_op E.eq (@eq _) (fun x => plus (if f x then 1 else 0))). 
+assert (st := gen_st nat).
+assert (cc : compat_op E.eq (@eq _) (fun x => plus (if f x then 1 else 0))). 
  unfold compat_op; intros.
  rewrite (Hf x x' H); auto.
-assert (ct  transpose (@eq _) (fun x => plus (if f x then 1 else 0))).
+assert (ct : transpose (@eq _) (fun x => plus (if f x then 1 else 0))).
  unfold transpose; intros; omega.
 intros s;pattern s; apply set_rec.
 intros.
@@ -884,32 +884,32 @@ unfold Empty; intros.
 rewrite filter_iff; auto; set_iff; tauto.
 Qed.
 
-Lemma fold_compat  
-  forall (ASet)(eqA:A->A->Prop)(st:(Setoid_Theory _ eqA))
-  (f gelt->A->A),
+Lemma fold_compat : 
+  forall (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory _ eqA))
+  (f g:elt->A->A),
   (compat_op E.eq eqA f) -> (transpose eqA f) -> 
   (compat_op E.eq eqA g) -> (transpose eqA g) -> 
-  forall (iA)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) -> 
+  forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) -> 
   (eqA (fold f s i) (fold g s i)).
 Proof.
 intros A eqA st f g fc ft gc gt i.
 intro s; pattern s; apply set_rec; intros.
 trans_st (fold f s0 i).
-apply fold_equal with (eqA=eqA); auto.
+apply fold_equal with (eqA:=eqA); auto.
 rewrite equal_sym; auto.
 trans_st (fold g s0 i).
 apply H0; intros; apply H1; auto.
 elim  (equal_2 H x); auto; intros.
-apply fold_equal with (eqA=eqA); auto.
+apply fold_equal with (eqA:=eqA); auto.
 trans_st (f x (fold f s0 i)).
-apply fold_add with (eqA=eqA); auto.
+apply fold_add with (eqA:=eqA); auto.
 trans_st (g x (fold f s0 i)).
 trans_st (g x (fold g s0 i)).
-sym_st; apply fold_add with (eqA=eqA); auto.
+sym_st; apply fold_add with (eqA:=eqA); auto.
 trans_st i; [idtac | sym_st ]; apply fold_empty; auto.
 Qed.
 
-Lemma sum_compat  
+Lemma sum_compat : 
   forall f g, compat_nat E.eq f -> compat_nat E.eq g -> 
   forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s.
 intros.