diff options
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FSetAVL.v | 43 | ||||
| -rw-r--r-- | theories/FSets/FSetEqProperties.v | 17 | ||||
| -rw-r--r-- | theories/FSets/FSetFacts.v | 90 | ||||
| -rw-r--r-- | theories/FSets/FSetProperties.v | 110 |
4 files changed, 215 insertions, 45 deletions
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index f12a92e07c..a49887bf09 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -2576,6 +2576,9 @@ Qed. End Raw. +Set Implicit Arguments. +Unset Strict Implicit. + (** * Encapsulation Now, in order to really provide a functor implementing [S], we @@ -2602,21 +2605,21 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Definition mem (x:elt)(s:t) : bool := Raw.mem x s. - Definition empty : t := Bbst _ Raw.empty_bst Raw.empty_avl. + Definition empty : t := Bbst Raw.empty_bst Raw.empty_avl. Definition is_empty (s:t) : bool := Raw.is_empty s. - Definition singleton (x:elt) : t := Bbst _ (Raw.singleton_bst x) (Raw.singleton_avl x). + Definition singleton (x:elt) : t := Bbst (Raw.singleton_bst x) (Raw.singleton_avl x). Definition add (x:elt)(s:t) : t := - Bbst _ (Raw.add_bst s x (is_bst s) (is_avl s)) - (Raw.add_avl s x (is_avl s)). + Bbst (Raw.add_bst s x (is_bst s) (is_avl s)) + (Raw.add_avl s x (is_avl s)). Definition remove (x:elt)(s:t) : t := - Bbst _ (Raw.remove_bst s x (is_bst s) (is_avl s)) - (Raw.remove_avl s x (is_avl s)). + Bbst (Raw.remove_bst s x (is_bst s) (is_avl s)) + (Raw.remove_avl s x (is_avl s)). Definition inter (s s':t) : t := - Bbst _ (Raw.inter_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) - (Raw.inter_avl _ _ (is_avl s) (is_avl s')). + Bbst (Raw.inter_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) + (Raw.inter_avl _ _ (is_avl s) (is_avl s')). Definition diff (s s':t) : t := - Bbst _ (Raw.diff_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) - (Raw.diff_avl _ _ (is_avl s) (is_avl s')). + Bbst (Raw.diff_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) + (Raw.diff_avl _ _ (is_avl s) (is_avl 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. @@ -2624,26 +2627,26 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Definition fold (B : Type) (f : elt -> B -> B) (s:t) : B -> B := Raw.fold f s. Definition cardinal (s:t) : nat := Raw.cardinal s. Definition filter (f : elt -> bool) (s:t) : t := - Bbst _ (Raw.filter_bst f _ (is_bst s) (is_avl s)) - (Raw.filter_avl f _ (is_avl s)). + Bbst (Raw.filter_bst f _ (is_bst s) (is_avl s)) + (Raw.filter_avl f _ (is_avl s)). 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 - (Bbst (fst p) (Raw.partition_bst_1 f _ (is_bst s) (is_avl s)) - (Raw.partition_avl_1 f _ (is_avl s)), - Bbst (snd p) (Raw.partition_bst_2 f _ (is_bst s) (is_avl s)) - (Raw.partition_avl_2 f _ (is_avl s))). + (Bbst (Raw.partition_bst_1 f _ (is_bst s) (is_avl s)) + (Raw.partition_avl_1 f _ (is_avl s)), + Bbst (Raw.partition_bst_2 f _ (is_bst s) (is_avl s)) + (Raw.partition_avl_2 f _ (is_avl s))). Definition union (s s':t) : t := let (u,p) := Raw.union _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s') in let (b,p) := p in let (a,_) := p in - Bbst u b a. + Bbst b a. Definition union' (s s' : t) : t := - Bbst _ (Raw.union'_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) - (Raw.union'_avl _ _ (is_avl s) (is_avl s')). + Bbst (Raw.union'_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) + (Raw.union'_avl _ _ (is_avl s) (is_avl s')). Definition equal (s s': t) : bool := if Raw.equal _ _ (is_bst s) (is_bst s') then true else false. Definition equal' (s s':t) : bool := Raw.equal' s s'. @@ -2817,7 +2820,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Qed. Lemma fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A), - fold A f s i = fold_left (fun a e => f e a) (elements s) i. + fold f s i = fold_left (fun a e => f e a) (elements s) i. Proof. unfold fold, elements; intros; apply Raw.fold_1; auto. Qed. diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index 4645a6bbc6..a970c092dc 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -665,6 +665,23 @@ Proof. auto. Qed. +Lemma filter_add_1 : forall s x, f x = true -> + filter f (add x s) [=] add x (filter f s). +Proof. +red; intros; set_iff; do 2 (rewrite filter_iff; auto); set_iff. +intuition. +rewrite <- H; apply Comp; auto. +Qed. + +Lemma filter_add_2 : forall s x, f x = false -> + filter f (add x s) [=] filter f s. +Proof. +red; intros; do 2 (rewrite filter_iff; auto); set_iff. +intuition. +assert (f x = f a) by (apply Comp; auto). +rewrite H in H1; rewrite H2 in H1; discriminate. +Qed. + Lemma add_filter_1 : forall s s' x, f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')). Proof. diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index 6874ceb33e..4c1c51c497 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -287,19 +287,17 @@ End BoolSpec. (** * [E.eq] and [Equal] are setoid equalities *) -Definition E_ST : Setoid_Theory elt E.eq. -Proof. -constructor; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans]. -Qed. - -Add Setoid elt E.eq E_ST as EltSetoid. - -Definition Equal_ST : Setoid_Theory t Equal. -Proof. -constructor; [apply eq_refl | apply eq_sym | apply eq_trans]. -Qed. - -Add Setoid t Equal Equal_ST as EqualSetoid. +Add Relation elt E.eq + reflexivity proved by E.eq_refl + symmetry proved by E.eq_sym + transitivity proved by E.eq_trans + as EltSetoid. + +Add Relation t Equal + reflexivity proved by eq_refl + symmetry proved by eq_sym + transitivity proved by eq_trans + as EqualSetoid. Add Morphism In with signature E.eq ==> Equal ==> iff as In_m. Proof. @@ -396,6 +394,65 @@ rewrite H in H1; rewrite H0 in H1; intuition. rewrite H in H1; rewrite H0 in H1; intuition. Qed. + +(* [Subset] is a setoid order *) + +Lemma Subset_refl : forall s, s[<=]s. +Proof. red; auto. Qed. + +Lemma Subset_trans : forall s s' s'', s[<=]s'->s'[<=]s''->s[<=]s''. +Proof. unfold Subset; eauto. Qed. + +Add Relation t Subset + reflexivity proved by Subset_refl + transitivity proved by Subset_trans + as SubsetSetoid. + +Add Morphism In with signature E.eq ==> Subset ++> impl as In_s_m. +Proof. +unfold Subset, impl; intros; eauto. +Qed. + +Add Morphism Empty with signature Subset --> impl as Empty_s_m. +Proof. +unfold Subset, Empty, impl; firstorder. +Qed. + +Add Morphism add with signature E.eq ==> Subset ++> Subset as add_s_m. +Proof. +unfold Subset; intros x y H s s' H0 a. +do 2 rewrite add_iff; rewrite H; intuition. +Qed. + +Add Morphism remove with signature E.eq ==> Subset ++> Subset as remove_s_m. +Proof. +unfold Subset; intros x y H s s' H0 a. +do 2 rewrite remove_iff; rewrite H; intuition. +Qed. + +Add Morphism union with signature Subset ++> Subset ++> Subset as union_s_m. +Proof. +unfold Equal; intros s s' H s'' s''' H0 a. +do 2 rewrite union_iff; intuition. +Qed. + +Add Morphism inter with signature Subset ++> Subset ++> Subset as inter_s_m. +Proof. +unfold Equal; intros s s' H s'' s''' H0 a. +do 2 rewrite inter_iff; intuition. +Qed. + +Add Morphism diff with signature Subset ++> Subset --> Subset as diff_s_m. +Proof. +unfold Subset; intros s s' H s'' s''' H0 a. +do 2 rewrite diff_iff; intuition. +Qed. + +Add Morphism Subset with signature Subset --> Subset ++> impl as Subset_s_m. +Proof. +unfold Subset, impl; auto. +Qed. + (* [fold], [filter], [for_all], [exists_] and [partition] cannot be proved morphism without additional hypothesis on [f]. For instance: *) @@ -405,6 +462,12 @@ Proof. unfold Equal; intros; repeat rewrite filter_iff; auto; rewrite H0; tauto. Qed. +Lemma filter_subset : forall f, compat_bool E.eq f -> + forall s s', s[<=]s' -> filter f s [<=] filter f s'. +Proof. +unfold Subset; intros; rewrite filter_iff in *; intuition. +Qed. + (* For [elements], [min_elt], [max_elt] and [choose], we would need setoid structures on [list elt] and [option elt]. *) @@ -412,4 +475,5 @@ Qed. Add Morphism cardinal ; cardinal_m. *) + End Facts. diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 7b25e8d61d..3b8d0d708a 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -51,21 +51,21 @@ Module Properties (M: S). Lemma equal_refl : forall s, s[=]s. Proof. - unfold Equal; intuition. + exact eq_refl. Qed. Lemma equal_sym : forall s s', s[=]s' -> s'[=]s. Proof. - unfold Equal; intros. - rewrite H; intuition. + exact eq_sym. Qed. Lemma equal_trans : forall s1 s2 s3, s1[=]s2 -> s2[=]s3 -> s1[=]s3. Proof. - unfold Equal; intros. - rewrite H; exact (H0 a). + exact eq_trans. Qed. + Hint Immediate equal_refl equal_sym : set. + Variable s s' s'' s1 s2 s3 : t. Variable x x' : elt. @@ -73,22 +73,24 @@ Module Properties (M: S). Lemma subset_refl : s[<=]s. Proof. - unfold Subset; intuition. + apply Subset_refl. Qed. - Lemma subset_antisym : s[<=]s' -> s'[<=]s -> s[=]s'. + Lemma subset_trans : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3. Proof. - unfold Subset, Equal; intuition. + apply Subset_trans. Qed. - Lemma subset_trans : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3. + Lemma subset_antisym : s[<=]s' -> s'[<=]s -> s[=]s'. Proof. - unfold Subset; intuition. + unfold Subset, Equal; intuition. Qed. + Hint Immediate subset_refl : set. + Lemma subset_equal : s[=]s' -> s[<=]s'. Proof. - unfold Subset, Equal; firstorder. + unfold Subset, Equal; intros; rewrite <- H; auto. Qed. Lemma subset_empty : empty[<=]s. @@ -119,7 +121,7 @@ Module Properties (M: S). Lemma in_subset : In x s1 -> s1[<=]s2 -> In x s2. Proof. - unfold Subset; intuition. + intros; rewrite <- H0; auto. Qed. Lemma double_inclusion : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1. @@ -223,6 +225,21 @@ Module Properties (M: S). unfold Equal; intros; set_iff; tauto. Qed. + Lemma union_remove_add_1 : + union (remove x s) (add x s') [=] union (add x s) (remove x s'). + Proof. + unfold Equal; intros; set_iff. + destruct (ME.eq_dec x a); intuition. + Qed. + + Lemma union_remove_add_2 : In x s -> + union (remove x s) (add x s') [=] union s s'. + Proof. + unfold Equal; intros; set_iff. + destruct (ME.eq_dec x a); intuition. + left; eauto. + Qed. + Lemma union_subset_1 : s [<=] union s s'. Proof. unfold Subset; intuition. @@ -892,4 +909,73 @@ Module Properties (M: S). Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2. + (** Two other induction principles on sets: we can be more restrictive + on the element we add at each step. *) + + Definition Above x s := forall y, In y s -> E.lt y x. + Definition Below x s := forall y, In y s -> E.lt x y. + + Lemma set_induction_max : + forall P : t -> Type, + (forall s : t, Empty s -> P s) -> + (forall s s', P s -> forall x, Above x s -> Add x s s' -> P s') -> + forall s : t, P s. + Proof. + intros. + remember (cardinal s) as n; revert s Heqn; induction n. + intros. + apply X. + apply cardinal_inv_1; auto. + + intros. + case_eq (max_elt s); intros. + apply X0 with (remove e s) e. + apply IHn. + assert (S (cardinal (remove e s)) = S n). + rewrite Heqn. + apply remove_cardinal_1; auto. + inversion H0; auto. + red; intros. + rewrite remove_iff in H0; destruct H0. + generalize (@max_elt_2 s e y H H0). + intros. + destruct (E.compare y e); intuition. + elim H1; auto. + apply Add_remove; auto. + + rewrite (cardinal_1 (max_elt_3 H)) in Heqn; inversion Heqn. + Qed. + + Lemma set_induction_min : + forall P : t -> Type, + (forall s : t, Empty s -> P s) -> + (forall s s', P s -> forall x, Below x s -> Add x s s' -> P s') -> + forall s : t, P s. + Proof. + intros. + remember (cardinal s) as n; revert s Heqn; induction n. + intros. + apply X. + apply cardinal_inv_1; auto. + + intros. + case_eq (min_elt s); intros. + apply X0 with (remove e s) e. + apply IHn. + assert (S (cardinal (remove e s)) = S n). + rewrite Heqn. + apply remove_cardinal_1; auto. + inversion H0; auto. + red; intros. + rewrite remove_iff in H0; destruct H0. + generalize (@min_elt_2 s e y H H0). + intros. + destruct (E.compare y e); intuition. + elim H1; auto. + apply Add_remove; auto. + + rewrite (cardinal_1 (min_elt_3 H)) in Heqn; inversion Heqn. + Qed. + + End Properties. |