Ajout de theories/FSets contenant la partie "light" de FSets et FMap:

pas d'implementations par AVL, mais celles par lists, ainsi que les 
foncteurs de proprietes. 

Au passage, ajout de MoreList (complements de List) et SetoidList 
(quelques relations sur des listes considerees modulo un eq ou lt 
non standard.



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

1 files changed, 416 insertions, 0 deletions

diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
new file mode 100644
index 000000000..ff3d7e578
--- /dev/null
+++ b/theories/FSets/FSetInterface.v
@@ -0,0 +1,416 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id: FSetInterface.v,v 1.11 2006/03/10 10:49:48 letouzey Exp $ *)
+
+(** * Finite set library *)
+
+(** Set interfaces *)
+
+Require Export Bool.
+Require Export OrderedType.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** Compatibility of a  boolean function with respect to an equality. *)
+Definition compat_bool (A:Set)(eqA: A->A->Prop)(f: A-> bool) :=
+  forall x y : A, eqA x y -> f x = f y.
+
+(** Compatibility of a predicate with respect to an equality. *)
+Definition compat_P (A:Set)(eqA: A->A->Prop)(P : A -> Prop) :=
+  forall x y : A, eqA x y -> P x -> P y.
+
+Hint Unfold compat_bool compat_P.
+
+(** * Non-dependent signature
+
+    Signature [S] presents sets as purely informative programs 
+    together with axioms *)
+
+Module Type S.
+
+  Declare Module E : OrderedType.
+  Definition elt := E.t.
+
+  Parameter t : Set. (** the abstract type of sets *)
+
+  (** Logical predicates *)
+  Parameter In : elt -> t -> Prop.
+  Definition Equal s s' := forall a : elt, In a s <-> In a s'.
+  Definition Subset s s' := forall a : elt, In a s -> In a s'.
+  Definition Empty s := forall a : elt, ~ In a s.
+  Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
+  Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
+  
+  Notation "s [=] t" := (Equal s t) (at level 70, no associativity).
+  Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).
+
+  Parameter empty : t.
+  (** The empty set. *)
+
+  Parameter is_empty : t -> bool.
+  (** Test whether a set is empty or not. *)
+
+  Parameter mem : elt -> t -> bool.
+  (** [mem x s] tests whether [x] belongs to the set [s]. *)
+
+  Parameter add : elt -> t -> t.
+  (** [add x s] returns a set containing all elements of [s],
+  plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
+
+  Parameter singleton : elt -> t.
+  (** [singleton x] returns the one-element set containing only [x]. *)
+
+  Parameter remove : elt -> t -> t.
+  (** [remove x s] returns a set containing all elements of [s],
+  except [x]. If [x] was not in [s], [s] is returned unchanged. *)
+
+  Parameter union : t -> t -> t.
+  (** Set union. *)
+
+  Parameter inter : t -> t -> t.
+  (** Set intersection. *)
+
+  Parameter diff : t -> t -> t.
+  (** Set difference. *)
+
+  Definition eq : t -> t -> Prop := Equal.
+  Parameter lt : t -> t -> Prop.
+  Parameter compare : forall s s' : t, Compare lt eq s s'.
+  (** Total ordering between sets. Can be used as the ordering function
+  for doing sets of sets. *)
+
+  Parameter equal : t -> t -> bool.
+  (** [equal s1 s2] tests whether the sets [s1] and [s2] are
+  equal, that is, contain equal elements. *)
+
+  Parameter subset : t -> t -> bool.
+  (** [subset s1 s2] tests whether the set [s1] is a subset of
+  the set [s2]. *)
+
+  (** Coq comment: [iter] is useless in a purely functional world *)
+  (**  iter: (elt -> unit) -> set -> unit. i*)
+  (** [iter f s] applies [f] in turn to all elements of [s].
+  The order in which the elements of [s] are presented to [f]
+  is unspecified. *)
+
+  Parameter fold : forall A : Set, (elt -> A -> A) -> t -> A -> A.
+  (** [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)],
+  where [x1 ... xN] are the elements of [s], in increasing order. *)
+
+  Parameter for_all : (elt -> bool) -> t -> bool.
+  (** [for_all p s] checks if all elements of the set
+  satisfy the predicate [p]. *)
+
+  Parameter exists_ : (elt -> bool) -> t -> bool.
+  (** [exists p s] checks if at least one element of
+  the set satisfies the predicate [p]. *)
+
+  Parameter filter : (elt -> bool) -> t -> t.
+  (** [filter p s] returns the set of all elements in [s]
+  that satisfy predicate [p]. *)
+
+  Parameter partition : (elt -> bool) -> t -> t * t.
+  (** [partition p s] returns a pair of sets [(s1, s2)], where
+  [s1] is the set of all the elements of [s] that satisfy the
+  predicate [p], and [s2] is the set of all the elements of
+  [s] that do not satisfy [p]. *)
+
+  Parameter cardinal : t -> nat.
+  (** Return the number of elements of a set. *)
+  (** Coq comment: nat instead of int ... *)
+
+  Parameter elements : t -> list elt.
+  (** Return the list of all elements of the given set.
+  The returned list is sorted in increasing order with respect
+  to the ordering [Ord.compare], where [Ord] is the argument
+  given to {!Set.Make}. *)
+
+  Parameter min_elt : t -> option elt.
+  (** Return the smallest element of the given set
+  (with respect to the [Ord.compare] ordering), or raise
+  [Not_found] if the set is empty. *)
+  (** Coq comment: [Not_found] is represented by the option type *)
+
+  Parameter max_elt : t -> option elt.
+  (** Same as {!Set.S.min_elt}, but returns the largest element of the
+  given set. *)
+  (** Coq comment: [Not_found] is represented by the option type *)
+
+  Parameter choose : t -> option elt.
+  (** Return one element of the given set, or raise [Not_found] if
+  the set is empty. Which element is chosen is unspecified,
+  but equal elements will be chosen for equal sets. *)
+  (** Coq comment: [Not_found] is represented by the option type *)
+
+  Section Spec. 
+
+  Variable s s' s'' : t.
+  Variable x y z : elt.
+
+  (** Specification of [In] *)
+  Parameter In_1 : E.eq x y -> In x s -> In y s.
+ 
+  (** Specification of [eq] *)
+  Parameter eq_refl : eq s s. 
+  Parameter eq_sym : eq s s' -> eq s' s.
+  Parameter eq_trans : eq s s' -> eq s' s'' -> eq s s''.
+ 
+  (** Specification of [lt] *)
+  Parameter lt_trans : lt s s' -> lt s' s'' -> lt s s''.
+  Parameter lt_not_eq : lt s s' -> ~ eq s s'.
+
+  (** Specification of [mem] *)
+  Parameter mem_1 : In x s -> mem x s = true.
+  Parameter mem_2 : mem x s = true -> In x s. 
+ 
+  (** Specification of [equal] *) 
+  Parameter equal_1 : s[=]s' -> equal s s' = true.
+  Parameter equal_2 : equal s s' = true ->s[=]s'.
+
+  (** Specification of [subset] *)
+  Parameter subset_1 : s[<=]s' -> subset s s' = true.
+  Parameter subset_2 : subset s s' = true -> s[<=]s'.
+
+  (** Specification of [empty] *)
+  Parameter empty_1 : Empty empty.
+
+  (** Specification of [is_empty] *)
+  Parameter is_empty_1 : Empty s -> is_empty s = true. 
+  Parameter is_empty_2 : is_empty s = true -> Empty s.
+ 
+  (** Specification of [add] *)
+  Parameter add_1 : E.eq x y -> In y (add x s).
+  Parameter add_2 : In y s -> In y (add x s).
+  Parameter add_3 : ~ E.eq x y -> In y (add x s) -> In y s. 
+
+  (** Specification of [remove] *)
+  Parameter remove_1 : E.eq x y -> ~ In y (remove x s).
+  Parameter remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
+  Parameter remove_3 : In y (remove x s) -> In y s.
+
+  (** Specification of [singleton] *)
+  Parameter singleton_1 : In y (singleton x) -> E.eq x y. 
+  Parameter singleton_2 : E.eq x y -> In y (singleton x). 
+
+  (** Specification of [union] *)
+  Parameter union_1 : In x (union s s') -> In x s \/ In x s'.
+  Parameter union_2 : In x s -> In x (union s s'). 
+  Parameter union_3 : In x s' -> In x (union s s').
+
+  (** Specification of [inter] *)
+  Parameter inter_1 : In x (inter s s') -> In x s.
+  Parameter inter_2 : In x (inter s s') -> In x s'.
+  Parameter inter_3 : In x s -> In x s' -> In x (inter s s').
+
+  (** Specification of [diff] *)
+  Parameter diff_1 : In x (diff s s') -> In x s. 
+  Parameter diff_2 : In x (diff s s') -> ~ In x s'.
+  Parameter diff_3 : In x s -> ~ In x s' -> In x (diff s s').
+ 
+  (** Specification of [fold] *)  
+  Parameter fold_1 : forall (A : Set) (i : A) (f : elt -> A -> A),
+      fold f s i = fold_left (fun a e => f e a) (elements s) i.
+
+  (** Specification of [cardinal] *)  
+  Parameter cardinal_1 : cardinal s = length (elements s).
+
+  Section Filter.
+  
+  Variable f : elt -> bool.
+
+  (** Specification of [filter] *)
+  Parameter filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s. 
+  Parameter filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true. 
+  Parameter filter_3 :
+      compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
+
+  (** Specification of [for_all] *)
+  Parameter for_all_1 :
+      compat_bool E.eq f ->
+      For_all (fun x => f x = true) s -> for_all f s = true.
+  Parameter for_all_2 :
+      compat_bool E.eq f ->
+      for_all f s = true -> For_all (fun x => f x = true) s.
+
+  (** Specification of [exists] *)
+  Parameter exists_1 :
+      compat_bool E.eq f ->
+      Exists (fun x => f x = true) s -> exists_ f s = true.
+  Parameter exists_2 :
+      compat_bool E.eq f ->
+      exists_ f s = true -> Exists (fun x => f x = true) s.
+
+  (** Specification of [partition] *)
+  Parameter partition_1 : compat_bool E.eq f -> 
+      fst (partition f s) [=] filter f s.
+  Parameter partition_2 : compat_bool E.eq f -> 
+      snd (partition f s) [=] filter (fun x => negb (f x)) s.
+
+  (** Specification of [elements] *)
+  Parameter elements_1 : In x s -> InA E.eq x (elements s).
+  Parameter elements_2 : InA E.eq x (elements s) -> In x s.
+  Parameter elements_3 : sort E.lt (elements s).  
+
+  (** Specification of [min_elt] *)
+  Parameter min_elt_1 : min_elt s = Some x -> In x s. 
+  Parameter min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x. 
+  Parameter min_elt_3 : min_elt s = None -> Empty s.
+
+  (** Specification of [max_elt] *)  
+  Parameter max_elt_1 : max_elt s = Some x -> In x s. 
+  Parameter max_elt_2 : max_elt s = Some x -> In y s -> ~ E.lt x y. 
+  Parameter max_elt_3 : max_elt s = None -> Empty s.
+
+  (** Specification of [choose] *)
+  Parameter choose_1 : choose s = Some x -> In x s.
+  Parameter choose_2 : choose s = None -> Empty s.
+(*  Parameter choose_equal: 
+      (equal s s')=true -> E.eq (choose s) (choose s'). *)
+
+  End Filter.
+  End Spec.
+
+  Hint Immediate In_1.
+  
+  Hint Resolve mem_1 mem_2 equal_1 equal_2 subset_1 subset_2 empty_1
+    is_empty_1 is_empty_2 choose_1 choose_2 add_1 add_2 add_3 remove_1
+    remove_2 remove_3 singleton_1 singleton_2 union_1 union_2 union_3 inter_1
+    inter_2 inter_3 diff_1 diff_2 diff_3 filter_1 filter_2 filter_3 for_all_1
+    for_all_2 exists_1 exists_2 partition_1 partition_2 elements_1 elements_2
+    elements_3 min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3.
+
+End S.
+
+(** * Dependent signature 
+
+    Signature [Sdep] presents sets using dependent types *)
+
+Module Type Sdep.
+
+  Declare Module E : OrderedType.
+  Definition elt := E.t.
+
+  Parameter t : Set.
+
+  Parameter In : elt -> t -> Prop.
+  Definition Equal s s' := forall a : elt, In a s <-> In a s'.
+  Definition Subset s s' := forall a : elt, In a s -> In a s'.
+  Definition Add x s s' := forall y, In y s' <-> E.eq x y \/ In y s.
+  Definition Empty s := forall a : elt, ~ In a s.
+  Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
+  Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
+
+  Notation "s [=] t" := (Equal s t) (at level 70, no associativity).
+
+  Definition eq : t -> t -> Prop := Equal.
+  Parameter lt : t -> t -> Prop.
+  Parameter compare : forall s s' : t, Compare lt eq s s'.
+
+  Parameter eq_refl : forall s : t, eq s s. 
+  Parameter eq_sym : forall s s' : t, eq s s' -> eq s' s.
+  Parameter eq_trans : forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''.
+  Parameter lt_trans : forall s s' s'' : t, lt s s' -> lt s' s'' -> lt s s''.
+  Parameter lt_not_eq : forall s s' : t, lt s s' -> ~ eq s s'.
+
+  Parameter eq_In : forall (s : t) (x y : elt), E.eq x y -> In x s -> In y s.
+
+  Parameter empty : {s : t | Empty s}.
+
+  Parameter is_empty : forall s : t, {Empty s} + {~ Empty s}.
+
+  Parameter mem : forall (x : elt) (s : t), {In x s} + {~ In x s}.
+
+  Parameter add : forall (x : elt) (s : t), {s' : t | Add x s s'}.
+
+  Parameter
+    singleton : forall x : elt, {s : t | forall y : elt, In y s <-> E.eq x y}.
+  
+  Parameter
+    remove :
+      forall (x : elt) (s : t),
+      {s' : t | forall y : elt, In y s' <-> ~ E.eq x y /\ In y s}.
+
+  Parameter
+    union :
+      forall s s' : t,
+      {s'' : t | forall x : elt, In x s'' <-> In x s \/ In x s'}.
+
+  Parameter
+    inter :
+      forall s s' : t,
+      {s'' : t | forall x : elt, In x s'' <-> In x s /\ In x s'}.
+
+  Parameter
+    diff :
+      forall s s' : t,
+      {s'' : t | forall x : elt, In x s'' <-> In x s /\ ~ In x s'}.
+
+  Parameter equal : forall s s' : t, {s[=]s'} + {~ s[=]s'}.
+ 
+  Parameter subset : forall s s' : t, {Subset s s'} + {~ Subset s s'}.
+
+  Parameter
+    filter :
+      forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
+        (s : t),
+      {s' : t | compat_P E.eq P -> forall x : elt, In x s' <-> In x s /\ P x}.
+
+  Parameter
+    for_all :
+      forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
+        (s : t),
+      {compat_P E.eq P -> For_all P s} + {compat_P E.eq P -> ~ For_all P s}.
+  
+  Parameter
+    exists_ :
+      forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
+        (s : t),
+      {compat_P E.eq P -> Exists P s} + {compat_P E.eq P -> ~ Exists P s}.
+
+  Parameter
+    partition :
+      forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
+        (s : t),
+      {partition : t * t |
+      let (s1, s2) := partition in
+      compat_P E.eq P ->
+      For_all P s1 /\
+      For_all (fun x => ~ P x) s2 /\
+      (forall x : elt, In x s <-> In x s1 \/ In x s2)}.
+
+  Parameter
+    elements :
+      forall s : t,
+      {l : list elt |
+      sort E.lt l /\ (forall x : elt, In x s <-> InA E.eq x l)}.
+
+  Parameter
+    fold :
+      forall (A : Set) (f : elt -> A -> A) (s : t) (i : A),
+      {r : A | let (l,_) := elements s in 
+                  r = fold_left (fun a e => f e a) l i}.
+
+  Parameter
+    cardinal :
+      forall s : t,
+      {r : nat | let (l,_) := elements s in r = length l }.
+
+  Parameter
+    min_elt :
+      forall s : t,
+      {x : elt | In x s /\ For_all (fun y => ~ E.lt y x) s} + {Empty s}.
+
+  Parameter
+    max_elt :
+      forall s : t,
+      {x : elt | In x s /\ For_all (fun y => ~ E.lt x y) s} + {Empty s}.
+
+  Parameter choose : forall s : t, {x : elt | In x s} + {Empty s}.
+
+End Sdep.