Coral.Metalib.FSetExtra
(* This file is distributed under the terms of the MIT License, also
known as the X11 Licence. A copy of this license is in the README
file that accompanied the original distribution of this file.
Based on code written by:
Brian Aydemir
Arthur Charg\'eraud *)
Require Import Coq.FSets.FSets.
Require Import Metalib.CoqFSetInterface.
(* *********************************************************************** *)
known as the X11 Licence. A copy of this license is in the README
file that accompanied the original distribution of this file.
Based on code written by:
Brian Aydemir
Arthur Charg\'eraud *)
Require Import Coq.FSets.FSets.
Require Import Metalib.CoqFSetInterface.
(* *********************************************************************** *)
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.