Library Coq.MSets.MSetEqProperties

Finite sets library

This module proves many properties of finite sets that are consequences of the axiomatization in FsetInterface 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 MSetProperties Zerob Sumbool Lia DecidableTypeEx.
Require FSetEqProperties.

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

Lemma equal_mem_1:
  (forall a, mem a s =mem a s') -> equal s s'=true.

Lemma equal_mem_2:
  equal s s'=true -> forall a, mem a s =mem a s'.

Lemma subset_mem_1:
  (forall a, mem a s =true ->mem a s'=true ) -> subset s s'=true.

Lemma subset_mem_2:
  subset s s'=true -> forall a, mem a s =true -> mem a s'=true.

Lemma empty_mem: mem x empty =false.

Lemma is_empty_equal_empty: is_empty s = equal s empty.

Lemma choose_mem_1: choose s =Some x -> mem x s =true.

Lemma choose_mem_2: choose s =None -> is_empty s =true.

Lemma add_mem_1: mem x (add x s)=true.

Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s.

Lemma remove_mem_1: mem x (remove x s)=false.

Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s.

Lemma singleton_equal_add:
  equal (singleton x) (add x empty)=true.

Lemma union_mem:
  mem x (union s s')=mem x s || mem x s'.

Lemma inter_mem:
  mem x (inter s s')=mem x s && mem x s'.

Lemma diff_mem:
  mem x (diff s s')=mem x s && negb (mem x s').

properties of mem

Lemma mem_3 : ~In x s -> mem x s =false.

Lemma mem_4 : mem x s =false -> ~In x s.

Properties of equal

Lemma equal_refl: equal s s =true.

Lemma equal_sym: equal s s'=equal s' s.

Lemma equal_trans:
equal s s'=true -> equal s' s''=true -> equal s s''=true.

Lemma equal_equal:
equal s s'=true -> equal s s''=equal s' s''.

Lemma equal_cardinal:
equal s s'=true -> cardinal s =cardinal s'.

Lemma subset_refl: subset s s =true.

Lemma subset_antisym:
subset s s'=true -> subset s' s =true -> equal s s'=true.

Lemma subset_trans:
subset s s'=true -> subset s' s''=true -> subset s s''=true.

Lemma subset_equal:
equal s s'=true -> subset s s'=true.

Properties of choose

Lemma choose_mem_3:
is_empty s =false -> {x :elt |choose s =Some x /\ mem x s =true }.

Lemma choose_mem_4: choose empty =None.

Properties of add

Lemma add_mem_3:
mem y s =true -> mem y (add x s)=true.

Lemma add_equal:
mem x s =true -> equal (add x s) s =true.

Properties of remove

Lemma remove_mem_3:
mem y (remove x s)=true -> mem y s =true.

Lemma remove_equal:
mem x s =false -> equal (remove x s) s =true.

Lemma add_remove:
mem x s =true -> equal (add x (remove x s)) s =true.

Lemma remove_add:
mem x s =false -> equal (remove x (add x s)) s =true.

Properties of is_empty

Lemma is_empty_cardinal: is_empty s = zerob (cardinal s).

Properties of singleton

Lemma singleton_mem_1: mem x (singleton x)=true.

Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false.

Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y.

Properties of union

Lemma union_sym:
equal (union s s') (union s' s)=true.

Lemma union_subset_equal:
subset s s'=true -> equal (union s s') s'=true.

Lemma union_equal_1:
equal s s'=true -> equal (union s s'') (union s' s'')=true.

Lemma union_equal_2:
equal s' s''=true -> equal (union s s') (union s s'')=true.

Lemma union_assoc:
equal (union (union s s') s'') (union s (union s' s''))=true.

Lemma add_union_singleton:
equal (add x s) (union (singleton x) s)=true.

Lemma union_add:
equal (union (add x s) s') (add x (union s s'))=true.

Lemma union_subset_1: subset s (union s s')=true.

Lemma union_subset_2: subset s' (union s s')=true.

Lemma union_subset_3:
subset s s''=true -> subset s' s''=true ->
subset (union s s') s''=true.

Properties of inter

Lemma inter_sym: equal (inter s s') (inter s' s)=true.

Lemma inter_subset_equal:
subset s s'=true -> equal (inter s s') s =true.

Lemma inter_equal_1:
equal s s'=true -> equal (inter s s'') (inter s' s'')=true.

Lemma inter_equal_2:
equal s' s''=true -> equal (inter s s') (inter s s'')=true.

Lemma inter_assoc:
equal (inter (inter s s') s'') (inter s (inter s' s''))=true.

Lemma union_inter_1:
equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))=true.

Lemma union_inter_2:
equal (union (inter s s') s'') (inter (union s s'') (union s' s''))=true.

Lemma inter_add_1: mem x s'=true ->
equal (inter (add x s) s') (add x (inter s s'))=true.

Lemma inter_add_2: mem x s'=false ->
equal (inter (add x s) s') (inter s s')=true.

Lemma inter_subset_1: subset (inter s s') s =true.

Lemma inter_subset_2: subset (inter s s') s'=true.

Lemma inter_subset_3:
subset s'' s =true -> subset s'' s'=true ->
subset s'' (inter s s')=true.

Properties of diff

Lemma diff_subset: subset (diff s s') s =true.

Lemma diff_subset_equal:
subset s s'=true -> equal (diff s s') empty =true.

Lemma remove_inter_singleton:
equal (remove x s) (diff s (singleton x))=true.

Lemma diff_inter_empty:
equal (inter (diff s s') (inter s s')) empty =true.

Lemma diff_inter_all:
equal (union (diff s s') (inter s s')) s =true.

End BasicProperties.

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

Properties of fold

Lemma exclusive_set : forall s s' x,
~(In x s /\In x s') <-> mem x s && mem x s'=false.

Section Fold.
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).
Variables (i:A).
Variables (s s':t)(x:elt).

Lemma fold_empty: (fold f empty i ) = i.

Lemma fold_equal:
equal s s'=true -> eqA (fold f s i) (fold f s' i).

Lemma fold_add:
mem x s =false -> eqA (fold f (add x s) i) (f x (fold f s i)).

Lemma add_fold:
mem x s =true -> eqA (fold f (add x s) i) (fold f s i).

Lemma remove_fold_1:
mem x s =true -> eqA (f x (fold f (remove x s) i)) (fold f s i).

Lemma remove_fold_2:
mem x s =false -> eqA (fold f (remove x s) i) (fold f s i).

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

End Fold.

Properties of cardinal

Lemma add_cardinal_1:
forall s x, mem x s =true -> cardinal (add x s)=cardinal s.

Lemma add_cardinal_2:
forall s x, mem x s =false -> cardinal (add x s)=S (cardinal s).

Lemma remove_cardinal_1:
forall s x, mem x s =true -> S (cardinal (remove x s))=cardinal s.

Lemma remove_cardinal_2:
forall s x, mem x s =false -> cardinal (remove x s)=cardinal s.

Lemma union_cardinal:
forall s s', (forall x, mem x s && mem x s'=false ) ->
cardinal (union s s')=cardinal s +cardinal s'.

Lemma subset_cardinal:
forall s s', subset s s'=true -> cardinal s <=cardinal s'.

Section Bool.

Properties of filter

Variable f:elt ->bool.
Variable Comp: Proper (E.eq ==>Logic.eq) f.

Let Comp' : Proper (E.eq ==>Logic.eq) (fun x =>negb (f x)).

Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x.

Lemma for_all_filter:
forall s, for_all f s =is_empty (filter (fun x => negb (f x)) s).

Lemma exists_filter :
forall s, exists_ f s =negb (is_empty (filter f s)).

Lemma partition_filter_1:
forall s, equal (fst (partition f s)) (filter f s)=true.

Lemma partition_filter_2:
forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true.

Lemma filter_add_1 : forall s x, f x = true ->
filter f (add x s) [=] add x (filter f s).

Lemma filter_add_2 : forall s x, f x = false ->
filter f (add x s) [=] filter f s.

Lemma add_filter_1 : forall s s' x,
f x =true -> (Add x s s') -> (Add x (filter f s) (filter f s')).

Lemma add_filter_2 : forall s s' x,
f x =false -> (Add x s s') -> filter f s [=] filter f s'.

Lemma union_filter: forall f g,
Proper (E.eq ==>Logic.eq) f -> Proper (E.eq ==>Logic.eq) g ->
forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s.

Lemma filter_union: forall s s', filter f (union s s') [=] union (filter f s) (filter f s').

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.

Lemma for_all_mem_2: forall s,
(for_all f s )=true -> forall x,(mem x s )=true -> (f x )=true.

Lemma for_all_mem_3:
forall s x,(mem x s )=true -> (f x )=false -> (for_all f s )=false.

Lemma for_all_mem_4:
forall s, for_all f s =false -> {x :elt | mem x s =true /\ f x =false }.

Properties of exists

Lemma for_all_exists:
forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s).

End Bool.
Section Bool'.

Variable f:elt ->bool.
Variable Comp: Proper (E.eq ==>Logic.eq) f.

Local Definition Comp' : Proper (E.eq ==>Logic.eq) (fun x => negb (f x)).

Local Hint Resolve Comp' : core.

Lemma exists_mem_1:
forall s, (forall x, mem x s =true ->f x =false ) -> exists_ f s =false.

Lemma exists_mem_2:
forall s, exists_ f s =false -> forall x, mem x s =true -> f x =false.

Lemma exists_mem_3:
forall s x, mem x s =true -> f x =true -> exists_ f s =true.

Lemma exists_mem_4:
forall s, exists_ f s =true -> {x :elt | (mem x s )=true /\ (f x )=true }.

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 := (Proper (E.eq ==>Logic.eq ==>Logic.eq)).
Notation transposeL := (transpose Logic.eq).

Lemma sum_plus :
  forall f g,
  Proper (E.eq ==>Logic.eq) f -> Proper (E.eq ==>Logic.eq) g ->
    forall s, sum (fun x =>f x +g x) s = sum f s + sum g s.

Lemma sum_filter : forall f : elt -> bool, Proper (E.eq ==>Logic.eq) f ->
  forall s, (sum (fun x => if f x then 1 else 0) s ) = (cardinal (filter f s)).

Lemma fold_compat :
  forall (A:Type)(eqA:A ->A ->Prop)(st:Equivalence eqA)
  (f g:elt ->A ->A),
  Proper (E.eq ==>eqA ==>eqA) f -> transpose eqA f ->
  Proper (E.eq ==>eqA ==>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)).

Lemma sum_compat :
  forall f g, Proper (E.eq ==>Logic.eq) f -> Proper (E.eq ==>Logic.eq) g ->
  forall s, (forall x, In x s -> f x =g x ) -> sum f s =sum g s.

End Sum.

End WEqPropertiesOn.

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 EqProperties functor which is meant to be used on modules (M:S) can simply be an alias of WEqProperties.

Module WEqProperties (M:WSets) := WEqPropertiesOn M.E M.
Module EqProperties := WEqProperties.

Library Coq.MSets.MSetEqProperties

Finite sets library

Navigation