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 WSfun.
Module Make (X : DecidableType) <: WSfun X.
Include FSetWeakList.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.
This page has been generated by coqdoc