diff options
| -rw-r--r-- | Makefile.common | 10 | ||||
| -rw-r--r-- | theories/FSets/FMapFacts.v | 373 | ||||
| -rw-r--r-- | theories/FSets/FMapInterface.v | 84 | ||||
| -rw-r--r-- | theories/FSets/FMapList.v | 7 | ||||
| -rw-r--r-- | theories/FSets/FMapWeak.v | 15 | ||||
| -rw-r--r-- | theories/FSets/FMapWeakFacts.v | 763 | ||||
| -rw-r--r-- | theories/FSets/FMapWeakInterface.v | 209 | ||||
| -rw-r--r-- | theories/FSets/FMapWeakList.v | 13 | ||||
| -rw-r--r-- | theories/FSets/FMaps.v | 6 | ||||
| -rw-r--r-- | theories/FSets/FSetDecide.v | 21 | ||||
| -rw-r--r-- | theories/FSets/FSetEqProperties.v | 920 | ||||
| -rw-r--r-- | theories/FSets/FSetFacts.v | 489 | ||||
| -rw-r--r-- | theories/FSets/FSetInterface.v | 211 | ||||
| -rw-r--r-- | theories/FSets/FSetProperties.v | 759 | ||||
| -rw-r--r-- | theories/FSets/FSetToFiniteSet.v | 18 | ||||
| -rw-r--r-- | theories/FSets/FSetWeak.v | 16 | ||||
| -rw-r--r-- | theories/FSets/FSetWeakEqProperties.v | 934 | ||||
| -rw-r--r-- | theories/FSets/FSetWeakFacts.v | 494 | ||||
| -rw-r--r-- | theories/FSets/FSetWeakInterface.v | 264 | ||||
| -rw-r--r-- | theories/FSets/FSetWeakList.v | 4 | ||||
| -rw-r--r-- | theories/FSets/FSetWeakProperties.v | 771 | ||||
| -rw-r--r-- | theories/FSets/FSets.v | 3 |
22 files changed, 2637 insertions, 3747 deletions
diff --git a/Makefile.common b/Makefile.common index 4a60b251a..3ba5fcede 100644 --- a/Makefile.common +++ b/Makefile.common @@ -563,16 +563,12 @@ FSETSBASEVO:=\ theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo \ theories/FSets/FSetBridge.vo theories/FSets/FSetFacts.vo \ theories/FSets/FSetProperties.vo theories/FSets/FSetEqProperties.vo \ - theories/FSets/FSets.vo theories/FSets/FSetWeakProperties.vo \ - theories/FSets/FSetWeakInterface.vo theories/FSets/FSetWeakList.vo \ - theories/FSets/FSetWeakFacts.vo theories/FSets/FSetWeak.vo \ + theories/FSets/FSets.vo theories/FSets/FSetWeakList.vo \ theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo \ theories/FSets/FMaps.vo theories/FSets/FMapFacts.vo \ - theories/FSets/FMapWeakFacts.vo \ - theories/FSets/FMapWeakInterface.vo theories/FSets/FMapWeakList.vo \ - theories/FSets/FMapWeak.vo theories/FSets/FMapPositive.vo \ + theories/FSets/FMapWeakList.vo theories/FSets/FMapPositive.vo \ theories/FSets/FMapIntMap.vo theories/FSets/FSetToFiniteSet.vo \ - theories/FSets/FSetDecide.vo theories/FSets/FSetWeakEqProperties.vo + theories/FSets/FSetDecide.vo FSETS_basic:= diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index f696ff075..3a3698239 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -15,18 +15,17 @@ different styles: equivalence and boolean equalities. *) -Require Import Bool. -Require Import OrderedType. +Require Import Bool DecidableType DecidableTypeEx OrderedType. Require Export FMapInterface. Set Implicit Arguments. Unset Strict Implicit. -Module Facts (M: S). -Module ME := OrderedTypeFacts M.E. -Import ME. -Import M. -Import Logic. (* to unmask [eq] *) -Import Peano. (* to unmask [lt] *) +(** * Facts about weak maps *) + +Module WFacts (E:DecidableType)(Import M:WSfun E). + +Notation eq_dec := E.eq_dec. +Definition eqb x y := if eq_dec x y then true else false. Lemma MapsTo_fun : forall (elt:Set) m x (e e':elt), MapsTo x e m -> MapsTo x e' m -> e=e'. @@ -36,7 +35,7 @@ generalize (find_1 H) (find_1 H0); clear H H0. intros; rewrite H in H0; injection H0; auto. Qed. -(** * Specifications written using equivalences *) +(** ** Specifications written using equivalences *) Section IffSpec. Variable elt elt' elt'': Set. @@ -230,7 +229,7 @@ destruct (mapi_1 f H) as (y,(H0,H1)). exists (f y a); auto. Qed. -(* Unfortunately, we don't have simple equivalences for [mapi] +(** Unfortunately, we don't have simple equivalences for [mapi] and [MapsTo]. The only correct one needs compatibility of [f]. *) Lemma mapi_inv : forall m x b (f : key -> elt -> elt'), @@ -287,7 +286,7 @@ Ltac map_iff := rewrite map_mapsto_iff || rewrite map_in_iff || rewrite mapi_in_iff)). -(** * Specifications written using boolean predicates *) +(** ** Specifications written using boolean predicates *) Section BoolSpec. @@ -494,7 +493,7 @@ Proof. intros. case_eq (find x m); intros. rewrite <- H0. -apply map2_1; auto. +apply map2_1; auto with map. left; exists e; auto with map. case_eq (find x m'); intros. rewrite <- H0; rewrite <- H1. @@ -514,21 +513,18 @@ Proof. intros. assert (forall e, find x m = Some e <-> InA (eq_key_elt (elt:=elt)) (x,e) (elements m)). intros; rewrite <- find_mapsto_iff; apply elements_mapsto_iff. -assert (NoDupA (eq_key (elt:=elt)) (elements m)). - apply SortA_NoDupA with (lt_key (elt:=elt)); unfold eq_key, lt_key; intuition eauto. - destruct y; simpl in *. - apply (E.lt_not_eq H0 H1). - exact (elements_3 m). +assert (H0:=elements_3w m). generalize (fun e => @findA_NoDupA _ _ _ E.eq_sym E.eq_trans eq_dec (elements m) x e H0). -unfold eqb. -destruct (find x m); destruct (findA (fun y : E.t => if eq_dec x y then true else false) (elements m)); +fold (eqb x). +destruct (find x m); destruct (findA (eqb x) (elements m)); simpl; auto; intros. symmetry; rewrite <- H1; rewrite <- H; auto. symmetry; rewrite <- H1; rewrite <- H; auto. rewrite H; rewrite H1; auto. Qed. -Lemma elements_b : forall m x, mem x m = existsb (fun p => eqb x (fst p)) (elements m). +Lemma elements_b : forall m x, + mem x m = existsb (fun p => eqb x (fst p)) (elements m). Proof. intros. generalize (mem_in_iff m x)(elements_in_iff m x) @@ -554,31 +550,34 @@ Qed. End BoolSpec. +End WFacts. + +(** * Same facts for full maps *) + +Module Facts (M:S). + Module D := OT_as_DT M.E. + Include WFacts D M. End Facts. -Module Properties (M: S). - Module F:=Facts M. - Import F. - Module O:=KeyOrderedType M.E. - Import O. +(** * Additional Properties for weak maps + + Results about [fold], [elements], induction principles... +*) + +Module WProperties (E:DecidableType)(M:WSfun E). + Module Import F:=WFacts E M. Import M. Section Elt. Variable elt:Set. - Notation eqke := (@eqke elt). - Notation eqk := (@eqk elt). - Notation ltk := (@ltk elt). - Definition cardinal (m:t elt) := length (elements m). Definition Equal (m m':t elt) := forall y, find y m = find y m'. Definition Add x (e:elt) m m' := forall y, find y m' = find y (add x e m). - Definition Above x (m:t elt) := forall y, In y m -> E.lt y x. - Definition Below x (m:t elt) := forall y, In y m -> E.lt x y. - - Section Elements. + Notation eqke := (@eq_key_elt elt). + Notation eqk := (@eq_key elt). Lemma elements_Empty : forall m:t elt, Empty m <-> elements m = nil. Proof. @@ -599,6 +598,208 @@ Module Properties (M: S). rewrite H in H0; destruct H0 as (_,H0); inversion H0. Qed. + Lemma fold_Empty : forall m (A:Set)(f:key->elt->A->A)(i:A), + Empty m -> fold f m i = i. + Proof. + intros. + rewrite fold_1. + rewrite elements_Empty in H; rewrite H; simpl; auto. + Qed. + + Lemma NoDupA_eqk_eqke : forall l, NoDupA eqk l -> NoDupA eqke l. + Proof. + induction 1; auto. + constructor; auto. + contradict H. + destruct x as (x,y). + rewrite InA_alt in *; destruct H as ((a,b),((H1,H2),H3)); simpl in *. + exists (a,b); auto. + Qed. + + Lemma fold_Equal : forall m1 m2 (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) + (f:key->elt->A->A)(i:A), + compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> + transpose eqA (fun y => f (fst y) (snd y)) -> + Equal m1 m2 -> + eqA (fold f m1 i) (fold f m2 i). + Proof. + assert (eqke_refl : forall p, eqke p p). + red; auto. + assert (eqke_sym : forall p p', eqke p p' -> eqke p' p). + intros (x1,x2) (y1,y2); unfold eq_key_elt; simpl; intuition. + assert (eqke_trans : forall p p' p'', eqke p p' -> eqke p' p'' -> eqke p p''). + intros (x1,x2) (y1,y2) (z1,z2); unfold eq_key_elt; simpl. + intuition; eauto; congruence. + intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right. + apply fold_right_equivlistA with (eqA:=eqke) (eqB:=eqA); auto. + apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w. + apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w. + red; intros. + do 2 rewrite InA_rev. + destruct x; do 2 rewrite <- elements_mapsto_iff. + do 2 rewrite find_mapsto_iff. + rewrite H1; split; auto. + Qed. + + Lemma fold_Add : forall m1 m2 x e (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) + (f:key->elt->A->A)(i:A), + compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> + transpose eqA (fun y =>f (fst y) (snd y)) -> + ~In x m1 -> Add x e m1 m2 -> + eqA (fold f m2 i) (f x e (fold f m1 i)). + Proof. + assert (eqke_refl : forall p, eqke p p). + red; auto. + assert (eqke_sym : forall p p', eqke p p' -> eqke p' p). + intros (x1,x2) (y1,y2); unfold eq_key_elt; simpl; intuition. + assert (eqke_trans : forall p p' p'', eqke p p' -> eqke p' p'' -> eqke p p''). + intros (x1,x2) (y1,y2) (z1,z2); unfold eq_key_elt; simpl. + intuition; eauto; congruence. + intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right. + set (f':=fun y x0 => f (fst y) (snd y) x0) in *. + change (f x e (fold_right f' i (rev (elements m1)))) + with (f' (x,e) (fold_right f' i (rev (elements m1)))). + apply fold_right_add with (eqA:=eqke)(eqB:=eqA); auto. + apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w. + apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w. + rewrite InA_rev. + contradict H1. + exists e. + rewrite elements_mapsto_iff; auto. + intros a. + rewrite InA_cons; do 2 rewrite InA_rev; + destruct a as (a,b); do 2 rewrite <- elements_mapsto_iff. + do 2 rewrite find_mapsto_iff; unfold eq_key_elt; simpl. + rewrite H2. + rewrite add_o. + destruct (eq_dec x a); intuition. + inversion H3; auto. + f_equal; auto. + elim H1. + exists b; apply MapsTo_1 with a; auto with map. + elim n; auto. + Qed. + + Lemma cardinal_fold : forall m, cardinal m = fold (fun _ _ => S) m 0. + Proof. + intros; unfold cardinal; rewrite fold_1. + symmetry; apply fold_left_length; auto. + Qed. + + Lemma cardinal_Empty : forall m, Empty m <-> cardinal m = 0. + Proof. + intros. + rewrite elements_Empty. + unfold cardinal. + destruct (elements m); intuition; discriminate. + Qed. + + Lemma Equal_cardinal : forall m m', Equal m m' -> cardinal m = cardinal m'. + Proof. + intros; do 2 rewrite cardinal_fold. + apply fold_Equal with (eqA:=@eq _); auto. + constructor; auto; congruence. + red; auto. + red; auto. + Qed. + + Lemma cardinal_1 : forall m, Empty m -> cardinal m = 0. + Proof. + intros; rewrite <- cardinal_Empty; auto. + Qed. + + Lemma cardinal_2 : + forall m m' x e, ~ In x m -> Add x e m m' -> cardinal m' = S (cardinal m). + Proof. + intros; do 2 rewrite cardinal_fold. + change S with ((fun _ _ => S) x e). + apply fold_Add; auto. + constructor; intros; auto; congruence. + red; simpl; auto. + red; simpl; auto. + Qed. + + Lemma cardinal_inv_1 : forall m, cardinal m = 0 -> Empty m. + Proof. + intros; rewrite cardinal_Empty; auto. + Qed. + Hint Resolve cardinal_inv_1 : map. + + Lemma cardinal_inv_2 : + forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }. + Proof. + unfold cardinal; intros. + generalize (elements_mapsto_iff m). + destruct (elements m); try discriminate. + exists p; auto. + rewrite H0; destruct p; simpl; auto. + constructor; red; auto. + Qed. + + Lemma cardinal_inv_2b : + forall m, cardinal m <> 0 -> { p : key*elt | MapsTo (fst p) (snd p) m }. + Proof. + intros. + generalize (@cardinal_inv_2 m); destruct cardinal. + elim H;auto. + eauto. + Qed. + + Lemma map_induction : + forall P : t elt -> Type, + (forall m, Empty m -> P m) -> + (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') -> + forall m, P m. + Proof. + intros; remember (cardinal m) as n; revert m Heqn; induction n; intros. + apply X; apply cardinal_inv_1; auto. + + destruct (cardinal_inv_2 (sym_eq Heqn)) as ((x,e),H0); simpl in *. + assert (Add x e (remove x m) m). + red; intros. + rewrite add_o; rewrite remove_o; destruct (eq_dec x y); eauto with map. + apply X0 with (remove x m) x e; auto with map. + apply IHn; auto with map. + assert (S n = S (cardinal (remove x m))). + rewrite Heqn; eapply cardinal_2; eauto with map. + inversion H1; auto with map. + Qed. + + End Elt. + +End WProperties. + +(** * Same Properties for full maps *) + +Module Properties (M:S). + Module D := OT_as_DT M.E. + Include WProperties D M. +End Properties. + +(** * Properties specific to maps with ordered keys *) + +Module OrdProperties (M:S). + Module Import ME := OrderedTypeFacts M.E. + Module Import O:=KeyOrderedType M.E. + Module Import P:=Properties M. + Import F. + Import M. + + Section Elt. + Variable elt:Set. + + Notation eqke := (@eqke elt). + Notation eqk := (@eqk elt). + Notation ltk := (@ltk elt). + Notation cardinal := (@cardinal elt). + Notation Equal := (@P.Equal elt). + Notation Add := (@Add elt). + + Definition Above x (m:t elt) := forall y, In y m -> E.lt y x. + Definition Below x (m:t elt) := forall y, In y m -> E.lt x y. + + Section Elements. + Lemma sort_equivlistA_eqlistA : forall l l' : list (key*elt), sort ltk l -> sort ltk l' -> equivlistA eqke l l' -> eqlistA eqke l l'. Proof. @@ -782,75 +983,6 @@ Module Properties (M: S). End Elements. - Section Cardinal. - - Lemma cardinal_Empty : forall m, Empty m <-> cardinal m = 0. - Proof. - intros. - rewrite elements_Empty. - unfold cardinal. - destruct (elements m); intuition; discriminate. - Qed. - - Lemma cardinal_inv_1 : forall (m:t elt), cardinal m = 0 -> Empty m. - Proof. - intros m; unfold cardinal; intros H e a. - rewrite elements_mapsto_iff. - destruct (elements m); simpl in *; discriminate || red; inversion 1. - Qed. - - Lemma cardinal_inv_2 : - forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }. - Proof. - intros; unfold cardinal in *. - generalize (elements_2 (m:=m)). - destruct (elements m); try discriminate. - exists p; auto. - destruct p; simpl; auto. - apply H0; constructor; red; auto. - Qed. - - Lemma cardinal_inv_2b : - forall m, cardinal m <> 0 -> { p : key*elt | MapsTo (fst p) (snd p) m }. - Proof. - intros; unfold cardinal in *. - generalize (elements_2 (m:=m)). - destruct (elements m). - simpl in H; elim H; auto. - exists p; auto. - destruct p; simpl; auto. - apply H0; constructor; red; auto. - Qed. - - Lemma cardinal_1 : forall (m:t elt), Empty m -> cardinal m = 0. - Proof. - intros; rewrite <- cardinal_Empty; auto. - Qed. - - Lemma cardinal_2 : forall m m' x e, ~In x m -> Add x e m m' -> - cardinal m' = S (cardinal m). - Proof. - intros. - unfold cardinal. - unfold key. - rewrite (eqlistA_length (elements_Add H H0)); simpl. - rewrite app_length; simpl. - rewrite <- plus_n_Sm. - f_equal. - rewrite <- app_length. - f_equal. - symmetry; apply elements_split; auto. - Qed. - - Lemma cardinal_Equal : forall m m', Equal m m' -> cardinal m = cardinal m'. - Proof. - unfold cardinal; intros. - apply eqlistA_length with (eqA:=eqke). - apply elements_Equal_eqlistA; auto. - Qed. - - End Cardinal. - Section Min_Max_Elt. (** We emulate two [max_elt] and [min_elt] functions. *) @@ -977,26 +1109,6 @@ Module Properties (M: S). End Min_Max_Elt. Section Induction_Principles. - - Lemma map_induction : - forall P : t elt -> Type, - (forall m, Empty m -> P m) -> - (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') -> - forall m, P m. - Proof. - intros; remember (cardinal m) as n; revert m Heqn; induction n; intros. - apply X; apply cardinal_inv_1; auto. - - destruct (cardinal_inv_2 (sym_eq Heqn)) as ((x,e),H0); simpl in *. - assert (Add x e (remove x m) m). - red; intros. - rewrite add_o; rewrite remove_o; destruct (ME.eq_dec x y); eauto with map. - apply X0 with (remove x m) x e; auto with map. - apply IHn; auto with map. - assert (S n = S (cardinal (remove x m))). - rewrite Heqn; eapply cardinal_2; eauto with map. - inversion H1; auto with map. - Qed. Lemma map_induction_max : forall P : t elt -> Type, @@ -1011,7 +1123,7 @@ Module Properties (M: S). destruct p. assert (Add k e (remove k m) m). red; intros. - rewrite add_o; rewrite remove_o; destruct (ME.eq_dec k y); eauto. + rewrite add_o; rewrite remove_o; destruct (eq_dec k y); eauto. apply find_1; apply MapsTo_1 with k; auto. apply max_elt_MapsTo; auto. apply X0 with (remove k m) k e; auto with map. @@ -1038,7 +1150,7 @@ Module Properties (M: S). destruct p. assert (Add k e (remove k m) m). red; intros. - rewrite add_o; rewrite remove_o; destruct (ME.eq_dec k y); eauto. + rewrite add_o; rewrite remove_o; destruct (eq_dec k y); eauto. apply find_1; apply MapsTo_1 with k; auto. apply min_elt_MapsTo; auto. apply X0 with (remove k m) k e; auto. @@ -1056,13 +1168,8 @@ Module Properties (M: S). Section Fold_properties. - Lemma fold_Empty : forall s (A:Set)(f:key->elt->A->A)(i:A), - Empty s -> fold f s i = i. - Proof. - intros. - rewrite fold_1. - rewrite elements_Empty in H; rewrite H; simpl; auto. - Qed. + (** The following lemma has already been proved on Weak Maps, + but with one additionnal hypothesis (some [transpose] fact). *) Lemma fold_Equal : forall s1 s2 (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) (f:key->elt->A->A)(i:A), @@ -1138,5 +1245,7 @@ Module Properties (M: S). End Elt. -End Properties. +End OrdProperties. + + diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v index c235976bd..53173e968 100644 --- a/theories/FSets/FMapInterface.v +++ b/theories/FSets/FMapInterface.v @@ -10,25 +10,45 @@ (** * Finite map library *) -(** This file proposes an interface for finite maps *) +(** This file proposes interfaces for finite maps *) -Require Export Bool OrderedType. +Require Export Bool DecidableType OrderedType. Set Implicit Arguments. Unset Strict Implicit. -(** When compared with Ocaml Map, this signature has been split in two: - - The first part [S] contains the usual operators (add, find, ...) - It only requires a ordered key type, the data type can be arbitrary. - The only function that asks more is [equal], whose first argument should - be an equality on data. - - Then, [Sord] extends [S] with a complete comparison function. For - that, the data type should have a decidable total ordering. +(** When compared with Ocaml Map, this signature has been split in + several parts : + + - The first parts [WSfun] and [WS] propose signatures for weak + maps, which are maps with no ordering on the key type nor the + data type. [WSfun] and [WS] are almost identical, apart from the + fact that [WSfun] is expressed in a functorial way whereas [WS] + is self-contained. For obtaining an instance of such signatures, + a decidable equality on keys in enough (see for instance + [FMapWeakList]). These signatures contain the usual operators + (add, find, ...). The only function that asks for more is + [equal], whose first argument should be a comparison on data. + + - Then comes [Sfun] and [S], that extend [WSfun] and [WS] to the + case where the key type is ordered. The main addition states that + [elements] produces sorted lists. + + - Finally, [Sord] extends [S] with a complete comparison function. For + that, the data type should have a decidable total ordering as well. *) -Module Type S. - Declare Module E : OrderedType. +(** ** Weak Signature for maps + + No requirements for an ordering on elements, only decidability + of equality. First, a functorial signature: *) + +Module Type WSfun (E : EqualityType). + + (** The module E of base objects is meant to be a DecidableType + (and used to be so). But requiring only an EqualityType here + allows subtyping between FMap and FMapWeak *) Definition key := E.t. @@ -125,8 +145,6 @@ Module Type S. Definition eq_key_elt (p p':key*elt) := E.eq (fst p) (fst p') /\ (snd p) = (snd p'). - Definition lt_key (p p':key*elt) := E.lt (fst p) (fst p'). - (** Specification of [MapsTo] *) Parameter MapsTo_1 : E.eq x y -> MapsTo x e m -> MapsTo y e m. @@ -160,9 +178,8 @@ Module Type S. MapsTo x e m -> InA eq_key_elt (x,e) (elements m). Parameter elements_2 : InA eq_key_elt (x,e) (elements m) -> MapsTo x e m. - Parameter elements_3 : sort lt_key (elements m). - (* We add artificially elements_3w, a weaker version of - elements_3, for allowing FMapWeak < FMap subtyping. *) + (** When compared with ordered FMap, here comes the only + property that is really weaker: *) Parameter elements_3w : NoDupA eq_key (elements m). (** Specification of [fold] *) @@ -206,7 +223,7 @@ Module Type S. (x:key)(f:option elt->option elt'->option elt''), In x (map2 f m m') -> In x m \/ In x m'. - Hint Immediate MapsTo_1 mem_2 is_empty_2 + Hint Immediate MapsTo_1 mem_2 is_empty_2 map_2 mapi_2 add_3 remove_3 find_2 : map. Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1 @@ -215,11 +232,40 @@ Module Type S. (** for compatibility with earlier hints *) Hint Resolve map_2 mapi_2 add_3 remove_3 find_2 : oldmap. +End WSfun. + +(** ** Main signature [WS] for Weak Maps + + Similar to [WSfun] but expressed in a self-contained way. *) + +Module Type WS. + Declare Module E : EqualityType. + Include Type WSfun E. +End WS. + +(** ** Maps on ordered keys, functorial signature *) + +Module Type Sfun (E : OrderedType). + Include Type WSfun E. + Section elt. + Variable elt:Set. + Definition lt_key (p p':key*elt) := E.lt (fst p) (fst p'). + (* Additionnal specification of [elements] *) + Parameter elements_3 : forall m, sort lt_key (elements m). + End elt. +End Sfun. + +(** ** Maps on ordered keys, self-contained signature *) + +Module Type S. + Declare Module E : OrderedType. + Include Type Sfun E. End S. +(** ** Maps with ordering both on keys and datas *) Module Type Sord. - + Declare Module Data : OrderedType. Declare Module MapS : S. Import MapS. @@ -245,4 +291,4 @@ Module Type Sord. is a total ordering used to compare data associated with equal keys in the two maps. *) -End Sord.
\ No newline at end of file +End Sord. diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index b2cedaabb..b86e558b3 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -14,7 +14,6 @@ [FMapInterface.S] using lists of pairs ordered (increasing) with respect to left projection. *) -Require Import FSetInterface. Require Import FMapInterface. Set Implicit Arguments. @@ -23,10 +22,8 @@ Unset Strict Implicit. Module Raw (X:OrderedType). Module E := X. -Module MX := OrderedTypeFacts X. -Module PX := KeyOrderedType X. -Import MX. -Import PX. +Module Import MX := OrderedTypeFacts X. +Module Import PX := KeyOrderedType X. Definition key := X.t. Definition t (elt:Set) := list (X.t * elt). diff --git a/theories/FSets/FMapWeak.v b/theories/FSets/FMapWeak.v deleted file mode 100644 index a04ace03c..000000000 --- a/theories/FSets/FMapWeak.v +++ /dev/null @@ -1,15 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(* $Id$ *) - -Require Export DecidableType. -Require Export DecidableTypeEx. -Require Export FMapWeakInterface. -Require Export FMapWeakList. -Require Export FMapWeakFacts.
\ No newline at end of file diff --git a/theories/FSets/FMapWeakFacts.v b/theories/FSets/FMapWeakFacts.v deleted file mode 100644 index fbf761d8e..000000000 --- a/theories/FSets/FMapWeakFacts.v +++ /dev/null @@ -1,763 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(* $Id$ *) - -(** * Finite maps library *) - -(** This functor derives additional facts from [FMapWeakInterface.S]. These - facts are mainly the specifications of [FMapWeakInterface.S] written using - different styles: equivalence and boolean equalities. -*) - -Require Import Bool. -Require Import OrderedType. -Require Export FMapWeakInterface. -Set Implicit Arguments. -Unset Strict Implicit. - -Module Facts (M:S)(D:DecidableType with Definition t:=M.E.t - with Definition eq:=M.E.eq). -Import M. - -Notation eq_dec := D.eq_dec. -Definition eqb x y := if eq_dec x y then true else false. - -Lemma MapsTo_fun : forall (elt:Set) m x (e e':elt), - MapsTo x e m -> MapsTo x e' m -> e=e'. -Proof. -intros. -generalize (find_1 H) (find_1 H0); clear H H0. -intros; rewrite H in H0; injection H0; auto. -Qed. - -(** * Specifications written using equivalences *) - -Section IffSpec. -Variable elt elt' elt'': Set. -Implicit Type m: t elt. -Implicit Type x y z: key. -Implicit Type e: elt. - -Lemma MapsTo_iff : forall m x y e, E.eq x y -> (MapsTo x e m <-> MapsTo y e m). -Proof. -split; apply MapsTo_1; auto. -Qed. - -Lemma In_iff : forall m x y, E.eq x y -> (In x m <-> In y m). -Proof. -unfold In. -split; intros (e0,H0); exists e0. -apply (MapsTo_1 H H0); auto. -apply (MapsTo_1 (E.eq_sym H) H0); auto. -Qed. - -Lemma find_mapsto_iff : forall m x e, MapsTo x e m <-> find x m = Some e. -Proof. -split; [apply find_1|apply find_2]. -Qed. - -Lemma not_find_mapsto_iff : forall m x, ~In x m <-> find x m = None. -Proof. -intros. -generalize (find_mapsto_iff m x); destruct (find x m). -split; intros; try discriminate. -destruct H0. -exists e; rewrite H; auto. -split; auto. -intros; intros (e,H1). -rewrite H in H1; discriminate. -Qed. - -Lemma mem_in_iff : forall m x, In x m <-> mem x m = true. -Proof. -split; [apply mem_1|apply mem_2]. -Qed. - -Lemma not_mem_in_iff : forall m x, ~In x m <-> mem x m = false. -Proof. -intros; rewrite mem_in_iff; destruct (mem x m); intuition. -Qed. - -Lemma equal_iff : forall m m' cmp, Equal cmp m m' <-> equal cmp m m' = true. -Proof. -split; [apply equal_1|apply equal_2]. -Qed. - -Lemma empty_mapsto_iff : forall x e, MapsTo x e (empty elt) <-> False. -Proof. -intuition; apply (empty_1 H). -Qed. - -Lemma empty_in_iff : forall x, In x (empty elt) <-> False. -Proof. -unfold In. -split; [intros (e,H); rewrite empty_mapsto_iff in H|]; intuition. -Qed. - -Lemma is_empty_iff : forall m, Empty m <-> is_empty m = true. -Proof. -split; [apply is_empty_1|apply is_empty_2]. -Qed. - -Lemma add_mapsto_iff : forall m x y e e', - MapsTo y e' (add x e m) <-> - (E.eq x y /\ e=e') \/ - (~E.eq x y /\ MapsTo y e' m). -Proof. -intros. -intuition. -destruct (eq_dec x y); [left|right]. -split; auto. -symmetry; apply (MapsTo_fun (e':=e) H); auto with map. -split; auto; apply add_3 with x e; auto. -subst; auto with map. -Qed. - -Lemma add_in_iff : forall m x y e, In y (add x e m) <-> E.eq x y \/ In y m. -Proof. -unfold In; split. -intros (e',H). -destruct (eq_dec x y) as [E|E]; auto. -right; exists e'; auto. -apply (add_3 E H). -destruct (eq_dec x y) as [E|E]; auto. -intros. -exists e; apply add_1; auto. -intros [H|(e',H)]. -destruct E; auto. -exists e'; apply add_2; auto. -Qed. - -Lemma add_neq_mapsto_iff : forall m x y e e', - ~ E.eq x y -> (MapsTo y e' (add x e m) <-> MapsTo y e' m). -Proof. -split; [apply add_3|apply add_2]; auto. -Qed. - -Lemma add_neq_in_iff : forall m x y e, - ~ E.eq x y -> (In y (add x e m) <-> In y m). -Proof. -split; intros (e',H0); exists e'. -apply (add_3 H H0). -apply add_2; auto. -Qed. - -Lemma remove_mapsto_iff : forall m x y e, - MapsTo y e (remove x m) <-> ~E.eq x y /\ MapsTo y e m. -Proof. -intros. -split; intros. -split. -assert (In y (remove x m)) by (exists e; auto). -intro H1; apply (remove_1 H1 H0). -apply remove_3 with x; auto. -apply remove_2; intuition. -Qed. - -Lemma remove_in_iff : forall m x y, In y (remove x m) <-> ~E.eq x y /\ In y m. -Proof. -unfold In; split. -intros (e,H). -split. -assert (In y (remove x m)) by (exists e; auto). -intro H1; apply (remove_1 H1 H0). -exists e; apply remove_3 with x; auto. -intros (H,(e,H0)); exists e; apply remove_2; auto. -Qed. - -Lemma remove_neq_mapsto_iff : forall m x y e, - ~ E.eq x y -> (MapsTo y e (remove x m) <-> MapsTo y e m). -Proof. -split; [apply remove_3|apply remove_2]; auto. -Qed. - -Lemma remove_neq_in_iff : forall m x y, - ~ E.eq x y -> (In y (remove x m) <-> In y m). -Proof. -split; intros (e',H0); exists e'. -apply (remove_3 H0). -apply remove_2; auto. -Qed. - -Lemma elements_mapsto_iff : forall m x e, - MapsTo x e m <-> InA (@eq_key_elt _) (x,e) (elements m). -Proof. -split; [apply elements_1 | apply elements_2]. -Qed. - -Lemma elements_in_iff : forall m x, - In x m <-> exists e, InA (@eq_key_elt _) (x,e) (elements m). -Proof. -unfold In; split; intros (e,H); exists e; [apply elements_1 | apply elements_2]; auto. -Qed. - -Lemma map_mapsto_iff : forall m x b (f : elt -> elt'), - MapsTo x b (map f m) <-> exists a, b = f a /\ MapsTo x a m. -Proof. -split. -case_eq (find x m); intros. -exists e. -split. -apply (MapsTo_fun (m:=map f m) (x:=x)); auto with map. -apply find_2; auto with map. -assert (In x (map f m)) by (exists b; auto). -destruct (map_2 H1) as (a,H2). -rewrite (find_1 H2) in H; discriminate. -intros (a,(H,H0)). -subst b; auto with map. -Qed. - -Lemma map_in_iff : forall m x (f : elt -> elt'), - In x (map f m) <-> In x m. -Proof. -split; intros; eauto with map. -destruct H as (a,H). -exists (f a); auto with map. -Qed. - -Lemma mapi_in_iff : forall m x (f:key->elt->elt'), - In x (mapi f m) <-> In x m. -Proof. -split; intros; eauto with map. -destruct H as (a,H). -destruct (mapi_1 f H) as (y,(H0,H1)). -exists (f y a); auto. -Qed. - -(* Unfortunately, we don't have simple equivalences for [mapi] - and [MapsTo]. The only correct one needs compatibility of [f]. *) - -Lemma mapi_inv : forall m x b (f : key -> elt -> elt'), - MapsTo x b (mapi f m) -> - exists a, exists y, E.eq y x /\ b = f y a /\ MapsTo x a m. -Proof. -intros; case_eq (find x m); intros. -exists e. -destruct (@mapi_1 _ _ m x e f) as (y,(H1,H2)). -apply find_2; auto with map. -exists y; repeat split; auto with map. -apply (MapsTo_fun (m:=mapi f m) (x:=x)); auto with map. -assert (In x (mapi f m)) by (exists b; auto). -destruct (mapi_2 H1) as (a,H2). -rewrite (find_1 H2) in H0; discriminate. -Qed. - -Lemma mapi_1bis : forall m x e (f:key->elt->elt'), - (forall x y e, E.eq x y -> f x e = f y e) -> - MapsTo x e m -> MapsTo x (f x e) (mapi f m). -Proof. -intros. -destruct (mapi_1 f H0) as (y,(H1,H2)). -replace (f x e) with (f y e) by auto. -auto. -Qed. - -Lemma mapi_mapsto_iff : forall m x b (f:key->elt->elt'), - (forall x y e, E.eq x y -> f x e = f y e) -> - (MapsTo x b (mapi f m) <-> exists a, b = f x a /\ MapsTo x a m). -Proof. -split. -intros. -destruct (mapi_inv H0) as (a,(y,(H1,(H2,H3)))). -exists a; split; auto. -subst b; auto. -intros (a,(H0,H1)). -subst b. -apply mapi_1bis; auto. -Qed. - -(** Things are even worse for [map2] : we don't try to state any - equivalence, see instead boolean results below. *) - -End IffSpec. - -(** Useful tactic for simplifying expressions like [In y (add x e (remove z m))] *) - -Ltac map_iff := - repeat (progress ( - rewrite add_mapsto_iff || rewrite add_in_iff || - rewrite remove_mapsto_iff || rewrite remove_in_iff || - rewrite empty_mapsto_iff || rewrite empty_in_iff || - rewrite map_mapsto_iff || rewrite map_in_iff || - rewrite mapi_in_iff)). - -(** * Specifications written using boolean predicates *) - -Section BoolSpec. - -Lemma mem_find_b : forall (elt:Set)(m:t elt)(x:key), mem x m = if find x m then true else false. -Proof. -intros. -generalize (find_mapsto_iff m x)(mem_in_iff m x); unfold In. -destruct (find x m); destruct (mem x m); auto. -intros. -rewrite <- H0; exists e; rewrite H; auto. -intuition. -destruct H0 as (e,H0). -destruct (H e); intuition discriminate. -Qed. - -Variable elt elt' elt'' : Set. -Implicit Types m : t elt. -Implicit Types x y z : key. -Implicit Types e : elt. - -Lemma mem_b : forall m x y, E.eq x y -> mem x m = mem y m. -Proof. -intros. -generalize (mem_in_iff m x) (mem_in_iff m y)(In_iff m H). -destruct (mem x m); destruct (mem y m); intuition. -Qed. - -Lemma find_o : forall m x y, E.eq x y -> find x m = find y m. -Proof. -intros. -generalize (find_mapsto_iff m x) (find_mapsto_iff m y) (fun e => MapsTo_iff m e H). -destruct (find x m); destruct (find y m); intros. -rewrite <- H0; rewrite H2; rewrite H1; auto. -symmetry; rewrite <- H1; rewrite <- H2; rewrite H0; auto. -rewrite <- H0; rewrite H2; rewrite H1; auto. -auto. -Qed. - -Lemma empty_o : forall x, find x (empty elt) = None. -Proof. -intros. -case_eq (find x (empty elt)); intros; auto. -generalize (find_2 H). -rewrite empty_mapsto_iff; intuition. -Qed. - -Lemma empty_a : forall x, mem x (empty elt) = false. -Proof. -intros. -case_eq (mem x (empty elt)); intros; auto. -generalize (mem_2 H). -rewrite empty_in_iff; intuition. -Qed. - -Lemma add_eq_o : forall m x y e, - E.eq x y -> find y (add x e m) = Some e. -Proof. -auto with map. -Qed. - -Lemma add_neq_o : forall m x y e, - ~ E.eq x y -> find y (add x e m) = find y m. -Proof. -intros. -case_eq (find y m); intros; auto with map. -case_eq (find y (add x e m)); intros; auto with map. -rewrite <- H0; symmetry. -apply find_1; apply add_3 with x e; auto with map. -Qed. -Hint Resolve add_neq_o : map. - -Lemma add_o : forall m x y e, - find y (add x e m) = if eq_dec x y then Some e else find y m. -Proof. -intros; destruct (eq_dec x y); auto with map. -Qed. - -Lemma add_eq_b : forall m x y e, - E.eq x y -> mem y (add x e m) = true. -Proof. -intros; rewrite mem_find_b; rewrite add_eq_o; auto. -Qed. - -Lemma add_neq_b : forall m x y e, - ~E.eq x y -> mem y (add x e m) = mem y m. -Proof. -intros; do 2 rewrite mem_find_b; rewrite add_neq_o; auto. -Qed. - -Lemma add_b : forall m x y e, - mem y (add x e m) = eqb x y || mem y m. -Proof. -intros; do 2 rewrite mem_find_b; rewrite add_o; unfold eqb. -destruct (eq_dec x y); simpl; auto. -Qed. - -Lemma remove_eq_o : forall m x y, - E.eq x y -> find y (remove x m) = None. -Proof. -intros. -generalize (remove_1 (m:=m) H). -generalize (find_mapsto_iff (remove x m) y). -destruct (find y (remove x m)); auto. -destruct 2. -exists e; rewrite H0; auto. -Qed. -Hint Resolve remove_eq_o : map. - -Lemma remove_neq_o : forall m x y, - ~ E.eq x y -> find y (remove x m) = find y m. -Proof. -intros. -case_eq (find y m); intros; auto with map. -case_eq (find y (remove x m)); intros; auto with map. -rewrite <- H0; symmetry. -apply find_1; apply remove_3 with x; auto with map. -Qed. -Hint Resolve remove_neq_o : map. - -Lemma remove_o : forall m x y, - find y (remove x m) = if eq_dec x y then None else find y m. -Proof. -intros; destruct (eq_dec x y); auto with map. -Qed. - -Lemma remove_eq_b : forall m x y, - E.eq x y -> mem y (remove x m) = false. -Proof. -intros; rewrite mem_find_b; rewrite remove_eq_o; auto. -Qed. - -Lemma remove_neq_b : forall m x y, - ~ E.eq x y -> mem y (remove x m) = mem y m. -Proof. -intros; do 2 rewrite mem_find_b; rewrite remove_neq_o; auto. -Qed. - -Lemma remove_b : forall m x y, - mem y (remove x m) = negb (eqb x y) && mem y m. -Proof. -intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb. -destruct (eq_dec x y); auto. -Qed. - -Definition option_map (A:Set)(B:Set)(f:A->B)(o:option A) : option B := - match o with - | Some a => Some (f a) - | None => None - end. - -Lemma map_o : forall m x (f:elt->elt'), - find x (map f m) = option_map f (find x m). -Proof. -intros. -generalize (find_mapsto_iff (map f m) x) (find_mapsto_iff m x) - (fun b => map_mapsto_iff m x b f). -destruct (find x (map f m)); destruct (find x m); simpl; auto; intros. -rewrite <- H; rewrite H1; exists e0; rewrite H0; auto. -destruct (H e) as [_ H2]. -rewrite H1 in H2. -destruct H2 as (a,(_,H2)); auto. -rewrite H0 in H2; discriminate. -rewrite <- H; rewrite H1; exists e; rewrite H0; auto. -Qed. - -Lemma map_b : forall m x (f:elt->elt'), - mem x (map f m) = mem x m. -Proof. -intros; do 2 rewrite mem_find_b; rewrite map_o. -destruct (find x m); simpl; auto. -Qed. - -Lemma mapi_b : forall m x (f:key->elt->elt'), - mem x (mapi f m) = mem x m. -Proof. -intros. -generalize (mem_in_iff (mapi f m) x) (mem_in_iff m x) (mapi_in_iff m x f). -destruct (mem x (mapi f m)); destruct (mem x m); simpl; auto; intros. -symmetry; rewrite <- H0; rewrite <- H1; rewrite H; auto. -rewrite <- H; rewrite H1; rewrite H0; auto. -Qed. - -Lemma mapi_o : forall m x (f:key->elt->elt'), - (forall x y e, E.eq x y -> f x e = f y e) -> - find x (mapi f m) = option_map (f x) (find x m). -Proof. -intros. -generalize (find_mapsto_iff (mapi f m) x) (find_mapsto_iff m x) - (fun b => mapi_mapsto_iff m x b H). -destruct (find x (mapi f m)); destruct (find x m); simpl; auto; intros. -rewrite <- H0; rewrite H2; exists e0; rewrite H1; auto. -destruct (H0 e) as [_ H3]. -rewrite H2 in H3. -destruct H3 as (a,(_,H3)); auto. -rewrite H1 in H3; discriminate. -rewrite <- H0; rewrite H2; exists e; rewrite H1; auto. -Qed. - -Lemma map2_1bis : forall (m: t elt)(m': t elt') x - (f:option elt->option elt'->option elt''), - f None None = None -> - find x (map2 f m m') = f (find x m) (find x m'). -Proof. -intros. -case_eq (find x m); intros. -rewrite <- H0. -apply map2_1; auto with map. -left; exists e; auto with map. -case_eq (find x m'); intros. -rewrite <- H0; rewrite <- H1. -apply map2_1; auto. -right; exists e; auto with map. -rewrite H. -case_eq (find x (map2 f m m')); intros; auto with map. -assert (In x (map2 f m m')) by (exists e; auto with map). -destruct (map2_2 H3) as [(e0,H4)|(e0,H4)]. -rewrite (find_1 H4) in H0; discriminate. -rewrite (find_1 H4) in H1; discriminate. -Qed. - -Lemma elements_o : forall m x, - find x m = findA (eqb x) (elements m). -Proof. -intros. -assert (forall e, find x m = Some e <-> InA (eq_key_elt (elt:=elt)) (x,e) (elements m)). - intros; rewrite <- find_mapsto_iff; apply elements_mapsto_iff. -assert (NoDupA (eq_key (elt:=elt)) (elements m)). - exact (elements_3w m). -generalize (fun e => @findA_NoDupA _ _ _ D.eq_sym D.eq_trans eq_dec (elements m) x e H0). -unfold eqb. -destruct (find x m); destruct (findA (fun y:D.t => if eq_dec x y then true else false) (elements m)); - simpl; auto; intros. -symmetry; rewrite <- H1; rewrite <- H; auto. -symmetry; rewrite <- H1; rewrite <- H; auto. -rewrite H; rewrite H1; auto. -Qed. - -Lemma elements_b : forall m x, mem x m = existsb (fun p => eqb x (fst p)) (elements m). -Proof. -intros. -generalize (mem_in_iff m x)(elements_in_iff m x) - (existsb_exists (fun p => eqb x (fst p)) (elements m)). -destruct (mem x m); destruct (existsb (fun p => eqb x (fst p)) (elements m)); auto; intros. -symmetry; rewrite H1. -destruct H0 as (H0,_). -destruct H0 as (e,He); [ intuition |]. -rewrite InA_alt in He. -destruct He as ((y,e'),(Ha1,Ha2)). -compute in Ha1; destruct Ha1; subst e'. -exists (y,e); split; simpl; auto. -unfold eqb; destruct (eq_dec x y); intuition. -rewrite <- H; rewrite H0. -destruct H1 as (H1,_). -destruct H1 as ((y,e),(Ha1,Ha2)); [intuition|]. -simpl in Ha2. -unfold eqb in *; destruct (eq_dec x y); auto; try discriminate. -exists e; rewrite InA_alt. -exists (y,e); intuition. -compute; auto. -Qed. - -End BoolSpec. - -End Facts. - - -Module Properties - (M:S)(D:DecidableType with Definition t:=M.E.t - with Definition eq:=M.E.eq). - Module F:=Facts M D. - Import F. - Import M. - - Section Elt. - Variable elt:Set. - - Definition cardinal (m:t elt) := length (elements m). - - Definition Equal (m m':t elt) := forall y, find y m = find y m'. - Definition Add x (e:elt) m m' := forall y, find y m' = find y (add x e m). - - Notation eqke := (@eq_key_elt elt). - Notation eqk := (@eq_key elt). - - Lemma elements_Empty : forall m:t elt, Empty m <-> elements m = nil. - Proof. - intros. - unfold Empty. - split; intros. - assert (forall a, ~ List.In a (elements m)). - red; intros. - apply (H (fst a) (snd a)). - rewrite elements_mapsto_iff. - rewrite InA_alt; exists a; auto. - split; auto; split; auto. - destruct (elements m); auto. - elim (H0 p); simpl; auto. - red; intros. - rewrite elements_mapsto_iff in H0. - rewrite InA_alt in H0; destruct H0. - rewrite H in H0; destruct H0 as (_,H0); inversion H0. - Qed. - - Lemma fold_Empty : forall m (A:Set)(f:key->elt->A->A)(i:A), - Empty m -> fold f m i = i. - Proof. - intros. - rewrite fold_1. - rewrite elements_Empty in H; rewrite H; simpl; auto. - Qed. - - Lemma NoDupA_eqk_eqke : forall l, NoDupA eqk l -> NoDupA eqke l. - Proof. - induction 1; auto. - constructor; auto. - contradict H. - destruct x as (x,y). - rewrite InA_alt in *; destruct H as ((a,b),((H1,H2),H3)); simpl in *. - exists (a,b); auto. - Qed. - - Lemma fold_Equal : forall m1 m2 (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) - (f:key->elt->A->A)(i:A), - compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> - transpose eqA (fun y => f (fst y) (snd y)) -> - Equal m1 m2 -> - eqA (fold f m1 i) (fold f m2 i). - Proof. - assert (eqke_refl : forall p, eqke p p). - red; auto. - assert (eqke_sym : forall p p', eqke p p' -> eqke p' p). - intros (x1,x2) (y1,y2); unfold eq_key_elt; simpl; intuition. - assert (eqke_trans : forall p p' p'', eqke p p' -> eqke p' p'' -> eqke p p''). - intros (x1,x2) (y1,y2) (z1,z2); unfold eq_key_elt; simpl. - intuition; eauto; congruence. - intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right. - apply fold_right_equivlistA with (eqA:=eqke) (eqB:=eqA); auto. - apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w. - apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w. - red; intros. - do 2 rewrite InA_rev. - destruct x; do 2 rewrite <- elements_mapsto_iff. - do 2 rewrite find_mapsto_iff. - rewrite H1; split; auto. - Qed. - - Lemma fold_Add : forall m1 m2 x e (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) - (f:key->elt->A->A)(i:A), - compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> - transpose eqA (fun y =>f (fst y) (snd y)) -> - ~In x m1 -> Add x e m1 m2 -> - eqA (fold f m2 i) (f x e (fold f m1 i)). - Proof. - assert (eqke_refl : forall p, eqke p p). - red; auto. - assert (eqke_sym : forall p p', eqke p p' -> eqke p' p). - intros (x1,x2) (y1,y2); unfold eq_key_elt; simpl; intuition. - assert (eqke_trans : forall p p' p'', eqke p p' -> eqke p' p'' -> eqke p p''). - intros (x1,x2) (y1,y2) (z1,z2); unfold eq_key_elt; simpl. - intuition; eauto; congruence. - intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right. - set (f':=fun y x0 => f (fst y) (snd y) x0) in *. - change (f x e (fold_right f' i (rev (elements m1)))) - with (f' (x,e) (fold_right f' i (rev (elements m1)))). - apply fold_right_add with (eqA:=eqke)(eqB:=eqA); auto. - apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w. - apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w. - rewrite InA_rev. - contradict H1. - exists e. - rewrite elements_mapsto_iff; auto. - intros a. - rewrite InA_cons; do 2 rewrite InA_rev; - destruct a as (a,b); do 2 rewrite <- elements_mapsto_iff. - do 2 rewrite find_mapsto_iff; unfold eq_key_elt; simpl. - rewrite H2. - rewrite add_o. - destruct (eq_dec x a); intuition. - inversion H3; auto. - f_equal; auto. - elim H1. - exists b; apply MapsTo_1 with a; auto with map. - elim n; auto. - Qed. - - Lemma cardinal_fold : forall m, cardinal m = fold (fun _ _ => S) m 0. - Proof. - intros; unfold cardinal; rewrite fold_1. - symmetry; apply fold_left_length; auto. - Qed. - - Lemma Equal_cardinal : forall m m', Equal m m' -> cardinal m = cardinal m'. - Proof. - intros; do 2 rewrite cardinal_fold. - apply fold_Equal with (eqA:=@eq _); auto. - constructor; auto; congruence. - red; auto. - red; auto. - Qed. - - Lemma cardinal_1 : forall m, Empty m -> cardinal m = 0. - Proof. - intros; unfold cardinal; rewrite elements_Empty in H; rewrite H; simpl; auto. - Qed. - - Lemma cardinal_2 : - forall m m' x e, ~ In x m -> Add x e m m' -> cardinal m' = S (cardinal m). - Proof. - intros; do 2 rewrite cardinal_fold. - change S with ((fun _ _ => S) x e). - apply fold_Add; auto. - constructor; intros; auto; congruence. - red; simpl; auto. - red; simpl; auto. - Qed. - - Lemma cardinal_inv_1 : forall m, cardinal m = 0 -> Empty m. - Proof. - unfold cardinal; intros m H a e. - rewrite elements_mapsto_iff. - destruct (elements m); simpl in *. - red; inversion 1. - inversion H. - Qed. - Hint Resolve cardinal_inv_1 : map. - - Lemma cardinal_inv_2 : - forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }. - Proof. - unfold cardinal; intros. - generalize (elements_mapsto_iff m). - destruct (elements m); try discriminate. - exists p; auto. - rewrite H0; destruct p; simpl; auto. - constructor; red; auto. - Qed. - - Lemma cardinal_inv_2b : - forall m, cardinal m <> 0 -> { p : key*elt | MapsTo (fst p) (snd p) m }. - Proof. - intros; unfold cardinal in *. - generalize (elements_2 (m:=m)). - destruct (elements m). - simpl in H; elim H; auto. - exists p; auto. - destruct p; simpl; auto. - apply H0; constructor; red; auto. - Qed. - - Lemma map_induction : - forall P : t elt -> Type, - (forall m, Empty m -> P m) -> - (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') -> - forall m, P m. - Proof. - intros; remember (cardinal m) as n; revert m Heqn; induction n; intros. - apply X; apply cardinal_inv_1; auto. - - destruct (cardinal_inv_2 (sym_eq Heqn)) as ((x,e),H0); simpl in *. - assert (Add x e (remove x m) m). - red; intros. - rewrite add_o; rewrite remove_o; destruct (eq_dec x y); eauto with map. - apply X0 with (remove x m) x e; auto with map. - apply IHn; auto with map. - assert (S n = S (cardinal (remove x m))). - rewrite Heqn; eapply cardinal_2; eauto with map. - inversion H1; auto with map. - Qed. - - End Elt. - -End Properties. - diff --git a/theories/FSets/FMapWeakInterface.v b/theories/FSets/FMapWeakInterface.v deleted file mode 100644 index 49dcb5214..000000000 --- a/theories/FSets/FMapWeakInterface.v +++ /dev/null @@ -1,209 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(* $Id$ *) - -(** * Finite map library *) - -(** This file proposes an interface for finite maps over keys with decidable - equality, but no decidable order. *) - -Require Export Bool DecidableType. -Set Implicit Arguments. -Unset Strict Implicit. - -Module Type S. - - (** The module E of base objects is meant to be a DecidableType - (and used to be so). But requiring only an EqualityType here - allows subtyping between FMap and FMapWeak *) - Declare Module E : EqualityType. - - Definition key := E.t. - - Parameter t : Set -> Set. (** the abstract type of maps *) - - Section Types. - - Variable elt:Set. - - Parameter empty : t elt. - (** The empty map. *) - - Parameter is_empty : t elt -> bool. - (** Test whether a map is empty or not. *) - - Parameter add : key -> elt -> t elt -> t elt. - (** [add x y m] returns a map containing the same bindings as [m], - plus a binding of [x] to [y]. If [x] was already bound in [m], - its previous binding disappears. *) - - Parameter find : key -> t elt -> option elt. - (** [find x m] returns the current binding of [x] in [m], - or raises [Not_found] if no such binding exists. - NB: in Coq, the exception mechanism becomes a option type. *) - - Parameter remove : key -> t elt -> t elt. - (** [remove x m] returns a map containing the same bindings as [m], - except for [x] which is unbound in the returned map. *) - - Parameter mem : key -> t elt -> bool. - (** [mem x m] returns [true] if [m] contains a binding for [x], - and [false] otherwise. *) - - (** Coq comment: [iter] is useless in a purely functional world *) - (** val iter : (key -> 'a -> unit) -> 'a t -> unit *) - (** iter f m applies f to all bindings in map m. f receives the key as - first argument, and the associated value as second argument. - The bindings are passed to f in increasing order with respect to the - ordering over the type of the keys. Only current bindings are - presented to f: bindings hidden by more recent bindings are not - passed to f. *) - - Variable elt' : Set. - Variable elt'': Set. - - Parameter map : (elt -> elt') -> t elt -> t elt'. - (** [map f m] returns a map with same domain as [m], where the associated - value a of all bindings of [m] has been replaced by the result of the - application of [f] to [a]. The bindings are passed to [f] in - increasing order with respect to the ordering over the type of the - keys. *) - - Parameter mapi : (key -> elt -> elt') -> t elt -> t elt'. - (** Same as [S.map], but the function receives as arguments both the - key and the associated value for each binding of the map. *) - - Parameter map2 : (option elt -> option elt' -> option elt'') -> t elt -> t elt' -> t elt''. - (** Not present in Ocaml. - [map f m m'] creates a new map whose bindings belong to the ones of either - [m] or [m']. The presence and value for a key [k] is determined by [f e e'] - where [e] and [e'] are the (optional) bindings of [k] in [m] and [m']. *) - - Parameter elements : t elt -> list (key*elt). - (** Not present in Ocaml. - [elements m] returns an assoc list corresponding to the bindings of [m]. - Elements of this list are sorted with respect to their first components. - Useful to specify [fold] ... *) - - Parameter fold : forall A: Type, (key -> elt -> A -> A) -> t elt -> A -> A. - (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)], - where [k1] ... [kN] are the keys of all bindings in [m] - (in increasing order), and [d1] ... [dN] are the associated data. *) - - Parameter equal : (elt -> elt -> bool) -> t elt -> t elt -> bool. - (** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are equal, - that is, contain equal keys and associate them with equal data. - [cmp] is the equality predicate used to compare the data associated - with the keys. *) - - Section Spec. - - Variable m m' m'' : t elt. - Variable x y z : key. - Variable e e' : elt. - - Parameter MapsTo : key -> elt -> t elt -> Prop. - - Definition In (k:key)(m: t elt) : Prop := exists e:elt, MapsTo k e m. - - Definition Empty m := forall (a : key)(e:elt) , ~ MapsTo a e m. - - Definition eq_key (p p':key*elt) := E.eq (fst p) (fst p'). - - Definition eq_key_elt (p p':key*elt) := - E.eq (fst p) (fst p') /\ (snd p) = (snd p'). - - (** Specification of [MapsTo] *) - Parameter MapsTo_1 : E.eq x y -> MapsTo x e m -> MapsTo y e m. - - (** Specification of [mem] *) - Parameter mem_1 : In x m -> mem x m = true. - Parameter mem_2 : mem x m = true -> In x m. - - (** Specification of [empty] *) - Parameter empty_1 : Empty empty. - - (** Specification of [is_empty] *) - Parameter is_empty_1 : Empty m -> is_empty m = true. - Parameter is_empty_2 : is_empty m = true -> Empty m. - - (** Specification of [add] *) - Parameter add_1 : E.eq x y -> MapsTo y e (add x e m). - Parameter add_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). - Parameter add_3 : ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. - - (** Specification of [remove] *) - Parameter remove_1 : E.eq x y -> ~ In y (remove x m). - Parameter remove_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m). - Parameter remove_3 : MapsTo y e (remove x m) -> MapsTo y e m. - - (** Specification of [find] *) - Parameter find_1 : MapsTo x e m -> find x m = Some e. - Parameter find_2 : find x m = Some e -> MapsTo x e m. - - (** Specification of [elements] *) - Parameter elements_1 : - MapsTo x e m -> InA eq_key_elt (x,e) (elements m). - Parameter elements_2 : - InA eq_key_elt (x,e) (elements m) -> MapsTo x e m. - (** When compared with ordered FMap, here comes the only - property that is really weaker: *) - Parameter elements_3w : NoDupA eq_key (elements m). - - (** Specification of [fold] *) - Parameter fold_1 : - forall (A : Type) (i : A) (f : key -> elt -> A -> A), - fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. - - Definition Equal cmp m m' := - (forall k, In k m <-> In k m') /\ - (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true). - - Variable cmp : elt -> elt -> bool. - - (** Specification of [equal] *) - Parameter equal_1 : Equal cmp m m' -> equal cmp m m' = true. - Parameter equal_2 : equal cmp m m' = true -> Equal cmp m m'. - - End Spec. - End Types. - - (** Specification of [map] *) - Parameter map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), - MapsTo x e m -> MapsTo x (f e) (map f m). - Parameter map_2 : forall (elt elt':Set)(m: t elt)(x:key)(f:elt->elt'), - In x (map f m) -> In x m. - - (** Specification of [mapi] *) - Parameter mapi_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt) - (f:key->elt->elt'), MapsTo x e m -> - exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m). - Parameter mapi_2 : forall (elt elt':Set)(m: t elt)(x:key) - (f:key->elt->elt'), In x (mapi f m) -> In x m. - - (** Specification of [map2] *) - Parameter map2_1 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') - (x:key)(f:option elt->option elt'->option elt''), - In x m \/ In x m' -> - find x (map2 f m m') = f (find x m) (find x m'). - - Parameter map2_2 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') - (x:key)(f:option elt->option elt'->option elt''), - In x (map2 f m m') -> In x m \/ In x m'. - - Hint Immediate MapsTo_1 mem_2 is_empty_2 - map_2 mapi_2 add_3 remove_3 find_2 - : map. - Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1 - remove_2 find_1 fold_1 map_1 mapi_1 mapi_2 - : map. - (** for compatibility with earlier hints *) - Hint Resolve map_2 mapi_2 add_3 remove_3 find_2 : oldmap. - -End S. diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index dca6e5498..579fd50c9 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -11,21 +11,16 @@ (** * Finite map library *) (** This file proposes an implementation of the non-dependant interface - [FMapInterface.S] using lists of pairs, unordered but without redundancy. *) + [FMapInterface.WS] using lists of pairs, unordered but without redundancy. *) -Require Import FSetInterface. -Require Import FSetWeakInterface. -Require Import FMapWeakInterface. +Require Import FMapInterface. Set Implicit Arguments. Unset Strict Implicit. -Arguments Scope list [type_scope]. - Module Raw (X:DecidableType). -Module PX := KeyDecidableType X. -Import PX. +Module Import PX := KeyDecidableType X. Definition key := X.t. Definition t (elt:Set) := list (X.t * elt). @@ -873,7 +868,7 @@ End Elt3. End Raw. -Module Make (X: DecidableType) <: S with Module E:=X. +Module Make (X: DecidableType) <: WS with Module E:=X. Module Raw := Raw X. Module E := X. diff --git a/theories/FSets/FMaps.v b/theories/FSets/FMaps.v index f812e56e8..644f73a9e 100644 --- a/theories/FSets/FMaps.v +++ b/theories/FSets/FMaps.v @@ -8,9 +8,9 @@ (* $Id$ *) -Require Export OrderedType. -Require Export OrderedTypeEx. -Require Export OrderedTypeAlt. + +Require Export OrderedType OrderedTypeEx OrderedTypeAlt. +Require Export DecidableType DecidableTypeEx. Require Export FMapInterface. Require Export FMapList. Require Export FMapPositive. diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index 825bdefed..d6a92b673 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -17,11 +17,11 @@ (** This file implements a decision procedure for a certain class of propositions involving finite sets. *) -Require Import Decidable DecidableTypeEx FSetWeakFacts. +Require Import Decidable DecidableTypeEx FSetFacts. -Module WeakDecide - (Import M : FSetWeakInterface.S) - (D:DecidableType with Definition t:=M.E.t with Definition eq:=M.E.eq). +(** First, a version for Weak Sets *) + +Module WDecide (E : DecidableType)(Import M : WSfun E). (** * Overview This functor defines the tactic [fsetdec], which will @@ -566,7 +566,7 @@ the above form: the predicates [In] and [E.eq] applied only to variables. We are going to use them with [autorewrite]. *) - Module F := FSetWeakFacts.Facts M D. + Module F := FSetFacts.WFacts E M. Hint Rewrite F.empty_iff F.singleton_iff F.add_iff F.remove_iff F.union_iff F.inter_iff F.diff_iff @@ -585,7 +585,7 @@ the above form: Lemma dec_eq : forall (x y : E.t), decidable (E.eq x y). Proof. - red; intros x y; destruct (D.eq_dec x y); auto. + red; intros x y; destruct (E.eq_dec x y); auto. Qed. (** The hint database [FSet_decidability] will be given to @@ -930,12 +930,15 @@ the above form: End FSetDecideTestCases. -End WeakDecide. +End WDecide. Require Import FSetInterface. -Module Decide (M : FSetInterface.S). +(** Now comes a special version dedicated to full sets. For this + one, only one argument [(M:S)] is necessary. *) + +Module Decide (M : S). Module D:=OT_as_DT M.E. - Module WD := WeakDecide M D. + Module WD := WDecide D M. Ltac fsetdec := WD.fsetdec. End Decide.
\ No newline at end of file diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index 89fae94e6..e0e83c57c 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -12,20 +12,928 @@ (** This module proves many properties of finite sets that are consequences of the axiomatization in [FsetInterface] - Contrary to the functor in [FsetWeakProperties] it uses + Contrary to the functor in [FsetProperties] it uses sets operations instead of predicates over sets, i.e. [mem x s=true] instead of [In x s], [equal s s'=true] instead of [Equal s s'], etc. *) Require Import FSetProperties Zerob Sumbool Omega DecidableTypeEx. -(** Since the properties that used to be there do not depend on - the element ordering, we now simply import them from - FSetWeakEqProperties *) +Module WEqProperties (Import E:DecidableType)(M:WSfun E). +Module Import MP := WProperties E M. +Import FM. +Import M. -Require FSetWeakEqProperties. +Definition Add := MP.Add. + +Section BasicProperties. + +(** Some old specifications written with boolean equalities. *) + +Variable s s' s'': t. +Variable x y z : elt. + +Lemma mem_eq: + E.eq x y -> mem x s=mem y s. +Proof. +intro H; rewrite H; auto. +Qed. + +Lemma equal_mem_1: + (forall a, mem a s=mem a s') -> equal s s'=true. +Proof. +intros; apply equal_1; unfold Equal; intros. +do 2 rewrite mem_iff; rewrite H; tauto. +Qed. + +Lemma equal_mem_2: + equal s s'=true -> forall a, mem a s=mem a s'. +Proof. +intros; rewrite (equal_2 H); auto. +Qed. + +Lemma subset_mem_1: + (forall a, mem a s=true->mem a s'=true) -> subset s s'=true. +Proof. +intros; apply subset_1; unfold Subset; intros a. +do 2 rewrite mem_iff; auto. +Qed. + +Lemma subset_mem_2: + subset s s'=true -> forall a, mem a s=true -> mem a s'=true. +Proof. +intros H a; do 2 rewrite <- mem_iff; apply subset_2; auto. +Qed. + +Lemma empty_mem: mem x empty=false. +Proof. +rewrite <- not_mem_iff; auto with set. +Qed. + +Lemma is_empty_equal_empty: is_empty s = equal s empty. +Proof. +apply bool_1; split; intros. +rewrite <- (empty_is_empty_1 (s:=empty)); auto with set. +rewrite <- is_empty_iff; auto with set. +Qed. + +Lemma choose_mem_1: choose s=Some x -> mem x s=true. +Proof. +auto with set. +Qed. + +Lemma choose_mem_2: choose s=None -> is_empty s=true. +Proof. +auto with set. +Qed. + +Lemma add_mem_1: mem x (add x s)=true. +Proof. +auto with set. +Qed. + +Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s. +Proof. +apply add_neq_b. +Qed. + +Lemma remove_mem_1: mem x (remove x s)=false. +Proof. +rewrite <- not_mem_iff; auto with set. +Qed. + +Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s. +Proof. +apply remove_neq_b. +Qed. + +Lemma singleton_equal_add: + equal (singleton x) (add x empty)=true. +Proof. +rewrite (singleton_equal_add x); auto with set. +Qed. + +Lemma union_mem: + mem x (union s s')=mem x s || mem x s'. +Proof. +apply union_b. +Qed. + +Lemma inter_mem: + mem x (inter s s')=mem x s && mem x s'. +Proof. +apply inter_b. +Qed. + +Lemma diff_mem: + mem x (diff s s')=mem x s && negb (mem x s'). +Proof. +apply diff_b. +Qed. + +(** properties of [mem] *) + +Lemma mem_3 : ~In x s -> mem x s=false. +Proof. +intros; rewrite <- not_mem_iff; auto. +Qed. + +Lemma mem_4 : mem x s=false -> ~In x s. +Proof. +intros; rewrite not_mem_iff; auto. +Qed. + +(** Properties of [equal] *) + +Lemma equal_refl: equal s s=true. +Proof. +auto with set. +Qed. + +Lemma equal_sym: equal s s'=equal s' s. +Proof. +intros; apply bool_1; do 2 rewrite <- equal_iff; intuition. +Qed. + +Lemma equal_trans: + equal s s'=true -> equal s' s''=true -> equal s s''=true. +Proof. +intros; rewrite (equal_2 H); auto. +Qed. + +Lemma equal_equal: + equal s s'=true -> equal s s''=equal s' s''. +Proof. +intros; rewrite (equal_2 H); auto. +Qed. + +Lemma equal_cardinal: + equal s s'=true -> cardinal s=cardinal s'. +Proof. +auto with set. +Qed. + +(* Properties of [subset] *) + +Lemma subset_refl: subset s s=true. +Proof. +auto with set. +Qed. + +Lemma subset_antisym: + subset s s'=true -> subset s' s=true -> equal s s'=true. +Proof. +auto with set. +Qed. + +Lemma subset_trans: + subset s s'=true -> subset s' s''=true -> subset s s''=true. +Proof. +do 3 rewrite <- subset_iff; intros. +apply subset_trans with s'; auto. +Qed. + +Lemma subset_equal: + equal s s'=true -> subset s s'=true. +Proof. +auto with set. +Qed. + +(** Properties of [choose] *) + +Lemma choose_mem_3: + is_empty s=false -> {x:elt|choose s=Some x /\ mem x s=true}. +Proof. +intros. +generalize (@choose_1 s) (@choose_2 s). +destruct (choose s);intros. +exists e;auto with set. +generalize (H1 (refl_equal None)); clear H1. +intros; rewrite (is_empty_1 H1) in H; discriminate. +Qed. + +Lemma choose_mem_4: choose empty=None. +Proof. +generalize (@choose_1 empty). +case (@choose empty);intros;auto. +elim (@empty_1 e); auto. +Qed. + +(** Properties of [add] *) + +Lemma add_mem_3: + mem y s=true -> mem y (add x s)=true. +Proof. +auto with set. +Qed. + +Lemma add_equal: + mem x s=true -> equal (add x s) s=true. +Proof. +auto with set. +Qed. + +(** Properties of [remove] *) + +Lemma remove_mem_3: + mem y (remove x s)=true -> mem y s=true. +Proof. +rewrite remove_b; intros H;destruct (andb_prop _ _ H); auto. +Qed. + +Lemma remove_equal: + mem x s=false -> equal (remove x s) s=true. +Proof. +intros; apply equal_1; apply remove_equal. +rewrite not_mem_iff; auto. +Qed. + +Lemma add_remove: + mem x s=true -> equal (add x (remove x s)) s=true. +Proof. +intros; apply equal_1; apply add_remove; auto with set. +Qed. + +Lemma remove_add: + mem x s=false -> equal (remove x (add x s)) s=true. +Proof. +intros; apply equal_1; apply remove_add; auto. +rewrite not_mem_iff; auto. +Qed. + +(** Properties of [is_empty] *) + +Lemma is_empty_cardinal: is_empty s = zerob (cardinal s). +Proof. +intros; apply bool_1; split; intros. +rewrite MP.cardinal_1; simpl; auto with set. +assert (cardinal s = 0) by (apply zerob_true_elim; auto). +auto with set. +Qed. + +(** Properties of [singleton] *) + +Lemma singleton_mem_1: mem x (singleton x)=true. +Proof. +auto with set. +Qed. + +Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false. +Proof. +intros; rewrite singleton_b. +unfold eqb; destruct (eq_dec x y); intuition. +Qed. + +Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y. +Proof. +intros; apply singleton_1; auto with set. +Qed. + +(** Properties of [union] *) + +Lemma union_sym: + equal (union s s') (union s' s)=true. +Proof. +auto with set. +Qed. + +Lemma union_subset_equal: + subset s s'=true -> equal (union s s') s'=true. +Proof. +auto with set. +Qed. + +Lemma union_equal_1: + equal s s'=true-> equal (union s s'') (union s' s'')=true. +Proof. +auto with set. +Qed. + +Lemma union_equal_2: + equal s' s''=true-> equal (union s s') (union s s'')=true. +Proof. +auto with set. +Qed. + +Lemma union_assoc: + equal (union (union s s') s'') (union s (union s' s''))=true. +Proof. +auto with set. +Qed. + +Lemma add_union_singleton: + equal (add x s) (union (singleton x) s)=true. +Proof. +auto with set. +Qed. + +Lemma union_add: + equal (union (add x s) s') (add x (union s s'))=true. +Proof. +auto with set. +Qed. + +(* caracterisation of [union] via [subset] *) + +Lemma union_subset_1: subset s (union s s')=true. +Proof. +auto with set. +Qed. + +Lemma union_subset_2: subset s' (union s s')=true. +Proof. +auto with set. +Qed. + +Lemma union_subset_3: + subset s s''=true -> subset s' s''=true -> + subset (union s s') s''=true. +Proof. +intros; apply subset_1; apply union_subset_3; auto with set. +Qed. + +(** Properties of [inter] *) + +Lemma inter_sym: equal (inter s s') (inter s' s)=true. +Proof. +auto with set. +Qed. + +Lemma inter_subset_equal: + subset s s'=true -> equal (inter s s') s=true. +Proof. +auto with set. +Qed. + +Lemma inter_equal_1: + equal s s'=true -> equal (inter s s'') (inter s' s'')=true. +Proof. +auto with set. +Qed. + +Lemma inter_equal_2: + equal s' s''=true -> equal (inter s s') (inter s s'')=true. +Proof. +auto with set. +Qed. + +Lemma inter_assoc: + equal (inter (inter s s') s'') (inter s (inter s' s''))=true. +Proof. +auto with set. +Qed. + +Lemma union_inter_1: + equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))=true. +Proof. +auto with set. +Qed. + +Lemma union_inter_2: + equal (union (inter s s') s'') (inter (union s s'') (union s' s''))=true. +Proof. +auto with set. +Qed. + +Lemma inter_add_1: mem x s'=true -> + equal (inter (add x s) s') (add x (inter s s'))=true. +Proof. +auto with set. +Qed. + +Lemma inter_add_2: mem x s'=false -> + equal (inter (add x s) s') (inter s s')=true. +Proof. +intros; apply equal_1; apply inter_add_2. +rewrite not_mem_iff; auto. +Qed. + +(* caracterisation of [union] via [subset] *) + +Lemma inter_subset_1: subset (inter s s') s=true. +Proof. +auto with set. +Qed. + +Lemma inter_subset_2: subset (inter s s') s'=true. +Proof. +auto with set. +Qed. + +Lemma inter_subset_3: + subset s'' s=true -> subset s'' s'=true -> + subset s'' (inter s s')=true. +Proof. +intros; apply subset_1; apply inter_subset_3; auto with set. +Qed. + +(** Properties of [diff] *) + +Lemma diff_subset: subset (diff s s') s=true. +Proof. +auto with set. +Qed. + +Lemma diff_subset_equal: + subset s s'=true -> equal (diff s s') empty=true. +Proof. +auto with set. +Qed. + +Lemma remove_inter_singleton: + equal (remove x s) (diff s (singleton x))=true. +Proof. +auto with set. +Qed. + +Lemma diff_inter_empty: + equal (inter (diff s s') (inter s s')) empty=true. +Proof. +auto with set. +Qed. + +Lemma diff_inter_all: + equal (union (diff s s') (inter s s')) s=true. +Proof. +auto with set. +Qed. + +End BasicProperties. + +Hint Immediate empty_mem is_empty_equal_empty add_mem_1 + remove_mem_1 singleton_equal_add union_mem inter_mem + diff_mem equal_sym add_remove remove_add : set. +Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1 + choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal + subset_refl subset_equal subset_antisym + add_mem_3 add_equal remove_mem_3 remove_equal : set. + + +(** General recursion principle *) + +Lemma set_rec: forall (P:t->Type), + (forall s s', equal s s'=true -> P s -> P s') -> + (forall s x, mem x s=false -> P s -> P (add x s)) -> + P empty -> forall s, P s. +Proof. +intros. +apply set_induction; auto; intros. +apply X with empty; auto with set. +apply X with (add x s0); auto with set. +apply equal_1; intro a; rewrite add_iff; rewrite (H0 a); tauto. +apply X0; auto with set; apply mem_3; auto. +Qed. + +(** Properties of [fold] *) + +Lemma exclusive_set : forall s s' x, + ~(In x s/\In x s') <-> mem x s && mem x s'=false. +Proof. +intros; do 2 rewrite mem_iff. +destruct (mem x s); destruct (mem x s'); intuition. +Qed. + +Section Fold. +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). +Variables (s s':t)(x:elt). + +Lemma fold_empty: (fold f empty i) = i. +Proof. +apply fold_empty; auto. +Qed. + +Lemma fold_equal: + equal s s'=true -> eqA (fold f s i) (fold f s' i). +Proof. +intros; apply fold_equal with (eqA:=eqA); auto with set. +Qed. + +Lemma fold_add: + mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)). +Proof. +intros; apply fold_add with (eqA:=eqA); auto. +rewrite not_mem_iff; auto. +Qed. + +Lemma add_fold: + mem x s=true -> eqA (fold f (add x s) i) (fold f s i). +Proof. +intros; apply add_fold with (eqA:=eqA); auto with set. +Qed. + +Lemma remove_fold_1: + mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i). +Proof. +intros; apply remove_fold_1 with (eqA:=eqA); auto with set. +Qed. + +Lemma remove_fold_2: + mem x s=false -> eqA (fold f (remove x s) i) (fold f s i). +Proof. +intros; apply remove_fold_2 with (eqA:=eqA); auto. +rewrite not_mem_iff; auto. +Qed. + +Lemma fold_union: + (forall x, mem x s && mem x s'=false) -> + eqA (fold f (union s s') i) (fold f s (fold f s' i)). +Proof. +intros; apply fold_union with (eqA:=eqA); auto. +intros; rewrite exclusive_set; auto. +Qed. + +End Fold. + +(** Properties of [cardinal] *) + +Lemma add_cardinal_1: + forall s x, mem x s=true -> cardinal (add x s)=cardinal s. +Proof. +auto with set. +Qed. + +Lemma add_cardinal_2: + forall s x, mem x s=false -> cardinal (add x s)=S (cardinal s). +Proof. +intros; apply add_cardinal_2; auto. +rewrite not_mem_iff; auto. +Qed. + +Lemma remove_cardinal_1: + forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s. +Proof. +intros; apply remove_cardinal_1; auto with set. +Qed. + +Lemma remove_cardinal_2: + forall s x, mem x s=false -> cardinal (remove x s)=cardinal s. +Proof. +intros; apply Equal_cardinal; apply equal_2; auto with set. +Qed. + +Lemma union_cardinal: + forall s s', (forall x, mem x s && mem x s'=false) -> + cardinal (union s s')=cardinal s+cardinal s'. +Proof. +intros; apply union_cardinal; auto; intros. +rewrite exclusive_set; auto. +Qed. + +Lemma subset_cardinal: + forall s s', subset s s'=true -> cardinal s<=cardinal s'. +Proof. +intros; apply subset_cardinal; auto with set. +Qed. + +Section Bool. + +(** Properties of [filter] *) + +Variable f:elt->bool. +Variable Comp: compat_bool E.eq f. + +Let Comp' : compat_bool E.eq (fun x =>negb (f x)). +Proof. +unfold compat_bool in *; intros; f_equal; auto. +Qed. + +Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x. +Proof. +intros; apply filter_b; auto. +Qed. + +Lemma for_all_filter: + forall s, for_all f s=is_empty (filter (fun x => negb (f x)) s). +Proof. +intros; apply bool_1; split; intros. +apply is_empty_1. +unfold Empty; intros. +rewrite filter_iff; auto. +red; destruct 1. +rewrite <- (@for_all_iff s f) in H; auto. +rewrite (H a H0) in H1; discriminate. +apply for_all_1; auto; red; intros. +revert H; rewrite <- is_empty_iff. +unfold Empty; intro H; generalize (H x); clear H. +rewrite filter_iff; auto. +destruct (f x); auto. +Qed. + +Lemma exists_filter : + forall s, exists_ f s=negb (is_empty (filter f s)). +Proof. +intros; apply bool_1; split; intros. +destruct (exists_2 Comp H) as (a,(Ha1,Ha2)). +apply bool_6. +red; intros; apply (@is_empty_2 _ H0 a); auto with set. +generalize (@choose_1 (filter f s)) (@choose_2 (filter f s)). +destruct (choose (filter f s)). +intros H0 _; apply exists_1; auto. +exists e; generalize (H0 e); rewrite filter_iff; auto. +intros _ H0. +rewrite (is_empty_1 (H0 (refl_equal None))) in H; auto; discriminate. +Qed. + +Lemma partition_filter_1: + forall s, equal (fst (partition f s)) (filter f s)=true. +Proof. +auto with set. +Qed. + +Lemma partition_filter_2: + forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true. +Proof. +auto with set. +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. +unfold Add, MP.Add; intros. +repeat rewrite filter_iff; auto. +rewrite H0; clear H0. +assert (E.eq x y -> f y = true) by + (intro H0; rewrite <- (Comp _ _ H0); auto). +tauto. +Qed. + +Lemma add_filter_2 : forall s s' x, + f x=false -> (Add x s s') -> filter f s [=] filter f s'. +Proof. +unfold Add, MP.Add, Equal; intros. +repeat rewrite filter_iff; auto. +rewrite H0; clear H0. +assert (f a = true -> ~E.eq x a). + intros H0 H1. + rewrite (Comp _ _ H1) in H. + rewrite H in H0; discriminate. +tauto. +Qed. + +Lemma union_filter: forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) -> + forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s. +Proof. +clear Comp' Comp f. +intros. +assert (compat_bool E.eq (fun x => orb (f x) (g x))). + unfold compat_bool; intros. + rewrite (H x y H1); rewrite (H0 x y H1); auto. +unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto. +assert (f a || g a = true <-> f a = true \/ g a = true). + split; auto with bool. + intro H3; destruct (orb_prop _ _ H3); auto. +tauto. +Qed. + +Lemma filter_union: forall s s', filter f (union s s') [=] union (filter f s) (filter f s'). +Proof. +unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto; set_iff; tauto. +Qed. + +(** Properties of [for_all] *) + +Lemma for_all_mem_1: forall s, + (forall x, (mem x s)=true->(f x)=true) -> (for_all f s)=true. +Proof. +intros. +rewrite for_all_filter; auto. +rewrite is_empty_equal_empty. +apply equal_mem_1;intros. +rewrite filter_b; auto. +rewrite empty_mem. +generalize (H a); case (mem a s);intros;auto. +rewrite H0;auto. +Qed. + +Lemma for_all_mem_2: forall s, + (for_all f s)=true -> forall x,(mem x s)=true -> (f x)=true. +Proof. +intros. +rewrite for_all_filter in H; auto. +rewrite is_empty_equal_empty in H. +generalize (equal_mem_2 _ _ H x). +rewrite filter_b; auto. +rewrite empty_mem. +rewrite H0; simpl;intros. +replace true with (negb false);auto;apply negb_sym;auto. +Qed. + +Lemma for_all_mem_3: + forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false. +Proof. +intros. +apply (bool_eq_ind (for_all f s));intros;auto. +rewrite for_all_filter in H1; auto. +rewrite is_empty_equal_empty in H1. +generalize (equal_mem_2 _ _ H1 x). +rewrite filter_b; auto. +rewrite empty_mem. +rewrite H. +rewrite H0. +simpl;auto. +Qed. + +Lemma for_all_mem_4: + forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false}. +Proof. +intros. +rewrite for_all_filter in H; auto. +destruct (choose_mem_3 _ H) as (x,(H0,H1));intros. +exists x. +rewrite filter_b in H1; auto. +elim (andb_prop _ _ H1). +split;auto. +replace false with (negb true);auto;apply negb_sym;auto. +Qed. + +(** Properties of [exists] *) + +Lemma for_all_exists: + forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s). +Proof. +intros. +rewrite for_all_b; auto. +rewrite exists_b; auto. +induction (elements s); simpl; auto. +destruct (f a); simpl; auto. +Qed. + +End Bool. +Section Bool'. + +Variable f:elt->bool. +Variable Comp: compat_bool E.eq f. + +Let Comp' : compat_bool E.eq (fun x =>negb (f x)). +Proof. +unfold compat_bool in *; intros; f_equal; auto. +Qed. + +Lemma exists_mem_1: + forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false. +Proof. +intros. +rewrite for_all_exists; auto. +rewrite for_all_mem_1;auto with bool. +intros;generalize (H x H0);intros. +symmetry;apply negb_sym;simpl;auto. +Qed. + +Lemma exists_mem_2: + forall s, exists_ f s=false -> forall x, mem x s=true -> f x=false. +Proof. +intros. +rewrite for_all_exists in H; auto. +replace false with (negb true);auto;apply negb_sym;symmetry. +rewrite (for_all_mem_2 (fun x => negb (f x)) Comp' s);simpl;auto. +replace true with (negb false);auto;apply negb_sym;auto. +Qed. + +Lemma exists_mem_3: + forall s x, mem x s=true -> f x=true -> exists_ f s=true. +Proof. +intros. +rewrite for_all_exists; auto. +symmetry;apply negb_sym;simpl. +apply for_all_mem_3 with x;auto. +rewrite H0;auto. +Qed. + +Lemma exists_mem_4: + forall s, exists_ f s=true -> {x:elt | (mem x s)=true /\ (f x)=true}. +Proof. +intros. +rewrite for_all_exists in H; auto. +elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros. +elim p;intros. +exists x;split;auto. +replace true with (negb false);auto;apply negb_sym;auto. +replace false with (negb true);auto;apply negb_sym;auto. +Qed. + +End Bool'. + +Section Sum. + +(** Adding a valuation function on all elements of a set. *) + +Definition sum (f:elt -> nat)(s:t) := fold (fun x => plus (f x)) s 0. +Notation compat_opL := (compat_op E.eq (@Logic.eq _)). +Notation transposeL := (transpose (@Logic.eq _)). + +Lemma sum_plus : + forall f g, compat_nat E.eq f -> compat_nat E.eq g -> + forall s, sum (fun x =>f x+g x) s = sum f s + sum g s. +Proof. +unfold sum. +intros f g Hf Hg. +assert (fc : compat_opL (fun x:elt =>plus (f x))). auto. +assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega. +assert (gc : compat_opL (fun x:elt => plus (g x))). auto. +assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega. +assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). auto. +assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega. +assert (st := gen_st nat). +intros s;pattern s; apply set_rec. +intros. +rewrite <- (fold_equal _ _ st _ fc ft 0 _ _ H). +rewrite <- (fold_equal _ _ st _ gc gt 0 _ _ H). +rewrite <- (fold_equal _ _ st _ fgc fgt 0 _ _ H); auto. +intros; do 3 (rewrite (fold_add _ _ st);auto). +rewrite H0;simpl;omega. +do 3 rewrite fold_empty;auto. +Qed. + +Lemma sum_filter : forall f, (compat_bool E.eq f) -> + forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)). +Proof. +unfold sum; intros f Hf. +assert (st := gen_st nat). +assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))). + red; intros. + rewrite (Hf x x' H); auto. +assert (ct : transposeL (fun x => plus (if f x then 1 else 0))). + red; intros; omega. +intros s;pattern s; apply set_rec. +intros. +change elt with E.t. +rewrite <- (fold_equal _ _ st _ cc ct 0 _ _ H). +rewrite <- (MP.Equal_cardinal (filter_equal Hf (equal_2 H))); auto. +intros; rewrite (fold_add _ _ st _ cc ct); auto. +generalize (@add_filter_1 f Hf s0 (add x s0) x) (@add_filter_2 f Hf s0 (add x s0) x) . +assert (~ In x (filter f s0)). + intro H1; rewrite (mem_1 (filter_1 Hf H1)) in H; discriminate H. +case (f x); simpl; intros. +rewrite (MP.cardinal_2 H1 (H2 (refl_equal true) (MP.Add_add s0 x))); auto. +rewrite <- (MP.Equal_cardinal (H3 (refl_equal false) (MP.Add_add s0 x))); auto. +intros; rewrite fold_empty;auto. +rewrite MP.cardinal_1; auto. +unfold Empty; intros. +rewrite filter_iff; auto; set_iff; tauto. +Qed. + +Lemma fold_compat : + forall (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory _ eqA)) + (f g:elt->A->A), + (compat_op E.eq eqA f) -> (transpose eqA f) -> + (compat_op E.eq eqA g) -> (transpose eqA g) -> + forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) -> + (eqA (fold f s i) (fold g s i)). +Proof. +intros A eqA st f g fc ft gc gt i. +intro s; pattern s; apply set_rec; intros. +trans_st (fold f s0 i). +apply fold_equal with (eqA:=eqA); auto. +rewrite equal_sym; auto. +trans_st (fold g s0 i). +apply H0; intros; apply H1; auto with set. +elim (equal_2 H x); auto with set; intros. +apply fold_equal with (eqA:=eqA); auto with set. +trans_st (f x (fold f s0 i)). +apply fold_add with (eqA:=eqA); auto with set. +trans_st (g x (fold f s0 i)); auto with set. +trans_st (g x (fold g s0 i)); auto with set. +sym_st; apply fold_add with (eqA:=eqA); auto. +do 2 rewrite fold_empty; refl_st. +Qed. + +Lemma sum_compat : + forall f g, compat_nat E.eq f -> compat_nat E.eq g -> + forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s. +intros. +unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto. +red; intros; omega. +red; intros; omega. +Qed. + +End Sum. + +End WEqProperties. + + +(** Now comes a special version dedicated to full sets. For this + one, only one argument [(M:S)] is necessary. *) Module EqProperties (M:S). Module D := OT_as_DT M.E. - Include FSetWeakEqProperties.EqProperties M D. + Include WEqProperties D M. End EqProperties. diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index a433a9d04..2bf0c1cae 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -14,16 +14,491 @@ facts are mainly the specifications of [FSetInterface.S] written using different styles: equivalence and boolean equalities. Moreover, we prove that [E.Eq] and [Equal] are setoid equalities. - - We now simply reuse facts proved for weak sets (those without - order on elements). *) Require Import DecidableTypeEx. -Require Export FSetInterface. -Require FSetWeakFacts. +Require Export FSetInterface. +Set Implicit Arguments. +Unset Strict Implicit. + +(** First, a functor for Weak Sets. Since the signature [WS] includes + an EqualityType and not a stronger DecidableType, this functor + should take two arguments in order to compensate this. *) + +Module WFacts (Import E : DecidableType)(Import M : WSfun E). + +Notation eq_dec := E.eq_dec. +Definition eqb x y := if eq_dec x y then true else false. + +(** * Specifications written using equivalences *) + +Section IffSpec. +Variable s s' s'' : t. +Variable x y z : elt. + +Lemma In_eq_iff : E.eq x y -> (In x s <-> In y s). +Proof. +split; apply In_1; auto. +Qed. + +Lemma mem_iff : In x s <-> mem x s = true. +Proof. +split; [apply mem_1|apply mem_2]. +Qed. + +Lemma not_mem_iff : ~In x s <-> mem x s = false. +Proof. +rewrite mem_iff; destruct (mem x s); intuition. +Qed. + +Lemma equal_iff : s[=]s' <-> equal s s' = true. +Proof. +split; [apply equal_1|apply equal_2]. +Qed. + +Lemma subset_iff : s[<=]s' <-> subset s s' = true. +Proof. +split; [apply subset_1|apply subset_2]. +Qed. + +Lemma empty_iff : In x empty <-> False. +Proof. +intuition; apply (empty_1 H). +Qed. + +Lemma is_empty_iff : Empty s <-> is_empty s = true. +Proof. +split; [apply is_empty_1|apply is_empty_2]. +Qed. + +Lemma singleton_iff : In y (singleton x) <-> E.eq x y. +Proof. +split; [apply singleton_1|apply singleton_2]. +Qed. + +Lemma add_iff : In y (add x s) <-> E.eq x y \/ In y s. +Proof. +split; [ | destruct 1; [apply add_1|apply add_2]]; auto. +destruct (eq_dec x y) as [E|E]; auto. +intro H; right; exact (add_3 E H). +Qed. + +Lemma add_neq_iff : ~ E.eq x y -> (In y (add x s) <-> In y s). +Proof. +split; [apply add_3|apply add_2]; auto. +Qed. + +Lemma remove_iff : In y (remove x s) <-> In y s /\ ~E.eq x y. +Proof. +split; [split; [apply remove_3 with x |] | destruct 1; apply remove_2]; auto. +intro. +apply (remove_1 H0 H). +Qed. + +Lemma remove_neq_iff : ~ E.eq x y -> (In y (remove x s) <-> In y s). +Proof. +split; [apply remove_3|apply remove_2]; auto. +Qed. + +Lemma union_iff : In x (union s s') <-> In x s \/ In x s'. +Proof. +split; [apply union_1 | destruct 1; [apply union_2|apply union_3]]; auto. +Qed. + +Lemma inter_iff : In x (inter s s') <-> In x s /\ In x s'. +Proof. +split; [split; [apply inter_1 with s' | apply inter_2 with s] | destruct 1; apply inter_3]; auto. +Qed. + +Lemma diff_iff : In x (diff s s') <-> In x s /\ ~ In x s'. +Proof. +split; [split; [apply diff_1 with s' | apply diff_2 with s] | destruct 1; apply diff_3]; auto. +Qed. + +Variable f : elt->bool. + +Lemma filter_iff : compat_bool E.eq f -> (In x (filter f s) <-> In x s /\ f x = true). +Proof. +split; [split; [apply filter_1 with f | apply filter_2 with s] | destruct 1; apply filter_3]; auto. +Qed. + +Lemma for_all_iff : compat_bool E.eq f -> + (For_all (fun x => f x = true) s <-> for_all f s = true). +Proof. +split; [apply for_all_1 | apply for_all_2]; auto. +Qed. + +Lemma exists_iff : compat_bool E.eq f -> + (Exists (fun x => f x = true) s <-> exists_ f s = true). +Proof. +split; [apply exists_1 | apply exists_2]; auto. +Qed. + +Lemma elements_iff : In x s <-> InA E.eq x (elements s). +Proof. +split; [apply elements_1 | apply elements_2]. +Qed. + +End IffSpec. + +(** Useful tactic for simplifying expressions like [In y (add x (union s s'))] *) + +Ltac set_iff := + repeat (progress ( + rewrite add_iff || rewrite remove_iff || rewrite singleton_iff + || rewrite union_iff || rewrite inter_iff || rewrite diff_iff + || rewrite empty_iff)). + +(** * Specifications written using boolean predicates *) + +Section BoolSpec. +Variable s s' s'' : t. +Variable x y z : elt. + +Lemma mem_b : E.eq x y -> mem x s = mem y s. +Proof. +intros. +generalize (mem_iff s x) (mem_iff s y)(In_eq_iff s H). +destruct (mem x s); destruct (mem y s); intuition. +Qed. + +Lemma empty_b : mem y empty = false. +Proof. +generalize (empty_iff y)(mem_iff empty y). +destruct (mem y empty); intuition. +Qed. + +Lemma add_b : mem y (add x s) = eqb x y || mem y s. +Proof. +generalize (mem_iff (add x s) y)(mem_iff s y)(add_iff s x y); unfold eqb. +destruct (eq_dec x y); destruct (mem y s); destruct (mem y (add x s)); intuition. +Qed. + +Lemma add_neq_b : ~ E.eq x y -> mem y (add x s) = mem y s. +Proof. +intros; generalize (mem_iff (add x s) y)(mem_iff s y)(add_neq_iff s H). +destruct (mem y s); destruct (mem y (add x s)); intuition. +Qed. + +Lemma remove_b : mem y (remove x s) = mem y s && negb (eqb x y). +Proof. +generalize (mem_iff (remove x s) y)(mem_iff s y)(remove_iff s x y); unfold eqb. +destruct (eq_dec x y); destruct (mem y s); destruct (mem y (remove x s)); simpl; intuition. +Qed. + +Lemma remove_neq_b : ~ E.eq x y -> mem y (remove x s) = mem y s. +Proof. +intros; generalize (mem_iff (remove x s) y)(mem_iff s y)(remove_neq_iff s H). +destruct (mem y s); destruct (mem y (remove x s)); intuition. +Qed. + +Lemma singleton_b : mem y (singleton x) = eqb x y. +Proof. +generalize (mem_iff (singleton x) y)(singleton_iff x y); unfold eqb. +destruct (eq_dec x y); destruct (mem y (singleton x)); intuition. +Qed. + +Lemma union_b : mem x (union s s') = mem x s || mem x s'. +Proof. +generalize (mem_iff (union s s') x)(mem_iff s x)(mem_iff s' x)(union_iff s s' x). +destruct (mem x s); destruct (mem x s'); destruct (mem x (union s s')); intuition. +Qed. + +Lemma inter_b : mem x (inter s s') = mem x s && mem x s'. +Proof. +generalize (mem_iff (inter s s') x)(mem_iff s x)(mem_iff s' x)(inter_iff s s' x). +destruct (mem x s); destruct (mem x s'); destruct (mem x (inter s s')); intuition. +Qed. + +Lemma diff_b : mem x (diff s s') = mem x s && negb (mem x s'). +Proof. +generalize (mem_iff (diff s s') x)(mem_iff s x)(mem_iff s' x)(diff_iff s s' x). +destruct (mem x s); destruct (mem x s'); destruct (mem x (diff s s')); simpl; intuition. +Qed. + +Lemma elements_b : mem x s = existsb (eqb x) (elements s). +Proof. +generalize (mem_iff s x)(elements_iff s x)(existsb_exists (eqb x) (elements s)). +rewrite InA_alt. +destruct (mem x s); destruct (existsb (eqb x) (elements s)); auto; intros. +symmetry. +rewrite H1. +destruct H0 as (H0,_). +destruct H0 as (a,(Ha1,Ha2)); [ intuition |]. +exists a; intuition. +unfold eqb; destruct (eq_dec x a); auto. +rewrite <- H. +rewrite H0. +destruct H1 as (H1,_). +destruct H1 as (a,(Ha1,Ha2)); [intuition|]. +exists a; intuition. +unfold eqb in *; destruct (eq_dec x a); auto; discriminate. +Qed. + +Variable f : elt->bool. + +Lemma filter_b : compat_bool E.eq f -> mem x (filter f s) = mem x s && f x. +Proof. +intros. +generalize (mem_iff (filter f s) x)(mem_iff s x)(filter_iff s x H). +destruct (mem x s); destruct (mem x (filter f s)); destruct (f x); simpl; intuition. +Qed. + +Lemma for_all_b : compat_bool E.eq f -> + for_all f s = forallb f (elements s). +Proof. +intros. +generalize (forallb_forall f (elements s))(for_all_iff s H)(elements_iff s). +unfold For_all. +destruct (forallb f (elements s)); destruct (for_all f s); auto; intros. +rewrite <- H1; intros. +destruct H0 as (H0,_). +rewrite (H2 x0) in H3. +rewrite (InA_alt E.eq x0 (elements s)) in H3. +destruct H3 as (a,(Ha1,Ha2)). +rewrite (H _ _ Ha1). +apply H0; auto. +symmetry. +rewrite H0; intros. +destruct H1 as (_,H1). +apply H1; auto. +rewrite H2. +rewrite InA_alt; eauto. +Qed. + +Lemma exists_b : compat_bool E.eq f -> + exists_ f s = existsb f (elements s). +Proof. +intros. +generalize (existsb_exists f (elements s))(exists_iff s H)(elements_iff s). +unfold Exists. +destruct (existsb f (elements s)); destruct (exists_ f s); auto; intros. +rewrite <- H1; intros. +destruct H0 as (H0,_). +destruct H0 as (a,(Ha1,Ha2)); auto. +exists a; split; auto. +rewrite H2; rewrite InA_alt; eauto. +symmetry. +rewrite H0. +destruct H1 as (_,H1). +destruct H1 as (a,(Ha1,Ha2)); auto. +rewrite (H2 a) in Ha1. +rewrite (InA_alt E.eq a (elements s)) in Ha1. +destruct Ha1 as (b,(Hb1,Hb2)). +exists b; auto. +rewrite <- (H _ _ Hb1); auto. +Qed. + +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. + +Definition Equal_ST : Setoid_Theory t Equal. +Proof. +constructor; [apply eq_refl | apply eq_sym | apply eq_trans]. +Qed. + +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. +unfold Equal; intros x y H s s' H0. +rewrite (In_eq_iff s H); auto. +Qed. + +Add Morphism is_empty : is_empty_m. +Proof. +unfold Equal; intros s s' H. +generalize (is_empty_iff s)(is_empty_iff s'). +destruct (is_empty s); destruct (is_empty s'); + unfold Empty; auto; intros. +symmetry. +rewrite <- H1; intros a Ha. +rewrite <- (H a) in Ha. +destruct H0 as (_,H0). +exact (H0 (refl_equal true) _ Ha). +rewrite <- H0; intros a Ha. +rewrite (H a) in Ha. +destruct H1 as (_,H1). +exact (H1 (refl_equal true) _ Ha). +Qed. + +Add Morphism Empty with signature Equal ==> iff as Empty_m. +Proof. +intros; do 2 rewrite is_empty_iff; rewrite H; intuition. +Qed. + +Add Morphism mem : mem_m. +Proof. +unfold Equal; intros x y H s s' H0. +generalize (H0 x); clear H0; rewrite (In_eq_iff s' H). +generalize (mem_iff s x)(mem_iff s' y). +destruct (mem x s); destruct (mem y s'); intuition. +Qed. + +Add Morphism singleton : singleton_m. +Proof. +unfold Equal; intros x y H a. +do 2 rewrite singleton_iff; split; intros. +apply E.eq_trans with x; auto. +apply E.eq_trans with y; auto. +Qed. + +Add Morphism add : add_m. +Proof. +unfold Equal; intros x y H s s' H0 a. +do 2 rewrite add_iff; rewrite H; rewrite H0; intuition. +Qed. + +Add Morphism remove : remove_m. +Proof. +unfold Equal; intros x y H s s' H0 a. +do 2 rewrite remove_iff; rewrite H; rewrite H0; intuition. +Qed. + +Add Morphism union : union_m. +Proof. +unfold Equal; intros s s' H s'' s''' H0 a. +do 2 rewrite union_iff; rewrite H; rewrite H0; intuition. +Qed. + +Add Morphism inter : inter_m. +Proof. +unfold Equal; intros s s' H s'' s''' H0 a. +do 2 rewrite inter_iff; rewrite H; rewrite H0; intuition. +Qed. + +Add Morphism diff : diff_m. +Proof. +unfold Equal; intros s s' H s'' s''' H0 a. +do 2 rewrite diff_iff; rewrite H; rewrite H0; intuition. +Qed. + +Add Morphism Subset with signature Equal ==> Equal ==> iff as Subset_m. +Proof. +unfold Equal, Subset; firstorder. +Qed. + +Add Morphism subset : subset_m. +Proof. +intros s s' H s'' s''' H0. +generalize (subset_iff s s'') (subset_iff s' s'''). +destruct (subset s s''); destruct (subset s' s'''); auto; intros. +rewrite H in H1; rewrite H0 in H1; intuition. +rewrite H in H1; rewrite H0 in H1; intuition. +Qed. + +Add Morphism equal : equal_m. +Proof. +intros s s' H s'' s''' H0. +generalize (equal_iff s s'') (equal_iff s' s'''). +destruct (equal s s''); destruct (equal s' s'''); auto; intros. +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. Defined. + +Lemma Subset_trans : forall s s' s'', s[<=]s'->s'[<=]s''->s[<=]s''. +Proof. unfold Subset; eauto. Defined. + +Add Relation t Subset + reflexivity proved by Subset_refl + transitivity proved by Subset_trans + as SubsetSetoid. +(* NB: for the moment, it is important to use Defined and not Qed in + the two previous lemmas, in order to allow conversion of + SubsetSetoid coming from separate Facts modules. See bug #1738. *) + +Add Morphism In with signature E.eq ==> Subset ++> impl as In_s_m. +Proof. +unfold Subset, impl; intros; eauto with set. +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. + +(* [fold], [filter], [for_all], [exists_] and [partition] cannot be proved morphism + without additional hypothesis on [f]. For instance: *) + +Lemma filter_equal : forall f, compat_bool E.eq f -> + forall s s', s[=]s' -> filter f s [=] filter f s'. +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]. *) + +(* Later: +Add Morphism cardinal ; cardinal_m. +*) + +End WFacts. + + +(** Now comes a special version dedicated to full sets. For this + one, only one argument [(M:S)] is necessary. *) Module Facts (M:S). - Module D:=OT_as_DT M.E. - Include FSetWeakFacts.Facts M D. + Module D:=OT_as_DT M.E. + Include WFacts D M. End Facts. + diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v index f701dcf12..3ae983641 100644 --- a/theories/FSets/FSetInterface.v +++ b/theories/FSets/FSetInterface.v @@ -12,18 +12,28 @@ (** Set interfaces *) -Require Export Bool OrderedType. +Require Export Bool OrderedType DecidableType. Set Implicit Arguments. Unset Strict Implicit. -(** * Non-dependent signature +(** * Non-dependent signatures - Signature [S] presents sets as purely informative programs - together with axioms *) + The following signatures presents sets as purely informative + programs together with axioms *) -Module Type S. - Declare Module E : OrderedType. + +(** ** Functorial signature for weak sets + + Weak sets are sets without ordering on base elements, only + a decidable equality. *) + +Module Type WSfun (E : EqualityType). + + (** The module E of base objects is meant to be a DecidableType + (and used to be so). But requiring only an EqualityType here + allows subtyping between FSet and FSetWeak *) + Definition elt := E.t. Parameter t : Set. (** the abstract type of sets *) @@ -69,10 +79,10 @@ Module Type S. (** Set difference. *) Definition eq : t -> t -> Prop := Equal. - Parameter lt : t -> t -> Prop. - Parameter compare : forall s s' : t, Compare lt eq s s'. - (** Total ordering between sets. Can be used as the ordering function - for doing sets of sets. *) + (** EqualityType is a subset of this interface, but not + DecidableType, in order to have FSetWeak < FSet. + Hence no weak sets of weak sets in general, but it works + at least with FSetWeakList.make that provides an eq_dec. *) Parameter equal : t -> t -> bool. (** [equal s1 s2] tests whether the sets [s1] and [s2] are @@ -90,7 +100,9 @@ Module Type S. Parameter fold : forall A : Type, (elt -> A -> A) -> t -> A -> A. (** [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)], - where [x1 ... xN] are the elements of [s], in increasing order. *) + where [x1 ... xN] are the elements of [s]. + The order in which elements of [s] are presented to [f] is + unspecified. *) Parameter for_all : (elt -> bool) -> t -> bool. (** [for_all p s] checks if all elements of the set @@ -115,56 +127,38 @@ Module Type S. (** Coq comment: nat instead of int ... *) Parameter elements : t -> list elt. - (** Return the list of all elements of the given set. - The returned list is sorted in increasing order with respect - to the ordering [Ord.compare], where [Ord] is the argument - given to {!Set.Make}. *) - - Parameter min_elt : t -> option elt. - (** Return the smallest element of the given set - (with respect to the [Ord.compare] ordering), or raise - [Not_found] if the set is empty. *) - (** Coq comment: [Not_found] is represented by the option type *) - - Parameter max_elt : t -> option elt. - (** Same as {!Set.S.min_elt}, but returns the largest element of the - given set. *) - (** Coq comment: [Not_found] is represented by the option type *) + (** Return the list of all elements of the given set, in any order. *) Parameter choose : t -> option elt. (** Return one element of the given set, or raise [Not_found] if - the set is empty. Which element is chosen is unspecified, - but equal elements will be chosen for equal sets. *) + the set is empty. Which element is chosen is unspecified. + Equal sets could return different elements. *) (** Coq comment: [Not_found] is represented by the option type *) Section Spec. - Variable s s' s'' : t. + Variable s s' s'': t. Variable x y : elt. (** Specification of [In] *) Parameter In_1 : E.eq x y -> In x s -> In y s. - + (** Specification of [eq] *) 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 [lt] *) - Parameter lt_trans : lt s s' -> lt s' s'' -> lt s s''. - Parameter lt_not_eq : lt 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 equal_1 : s[=]s' -> equal s s' = true. - Parameter equal_2 : equal s s' = true ->s[=]s'. + Parameter equal_1 : Equal s s' -> equal s s' = true. + Parameter equal_2 : equal s s' = true -> Equal s s'. (** Specification of [subset] *) - Parameter subset_1 : s[<=]s' -> subset s s' = true. - Parameter subset_2 : subset s s' = true -> s[<=]s'. + Parameter subset_1 : Subset s s' -> subset s s' = true. + Parameter subset_2 : subset s s' = true -> Subset s s'. (** Specification of [empty] *) Parameter empty_1 : Empty empty. @@ -236,21 +230,90 @@ Module Type S. exists_ f s = true -> Exists (fun x => f x = true) s. (** Specification of [partition] *) - Parameter partition_1 : compat_bool E.eq f -> - fst (partition f s) [=] filter f s. - Parameter partition_2 : compat_bool E.eq f -> - snd (partition f s) [=] filter (fun x => negb (f x)) s. + Parameter partition_1 : + compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s). + Parameter partition_2 : + compat_bool E.eq f -> + Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). End Filter. (** 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. - Parameter elements_3 : sort E.lt (elements s). - (* We add artificially elements_3w, a weaker version of - elements_3, for allowing FSetWeak < FSet subtyping. *) + (** When compared with ordered FSet, here comes the only + property that is really weaker: *) Parameter elements_3w : NoDupA E.eq (elements s). + (** Specification of [choose] *) + Parameter choose_1 : choose s = Some x -> In x s. + Parameter choose_2 : choose s = None -> Empty s. + + End Spec. + + Hint Resolve mem_1 equal_1 subset_1 empty_1 + 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 + : 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 + : set. + +End WSfun. + + + +(** ** Static signature for weak sets + + 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 : EqualityType. + Include Type WSfun E. +End WS. + + + +(** ** Functorial signature for full sets + + Based on [WSfun], plus ordering on sets and [min_elt] and [max_elt] + and some stronger specifications for other functions. *) + +Module Type Sfun (E : OrderedType). + Include Type WSfun E. + + Parameter lt : t -> t -> Prop. + Parameter compare : forall s s' : t, Compare lt eq s s'. + (** Total ordering between sets. Can be used as the ordering function + for doing sets of sets. *) + + Parameter min_elt : t -> option elt. + (** Return the smallest element of the given set + (with respect to the [Ord.compare] ordering), or raise + [Not_found] if the set is empty. *) + (** Coq comment: [Not_found] is represented by the option type *) + + Parameter max_elt : t -> option elt. + (** Same as {!Set.S.min_elt}, but returns the largest element of the + given set. *) + (** Coq comment: [Not_found] is represented by the option type *) + + 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'. + + (** Additionnal specification of [elements] *) + Parameter elements_3 : sort E.lt (elements s). + (** 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. @@ -261,9 +324,7 @@ Module Type 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. - (** Specification of [choose] *) - Parameter choose_1 : choose s = Some x -> In x s. - Parameter choose_2 : choose s = None -> Empty s. + (** Additionnal specification of [choose] *) Parameter choose_equal: (equal s s')=true -> match choose s, choose s' with | Some x, Some x' => E.eq x x' @@ -273,31 +334,42 @@ Module Type S. End Spec. - Hint Resolve mem_1 equal_1 subset_1 empty_1 - 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_3 - : 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 - min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3 - : set. - (** for compatibility with earlier hints *) - Hint Resolve 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 - min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3 - : oldset. - - + Hint Resolve elements_3 : set. + Hint Immediate + min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3 : set. + +End Sfun. + + +(** ** Static signature for full sets + 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. End S. + +(** ** Some subtyping tests + +WSfun ---> WS + | | + | | + V V +Sfun ---> S + +Module S_WS (M : S) <: SW := M. +Module Sfun_WSfun (E:OrderedType)(M : Sfun E) <: WSfun E := M. +Module S_Sfun (E:OrderedType)(M : S with Module E:=E) <: Sfun E := M. +Module WS_WSfun (E:EqualityType)(M : WS with Module E:=E) <: WSfun E := M. +*) + + (** * Dependent signature - Signature [Sdep] presents sets using dependent types *) + Signature [Sdep] presents full sets using dependent types *) Module Type Sdep. @@ -427,7 +499,8 @@ Module Type Sdep. match choose s, choose s' with | inleft (exist x _), inleft (exist x' _) => E.eq x x' | inright _, inright _ => True - | _, _ => False + | _, _ => False end. End Sdep. + diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index dd24d29b4..5525c3ecc 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -16,26 +16,771 @@ [In x s] instead of [mem x s=true], [Equal s s'] instead of [equal s s'=true], etc. *) -Require Export FSetInterface. +Require Export FSetInterface. Require Import DecidableTypeEx FSetFacts FSetDecide. Set Implicit Arguments. Unset Strict Implicit. -Hint Unfold transpose compat_op compat_nat. +Hint Unfold transpose compat_op. Hint Extern 1 (Setoid_Theory _ _) => constructor; congruence. -(** First, the properties that do not rely on the element ordering - are imported verbatim from FSetWeakProperties *) +(** First, a functor for Weak Sets. Since the signature [WS] includes + an EqualityType and not a stronger DecidableType, this functor + should take two arguments in order to compensate this. *) -Require FSetWeakProperties. +Module WProperties (Import E : DecidableType)(M : WSfun E). + Module Import FM := WFacts E M. + Module Import Dec := WDecide E M. + Import M. + + Lemma In_dec : forall x s, {In x s} + {~ In x s}. + Proof. + intros; generalize (mem_iff s x); case (mem x s); intuition. + Qed. + + Definition Add x s s' := forall y, In y s' <-> E.eq x y \/ In y s. + + Lemma Add_Equal : forall x s s', Add x s s' <-> s' [=] add x s. + Proof. + unfold Add. + split; intros. + red; intros. + rewrite H; clear H. + fsetdec. + fsetdec. + Qed. + + Ltac expAdd := repeat rewrite Add_Equal. + + Section BasicProperties. + + Variable s s' s'' s1 s2 s3 : t. + Variable x x' : elt. + + Lemma equal_refl : s[=]s. + Proof. fsetdec. Qed. + + Lemma equal_sym : s[=]s' -> s'[=]s. + Proof. fsetdec. Qed. + + Lemma equal_trans : s1[=]s2 -> s2[=]s3 -> s1[=]s3. + Proof. fsetdec. Qed. + + Lemma subset_refl : s[<=]s. + Proof. fsetdec. Qed. + + Lemma subset_trans : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3. + Proof. fsetdec. Qed. + + Lemma subset_antisym : s[<=]s' -> s'[<=]s -> s[=]s'. + Proof. fsetdec. Qed. + + Lemma subset_equal : s[=]s' -> s[<=]s'. + Proof. fsetdec. Qed. + + Lemma subset_empty : empty[<=]s. + Proof. fsetdec. Qed. + + Lemma subset_remove_3 : s1[<=]s2 -> remove x s1 [<=] s2. + Proof. fsetdec. Qed. + + Lemma subset_diff : s1[<=]s3 -> diff s1 s2 [<=] s3. + Proof. fsetdec. Qed. + + Lemma subset_add_3 : In x s2 -> s1[<=]s2 -> add x s1 [<=] s2. + Proof. fsetdec. Qed. + + Lemma subset_add_2 : s1[<=]s2 -> s1[<=] add x s2. + Proof. fsetdec. Qed. + + Lemma in_subset : In x s1 -> s1[<=]s2 -> In x s2. + Proof. fsetdec. Qed. + + Lemma double_inclusion : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1. + Proof. intuition fsetdec. Qed. + + Lemma empty_is_empty_1 : Empty s -> s[=]empty. + Proof. fsetdec. Qed. + + Lemma empty_is_empty_2 : s[=]empty -> Empty s. + Proof. fsetdec. Qed. + + Lemma add_equal : In x s -> add x s [=] s. + Proof. fsetdec. Qed. + + Lemma add_add : add x (add x' s) [=] add x' (add x s). + Proof. fsetdec. Qed. + + Lemma remove_equal : ~ In x s -> remove x s [=] s. + Proof. fsetdec. Qed. + + Lemma Equal_remove : s[=]s' -> remove x s [=] remove x s'. + Proof. fsetdec. Qed. + + Lemma add_remove : In x s -> add x (remove x s) [=] s. + Proof. fsetdec. Qed. + + Lemma remove_add : ~In x s -> remove x (add x s) [=] s. + Proof. fsetdec. Qed. + + Lemma singleton_equal_add : singleton x [=] add x empty. + Proof. fsetdec. Qed. + + Lemma union_sym : union s s' [=] union s' s. + Proof. fsetdec. Qed. + + Lemma union_subset_equal : s[<=]s' -> union s s' [=] s'. + Proof. fsetdec. Qed. + + Lemma union_equal_1 : s[=]s' -> union s s'' [=] union s' s''. + Proof. fsetdec. Qed. + + Lemma union_equal_2 : s'[=]s'' -> union s s' [=] union s s''. + Proof. fsetdec. Qed. + + Lemma union_assoc : union (union s s') s'' [=] union s (union s' s''). + Proof. fsetdec. Qed. + + Lemma add_union_singleton : add x s [=] union (singleton x) s. + Proof. fsetdec. Qed. + + Lemma union_add : union (add x s) s' [=] add x (union s s'). + Proof. fsetdec. Qed. + + Lemma union_remove_add_1 : + union (remove x s) (add x s') [=] union (add x s) (remove x s'). + Proof. fsetdec. Qed. + + Lemma union_remove_add_2 : In x s -> + union (remove x s) (add x s') [=] union s s'. + Proof. fsetdec. Qed. + + Lemma union_subset_1 : s [<=] union s s'. + Proof. fsetdec. Qed. + + Lemma union_subset_2 : s' [<=] union s s'. + Proof. fsetdec. Qed. + + Lemma union_subset_3 : s[<=]s'' -> s'[<=]s'' -> union s s' [<=] s''. + Proof. fsetdec. Qed. + + Lemma union_subset_4 : s[<=]s' -> union s s'' [<=] union s' s''. + Proof. fsetdec. Qed. + + Lemma union_subset_5 : s[<=]s' -> union s'' s [<=] union s'' s'. + Proof. fsetdec. Qed. + + Lemma empty_union_1 : Empty s -> union s s' [=] s'. + Proof. fsetdec. Qed. + + Lemma empty_union_2 : Empty s -> union s' s [=] s'. + Proof. fsetdec. Qed. + + Lemma not_in_union : ~In x s -> ~In x s' -> ~In x (union s s'). + Proof. fsetdec. Qed. + + Lemma inter_sym : inter s s' [=] inter s' s. + Proof. fsetdec. Qed. + + Lemma inter_subset_equal : s[<=]s' -> inter s s' [=] s. + Proof. fsetdec. Qed. + + Lemma inter_equal_1 : s[=]s' -> inter s s'' [=] inter s' s''. + Proof. fsetdec. Qed. + + Lemma inter_equal_2 : s'[=]s'' -> inter s s' [=] inter s s''. + Proof. fsetdec. Qed. + + Lemma inter_assoc : inter (inter s s') s'' [=] inter s (inter s' s''). + Proof. fsetdec. Qed. + + Lemma union_inter_1 : inter (union s s') s'' [=] union (inter s s'') (inter s' s''). + Proof. fsetdec. Qed. + + Lemma union_inter_2 : union (inter s s') s'' [=] inter (union s s'') (union s' s''). + Proof. fsetdec. Qed. + + Lemma inter_add_1 : In x s' -> inter (add x s) s' [=] add x (inter s s'). + Proof. fsetdec. Qed. + + Lemma inter_add_2 : ~ In x s' -> inter (add x s) s' [=] inter s s'. + Proof. fsetdec. Qed. + + Lemma empty_inter_1 : Empty s -> Empty (inter s s'). + Proof. fsetdec. Qed. + + Lemma empty_inter_2 : Empty s' -> Empty (inter s s'). + Proof. fsetdec. Qed. + + Lemma inter_subset_1 : inter s s' [<=] s. + Proof. fsetdec. Qed. + + Lemma inter_subset_2 : inter s s' [<=] s'. + Proof. fsetdec. Qed. + + Lemma inter_subset_3 : + s''[<=]s -> s''[<=]s' -> s''[<=] inter s s'. + Proof. fsetdec. Qed. + + Lemma empty_diff_1 : Empty s -> Empty (diff s s'). + Proof. fsetdec. Qed. + + Lemma empty_diff_2 : Empty s -> diff s' s [=] s'. + Proof. fsetdec. Qed. + + Lemma diff_subset : diff s s' [<=] s. + Proof. fsetdec. Qed. + + Lemma diff_subset_equal : s[<=]s' -> diff s s' [=] empty. + Proof. fsetdec. Qed. + + Lemma remove_diff_singleton : + remove x s [=] diff s (singleton x). + Proof. fsetdec. Qed. + + Lemma diff_inter_empty : inter (diff s s') (inter s s') [=] empty. + Proof. fsetdec. Qed. + + Lemma diff_inter_all : union (diff s s') (inter s s') [=] s. + Proof. fsetdec. Qed. + + Lemma Add_add : Add x s (add x s). + Proof. expAdd; fsetdec. Qed. + + Lemma Add_remove : In x s -> Add x (remove x s) s. + Proof. expAdd; fsetdec. Qed. + + Lemma union_Add : Add x s s' -> Add x (union s s'') (union s' s''). + Proof. expAdd; fsetdec. Qed. + + Lemma inter_Add : + In x s'' -> Add x s s' -> Add x (inter s s'') (inter s' s''). + Proof. expAdd; fsetdec. Qed. + + Lemma union_Equal : + In x s'' -> Add x s s' -> union s s'' [=] union s' s''. + Proof. expAdd; fsetdec. Qed. + + Lemma inter_Add_2 : + ~In x s'' -> Add x s s' -> inter s s'' [=] inter s' s''. + Proof. expAdd; fsetdec. Qed. + + End BasicProperties. + + Hint Immediate equal_sym add_remove remove_add union_sym inter_sym: set. + Hint Resolve equal_refl equal_trans subset_refl subset_equal subset_antisym + subset_trans subset_empty subset_remove_3 subset_diff subset_add_3 + subset_add_2 in_subset empty_is_empty_1 empty_is_empty_2 add_equal + remove_equal singleton_equal_add union_subset_equal union_equal_1 + union_equal_2 union_assoc add_union_singleton union_add union_subset_1 + union_subset_2 union_subset_3 inter_subset_equal inter_equal_1 inter_equal_2 + inter_assoc union_inter_1 union_inter_2 inter_add_1 inter_add_2 + empty_inter_1 empty_inter_2 empty_union_1 empty_union_2 empty_diff_1 + 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 add_add : set. + + (** * Properties of elements *) + + Lemma elements_Empty : forall s, Empty s <-> elements s = nil. + Proof. + intros. + unfold Empty. + split; intros. + assert (forall a, ~ List.In a (elements s)). + red; intros. + apply (H a). + rewrite elements_iff. + rewrite InA_alt; exists a; auto. + destruct (elements s); auto. + elim (H0 e); simpl; auto. + red; intros. + rewrite elements_iff in H0. + rewrite InA_alt in H0; destruct H0. + rewrite H in H0; destruct H0 as (_,H0); inversion H0. + Qed. + + (** * 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: + *) + + Lemma fold_0 : + forall s (A : Set) (i : A) (f : elt -> A -> A), + exists l : list elt, + NoDup l /\ + (forall x : elt, In x s <-> InA E.eq x l) /\ + fold f s i = fold_right f i l. + Proof. + intros; exists (rev (elements s)); split. + apply NoDupA_rev; auto with set. + exact E.eq_trans. + split; intros. + rewrite elements_iff; do 2 rewrite InA_alt. + split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition. + rewrite fold_left_rev_right. + apply fold_1. + Qed. + + (** An alternate (and previous) specification for [fold] was based on + the recursive structure of a set. It is now lemmas [fold_1] and + [fold_2]. *) + + Lemma fold_1 : + forall s (A : Set) (eqA : A -> A -> Prop) + (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A), + Empty s -> eqA (fold f s i) i. + Proof. + unfold Empty; intros; destruct (fold_0 s i f) as (l,(H1, (H2, H3))). + rewrite H3; clear H3. + generalize H H2; clear H H2; case l; simpl; intros. + refl_st. + elim (H e). + elim (H2 e); intuition. + Qed. + + Lemma fold_2 : + forall s s' x (A : Set) (eqA : A -> A -> Prop) + (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A), + compat_op E.eq eqA f -> + transpose eqA f -> + ~ In x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)). + Proof. + 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:=E.eq)(eqB:=eqA); auto. + eauto. + rewrite <- Hl1; auto. + intros a; rewrite InA_cons; rewrite <- Hl1; rewrite <- Hl'1; + rewrite (H2 a); intuition. + Qed. + + (** In fact, [fold] on empty sets is more than equivalent to + the initial element, it is Leibniz-equal to it. *) + + Lemma fold_1b : + forall s (A : Set)(i : A) (f : elt -> A -> A), + Empty s -> (fold f s i) = i. + Proof. + intros. + rewrite M.fold_1. + rewrite elements_Empty in H; rewrite H; simpl; auto. + Qed. + + (** Similar specifications for [cardinal]. *) + + Lemma cardinal_fold : forall s, cardinal s = fold (fun _ => S) s 0. + Proof. + intros; rewrite cardinal_1; rewrite M.fold_1. + symmetry; apply fold_left_length; auto. + Qed. + + Lemma cardinal_0 : + forall s, exists l : list elt, + NoDupA E.eq l /\ + (forall x : elt, In x s <-> InA E.eq x l) /\ + cardinal s = length l. + Proof. + intros; exists (elements s); intuition; apply cardinal_1. + Qed. + + Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0. + Proof. + intros; rewrite cardinal_fold; apply fold_1; auto. + Qed. + + Lemma cardinal_2 : + forall s s' x, ~ In x s -> Add x s s' -> cardinal s' = S (cardinal s). + Proof. + intros; do 2 rewrite cardinal_fold. + change S with ((fun _ => S) x). + apply fold_2; auto. + Qed. + + End Old_Spec_Now_Properties. + + (** * Induction principle over sets *) + + Lemma cardinal_Empty : forall s, Empty s <-> cardinal s = 0. + Proof. + intros. + rewrite elements_Empty, M.cardinal_1. + destruct (elements s); intuition; discriminate. + Qed. + + Lemma cardinal_inv_1 : forall s, cardinal s = 0 -> Empty s. + Proof. + intros; rewrite cardinal_Empty; auto. + Qed. + Hint Resolve cardinal_inv_1. + + Lemma cardinal_inv_2 : + forall s n, cardinal s = S n -> { x : elt | In x s }. + Proof. + intros; rewrite M.cardinal_1 in H. + generalize (elements_2 (s:=s)). + destruct (elements s); try discriminate. + exists e; auto. + Qed. + + Lemma cardinal_inv_2b : + forall s, cardinal s <> 0 -> { x : elt | In x s }. + Proof. + intro; generalize (@cardinal_inv_2 s); destruct cardinal; + [intuition|eauto]. + Qed. + + Lemma Equal_cardinal : forall s s', s[=]s' -> cardinal s = cardinal s'. + Proof. + symmetry. + remember (cardinal s) as n; symmetry in Heqn; revert s s' Heqn H. + induction n; intros. + apply cardinal_1; rewrite <- H; auto. + destruct (cardinal_inv_2 Heqn) as (x,H2). + revert Heqn. + rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); auto with set. + rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); eauto with set. + Qed. + + Add Morphism cardinal : cardinal_m. + Proof. + exact Equal_cardinal. + Qed. + + Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal. + + Lemma set_induction : + forall P : t -> Type, + (forall s : t, Empty s -> P s) -> + (forall s s' : t, P s -> forall x : elt, ~In 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; auto. + destruct (cardinal_inv_2 (sym_eq Heqn)) as (x,H0). + apply X0 with (remove x s) x; auto with set. + apply IHn; auto. + assert (S n = S (cardinal (remove x s))). + rewrite Heqn; apply cardinal_2 with x; auto with set. + inversion H; auto. + Qed. + + (** Other properties of [fold]. *) + + Section Fold. + 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). + + Section Fold_1. + Variable i i':A. + + Lemma fold_empty : (fold f empty i) = i. + Proof. + apply fold_1b; auto with set. + Qed. + + Lemma fold_equal : + forall s s', s[=]s' -> eqA (fold f s i) (fold f s' i). + Proof. + intros s; pattern s; apply set_induction; clear s; intros. + trans_st i. + apply fold_1; auto. + sym_st; apply fold_1; auto. + rewrite <- H0; auto. + trans_st (f x (fold f s i)). + apply fold_2 with (eqA := eqA); auto. + sym_st; apply fold_2 with (eqA := eqA); auto. + unfold Add in *; intros. + rewrite <- H2; auto. + Qed. + + Lemma fold_add : forall s x, ~In x s -> + eqA (fold f (add x s) i) (f x (fold f s i)). + Proof. + intros; apply fold_2 with (eqA := eqA); auto. + Qed. + + Lemma add_fold : forall s x, In x s -> + eqA (fold f (add x s) i) (fold f s i). + Proof. + intros; apply fold_equal; auto with set. + Qed. + + Lemma remove_fold_1: forall s x, In x s -> + eqA (f x (fold f (remove x s) i)) (fold f s i). + Proof. + intros. + sym_st. + apply fold_2 with (eqA:=eqA); auto with set. + Qed. + + Lemma remove_fold_2: forall s x, ~In x s -> + eqA (fold f (remove x s) i) (fold f s i). + Proof. + intros. + apply fold_equal; auto with set. + Qed. + + Lemma fold_commutes : forall s x, + eqA (fold f s (f x i)) (f x (fold f s i)). + Proof. + intros; pattern s; apply set_induction; clear s; intros. + trans_st (f x i). + apply fold_1; auto. + sym_st. + apply Comp; auto. + apply fold_1; auto. + trans_st (f x0 (fold f s (f x i))). + apply fold_2 with (eqA:=eqA); auto. + trans_st (f x0 (f x (fold f s i))). + trans_st (f x (f x0 (fold f s i))). + apply Comp; auto. + sym_st. + apply fold_2 with (eqA:=eqA); auto. + Qed. + + Lemma fold_init : forall s, eqA i i' -> + eqA (fold f s i) (fold f s i'). + Proof. + intros; pattern s; apply set_induction; clear s; intros. + trans_st i. + apply fold_1; auto. + trans_st i'. + sym_st; apply fold_1; auto. + trans_st (f x (fold f s i)). + apply fold_2 with (eqA:=eqA); auto. + trans_st (f x (fold f s i')). + sym_st; apply fold_2 with (eqA:=eqA); auto. + Qed. + + End Fold_1. + Section Fold_2. + Variable i:A. + + Lemma fold_union_inter : forall s s', + eqA (fold f (union s s') (fold f (inter s s') i)) + (fold f s (fold f s' i)). + Proof. + intros; pattern s; apply set_induction; clear s; intros. + trans_st (fold f s' (fold f (inter s s') i)). + apply fold_equal; auto with set. + trans_st (fold f s' i). + apply fold_init; auto. + apply fold_1; auto with set. + sym_st; apply fold_1; auto. + rename s'0 into s''. + destruct (In_dec x s'). + (* In x s' *) + trans_st (fold f (union s'' s') (f x (fold f (inter s s') i))); auto with set. + apply fold_init; auto. + apply fold_2 with (eqA:=eqA); auto with set. + rewrite inter_iff; intuition. + trans_st (f x (fold f s (fold f s' i))). + trans_st (fold f (union s s') (f x (fold f (inter s s') i))). + apply fold_equal; auto. + apply equal_sym; apply union_Equal with x; auto with set. + trans_st (f x (fold f (union s s') (fold f (inter s s') i))). + apply fold_commutes; auto. + sym_st; apply fold_2 with (eqA:=eqA); auto. + (* ~(In x s') *) + trans_st (f x (fold f (union s s') (fold f (inter s'' s') i))). + apply fold_2 with (eqA:=eqA); auto with set. + trans_st (f x (fold f (union s s') (fold f (inter s s') i))). + apply Comp;auto. + apply fold_init;auto. + apply fold_equal;auto. + apply equal_sym; apply inter_Add_2 with x; auto with set. + trans_st (f x (fold f s (fold f s' i))). + sym_st; apply fold_2 with (eqA:=eqA); auto. + Qed. + + End Fold_2. + Section Fold_3. + Variable i:A. + + Lemma fold_diff_inter : forall s s', + eqA (fold f (diff s s') (fold f (inter s s') i)) (fold f s i). + Proof. + intros. + trans_st (fold f (union (diff s s') (inter s s')) + (fold f (inter (diff s s') (inter s s')) i)). + sym_st; apply fold_union_inter; auto. + trans_st (fold f s (fold f (inter (diff s s') (inter s s')) i)). + apply fold_equal; auto with set. + apply fold_init; auto. + apply fold_1; auto with set. + Qed. + + Lemma fold_union: forall s s', + (forall x, ~(In x s/\In x s')) -> + eqA (fold f (union s s') i) (fold f s (fold f s' i)). + Proof. + intros. + trans_st (fold f (union s s') (fold f (inter s s') i)). + apply fold_init; auto. + sym_st; apply fold_1; auto with set. + unfold Empty; intro a; generalize (H a); set_iff; tauto. + apply fold_union_inter; auto. + Qed. + + End Fold_3. + End Fold. + + Lemma fold_plus : + 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 (@Logic.eq _) (fun _ => S)) by (unfold compat_op; auto). + assert (fp : transpose (@Logic.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. + assert (forall p s', Add x s s' -> fold (fun _ => S) s' p = S (fold (fun _ => S) s p)). + change S with ((fun _ => S) x). + intros; apply fold_2; auto. + rewrite H2; auto. + rewrite (H2 0); auto. + rewrite H. + simpl; auto. + Qed. + + (** more properties of [cardinal] *) + + Lemma empty_cardinal : cardinal empty = 0. + Proof. + rewrite cardinal_fold; apply fold_1; auto with set. + Qed. + + Hint Immediate empty_cardinal cardinal_1 : set. + + Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1. + Proof. + intros. + rewrite (singleton_equal_add x). + replace 0 with (cardinal empty); auto with set. + apply cardinal_2 with x; auto with set. + Qed. + + Hint Resolve singleton_cardinal: set. + + Lemma diff_inter_cardinal : + forall s s', cardinal (diff s s') + cardinal (inter s s') = cardinal s . + Proof. + intros; do 3 rewrite cardinal_fold. + rewrite <- fold_plus. + apply fold_diff_inter with (eqA:=@Logic.eq nat); auto. + Qed. + + Lemma union_cardinal: + forall s s', (forall x, ~(In x s/\In x s')) -> + cardinal (union s s')=cardinal s+cardinal s'. + Proof. + intros; do 3 rewrite cardinal_fold. + rewrite <- fold_plus. + apply fold_union; auto. + Qed. + + Lemma subset_cardinal : + forall s s', s[<=]s' -> cardinal s <= cardinal s' . + Proof. + intros. + rewrite <- (diff_inter_cardinal s' s). + rewrite (inter_sym s' s). + rewrite (inter_subset_equal H); auto with arith. + Qed. + + 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. + do 4 rewrite cardinal_fold. + do 2 rewrite <- fold_plus. + apply fold_union_inter with (eqA:=@Logic.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. + intros; generalize (union_inter_cardinal s s'). + intros; rewrite <- H; auto with arith. + Qed. + + Lemma add_cardinal_1 : + forall s x, In x s -> cardinal (add x s) = cardinal s. + Proof. + auto with set. + Qed. + + Lemma add_cardinal_2 : + forall s x, ~In x s -> cardinal (add x s) = S (cardinal s). + Proof. + intros. + do 2 rewrite cardinal_fold. + change S with ((fun _ => S) x); + apply fold_add with (eqA:=@Logic.eq nat); auto. + Qed. + + Lemma remove_cardinal_1 : + forall s x, In x s -> S (cardinal (remove x s)) = cardinal s. + Proof. + intros. + do 2 rewrite cardinal_fold. + change S with ((fun _ =>S) x). + apply remove_fold_1 with (eqA:=@Logic.eq nat); auto. + Qed. + + Lemma remove_cardinal_2 : + forall s x, ~In x s -> cardinal (remove x s) = cardinal s. + Proof. + auto with set. + Qed. + + Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2. + +End WProperties. + + +(** A clone of [WProperties] working on full sets. *) Module Properties (M:S). Module D := OT_as_DT M.E. - Include FSetWeakProperties.Properties M D. + Include WProperties D M. End Properties. + (** Now comes some properties specific to the element ordering, - invalid in FSetWeak. *) + invalid for Weak Sets. *) Module OrdProperties (M:S). Module ME:=OrderedTypeFacts(M.E). diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v index de483f158..8c48bc24d 100644 --- a/theories/FSets/FSetToFiniteSet.v +++ b/theories/FSets/FSetToFiniteSet.v @@ -14,13 +14,13 @@ (* $Id$ *) Require Import Ensembles Finite_sets. -Require Import FSetInterface FSetProperties OrderedTypeEx. +Require Import FSetInterface FSetProperties OrderedTypeEx DecidableTypeEx. (** * Going from [FSets] with usual equality to the old [Ensembles] and [Finite_sets] theory. *) -Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U). - Module MP:= Properties(M). +Module WS_to_Finite_set (U:UsualDecidableType)(M: WSfun U). + Module MP:= WProperties U M. Import M MP FM Ensembles Finite_sets. Definition mkEns : M.t -> Ensemble M.elt := @@ -82,7 +82,7 @@ Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U). Lemma add_Add : forall x s, !!(add x s) === Add _ (!!s) x. Proof. unfold Same_set, Included, mkEns, In. - split; intro; set_iff; inversion 1; unfold E.eq; auto with sets. + split; intro; set_iff; inversion 1; auto with sets. inversion H0. constructor 2; constructor. constructor 1; auto. @@ -97,7 +97,7 @@ Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U). inversion H0. constructor 2; constructor. constructor 1; auto. - red in H; rewrite H; unfold E.eq in *. + red in H; rewrite H. inversion H0; auto. inversion H1; auto. Qed. @@ -105,7 +105,7 @@ Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U). Lemma remove_Subtract : forall x s, !!(remove x s) === Subtract _ (!!s) x. Proof. unfold Same_set, Included, mkEns, In. - split; intro; set_iff; inversion 1; unfold E.eq in *; auto with sets. + split; intro; set_iff; inversion 1; auto with sets. split; auto. contradict H1. inversion H1; auto. @@ -136,4 +136,10 @@ Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U). apply Add_Add; auto. Qed. +End WS_to_Finite_set. + + +Module S_to_Finite_set (U:UsualOrderedType)(M: Sfun U). + Module D := OT_as_DT U. + Include WS_to_Finite_set D M. End S_to_Finite_set. diff --git a/theories/FSets/FSetWeak.v b/theories/FSets/FSetWeak.v deleted file mode 100644 index 080f2a4c2..000000000 --- a/theories/FSets/FSetWeak.v +++ /dev/null @@ -1,16 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(* $Id$ *) - -Require Export DecidableType. -Require Export DecidableTypeEx. -Require Export FSetWeakInterface. -Require Export FSetWeakFacts. -Require Export FSetWeakProperties. -Require Export FSetWeakList. diff --git a/theories/FSets/FSetWeakEqProperties.v b/theories/FSets/FSetWeakEqProperties.v deleted file mode 100644 index d5fa13bdd..000000000 --- a/theories/FSets/FSetWeakEqProperties.v +++ /dev/null @@ -1,934 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(* $Id$ *) - -(** * Finite sets library *) - -(** This module proves many properties of finite sets that - are consequences of the axiomatization in [FsetInterface] - Contrary to the functor in [FsetWeakProperties] it uses - sets operations instead of predicates over sets, i.e. - [mem x s=true] instead of [In x s], - [equal s s'=true] instead of [Equal s s'], etc. *) - -Require Import FSetWeakProperties Zerob Sumbool Omega. - -Module EqProperties - (M:S) - (D:DecidableType with Definition t:=M.E.t - with Definition eq:=M.E.eq). -Module Import MP := Properties M D. -Import FM. -Import M.E. -Import M. - -Definition Add := MP.Add. - -Section BasicProperties. - -(** Some old specifications written with boolean equalities. *) - -Variable s s' s'': t. -Variable x y z : elt. - -Lemma mem_eq: - E.eq x y -> mem x s=mem y s. -Proof. -intro H; rewrite H; auto. -Qed. - -Lemma equal_mem_1: - (forall a, mem a s=mem a s') -> equal s s'=true. -Proof. -intros; apply equal_1; unfold Equal; intros. -do 2 rewrite mem_iff; rewrite H; tauto. -Qed. - -Lemma equal_mem_2: - equal s s'=true -> forall a, mem a s=mem a s'. -Proof. -intros; rewrite (equal_2 H); auto. -Qed. - -Lemma subset_mem_1: - (forall a, mem a s=true->mem a s'=true) -> subset s s'=true. -Proof. -intros; apply subset_1; unfold Subset; intros a. -do 2 rewrite mem_iff; auto. -Qed. - -Lemma subset_mem_2: - subset s s'=true -> forall a, mem a s=true -> mem a s'=true. -Proof. -intros H a; do 2 rewrite <- mem_iff; apply subset_2; auto. -Qed. - -Lemma empty_mem: mem x empty=false. -Proof. -rewrite <- not_mem_iff; auto with set. -Qed. - -Lemma is_empty_equal_empty: is_empty s = equal s empty. -Proof. -apply bool_1; split; intros. -rewrite <- (empty_is_empty_1 (s:=empty)); auto with set. -rewrite <- is_empty_iff; auto with set. -Qed. - -Lemma choose_mem_1: choose s=Some x -> mem x s=true. -Proof. -auto with set. -Qed. - -Lemma choose_mem_2: choose s=None -> is_empty s=true. -Proof. -auto with set. -Qed. - -Lemma add_mem_1: mem x (add x s)=true. -Proof. -auto with set. -Qed. - -Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s. -Proof. -apply add_neq_b. -Qed. - -Lemma remove_mem_1: mem x (remove x s)=false. -Proof. -rewrite <- not_mem_iff; auto with set. -Qed. - -Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s. -Proof. -apply remove_neq_b. -Qed. - -Lemma singleton_equal_add: - equal (singleton x) (add x empty)=true. -Proof. -rewrite (singleton_equal_add x); auto with set. -Qed. - -Lemma union_mem: - mem x (union s s')=mem x s || mem x s'. -Proof. -apply union_b. -Qed. - -Lemma inter_mem: - mem x (inter s s')=mem x s && mem x s'. -Proof. -apply inter_b. -Qed. - -Lemma diff_mem: - mem x (diff s s')=mem x s && negb (mem x s'). -Proof. -apply diff_b. -Qed. - -(** properties of [mem] *) - -Lemma mem_3 : ~In x s -> mem x s=false. -Proof. -intros; rewrite <- not_mem_iff; auto. -Qed. - -Lemma mem_4 : mem x s=false -> ~In x s. -Proof. -intros; rewrite not_mem_iff; auto. -Qed. - -(** Properties of [equal] *) - -Lemma equal_refl: equal s s=true. -Proof. -auto with set. -Qed. - -Lemma equal_sym: equal s s'=equal s' s. -Proof. -intros; apply bool_1; do 2 rewrite <- equal_iff; intuition. -Qed. - -Lemma equal_trans: - equal s s'=true -> equal s' s''=true -> equal s s''=true. -Proof. -intros; rewrite (equal_2 H); auto. -Qed. - -Lemma equal_equal: - equal s s'=true -> equal s s''=equal s' s''. -Proof. -intros; rewrite (equal_2 H); auto. -Qed. - -Lemma equal_cardinal: - equal s s'=true -> cardinal s=cardinal s'. -Proof. -auto with set. -Qed. - -(* Properties of [subset] *) - -Lemma subset_refl: subset s s=true. -Proof. -auto with set. -Qed. - -Lemma subset_antisym: - subset s s'=true -> subset s' s=true -> equal s s'=true. -Proof. -auto with set. -Qed. - -Lemma subset_trans: - subset s s'=true -> subset s' s''=true -> subset s s''=true. -Proof. -do 3 rewrite <- subset_iff; intros. -apply subset_trans with s'; auto. -Qed. - -Lemma subset_equal: - equal s s'=true -> subset s s'=true. -Proof. -auto with set. -Qed. - -(** Properties of [choose] *) - -Lemma choose_mem_3: - is_empty s=false -> {x:elt|choose s=Some x /\ mem x s=true}. -Proof. -intros. -generalize (@choose_1 s) (@choose_2 s). -destruct (choose s);intros. -exists e;auto with set. -generalize (H1 (refl_equal None)); clear H1. -intros; rewrite (is_empty_1 H1) in H; discriminate. -Qed. - -Lemma choose_mem_4: choose empty=None. -Proof. -generalize (@choose_1 empty). -case (@choose empty);intros;auto. -elim (@empty_1 e); auto. -Qed. - -(** Properties of [add] *) - -Lemma add_mem_3: - mem y s=true -> mem y (add x s)=true. -Proof. -auto with set. -Qed. - -Lemma add_equal: - mem x s=true -> equal (add x s) s=true. -Proof. -auto with set. -Qed. - -(** Properties of [remove] *) - -Lemma remove_mem_3: - mem y (remove x s)=true -> mem y s=true. -Proof. -rewrite remove_b; intros H;destruct (andb_prop _ _ H); auto. -Qed. - -Lemma remove_equal: - mem x s=false -> equal (remove x s) s=true. -Proof. -intros; apply equal_1; apply remove_equal. -rewrite not_mem_iff; auto. -Qed. - -Lemma add_remove: - mem x s=true -> equal (add x (remove x s)) s=true. -Proof. -intros; apply equal_1; apply add_remove; auto with set. -Qed. - -Lemma remove_add: - mem x s=false -> equal (remove x (add x s)) s=true. -Proof. -intros; apply equal_1; apply remove_add; auto. -rewrite not_mem_iff; auto. -Qed. - -(** Properties of [is_empty] *) - -Lemma is_empty_cardinal: is_empty s = zerob (cardinal s). -Proof. -intros; apply bool_1; split; intros. -rewrite MP.cardinal_1; simpl; auto with set. -assert (cardinal s = 0) by (apply zerob_true_elim; auto). -auto with set. -Qed. - -(** Properties of [singleton] *) - -Lemma singleton_mem_1: mem x (singleton x)=true. -Proof. -auto with set. -Qed. - -Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false. -Proof. -intros; rewrite singleton_b. -unfold eqb; destruct (eq_dec x y); intuition. -Qed. - -Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y. -Proof. -intros; apply singleton_1; auto with set. -Qed. - -(** Properties of [union] *) - -Lemma union_sym: - equal (union s s') (union s' s)=true. -Proof. -auto with set. -Qed. - -Lemma union_subset_equal: - subset s s'=true -> equal (union s s') s'=true. -Proof. -auto with set. -Qed. - -Lemma union_equal_1: - equal s s'=true-> equal (union s s'') (union s' s'')=true. -Proof. -auto with set. -Qed. - -Lemma union_equal_2: - equal s' s''=true-> equal (union s s') (union s s'')=true. -Proof. -auto with set. -Qed. - -Lemma union_assoc: - equal (union (union s s') s'') (union s (union s' s''))=true. -Proof. -auto with set. -Qed. - -Lemma add_union_singleton: - equal (add x s) (union (singleton x) s)=true. -Proof. -auto with set. -Qed. - -Lemma union_add: - equal (union (add x s) s') (add x (union s s'))=true. -Proof. -auto with set. -Qed. - -(* caracterisation of [union] via [subset] *) - -Lemma union_subset_1: subset s (union s s')=true. -Proof. -auto with set. -Qed. - -Lemma union_subset_2: subset s' (union s s')=true. -Proof. -auto with set. -Qed. - -Lemma union_subset_3: - subset s s''=true -> subset s' s''=true -> - subset (union s s') s''=true. -Proof. -intros; apply subset_1; apply union_subset_3; auto with set. -Qed. - -(** Properties of [inter] *) - -Lemma inter_sym: equal (inter s s') (inter s' s)=true. -Proof. -auto with set. -Qed. - -Lemma inter_subset_equal: - subset s s'=true -> equal (inter s s') s=true. -Proof. -auto with set. -Qed. - -Lemma inter_equal_1: - equal s s'=true -> equal (inter s s'') (inter s' s'')=true. -Proof. -auto with set. -Qed. - -Lemma inter_equal_2: - equal s' s''=true -> equal (inter s s') (inter s s'')=true. -Proof. -auto with set. -Qed. - -Lemma inter_assoc: - equal (inter (inter s s') s'') (inter s (inter s' s''))=true. -Proof. -auto with set. -Qed. - -Lemma union_inter_1: - equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))=true. -Proof. -auto with set. -Qed. - -Lemma union_inter_2: - equal (union (inter s s') s'') (inter (union s s'') (union s' s''))=true. -Proof. -auto with set. -Qed. - -Lemma inter_add_1: mem x s'=true -> - equal (inter (add x s) s') (add x (inter s s'))=true. -Proof. -auto with set. -Qed. - -Lemma inter_add_2: mem x s'=false -> - equal (inter (add x s) s') (inter s s')=true. -Proof. -intros; apply equal_1; apply inter_add_2. -rewrite not_mem_iff; auto. -Qed. - -(* caracterisation of [union] via [subset] *) - -Lemma inter_subset_1: subset (inter s s') s=true. -Proof. -auto with set. -Qed. - -Lemma inter_subset_2: subset (inter s s') s'=true. -Proof. -auto with set. -Qed. - -Lemma inter_subset_3: - subset s'' s=true -> subset s'' s'=true -> - subset s'' (inter s s')=true. -Proof. -intros; apply subset_1; apply inter_subset_3; auto with set. -Qed. - -(** Properties of [diff] *) - -Lemma diff_subset: subset (diff s s') s=true. -Proof. -auto with set. -Qed. - -Lemma diff_subset_equal: - subset s s'=true -> equal (diff s s') empty=true. -Proof. -auto with set. -Qed. - -Lemma remove_inter_singleton: - equal (remove x s) (diff s (singleton x))=true. -Proof. -auto with set. -Qed. - -Lemma diff_inter_empty: - equal (inter (diff s s') (inter s s')) empty=true. -Proof. -auto with set. -Qed. - -Lemma diff_inter_all: - equal (union (diff s s') (inter s s')) s=true. -Proof. -auto with set. -Qed. - -End BasicProperties. - -Hint Immediate empty_mem is_empty_equal_empty add_mem_1 - remove_mem_1 singleton_equal_add union_mem inter_mem - diff_mem equal_sym add_remove remove_add : set. -Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1 - choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal - subset_refl subset_equal subset_antisym - add_mem_3 add_equal remove_mem_3 remove_equal : set. - - -(** General recursion principle *) - -Lemma set_rec: forall (P:t->Type), - (forall s s', equal s s'=true -> P s -> P s') -> - (forall s x, mem x s=false -> P s -> P (add x s)) -> - P empty -> forall s, P s. -Proof. -intros. -apply set_induction; auto; intros. -apply X with empty; auto with set. -apply X with (add x s0); auto with set. -apply equal_1; intro a; rewrite add_iff; rewrite (H0 a); tauto. -apply X0; auto with set; apply mem_3; auto. -Qed. - -(** Properties of [fold] *) - -Lemma exclusive_set : forall s s' x, - ~(In x s/\In x s') <-> mem x s && mem x s'=false. -Proof. -intros; do 2 rewrite mem_iff. -destruct (mem x s); destruct (mem x s'); intuition. -Qed. - -Section Fold. -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). -Variables (s s':t)(x:elt). - -Lemma fold_empty: (fold f empty i) = i. -Proof. -apply fold_empty; auto. -Qed. - -Lemma fold_equal: - equal s s'=true -> eqA (fold f s i) (fold f s' i). -Proof. -intros; apply fold_equal with (eqA:=eqA); auto with set. -Qed. - -Lemma fold_add: - mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)). -Proof. -intros; apply fold_add with (eqA:=eqA); auto. -rewrite not_mem_iff; auto. -Qed. - -Lemma add_fold: - mem x s=true -> eqA (fold f (add x s) i) (fold f s i). -Proof. -intros; apply add_fold with (eqA:=eqA); auto with set. -Qed. - -Lemma remove_fold_1: - mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i). -Proof. -intros; apply remove_fold_1 with (eqA:=eqA); auto with set. -Qed. - -Lemma remove_fold_2: - mem x s=false -> eqA (fold f (remove x s) i) (fold f s i). -Proof. -intros; apply remove_fold_2 with (eqA:=eqA); auto. -rewrite not_mem_iff; auto. -Qed. - -Lemma fold_union: - (forall x, mem x s && mem x s'=false) -> - eqA (fold f (union s s') i) (fold f s (fold f s' i)). -Proof. -intros; apply fold_union with (eqA:=eqA); auto. -intros; rewrite exclusive_set; auto. -Qed. - -End Fold. - -(** Properties of [cardinal] *) - -Lemma add_cardinal_1: - forall s x, mem x s=true -> cardinal (add x s)=cardinal s. -Proof. -auto with set. -Qed. - -Lemma add_cardinal_2: - forall s x, mem x s=false -> cardinal (add x s)=S (cardinal s). -Proof. -intros; apply add_cardinal_2; auto. -rewrite not_mem_iff; auto. -Qed. - -Lemma remove_cardinal_1: - forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s. -Proof. -intros; apply remove_cardinal_1; auto with set. -Qed. - -Lemma remove_cardinal_2: - forall s x, mem x s=false -> cardinal (remove x s)=cardinal s. -Proof. -intros; apply Equal_cardinal; apply equal_2; auto with set. -Qed. - -Lemma union_cardinal: - forall s s', (forall x, mem x s && mem x s'=false) -> - cardinal (union s s')=cardinal s+cardinal s'. -Proof. -intros; apply union_cardinal; auto; intros. -rewrite exclusive_set; auto. -Qed. - -Lemma subset_cardinal: - forall s s', subset s s'=true -> cardinal s<=cardinal s'. -Proof. -intros; apply subset_cardinal; auto with set. -Qed. - -Section Bool. - -(** Properties of [filter] *) - -Variable f:elt->bool. -Variable Comp: compat_bool E.eq f. - -Let Comp' : compat_bool E.eq (fun x =>negb (f x)). -Proof. -unfold compat_bool in *; intros; f_equal; auto. -Qed. - -Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x. -Proof. -intros; apply filter_b; auto. -Qed. - -Lemma for_all_filter: - forall s, for_all f s=is_empty (filter (fun x => negb (f x)) s). -Proof. -intros; apply bool_1; split; intros. -apply is_empty_1. -unfold Empty; intros. -rewrite filter_iff; auto. -red; destruct 1. -rewrite <- (@for_all_iff s f) in H; auto. -rewrite (H a H0) in H1; discriminate. -apply for_all_1; auto; red; intros. -revert H; rewrite <- is_empty_iff. -unfold Empty; intro H; generalize (H x); clear H. -rewrite filter_iff; auto. -destruct (f x); auto. -Qed. - -Lemma exists_filter : - forall s, exists_ f s=negb (is_empty (filter f s)). -Proof. -intros; apply bool_1; split; intros. -destruct (exists_2 Comp H) as (a,(Ha1,Ha2)). -apply bool_6. -red; intros; apply (@is_empty_2 _ H0 a); auto with set. -generalize (@choose_1 (filter f s)) (@choose_2 (filter f s)). -destruct (choose (filter f s)). -intros H0 _; apply exists_1; auto. -exists e; generalize (H0 e); rewrite filter_iff; auto. -intros _ H0. -rewrite (is_empty_1 (H0 (refl_equal None))) in H; auto; discriminate. -Qed. - -Lemma partition_filter_1: - forall s, equal (fst (partition f s)) (filter f s)=true. -Proof. -auto with set. -Qed. - -Lemma partition_filter_2: - forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true. -Proof. -auto with set. -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. -unfold Add, MP.Add; intros. -repeat rewrite filter_iff; auto. -rewrite H0; clear H0. -assert (E.eq x y -> f y = true) by - (intro H0; rewrite <- (Comp _ _ H0); auto). -tauto. -Qed. - -Lemma add_filter_2 : forall s s' x, - f x=false -> (Add x s s') -> filter f s [=] filter f s'. -Proof. -unfold Add, MP.Add, Equal; intros. -repeat rewrite filter_iff; auto. -rewrite H0; clear H0. -assert (f a = true -> ~E.eq x a). - intros H0 H1. - rewrite (Comp _ _ H1) in H. - rewrite H in H0; discriminate. -tauto. -Qed. - -Lemma union_filter: forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) -> - forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s. -Proof. -clear Comp' Comp f. -intros. -assert (compat_bool E.eq (fun x => orb (f x) (g x))). - unfold compat_bool; intros. - rewrite (H x y H1); rewrite (H0 x y H1); auto. -unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto. -assert (f a || g a = true <-> f a = true \/ g a = true). - split; auto with bool. - intro H3; destruct (orb_prop _ _ H3); auto. -tauto. -Qed. - -Lemma filter_union: forall s s', filter f (union s s') [=] union (filter f s) (filter f s'). -Proof. -unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto; set_iff; tauto. -Qed. - -(** Properties of [for_all] *) - -Lemma for_all_mem_1: forall s, - (forall x, (mem x s)=true->(f x)=true) -> (for_all f s)=true. -Proof. -intros. -rewrite for_all_filter; auto. -rewrite is_empty_equal_empty. -apply equal_mem_1;intros. -rewrite filter_b; auto. -rewrite empty_mem. -generalize (H a); case (mem a s);intros;auto. -rewrite H0;auto. -Qed. - -Lemma for_all_mem_2: forall s, - (for_all f s)=true -> forall x,(mem x s)=true -> (f x)=true. -Proof. -intros. -rewrite for_all_filter in H; auto. -rewrite is_empty_equal_empty in H. -generalize (equal_mem_2 _ _ H x). -rewrite filter_b; auto. -rewrite empty_mem. -rewrite H0; simpl;intros. -replace true with (negb false);auto;apply negb_sym;auto. -Qed. - -Lemma for_all_mem_3: - forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false. -Proof. -intros. -apply (bool_eq_ind (for_all f s));intros;auto. -rewrite for_all_filter in H1; auto. -rewrite is_empty_equal_empty in H1. -generalize (equal_mem_2 _ _ H1 x). -rewrite filter_b; auto. -rewrite empty_mem. -rewrite H. -rewrite H0. -simpl;auto. -Qed. - -Lemma for_all_mem_4: - forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false}. -Proof. -intros. -rewrite for_all_filter in H; auto. -destruct (choose_mem_3 _ H) as (x,(H0,H1));intros. -exists x. -rewrite filter_b in H1; auto. -elim (andb_prop _ _ H1). -split;auto. -replace false with (negb true);auto;apply negb_sym;auto. -Qed. - -(** Properties of [exists] *) - -Lemma for_all_exists: - forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s). -Proof. -intros. -rewrite for_all_b; auto. -rewrite exists_b; auto. -induction (elements s); simpl; auto. -destruct (f a); simpl; auto. -Qed. - -End Bool. -Section Bool'. - -Variable f:elt->bool. -Variable Comp: compat_bool E.eq f. - -Let Comp' : compat_bool E.eq (fun x =>negb (f x)). -Proof. -unfold compat_bool in *; intros; f_equal; auto. -Qed. - -Lemma exists_mem_1: - forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false. -Proof. -intros. -rewrite for_all_exists; auto. -rewrite for_all_mem_1;auto with bool. -intros;generalize (H x H0);intros. -symmetry;apply negb_sym;simpl;auto. -Qed. - -Lemma exists_mem_2: - forall s, exists_ f s=false -> forall x, mem x s=true -> f x=false. -Proof. -intros. -rewrite for_all_exists in H; auto. -replace false with (negb true);auto;apply negb_sym;symmetry. -rewrite (for_all_mem_2 (fun x => negb (f x)) Comp' s);simpl;auto. -replace true with (negb false);auto;apply negb_sym;auto. -Qed. - -Lemma exists_mem_3: - forall s x, mem x s=true -> f x=true -> exists_ f s=true. -Proof. -intros. -rewrite for_all_exists; auto. -symmetry;apply negb_sym;simpl. -apply for_all_mem_3 with x;auto. -rewrite H0;auto. -Qed. - -Lemma exists_mem_4: - forall s, exists_ f s=true -> {x:elt | (mem x s)=true /\ (f x)=true}. -Proof. -intros. -rewrite for_all_exists in H; auto. -elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros. -elim p;intros. -exists x;split;auto. -replace true with (negb false);auto;apply negb_sym;auto. -replace false with (negb true);auto;apply negb_sym;auto. -Qed. - -End Bool'. - -Section Sum. - -(** Adding a valuation function on all elements of a set. *) - -Definition sum (f:elt -> nat)(s:t) := fold (fun x => plus (f x)) s 0. -Notation compat_opL := (compat_op E.eq (@Logic.eq _)). -Notation transposeL := (transpose (@Logic.eq _)). - -Lemma sum_plus : - forall f g, compat_nat E.eq f -> compat_nat E.eq g -> - forall s, sum (fun x =>f x+g x) s = sum f s + sum g s. -Proof. -unfold sum. -intros f g Hf Hg. -assert (fc : compat_opL (fun x:elt =>plus (f x))). auto. -assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega. -assert (gc : compat_opL (fun x:elt => plus (g x))). auto. -assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega. -assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). auto. -assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega. -assert (st := gen_st nat). -intros s;pattern s; apply set_rec. -intros. -rewrite <- (fold_equal _ _ st _ fc ft 0 _ _ H). -rewrite <- (fold_equal _ _ st _ gc gt 0 _ _ H). -rewrite <- (fold_equal _ _ st _ fgc fgt 0 _ _ H); auto. -intros; do 3 (rewrite (fold_add _ _ st);auto). -rewrite H0;simpl;omega. -do 3 rewrite fold_empty;auto. -Qed. - -Lemma sum_filter : forall f, (compat_bool E.eq f) -> - forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)). -Proof. -unfold sum; intros f Hf. -assert (st := gen_st nat). -assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))). - red; intros. - rewrite (Hf x x' H); auto. -assert (ct : transposeL (fun x => plus (if f x then 1 else 0))). - red; intros; omega. -intros s;pattern s; apply set_rec. -intros. -change elt with E.t. -rewrite <- (fold_equal _ _ st _ cc ct 0 _ _ H). -rewrite <- (MP.Equal_cardinal (filter_equal Hf (equal_2 H))); auto. -intros; rewrite (fold_add _ _ st _ cc ct); auto. -generalize (@add_filter_1 f Hf s0 (add x s0) x) (@add_filter_2 f Hf s0 (add x s0) x) . -assert (~ In x (filter f s0)). - intro H1; rewrite (mem_1 (filter_1 Hf H1)) in H; discriminate H. -case (f x); simpl; intros. -rewrite (MP.cardinal_2 H1 (H2 (refl_equal true) (MP.Add_add s0 x))); auto. -rewrite <- (MP.Equal_cardinal (H3 (refl_equal false) (MP.Add_add s0 x))); auto. -intros; rewrite fold_empty;auto. -rewrite MP.cardinal_1; auto. -unfold Empty; intros. -rewrite filter_iff; auto; set_iff; tauto. -Qed. - -Lemma fold_compat : - forall (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory _ eqA)) - (f g:elt->A->A), - (compat_op E.eq eqA f) -> (transpose eqA f) -> - (compat_op E.eq eqA g) -> (transpose eqA g) -> - forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) -> - (eqA (fold f s i) (fold g s i)). -Proof. -intros A eqA st f g fc ft gc gt i. -intro s; pattern s; apply set_rec; intros. -trans_st (fold f s0 i). -apply fold_equal with (eqA:=eqA); auto. -rewrite equal_sym; auto. -trans_st (fold g s0 i). -apply H0; intros; apply H1; auto with set. -elim (equal_2 H x); auto with set; intros. -apply fold_equal with (eqA:=eqA); auto with set. -trans_st (f x (fold f s0 i)). -apply fold_add with (eqA:=eqA); auto with set. -trans_st (g x (fold f s0 i)); auto with set. -trans_st (g x (fold g s0 i)); auto with set. -sym_st; apply fold_add with (eqA:=eqA); auto. -do 2 rewrite fold_empty; refl_st. -Qed. - -Lemma sum_compat : - forall f g, compat_nat E.eq f -> compat_nat E.eq g -> - forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s. -intros. -unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto. -red; intros; omega. -red; intros; omega. -Qed. - -End Sum. - -End EqProperties. diff --git a/theories/FSets/FSetWeakFacts.v b/theories/FSets/FSetWeakFacts.v deleted file mode 100644 index 0740d7f8e..000000000 --- a/theories/FSets/FSetWeakFacts.v +++ /dev/null @@ -1,494 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(* $Id$ *) - -(** * Finite sets library *) - -(** This functor derives additional facts from [FSetInterface.S]. These - facts are mainly the specifications of [FSetInterface.S] written using - different styles: equivalence and boolean equalities. - Moreover, we prove that [E.Eq] and [Equal] are setoid equalities. -*) - -Require Import DecidableTypeEx. -Require Export FSetWeakInterface. -Set Implicit Arguments. -Unset Strict Implicit. - -Module Facts - (M:FSetWeakInterface.S) - (D:DecidableType with Definition t:=M.E.t with Definition eq:=M.E.eq). -Import M.E. -Import M. - -Notation eq_dec := D.eq_dec. -Definition eqb x y := if eq_dec x y then true else false. - -(** * Specifications written using equivalences *) - -Section IffSpec. -Variable s s' s'' : t. -Variable x y z : elt. - -Lemma In_eq_iff : E.eq x y -> (In x s <-> In y s). -Proof. -split; apply In_1; auto. -Qed. - -Lemma mem_iff : In x s <-> mem x s = true. -Proof. -split; [apply mem_1|apply mem_2]. -Qed. - -Lemma not_mem_iff : ~In x s <-> mem x s = false. -Proof. -rewrite mem_iff; destruct (mem x s); intuition. -Qed. - -Lemma equal_iff : s[=]s' <-> equal s s' = true. -Proof. -split; [apply equal_1|apply equal_2]. -Qed. - -Lemma subset_iff : s[<=]s' <-> subset s s' = true. -Proof. -split; [apply subset_1|apply subset_2]. -Qed. - -Lemma empty_iff : In x empty <-> False. -Proof. -intuition; apply (empty_1 H). -Qed. - -Lemma is_empty_iff : Empty s <-> is_empty s = true. -Proof. -split; [apply is_empty_1|apply is_empty_2]. -Qed. - -Lemma singleton_iff : In y (singleton x) <-> E.eq x y. -Proof. -split; [apply singleton_1|apply singleton_2]. -Qed. - -Lemma add_iff : In y (add x s) <-> E.eq x y \/ In y s. -Proof. -split; [ | destruct 1; [apply add_1|apply add_2]]; auto. -destruct (eq_dec x y) as [E|E]; auto. -intro H; right; exact (add_3 E H). -Qed. - -Lemma add_neq_iff : ~ E.eq x y -> (In y (add x s) <-> In y s). -Proof. -split; [apply add_3|apply add_2]; auto. -Qed. - -Lemma remove_iff : In y (remove x s) <-> In y s /\ ~E.eq x y. -Proof. -split; [split; [apply remove_3 with x |] | destruct 1; apply remove_2]; auto. -intro. -apply (remove_1 H0 H). -Qed. - -Lemma remove_neq_iff : ~ E.eq x y -> (In y (remove x s) <-> In y s). -Proof. -split; [apply remove_3|apply remove_2]; auto. -Qed. - -Lemma union_iff : In x (union s s') <-> In x s \/ In x s'. -Proof. -split; [apply union_1 | destruct 1; [apply union_2|apply union_3]]; auto. -Qed. - -Lemma inter_iff : In x (inter s s') <-> In x s /\ In x s'. -Proof. -split; [split; [apply inter_1 with s' | apply inter_2 with s] | destruct 1; apply inter_3]; auto. -Qed. - -Lemma diff_iff : In x (diff s s') <-> In x s /\ ~ In x s'. -Proof. -split; [split; [apply diff_1 with s' | apply diff_2 with s] | destruct 1; apply diff_3]; auto. -Qed. - -Variable f : elt->bool. - -Lemma filter_iff : compat_bool E.eq f -> (In x (filter f s) <-> In x s /\ f x = true). -Proof. -split; [split; [apply filter_1 with f | apply filter_2 with s] | destruct 1; apply filter_3]; auto. -Qed. - -Lemma for_all_iff : compat_bool E.eq f -> - (For_all (fun x => f x = true) s <-> for_all f s = true). -Proof. -split; [apply for_all_1 | apply for_all_2]; auto. -Qed. - -Lemma exists_iff : compat_bool E.eq f -> - (Exists (fun x => f x = true) s <-> exists_ f s = true). -Proof. -split; [apply exists_1 | apply exists_2]; auto. -Qed. - -Lemma elements_iff : In x s <-> InA E.eq x (elements s). -Proof. -split; [apply elements_1 | apply elements_2]. -Qed. - -End IffSpec. - -(** Useful tactic for simplifying expressions like [In y (add x (union s s'))] *) - -Ltac set_iff := - repeat (progress ( - rewrite add_iff || rewrite remove_iff || rewrite singleton_iff - || rewrite union_iff || rewrite inter_iff || rewrite diff_iff - || rewrite empty_iff)). - -(** * Specifications written using boolean predicates *) - -Section BoolSpec. -Variable s s' s'' : t. -Variable x y z : elt. - -Lemma mem_b : E.eq x y -> mem x s = mem y s. -Proof. -intros. -generalize (mem_iff s x) (mem_iff s y)(In_eq_iff s H). -destruct (mem x s); destruct (mem y s); intuition. -Qed. - -Lemma empty_b : mem y empty = false. -Proof. -generalize (empty_iff y)(mem_iff empty y). -destruct (mem y empty); intuition. -Qed. - -Lemma add_b : mem y (add x s) = eqb x y || mem y s. -Proof. -generalize (mem_iff (add x s) y)(mem_iff s y)(add_iff s x y); unfold eqb. -destruct (eq_dec x y); destruct (mem y s); destruct (mem y (add x s)); intuition. -Qed. - -Lemma add_neq_b : ~ E.eq x y -> mem y (add x s) = mem y s. -Proof. -intros; generalize (mem_iff (add x s) y)(mem_iff s y)(add_neq_iff s H). -destruct (mem y s); destruct (mem y (add x s)); intuition. -Qed. - -Lemma remove_b : mem y (remove x s) = mem y s && negb (eqb x y). -Proof. -generalize (mem_iff (remove x s) y)(mem_iff s y)(remove_iff s x y); unfold eqb. -destruct (eq_dec x y); destruct (mem y s); destruct (mem y (remove x s)); simpl; intuition. -Qed. - -Lemma remove_neq_b : ~ E.eq x y -> mem y (remove x s) = mem y s. -Proof. -intros; generalize (mem_iff (remove x s) y)(mem_iff s y)(remove_neq_iff s H). -destruct (mem y s); destruct (mem y (remove x s)); intuition. -Qed. - -Lemma singleton_b : mem y (singleton x) = eqb x y. -Proof. -generalize (mem_iff (singleton x) y)(singleton_iff x y); unfold eqb. -destruct (eq_dec x y); destruct (mem y (singleton x)); intuition. -Qed. - -Lemma union_b : mem x (union s s') = mem x s || mem x s'. -Proof. -generalize (mem_iff (union s s') x)(mem_iff s x)(mem_iff s' x)(union_iff s s' x). -destruct (mem x s); destruct (mem x s'); destruct (mem x (union s s')); intuition. -Qed. - -Lemma inter_b : mem x (inter s s') = mem x s && mem x s'. -Proof. -generalize (mem_iff (inter s s') x)(mem_iff s x)(mem_iff s' x)(inter_iff s s' x). -destruct (mem x s); destruct (mem x s'); destruct (mem x (inter s s')); intuition. -Qed. - -Lemma diff_b : mem x (diff s s') = mem x s && negb (mem x s'). -Proof. -generalize (mem_iff (diff s s') x)(mem_iff s x)(mem_iff s' x)(diff_iff s s' x). -destruct (mem x s); destruct (mem x s'); destruct (mem x (diff s s')); simpl; intuition. -Qed. - -Lemma elements_b : mem x s = existsb (eqb x) (elements s). -Proof. -generalize (mem_iff s x)(elements_iff s x)(existsb_exists (eqb x) (elements s)). -rewrite InA_alt. -destruct (mem x s); destruct (existsb (eqb x) (elements s)); auto; intros. -symmetry. -rewrite H1. -destruct H0 as (H0,_). -destruct H0 as (a,(Ha1,Ha2)); [ intuition |]. -exists a; intuition. -unfold eqb; destruct (eq_dec x a); auto. -rewrite <- H. -rewrite H0. -destruct H1 as (H1,_). -destruct H1 as (a,(Ha1,Ha2)); [intuition|]. -exists a; intuition. -unfold eqb in *; destruct (eq_dec x a); auto; discriminate. -Qed. - -Variable f : elt->bool. - -Lemma filter_b : compat_bool E.eq f -> mem x (filter f s) = mem x s && f x. -Proof. -intros. -generalize (mem_iff (filter f s) x)(mem_iff s x)(filter_iff s x H). -destruct (mem x s); destruct (mem x (filter f s)); destruct (f x); simpl; intuition. -Qed. - -Lemma for_all_b : compat_bool E.eq f -> - for_all f s = forallb f (elements s). -Proof. -intros. -generalize (forallb_forall f (elements s))(for_all_iff s H)(elements_iff s). -unfold For_all. -destruct (forallb f (elements s)); destruct (for_all f s); auto; intros. -rewrite <- H1; intros. -destruct H0 as (H0,_). -rewrite (H2 x0) in H3. -rewrite (InA_alt E.eq x0 (elements s)) in H3. -destruct H3 as (a,(Ha1,Ha2)). -rewrite (H _ _ Ha1). -apply H0; auto. -symmetry. -rewrite H0; intros. -destruct H1 as (_,H1). -apply H1; auto. -rewrite H2. -rewrite InA_alt; eauto. -Qed. - -Lemma exists_b : compat_bool E.eq f -> - exists_ f s = existsb f (elements s). -Proof. -intros. -generalize (existsb_exists f (elements s))(exists_iff s H)(elements_iff s). -unfold Exists. -destruct (existsb f (elements s)); destruct (exists_ f s); auto; intros. -rewrite <- H1; intros. -destruct H0 as (H0,_). -destruct H0 as (a,(Ha1,Ha2)); auto. -exists a; split; auto. -rewrite H2; rewrite InA_alt; eauto. -symmetry. -rewrite H0. -destruct H1 as (_,H1). -destruct H1 as (a,(Ha1,Ha2)); auto. -rewrite (H2 a) in Ha1. -rewrite (InA_alt E.eq a (elements s)) in Ha1. -destruct Ha1 as (b,(Hb1,Hb2)). -exists b; auto. -rewrite <- (H _ _ Hb1); auto. -Qed. - -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. - -Definition Equal_ST : Setoid_Theory t Equal. -Proof. -constructor; [apply eq_refl | apply eq_sym | apply eq_trans]. -Qed. - -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. -unfold Equal; intros x y H s s' H0. -rewrite (In_eq_iff s H); auto. -Qed. - -Add Morphism is_empty : is_empty_m. -Proof. -unfold Equal; intros s s' H. -generalize (is_empty_iff s)(is_empty_iff s'). -destruct (is_empty s); destruct (is_empty s'); - unfold Empty; auto; intros. -symmetry. -rewrite <- H1; intros a Ha. -rewrite <- (H a) in Ha. -destruct H0 as (_,H0). -exact (H0 (refl_equal true) _ Ha). -rewrite <- H0; intros a Ha. -rewrite (H a) in Ha. -destruct H1 as (_,H1). -exact (H1 (refl_equal true) _ Ha). -Qed. - -Add Morphism Empty with signature Equal ==> iff as Empty_m. -Proof. -intros; do 2 rewrite is_empty_iff; rewrite H; intuition. -Qed. - -Add Morphism mem : mem_m. -Proof. -unfold Equal; intros x y H s s' H0. -generalize (H0 x); clear H0; rewrite (In_eq_iff s' H). -generalize (mem_iff s x)(mem_iff s' y). -destruct (mem x s); destruct (mem y s'); intuition. -Qed. - -Add Morphism singleton : singleton_m. -Proof. -unfold Equal; intros x y H a. -do 2 rewrite singleton_iff; split; intros. -apply E.eq_trans with x; auto. -apply E.eq_trans with y; auto. -Qed. - -Add Morphism add : add_m. -Proof. -unfold Equal; intros x y H s s' H0 a. -do 2 rewrite add_iff; rewrite H; rewrite H0; intuition. -Qed. - -Add Morphism remove : remove_m. -Proof. -unfold Equal; intros x y H s s' H0 a. -do 2 rewrite remove_iff; rewrite H; rewrite H0; intuition. -Qed. - -Add Morphism union : union_m. -Proof. -unfold Equal; intros s s' H s'' s''' H0 a. -do 2 rewrite union_iff; rewrite H; rewrite H0; intuition. -Qed. - -Add Morphism inter : inter_m. -Proof. -unfold Equal; intros s s' H s'' s''' H0 a. -do 2 rewrite inter_iff; rewrite H; rewrite H0; intuition. -Qed. - -Add Morphism diff : diff_m. -Proof. -unfold Equal; intros s s' H s'' s''' H0 a. -do 2 rewrite diff_iff; rewrite H; rewrite H0; intuition. -Qed. - -Add Morphism Subset with signature Equal ==> Equal ==> iff as Subset_m. -Proof. -unfold Equal, Subset; firstorder. -Qed. - -Add Morphism subset : subset_m. -Proof. -intros s s' H s'' s''' H0. -generalize (subset_iff s s'') (subset_iff s' s'''). -destruct (subset s s''); destruct (subset s' s'''); auto; intros. -rewrite H in H1; rewrite H0 in H1; intuition. -rewrite H in H1; rewrite H0 in H1; intuition. -Qed. - -Add Morphism equal : equal_m. -Proof. -intros s s' H s'' s''' H0. -generalize (equal_iff s s'') (equal_iff s' s'''). -destruct (equal s s''); destruct (equal s' s'''); auto; intros. -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. Defined. - -Lemma Subset_trans : forall s s' s'', s[<=]s'->s'[<=]s''->s[<=]s''. -Proof. unfold Subset; eauto. Defined. - -Add Relation t Subset - reflexivity proved by Subset_refl - transitivity proved by Subset_trans - as SubsetSetoid. -(* NB: for the moment, it is important to use Defined and not Qed in - the two previous lemmas, in order to allow conversion of - SubsetSetoid coming from separate Facts modules. See bug #1738. *) - -Add Morphism In with signature E.eq ==> Subset ++> impl as In_s_m. -Proof. -unfold Subset, impl; intros; eauto with set. -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. - -(* [fold], [filter], [for_all], [exists_] and [partition] cannot be proved morphism - without additional hypothesis on [f]. For instance: *) - -Lemma filter_equal : forall f, compat_bool E.eq f -> - forall s s', s[=]s' -> filter f s [=] filter f s'. -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]. *) - -(* Later: -Add Morphism cardinal ; cardinal_m. -*) - -End Facts. diff --git a/theories/FSets/FSetWeakInterface.v b/theories/FSets/FSetWeakInterface.v deleted file mode 100644 index 5fa6c757f..000000000 --- a/theories/FSets/FSetWeakInterface.v +++ /dev/null @@ -1,264 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(* $Id$ *) - -(** * Finite sets library *) - -(** Set interfaces for types with only a decidable equality, but no ordering *) - -Require Export Bool DecidableType. -Set Implicit Arguments. -Unset Strict Implicit. - -(** * Non-dependent signature - - Signature [S] presents sets as purely informative programs - together with axioms *) - -Module Type S. - - (** The module E of base objects is meant to be a DecidableType - (and used to be so). But requiring only an EqualityType here - allows subtyping between FSet and FSetWeak *) - Declare Module E : EqualityType. - Definition elt := E.t. - - Parameter t : Set. (** the abstract type of sets *) - - (** Logical predicates *) - Parameter In : elt -> t -> Prop. - 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 := 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). - - Parameter empty : t. - (** The empty set. *) - - Parameter is_empty : t -> bool. - (** Test whether a set is empty or not. *) - - Parameter mem : elt -> t -> bool. - (** [mem x s] tests whether [x] belongs to the set [s]. *) - - Parameter add : elt -> t -> t. - (** [add x s] returns a set containing all elements of [s], - plus [x]. If [x] was already in [s], [s] is returned unchanged. *) - - Parameter singleton : elt -> t. - (** [singleton x] returns the one-element set containing only [x]. *) - - Parameter remove : elt -> t -> t. - (** [remove x s] returns a set containing all elements of [s], - except [x]. If [x] was not in [s], [s] is returned unchanged. *) - - Parameter union : t -> t -> t. - (** Set union. *) - - Parameter inter : t -> t -> t. - (** Set intersection. *) - - Parameter diff : t -> t -> t. - (** Set difference. *) - - Definition eq : t -> t -> Prop := Equal. - (** EqualityType is a subset of this interface, but not - DecidableType, in order to have FSetWeak < FSet. - Hence no weak sets of weak sets in general, but it works - at least with FSetWeakList.make that provides an eq_dec. *) - - Parameter equal : t -> t -> bool. - (** [equal s1 s2] tests whether the sets [s1] and [s2] are - equal, that is, contain equal elements. *) - - Parameter subset : t -> t -> bool. - (** [subset s1 s2] tests whether the set [s1] is a subset of - the set [s2]. *) - - (** Coq comment: [iter] is useless in a purely functional world *) - (** iter: (elt -> unit) -> set -> unit. i*) - (** [iter f s] applies [f] in turn to all elements of [s]. - The order in which the elements of [s] are presented to [f] - is unspecified. *) - - Parameter fold : forall A : Type, (elt -> A -> A) -> t -> A -> A. - (** [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)], - where [x1 ... xN] are the elements of [s]. - The order in which elements of [s] are presented to [f] is - unspecified. *) - - Parameter for_all : (elt -> bool) -> t -> bool. - (** [for_all p s] checks if all elements of the set - satisfy the predicate [p]. *) - - Parameter exists_ : (elt -> bool) -> t -> bool. - (** [exists p s] checks if at least one element of - the set satisfies the predicate [p]. *) - - Parameter filter : (elt -> bool) -> t -> t. - (** [filter p s] returns the set of all elements in [s] - that satisfy predicate [p]. *) - - Parameter partition : (elt -> bool) -> t -> t * t. - (** [partition p s] returns a pair of sets [(s1, s2)], where - [s1] is the set of all the elements of [s] that satisfy the - predicate [p], and [s2] is the set of all the elements of - [s] that do not satisfy [p]. *) - - Parameter cardinal : t -> nat. - (** Return the number of elements of a set. *) - (** Coq comment: nat instead of int ... *) - - Parameter elements : t -> list elt. - (** Return the list of all elements of the given set, in any order. *) - - Parameter choose : t -> option elt. - (** Return one element of the given set, or raise [Not_found] if - the set is empty. Which element is chosen is unspecified. - Equal sets could return different elements. *) - (** Coq comment: [Not_found] is represented by the option type *) - - Section Spec. - - Variable s s' s'': t. - Variable x y : elt. - - (** Specification of [In] *) - Parameter In_1 : E.eq x y -> In x s -> In y s. - - (** Specification of [eq] *) - 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 equal_1 : Equal s s' -> equal s s' = true. - Parameter equal_2 : equal s s' = true -> Equal s s'. - - (** Specification of [subset] *) - Parameter subset_1 : Subset s s' -> subset s s' = true. - Parameter subset_2 : subset s s' = true -> Subset s s'. - - (** Specification of [empty] *) - Parameter empty_1 : Empty empty. - - (** Specification of [is_empty] *) - 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. - - (** Specification of [remove] *) - Parameter remove_1 : E.eq x y -> ~ In y (remove x s). - Parameter remove_2 : ~ E.eq x y -> In y s -> In y (remove x s). - 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). - - (** 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_3 : In x s' -> In x (union s s'). - - (** Specification of [inter] *) - Parameter inter_1 : In x (inter s s') -> In x s. - Parameter inter_2 : In x (inter s s') -> In x s'. - 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_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] *) - 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] *) - 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_3 : - compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s). - - (** Specification of [for_all] *) - Parameter for_all_1 : - compat_bool E.eq f -> - For_all (fun x => f x = true) s -> for_all f s = true. - Parameter for_all_2 : - compat_bool E.eq f -> - for_all f s = true -> For_all (fun x => f x = true) s. - - (** Specification of [exists] *) - Parameter exists_1 : - compat_bool E.eq f -> - Exists (fun x => f x = true) s -> exists_ f s = true. - Parameter exists_2 : - compat_bool E.eq f -> - exists_ f s = true -> Exists (fun x => f x = true) s. - - (** Specification of [partition] *) - Parameter partition_1 : - compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s). - Parameter partition_2 : - compat_bool E.eq f -> - Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). - - End Filter. - - (** 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 FSet, here comes the only - property that is really weaker: *) - Parameter elements_3w : NoDupA E.eq (elements s). - - (** Specification of [choose] *) - Parameter choose_1 : choose s = Some x -> In x s. - Parameter choose_2 : choose s = None -> Empty s. - - End Spec. - - Hint Resolve mem_1 equal_1 subset_1 empty_1 - 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 - : 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 - : set. - (* for compatibility with earlier hints *) - Hint Resolve 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 - : oldset. - - -End S. diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v index b207f1f1e..c692950e0 100644 --- a/theories/FSets/FSetWeakList.v +++ b/theories/FSets/FSetWeakList.v @@ -13,7 +13,7 @@ (** This file proposes an implementation of the non-dependant interface [FSetWeakInterface.S] using lists without redundancy. *) -Require Import FSetWeakInterface. +Require Import FSetInterface. Set Implicit Arguments. Unset Strict Implicit. @@ -804,7 +804,7 @@ End Raw. Now, in order to really provide a functor implementing [S], we need to encapsulate everything into a type of lists without redundancy. *) -Module Make (X: DecidableType) <: S with Module E := X. +Module Make (X: DecidableType) <: WS with Module E := X. Module Raw := Raw X. Module E := X. diff --git a/theories/FSets/FSetWeakProperties.v b/theories/FSets/FSetWeakProperties.v deleted file mode 100644 index 3a8bdb032..000000000 --- a/theories/FSets/FSetWeakProperties.v +++ /dev/null @@ -1,771 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(* $Id$ *) - -(** * Finite sets library *) - -(** This functor derives additional properties from [FSetWeakInterface.S]. - Contrary to the functor in [FSetWeakEqProperties] it uses - predicates over sets instead of sets operations, i.e. - [In x s] instead of [mem x s=true], - [Equal s s'] instead of [equal s s'=true], etc. *) - -Require Export FSetWeakInterface. -Require Import FSetWeakFacts FSetDecide. -Set Implicit Arguments. -Unset Strict Implicit. - -Hint Unfold transpose compat_op. -Hint Extern 1 (Setoid_Theory _ _) => constructor; congruence. - -Module Properties - (M:FSetWeakInterface.S) - (D:DecidableType with Definition t:=M.E.t - with Definition eq:=M.E.eq). - Module Import FM := Facts M D. - Module Import Dec := FSetDecide.WeakDecide M D. - Import M.E. - Import M. - - Lemma In_dec : forall x s, {In x s} + {~ In x s}. - Proof. - intros; generalize (mem_iff s x); case (mem x s); intuition. - Qed. - - Definition Add x s s' := forall y, In y s' <-> E.eq x y \/ In y s. - - Lemma Add_Equal : forall x s s', Add x s s' <-> s' [=] add x s. - Proof. - unfold Add. - split; intros. - red; intros. - rewrite H; clear H. - fsetdec. - fsetdec. - Qed. - - Ltac expAdd := repeat rewrite Add_Equal. - - Section BasicProperties. - - Variable s s' s'' s1 s2 s3 : t. - Variable x x' : elt. - - Lemma equal_refl : s[=]s. - Proof. fsetdec. Qed. - - Lemma equal_sym : s[=]s' -> s'[=]s. - Proof. fsetdec. Qed. - - Lemma equal_trans : s1[=]s2 -> s2[=]s3 -> s1[=]s3. - Proof. fsetdec. Qed. - - Lemma subset_refl : s[<=]s. - Proof. fsetdec. Qed. - - Lemma subset_trans : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3. - Proof. fsetdec. Qed. - - Lemma subset_antisym : s[<=]s' -> s'[<=]s -> s[=]s'. - Proof. fsetdec. Qed. - - Lemma subset_equal : s[=]s' -> s[<=]s'. - Proof. fsetdec. Qed. - - Lemma subset_empty : empty[<=]s. - Proof. fsetdec. Qed. - - Lemma subset_remove_3 : s1[<=]s2 -> remove x s1 [<=] s2. - Proof. fsetdec. Qed. - - Lemma subset_diff : s1[<=]s3 -> diff s1 s2 [<=] s3. - Proof. fsetdec. Qed. - - Lemma subset_add_3 : In x s2 -> s1[<=]s2 -> add x s1 [<=] s2. - Proof. fsetdec. Qed. - - Lemma subset_add_2 : s1[<=]s2 -> s1[<=] add x s2. - Proof. fsetdec. Qed. - - Lemma in_subset : In x s1 -> s1[<=]s2 -> In x s2. - Proof. fsetdec. Qed. - - Lemma double_inclusion : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1. - Proof. intuition fsetdec. Qed. - - Lemma empty_is_empty_1 : Empty s -> s[=]empty. - Proof. fsetdec. Qed. - - Lemma empty_is_empty_2 : s[=]empty -> Empty s. - Proof. fsetdec. Qed. - - Lemma add_equal : In x s -> add x s [=] s. - Proof. fsetdec. Qed. - - Lemma add_add : add x (add x' s) [=] add x' (add x s). - Proof. fsetdec. Qed. - - Lemma remove_equal : ~ In x s -> remove x s [=] s. - Proof. fsetdec. Qed. - - Lemma Equal_remove : s[=]s' -> remove x s [=] remove x s'. - Proof. fsetdec. Qed. - - Lemma add_remove : In x s -> add x (remove x s) [=] s. - Proof. fsetdec. Qed. - - Lemma remove_add : ~In x s -> remove x (add x s) [=] s. - Proof. fsetdec. Qed. - - Lemma singleton_equal_add : singleton x [=] add x empty. - Proof. fsetdec. Qed. - - Lemma union_sym : union s s' [=] union s' s. - Proof. fsetdec. Qed. - - Lemma union_subset_equal : s[<=]s' -> union s s' [=] s'. - Proof. fsetdec. Qed. - - Lemma union_equal_1 : s[=]s' -> union s s'' [=] union s' s''. - Proof. fsetdec. Qed. - - Lemma union_equal_2 : s'[=]s'' -> union s s' [=] union s s''. - Proof. fsetdec. Qed. - - Lemma union_assoc : union (union s s') s'' [=] union s (union s' s''). - Proof. fsetdec. Qed. - - Lemma add_union_singleton : add x s [=] union (singleton x) s. - Proof. fsetdec. Qed. - - Lemma union_add : union (add x s) s' [=] add x (union s s'). - Proof. fsetdec. Qed. - - Lemma union_remove_add_1 : - union (remove x s) (add x s') [=] union (add x s) (remove x s'). - Proof. fsetdec. Qed. - - Lemma union_remove_add_2 : In x s -> - union (remove x s) (add x s') [=] union s s'. - Proof. fsetdec. Qed. - - Lemma union_subset_1 : s [<=] union s s'. - Proof. fsetdec. Qed. - - Lemma union_subset_2 : s' [<=] union s s'. - Proof. fsetdec. Qed. - - Lemma union_subset_3 : s[<=]s'' -> s'[<=]s'' -> union s s' [<=] s''. - Proof. fsetdec. Qed. - - Lemma union_subset_4 : s[<=]s' -> union s s'' [<=] union s' s''. - Proof. fsetdec. Qed. - - Lemma union_subset_5 : s[<=]s' -> union s'' s [<=] union s'' s'. - Proof. fsetdec. Qed. - - Lemma empty_union_1 : Empty s -> union s s' [=] s'. - Proof. fsetdec. Qed. - - Lemma empty_union_2 : Empty s -> union s' s [=] s'. - Proof. fsetdec. Qed. - - Lemma not_in_union : ~In x s -> ~In x s' -> ~In x (union s s'). - Proof. fsetdec. Qed. - - Lemma inter_sym : inter s s' [=] inter s' s. - Proof. fsetdec. Qed. - - Lemma inter_subset_equal : s[<=]s' -> inter s s' [=] s. - Proof. fsetdec. Qed. - - Lemma inter_equal_1 : s[=]s' -> inter s s'' [=] inter s' s''. - Proof. fsetdec. Qed. - - Lemma inter_equal_2 : s'[=]s'' -> inter s s' [=] inter s s''. - Proof. fsetdec. Qed. - - Lemma inter_assoc : inter (inter s s') s'' [=] inter s (inter s' s''). - Proof. fsetdec. Qed. - - Lemma union_inter_1 : inter (union s s') s'' [=] union (inter s s'') (inter s' s''). - Proof. fsetdec. Qed. - - Lemma union_inter_2 : union (inter s s') s'' [=] inter (union s s'') (union s' s''). - Proof. fsetdec. Qed. - - Lemma inter_add_1 : In x s' -> inter (add x s) s' [=] add x (inter s s'). - Proof. fsetdec. Qed. - - Lemma inter_add_2 : ~ In x s' -> inter (add x s) s' [=] inter s s'. - Proof. fsetdec. Qed. - - Lemma empty_inter_1 : Empty s -> Empty (inter s s'). - Proof. fsetdec. Qed. - - Lemma empty_inter_2 : Empty s' -> Empty (inter s s'). - Proof. fsetdec. Qed. - - Lemma inter_subset_1 : inter s s' [<=] s. - Proof. fsetdec. Qed. - - Lemma inter_subset_2 : inter s s' [<=] s'. - Proof. fsetdec. Qed. - - Lemma inter_subset_3 : - s''[<=]s -> s''[<=]s' -> s''[<=] inter s s'. - Proof. fsetdec. Qed. - - Lemma empty_diff_1 : Empty s -> Empty (diff s s'). - Proof. fsetdec. Qed. - - Lemma empty_diff_2 : Empty s -> diff s' s [=] s'. - Proof. fsetdec. Qed. - - Lemma diff_subset : diff s s' [<=] s. - Proof. fsetdec. Qed. - - Lemma diff_subset_equal : s[<=]s' -> diff s s' [=] empty. - Proof. fsetdec. Qed. - - Lemma remove_diff_singleton : - remove x s [=] diff s (singleton x). - Proof. fsetdec. Qed. - - Lemma diff_inter_empty : inter (diff s s') (inter s s') [=] empty. - Proof. fsetdec. Qed. - - Lemma diff_inter_all : union (diff s s') (inter s s') [=] s. - Proof. fsetdec. Qed. - - Lemma Add_add : Add x s (add x s). - Proof. expAdd; fsetdec. Qed. - - Lemma Add_remove : In x s -> Add x (remove x s) s. - Proof. expAdd; fsetdec. Qed. - - Lemma union_Add : Add x s s' -> Add x (union s s'') (union s' s''). - Proof. expAdd; fsetdec. Qed. - - Lemma inter_Add : - In x s'' -> Add x s s' -> Add x (inter s s'') (inter s' s''). - Proof. expAdd; fsetdec. Qed. - - Lemma union_Equal : - In x s'' -> Add x s s' -> union s s'' [=] union s' s''. - Proof. expAdd; fsetdec. Qed. - - Lemma inter_Add_2 : - ~In x s'' -> Add x s s' -> inter s s'' [=] inter s' s''. - Proof. expAdd; fsetdec. Qed. - - End BasicProperties. - - Hint Immediate equal_sym add_remove remove_add union_sym inter_sym: set. - Hint Resolve equal_refl equal_trans subset_refl subset_equal subset_antisym - subset_trans subset_empty subset_remove_3 subset_diff subset_add_3 - subset_add_2 in_subset empty_is_empty_1 empty_is_empty_2 add_equal - remove_equal singleton_equal_add union_subset_equal union_equal_1 - union_equal_2 union_assoc add_union_singleton union_add union_subset_1 - union_subset_2 union_subset_3 inter_subset_equal inter_equal_1 inter_equal_2 - inter_assoc union_inter_1 union_inter_2 inter_add_1 inter_add_2 - empty_inter_1 empty_inter_2 empty_union_1 empty_union_2 empty_diff_1 - 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 add_add : set. - - (** * Properties of elements *) - - Lemma elements_Empty : forall s, Empty s <-> elements s = nil. - Proof. - intros. - unfold Empty. - split; intros. - assert (forall a, ~ List.In a (elements s)). - red; intros. - apply (H a). - rewrite elements_iff. - rewrite InA_alt; exists a; auto. - destruct (elements s); auto. - elim (H0 e); simpl; auto. - red; intros. - rewrite elements_iff in H0. - rewrite InA_alt in H0; destruct H0. - rewrite H in H0; destruct H0 as (_,H0); inversion H0. - Qed. - - (** * 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: - *) - - Lemma fold_0 : - forall s (A : Set) (i : A) (f : elt -> A -> A), - exists l : list elt, - NoDup l /\ - (forall x : elt, In x s <-> InA E.eq x l) /\ - fold f s i = fold_right f i l. - Proof. - intros; exists (rev (elements s)); split. - apply NoDupA_rev; auto with set. - exact E.eq_trans. - split; intros. - rewrite elements_iff; do 2 rewrite InA_alt. - split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition. - rewrite fold_left_rev_right. - apply fold_1. - Qed. - - (** An alternate (and previous) specification for [fold] was based on - the recursive structure of a set. It is now lemmas [fold_1] and - [fold_2]. *) - - Lemma fold_1 : - forall s (A : Set) (eqA : A -> A -> Prop) - (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A), - Empty s -> eqA (fold f s i) i. - Proof. - unfold Empty; intros; destruct (fold_0 s i f) as (l,(H1, (H2, H3))). - rewrite H3; clear H3. - generalize H H2; clear H H2; case l; simpl; intros. - refl_st. - elim (H e). - elim (H2 e); intuition. - Qed. - - Lemma fold_2 : - forall s s' x (A : Set) (eqA : A -> A -> Prop) - (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A), - compat_op E.eq eqA f -> - transpose eqA f -> - ~ In x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)). - Proof. - 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:=E.eq)(eqB:=eqA); auto. - eauto. - rewrite <- Hl1; auto. - intros a; rewrite InA_cons; rewrite <- Hl1; rewrite <- Hl'1; - rewrite (H2 a); intuition. - Qed. - - (** In fact, [fold] on empty sets is more than equivalent to - the initial element, it is Leibniz-equal to it. *) - - Lemma fold_1b : - forall s (A : Set)(i : A) (f : elt -> A -> A), - Empty s -> (fold f s i) = i. - Proof. - intros. - rewrite M.fold_1. - rewrite elements_Empty in H; rewrite H; simpl; auto. - Qed. - - (** Similar specifications for [cardinal]. *) - - Lemma cardinal_fold : forall s, cardinal s = fold (fun _ => S) s 0. - Proof. - intros; rewrite cardinal_1; rewrite M.fold_1. - symmetry; apply fold_left_length; auto. - Qed. - - Lemma cardinal_0 : - forall s, exists l : list elt, - NoDupA E.eq l /\ - (forall x : elt, In x s <-> InA E.eq x l) /\ - cardinal s = length l. - Proof. - intros; exists (elements s); intuition; apply cardinal_1. - Qed. - - Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0. - Proof. - intros; rewrite cardinal_fold; apply fold_1; auto. - Qed. - - Lemma cardinal_2 : - forall s s' x, ~ In x s -> Add x s s' -> cardinal s' = S (cardinal s). - Proof. - intros; do 2 rewrite cardinal_fold. - change S with ((fun _ => S) x). - apply fold_2; auto. - Qed. - - End Old_Spec_Now_Properties. - - (** * Induction principle over sets *) - - Lemma cardinal_Empty : forall s, Empty s <-> cardinal s = 0. - Proof. - intros. - rewrite elements_Empty, M.cardinal_1. - destruct (elements s); intuition; discriminate. - Qed. - - Lemma cardinal_inv_1 : forall s, cardinal s = 0 -> Empty s. - Proof. - intros; rewrite cardinal_Empty; auto. - Qed. - Hint Resolve cardinal_inv_1. - - Lemma cardinal_inv_2 : - forall s n, cardinal s = S n -> { x : elt | In x s }. - Proof. - intros; rewrite M.cardinal_1 in H. - generalize (elements_2 (s:=s)). - destruct (elements s); try discriminate. - exists e; auto. - Qed. - - Lemma cardinal_inv_2b : - forall s, cardinal s <> 0 -> { x : elt | In x s }. - Proof. - intro; generalize (@cardinal_inv_2 s); destruct cardinal; - [intuition|eauto]. - Qed. - - Lemma Equal_cardinal : forall s s', s[=]s' -> cardinal s = cardinal s'. - Proof. - symmetry. - remember (cardinal s) as n; symmetry in Heqn; revert s s' Heqn H. - induction n; intros. - apply cardinal_1; rewrite <- H; auto. - destruct (cardinal_inv_2 Heqn) as (x,H2). - revert Heqn. - rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); auto with set. - rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); eauto with set. - Qed. - - Add Morphism cardinal : cardinal_m. - Proof. - exact Equal_cardinal. - Qed. - - Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal. - - Lemma set_induction : - forall P : t -> Type, - (forall s : t, Empty s -> P s) -> - (forall s s' : t, P s -> forall x : elt, ~In 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; auto. - destruct (cardinal_inv_2 (sym_eq Heqn)) as (x,H0). - apply X0 with (remove x s) x; auto with set. - apply IHn; auto. - assert (S n = S (cardinal (remove x s))). - rewrite Heqn; apply cardinal_2 with x; auto with set. - inversion H; auto. - Qed. - - (** Other properties of [fold]. *) - - Section Fold. - 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). - - Section Fold_1. - Variable i i':A. - - Lemma fold_empty : (fold f empty i) = i. - Proof. - apply fold_1b; auto with set. - Qed. - - Lemma fold_equal : - forall s s', s[=]s' -> eqA (fold f s i) (fold f s' i). - Proof. - intros s; pattern s; apply set_induction; clear s; intros. - trans_st i. - apply fold_1; auto. - sym_st; apply fold_1; auto. - rewrite <- H0; auto. - trans_st (f x (fold f s i)). - apply fold_2 with (eqA := eqA); auto. - sym_st; apply fold_2 with (eqA := eqA); auto. - unfold Add in *; intros. - rewrite <- H2; auto. - Qed. - - Lemma fold_add : forall s x, ~In x s -> - eqA (fold f (add x s) i) (f x (fold f s i)). - Proof. - intros; apply fold_2 with (eqA := eqA); auto. - Qed. - - Lemma add_fold : forall s x, In x s -> - eqA (fold f (add x s) i) (fold f s i). - Proof. - intros; apply fold_equal; auto with set. - Qed. - - Lemma remove_fold_1: forall s x, In x s -> - eqA (f x (fold f (remove x s) i)) (fold f s i). - Proof. - intros. - sym_st. - apply fold_2 with (eqA:=eqA); auto with set. - Qed. - - Lemma remove_fold_2: forall s x, ~In x s -> - eqA (fold f (remove x s) i) (fold f s i). - Proof. - intros. - apply fold_equal; auto with set. - Qed. - - Lemma fold_commutes : forall s x, - eqA (fold f s (f x i)) (f x (fold f s i)). - Proof. - intros; pattern s; apply set_induction; clear s; intros. - trans_st (f x i). - apply fold_1; auto. - sym_st. - apply Comp; auto. - apply fold_1; auto. - trans_st (f x0 (fold f s (f x i))). - apply fold_2 with (eqA:=eqA); auto. - trans_st (f x0 (f x (fold f s i))). - trans_st (f x (f x0 (fold f s i))). - apply Comp; auto. - sym_st. - apply fold_2 with (eqA:=eqA); auto. - Qed. - - Lemma fold_init : forall s, eqA i i' -> - eqA (fold f s i) (fold f s i'). - Proof. - intros; pattern s; apply set_induction; clear s; intros. - trans_st i. - apply fold_1; auto. - trans_st i'. - sym_st; apply fold_1; auto. - trans_st (f x (fold f s i)). - apply fold_2 with (eqA:=eqA); auto. - trans_st (f x (fold f s i')). - sym_st; apply fold_2 with (eqA:=eqA); auto. - Qed. - - End Fold_1. - Section Fold_2. - Variable i:A. - - Lemma fold_union_inter : forall s s', - eqA (fold f (union s s') (fold f (inter s s') i)) - (fold f s (fold f s' i)). - Proof. - intros; pattern s; apply set_induction; clear s; intros. - trans_st (fold f s' (fold f (inter s s') i)). - apply fold_equal; auto with set. - trans_st (fold f s' i). - apply fold_init; auto. - apply fold_1; auto with set. - sym_st; apply fold_1; auto. - rename s'0 into s''. - destruct (In_dec x s'). - (* In x s' *) - trans_st (fold f (union s'' s') (f x (fold f (inter s s') i))); auto with set. - apply fold_init; auto. - apply fold_2 with (eqA:=eqA); auto with set. - rewrite inter_iff; intuition. - trans_st (f x (fold f s (fold f s' i))). - trans_st (fold f (union s s') (f x (fold f (inter s s') i))). - apply fold_equal; auto. - apply equal_sym; apply union_Equal with x; auto with set. - trans_st (f x (fold f (union s s') (fold f (inter s s') i))). - apply fold_commutes; auto. - sym_st; apply fold_2 with (eqA:=eqA); auto. - (* ~(In x s') *) - trans_st (f x (fold f (union s s') (fold f (inter s'' s') i))). - apply fold_2 with (eqA:=eqA); auto with set. - trans_st (f x (fold f (union s s') (fold f (inter s s') i))). - apply Comp;auto. - apply fold_init;auto. - apply fold_equal;auto. - apply equal_sym; apply inter_Add_2 with x; auto with set. - trans_st (f x (fold f s (fold f s' i))). - sym_st; apply fold_2 with (eqA:=eqA); auto. - Qed. - - End Fold_2. - Section Fold_3. - Variable i:A. - - Lemma fold_diff_inter : forall s s', - eqA (fold f (diff s s') (fold f (inter s s') i)) (fold f s i). - Proof. - intros. - trans_st (fold f (union (diff s s') (inter s s')) - (fold f (inter (diff s s') (inter s s')) i)). - sym_st; apply fold_union_inter; auto. - trans_st (fold f s (fold f (inter (diff s s') (inter s s')) i)). - apply fold_equal; auto with set. - apply fold_init; auto. - apply fold_1; auto with set. - Qed. - - Lemma fold_union: forall s s', - (forall x, ~(In x s/\In x s')) -> - eqA (fold f (union s s') i) (fold f s (fold f s' i)). - Proof. - intros. - trans_st (fold f (union s s') (fold f (inter s s') i)). - apply fold_init; auto. - sym_st; apply fold_1; auto with set. - unfold Empty; intro a; generalize (H a); set_iff; tauto. - apply fold_union_inter; auto. - Qed. - - End Fold_3. - End Fold. - - Lemma fold_plus : - 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 (@Logic.eq _) (fun _ => S)) by (unfold compat_op; auto). - assert (fp : transpose (@Logic.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. - assert (forall p s', Add x s s' -> fold (fun _ => S) s' p = S (fold (fun _ => S) s p)). - change S with ((fun _ => S) x). - intros; apply fold_2; auto. - rewrite H2; auto. - rewrite (H2 0); auto. - rewrite H. - simpl; auto. - Qed. - - (** more properties of [cardinal] *) - - Lemma empty_cardinal : cardinal empty = 0. - Proof. - rewrite cardinal_fold; apply fold_1; auto with set. - Qed. - - Hint Immediate empty_cardinal cardinal_1 : set. - - Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1. - Proof. - intros. - rewrite (singleton_equal_add x). - replace 0 with (cardinal empty); auto with set. - apply cardinal_2 with x; auto with set. - Qed. - - Hint Resolve singleton_cardinal: set. - - Lemma diff_inter_cardinal : - forall s s', cardinal (diff s s') + cardinal (inter s s') = cardinal s . - Proof. - intros; do 3 rewrite cardinal_fold. - rewrite <- fold_plus. - apply fold_diff_inter with (eqA:=@Logic.eq nat); auto. - Qed. - - Lemma union_cardinal: - forall s s', (forall x, ~(In x s/\In x s')) -> - cardinal (union s s')=cardinal s+cardinal s'. - Proof. - intros; do 3 rewrite cardinal_fold. - rewrite <- fold_plus. - apply fold_union; auto. - Qed. - - Lemma subset_cardinal : - forall s s', s[<=]s' -> cardinal s <= cardinal s' . - Proof. - intros. - rewrite <- (diff_inter_cardinal s' s). - rewrite (inter_sym s' s). - rewrite (inter_subset_equal H); auto with arith. - Qed. - - 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. - do 4 rewrite cardinal_fold. - do 2 rewrite <- fold_plus. - apply fold_union_inter with (eqA:=@Logic.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. - intros; generalize (union_inter_cardinal s s'). - intros; rewrite <- H; auto with arith. - Qed. - - Lemma add_cardinal_1 : - forall s x, In x s -> cardinal (add x s) = cardinal s. - Proof. - auto with set. - Qed. - - Lemma add_cardinal_2 : - forall s x, ~In x s -> cardinal (add x s) = S (cardinal s). - Proof. - intros. - do 2 rewrite cardinal_fold. - change S with ((fun _ => S) x); - apply fold_add with (eqA:=@Logic.eq nat); auto. - Qed. - - Lemma remove_cardinal_1 : - forall s x, In x s -> S (cardinal (remove x s)) = cardinal s. - Proof. - intros. - do 2 rewrite cardinal_fold. - change S with ((fun _ =>S) x). - apply remove_fold_1 with (eqA:=@Logic.eq nat); auto. - Qed. - - Lemma remove_cardinal_2 : - forall s x, ~In x s -> cardinal (remove x s) = cardinal s. - Proof. - auto with set. - Qed. - - Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2. - -End Properties. diff --git a/theories/FSets/FSets.v b/theories/FSets/FSets.v index 6751eb427..012c0d60b 100644 --- a/theories/FSets/FSets.v +++ b/theories/FSets/FSets.v @@ -11,8 +11,11 @@ Require Export OrderedType. Require Export OrderedTypeEx. Require Export OrderedTypeAlt. +Require Export DecidableType. +Require Export DecidableTypeEx. Require Export FSetInterface. Require Export FSetBridge. Require Export FSetProperties. Require Export FSetEqProperties. +Require Export FSetWeakList. Require Export FSetList. |