1 files changed, 248 insertions, 0 deletions
diff --git a/theories/FSets/FSetWeakInterface.v b/theories/FSets/FSetWeakInterface.v
new file mode 100644
index 00000000..c1845494
--- /dev/null
+++ b/theories/FSets/FSetWeakInterface.v
@@ -0,0 +1,248 @@
+(***********************************************************************)
+(*  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: FSetWeakInterface.v 8641 2006-03-17 09:56:54Z letouzey $ *)
+
+(** * Finite sets library *)
+
+(** Set interfaces for types with only a decidable equality, but no ordering *)
+
+Require Export Bool.
+Require Export DecidableType.
+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 : DecidableType.
+  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. *)
+
+  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].
+  The order in which elements of [s] are presented to [f] is
+  unspecified. *)
+
+  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, in any order. *)
+
+  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.
+  Equal sets could return different elements. *)
+  (** 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 [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 : Equal s s' -> equal s s' = true.
+  Parameter equal_2 : equal s s' = true -> Equal s s'.
+
+  (** Specification of [subset] *)
+  Parameter subset_1 : Subset s s' -> subset s s' = true.
+  Parameter subset_2 : subset s s' = true -> Subset 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 -> Equal (fst (partition f s)) (filter f s).
+  Parameter partition_2 :
+      compat_bool E.eq f ->
+      Equal (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.
+
+  (** Specification of [choose] *)
+  Parameter choose_1 : choose s = Some x -> In x s.
+  Parameter choose_2 : choose s = None -> Empty 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.
+
+End S.