Library Lib_FinSet

Require Import OrderedTypeEx.
Require Import Lib_Tactic Lib_MyFSetInterface.

Interface for Finite Sets


Module Type FinSet.
Declare Module E : UsualOrderedType.

These finite sets are compatible with Coq's FSet library, except with respect to Hints. MyFSetInterface.S is a redeclaration of FSetInterface.S with all the Hints 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.

Facts


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.