Library Stdlib.MSets.MSetProperties

Finite sets library

This functor derives additional properties from MSetInterface.S. Contrary to the functor in MSetEqProperties 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 MSetInterface.
Require Import PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide.
Set Implicit Arguments.

Local Ltac Tauto.intuition_solver ::= auto with relations.

#[global]
Hint Unfold transpose : core.

First, a functor for Weak Sets in functorial version.

Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
  Module Import Dec := WDecideOn 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.

  #[global]
  Hint Immediate equal_sym add_remove remove_add union_sym inter_sym: set.
  #[global]
  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.

Lemma elements_empty : elements empty = nil.

Conversions between lists and sets

  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.

Fold

  Section Fold.

  Notation NoDup := (NoDupA E.eq).
  Notation InA := (InA E.eq).

Alternative specification via fold_right

Lemma fold_spec_right (s:t)(A:Type)(i:A)(f : elt -> A -> A) :
fold f s i = List.fold_right f i (rev (elements s)).

Induction principles for fold (contributed by S. Lescuyer)

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.

Lemma fold_identity : forall s, fold add s empty [=] s.

Alternative (weaker) specifications for fold

When MSets 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),
   Proper (E.eq ==>eqA ==>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:Proper (E.eq ==>eqA ==>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)).

Fold is a morphism

  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).

Fold and other set operators

  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.

Cardinal

Characterization of cardinal in terms of fold

Lemma cardinal_fold : forall s, cardinal s = fold (fun _ => S) s 0.

Old specifications for cardinal.

  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).

Cardinal and (non-)emptiness

  Lemma cardinal_Empty : forall s, Empty s <-> cardinal s = 0.

  Lemma cardinal_inv_1 : forall s, cardinal s = 0 -> Empty s.
  #[global]
  Hint Resolve cardinal_inv_1 : core.

  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 }.

Cardinal is a morphism

  Lemma Equal_cardinal : forall s s', s [=]s' -> cardinal s = cardinal s'.

#[global]
  Instance cardinal_m : Proper (Equal ==>Logic.eq) cardinal.

  #[global]
  Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : core.

Cardinal and set operators

  Lemma empty_cardinal : cardinal empty = 0.

  #[global]
  Hint Immediate empty_cardinal cardinal_1 : set.

  Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1.

  #[global]
  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.

  #[global]
  Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : core.

End WPropertiesOn.

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.

Module WProperties (M:WSets) := WPropertiesOn M.E M.
Module Properties := WProperties.

Now comes some properties specific to the element ordering, invalid for Weak Sets.

Module OrdProperties (M:Sets).
  Module Import ME:=OrderedTypeFacts(M.E).
  Module Import ML:=OrderedTypeLists(M.E).
  Module Import P := Properties M.
  Import FM.
  Import M.E.
  Import M.

  #[global]
  Hint Resolve elements_spec2 : core.
  #[global]
  Hint Immediate
    min_elt_spec1 min_elt_spec2 min_elt_spec3
    max_elt_spec1 max_elt_spec2 max_elt_spec3 : set.

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.

#[global]
  Instance gtb_compat x : Proper (E.eq ==>Logic.eq) (gtb x).

#[global]
  Instance leb_compat x : Proper (E.eq ==>Logic.eq) (leb x).
  #[global]
  Hint Resolve gtb_compat leb_compat : core.

  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),
   Proper (E.eq ==>eqA ==>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),
   Proper (E.eq ==>eqA ==>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:Proper (E.eq ==>eqA ==>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

  Lemma choose_equal : forall s s', Equal s s' ->
    match choose s, choose s' with
      | Some x, Some x' => E.eq x x'
      | None, None => True
      | _, _ => False
     end.

End OrdProperties.