Library Stdlib.MSets.MSetFacts

Finite sets library

This functor derives additional facts from MSetInterface.S. These facts are mainly the specifications of MSetInterface.S written using different styles: equivalence and boolean equalities. Moreover, we prove that E.Eq and Equal are setoid equalities.

From Stdlib Require Export FSetInterface.
From Stdlib Require Import DecidableTypeEx.
From Stdlib Require Export MSetInterface.
Set Implicit Arguments.

#[local] Ltac Tauto.intuition_solver ::= auto with relations.

First, a functor for Weak Sets in functorial version.

Module WFactsOn (Import E : DecidableType)(Import M : WSetsOn E).

Definition eqb x y := if eq_dec x y then true else false.

Specifications written using implications :

this used to be the default interface.

Section ImplSpec.
Variable s s' : t.
Variable x y : elt.

Lemma In_1 : E.eq x y -> In x s -> In y s.

Lemma mem_1 : In x s -> mem x s = true.
Lemma mem_2 : mem x s = true -> In x s.

Lemma equal_1 : Equal s s' -> equal s s' = true.
Lemma equal_2 : equal s s' = true -> Equal s s'.

Lemma subset_1 : Subset s s' -> subset s s' = true.
Lemma subset_2 : subset s s' = true -> Subset s s'.

Lemma is_empty_1 : Empty s -> is_empty s = true.
Lemma is_empty_2 : is_empty s = true -> Empty s.

Lemma add_1 : E.eq x y -> In y (add x s).
Lemma add_2 : In y s -> In y (add x s).
Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s.

Lemma remove_1 : E.eq x y -> ~ In y (remove x s).
Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
Lemma remove_3 : In y (remove x s) -> In y s.

Lemma singleton_1 : In y (singleton x) -> E.eq x y.
Lemma singleton_2 : E.eq x y -> In y (singleton x).

Lemma union_1 : In x (union s s') -> In x s \/ In x s'.
Lemma union_2 : In x s -> In x (union s s').
Lemma union_3 : In x s' -> In x (union s s').

Lemma inter_1 : In x (inter s s') -> In x s.
Lemma inter_2 : In x (inter s s') -> In x s'.
Lemma inter_3 : In x s -> In x s' -> In x (inter s s').

Lemma diff_1 : In x (diff s s') -> In x s.
Lemma diff_2 : In x (diff s s') -> ~ In x s'.
Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').

Variable f : elt -> bool.

Lemma filter_1 : compatb f -> In x (filter f s) -> In x s.
Lemma filter_2 : compatb f -> In x (filter f s) -> f x = true.
Lemma filter_3 : compatb f -> In x s -> f x = true -> In x (filter f s).

Lemma for_all_1 : compatb f ->
      For_all (fun x => f x = true) s -> for_all f s = true.
Lemma for_all_2 : compatb f ->
      for_all f s = true -> For_all (fun x => f x = true) s.

Lemma exists_1 : compatb f ->
      Exists (fun x => f x = true) s -> exists_ f s = true.

Lemma exists_2 : compatb f ->
      exists_ f s = true -> Exists (fun x => f x = true) s.

Lemma elements_1 : In x s -> InA E.eq x (elements s).
Lemma elements_2 : InA E.eq x (elements s) -> In x s.

End ImplSpec.

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

Specifications written using equivalences :

this is now provided by the default interface.

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

Lemma mem_iff : In x s <-> mem x s = true.

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

Lemma equal_iff : s [=]s' <-> equal s s' = true.

Lemma subset_iff : s [<=]s' <-> subset s s' = true.

Lemma empty_iff : In x empty <-> False.

Lemma is_empty_iff : Empty s <-> is_empty s = true.

Lemma singleton_iff : In y (singleton x) <-> E.eq x y.

Lemma add_iff : In y (add x s) <-> E.eq x y \/ In y s.

Lemma add_neq_iff : ~ E.eq x y -> (In y (add x s) <-> In y s ).

Lemma remove_iff : In y (remove x s) <-> In y s /\ ~E.eq x y.

Lemma remove_neq_iff : ~ E.eq x y -> (In y (remove x s) <-> In y s ).

Variable f : elt -> bool.

Lemma for_all_iff : Proper (E.eq ==>Logic.eq) f ->
(For_all (fun x => f x = true) s <-> for_all f s = true ).

Lemma exists_iff : Proper (E.eq ==>Logic.eq) f ->
(Exists (fun x => f x = true) s <-> exists_ f s = true ).

Lemma elements_iff : In x s <-> InA E.eq x (elements s).

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.

Lemma empty_b : mem y empty = false.

Lemma add_b : mem y (add x s) = eqb x y || mem y s.

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

Lemma remove_b : mem y (remove x s) = mem y s && negb (eqb x y).

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

Lemma singleton_b : mem y (singleton x) = eqb x y.

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

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

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

Lemma elements_b : mem x s = existsb (eqb x) (elements s).

Variable f : elt ->bool.

Lemma filter_b : Proper (E.eq ==>Logic.eq) f -> mem x (filter f s) = mem x s && f x.

Lemma for_all_b : Proper (E.eq ==>Logic.eq) f ->
for_all f s = forallb f (elements s).

Lemma exists_b : Proper (E.eq ==>Logic.eq) f ->
exists_ f s = existsb f (elements s).

End BoolSpec.

Declarations of morphisms with respects to E.eq and Equal

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

Module WFacts (M:WSets) := WFactsOn M.E M.
Module Facts := WFacts.