Library Coq.FSets.FSetWeakList
This file proposes an implementation of the non-dependant
interface FSetWeakInterface.S using lists without redundancy.
Functions over lists
First, we provide sets as lists which are (morally) without redundancy. The specs are proved under the additional condition of no redundancy. And the functions returning sets are proved to preserve this invariant.
Module Raw (X: DecidableType).
Definition elt := X.t.
Definition t := list elt.
Definition empty : t := nil.
Definition is_empty (l : t) : bool := if l then true else false.
Fixpoint mem (x : elt) (s : t) {struct s} : bool :=
match s with
| nil => false
| y :: l =>
if X.eq_dec x y then true else mem x l
end.
Fixpoint add (x : elt) (s : t) {struct s} : t :=
match s with
| nil => x :: nil
| y :: l =>
if X.eq_dec x y then s else y :: add x l
end.
Definition singleton (x : elt) : t := x :: nil.
Fixpoint remove (x : elt) (s : t) {struct s} : t :=
match s with
| nil => nil
| y :: l =>
if X.eq_dec x y then l else y :: remove x l
end.
Fixpoint fold (B : Type) (f : elt -> B -> B) (s : t) {struct s} :
B -> B := fun i => match s with
| nil => i
| x :: l => fold f l (f x i)
end.
Definition union (s : t) : t -> t := fold add s.
Definition diff (s s' : t) : t := fold remove s' s.
Definition inter (s s': t) : t :=
fold (fun x s => if mem x s' then add x s else s) s nil.
Definition subset (s s' : t) : bool := is_empty (diff s s').
Definition equal (s s' : t) : bool := andb (subset s s') (subset s' s).
Fixpoint filter (f : elt -> bool) (s : t) {struct s} : t :=
match s with
| nil => nil
| x :: l => if f x then x :: filter f l else filter f l
end.
Fixpoint for_all (f : elt -> bool) (s : t) {struct s} : bool :=
match s with
| nil => true
| x :: l => if f x then for_all f l else false
end.
Fixpoint exists_ (f : elt -> bool) (s : t) {struct s} : bool :=
match s with
| nil => false
| x :: l => if f x then true else exists_ f l
end.
Fixpoint partition (f : elt -> bool) (s : t) {struct s} :
t * t :=
match s with
| nil => (nil, nil)
| x :: l =>
let (s1, s2) := partition f l in
if f x then (x :: s1, s2) else (s1, x :: s2)
end.
Definition cardinal (s : t) : nat := length s.
Definition elements (s : t) : list elt := s.
Definition choose (s : t) : option elt :=
match s with
| nil => None
| x::_ => Some x
end.
Section ForNotations.
Notation NoDup := (NoDupA X.eq).
Notation In := (InA X.eq).
Definition Equal s s' := forall a : elt, In a s <-> In a s'.
Definition Subset s s' := forall a : elt, In a s -> In a s'.
Definition Empty s := forall a : elt, ~ In a s.
Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
Lemma In_eq :
forall (s : t) (x y : elt), X.eq x y -> In x s -> In y s.
Hint Immediate In_eq.
Lemma mem_1 :
forall (s : t)(x : elt), In x s -> mem x s = true.
Lemma mem_2 : forall (s : t) (x : elt), mem x s = true -> In x s.
Lemma add_1 :
forall (s : t) (Hs : NoDup s) (x y : elt), X.eq x y -> In y (add x s).
Lemma add_2 :
forall (s : t) (Hs : NoDup s) (x y : elt), In y s -> In y (add x s).
Lemma add_3 :
forall (s : t) (Hs : NoDup s) (x y : elt),
~ X.eq x y -> In y (add x s) -> In y s.
Lemma add_unique :
forall (s : t) (Hs : NoDup s)(x:elt), NoDup (add x s).
Lemma remove_1 :
forall (s : t) (Hs : NoDup s) (x y : elt), X.eq x y -> ~ In y (remove x s).
Lemma remove_2 :
forall (s : t) (Hs : NoDup s) (x y : elt),
~ X.eq x y -> In y s -> In y (remove x s).
Lemma remove_3 :
forall (s : t) (Hs : NoDup s) (x y : elt), In y (remove x s) -> In y s.
Lemma remove_unique :
forall (s : t) (Hs : NoDup s) (x : elt), NoDup (remove x s).
Lemma singleton_unique : forall x : elt, NoDup (singleton x).
Lemma singleton_1 : forall x y : elt, In y (singleton x) -> X.eq x y.
Lemma singleton_2 : forall x y : elt, X.eq x y -> In y (singleton x).
Lemma empty_unique : NoDup empty.
Lemma empty_1 : Empty empty.
Lemma is_empty_1 : forall s : t, Empty s -> is_empty s = true.
Lemma is_empty_2 : forall s : t, is_empty s = true -> Empty s.
Lemma elements_1 : forall (s : t) (x : elt), In x s -> In x (elements s).
Lemma elements_2 : forall (s : t) (x : elt), In x (elements s) -> In x s.
Lemma elements_3w : forall (s : t) (Hs : NoDup s), NoDup (elements s).
Lemma fold_1 :
forall (s : t) (Hs : NoDup s) (A : Type) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (fun a e => f e a) (elements s) i.
Lemma union_unique :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (union s s').
Lemma union_1 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x (union s s') -> In x s \/ In x s'.
Lemma union_0 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x s \/ In x s' -> In x (union s s').
Lemma union_2 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x s -> In x (union s s').
Lemma union_3 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x s' -> In x (union s s').
Lemma inter_unique :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (inter s s').
Lemma inter_0 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x (inter s s') -> In x s /\ In x s'.
Lemma inter_1 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x (inter s s') -> In x s.
Lemma inter_2 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x (inter s s') -> In x s'.
Lemma inter_3 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x s -> In x s' -> In x (inter s s').
Lemma diff_unique :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (diff s s').
Lemma diff_0 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x (diff s s') -> In x s /\ ~ In x s'.
Lemma diff_1 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x (diff s s') -> In x s.
Lemma diff_2 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x (diff s s') -> ~ In x s'.
Lemma diff_3 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x s -> ~ In x s' -> In x (diff s s').
Lemma subset_1 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'),
Subset s s' -> subset s s' = true.
Lemma subset_2 : forall (s s' : t)(Hs : NoDup s) (Hs' : NoDup s'),
subset s s' = true -> Subset s s'.
Lemma equal_1 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'),
Equal s s' -> equal s s' = true.
Lemma equal_2 : forall (s s' : t)(Hs : NoDup s) (Hs' : NoDup s'),
equal s s' = true -> Equal s s'.
Definition choose_1 :
forall (s : t) (x : elt), choose s = Some x -> In x s.
Definition choose_2 : forall s : t, choose s = None -> Empty s.
Lemma cardinal_1 :
forall (s : t) (Hs : NoDup s), cardinal s = length (elements s).
Lemma filter_1 :
forall (s : t) (x : elt) (f : elt -> bool),
In x (filter f s) -> In x s.
Lemma filter_2 :
forall (s : t) (x : elt) (f : elt -> bool),
compat_bool X.eq f -> In x (filter f s) -> f x = true.
Lemma filter_3 :
forall (s : t) (x : elt) (f : elt -> bool),
compat_bool X.eq f -> In x s -> f x = true -> In x (filter f s).
Lemma filter_unique :
forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (filter f s).
Lemma for_all_1 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f ->
For_all (fun x => f x = true) s -> for_all f s = true.
Lemma for_all_2 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f ->
for_all f s = true -> For_all (fun x => f x = true) s.
Lemma exists_1 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true.
Lemma exists_2 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s.
Lemma partition_1 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f -> Equal (fst (partition f s)) (filter f s).
Lemma partition_2 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f ->
Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
Lemma partition_aux_1 :
forall (s : t) (Hs : NoDup s) (f : elt -> bool)(x:elt),
In x (fst (partition f s)) -> In x s.
Lemma partition_aux_2 :
forall (s : t) (Hs : NoDup s) (f : elt -> bool)(x:elt),
In x (snd (partition f s)) -> In x s.
Lemma partition_unique_1 :
forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (fst (partition f s)).
Lemma partition_unique_2 :
forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (snd (partition f s)).
Definition eq : t -> t -> Prop := Equal.
Lemma eq_refl : forall s, eq s s.
Lemma eq_sym : forall s s', eq s s' -> eq s' s.
Lemma eq_trans :
forall s s' s'', eq s s' -> eq s' s'' -> eq s s''.
Definition eq_dec : forall (s s':t)(Hs:NoDup s)(Hs':NoDup s'),
{ eq s s' }+{ ~eq s s' }.
End ForNotations.
End Raw.
Notation NoDup := (NoDupA X.eq).
Notation In := (InA X.eq).
Definition Equal s s' := forall a : elt, In a s <-> In a s'.
Definition Subset s s' := forall a : elt, In a s -> In a s'.
Definition Empty s := forall a : elt, ~ In a s.
Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
Lemma In_eq :
forall (s : t) (x y : elt), X.eq x y -> In x s -> In y s.
Hint Immediate In_eq.
Lemma mem_1 :
forall (s : t)(x : elt), In x s -> mem x s = true.
Lemma mem_2 : forall (s : t) (x : elt), mem x s = true -> In x s.
Lemma add_1 :
forall (s : t) (Hs : NoDup s) (x y : elt), X.eq x y -> In y (add x s).
Lemma add_2 :
forall (s : t) (Hs : NoDup s) (x y : elt), In y s -> In y (add x s).
Lemma add_3 :
forall (s : t) (Hs : NoDup s) (x y : elt),
~ X.eq x y -> In y (add x s) -> In y s.
Lemma add_unique :
forall (s : t) (Hs : NoDup s)(x:elt), NoDup (add x s).
Lemma remove_1 :
forall (s : t) (Hs : NoDup s) (x y : elt), X.eq x y -> ~ In y (remove x s).
Lemma remove_2 :
forall (s : t) (Hs : NoDup s) (x y : elt),
~ X.eq x y -> In y s -> In y (remove x s).
Lemma remove_3 :
forall (s : t) (Hs : NoDup s) (x y : elt), In y (remove x s) -> In y s.
Lemma remove_unique :
forall (s : t) (Hs : NoDup s) (x : elt), NoDup (remove x s).
Lemma singleton_unique : forall x : elt, NoDup (singleton x).
Lemma singleton_1 : forall x y : elt, In y (singleton x) -> X.eq x y.
Lemma singleton_2 : forall x y : elt, X.eq x y -> In y (singleton x).
Lemma empty_unique : NoDup empty.
Lemma empty_1 : Empty empty.
Lemma is_empty_1 : forall s : t, Empty s -> is_empty s = true.
Lemma is_empty_2 : forall s : t, is_empty s = true -> Empty s.
Lemma elements_1 : forall (s : t) (x : elt), In x s -> In x (elements s).
Lemma elements_2 : forall (s : t) (x : elt), In x (elements s) -> In x s.
Lemma elements_3w : forall (s : t) (Hs : NoDup s), NoDup (elements s).
Lemma fold_1 :
forall (s : t) (Hs : NoDup s) (A : Type) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (fun a e => f e a) (elements s) i.
Lemma union_unique :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (union s s').
Lemma union_1 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x (union s s') -> In x s \/ In x s'.
Lemma union_0 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x s \/ In x s' -> In x (union s s').
Lemma union_2 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x s -> In x (union s s').
Lemma union_3 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x s' -> In x (union s s').
Lemma inter_unique :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (inter s s').
Lemma inter_0 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x (inter s s') -> In x s /\ In x s'.
Lemma inter_1 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x (inter s s') -> In x s.
Lemma inter_2 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x (inter s s') -> In x s'.
Lemma inter_3 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x s -> In x s' -> In x (inter s s').
Lemma diff_unique :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (diff s s').
Lemma diff_0 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x (diff s s') -> In x s /\ ~ In x s'.
Lemma diff_1 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x (diff s s') -> In x s.
Lemma diff_2 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x (diff s s') -> ~ In x s'.
Lemma diff_3 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
In x s -> ~ In x s' -> In x (diff s s').
Lemma subset_1 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'),
Subset s s' -> subset s s' = true.
Lemma subset_2 : forall (s s' : t)(Hs : NoDup s) (Hs' : NoDup s'),
subset s s' = true -> Subset s s'.
Lemma equal_1 :
forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'),
Equal s s' -> equal s s' = true.
Lemma equal_2 : forall (s s' : t)(Hs : NoDup s) (Hs' : NoDup s'),
equal s s' = true -> Equal s s'.
Definition choose_1 :
forall (s : t) (x : elt), choose s = Some x -> In x s.
Definition choose_2 : forall s : t, choose s = None -> Empty s.
Lemma cardinal_1 :
forall (s : t) (Hs : NoDup s), cardinal s = length (elements s).
Lemma filter_1 :
forall (s : t) (x : elt) (f : elt -> bool),
In x (filter f s) -> In x s.
Lemma filter_2 :
forall (s : t) (x : elt) (f : elt -> bool),
compat_bool X.eq f -> In x (filter f s) -> f x = true.
Lemma filter_3 :
forall (s : t) (x : elt) (f : elt -> bool),
compat_bool X.eq f -> In x s -> f x = true -> In x (filter f s).
Lemma filter_unique :
forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (filter f s).
Lemma for_all_1 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f ->
For_all (fun x => f x = true) s -> for_all f s = true.
Lemma for_all_2 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f ->
for_all f s = true -> For_all (fun x => f x = true) s.
Lemma exists_1 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true.
Lemma exists_2 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s.
Lemma partition_1 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f -> Equal (fst (partition f s)) (filter f s).
Lemma partition_2 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f ->
Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
Lemma partition_aux_1 :
forall (s : t) (Hs : NoDup s) (f : elt -> bool)(x:elt),
In x (fst (partition f s)) -> In x s.
Lemma partition_aux_2 :
forall (s : t) (Hs : NoDup s) (f : elt -> bool)(x:elt),
In x (snd (partition f s)) -> In x s.
Lemma partition_unique_1 :
forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (fst (partition f s)).
Lemma partition_unique_2 :
forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (snd (partition f s)).
Definition eq : t -> t -> Prop := Equal.
Lemma eq_refl : forall s, eq s s.
Lemma eq_sym : forall s s', eq s s' -> eq s' s.
Lemma eq_trans :
forall s s' s'', eq s s' -> eq s' s'' -> eq s s''.
Definition eq_dec : forall (s s':t)(Hs:NoDup s)(Hs':NoDup s'),
{ eq s s' }+{ ~eq s s' }.
End ForNotations.
End Raw.
Encapsulation
Now, in order to really provide a functor implementing S, we need to encapsulate everything into a type of lists without redundancy.
Module Make (X: DecidableType) <: WS with Module E := X.
Module Raw := Raw X.
Module E := X.
Record slist := {this :> Raw.t; unique : NoDupA E.eq this}.
Definition t := slist.
Definition elt := E.t.
Definition In (x : elt) (s : t) : Prop := InA E.eq x s.(this).
Definition Equal (s s':t) : Prop := forall a : elt, In a s <-> In a s'.
Definition Subset (s s':t) : Prop := forall a : elt, In a s -> In a s'.
Definition Empty (s:t) : Prop := forall a : elt, ~ In a s.
Definition For_all (P : elt -> Prop) (s : t) : Prop :=
forall x : elt, In x s -> P x.
Definition Exists (P : elt -> Prop) (s : t) : Prop := exists x : elt, In x s /\ P x.
Definition mem (x : elt) (s : t) : bool := Raw.mem x s.
Definition add (x : elt)(s : t) : t := Build_slist (Raw.add_unique (unique s) x).
Definition remove (x : elt)(s : t) : t := Build_slist (Raw.remove_unique (unique s) x).
Definition singleton (x : elt) : t := Build_slist (Raw.singleton_unique x).
Definition union (s s' : t) : t :=
Build_slist (Raw.union_unique (unique s) (unique s')).
Definition inter (s s' : t) : t :=
Build_slist (Raw.inter_unique (unique s) (unique s')).
Definition diff (s s' : t) : t :=
Build_slist (Raw.diff_unique (unique s) (unique s')).
Definition equal (s s' : t) : bool := Raw.equal s s'.
Definition subset (s s' : t) : bool := Raw.subset s s'.
Definition empty : t := Build_slist Raw.empty_unique.
Definition is_empty (s : t) : bool := Raw.is_empty s.
Definition elements (s : t) : list elt := Raw.elements s.
Definition choose (s:t) : option elt := Raw.choose s.
Definition fold (B : Type) (f : elt -> B -> B) (s : t) : B -> B := Raw.fold (B:=B) f s.
Definition cardinal (s : t) : nat := Raw.cardinal s.
Definition filter (f : elt -> bool) (s : t) : t :=
Build_slist (Raw.filter_unique (unique s) f).
Definition for_all (f : elt -> bool) (s : t) : bool := Raw.for_all f s.
Definition exists_ (f : elt -> bool) (s : t) : bool := Raw.exists_ f s.
Definition partition (f : elt -> bool) (s : t) : t * t :=
let p := Raw.partition f s in
(Build_slist (this:=fst p) (Raw.partition_unique_1 (unique s) f),
Build_slist (this:=snd p) (Raw.partition_unique_2 (unique s) f)).
Section Spec.
Variable s s' : t.
Variable x y : elt.
Lemma In_1 : E.eq x y -> In x s -> In y s.
Lemma mem_1 : In x s -> mem x s = true.
Lemma mem_2 : mem x s = true -> In x s.
Lemma equal_1 : Equal s s' -> equal s s' = true.
Lemma equal_2 : equal s s' = true -> Equal s s'.
Lemma subset_1 : Subset s s' -> subset s s' = true.
Lemma subset_2 : subset s s' = true -> Subset s s'.
Lemma empty_1 : Empty empty.
Lemma is_empty_1 : Empty s -> is_empty s = true.
Lemma is_empty_2 : is_empty s = true -> Empty s.
Lemma add_1 : E.eq x y -> In y (add x s).
Lemma add_2 : In y s -> In y (add x s).
Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s.
Lemma remove_1 : E.eq x y -> ~ In y (remove x s).
Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
Lemma remove_3 : In y (remove x s) -> In y s.
Lemma singleton_1 : In y (singleton x) -> E.eq x y.
Lemma singleton_2 : E.eq x y -> In y (singleton x).
Lemma union_1 : In x (union s s') -> In x s \/ In x s'.
Lemma union_2 : In x s -> In x (union s s').
Lemma union_3 : In x s' -> In x (union s s').
Lemma inter_1 : In x (inter s s') -> In x s.
Lemma inter_2 : In x (inter s s') -> In x s'.
Lemma inter_3 : In x s -> In x s' -> In x (inter s s').
Lemma diff_1 : In x (diff s s') -> In x s.
Lemma diff_2 : In x (diff s s') -> ~ In x s'.
Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').
Lemma fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (fun a e => f e a) (elements s) i.
Lemma cardinal_1 : cardinal s = length (elements s).
Section Filter.
Variable f : elt -> bool.
Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s.
Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true.
Lemma filter_3 :
compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
Lemma for_all_1 :
compat_bool E.eq f ->
For_all (fun x => f x = true) s -> for_all f s = true.
Lemma for_all_2 :
compat_bool E.eq f ->
for_all f s = true -> For_all (fun x => f x = true) s.
Lemma exists_1 :
compat_bool E.eq f ->
Exists (fun x => f x = true) s -> exists_ f s = true.
Lemma exists_2 :
compat_bool E.eq f ->
exists_ f s = true -> Exists (fun x => f x = true) s.
Lemma partition_1 :
compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s).
Lemma partition_2 :
compat_bool E.eq f ->
Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
End Filter.
Lemma elements_1 : In x s -> InA E.eq x (elements s).
Lemma elements_2 : InA E.eq x (elements s) -> In x s.
Lemma elements_3w : NoDupA E.eq (elements s).
Lemma choose_1 : choose s = Some x -> In x s.
Lemma choose_2 : choose s = None -> Empty s.
End Spec.
Definition eq : t -> t -> Prop := Equal.
Lemma eq_refl : forall s, eq s s.
Lemma eq_sym : forall s s', eq s s' -> eq s' s.
Lemma eq_trans :
forall s s' s'', eq s s' -> eq s' s'' -> eq s s''.
Definition eq_dec : forall (s s':t),
{ eq s s' }+{ ~eq s s' }.
End Make.