summaryrefslogtreecommitdiff
path: root/theories/FSets/FSetProperties.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FSetProperties.v')
-rw-r--r--theories/FSets/FSetProperties.v260
1 files changed, 74 insertions, 186 deletions
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 23843084..6e93a546 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetProperties.v 8639 2006-03-16 19:21:55Z letouzey $ *)
+(* $Id: FSetProperties.v 8853 2006-05-23 18:17:38Z herbelin $ *)
(** * Finite sets library *)
@@ -21,49 +21,13 @@ Require Import FSetFacts.
Set Implicit Arguments.
Unset Strict Implicit.
-Section Misc.
-Variable A B : Set.
-Variable eqA : A -> A -> Prop.
-Variable eqB : B -> B -> Prop.
-
-(** Two-argument functions that allow to reorder its arguments. *)
-Definition transpose (f : A -> B -> B) :=
- forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)).
-
-(** Compatibility of a two-argument function with respect to two equalities. *)
-Definition compat_op (f : A -> B -> B) :=
- forall (x x' : A) (y y' : B), eqA x x' -> eqB y y' -> eqB (f x y) (f x' y').
-
-(** Compatibility of a function upon natural numbers. *)
-Definition compat_nat (f : A -> nat) :=
- forall x x' : A, eqA x x' -> f x = f x'.
-
-End Misc.
Hint Unfold transpose compat_op compat_nat.
-
Hint Extern 1 (Setoid_Theory _ _) => constructor; congruence.
-Ltac trans_st x := match goal with
- | H : Setoid_Theory _ ?eqA |- ?eqA _ _ =>
- apply (Seq_trans _ _ H) with x; auto
- end.
-
-Ltac sym_st := match goal with
- | H : Setoid_Theory _ ?eqA |- ?eqA _ _ =>
- apply (Seq_sym _ _ H); auto
- end.
-
-Ltac refl_st := match goal with
- | H : Setoid_Theory _ ?eqA |- ?eqA _ _ =>
- apply (Seq_refl _ _ H); auto
- end.
-
-Definition gen_st : forall A : Set, Setoid_Theory _ (@eq A).
-Proof. auto. Qed.
-
Module Properties (M: S).
- Module ME := OrderedTypeFacts M.E.
- Import ME.
+ Module ME:=OrderedTypeFacts(M.E).
+ Import ME. (* for ME.eq_dec *)
+ Import M.E.
Import M.
Import Logic. (* to unmask [eq] *)
Import Peano. (* to unmask [lt] *)
@@ -82,26 +46,29 @@ Module Properties (M: S).
Qed.
Section BasicProperties.
- Variable s s' s'' s1 s2 s3 : t.
- Variable x : elt.
(** properties of [Equal] *)
- Lemma equal_refl : s[=]s.
+ Lemma equal_refl : forall s, s[=]s.
Proof.
- apply eq_refl.
+ unfold Equal; intuition.
Qed.
- Lemma equal_sym : s[=]s' -> s'[=]s.
+ Lemma equal_sym : forall s s', s[=]s' -> s'[=]s.
Proof.
- apply eq_sym.
+ unfold Equal; intros.
+ rewrite H; intuition.
Qed.
- Lemma equal_trans : s1[=]s2 -> s2[=]s3 -> s1[=]s3.
+ Lemma equal_trans : forall s1 s2 s3, s1[=]s2 -> s2[=]s3 -> s1[=]s3.
Proof.
- intros; apply eq_trans with s2; auto.
+ unfold Equal; intros.
+ rewrite H; exact (H0 a).
Qed.
+ Variable s s' s'' s1 s2 s3 : t.
+ Variable x x' : elt.
+
(** properties of [Subset] *)
Lemma subset_refl : s[<=]s.
@@ -154,6 +121,11 @@ Module Properties (M: S).
Proof.
unfold Subset; intuition.
Qed.
+
+ Lemma double_inclusion : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1.
+ Proof.
+ unfold Subset, Equal; split; intros; intuition; generalize (H a); intuition.
+ Qed.
(** properties of [empty] *)
@@ -174,6 +146,11 @@ Module Properties (M: S).
unfold Equal; intros; set_iff; intuition.
rewrite <- H1; auto.
Qed.
+
+ Lemma add_add : add x (add x' s) [=] add x' (add x s).
+ Proof.
+ unfold Equal; intros; set_iff; tauto.
+ Qed.
(** properties of [remove] *)
@@ -185,7 +162,7 @@ Module Properties (M: S).
Lemma Equal_remove : s[=]s' -> remove x s [=] remove x s'.
Proof.
- intros; rewrite H; apply eq_refl.
+ intros; rewrite H; apply equal_refl.
Qed.
(** properties of [add] and [remove] *)
@@ -223,12 +200,12 @@ Module Properties (M: S).
Lemma union_equal_1 : s[=]s' -> union s s'' [=] union s' s''.
Proof.
- intros; rewrite H; apply eq_refl.
+ intros; rewrite H; apply equal_refl.
Qed.
Lemma union_equal_2 : s'[=]s'' -> union s s' [=] union s s''.
Proof.
- intros; rewrite H; apply eq_refl.
+ intros; rewrite H; apply equal_refl.
Qed.
Lemma union_assoc : union (union s s') s'' [=] union s (union s' s'').
@@ -261,6 +238,16 @@ Module Properties (M: S).
unfold Subset; intros H H0 a; set_iff; intuition.
Qed.
+ Lemma union_subset_4 : s[<=]s' -> union s s'' [<=] union s' s''.
+ Proof.
+ unfold Subset; intros H a; set_iff; intuition.
+ Qed.
+
+ Lemma union_subset_5 : s[<=]s' -> union s'' s [<=] union s'' s'.
+ Proof.
+ unfold Subset; intros H a; set_iff; intuition.
+ Qed.
+
Lemma empty_union_1 : Empty s -> union s s' [=] s'.
Proof.
unfold Equal, Empty; intros; set_iff; firstorder.
@@ -290,12 +277,12 @@ Module Properties (M: S).
Lemma inter_equal_1 : s[=]s' -> inter s s'' [=] inter s' s''.
Proof.
- intros; rewrite H; apply eq_refl.
+ intros; rewrite H; apply equal_refl.
Qed.
Lemma inter_equal_2 : s'[=]s'' -> inter s s' [=] inter s s''.
Proof.
- intros; rewrite H; apply eq_refl.
+ intros; rewrite H; apply equal_refl.
Qed.
Lemma inter_assoc : inter (inter s s') s'' [=] inter s (inter s' s'').
@@ -447,140 +434,14 @@ Module Properties (M: S).
empty_diff_2 union_Add inter_Add union_Equal inter_Add_2 not_in_union
inter_subset_1 inter_subset_2 inter_subset_3 diff_subset diff_subset_equal
remove_diff_singleton diff_inter_empty diff_inter_all Add_add Add_remove
- Equal_remove : set.
-
- Notation NoDup := (NoDupA E.eq).
- Notation EqList := (eqlistA E.eq).
-
- Section NoDupA_Remove.
-
- Let ListAdd x l l' := forall y : elt, ME.In y l' <-> E.eq x y \/ ME.In y l.
-
- Lemma removeA_add :
- forall s s' x x', NoDup s -> NoDup (x' :: s') ->
- ~ E.eq x x' -> ~ ME.In x s ->
- ListAdd x s (x' :: s') -> ListAdd x (removeA eq_dec x' s) s'.
- Proof.
- unfold ListAdd; intros.
- inversion_clear H0.
- rewrite removeA_InA; auto; [apply E.eq_trans|].
- split; intros.
- destruct (eq_dec x y); auto; intros.
- right; split; auto.
- destruct (H3 y); clear H3.
- destruct H6; intuition.
- swap H4; apply In_eq with y; auto.
- destruct H0.
- assert (ME.In y (x' :: s')) by rewrite H3; auto.
- inversion_clear H6; auto.
- elim H1; apply E.eq_trans with y; auto.
- destruct H0.
- assert (ME.In y (x' :: s')) by rewrite H3; auto.
- inversion_clear H7; auto.
- elim H6; auto.
- Qed.
-
- Variables (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA).
- Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
- Variables (i:A).
-
- Lemma removeA_fold_right_0 :
- forall s x, NoDup s -> ~ME.In x s ->
- eqA (fold_right f i s) (fold_right f i (removeA eq_dec x s)).
- Proof.
- simple induction s; simpl; intros.
- refl_st.
- inversion_clear H0.
- destruct (eq_dec x a); simpl; intros.
- absurd_hyp e; auto.
- apply Comp; auto.
- Qed.
-
- Lemma removeA_fold_right :
- forall s x, NoDup s -> ME.In x s ->
- eqA (fold_right f i s) (f x (fold_right f i (removeA eq_dec x s))).
- Proof.
- simple induction s; simpl.
- inversion_clear 2.
- intros.
- inversion_clear H0.
- destruct (eq_dec x a); simpl; intros.
- apply Comp; auto.
- apply removeA_fold_right_0; auto.
- swap H2; apply ME.In_eq with x; auto.
- inversion_clear H1.
- destruct n; auto.
- trans_st (f a (f x (fold_right f i (removeA eq_dec x l)))).
- Qed.
-
- Lemma fold_right_equal :
- forall s s', NoDup s -> NoDup s' ->
- EqList s s' -> eqA (fold_right f i s) (fold_right f i s').
- Proof.
- simple induction s.
- destruct s'; simpl.
- intros; refl_st; auto.
- unfold eqlistA; intros.
- destruct (H1 t0).
- assert (X : ME.In t0 nil); auto; inversion X.
- intros x l Hrec s' N N' E; simpl in *.
- trans_st (f x (fold_right f i (removeA eq_dec x s'))).
- apply Comp; auto.
- apply Hrec; auto.
- inversion N; auto.
- apply removeA_NoDupA; auto; apply E.eq_trans.
- apply removeA_eqlistA; auto; [apply E.eq_trans|].
- inversion_clear N; auto.
- sym_st.
- apply removeA_fold_right; auto.
- unfold eqlistA in E.
- rewrite <- E; auto.
- Qed.
-
- Lemma fold_right_add :
- forall s' s x, NoDup s -> NoDup s' -> ~ ME.In x s ->
- ListAdd x s s' -> eqA (fold_right f i s') (f x (fold_right f i s)).
- Proof.
- simple induction s'.
- unfold ListAdd; intros.
- destruct (H2 x); clear H2.
- assert (X : ME.In x nil); auto; inversion X.
- intros x' l' Hrec s x N N' IN EQ; simpl.
- (* if x=x' *)
- destruct (eq_dec x x').
- apply Comp; auto.
- apply fold_right_equal; auto.
- inversion_clear N'; trivial.
- unfold eqlistA; unfold ListAdd in EQ; intros.
- destruct (EQ x0); clear EQ.
- split; intros.
- destruct H; auto.
- inversion_clear N'.
- destruct H2; apply In_eq with x0; auto; order.
- assert (X:ME.In x0 (x' :: l')); auto; inversion_clear X; auto.
- destruct IN; apply In_eq with x0; auto; order.
- (* else x<>x' *)
- trans_st (f x' (f x (fold_right f i (removeA eq_dec x' s)))).
- apply Comp; auto.
- apply Hrec; auto.
- apply removeA_NoDupA; auto; apply E.eq_trans.
- inversion_clear N'; auto.
- rewrite removeA_InA; auto; [apply E.eq_trans|intuition].
- apply removeA_add; auto.
- trans_st (f x (f x' (fold_right f i (removeA eq_dec x' s)))).
- apply Comp; auto.
- sym_st.
- apply removeA_fold_right; auto.
- destruct (EQ x').
- destruct H; auto; destruct n; auto.
- Qed.
-
- End NoDupA_Remove.
+ Equal_remove add_add : set.
(** * Alternative (weaker) specifications for [fold] *)
Section Old_Spec_Now_Properties.
+ Notation NoDup := (NoDupA E.eq).
+
(** When [FSets] was first designed, the order in which Ocaml's [Set.fold]
takes the set elements was unspecified. This specification reflects this fact:
*)
@@ -629,7 +490,9 @@ Module Properties (M: S).
intros; destruct (fold_0 s i f) as (l,(Hl, (Hl1, Hl2)));
destruct (fold_0 s' i f) as (l',(Hl', (Hl'1, Hl'2))).
rewrite Hl2; rewrite Hl'2; clear Hl2 Hl'2.
- apply fold_right_add with (eqA := eqA); auto.
+ apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto.
+ eauto.
+ exact eq_dec.
rewrite <- Hl1; auto.
intros; rewrite <- Hl1; rewrite <- Hl'1; auto.
Qed.
@@ -897,8 +760,8 @@ Module Properties (M: S).
forall s p, fold (fun _ => S) s p = fold (fun _ => S) s 0 + p.
Proof.
assert (st := gen_st nat).
- assert (fe : compat_op E.eq (@eq _) (fun _ => S)) by unfold compat_op; auto.
- assert (fp : transpose (@eq _) (fun _:elt => S)) by unfold transpose; auto.
+ assert (fe : compat_op E.eq (@eq _) (fun _ => S)) by (unfold compat_op; auto).
+ assert (fp : transpose (@eq _) (fun _:elt => S)) by (unfold transpose; auto).
intros s p; pattern s; apply set_induction; clear s; intros.
rewrite (fold_1 st p (fun _ => S) H).
rewrite (fold_1 st 0 (fun _ => S) H); trivial.
@@ -956,7 +819,23 @@ Module Properties (M: S).
rewrite (inter_subset_equal H); auto with arith.
Qed.
- Lemma union_inter_cardinal :
+ Lemma subset_cardinal_lt :
+ forall s s' x, s[<=]s' -> In x s' -> ~In x s -> cardinal s < cardinal s'.
+ Proof.
+ intros.
+ rewrite <- (diff_inter_cardinal s' s).
+ rewrite (inter_sym s' s).
+ rewrite (inter_subset_equal H).
+ generalize (@cardinal_inv_1 (diff s' s)).
+ destruct (cardinal (diff s' s)).
+ intro H2; destruct (H2 (refl_equal _) x).
+ set_iff; auto.
+ intros _.
+ change (0 + cardinal s < S n + cardinal s).
+ apply Plus.plus_lt_le_compat; auto with arith.
+ Qed.
+
+ Theorem union_inter_cardinal :
forall s s', cardinal (union s s') + cardinal (inter s s') = cardinal s + cardinal s' .
Proof.
intros.
@@ -965,6 +844,15 @@ Module Properties (M: S).
apply fold_union_inter with (eqA:=@eq nat); auto.
Qed.
+ Lemma union_cardinal_inter :
+ forall s s', cardinal (union s s') = cardinal s + cardinal s' - cardinal (inter s s').
+ Proof.
+ intros.
+ rewrite <- union_inter_cardinal.
+ rewrite Plus.plus_comm.
+ auto with arith.
+ Qed.
+
Lemma union_cardinal_le :
forall s s', cardinal (union s s') <= cardinal s + cardinal s'.
Proof.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 19:41:23 +0000