diff options
Diffstat (limited to 'theories/FSets/FSetWeakList.v')
| -rw-r--r-- | theories/FSets/FSetWeakList.v | 257 |
1 files changed, 160 insertions, 97 deletions
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v index 74c81f37..97080b7a 100644 --- a/theories/FSets/FSetWeakList.v +++ b/theories/FSets/FSetWeakList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FSetWeakList.v 8639 2006-03-16 19:21:55Z letouzey $ *) +(* $Id: FSetWeakList.v 8834 2006-05-20 00:41:35Z letouzey $ *) (** * Finite sets library *) @@ -114,7 +114,7 @@ Module Raw (X: DecidableType). end. (** ** Proofs of set operation specifications. *) - + Section ForNotations. Notation NoDup := (NoDupA X.eq). Notation In := (InA X.eq). @@ -750,6 +750,7 @@ Module Raw (X: DecidableType). unfold eq, Equal; firstorder. Qed. + End ForNotations. End Raw. (** * Encapsulation @@ -759,115 +760,177 @@ End Raw. Module Make (X: DecidableType) <: S with Module E := X. - Module E := X. Module Raw := Raw X. + Module E := X. - Record slist : Set := {this :> Raw.t; unique : NoDupA X.eq this}. + Record slist : Set := {this :> Raw.t; unique : NoDupA E.eq this}. Definition t := slist. - Definition elt := X.t. + Definition elt := E.t. - Definition In (x : elt) (s : t) := InA X.eq x s.(this). - 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 : t) := + Definition In (x : elt) (s : t) : Prop := InA E.eq x s.(this). + Definition Equal (s s':t) : Prop := forall a : elt, In a s <-> In a s'. + Definition Subset (s s':t) : Prop := forall a : elt, In a s -> In a s'. + Definition Empty (s:t) : Prop := forall a : elt, ~ In a s. + Definition For_all (P : elt -> Prop) (s : t) : Prop := forall x : elt, In x s -> P x. - Definition Exists (P : elt -> Prop) (s : t) := exists x : elt, In x s /\ P x. - - Definition In_1 (s : t) := Raw.In_eq (s:=s). - - Definition mem (x : elt) (s : t) := Raw.mem x s. - Definition mem_1 (s : t) := Raw.mem_1 (s:=s). - Definition mem_2 (s : t) := Raw.mem_2 (s:=s). - - Definition add x s := Build_slist (Raw.add_unique (unique s) x). - Definition add_1 (s : t) := Raw.add_1 (unique s). - Definition add_2 (s : t) := Raw.add_2 (unique s). - Definition add_3 (s : t) := Raw.add_3 (unique s). - - Definition remove x s := Build_slist (Raw.remove_unique (unique s) x). - Definition remove_1 (s : t) := Raw.remove_1 (unique s). - Definition remove_2 (s : t) := Raw.remove_2 (unique s). - Definition remove_3 (s : t) := Raw.remove_3 (unique s). - - Definition singleton x := Build_slist (Raw.singleton_unique x). - Definition singleton_1 := Raw.singleton_1. - Definition singleton_2 := Raw.singleton_2. - - Definition union (s s' : t) := - Build_slist (Raw.union_unique (unique s) (unique s')). - Definition union_1 (s s' : t) := Raw.union_1 (unique s) (unique s'). - Definition union_2 (s s' : t) := Raw.union_2 (unique s) (unique s'). - Definition union_3 (s s' : t) := Raw.union_3 (unique s) (unique s'). + Definition Exists (P : elt -> Prop) (s : t) : Prop := exists x : elt, In x s /\ P x. - Definition inter (s s' : t) := + Definition mem (x : elt) (s : t) : bool := Raw.mem x s. + Definition add (x : elt)(s : t) : t := Build_slist (Raw.add_unique (unique s) x). + Definition remove (x : elt)(s : t) : t := Build_slist (Raw.remove_unique (unique s) x). + Definition singleton (x : elt) : t := Build_slist (Raw.singleton_unique x). + Definition union (s s' : t) : t := + Build_slist (Raw.union_unique (unique s) (unique s')). + Definition inter (s s' : t) : t := Build_slist (Raw.inter_unique (unique s) (unique s')). - Definition inter_1 (s s' : t) := Raw.inter_1 (unique s) (unique s'). - Definition inter_2 (s s' : t) := Raw.inter_2 (unique s) (unique s'). - Definition inter_3 (s s' : t) := Raw.inter_3 (unique s) (unique s'). - - Definition diff (s s' : t) := + Definition diff (s s' : t) : t := Build_slist (Raw.diff_unique (unique s) (unique s')). - Definition diff_1 (s s' : t) := Raw.diff_1 (unique s) (unique s'). - Definition diff_2 (s s' : t) := Raw.diff_2 (unique s) (unique s'). - Definition diff_3 (s s' : t) := Raw.diff_3 (unique s) (unique s'). - - Definition equal (s s' : t) := Raw.equal s s'. - Definition equal_1 (s s' : t) := Raw.equal_1 (unique s) (unique s'). - Definition equal_2 (s s' : t) := Raw.equal_2 (unique s) (unique s'). - - Definition subset (s s' : t) := Raw.subset s s'. - Definition subset_1 (s s' : t) := Raw.subset_1 (unique s) (unique s'). - Definition subset_2 (s s' : t) := Raw.subset_2 (unique s) (unique s'). + Definition equal (s s' : t) : bool := Raw.equal s s'. + Definition subset (s s' : t) : bool := Raw.subset s s'. + Definition empty : t := Build_slist Raw.empty_unique. + Definition is_empty (s : t) : bool := Raw.is_empty s. + Definition elements (s : t) : list elt := Raw.elements s. + Definition choose (s:t) : option elt := Raw.choose s. + Definition fold (B : Set) (f : elt -> B -> B) (s : t) : B -> B := Raw.fold (B:=B) f s. + Definition cardinal (s : t) : nat := Raw.cardinal s. + Definition filter (f : elt -> bool) (s : t) : t := + Build_slist (Raw.filter_unique (unique s) f). + Definition for_all (f : elt -> bool) (s : t) : bool := Raw.for_all f s. + Definition exists_ (f : elt -> bool) (s : t) : bool := Raw.exists_ f s. + Definition partition (f : elt -> bool) (s : t) : t * t := + let p := Raw.partition f s in + (Build_slist (this:=fst p) (Raw.partition_unique_1 (unique s) f), + Build_slist (this:=snd p) (Raw.partition_unique_2 (unique s) f)). + + Section Spec. + Variable s s' : t. + Variable x y : elt. - Definition empty := Build_slist Raw.empty_unique. - Definition empty_1 := Raw.empty_1. + Lemma In_1 : E.eq x y -> In x s -> In y s. + Proof. exact (fun H H' => Raw.In_eq H H'). Qed. - Definition is_empty (s : t) := Raw.is_empty s. - Definition is_empty_1 (s : t) := Raw.is_empty_1 (s:=s). - Definition is_empty_2 (s : t) := Raw.is_empty_2 (s:=s). - - Definition elements (s : t) := Raw.elements s. - Definition elements_1 (s : t) := Raw.elements_1 (s:=s). - Definition elements_2 (s : t) := Raw.elements_2 (s:=s). - Definition elements_3 (s : t) := Raw.elements_3 (unique s). - - Definition choose (s:t) := Raw.choose s. - Definition choose_1 (s : t) := Raw.choose_1 (s:=s). - Definition choose_2 (s : t) := Raw.choose_2 (s:=s). - - Definition fold (B : Set) (f : elt -> B -> B) (s : t) := Raw.fold (B:=B) f s. - Definition fold_1 (s : t) := Raw.fold_1 (unique s). + Lemma mem_1 : In x s -> mem x s = true. + Proof. exact (fun H => Raw.mem_1 H). Qed. + Lemma mem_2 : mem x s = true -> In x s. + Proof. exact (fun H => Raw.mem_2 H). Qed. - Definition cardinal (s : t) := Raw.cardinal s. - Definition cardinal_1 (s : t) := Raw.cardinal_1 (unique s). + Lemma equal_1 : Equal s s' -> equal s s' = true. + Proof. exact (Raw.equal_1 s.(unique) s'.(unique)). Qed. + Lemma equal_2 : equal s s' = true -> Equal s s'. + Proof. exact (Raw.equal_2 s.(unique) s'.(unique)). Qed. + + Lemma subset_1 : Subset s s' -> subset s s' = true. + Proof. exact (Raw.subset_1 s.(unique) s'.(unique)). Qed. + Lemma subset_2 : subset s s' = true -> Subset s s'. + Proof. exact (Raw.subset_2 s.(unique) s'.(unique)). Qed. + + Lemma empty_1 : Empty empty. + Proof. exact Raw.empty_1. Qed. + + Lemma is_empty_1 : Empty s -> is_empty s = true. + Proof. exact (fun H => Raw.is_empty_1 H). Qed. + Lemma is_empty_2 : is_empty s = true -> Empty s. + Proof. exact (fun H => Raw.is_empty_2 H). Qed. - Definition filter (f : elt -> bool) (s : t) := - Build_slist (Raw.filter_unique (unique s) f). - Definition filter_1 (s : t)(x:elt)(f: elt -> bool)(H:compat_bool X.eq f) := - @Raw.filter_1 s x f. - Definition filter_2 (s : t) := Raw.filter_2 (s:=s). - Definition filter_3 (s : t) := Raw.filter_3 (s:=s). + Lemma add_1 : E.eq x y -> In y (add x s). + Proof. exact (fun H => Raw.add_1 s.(unique) H). Qed. + Lemma add_2 : In y s -> In y (add x s). + Proof. exact (fun H => Raw.add_2 s.(unique) x H). Qed. + Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s. + Proof. exact (fun H => Raw.add_3 s.(unique) H). Qed. + + Lemma remove_1 : E.eq x y -> ~ In y (remove x s). + Proof. exact (fun H => Raw.remove_1 s.(unique) H). Qed. + Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s). + Proof. exact (fun H H' => Raw.remove_2 s.(unique) H H'). Qed. + Lemma remove_3 : In y (remove x s) -> In y s. + Proof. exact (fun H => Raw.remove_3 s.(unique) H). Qed. + + Lemma singleton_1 : In y (singleton x) -> E.eq x y. + Proof. exact (fun H => Raw.singleton_1 H). Qed. + Lemma singleton_2 : E.eq x y -> In y (singleton x). + Proof. exact (fun H => Raw.singleton_2 H). Qed. + + Lemma union_1 : In x (union s s') -> In x s \/ In x s'. + Proof. exact (fun H => Raw.union_1 s.(unique) s'.(unique) H). Qed. + Lemma union_2 : In x s -> In x (union s s'). + Proof. exact (fun H => Raw.union_2 s.(unique) s'.(unique) H). Qed. + Lemma union_3 : In x s' -> In x (union s s'). + Proof. exact (fun H => Raw.union_3 s.(unique) s'.(unique) H). Qed. + + Lemma inter_1 : In x (inter s s') -> In x s. + Proof. exact (fun H => Raw.inter_1 s.(unique) s'.(unique) H). Qed. + Lemma inter_2 : In x (inter s s') -> In x s'. + Proof. exact (fun H => Raw.inter_2 s.(unique) s'.(unique) H). Qed. + Lemma inter_3 : In x s -> In x s' -> In x (inter s s'). + Proof. exact (fun H => Raw.inter_3 s.(unique) s'.(unique) H). Qed. + + Lemma diff_1 : In x (diff s s') -> In x s. + Proof. exact (fun H => Raw.diff_1 s.(unique) s'.(unique) H). Qed. + Lemma diff_2 : In x (diff s s') -> ~ In x s'. + Proof. exact (fun H => Raw.diff_2 s.(unique) s'.(unique) H). Qed. + Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s'). + Proof. exact (fun H => Raw.diff_3 s.(unique) s'.(unique) H). Qed. - Definition for_all (f : elt -> bool) (s : t) := Raw.for_all f s. - Definition for_all_1 (s : t) := Raw.for_all_1 (s:=s). - Definition for_all_2 (s : t) := Raw.for_all_2 (s:=s). + Lemma 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. + Proof. exact (Raw.fold_1 s.(unique)). Qed. - Definition exists_ (f : elt -> bool) (s : t) := Raw.exists_ f s. - Definition exists_1 (s : t) := Raw.exists_1 (s:=s). - Definition exists_2 (s : t) := Raw.exists_2 (s:=s). + Lemma cardinal_1 : cardinal s = length (elements s). + Proof. exact (Raw.cardinal_1 s.(unique)). Qed. - Definition partition (f : elt -> bool) (s : t) := - let p := Raw.partition f s in - (Build_slist (this:=fst p) (Raw.partition_unique_1 (unique s) f), - Build_slist (this:=snd p) (Raw.partition_unique_2 (unique s) f)). - Definition partition_1 (s : t) := Raw.partition_1 s. - Definition partition_2 (s : t) := Raw.partition_2 s. - - Definition eq (s s' : t) := Raw.eq s s'. - Definition eq_refl (s : t) := Raw.eq_refl s. - Definition eq_sym (s s' : t) := Raw.eq_sym (s:=s) (s':=s'). - Definition eq_trans (s s' s'' : t) := - Raw.eq_trans (s:=s) (s':=s') (s'':=s''). + Section Filter. + + Variable f : elt -> bool. + + Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s. + Proof. exact (fun H => @Raw.filter_1 s x f). Qed. + Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true. + Proof. exact (@Raw.filter_2 s x f). Qed. + Lemma filter_3 : + compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s). + Proof. exact (@Raw.filter_3 s x f). Qed. + + Lemma for_all_1 : + compat_bool E.eq f -> + For_all (fun x => f x = true) s -> for_all f s = true. + Proof. exact (@Raw.for_all_1 s f). Qed. + Lemma for_all_2 : + compat_bool E.eq f -> + for_all f s = true -> For_all (fun x => f x = true) s. + Proof. exact (@Raw.for_all_2 s f). Qed. + + Lemma exists_1 : + compat_bool E.eq f -> + Exists (fun x => f x = true) s -> exists_ f s = true. + Proof. exact (@Raw.exists_1 s f). Qed. + Lemma exists_2 : + compat_bool E.eq f -> + exists_ f s = true -> Exists (fun x => f x = true) s. + Proof. exact (@Raw.exists_2 s f). Qed. + + Lemma partition_1 : + compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s). + Proof. exact (@Raw.partition_1 s f). Qed. + Lemma partition_2 : + compat_bool E.eq f -> + Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). + Proof. exact (@Raw.partition_2 s f). Qed. + + End Filter. + + Lemma elements_1 : In x s -> InA E.eq x (elements s). + Proof. exact (fun H => Raw.elements_1 H). Qed. + Lemma elements_2 : InA E.eq x (elements s) -> In x s. + Proof. exact (fun H => Raw.elements_2 H). Qed. + Lemma elements_3 : NoDupA E.eq (elements s). + Proof. exact (Raw.elements_3 s.(unique)). Qed. + + Lemma choose_1 : choose s = Some x -> In x s. + Proof. exact (fun H => Raw.choose_1 H). Qed. + Lemma choose_2 : choose s = None -> Empty s. + Proof. exact (fun H => Raw.choose_2 H). Qed. + + End Spec. End Make. |