# 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