Library Lib_FinSet
Require Import OrderedTypeEx.
Require Import Lib_Tactic Lib_MyFSetInterface.
Module Type FinSet.
Declare Module E : UsualOrderedType.
These finite sets are compatible with Coq's FSet library, except with
respect to
Hint
s. MyFSetInterface.S
is a redeclaration of
FSetInterface.S
with all the Hint
s placed in the sets
database
instead of core
. This is mainly to avoid polluting the core
database
with lemmas that are only usable by eauto
.
Declare Module S : Lib_MyFSetInterface.S with Module E := E.
Define aliases.
Definition fset := S.t.
Definition elt := S.elt.
Equality on these sets is extensional.
Parameter eq_ext :
forall s s' : fset, (forall a : elt, S.In a s <-> S.In a s') -> s = s'.
Parameter eq_if_Equal :
forall s s' : fset, S.Equal s s' -> s = s'.
Notations.
Notation "{}" := (S.empty) : set_scope.
Notation "{{ x }}" := (S.singleton x) : set_scope.
Notation "E \u F" := (S.union E F)
(at level 68, left associativity) : set_scope.
Notation "x \in E" := (S.In x E) (at level 69) : set_scope.
Notation "x \notin E" := (~(S.In x E)) (at level 69) : set_scope.
Notation "E << F" := (S.Subset E F) (at level 70) : set_scope.
End FinSet.
Module FinSetFacts (M : FinSet).
Import M.
Open Local Scope set_scope.
Interaction of in with constructions
Lemma in_empty : forall x,
x \in {} -> False.
Lemma in_singleton : forall x y,
x \in {{y}} <-> x = y.
Lemma in_union : forall x E F,
x \in (E \u F) <-> (x \in E) \/ (x \in F).
Properties of union
Lemma union_same : forall E,
E \u E = E.
Lemma union_comm : forall E F,
E \u F = F \u E.
Lemma union_assoc : forall E F G,
E \u (F \u G) = (E \u F) \u G.
Lemma union_empty_l : forall E,
{} \u E = E.
More properties of in
Lemma in_same : forall x,
x \in {{x}}.
More properties of union
Lemma union_empty_r : forall E,
E \u {} = E.
Lemma union_comm_assoc : forall E F G,
E \u (F \u G) = F \u (E \u G).
Subset relation properties
Lemma subset_refl : forall E,
E << E.
Lemma subset_trans : forall F E G,
E << F -> F << G -> E << G.
Interaction of subset with constructions
Lemma subset_empty_l : forall E,
{} << E.
Lemma subset_singleton : forall x E,
x \in E <-> {{x}} << E.
Lemma subset_union_weak_l : forall E F,
E << (E \u F).
Lemma subset_union_weak_r : forall E F,
F << (E \u F).
Lemma subset_union_l : forall E F G,
(E \u F) << G <-> (E << G) /\ (F << G).
Interaction of notin with constructions
Lemma notin_empty : forall x,
x \notin {}.
Lemma notin_singleton : forall x y,
x \notin {{y}} <-> x <> y.
Lemma notin_same : forall x,
x \notin {{x}} -> False.
Lemma notin_union : forall x E F,
x \notin (E \u F) <-> (x \notin E) /\ (x \notin F).
End FinSetFacts.