Library Coq.FSets.FSetProperties
This functor derives additional properties from FSetInterface.S.
Contrary to the functor in FSetEqProperties 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 FSetInterface.
Require Import DecidableTypeEx FSetFacts FSetDecide.
Hint Unfold transpose compat_op.
Hint Extern 1 (Equivalence _) => constructor; congruence.
First, a functor for Weak Sets in functorial version.
Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
Module Import Dec := WDecide_fun E M.
Module Import FM := Dec.F .
Import M.
Lemma In_dec : forall x s, {In x s} + {~ In x s}.
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.
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.
Lemma equal_sym : s[=]s' -> s'[=]s.
Lemma equal_trans : s1[=]s2 -> s2[=]s3 -> s1[=]s3.
Lemma subset_refl : s[<=]s.
Lemma subset_trans : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3.
Lemma subset_antisym : s[<=]s' -> s'[<=]s -> s[=]s'.
Lemma subset_equal : s[=]s' -> s[<=]s'.
Lemma subset_empty : empty[<=]s.
Lemma subset_remove_3 : s1[<=]s2 -> remove x s1 [<=] s2.
Lemma subset_diff : s1[<=]s3 -> diff s1 s2 [<=] s3.
Lemma subset_add_3 : In x s2 -> s1[<=]s2 -> add x s1 [<=] s2.
Lemma subset_add_2 : s1[<=]s2 -> s1[<=] add x s2.
Lemma in_subset : In x s1 -> s1[<=]s2 -> In x s2.
Lemma double_inclusion : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1.
Lemma empty_is_empty_1 : Empty s -> s[=]empty.
Lemma empty_is_empty_2 : s[=]empty -> Empty s.
Lemma add_equal : In x s -> add x s [=] s.
Lemma add_add : add x (add x' s) [=] add x' (add x s).
Lemma remove_equal : ~ In x s -> remove x s [=] s.
Lemma Equal_remove : s[=]s' -> remove x s [=] remove x s'.
Lemma add_remove : In x s -> add x (remove x s) [=] s.
Lemma remove_add : ~In x s -> remove x (add x s) [=] s.
Lemma singleton_equal_add : singleton x [=] add x empty.
Lemma remove_singleton_empty :
In x s -> remove x s [=] empty -> singleton x [=] s.
Lemma union_sym : union s s' [=] union s' s.
Lemma union_subset_equal : s[<=]s' -> union s s' [=] s'.
Lemma union_equal_1 : s[=]s' -> union s s'' [=] union s' s''.
Lemma union_equal_2 : s'[=]s'' -> union s s' [=] union s s''.
Lemma union_assoc : union (union s s') s'' [=] union s (union s' s'').
Lemma add_union_singleton : add x s [=] union (singleton x) s.
Lemma union_add : union (add x s) s' [=] add x (union s s').
Lemma union_remove_add_1 :
union (remove x s) (add x s') [=] union (add x s) (remove x s').
Lemma union_remove_add_2 : In x s ->
union (remove x s) (add x s') [=] union s s'.
Lemma union_subset_1 : s [<=] union s s'.
Lemma union_subset_2 : s' [<=] union s s'.
Lemma union_subset_3 : s[<=]s'' -> s'[<=]s'' -> union s s' [<=] s''.
Lemma union_subset_4 : s[<=]s' -> union s s'' [<=] union s' s''.
Lemma union_subset_5 : s[<=]s' -> union s'' s [<=] union s'' s'.
Lemma empty_union_1 : Empty s -> union s s' [=] s'.
Lemma empty_union_2 : Empty s -> union s' s [=] s'.
Lemma not_in_union : ~In x s -> ~In x s' -> ~In x (union s s').
Lemma inter_sym : inter s s' [=] inter s' s.
Lemma inter_subset_equal : s[<=]s' -> inter s s' [=] s.
Lemma inter_equal_1 : s[=]s' -> inter s s'' [=] inter s' s''.
Lemma inter_equal_2 : s'[=]s'' -> inter s s' [=] inter s s''.
Lemma inter_assoc : inter (inter s s') s'' [=] inter s (inter s' s'').
Lemma union_inter_1 : inter (union s s') s'' [=] union (inter s s'') (inter s' s'').
Lemma union_inter_2 : union (inter s s') s'' [=] inter (union s s'') (union s' s'').
Lemma inter_add_1 : In x s' -> inter (add x s) s' [=] add x (inter s s').
Lemma inter_add_2 : ~ In x s' -> inter (add x s) s' [=] inter s s'.
Lemma empty_inter_1 : Empty s -> Empty (inter s s').
Lemma empty_inter_2 : Empty s' -> Empty (inter s s').
Lemma inter_subset_1 : inter s s' [<=] s.
Lemma inter_subset_2 : inter s s' [<=] s'.
Lemma inter_subset_3 :
s''[<=]s -> s''[<=]s' -> s''[<=] inter s s'.
Lemma empty_diff_1 : Empty s -> Empty (diff s s').
Lemma empty_diff_2 : Empty s -> diff s' s [=] s'.
Lemma diff_subset : diff s s' [<=] s.
Lemma diff_subset_equal : s[<=]s' -> diff s s' [=] empty.
Lemma remove_diff_singleton :
remove x s [=] diff s (singleton x).
Lemma diff_inter_empty : inter (diff s s') (inter s s') [=] empty.
Lemma diff_inter_all : union (diff s s') (inter s s') [=] s.
Lemma Add_add : Add x s (add x s).
Lemma Add_remove : In x s -> Add x (remove x s) s.
Lemma union_Add : Add x s s' -> Add x (union s s'') (union s' s'').
Lemma inter_Add :
In x s'' -> Add x s s' -> Add x (inter s s'') (inter s' s'').
Lemma union_Equal :
In x s'' -> Add x s s' -> union s s'' [=] union s' s''.
Lemma inter_Add_2 :
~In x s'' -> Add x s s' -> inter s s'' [=] inter s' s''.
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.
Lemma elements_Empty : forall s, Empty s <-> elements s = nil.
Lemma elements_empty : elements empty = nil.
Definition of_list (l : list elt) := List.fold_right add empty l.
Definition to_list := elements.
Lemma of_list_1 : forall l x, In x (of_list l) <-> InA E.eq x l.
Lemma of_list_2 : forall l, equivlistA E.eq (to_list (of_list l)) l.
Lemma of_list_3 : forall s, of_list (to_list s) [=] s.
In the following lemma, the step hypothesis is deliberately restricted
to the precise set s we are considering.
Theorem fold_rec :
forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A)(s:t),
(forall s', Empty s' -> P s' i) ->
(forall x a s' s'', In x s -> ~In x s' -> Add x s' s'' ->
P s' a -> P s'' (f x a)) ->
P s (fold f s i).
Same, with empty and add instead of Empty and Add. In this
case, P must be compatible with equality of sets
Theorem fold_rec_bis :
forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A)(s:t),
(forall s s' a, s[=]s' -> P s a -> P s' a) ->
(P empty i) ->
(forall x a s', In x s -> ~In x s' -> P s' a -> P (add x s') (f x a)) ->
P s (fold f s i).
Lemma fold_rec_nodep :
forall (A:Type)(P : A -> Type)(f : elt -> A -> A)(i:A)(s:t),
P i -> (forall x a, In x s -> P a -> P (f x a)) ->
P (fold f s i).
fold_rec_weak is a weaker principle than fold_rec_bis :
the step hypothesis must here be applicable to any x.
At the same time, it looks more like an induction principle,
and hence can be easier to use.
Lemma fold_rec_weak :
forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A),
(forall s s' a, s[=]s' -> P s a -> P s' a) ->
P empty i ->
(forall x a s, ~In x s -> P s a -> P (add x s) (f x a)) ->
forall s, P s (fold f s i).
Lemma fold_rel :
forall (A B:Type)(R : A -> B -> Type)
(f : elt -> A -> A)(g : elt -> B -> B)(i : A)(j : B)(s : t),
R i j ->
(forall x a b, In x s -> R a b -> R (f x a) (g x b)) ->
R (fold f s i) (fold g s j).
From the induction principle on fold, we can deduce some general
induction principles on sets.
Lemma set_induction :
forall P : t -> Type,
(forall s, Empty s -> P s) ->
(forall s s', P s -> forall x, ~In x s -> Add x s s' -> P s') ->
forall s, P s.
Lemma set_induction_bis :
forall P : t -> Type,
(forall s s', s [=] s' -> P s -> P s') ->
P empty ->
(forall x s, ~In x s -> P s -> P (add x s)) ->
forall s, P s.
fold can be used to reconstruct the same initial set.
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 : Type) (i : A) (f : elt -> A -> A),
exists l : list elt,
NoDup l /\
(forall x : elt, In x s <-> InA x l) /\
fold f s i = fold_right f i l.
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 : Type) (eqA : A -> A -> Prop)
(st : Equivalence eqA) (i : A) (f : elt -> A -> A),
Empty s -> eqA (fold f s i) i.
Lemma fold_2 :
forall s s' x (A : Type) (eqA : A -> A -> Prop)
(st : Equivalence 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)).
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 : Type)(i : A) (f : elt -> A -> A),
Empty s -> (fold f s i) = i.
Section Fold_More.
Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
Lemma fold_commutes : forall i s x,
eqA (fold f s (f x i)) (f x (fold f s i)).
Lemma fold_init : forall i i' s, eqA i i' ->
eqA (fold f s i) (fold f s i').
Lemma fold_equal :
forall i s s', s[=]s' -> eqA (fold f s i) (fold f s' i).
Lemma fold_empty : forall i, fold f empty i = i.
Lemma fold_add : forall i s x, ~In x s ->
eqA (fold f (add x s) i) (f x (fold f s i)).
Lemma add_fold : forall i s x, In x s ->
eqA (fold f (add x s) i) (fold f s i).
Lemma remove_fold_1: forall i s x, In x s ->
eqA (f x (fold f (remove x s) i)) (fold f s i).
Lemma remove_fold_2: forall i s x, ~In x s ->
eqA (fold f (remove x s) i) (fold f s i).
Lemma fold_union_inter : forall i s s',
eqA (fold f (union s s') (fold f (inter s s') i))
(fold f s (fold f s' i)).
Lemma fold_diff_inter : forall i s s',
eqA (fold f (diff s s') (fold f (inter s s') i)) (fold f s i).
Lemma fold_union: forall i s s',
(forall x, ~(In x s/\In x s')) ->
eqA (fold f (union s s') i) (fold f s (fold f s' i)).
End Fold_More.
Lemma fold_plus :
forall s p, fold (fun _ => S) s p = fold (fun _ => S) s 0 + p.
End Fold.
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.
Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0.
Lemma cardinal_2 :
forall s s' x, ~ In x s -> Add x s s' -> cardinal s' = S (cardinal s).
Lemma cardinal_Empty : forall s, Empty s <-> cardinal s = 0.
Lemma cardinal_inv_1 : forall s, cardinal s = 0 -> Empty s.
Hint Resolve cardinal_inv_1.
Lemma cardinal_inv_2 :
forall s n, cardinal s = S n -> { x : elt | In x s }.
Lemma cardinal_inv_2b :
forall s, cardinal s <> 0 -> { x : elt | In x s }.
Lemma Equal_cardinal : forall s s', s[=]s' -> cardinal s = cardinal s'.
Add Morphism cardinal : cardinal_m.
Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal.
Lemma empty_cardinal : cardinal empty = 0.
Hint Immediate empty_cardinal cardinal_1 : set.
Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1.
Hint Resolve singleton_cardinal: set.
Lemma diff_inter_cardinal :
forall s s', cardinal (diff s s') + cardinal (inter s s') = cardinal s .
Lemma union_cardinal:
forall s s', (forall x, ~(In x s/\In x s')) ->
cardinal (union s s')=cardinal s+cardinal s'.
Lemma subset_cardinal :
forall s s', s[<=]s' -> cardinal s <= cardinal s' .
Lemma subset_cardinal_lt :
forall s s' x, s[<=]s' -> In x s' -> ~In x s -> cardinal s < cardinal s'.
Theorem union_inter_cardinal :
forall s s', cardinal (union s s') + cardinal (inter s s') = cardinal s + cardinal s' .
Lemma union_cardinal_inter :
forall s s', cardinal (union s s') = cardinal s + cardinal s' - cardinal (inter s s').
Lemma union_cardinal_le :
forall s s', cardinal (union s s') <= cardinal s + cardinal s'.
Lemma add_cardinal_1 :
forall s x, In x s -> cardinal (add x s) = cardinal s.
Lemma add_cardinal_2 :
forall s x, ~In x s -> cardinal (add x s) = S (cardinal s).
Lemma remove_cardinal_1 :
forall s x, In x s -> S (cardinal (remove x s)) = cardinal s.
Lemma remove_cardinal_2 :
forall s x, ~In x s -> cardinal (remove x s) = cardinal s.
Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2.
End WProperties_fun.
Now comes variants for self-contained weak sets and for full sets.
For these variants, only one argument is necessary. Thanks to
the subtyping WS<=S, the Properties functor which is meant to be
used on modules (M:S) can simply be an alias of WProperties.
Now comes some properties specific to the element ordering,
invalid for Weak Sets.
Module OrdProperties (M:S).
Module ME:=OrderedTypeFacts(M.E).
Module Import P := Properties M.
Import FM.
Import M.E.
Import M.
First, a specialized version of SortA_equivlistA_eqlistA:
Lemma sort_equivlistA_eqlistA : forall l l' : list elt,
sort E.lt l -> sort E.lt l' -> equivlistA E.eq l l' -> eqlistA E.eq l l'.
Definition gtb x y := match E.compare x y with GT _ => true | _ => false end.
Definition leb x := fun y => negb (gtb x y).
Definition elements_lt x s := List.filter (gtb x) (elements s).
Definition elements_ge x s := List.filter (leb x) (elements s).
Lemma gtb_1 : forall x y, gtb x y = true <-> E.lt y x.
Lemma leb_1 : forall x y, leb x y = true <-> ~E.lt y x.
Lemma gtb_compat : forall x, compat_bool E.eq (gtb x).
Lemma leb_compat : forall x, compat_bool E.eq (leb x).
Hint Resolve gtb_compat leb_compat.
Lemma elements_split : forall x s,
elements s = elements_lt x s ++ elements_ge x s.
Lemma elements_Add : forall s s' x, ~In x s -> Add x s s' ->
eqlistA E.eq (elements s') (elements_lt x s ++ x :: elements_ge x s).
Definition Above x s := forall y, In y s -> E.lt y x.
Definition Below x s := forall y, In y s -> E.lt x y.
Lemma elements_Add_Above : forall s s' x,
Above x s -> Add x s s' ->
eqlistA E.eq (elements s') (elements s ++ x::nil).
Lemma elements_Add_Below : forall s s' x,
Below x s -> Add x s s' ->
eqlistA E.eq (elements s') (x::elements s).
sort E.lt l -> sort E.lt l' -> equivlistA E.eq l l' -> eqlistA E.eq l l'.
Definition gtb x y := match E.compare x y with GT _ => true | _ => false end.
Definition leb x := fun y => negb (gtb x y).
Definition elements_lt x s := List.filter (gtb x) (elements s).
Definition elements_ge x s := List.filter (leb x) (elements s).
Lemma gtb_1 : forall x y, gtb x y = true <-> E.lt y x.
Lemma leb_1 : forall x y, leb x y = true <-> ~E.lt y x.
Lemma gtb_compat : forall x, compat_bool E.eq (gtb x).
Lemma leb_compat : forall x, compat_bool E.eq (leb x).
Hint Resolve gtb_compat leb_compat.
Lemma elements_split : forall x s,
elements s = elements_lt x s ++ elements_ge x s.
Lemma elements_Add : forall s s' x, ~In x s -> Add x s s' ->
eqlistA E.eq (elements s') (elements_lt x s ++ x :: elements_ge x s).
Definition Above x s := forall y, In y s -> E.lt y x.
Definition Below x s := forall y, In y s -> E.lt x y.
Lemma elements_Add_Above : forall s s' x,
Above x s -> Add x s s' ->
eqlistA E.eq (elements s') (elements s ++ x::nil).
Lemma elements_Add_Below : forall s s' x,
Below x s -> Add x s s' ->
eqlistA E.eq (elements s') (x::elements s).
Two other induction principles on sets: we can be more restrictive
on the element we add at each step.
Lemma set_induction_max :
forall P : t -> Type,
(forall s : t, Empty s -> P s) ->
(forall s s', P s -> forall x, Above x s -> Add x s s' -> P s') ->
forall s : t, P s.
Lemma set_induction_min :
forall P : t -> Type,
(forall s : t, Empty s -> P s) ->
(forall s s', P s -> forall x, Below x s -> Add x s s' -> P s') ->
forall s : t, P s.
More properties of fold : behavior with respect to Above/Below
Lemma fold_3 :
forall s s' x (A : Type) (eqA : A -> A -> Prop)
(st : Equivalence eqA) (i : A) (f : elt -> A -> A),
compat_op E.eq eqA f ->
Above x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
Lemma fold_4 :
forall s s' x (A : Type) (eqA : A -> A -> Prop)
(st : Equivalence eqA) (i : A) (f : elt -> A -> A),
compat_op E.eq eqA f ->
Below x s -> Add x s s' -> eqA (fold f s' i) (fold f s (f x i)).
The following results have already been proved earlier,
but we can now prove them with one hypothesis less:
no need for (transpose eqA f).
Section FoldOpt.
Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f).
Lemma fold_equal :
forall i s s', s[=]s' -> eqA (fold f s i) (fold f s' i).
Lemma add_fold : forall i s x, In x s ->
eqA (fold f (add x s) i) (fold f s i).
Lemma remove_fold_2: forall i s x, ~In x s ->
eqA (fold f (remove x s) i) (fold f s i).
End FoldOpt.
An alternative version of choose_3