renommage NoRedun vers le plus joli NoDup

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

1 files changed, 42 insertions, 42 deletions

diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index bcd966f9a..4b98474b1 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -115,7 +115,7 @@ Module Raw (X: DecidableType).
 
   (** ** Proofs of set operation specifications. *)
 
-  Notation NoRedun := (noredunA X.eq).
+  Notation NoDup := (NoDupA X.eq).
   Notation In := (InA X.eq).
 
   Definition Equal s s' := forall a : elt, In a s <-> In a s'.
@@ -149,7 +149,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma add_1 :
-   forall (s : t) (Hs : NoRedun s) (x y : elt), X.eq x y -> In y (add x s).
+   forall (s : t) (Hs : NoDup s) (x y : elt), X.eq x y -> In y (add x s).
   Proof.
   induction s. 
   simpl; intuition.
@@ -159,7 +159,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma add_2 :
-   forall (s : t) (Hs : NoRedun s) (x y : elt), In y s -> In y (add x s).
+   forall (s : t) (Hs : NoDup s) (x y : elt), In y s -> In y (add x s).
   Proof.
   induction s. 
   simpl; intuition.
@@ -168,7 +168,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma add_3 :
-   forall (s : t) (Hs : NoRedun s) (x y : elt),
+   forall (s : t) (Hs : NoDup s) (x y : elt),
    ~ X.eq x y -> In y (add x s) -> In y s.
   Proof.
   induction s. 
@@ -180,7 +180,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma add_unique :
-   forall (s : t) (Hs : NoRedun s)(x:elt), NoRedun (add x s).
+   forall (s : t) (Hs : NoDup s)(x:elt), NoDup (add x s).
   Proof.
   induction s.  
   simpl; intuition.
@@ -197,7 +197,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma remove_1 :
-   forall (s : t) (Hs : NoRedun s) (x y : elt), X.eq x y -> ~ In y (remove x s).
+   forall (s : t) (Hs : NoDup s) (x y : elt), X.eq x y -> ~ In y (remove x s).
   Proof.
   simple induction s. 
   simpl; red; intros; inversion H0.
@@ -208,7 +208,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma remove_2 :
-   forall (s : t) (Hs : NoRedun s) (x y : elt),
+   forall (s : t) (Hs : NoDup s) (x y : elt),
    ~ X.eq x y -> In y s -> In y (remove x s).
   Proof.
   simple induction s. 
@@ -219,7 +219,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma remove_3 :
-   forall (s : t) (Hs : NoRedun s) (x y : elt), In y (remove x s) -> In y s.
+   forall (s : t) (Hs : NoDup s) (x y : elt), In y (remove x s) -> In y s.
   Proof.
   simple induction s. 
   simpl; intuition.
@@ -228,7 +228,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma remove_unique :
-   forall (s : t) (Hs : NoRedun s) (x : elt), NoRedun (remove x s).
+   forall (s : t) (Hs : NoDup s) (x : elt), NoDup (remove x s).
   Proof.
   simple induction s.
   simpl; intuition.
@@ -239,7 +239,7 @@ Module Raw (X: DecidableType).
   eapply remove_3; eauto.
   Qed. 
 
-  Lemma singleton_unique : forall x : elt, NoRedun (singleton x).
+  Lemma singleton_unique : forall x : elt, NoDup (singleton x).
   Proof.
   unfold singleton; simpl; constructor; auto; intro H; inversion H.
   Qed.
@@ -255,7 +255,7 @@ Module Raw (X: DecidableType).
   unfold singleton; simpl; intuition.
   Qed. 
   
-  Lemma empty_unique : NoRedun empty.
+  Lemma empty_unique : NoDup empty.
   Proof.
   unfold empty; constructor.
   Qed.
@@ -287,13 +287,13 @@ Module Raw (X: DecidableType).
   unfold elements; auto.
   Qed.
  
-  Lemma elements_3 : forall (s : t) (Hs : NoRedun s), NoRedun (elements s).  
+  Lemma elements_3 : forall (s : t) (Hs : NoDup s), NoDup (elements s).  
   Proof. 
   unfold elements; auto.
   Qed.
 
   Lemma fold_1 :
-   forall (s : t) (Hs : NoRedun s) (A : Set) (i : A) (f : elt -> A -> A),
+   forall (s : t) (Hs : NoDup s) (A : Set) (i : A) (f : elt -> A -> A),
    fold f s i = fold_left (fun a e => f e a) (elements s) i.
   Proof.
   induction s; simpl; auto; intros.
@@ -301,7 +301,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma union_unique :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'), NoRedun (union s s').
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (union s s').
   Proof.
   unfold union; induction s; simpl; auto; intros.
   inversion_clear Hs.
@@ -310,7 +310,7 @@ Module Raw (X: DecidableType).
   Qed.
   
   Lemma union_1 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x (union s s') -> In x s \/ In x s'.
   Proof.
   unfold union; induction s; simpl; auto; intros.
@@ -322,7 +322,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma union_0 : 
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x s \/ In x s' -> In x (union s s').
   Proof.
   unfold union; induction s; simpl; auto; intros.
@@ -338,25 +338,25 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma union_2 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x s -> In x (union s s').
   Proof.
   intros; apply union_0; auto.
   Qed.
 
   Lemma union_3 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x s' -> In x (union s s').
   Proof.
   intros; apply union_0; auto.
   Qed.
 
   Lemma inter_unique :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'), NoRedun (inter s s').
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (inter s s').
   Proof.
   unfold inter; intros s.
   set (acc := nil (A:=elt)).
-  assert (NoRedun acc) by (unfold acc; auto).
+  assert (NoDup acc) by (unfold acc; auto).
   clearbody acc; generalize H; clear H; generalize acc; clear acc. 
   induction s; simpl; auto; intros.
   inversion_clear Hs.
@@ -366,12 +366,12 @@ Module Raw (X: DecidableType).
   Qed.  
   
   Lemma inter_0  :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x (inter s s') -> In x s /\ In x s'.
   Proof.
   unfold inter; intros.
   set (acc := nil (A:=elt)) in *.
-  assert (NoRedun acc) by (unfold acc; auto).
+  assert (NoDup acc) by (unfold acc; auto).
   cut ((In x s /\ In x s') \/ In x acc).
     destruct 1; auto.
     inversion H1.
@@ -393,21 +393,21 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma inter_1  :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x (inter s s') -> In x s.
   Proof.
   intros; cut (In x s /\ In x s'); [ intuition | apply inter_0; auto ].
   Qed.
 
   Lemma inter_2 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x (inter s s') -> In x s'.
   Proof.
   intros; cut (In x s /\ In x s'); [ intuition | apply inter_0; auto ].
   Qed.
 
   Lemma inter_3 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x s -> In x s' -> In x (inter s s').
   Proof.
   intros s s' Hs Hs' x.
@@ -415,7 +415,7 @@ Module Raw (X: DecidableType).
   intuition.
   unfold inter.
   set (acc := nil (A:=elt)) in *.
-  assert (NoRedun acc) by (unfold acc; auto).
+  assert (NoDup acc) by (unfold acc; auto).
   clearbody acc. 
   generalize H Hs' Hs; clear H Hs Hs'.
   generalize acc x s'; clear acc x s'.
@@ -441,7 +441,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma diff_unique :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'), NoRedun (diff s s').
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (diff s s').
   Proof.
   unfold diff; intros s s' Hs; generalize s Hs; clear Hs s.
   induction s'; simpl; auto; intros.
@@ -451,7 +451,7 @@ Module Raw (X: DecidableType).
   Qed.  
   
   Lemma diff_0 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x (diff s s') -> In x s /\ ~ In x s'.
   Proof.
   unfold diff; intros s s' Hs; generalize s Hs; clear Hs s.
@@ -468,21 +468,21 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma diff_1 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x (diff s s') -> In x s.
   Proof.
   intros; cut (In x s /\ ~ In x s'); [ intuition | apply diff_0; auto]. 
   Qed.
 
   Lemma diff_2 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x (diff s s') -> ~ In x s'.
   Proof.
   intros; cut (In x s /\ ~ In x s'); [ intuition | apply diff_0; auto]. 
   Qed.
 
   Lemma diff_3 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x s -> ~ In x s' -> In x (diff s s').
   Proof.
   unfold diff; intros s s' Hs; generalize s Hs; clear Hs s.
@@ -494,7 +494,7 @@ Module Raw (X: DecidableType).
   Qed.  
   
   Lemma subset_1 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'),
    Subset s s' -> subset s s' = true.
   Proof.
   unfold subset, Subset; intros.
@@ -506,7 +506,7 @@ Module Raw (X: DecidableType).
   eapply diff_1; eauto.
   Qed.
 
-  Lemma subset_2 : forall (s s' : t)(Hs : NoRedun s) (Hs' : NoRedun s'), 
+  Lemma subset_2 : forall (s s' : t)(Hs : NoDup s) (Hs' : NoDup s'), 
      subset s s' = true -> Subset s s'.
   Proof.
   unfold subset, Subset; intros.
@@ -519,14 +519,14 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma equal_1 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'),
    Equal s s' -> equal s s' = true.
   Proof.
   unfold Equal, equal; intros.
   apply andb_true_intro; split; apply subset_1; firstorder.
   Qed.
 
-  Lemma equal_2 : forall (s s' : t)(Hs : NoRedun s) (Hs' : NoRedun s'),  
+  Lemma equal_2 : forall (s s' : t)(Hs : NoDup s) (Hs' : NoDup s'),  
      equal s s' = true -> Equal s s'.
   Proof.
   unfold Equal, equal; intros.
@@ -548,7 +548,7 @@ Module Raw (X: DecidableType).
   Qed.  
 
   Lemma cardinal_1 :
-   forall (s : t) (Hs : NoRedun s), cardinal s = length (elements s).
+   forall (s : t) (Hs : NoDup s), cardinal s = length (elements s).
   Proof.
   auto.
   Qed.
@@ -593,7 +593,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma filter_unique :
-   forall (s : t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (filter f s).
+   forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (filter f s).
   Proof.
   simple induction s; simpl.
   auto.
@@ -690,7 +690,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma partition_aux_1 : 
-   forall (s : t) (Hs : NoRedun s) (f : elt -> bool)(x:elt), 
+   forall (s : t) (Hs : NoDup s) (f : elt -> bool)(x:elt), 
     In x (fst (partition f s)) -> In x s.
   Proof.
   induction s; simpl; auto; intros.
@@ -701,7 +701,7 @@ Module Raw (X: DecidableType).
   Qed. 
      
   Lemma partition_aux_2 : 
-   forall (s : t) (Hs : NoRedun s) (f : elt -> bool)(x:elt), 
+   forall (s : t) (Hs : NoDup s) (f : elt -> bool)(x:elt), 
     In x (snd (partition f s)) -> In x s.
   Proof.
   induction s; simpl; auto; intros.
@@ -712,7 +712,7 @@ Module Raw (X: DecidableType).
   Qed. 
   
   Lemma partition_unique_1 :
-   forall (s : t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (fst (partition f s)).
+   forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (fst (partition f s)).
   Proof.
   simple induction s; simpl.
   auto.
@@ -723,7 +723,7 @@ Module Raw (X: DecidableType).
   Qed.
   
   Lemma partition_unique_2 :
-   forall (s : t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (snd (partition f s)).
+   forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (snd (partition f s)).
   Proof.
   simple induction s; simpl.
   auto.
@@ -762,7 +762,7 @@ Module Make (X: DecidableType) <: S with Module E := X.
  Module E := X.
  Module Raw := Raw X. 
 
- Record slist : Set :=  {this :> Raw.t; unique : noredunA X.eq this}.
+ Record slist : Set :=  {this :> Raw.t; unique : NoDupA X.eq this}.
  Definition t := slist. 
  Definition elt := X.t.