Library Coq.FSets.FSetProperties

Finite sets library

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.
Set Implicit Arguments.

Hint Unfold transpose compat_op Proper respectful.
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.

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.

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

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

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

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

Cardinal is a morphism

  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.

Cardinal and set operators

  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.

Module WProperties (M:WS) := WProperties_fun M.E M.
Module Properties := 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, Proper (E.eq ==>Logic.eq) (gtb x).

  Lemma leb_compat : forall x, Proper (E.eq ==>Logic.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

  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.