diff options
-rw-r--r-- | theories/FSets/FSetAVL.v | 24 | ||||
-rw-r--r-- | theories/FSets/FSetBridge.v | 8 | ||||
-rw-r--r-- | theories/FSets/FSetFacts.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSetList.v | 216 | ||||
-rw-r--r-- | theories/FSets/FSetWeakList.v | 188 | ||||
-rw-r--r-- | theories/FSets/OrderedType.v | 4 |
6 files changed, 225 insertions, 217 deletions
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index cdc5e8d33..cb2a03cf2 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -1785,19 +1785,19 @@ Qed. (** Induction over cardinals *) Lemma sorted_subset_cardinal : forall l' l : list X.t, - MX.Sort l -> MX.Sort l' -> - (forall x : elt, MX.In x l -> MX.In x l') -> (length l <= length l')%nat. + sort X.lt l -> sort X.lt l' -> + (forall x : elt, InA X.eq x l -> InA X.eq x l') -> (length l <= length l')%nat. Proof. simple induction l'; simpl in |- *; intuition. destruct l; trivial; intros. - absurd (MX.In t nil); intuition. + absurd (InA X.eq t nil); intuition. inversion_clear H2. inversion_clear H1. destruct l0; simpl in |- *; intuition. inversion_clear H0. apply le_n_S. case (X.compare t a); intro. - absurd (MX.In t (a :: l)). + absurd (InA X.eq t (a :: l)). intro. inversion_clear H0. order. @@ -1807,7 +1807,7 @@ Proof. firstorder. apply H; auto. intros. - assert (MX.In x (a :: l)). + assert (InA X.eq x (a :: l)). apply H2; auto. inversion_clear H6; auto. assert (X.lt t x). @@ -1817,7 +1817,7 @@ Proof. simpl in |- *; omega. apply (H (t :: l0)); auto. intros. - assert (MX.In x (a :: l)); firstorder. + assert (InA X.eq x (a :: l)); firstorder. inversion_clear H6; auto. assert (X.lt a x). apply MX.Sort_Inf_In with (t :: l0); auto. @@ -2208,7 +2208,7 @@ Hint Constructors sorted_e. Lemma in_app : forall (x : elt) (l1 l2 : list elt), - L.MX.In x (l1 ++ l2) -> L.MX.In x l1 \/ L.MX.In x l2. + InA X.eq x (l1 ++ l2) -> InA X.eq x l1 \/ InA X.eq x l2. Proof. simple induction l1; simpl in |- *; intuition. inversion_clear H0; auto. @@ -2216,7 +2216,7 @@ Proof. Qed. Lemma in_flatten_e : - forall (x : elt) (e : enumeration), L.MX.In x (flatten_e e) -> In_e x e. + forall (x : elt) (e : enumeration), InA X.eq x (flatten_e e) -> In_e x e. Proof. simple induction e; simpl in |- *; intuition. inversion_clear H. @@ -2226,9 +2226,9 @@ Proof. Qed. Lemma sort_app : - forall l1 l2 : list elt, L.MX.Sort l1 -> L.MX.Sort l2 -> - (forall x y : elt, L.MX.In x l1 -> L.MX.In y l2 -> X.lt x y) -> - L.MX.Sort (l1 ++ l2). + forall l1 l2 : list elt, sort X.lt l1 -> sort X.lt l2 -> + (forall x y : elt, InA X.eq x l1 -> InA X.eq y l2 -> X.lt x y) -> + sort X.lt (l1 ++ l2). Proof. simple induction l1; simpl in |- *; intuition. apply cons_sort; auto. @@ -2240,7 +2240,7 @@ Proof. Qed. Lemma sorted_flatten_e : - forall e : enumeration, sorted_e e -> L.MX.Sort (flatten_e e). + forall e : enumeration, sorted_e e -> sort X.lt (flatten_e e). Proof. simple induction e; simpl in |- *; intuition. apply cons_sort. diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 90539ff05..9ac7b9c7c 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -109,7 +109,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. Definition elements : forall s : t, - {l : list elt | ME.Sort l /\ (forall x : elt, In x s <-> ME.In x l)}. + {l : list elt | sort E.lt l /\ (forall x : elt, In x s <-> InA E.eq x l)}. Proof. intros; exists (elements s); intuition. Defined. @@ -394,17 +394,17 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Definition elements (s : t) : list elt := let (l, _) := elements s in l. - Lemma elements_1 : forall (s : t) (x : elt), In x s -> ME.In x (elements s). + Lemma elements_1 : forall (s : t) (x : elt), In x s -> InA E.eq x (elements s). Proof. intros; unfold elements in |- *; case (M.elements s); firstorder. Qed. - Lemma elements_2 : forall (s : t) (x : elt), ME.In x (elements s) -> In x s. + Lemma elements_2 : forall (s : t) (x : elt), InA E.eq x (elements s) -> In x s. Proof. intros s x; unfold elements in |- *; case (M.elements s); firstorder. Qed. - Lemma elements_3 : forall s : t, ME.Sort (elements s). + Lemma elements_3 : forall s : t, sort E.lt (elements s). Proof. intros; unfold elements in |- *; case (M.elements s); firstorder. Qed. diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index 0edb009cf..2b9548fe4 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -131,7 +131,7 @@ Proof. split; [apply exists_1 | apply exists_2]; auto. Qed. -Lemma elements_iff : In x s <-> ME.In x (elements s). +Lemma elements_iff : In x s <-> InA E.eq x (elements s). Proof. split; [apply elements_1 | apply elements_2]. Qed. diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v index ac26d5786..51771fc41 100644 --- a/theories/FSets/FSetList.v +++ b/theories/FSets/FSetList.v @@ -199,6 +199,8 @@ Module Raw (X: OrderedType). (** ** Proofs of set operation specifications. *) + Section ForNotations. + Notation Sort := (sort X.lt). Notation Inf := (lelistA X.lt). Notation In := (InA X.eq). @@ -1020,6 +1022,9 @@ Module Raw (X: OrderedType). destruct (e1 a0); auto. Defined. + End ForNotations. + Hint Constructors lt. + End Raw. (** * Encapsulation @@ -1030,209 +1035,208 @@ End Raw. Module Make (X: OrderedType) <: S with Module E := X. Module Raw := Raw X. - Import Raw. Module E := X. - Record slist : Set := {this :> Raw.t; sorted : sort X.lt this}. + Record slist : Set := {this :> Raw.t; sorted : sort E.lt this}. Definition t := slist. - Definition elt := X.t. + Definition elt := E.t. - Definition In (x : elt) (s : t) : Prop := InA X.eq x s.(this). + 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, In x s -> P x. Definition Exists (P : elt -> Prop)(s:t) : Prop := exists x, In x s /\ P x. - Definition mem (x : elt) (s : t) : bool := mem x s. - Definition add (x : elt)(s : t) : t := Build_slist (add_sort (sorted s) x). - Definition remove (x : elt)(s : t) : t := Build_slist (remove_sort (sorted s) x). - Definition singleton (x : elt) : t := Build_slist (singleton_sort x). + Definition mem (x : elt) (s : t) : bool := Raw.mem x s. + Definition add (x : elt)(s : t) : t := Build_slist (Raw.add_sort (sorted s) x). + Definition remove (x : elt)(s : t) : t := Build_slist (Raw.remove_sort (sorted s) x). + Definition singleton (x : elt) : t := Build_slist (Raw.singleton_sort x). Definition union (s s' : t) : t := - Build_slist (union_sort (sorted s) (sorted s')). + Build_slist (Raw.union_sort (sorted s) (sorted s')). Definition inter (s s' : t) : t := - Build_slist (inter_sort (sorted s) (sorted s')). + Build_slist (Raw.inter_sort (sorted s) (sorted s')). Definition diff (s s' : t) : t := - Build_slist (diff_sort (sorted s) (sorted s')). - Definition equal (s s' : t) : bool := equal s s'. - Definition subset (s s' : t) : bool := subset s s'. - Definition empty : t := Build_slist empty_sort. - Definition is_empty (s : t) : bool := is_empty s. - Definition elements (s : t) : list elt := elements s. - Definition min_elt (s : t) : option elt := min_elt s. - Definition max_elt (s : t) : option elt := max_elt s. - Definition choose (s : t) : option elt := choose s. - Definition fold (B : Set) (f : elt -> B -> B) (s : t) : B -> B := fold (B:=B) f s. - Definition cardinal (s : t) : nat := cardinal s. + Build_slist (Raw.diff_sort (sorted s) (sorted 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_sort. + Definition is_empty (s : t) : bool := Raw.is_empty s. + Definition elements (s : t) : list elt := Raw.elements s. + Definition min_elt (s : t) : option elt := Raw.min_elt s. + Definition max_elt (s : t) : option elt := Raw.max_elt 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 (filter_sort (sorted s) f). - Definition for_all (f : elt -> bool) (s : t) : bool := for_all f s. - Definition exists_ (f : elt -> bool) (s : t) : bool := exists_ f s. + Build_slist (Raw.filter_sort (sorted 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 := partition f s in - (Build_slist (this:=fst p) (partition_sort_1 (sorted s) f), - Build_slist (this:=snd p) (partition_sort_2 (sorted s) f)). - Definition eq (s s' : t) : Prop := eq s s'. - Definition lt (s s' : t) : Prop := lt s s'. + let p := Raw.partition f s in + (Build_slist (this:=fst p) (Raw.partition_sort_1 (sorted s) f), + Build_slist (this:=snd p) (Raw.partition_sort_2 (sorted s) f)). + Definition eq (s s' : t) : Prop := Raw.eq s s'. + Definition lt (s s' : t) : Prop := Raw.lt s s'. Section Spec. Variable s s' s'': t. Variable x y : elt. - Lemma In_1 : X.eq x y -> In x s -> In y s. - Proof. exact (fun H H' => MX.In_eq H H'). Qed. + Lemma In_1 : E.eq x y -> In x s -> In y s. + Proof. exact (fun H H' => Raw.MX.In_eq H H'). Qed. Lemma mem_1 : In x s -> mem x s = true. - Proof. exact (fun H => mem_1 s.(sorted) H). Qed. + Proof. exact (fun H => Raw.mem_1 s.(sorted) H). Qed. Lemma mem_2 : mem x s = true -> In x s. - Proof. exact (fun H => mem_2 H). Qed. + Proof. exact (fun H => Raw.mem_2 H). Qed. Lemma equal_1 : Equal s s' -> equal s s' = true. - Proof. exact (equal_1 s.(sorted) s'.(sorted)). Qed. + Proof. exact (Raw.equal_1 s.(sorted) s'.(sorted)). Qed. Lemma equal_2 : equal s s' = true -> Equal s s'. - Proof. exact (fun H => equal_2 H). Qed. + Proof. exact (fun H => Raw.equal_2 H). Qed. Lemma subset_1 : Subset s s' -> subset s s' = true. - Proof. exact (subset_1 s.(sorted) s'.(sorted)). Qed. + Proof. exact (Raw.subset_1 s.(sorted) s'.(sorted)). Qed. Lemma subset_2 : subset s s' = true -> Subset s s'. - Proof. exact (fun H => subset_2 H). Qed. + Proof. exact (fun H => Raw.subset_2 H). Qed. Lemma empty_1 : Empty empty. - Proof. exact empty_1. Qed. + Proof. exact Raw.empty_1. Qed. Lemma is_empty_1 : Empty s -> is_empty s = true. - Proof. exact (fun H => is_empty_1 H). Qed. + Proof. exact (fun H => Raw.is_empty_1 H). Qed. Lemma is_empty_2 : is_empty s = true -> Empty s. - Proof. exact (fun H => is_empty_2 H). Qed. + Proof. exact (fun H => Raw.is_empty_2 H). Qed. - Lemma add_1 : X.eq x y -> In y (add x s). - Proof. exact (fun H => add_1 s.(sorted) H). Qed. + Lemma add_1 : E.eq x y -> In y (add x s). + Proof. exact (fun H => Raw.add_1 s.(sorted) H). Qed. Lemma add_2 : In y s -> In y (add x s). - Proof. exact (fun H => add_2 s.(sorted) x H). Qed. - Lemma add_3 : ~ X.eq x y -> In y (add x s) -> In y s. - Proof. exact (fun H => add_3 s.(sorted) H). Qed. - - Lemma remove_1 : X.eq x y -> ~ In y (remove x s). - Proof. exact (fun H => remove_1 s.(sorted) H). Qed. - Lemma remove_2 : ~ X.eq x y -> In y s -> In y (remove x s). - Proof. exact (fun H H' => remove_2 s.(sorted) H H'). Qed. + Proof. exact (fun H => Raw.add_2 s.(sorted) 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.(sorted) H). Qed. + + Lemma remove_1 : E.eq x y -> ~ In y (remove x s). + Proof. exact (fun H => Raw.remove_1 s.(sorted) 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.(sorted) H H'). Qed. Lemma remove_3 : In y (remove x s) -> In y s. - Proof. exact (fun H => remove_3 s.(sorted) H). Qed. + Proof. exact (fun H => Raw.remove_3 s.(sorted) H). Qed. - Lemma singleton_1 : In y (singleton x) -> X.eq x y. - Proof. exact (fun H => singleton_1 H). Qed. - Lemma singleton_2 : X.eq x y -> In y (singleton x). - Proof. exact (fun H => singleton_2 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 => union_1 s.(sorted) s'.(sorted) H). Qed. + Proof. exact (fun H => Raw.union_1 s.(sorted) s'.(sorted) H). Qed. Lemma union_2 : In x s -> In x (union s s'). - Proof. exact (fun H => union_2 s.(sorted) s'.(sorted) H). Qed. + Proof. exact (fun H => Raw.union_2 s.(sorted) s'.(sorted) H). Qed. Lemma union_3 : In x s' -> In x (union s s'). - Proof. exact (fun H => union_3 s.(sorted) s'.(sorted) H). Qed. + Proof. exact (fun H => Raw.union_3 s.(sorted) s'.(sorted) H). Qed. Lemma inter_1 : In x (inter s s') -> In x s. - Proof. exact (fun H => inter_1 s.(sorted) s'.(sorted) H). Qed. + Proof. exact (fun H => Raw.inter_1 s.(sorted) s'.(sorted) H). Qed. Lemma inter_2 : In x (inter s s') -> In x s'. - Proof. exact (fun H => inter_2 s.(sorted) s'.(sorted) H). Qed. + Proof. exact (fun H => Raw.inter_2 s.(sorted) s'.(sorted) H). Qed. Lemma inter_3 : In x s -> In x s' -> In x (inter s s'). - Proof. exact (fun H => inter_3 s.(sorted) s'.(sorted) H). Qed. + Proof. exact (fun H => Raw.inter_3 s.(sorted) s'.(sorted) H). Qed. Lemma diff_1 : In x (diff s s') -> In x s. - Proof. exact (fun H => diff_1 s.(sorted) s'.(sorted) H). Qed. + Proof. exact (fun H => Raw.diff_1 s.(sorted) s'.(sorted) H). Qed. Lemma diff_2 : In x (diff s s') -> ~ In x s'. - Proof. exact (fun H => diff_2 s.(sorted) s'.(sorted) H). Qed. + Proof. exact (fun H => Raw.diff_2 s.(sorted) s'.(sorted) H). Qed. Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s'). - Proof. exact (fun H => diff_3 s.(sorted) s'.(sorted) H). Qed. + Proof. exact (fun H => Raw.diff_3 s.(sorted) s'.(sorted) H). Qed. 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 (fold_1 s.(sorted)). Qed. + Proof. exact (Raw.fold_1 s.(sorted)). Qed. Lemma cardinal_1 : cardinal s = length (elements s). - Proof. exact (cardinal_1 s.(sorted)). Qed. + Proof. exact (Raw.cardinal_1 s.(sorted)). Qed. Section Filter. Variable f : elt -> bool. - Lemma filter_1 : compat_bool X.eq f -> In x (filter f s) -> In x s. - Proof. exact (@filter_1 s x f). Qed. - Lemma filter_2 : compat_bool X.eq f -> In x (filter f s) -> f x = true. - Proof. exact (@filter_2 s x f). Qed. + Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s. + Proof. exact (@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 X.eq f -> In x s -> f x = true -> In x (filter f s). - Proof. exact (@filter_3 s x f). Qed. + 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 X.eq f -> + compat_bool E.eq f -> For_all (fun x => f x = true) s -> for_all f s = true. - Proof. exact (@for_all_1 s f). Qed. + Proof. exact (@Raw.for_all_1 s f). Qed. Lemma for_all_2 : - compat_bool X.eq f -> + compat_bool E.eq f -> for_all f s = true -> For_all (fun x => f x = true) s. - Proof. exact (@for_all_2 s f). Qed. + Proof. exact (@Raw.for_all_2 s f). Qed. Lemma exists_1 : - compat_bool X.eq f -> + compat_bool E.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true. - Proof. exact (@exists_1 s f). Qed. + Proof. exact (@Raw.exists_1 s f). Qed. Lemma exists_2 : - compat_bool X.eq f -> + compat_bool E.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s. - Proof. exact (@exists_2 s f). Qed. + Proof. exact (@Raw.exists_2 s f). Qed. Lemma partition_1 : - compat_bool X.eq f -> Equal (fst (partition f s)) (filter f s). - Proof. exact (@partition_1 s f). Qed. + 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 X.eq f -> + compat_bool E.eq f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). - Proof. exact (@partition_2 s f). Qed. + Proof. exact (@Raw.partition_2 s f). Qed. End Filter. - Lemma elements_1 : In x s -> InA X.eq x (elements s). - Proof. exact (fun H => elements_1 H). Qed. - Lemma elements_2 : InA X.eq x (elements s) -> In x s. - Proof. exact (fun H => elements_2 H). Qed. - Lemma elements_3 : sort X.lt (elements s). - Proof. exact (elements_3 s.(sorted)). Qed. + 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 : sort E.lt (elements s). + Proof. exact (Raw.elements_3 s.(sorted)). Qed. Lemma min_elt_1 : min_elt s = Some x -> In x s. - Proof. exact (fun H => min_elt_1 H). Qed. - Lemma min_elt_2 : min_elt s = Some x -> In y s -> ~ X.lt y x. - Proof. exact (fun H => min_elt_2 s.(sorted) H). Qed. + Proof. exact (fun H => Raw.min_elt_1 H). Qed. + Lemma min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x. + Proof. exact (fun H => Raw.min_elt_2 s.(sorted) H). Qed. Lemma min_elt_3 : min_elt s = None -> Empty s. - Proof. exact (fun H => min_elt_3 H). Qed. + Proof. exact (fun H => Raw.min_elt_3 H). Qed. Lemma max_elt_1 : max_elt s = Some x -> In x s. - Proof. exact (fun H => max_elt_1 H). Qed. - Lemma max_elt_2 : max_elt s = Some x -> In y s -> ~ X.lt x y. - Proof. exact (fun H => max_elt_2 s.(sorted) H). Qed. + Proof. exact (fun H => Raw.max_elt_1 H). Qed. + Lemma max_elt_2 : max_elt s = Some x -> In y s -> ~ E.lt x y. + Proof. exact (fun H => Raw.max_elt_2 s.(sorted) H). Qed. Lemma max_elt_3 : max_elt s = None -> Empty s. - Proof. exact (fun H => max_elt_3 H). Qed. + Proof. exact (fun H => Raw.max_elt_3 H). Qed. Lemma choose_1 : choose s = Some x -> In x s. - Proof. exact (fun H => choose_1 H). Qed. + Proof. exact (fun H => Raw.choose_1 H). Qed. Lemma choose_2 : choose s = None -> Empty s. - Proof. exact (fun H => choose_2 H). Qed. + Proof. exact (fun H => Raw.choose_2 H). Qed. Lemma eq_refl : eq s s. - Proof. exact (eq_refl s). Qed. + Proof. exact (Raw.eq_refl s). Qed. Lemma eq_sym : eq s s' -> eq s' s. - Proof. exact (@eq_sym s s'). Qed. + Proof. exact (@Raw.eq_sym s s'). Qed. Lemma eq_trans : eq s s' -> eq s' s'' -> eq s s''. - Proof. exact (@eq_trans s s' s''). Qed. + Proof. exact (@Raw.eq_trans s s' s''). Qed. Lemma lt_trans : lt s s' -> lt s' s'' -> lt s s''. - Proof. exact (@lt_trans s s' s''). Qed. + Proof. exact (@Raw.lt_trans s s' s''). Qed. Lemma lt_not_eq : lt s s' -> ~ eq s s'. - Proof. exact (lt_not_eq s.(sorted) s'.(sorted)). Qed. + Proof. exact (Raw.lt_not_eq s.(sorted) s'.(sorted)). Qed. Definition compare : Compare lt eq s s'. Proof. - elim (compare s.(sorted) s'.(sorted)); + elim (Raw.compare s.(sorted) s'.(sorted)); [ constructor 1 | constructor 2 | constructor 3 ]; auto. Defined. diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v index 130d31d1d..2b6017c5e 100644 --- a/theories/FSets/FSetWeakList.v +++ b/theories/FSets/FSetWeakList.v @@ -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 @@ -760,176 +761,175 @@ End Raw. Module Make (X: DecidableType) <: S with Module E := X. Module Raw := Raw X. - Import Raw. 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':t) := forall a : elt, In a s <-> In a s'. - Definition Subset (s s':t) := forall a : elt, In a s -> In a s'. - Definition Empty (s:t) := 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 Exists (P : elt -> Prop) (s : t) : Prop := exists x : elt, In x s /\ P x. - Definition mem (x : elt) (s : t) : bool := mem x s. - Definition add (x : elt)(s : t) : t := Build_slist (add_unique (unique s) x). - Definition remove (x : elt)(s : t) : t := Build_slist (remove_unique (unique s) x). - Definition singleton (x : elt) : t := Build_slist (singleton_unique x). + 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 (union_unique (unique s) (unique s')). + Build_slist (Raw.union_unique (unique s) (unique s')). Definition inter (s s' : t) : t := - Build_slist (inter_unique (unique s) (unique s')). + Build_slist (Raw.inter_unique (unique s) (unique s')). Definition diff (s s' : t) : t := - Build_slist (diff_unique (unique s) (unique s')). - Definition equal (s s' : t) : bool := equal s s'. - Definition subset (s s' : t) : bool := subset s s'. - Definition empty : t := Build_slist empty_unique. - Definition is_empty (s : t) : bool := is_empty s. - Definition elements (s : t) : list elt := elements s. - Definition choose (s:t) : option elt := choose s. - Definition fold (B : Set) (f : elt -> B -> B) (s : t) : B -> B := fold (B:=B) f s. - Definition cardinal (s : t) : nat := cardinal s. + Build_slist (Raw.diff_unique (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 (filter_unique (unique s) f). - Definition for_all (f : elt -> bool) (s : t) : bool := for_all f s. - Definition exists_ (f : elt -> bool) (s : t) : bool := exists_ f s. + 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 := partition f s in - (Build_slist (this:=fst p) (partition_unique_1 (unique s) f), - Build_slist (this:=snd p) (partition_unique_2 (unique s) f)). + 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. - Lemma In_1 : X.eq x y -> In x s -> In y s. - Proof. exact (fun H H' => In_eq H H'). Qed. + Lemma In_1 : E.eq x y -> In x s -> In y s. + Proof. exact (fun H H' => Raw.In_eq H H'). Qed. Lemma mem_1 : In x s -> mem x s = true. - Proof. exact (fun H => mem_1 H). Qed. + Proof. exact (fun H => Raw.mem_1 H). Qed. Lemma mem_2 : mem x s = true -> In x s. - Proof. exact (fun H => mem_2 H). Qed. + Proof. exact (fun H => Raw.mem_2 H). Qed. Lemma equal_1 : Equal s s' -> equal s s' = true. - Proof. exact (equal_1 s.(unique) s'.(unique)). Qed. + Proof. exact (Raw.equal_1 s.(unique) s'.(unique)). Qed. Lemma equal_2 : equal s s' = true -> Equal s s'. - Proof. exact (equal_2 s.(unique) s'.(unique)). Qed. + Proof. exact (Raw.equal_2 s.(unique) s'.(unique)). Qed. Lemma subset_1 : Subset s s' -> subset s s' = true. - Proof. exact (subset_1 s.(unique) s'.(unique)). Qed. + Proof. exact (Raw.subset_1 s.(unique) s'.(unique)). Qed. Lemma subset_2 : subset s s' = true -> Subset s s'. - Proof. exact (subset_2 s.(unique) s'.(unique)). Qed. + Proof. exact (Raw.subset_2 s.(unique) s'.(unique)). Qed. Lemma empty_1 : Empty empty. - Proof. exact empty_1. Qed. + Proof. exact Raw.empty_1. Qed. Lemma is_empty_1 : Empty s -> is_empty s = true. - Proof. exact (fun H => is_empty_1 H). Qed. + Proof. exact (fun H => Raw.is_empty_1 H). Qed. Lemma is_empty_2 : is_empty s = true -> Empty s. - Proof. exact (fun H => is_empty_2 H). Qed. + Proof. exact (fun H => Raw.is_empty_2 H). Qed. - Lemma add_1 : X.eq x y -> In y (add x s). - Proof. exact (fun H => add_1 s.(unique) H). Qed. + 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 => add_2 s.(unique) x H). Qed. - Lemma add_3 : ~ X.eq x y -> In y (add x s) -> In y s. - Proof. exact (fun H => add_3 s.(unique) H). Qed. - - Lemma remove_1 : X.eq x y -> ~ In y (remove x s). - Proof. exact (fun H => remove_1 s.(unique) H). Qed. - Lemma remove_2 : ~ X.eq x y -> In y s -> In y (remove x s). - Proof. exact (fun H H' => remove_2 s.(unique) H H'). Qed. + 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 => remove_3 s.(unique) H). Qed. + Proof. exact (fun H => Raw.remove_3 s.(unique) H). Qed. - Lemma singleton_1 : In y (singleton x) -> X.eq x y. - Proof. exact (fun H => singleton_1 H). Qed. - Lemma singleton_2 : X.eq x y -> In y (singleton x). - Proof. exact (fun H => singleton_2 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 => union_1 s.(unique) s'.(unique) H). Qed. + 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 => union_2 s.(unique) s'.(unique) H). Qed. + 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 => union_3 s.(unique) s'.(unique) H). Qed. + 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 => inter_1 s.(unique) s'.(unique) H). Qed. + 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 => inter_2 s.(unique) s'.(unique) H). Qed. + 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 => inter_3 s.(unique) s'.(unique) H). Qed. + 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 => diff_1 s.(unique) s'.(unique) H). Qed. + 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 => diff_2 s.(unique) s'.(unique) H). Qed. + 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 => diff_3 s.(unique) s'.(unique) H). Qed. + Proof. exact (fun H => Raw.diff_3 s.(unique) s'.(unique) H). Qed. 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 (fold_1 s.(unique)). Qed. + Proof. exact (Raw.fold_1 s.(unique)). Qed. Lemma cardinal_1 : cardinal s = length (elements s). - Proof. exact (cardinal_1 s.(unique)). Qed. + Proof. exact (Raw.cardinal_1 s.(unique)). Qed. Section Filter. Variable f : elt -> bool. - Lemma filter_1 : compat_bool X.eq f -> In x (filter f s) -> In x s. - Proof. exact (fun H => @filter_1 s x f). Qed. - Lemma filter_2 : compat_bool X.eq f -> In x (filter f s) -> f x = true. - Proof. exact (@filter_2 s x f). Qed. + 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 X.eq f -> In x s -> f x = true -> In x (filter f s). - Proof. exact (@filter_3 s x f). Qed. + 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 X.eq f -> + compat_bool E.eq f -> For_all (fun x => f x = true) s -> for_all f s = true. - Proof. exact (@for_all_1 s f). Qed. + Proof. exact (@Raw.for_all_1 s f). Qed. Lemma for_all_2 : - compat_bool X.eq f -> + compat_bool E.eq f -> for_all f s = true -> For_all (fun x => f x = true) s. - Proof. exact (@for_all_2 s f). Qed. + Proof. exact (@Raw.for_all_2 s f). Qed. Lemma exists_1 : - compat_bool X.eq f -> + compat_bool E.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true. - Proof. exact (@exists_1 s f). Qed. + Proof. exact (@Raw.exists_1 s f). Qed. Lemma exists_2 : - compat_bool X.eq f -> + compat_bool E.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s. - Proof. exact (@exists_2 s f). Qed. + Proof. exact (@Raw.exists_2 s f). Qed. Lemma partition_1 : - compat_bool X.eq f -> Equal (fst (partition f s)) (filter f s). - Proof. exact (@partition_1 s f). Qed. + 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 X.eq f -> + compat_bool E.eq f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). - Proof. exact (@partition_2 s f). Qed. + Proof. exact (@Raw.partition_2 s f). Qed. End Filter. - Lemma elements_1 : In x s -> InA X.eq x (elements s). - Proof. exact (fun H => elements_1 H). Qed. - Lemma elements_2 : InA X.eq x (elements s) -> In x s. - Proof. exact (fun H => elements_2 H). Qed. - Lemma elements_3 : NoDupA X.eq (elements s). - Proof. exact (elements_3 s.(unique)). Qed. + 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 => choose_1 H). Qed. + Proof. exact (fun H => Raw.choose_1 H). Qed. Lemma choose_2 : choose s = None -> Empty s. - Proof. exact (fun H => choose_2 H). Qed. + Proof. exact (fun H => Raw.choose_2 H). Qed. End Spec. diff --git a/theories/FSets/OrderedType.v b/theories/FSets/OrderedType.v index 0268b38c9..d989d8937 100644 --- a/theories/FSets/OrderedType.v +++ b/theories/FSets/OrderedType.v @@ -313,6 +313,8 @@ Ltac false_order := elimtype False; order. (* Specialization of resuts about lists modulo. *) +Section ForNotations. + Notation In:=(InA eq). Notation Inf:=(lelistA lt). Notation Sort:=(sort lt). @@ -346,6 +348,8 @@ Proof. exact (InfA_alt eq_refl eq_sym lt_trans lt_eq eq_lt). Qed. Lemma Sort_NoDup : forall l, Sort l -> NoDup l. Proof. exact (SortA_NoDupA eq_refl eq_sym lt_trans lt_not_eq lt_eq eq_lt) . Qed. +End ForNotations. + Hint Resolve ListIn_In Sort_NoDup Inf_lt. Hint Immediate In_eq Inf_lt. |