Library FSetExtra
Definition of when two sets are disjoint.
We make notin a definition for ¬ In x L. We use this
definition whenever possible, so that the intuition tactic
does not turn ¬ In x L into In x L → False.
The predicate fresh_list L n xs holds when xs is a list of
length n such that the elements are distinct from each other
and from the elements of L.
Fixpoint fresh_list
(L : t) (n : nat) (xs : list X.t) {struct xs} : Prop :=
match xs, n with
| nil, O ⇒
True
| cons x xs', S n' ⇒
notin x L ∧ fresh_list (union L (singleton x)) n' xs'
| _, _ ⇒
False
end.
End Sfun.
Module Make (X : OrderedType) <: Sfun X.
Include FSetList.Make X.
Definition disjoint E F := Equal (inter E F) empty.
Definition notin x L := ¬ In x L.
Fixpoint fresh_list
(L : t) (n : nat) (xs : list X.t) {struct xs} : Prop :=
match xs, n with
| nil, O ⇒
True
| cons x xs', S n' ⇒
notin x L ∧ fresh_list (union L (singleton x)) n' xs'
| _, _ ⇒
False
end.
End Make.