diff options
Diffstat (limited to 'theories/FSets/FSetInterface.v')
| -rw-r--r-- | theories/FSets/FSetInterface.v | 108 |
1 files changed, 54 insertions, 54 deletions
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v index 79eea34e..8aede552 100644 --- a/theories/FSets/FSetInterface.v +++ b/theories/FSets/FSetInterface.v @@ -6,17 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FSetInterface.v 11701 2008-12-18 11:49:12Z letouzey $ *) +(* $Id$ *) (** * Finite set library *) -(** Set interfaces, inspired by the one of Ocaml. When compared with - Ocaml, the main differences are: +(** Set interfaces, inspired by the one of Ocaml. When compared with + Ocaml, the main differences are: - the lack of [iter] function, useless since Coq is purely functional - the use of [option] types instead of [Not_found] exceptions - - the use of [nat] instead of [int] for the [cardinal] function + - the use of [nat] instead of [int] for the [cardinal] function - Several variants of the set interfaces are available: + Several variants of the set interfaces are available: - [WSfun] : functorial signature for weak sets, non-dependent style - [WS] : self-contained version of [WSfun] - [Sfun] : functorial signature for ordered sets, non-dependent style @@ -24,7 +24,7 @@ - [Sdep] : analog of [S] written using dependent style If unsure, [S] is probably what you're looking for: other signatures - are subsets of it, apart from [Sdep] which is isomorphic to [S] (see + are subsets of it, apart from [Sdep] which is isomorphic to [S] (see [FSetBridge]). *) @@ -34,14 +34,14 @@ Unset Strict Implicit. (** * Non-dependent signatures - The following signatures presents sets as purely informative + The following signatures presents sets as purely informative programs together with axioms *) (** ** Functorial signature for weak sets - Weak sets are sets without ordering on base elements, only + Weak sets are sets without ordering on base elements, only a decidable equality. *) Module Type WSfun (E : DecidableType). @@ -57,7 +57,7 @@ Module Type WSfun (E : DecidableType). 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). @@ -137,7 +137,7 @@ Module Type WSfun (E : DecidableType). the set is empty. Which element is chosen is unspecified. Equal sets could return different elements. *) - Section Spec. + Section Spec. Variable s s' s'': t. Variable x y : elt. @@ -146,15 +146,15 @@ Module Type WSfun (E : DecidableType). Parameter In_1 : E.eq x y -> In x s -> In y s. (** Specification of [eq] *) - Parameter eq_refl : eq s s. + 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 [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 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'. @@ -166,13 +166,13 @@ Module Type WSfun (E : DecidableType). Parameter empty_1 : Empty empty. (** Specification of [is_empty] *) - Parameter is_empty_1 : Empty s -> is_empty s = true. + 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. + 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). @@ -180,12 +180,12 @@ Module Type WSfun (E : DecidableType). 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). + 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_2 : In x s -> In x (union s s'). Parameter union_3 : In x s' -> In x (union s s'). (** Specification of [inter] *) @@ -194,24 +194,24 @@ Module Type WSfun (E : DecidableType). 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_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] *) + + (** Specification of [fold] *) Parameter fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A), fold f s i = fold_left (fun a e => f e a) (elements s) i. - (** Specification of [cardinal] *) + (** 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_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). @@ -243,7 +243,7 @@ Module Type WSfun (E : DecidableType). (** 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. - (** When compared with ordered sets, here comes the only + (** When compared with ordered sets, here comes the only property that is really weaker: *) Parameter elements_3w : NoDupA E.eq (elements s). @@ -257,11 +257,11 @@ Module Type WSfun (E : DecidableType). is_empty_1 choose_1 choose_2 add_1 add_2 remove_1 remove_2 singleton_2 union_1 union_2 union_3 inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1 - partition_1 partition_2 elements_1 elements_3w + partition_1 partition_2 elements_1 elements_3w : set. Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3 remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2 - filter_1 filter_2 for_all_2 exists_2 elements_2 + filter_1 filter_2 for_all_2 exists_2 elements_2 : set. End WSfun. @@ -270,12 +270,12 @@ End WSfun. (** ** Static signature for weak sets - Similar to the functorial signature [SW], except that the + Similar to the functorial signature [SW], except that the module [E] of base elements is incorporated in the signature. *) Module Type WS. Declare Module E : DecidableType. - Include Type WSfun E. + Include WSfun E. End WS. @@ -286,7 +286,7 @@ End WS. and some stronger specifications for other functions. *) Module Type Sfun (E : OrderedType). - Include Type WSfun E. + Include WSfun E. Parameter lt : t -> t -> Prop. Parameter compare : forall s s' : t, Compare lt eq s s'. @@ -295,48 +295,48 @@ Module Type Sfun (E : OrderedType). Parameter min_elt : t -> option elt. (** Return the smallest element of the given set - (with respect to the [E.compare] ordering), + (with respect to the [E.compare] ordering), or [None] if the set is empty. *) Parameter max_elt : t -> option elt. (** Same as [min_elt], but returns the largest element of the given set. *) - Section Spec. + Section Spec. Variable s s' s'' : t. Variable x y : elt. - + (** 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'. (** Additional specification of [elements] *) - Parameter elements_3 : sort E.lt (elements s). + Parameter elements_3 : sort E.lt (elements s). (** Remark: since [fold] is specified via [elements], this stronger - specification of [elements] has an indirect impact on [fold], + specification of [elements] has an indirect impact on [fold], which can now be proved to receive elements in increasing order. *) (** 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_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. + (** 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. (** Additional specification of [choose] *) - Parameter choose_3 : choose s = Some x -> choose s' = Some y -> + Parameter choose_3 : choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y. End Spec. Hint Resolve elements_3 : set. - Hint Immediate + Hint Immediate min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3 : set. End Sfun. @@ -344,12 +344,12 @@ End Sfun. (** ** Static signature for sets on ordered elements - Similar to the functorial signature [Sfun], except that the + Similar to the functorial signature [Sfun], except that the module [E] of base elements is incorporated in the signature. *) Module Type S. Declare Module E : OrderedType. - Include Type Sfun E. + Include Sfun E. End S. @@ -411,7 +411,7 @@ Module Type Sdep. Parameter singleton : forall x : elt, {s : t | forall y : elt, In y s <-> E.eq x y}. - + Parameter remove : forall (x : elt) (s : t), @@ -433,7 +433,7 @@ Module Type Sdep. {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 @@ -447,7 +447,7 @@ Module Type Sdep. 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}) @@ -474,7 +474,7 @@ Module Type Sdep. Parameter fold : forall (A : Type) (f : elt -> A -> A) (s : t) (i : A), - {r : A | let (l,_) := elements s in + {r : A | let (l,_) := elements s in r = fold_left (fun a e => f e a) l i}. Parameter @@ -494,10 +494,10 @@ Module Type Sdep. Parameter choose : forall s : t, {x : elt | In x s} + {Empty s}. - (** The [choose_3] specification of [S] cannot be packed + (** The [choose_3] specification of [S] cannot be packed in the dependent version of [choose], so we leave it separate. *) - Parameter choose_equal : forall s s', Equal s s' -> - match choose s, choose s' with + Parameter choose_equal : forall s s', Equal s s' -> + match choose s, choose s' with | inleft (exist x _), inleft (exist x' _) => E.eq x x' | inright _, inright _ => True | _, _ => False |