Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Finite sets library

This functor derives additional facts from MSetInterface.S. These facts are mainly the specifications of MSetInterface.S written using different styles: equivalence and boolean equalities. Moreover, we prove that E.Eq and Equal are setoid equalities.

Require Import DecidableTypeEx.
Require Export MSetInterface.
Set Implicit Arguments.
Unset Strict Implicit.

First, a functor for Weak Sets in functorial version.

Module WFactsOn (Import E : DecidableType)(Import M : WSetsOn E).

Notation eq_dec := E.eq_dec.
Definition eqb x y := if eq_dec x y then true else false.

Specifications written using implications :

this used to be the default interface.

Section ImplSpec.
Variable s s' : t.
Variable x y : elt.

Lemma In_1 : E.eq x y -> In x s -> In y s.s, s':t
x, y:elt
E.eq x y -> In x s -> In y s
Proof.s, s':t
x, y:elt
E.eq x y -> In x s -> In y s intros E; rewrite E; auto. Qed.

Lemma mem_1 : In x s -> mem x s = true.s, s':t
x, y:elt
In x s -> mem x s = true
Proof.s, s':t
x, y:elt
In x s -> mem x s = true intros; apply <- mem_spec; auto. Qed.
Lemma mem_2 : mem x s = true -> In x s.s, s':t
x, y:elt
mem x s = true -> In x s
Proof.s, s':t
x, y:elt
mem x s = true -> In x s intros; apply -> mem_spec; auto. Qed.

Lemma equal_1 : Equal s s' -> equal s s' = true.s, s':t
x, y:elt
s [=] s' -> equal s s' = true
Proof.s, s':t
x, y:elt
s [=] s' -> equal s s' = true intros; apply <- equal_spec; auto. Qed.
Lemma equal_2 : equal s s' = true -> Equal s s'.s, s':t
x, y:elt
equal s s' = true -> s [=] s'
Proof.s, s':t
x, y:elt
equal s s' = true -> s [=] s' intros; apply -> equal_spec; auto. Qed.

Lemma subset_1 : Subset s s' -> subset s s' = true.s, s':t
x, y:elt
s [<=] s' -> subset s s' = true
Proof.s, s':t
x, y:elt
s [<=] s' -> subset s s' = true intros; apply <- subset_spec; auto. Qed.
Lemma subset_2 : subset s s' = true -> Subset s s'.s, s':t
x, y:elt
subset s s' = true -> s [<=] s'
Proof.s, s':t
x, y:elt
subset s s' = true -> s [<=] s' intros; apply -> subset_spec; auto. Qed.

Lemma is_empty_1 : Empty s -> is_empty s = true.s, s':t
x, y:elt
Empty s -> is_empty s = true
Proof.s, s':t
x, y:elt
Empty s -> is_empty s = true intros; apply <- is_empty_spec; auto. Qed.
Lemma is_empty_2 : is_empty s = true -> Empty s.s, s':t
x, y:elt
is_empty s = true -> Empty s
Proof.s, s':t
x, y:elt
is_empty s = true -> Empty s intros; apply -> is_empty_spec; auto. Qed.

Lemma add_1 : E.eq x y -> In y (add x s).s, s':t
x, y:elt
E.eq x y -> In y (add x s)
Proof.s, s':t
x, y:elt
E.eq x y -> In y (add x s) intros; apply <- add_spec.s, s':t
x, y:elt
H:E.eq x y
E.eq y x \/ In y s auto with relations. Qed.
Lemma add_2 : In y s -> In y (add x s).s, s':t
x, y:elt
In y s -> In y (add x s)
Proof.s, s':t
x, y:elt
In y s -> In y (add x s) intros; apply <- add_spec; auto. Qed.
Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s.s, s':t
x, y:elt
~ E.eq x y -> In y (add x s) -> In y s
Proof.s, s':t
x, y:elt
~ E.eq x y -> In y (add x s) -> In y s rewrite add_spec.s, s':t
x, y:elt
~ E.eq x y -> E.eq y x \/ In y s -> In y s intros H [H'|H']; auto.s, s':t
x, y:elt
H:~ E.eq x y
H':E.eq y x
In y s elim H; auto with relations. Qed.

Lemma remove_1 : E.eq x y -> ~ In y (remove x s).s, s':t
x, y:elt
E.eq x y -> ~ In y (remove x s)
Proof.s, s':t
x, y:elt
E.eq x y -> ~ In y (remove x s) intros; rewrite remove_spec; intuition. Qed.
Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).s, s':t
x, y:elt
~ E.eq x y -> In y s -> In y (remove x s)
Proof.s, s':t
x, y:elt
~ E.eq x y -> In y s -> In y (remove x s) intros; apply <- remove_spec; auto with relations. Qed.
Lemma remove_3 : In y (remove x s) -> In y s.s, s':t
x, y:elt
In y (remove x s) -> In y s
Proof.s, s':t
x, y:elt
In y (remove x s) -> In y s rewrite remove_spec; intuition. Qed.

Lemma singleton_1 : In y (singleton x) -> E.eq x y.s, s':t
x, y:elt
In y (singleton x) -> E.eq x y
Proof.s, s':t
x, y:elt
In y (singleton x) -> E.eq x y rewrite singleton_spec; auto with relations. Qed.
Lemma singleton_2 : E.eq x y -> In y (singleton x).s, s':t
x, y:elt
E.eq x y -> In y (singleton x)
Proof.s, s':t
x, y:elt
E.eq x y -> In y (singleton x) rewrite singleton_spec; auto with relations. Qed.

Lemma union_1 : In x (union s s') -> In x s \/ In x s'.s, s':t
x, y:elt
In x (union s s') -> In x s \/ In x s'
Proof.s, s':t
x, y:elt
In x (union s s') -> In x s \/ In x s' rewrite union_spec; auto. Qed.
Lemma union_2 : In x s -> In x (union s s').s, s':t
x, y:elt
In x s -> In x (union s s')
Proof.s, s':t
x, y:elt
In x s -> In x (union s s') rewrite union_spec; auto. Qed.
Lemma union_3 : In x s' -> In x (union s s').s, s':t
x, y:elt
In x s' -> In x (union s s')
Proof.s, s':t
x, y:elt
In x s' -> In x (union s s') rewrite union_spec; auto. Qed.

Lemma inter_1 : In x (inter s s') -> In x s.s, s':t
x, y:elt
In x (inter s s') -> In x s
Proof.s, s':t
x, y:elt
In x (inter s s') -> In x s rewrite inter_spec; intuition. Qed.
Lemma inter_2 : In x (inter s s') -> In x s'.s, s':t
x, y:elt
In x (inter s s') -> In x s'
Proof.s, s':t
x, y:elt
In x (inter s s') -> In x s' rewrite inter_spec; intuition. Qed.
Lemma inter_3 : In x s -> In x s' -> In x (inter s s').s, s':t
x, y:elt
In x s -> In x s' -> In x (inter s s')
Proof.s, s':t
x, y:elt
In x s -> In x s' -> In x (inter s s') rewrite inter_spec; intuition. Qed.

Lemma diff_1 : In x (diff s s') -> In x s.s, s':t
x, y:elt
In x (diff s s') -> In x s
Proof.s, s':t
x, y:elt
In x (diff s s') -> In x s rewrite diff_spec; intuition. Qed.
Lemma diff_2 : In x (diff s s') -> ~ In x s'.s, s':t
x, y:elt
In x (diff s s') -> ~ In x s'
Proof.s, s':t
x, y:elt
In x (diff s s') -> ~ In x s' rewrite diff_spec; intuition. Qed.
Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').s, s':t
x, y:elt
In x s -> ~ In x s' -> In x (diff s s')
Proof.s, s':t
x, y:elt
In x s -> ~ In x s' -> In x (diff s s') rewrite diff_spec; auto. Qed.

Variable f : elt -> bool.
Notation compatb := (Proper (E.eq==>Logic.eq)) (only parsing).

Lemma filter_1 : compatb f -> In x (filter f s) -> In x s.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
In x (filter f s) -> In x s
Proof.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
In x (filter f s) -> In x s intros P; rewrite filter_spec; intuition. Qed.
Lemma filter_2 : compatb f -> In x (filter f s) -> f x = true.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
In x (filter f s) -> f x = true
Proof.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
In x (filter f s) -> f x = true intros P; rewrite filter_spec; intuition. Qed.
Lemma filter_3 : compatb f -> In x s -> f x = true -> In x (filter f s).s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
In x s -> f x = true -> In x (filter f s)
Proof.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
In x s -> f x = true -> In x (filter f s) intros P; rewrite filter_spec; intuition. Qed.

Lemma for_all_1 : compatb f ->
      For_all (fun x => f x = true) s -> for_all f s = true.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
For_all (fun x0 : elt => f x0 = true) s ->
for_all f s = true
Proof.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
For_all (fun x0 : elt => f x0 = true) s ->
for_all f s = true intros; apply <- for_all_spec; auto. Qed.
Lemma for_all_2 : compatb f ->
      for_all f s = true -> For_all (fun x => f x = true) s.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
for_all f s = true ->
For_all (fun x0 : elt => f x0 = true) s
Proof.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
for_all f s = true ->
For_all (fun x0 : elt => f x0 = true) s intros; apply -> for_all_spec; auto. Qed.

Lemma exists_1 : compatb f ->
      Exists (fun x => f x = true) s -> exists_ f s = true.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
Exists (fun x0 : elt => f x0 = true) s ->
exists_ f s = true
Proof.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
Exists (fun x0 : elt => f x0 = true) s ->
exists_ f s = true intros; apply <- exists_spec; auto. Qed.

Lemma exists_2 : compatb f ->
      exists_ f s = true -> Exists (fun x => f x = true) s.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
exists_ f s = true ->
Exists (fun x0 : elt => f x0 = true) s
Proof.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
exists_ f s = true ->
Exists (fun x0 : elt => f x0 = true) s intros; apply -> exists_spec; auto. Qed.

Lemma elements_1 : In x s -> InA E.eq x (elements s).s, s':t
x, y:elt
f:elt -> bool
In x s -> InA E.eq x (elements s)
Proof.s, s':t
x, y:elt
f:elt -> bool
In x s -> InA E.eq x (elements s) intros; apply <- elements_spec1; auto. Qed.
Lemma elements_2 : InA E.eq x (elements s) -> In x s.s, s':t
x, y:elt
f:elt -> bool
InA E.eq x (elements s) -> In x s
Proof.s, s':t
x, y:elt
f:elt -> bool
InA E.eq x (elements s) -> In x s intros; apply -> elements_spec1; auto. Qed.

End ImplSpec.

Notation empty_1 := empty_spec (only parsing).
Notation fold_1 := fold_spec (only parsing).
Notation cardinal_1 := cardinal_spec (only parsing).
Notation partition_1 := partition_spec1 (only parsing).
Notation partition_2 := partition_spec2 (only parsing).
Notation choose_1 := choose_spec1 (only parsing).
Notation choose_2 := choose_spec2 (only parsing).
Notation elements_3w := elements_spec2w (only parsing).

Hint Resolve mem_1 equal_1 subset_1 empty_1
    is_empty_1 choose_1 choose_2 add_1 add_2 remove_1
    remove_2 singleton_2 union_1 union_2 union_3
    inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1
    partition_1 partition_2 elements_1 elements_3w
    : set.
Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3
    remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
    filter_1 filter_2 for_all_2 exists_2 elements_2
    : set.

Specifications written using equivalences :

this is now provided by the default interface.

Section IffSpec.
Variable s s' s'' : t.
Variable x y z : elt.

Lemma In_eq_iff : E.eq x y -> (In x s <-> In y s).s, s', s'':t
x, y, z:elt
E.eq x y -> In x s <-> In y s
Proof.s, s', s'':t
x, y, z:elt
E.eq x y -> In x s <-> In y s
intros E; rewrite E; intuition.
Qed.

Lemma mem_iff : In x s <-> mem x s = true.s, s', s'':t
x, y, z:elt
In x s <-> mem x s = true
Proof.s, s', s'':t
x, y, z:elt
In x s <-> mem x s = true apply iff_sym, mem_spec. Qed.

Lemma not_mem_iff : ~In x s <-> mem x s = false.s, s', s'':t
x, y, z:elt
~ In x s <-> mem x s = false
Proof.s, s', s'':t
x, y, z:elt
~ In x s <-> mem x s = false
rewrite <-mem_spec; destruct (mem x s); intuition.
Qed.

Lemma equal_iff : s[=]s' <-> equal s s' = true.s, s', s'':t
x, y, z:elt
s [=] s' <-> equal s s' = true
Proof.s, s', s'':t
x, y, z:elt
s [=] s' <-> equal s s' = true apply iff_sym, equal_spec. Qed.

Lemma subset_iff : s[<=]s' <-> subset s s' = true.s, s', s'':t
x, y, z:elt
s [<=] s' <-> subset s s' = true
Proof.s, s', s'':t
x, y, z:elt
s [<=] s' <-> subset s s' = true apply iff_sym, subset_spec. Qed.

Lemma empty_iff : In x empty <-> False.s, s', s'':t
x, y, z:elt
In x empty <-> False
Proof.s, s', s'':t
x, y, z:elt
In x empty <-> False intuition; apply (empty_spec H). Qed.

Lemma is_empty_iff : Empty s <-> is_empty s = true.s, s', s'':t
x, y, z:elt
Empty s <-> is_empty s = true
Proof.s, s', s'':t
x, y, z:elt
Empty s <-> is_empty s = true apply iff_sym, is_empty_spec. Qed.

Lemma singleton_iff : In y (singleton x) <-> E.eq x y.s, s', s'':t
x, y, z:elt
In y (singleton x) <-> E.eq x y
Proof.s, s', s'':t
x, y, z:elt
In y (singleton x) <-> E.eq x y rewrite singleton_spec; intuition. Qed.

Lemma add_iff : In y (add x s) <-> E.eq x y \/ In y s.s, s', s'':t
x, y, z:elt
In y (add x s) <-> E.eq x y \/ In y s
Proof.s, s', s'':t
x, y, z:elt
In y (add x s) <-> E.eq x y \/ In y s rewrite add_spec; intuition. Qed.

Lemma add_neq_iff : ~ E.eq x y -> (In y (add x s)  <-> In y s).s, s', s'':t
x, y, z:elt
~ E.eq x y -> In y (add x s) <-> In y s
Proof.s, s', s'':t
x, y, z:elt
~ E.eq x y -> In y (add x s) <-> In y s rewrite add_spec; intuition.s, s', s'':t
x, y, z:elt
H:E.eq x y -> False
H1:E.eq y x
In y s elim H; auto with relations. Qed.

Lemma remove_iff : In y (remove x s) <-> In y s /\ ~E.eq x y.s, s', s'':t
x, y, z:elt
In y (remove x s) <-> In y s /\ ~ E.eq x y
Proof.s, s', s'':t
x, y, z:elt
In y (remove x s) <-> In y s /\ ~ E.eq x y rewrite remove_spec; intuition. Qed.

Lemma remove_neq_iff : ~ E.eq x y -> (In y (remove x s) <-> In y s).s, s', s'':t
x, y, z:elt
~ E.eq x y -> In y (remove x s) <-> In y s
Proof.s, s', s'':t
x, y, z:elt
~ E.eq x y -> In y (remove x s) <-> In y s rewrite remove_spec; intuition. Qed.

Variable f : elt -> bool.

Lemma for_all_iff : Proper (E.eq==>Logic.eq) f ->
  (For_all (fun x => f x = true) s <-> for_all f s = true).s, s', s'':t
x, y, z:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
For_all (fun x0 : elt => f x0 = true) s <->
for_all f s = true
Proof.s, s', s'':t
x, y, z:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
For_all (fun x0 : elt => f x0 = true) s <->
for_all f s = true intros; apply iff_sym, for_all_spec; auto. Qed.

Lemma exists_iff : Proper (E.eq==>Logic.eq) f ->
  (Exists (fun x => f x = true) s <-> exists_ f s = true).s, s', s'':t
x, y, z:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
Exists (fun x0 : elt => f x0 = true) s <->
exists_ f s = true
Proof.s, s', s'':t
x, y, z:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
Exists (fun x0 : elt => f x0 = true) s <->
exists_ f s = true intros; apply iff_sym, exists_spec; auto. Qed.

Lemma elements_iff : In x s <-> InA E.eq x (elements s).s, s', s'':t
x, y, z:elt
f:elt -> bool
In x s <-> InA E.eq x (elements s)
Proof.s, s', s'':t
x, y, z:elt
f:elt -> bool
In x s <-> InA E.eq x (elements s) apply iff_sym, elements_spec1. Qed.

End IffSpec.

Notation union_iff := union_spec (only parsing).
Notation inter_iff := inter_spec (only parsing).
Notation diff_iff := diff_spec (only parsing).
Notation filter_iff := filter_spec (only parsing).

Useful tactic for simplifying expressions like In y (add x (union s s'))

Ltac set_iff :=
 repeat (progress (
  rewrite add_iff || rewrite remove_iff || rewrite singleton_iff
  || rewrite union_iff || rewrite inter_iff || rewrite diff_iff
  || rewrite empty_iff)).

Specifications written using boolean predicates

Section BoolSpec.
Variable s s' s'' : t.
Variable x y z : elt.

Lemma mem_b : E.eq x y -> mem x s = mem y s.s, s', s'':t
x, y, z:elt
E.eq x y -> mem x s = mem y s
Proof.s, s', s'':t
x, y, z:elt
E.eq x y -> mem x s = mem y s
intros.s, s', s'':t
x, y, z:elt
H:E.eq x y
mem x s = mem y s
generalize (mem_iff s x) (mem_iff s y)(In_eq_iff s H).s, s', s'':t
x, y, z:elt
H:E.eq x y
In x s <-> mem x s = true ->
In y s <-> mem y s = true ->
In x s <-> In y s -> mem x s = mem y s
destruct (mem x s); destruct (mem y s); intuition.
Qed.

Lemma empty_b : mem y empty = false.s, s', s'':t
x, y, z:elt
mem y empty = false
Proof.s, s', s'':t
x, y, z:elt
mem y empty = false
generalize (empty_iff y)(mem_iff empty y).s, s', s'':t
x, y, z:elt
In y empty <-> False ->
In y empty <-> mem y empty = true ->
mem y empty = false
destruct (mem y empty); intuition.
Qed.

Lemma add_b : mem y (add x s) = eqb x y || mem y s.s, s', s'':t
x, y, z:elt
mem y (add x s) = eqb x y || mem y s
Proof.s, s', s'':t
x, y, z:elt
mem y (add x s) = eqb x y || mem y s
generalize (mem_iff (add x s) y)(mem_iff s y)(add_iff s x y); unfold eqb.s, s', s'':t
x, y, z:elt
In y (add x s) <-> mem y (add x s) = true ->
In y s <-> mem y s = true ->
In y (add x s) <-> E.eq x y \/ In y s ->
mem y (add x s) =
(if eq_dec x y then true else false) || mem y s
destruct (eq_dec x y); destruct (mem y s); destruct (mem y (add x s)); intuition.
Qed.

Lemma add_neq_b : ~ E.eq x y -> mem y (add x s) = mem y s.s, s', s'':t
x, y, z:elt
~ E.eq x y -> mem y (add x s) = mem y s
Proof.s, s', s'':t
x, y, z:elt
~ E.eq x y -> mem y (add x s) = mem y s
intros; generalize (mem_iff (add x s) y)(mem_iff s y)(add_neq_iff s H).s, s', s'':t
x, y, z:elt
H:~ E.eq x y
In y (add x s) <-> mem y (add x s) = true ->
In y s <-> mem y s = true ->
In y (add x s) <-> In y s -> mem y (add x s) = mem y s
destruct (mem y s); destruct (mem y (add x s)); intuition.
Qed.

Lemma remove_b : mem y (remove x s) = mem y s && negb (eqb x y).s, s', s'':t
x, y, z:elt
mem y (remove x s) = mem y s && negb (eqb x y)
Proof.s, s', s'':t
x, y, z:elt
mem y (remove x s) = mem y s && negb (eqb x y)
generalize (mem_iff (remove x s) y)(mem_iff s y)(remove_iff s x y); unfold eqb.s, s', s'':t
x, y, z:elt
In y (remove x s) <-> mem y (remove x s) = true ->
In y s <-> mem y s = true ->
In y (remove x s) <-> In y s /\ ~ E.eq x y ->
mem y (remove x s) =
mem y s && negb (if eq_dec x y then true else false)
destruct (eq_dec x y); destruct (mem y s); destruct (mem y (remove x s)); simpl; intuition.
Qed.

Lemma remove_neq_b : ~ E.eq x y -> mem y (remove x s) = mem y s.s, s', s'':t
x, y, z:elt
~ E.eq x y -> mem y (remove x s) = mem y s
Proof.s, s', s'':t
x, y, z:elt
~ E.eq x y -> mem y (remove x s) = mem y s
intros; generalize (mem_iff (remove x s) y)(mem_iff s y)(remove_neq_iff s H).s, s', s'':t
x, y, z:elt
H:~ E.eq x y
In y (remove x s) <-> mem y (remove x s) = true ->
In y s <-> mem y s = true ->
In y (remove x s) <-> In y s ->
mem y (remove x s) = mem y s
destruct (mem y s); destruct (mem y (remove x s)); intuition.
Qed.

Lemma singleton_b : mem y (singleton x) = eqb x y.s, s', s'':t
x, y, z:elt
mem y (singleton x) = eqb x y
Proof.s, s', s'':t
x, y, z:elt
mem y (singleton x) = eqb x y
generalize (mem_iff (singleton x) y)(singleton_iff x y); unfold eqb.s, s', s'':t
x, y, z:elt
In y (singleton x) <-> mem y (singleton x) = true ->
In y (singleton x) <-> E.eq x y ->
mem y (singleton x) =
(if eq_dec x y then true else false)
destruct (eq_dec x y); destruct (mem y (singleton x)); intuition.
Qed.

Lemma union_b : mem x (union s s') = mem x s || mem x s'.s, s', s'':t
x, y, z:elt
mem x (union s s') = mem x s || mem x s'
Proof.s, s', s'':t
x, y, z:elt
mem x (union s s') = mem x s || mem x s'
generalize (mem_iff (union s s') x)(mem_iff s x)(mem_iff s' x)(union_iff s s' x).s, s', s'':t
x, y, z:elt
In x (union s s') <-> mem x (union s s') = true ->
In x s <-> mem x s = true ->
In x s' <-> mem x s' = true ->
In x (union s s') <-> In x s \/ In x s' ->
mem x (union s s') = mem x s || mem x s'
destruct (mem x s); destruct (mem x s'); destruct (mem x (union s s')); intuition.
Qed.

Lemma inter_b : mem x (inter s s') = mem x s && mem x s'.s, s', s'':t
x, y, z:elt
mem x (inter s s') = mem x s && mem x s'
Proof.s, s', s'':t
x, y, z:elt
mem x (inter s s') = mem x s && mem x s'
generalize (mem_iff (inter s s') x)(mem_iff s x)(mem_iff s' x)(inter_iff s s' x).s, s', s'':t
x, y, z:elt
In x (inter s s') <-> mem x (inter s s') = true ->
In x s <-> mem x s = true ->
In x s' <-> mem x s' = true ->
In x (inter s s') <-> In x s /\ In x s' ->
mem x (inter s s') = mem x s && mem x s'
destruct (mem x s); destruct (mem x s'); destruct (mem x (inter s s')); intuition.
Qed.

Lemma diff_b : mem x (diff s s') = mem x s && negb (mem x s').s, s', s'':t
x, y, z:elt
mem x (diff s s') = mem x s && negb (mem x s')
Proof.s, s', s'':t
x, y, z:elt
mem x (diff s s') = mem x s && negb (mem x s')
generalize (mem_iff (diff s s') x)(mem_iff s x)(mem_iff s' x)(diff_iff s s' x).s, s', s'':t
x, y, z:elt
In x (diff s s') <-> mem x (diff s s') = true ->
In x s <-> mem x s = true ->
In x s' <-> mem x s' = true ->
In x (diff s s') <-> In x s /\ ~ In x s' ->
mem x (diff s s') = mem x s && negb (mem x s')
destruct (mem x s); destruct (mem x s'); destruct (mem x (diff s s')); simpl; intuition.
Qed.

Lemma elements_b : mem x s = existsb (eqb x) (elements s).s, s', s'':t
x, y, z:elt
mem x s = existsb (eqb x) (elements s)
Proof.s, s', s'':t
x, y, z:elt
mem x s = existsb (eqb x) (elements s)
generalize (mem_iff s x)(elements_iff s x)(existsb_exists (eqb x) (elements s)).s, s', s'':t
x, y, z:elt
In x s <-> mem x s = true ->
In x s <-> InA E.eq x (elements s) ->
existsb (eqb x) (elements s) = true <->
(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true) ->
mem x s = existsb (eqb x) (elements s)
rewrite InA_alt.s, s', s'':t
x, y, z:elt
In x s <-> mem x s = true ->
In x s <->
(exists y0 : E.t, E.eq x y0 /\ List.In y0 (elements s)) ->
existsb (eqb x) (elements s) = true <->
(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true) ->
mem x s = existsb (eqb x) (elements s)
destruct (mem x s); destruct (existsb (eqb x) (elements s)); auto; intros.s, s', s'':t
x, y, z:elt
H:In x s <-> true = true
H0:In x s <->
(exists y0 : E.t,
   E.eq x y0 /\ List.In y0 (elements s))
H1:false = true <->
(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true)
true = false
s, s', s'':t
x, y, z:elt
H:In x s <-> false = true
H0:In x s <->
(exists y0 : E.t,
   E.eq x y0 /\ List.In y0 (elements s))
H1:true = true <->
(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true)
false = true
symmetry.s, s', s'':t
x, y, z:elt
H:In x s <-> true = true
H0:In x s <->
(exists y0 : E.t,
   E.eq x y0 /\ List.In y0 (elements s))
H1:false = true <->
(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true)
false = true
s, s', s'':t
x, y, z:elt
H:In x s <-> false = true
H0:In x s <->
(exists y0 : E.t,
   E.eq x y0 /\ List.In y0 (elements s))
H1:true = true <->
(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true)
false = true
rewrite H1.s, s', s'':t
x, y, z:elt
H:In x s <-> true = true
H0:In x s <->
(exists y0 : E.t,
   E.eq x y0 /\ List.In y0 (elements s))
H1:false = true <->
(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true)
exists x0 : E.t,
  List.In x0 (elements s) /\ eqb x x0 = true
s, s', s'':t
x, y, z:elt
H:In x s <-> false = true
H0:In x s <->
(exists y0 : E.t,
   E.eq x y0 /\ List.In y0 (elements s))
H1:true = true <->
(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true)
false = true
destruct H0 as (H0,_).s, s', s'':t
x, y, z:elt
H:In x s <-> true = true
H0:In x s ->
exists y0 : E.t,
  E.eq x y0 /\ List.In y0 (elements s)
H1:false = true <->
(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true)
exists x0 : E.t,
  List.In x0 (elements s) /\ eqb x x0 = true
s, s', s'':t
x, y, z:elt
H:In x s <-> false = true
H0:In x s <->
(exists y0 : E.t,
   E.eq x y0 /\ List.In y0 (elements s))
H1:true = true <->
(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true)
false = true
destruct H0 as (a,(Ha1,Ha2)); [ intuition |].s, s', s'':t
x, y, z:elt
H:In x s <-> true = true
H1:false = true <->
(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true)
a:E.t
Ha1:E.eq x a
Ha2:List.In a (elements s)
exists x0 : E.t,
  List.In x0 (elements s) /\ eqb x x0 = true
s, s', s'':t
x, y, z:elt
H:In x s <-> false = true
H0:In x s <->
(exists y0 : E.t,
   E.eq x y0 /\ List.In y0 (elements s))
H1:true = true <->
(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true)
false = true
exists a; intuition.s, s', s'':t
x, y, z:elt
a:E.t
Ha1:E.eq x a
Ha2:List.In a (elements s)
H:false = true ->
exists x0 : E.t,
  List.In x0 (elements s) /\ eqb x x0 = true
H3:(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true) ->
false = true
H1:In x s
H2:true = true
eqb x a = true
s, s', s'':t
x, y, z:elt
H:In x s <-> false = true
H0:In x s <->
(exists y0 : E.t,
   E.eq x y0 /\ List.In y0 (elements s))
H1:true = true <->
(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true)
false = true
unfold eqb; destruct (eq_dec x a); auto.s, s', s'':t
x, y, z:elt
H:In x s <-> false = true
H0:In x s <->
(exists y0 : E.t,
   E.eq x y0 /\ List.In y0 (elements s))
H1:true = true <->
(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true)
false = true
rewrite <- H.s, s', s'':t
x, y, z:elt
H:In x s <-> false = true
H0:In x s <->
(exists y0 : E.t,
   E.eq x y0 /\ List.In y0 (elements s))
H1:true = true <->
(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true)
In x s
rewrite H0.s, s', s'':t
x, y, z:elt
H:In x s <-> false = true
H0:In x s <->
(exists y0 : E.t,
   E.eq x y0 /\ List.In y0 (elements s))
H1:true = true <->
(exists x0 : E.t,
   List.In x0 (elements s) /\ eqb x x0 = true)
exists y0 : E.t, E.eq x y0 /\ List.In y0 (elements s)
destruct H1 as (H1,_).s, s', s'':t
x, y, z:elt
H:In x s <-> false = true
H0:In x s <->
(exists y0 : E.t,
   E.eq x y0 /\ List.In y0 (elements s))
H1:true = true ->
exists x0 : E.t,
  List.In x0 (elements s) /\ eqb x x0 = true
exists y0 : E.t, E.eq x y0 /\ List.In y0 (elements s)
destruct H1 as (a,(Ha1,Ha2)); [intuition|].s, s', s'':t
x, y, z:elt
H:In x s <-> false = true
H0:In x s <->
(exists y0 : E.t,
   E.eq x y0 /\ List.In y0 (elements s))
a:E.t
Ha1:List.In a (elements s)
Ha2:eqb x a = true
exists y0 : E.t, E.eq x y0 /\ List.In y0 (elements s)
exists a; intuition.s, s', s'':t
x, y, z:elt
a:E.t
Ha1:List.In a (elements s)
Ha2:eqb x a = true
H1:In x s -> false = true
H2:false = true -> In x s
H:In x s ->
exists y0 : E.t,
  E.eq x y0 /\ List.In y0 (elements s)
H3:(exists y0 : E.t,
   E.eq x y0 /\ List.In y0 (elements s)) ->
In x s
E.eq x a
unfold eqb in *; destruct (eq_dec x a); auto; discriminate.
Qed.

Variable f : elt->bool.

Lemma filter_b : Proper (E.eq==>Logic.eq) f -> mem x (filter f s) = mem x s && f x.s, s', s'':t
x, y, z:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
mem x (filter f s) = mem x s && f x
Proof.s, s', s'':t
x, y, z:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
mem x (filter f s) = mem x s && f x
intros.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
mem x (filter f s) = mem x s && f x
generalize (mem_iff (filter f s) x)(mem_iff s x)(filter_iff s x H).s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
In x (filter f s) <-> mem x (filter f s) = true ->
In x s <-> mem x s = true ->
In x (filter f s) <-> In x s /\ f x = true ->
mem x (filter f s) = mem x s && f x
destruct (mem x s); destruct (mem x (filter f s)); destruct (f x); simpl; intuition.
Qed.

Lemma for_all_b : Proper (E.eq==>Logic.eq) f ->
  for_all f s = forallb f (elements s).s, s', s'':t
x, y, z:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
for_all f s = forallb f (elements s)
Proof.s, s', s'':t
x, y, z:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
for_all f s = forallb f (elements s)
intros.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
for_all f s = forallb f (elements s)
generalize (forallb_forall f (elements s))(for_all_iff s H)(elements_iff s).s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
forallb f (elements s) = true <->
(forall x0 : elt,
 List.In x0 (elements s) -> f x0 = true) ->
For_all (fun x0 : elt => f x0 = true) s <->
for_all f s = true ->
(forall x0 : elt, In x0 s <-> InA E.eq x0 (elements s)) ->
for_all f s = forallb f (elements s)
unfold For_all.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
forallb f (elements s) = true <->
(forall x0 : elt,
 List.In x0 (elements s) -> f x0 = true) ->
(forall x0 : elt, In x0 s -> f x0 = true) <->
for_all f s = true ->
(forall x0 : elt, In x0 s <-> InA E.eq x0 (elements s)) ->
for_all f s = forallb f (elements s)
destruct (forallb f (elements s)); destruct (for_all f s); auto; intros.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:true = true <->
(forall x0 : elt,
 List.In x0 (elements s) -> f x0 = true)
H1:(forall x0 : elt, In x0 s -> f x0 = true) <->
false = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
false = true
s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(forall x0 : elt,
 List.In x0 (elements s) -> f x0 = true)
H1:(forall x0 : elt, In x0 s -> f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
true = false
rewrite <- H1; intros.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:true = true <->
(forall x1 : elt,
 List.In x1 (elements s) -> f x1 = true)
H1:(forall x1 : elt, In x1 s -> f x1 = true) <->
false = true
H2:forall x1 : elt,
In x1 s <-> InA E.eq x1 (elements s)
x0:elt
H3:In x0 s
f x0 = true
s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(forall x0 : elt,
 List.In x0 (elements s) -> f x0 = true)
H1:(forall x0 : elt, In x0 s -> f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
true = false
destruct H0 as (H0,_).s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:true = true ->
forall x1 : elt,
List.In x1 (elements s) -> f x1 = true
H1:(forall x1 : elt, In x1 s -> f x1 = true) <->
false = true
H2:forall x1 : elt,
In x1 s <-> InA E.eq x1 (elements s)
x0:elt
H3:In x0 s
f x0 = true
s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(forall x0 : elt,
 List.In x0 (elements s) -> f x0 = true)
H1:(forall x0 : elt, In x0 s -> f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
true = false
rewrite (H2 x0) in H3.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:true = true ->
forall x1 : elt,
List.In x1 (elements s) -> f x1 = true
H1:(forall x1 : elt, In x1 s -> f x1 = true) <->
false = true
H2:forall x1 : elt,
In x1 s <-> InA E.eq x1 (elements s)
x0:elt
H3:InA E.eq x0 (elements s)
f x0 = true
s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(forall x0 : elt,
 List.In x0 (elements s) -> f x0 = true)
H1:(forall x0 : elt, In x0 s -> f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
true = false
rewrite (InA_alt E.eq x0 (elements s)) in H3.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:true = true ->
forall x1 : elt,
List.In x1 (elements s) -> f x1 = true
H1:(forall x1 : elt, In x1 s -> f x1 = true) <->
false = true
H2:forall x1 : elt,
In x1 s <-> InA E.eq x1 (elements s)
x0:elt
H3:exists y0 : E.t,
  E.eq x0 y0 /\ List.In y0 (elements s)
f x0 = true
s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(forall x0 : elt,
 List.In x0 (elements s) -> f x0 = true)
H1:(forall x0 : elt, In x0 s -> f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
true = false
destruct H3 as (a,(Ha1,Ha2)).s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:true = true ->
forall x1 : elt,
List.In x1 (elements s) -> f x1 = true
H1:(forall x1 : elt, In x1 s -> f x1 = true) <->
false = true
H2:forall x1 : elt,
In x1 s <-> InA E.eq x1 (elements s)
x0:elt
a:E.t
Ha1:E.eq x0 a
Ha2:List.In a (elements s)
f x0 = true
s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(forall x0 : elt,
 List.In x0 (elements s) -> f x0 = true)
H1:(forall x0 : elt, In x0 s -> f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
true = false
rewrite (H _ _ Ha1).s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:true = true ->
forall x1 : elt,
List.In x1 (elements s) -> f x1 = true
H1:(forall x1 : elt, In x1 s -> f x1 = true) <->
false = true
H2:forall x1 : elt,
In x1 s <-> InA E.eq x1 (elements s)
x0:elt
a:E.t
Ha1:E.eq x0 a
Ha2:List.In a (elements s)
f a = true
s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(forall x0 : elt,
 List.In x0 (elements s) -> f x0 = true)
H1:(forall x0 : elt, In x0 s -> f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
true = false
apply H0; auto.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(forall x0 : elt,
 List.In x0 (elements s) -> f x0 = true)
H1:(forall x0 : elt, In x0 s -> f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
true = false
symmetry.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(forall x0 : elt,
 List.In x0 (elements s) -> f x0 = true)
H1:(forall x0 : elt, In x0 s -> f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
false = true
rewrite H0; intros.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(forall x1 : elt,
 List.In x1 (elements s) -> f x1 = true)
H1:(forall x1 : elt, In x1 s -> f x1 = true) <->
true = true
H2:forall x1 : elt,
In x1 s <-> InA E.eq x1 (elements s)
x0:elt
H3:List.In x0 (elements s)
f x0 = true
destruct H1 as (_,H1).s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(forall x1 : elt,
 List.In x1 (elements s) -> f x1 = true)
H1:true = true ->
forall x1 : elt, In x1 s -> f x1 = true
H2:forall x1 : elt,
In x1 s <-> InA E.eq x1 (elements s)
x0:elt
H3:List.In x0 (elements s)
f x0 = true
apply H1; auto.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(forall x1 : elt,
 List.In x1 (elements s) -> f x1 = true)
H1:true = true ->
forall x1 : elt, In x1 s -> f x1 = true
H2:forall x1 : elt,
In x1 s <-> InA E.eq x1 (elements s)
x0:elt
H3:List.In x0 (elements s)
In x0 s
rewrite H2.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(forall x1 : elt,
 List.In x1 (elements s) -> f x1 = true)
H1:true = true ->
forall x1 : elt, In x1 s -> f x1 = true
H2:forall x1 : elt,
In x1 s <-> InA E.eq x1 (elements s)
x0:elt
H3:List.In x0 (elements s)
InA E.eq x0 (elements s)
rewrite InA_alt.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(forall x1 : elt,
 List.In x1 (elements s) -> f x1 = true)
H1:true = true ->
forall x1 : elt, In x1 s -> f x1 = true
H2:forall x1 : elt,
In x1 s <-> InA E.eq x1 (elements s)
x0:elt
H3:List.In x0 (elements s)
exists y0 : E.t, E.eq x0 y0 /\ List.In y0 (elements s) exists x0; split; auto with relations.
Qed.

Lemma exists_b : Proper (E.eq==>Logic.eq) f ->
  exists_ f s = existsb f (elements s).s, s', s'':t
x, y, z:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
exists_ f s = existsb f (elements s)
Proof.s, s', s'':t
x, y, z:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
exists_ f s = existsb f (elements s)
intros.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
exists_ f s = existsb f (elements s)
generalize (existsb_exists f (elements s))(exists_iff s H)(elements_iff s).s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
existsb f (elements s) = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true) ->
Exists (fun x0 : elt => f x0 = true) s <->
exists_ f s = true ->
(forall x0 : elt, In x0 s <-> InA E.eq x0 (elements s)) ->
exists_ f s = existsb f (elements s)
unfold Exists.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
existsb f (elements s) = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true) ->
(exists x0 : elt, In x0 s /\ f x0 = true) <->
exists_ f s = true ->
(forall x0 : elt, In x0 s <-> InA E.eq x0 (elements s)) ->
exists_ f s = existsb f (elements s)
destruct (existsb f (elements s)); destruct (exists_ f s); auto; intros.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:true = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true)
H1:(exists x0 : elt, In x0 s /\ f x0 = true) <->
false = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
false = true
s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true)
H1:(exists x0 : elt, In x0 s /\ f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
true = false
rewrite <- H1; intros.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:true = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true)
H1:(exists x0 : elt, In x0 s /\ f x0 = true) <->
false = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
exists x0 : elt, In x0 s /\ f x0 = true
s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true)
H1:(exists x0 : elt, In x0 s /\ f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
true = false
destruct H0 as (H0,_).s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:true = true ->
exists x0 : elt,
  List.In x0 (elements s) /\ f x0 = true
H1:(exists x0 : elt, In x0 s /\ f x0 = true) <->
false = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
exists x0 : elt, In x0 s /\ f x0 = true
s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true)
H1:(exists x0 : elt, In x0 s /\ f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
true = false
destruct H0 as (a,(Ha1,Ha2)); auto.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H1:(exists x0 : elt, In x0 s /\ f x0 = true) <->
false = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
a:elt
Ha1:List.In a (elements s)
Ha2:f a = true
exists x0 : elt, In x0 s /\ f x0 = true
s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true)
H1:(exists x0 : elt, In x0 s /\ f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
true = false
exists a; split; auto.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H1:(exists x0 : elt, In x0 s /\ f x0 = true) <->
false = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
a:elt
Ha1:List.In a (elements s)
Ha2:f a = true
In a s
s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true)
H1:(exists x0 : elt, In x0 s /\ f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
true = false
rewrite H2; rewrite InA_alt; exists a; auto with relations.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true)
H1:(exists x0 : elt, In x0 s /\ f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
true = false
symmetry.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true)
H1:(exists x0 : elt, In x0 s /\ f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
false = true
rewrite H0.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true)
H1:(exists x0 : elt, In x0 s /\ f x0 = true) <->
true = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
exists x0 : elt,
  List.In x0 (elements s) /\ f x0 = true
destruct H1 as (_,H1).s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true)
H1:true = true ->
exists x0 : elt, In x0 s /\ f x0 = true
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
exists x0 : elt,
  List.In x0 (elements s) /\ f x0 = true
destruct H1 as (a,(Ha1,Ha2)); auto.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true)
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
a:elt
Ha1:In a s
Ha2:f a = true
exists x0 : elt,
  List.In x0 (elements s) /\ f x0 = true
rewrite (H2 a) in Ha1.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true)
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
a:elt
Ha1:InA E.eq a (elements s)
Ha2:f a = true
exists x0 : elt,
  List.In x0 (elements s) /\ f x0 = true
rewrite (InA_alt E.eq a (elements s)) in Ha1.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true)
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
a:elt
Ha1:exists y0 : E.t, E.eq a y0 /\ List.In y0 (elements s)
Ha2:f a = true
exists x0 : elt,
  List.In x0 (elements s) /\ f x0 = true
destruct Ha1 as (b,(Hb1,Hb2)).s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true)
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
a:elt
b:E.t
Hb1:E.eq a b
Hb2:List.In b (elements s)
Ha2:f a = true
exists x0 : elt,
  List.In x0 (elements s) /\ f x0 = true
exists b; auto.s, s', s'':t
x, y, z:elt
f:elt -> bool
H:Proper (E.eq ==> Logic.eq) f
H0:false = true <->
(exists x0 : elt,
   List.In x0 (elements s) /\ f x0 = true)
H2:forall x0 : elt,
In x0 s <-> InA E.eq x0 (elements s)
a:elt
b:E.t
Hb1:E.eq a b
Hb2:List.In b (elements s)
Ha2:f a = true
List.In b (elements s) /\ f b = true
rewrite <- (H _ _ Hb1); auto.
Qed.

End BoolSpec.

Declarations of morphisms with respects to E.eq and Equal

Instance In_m : Proper (E.eq==>Equal==>iff) In.Proper (E.eq ==> Equal ==> iff) In
Proof.Proper (E.eq ==> Equal ==> iff) In
unfold Equal; intros x y H s s' H0.x, y:E.t
H:E.eq x y
s, s':t
H0:forall a : elt, In a s <-> In a s'
In x s <-> In y s'
rewrite (In_eq_iff s H); auto.
Qed.

Instance Empty_m : Proper (Equal==>iff) Empty.Proper (Equal ==> iff) Empty
Proof.Proper (Equal ==> iff) Empty
repeat red; unfold Empty; intros s s' E.s, s':t
E:s [=] s'
((forall a : elt, ~ In a s) ->
 forall a : elt, ~ In a s') /\
((forall a : elt, ~ In a s') ->
 forall a : elt, ~ In a s)
setoid_rewrite E; auto.
Qed.

Instance is_empty_m : Proper (Equal==>Logic.eq) is_empty.Proper (Equal ==> Logic.eq) is_empty
Proof.Proper (Equal ==> Logic.eq) is_empty
intros s s' H.s, s':t
H:s [=] s'
is_empty s = is_empty s'
generalize (is_empty_iff s).s, s':t
H:s [=] s'
Empty s <-> is_empty s = true ->
is_empty s = is_empty s' rewrite H at 1.s, s':t
H:s [=] s'
Empty s' <-> is_empty s = true ->
is_empty s = is_empty s' rewrite is_empty_iff.s, s':t
H:s [=] s'
is_empty s' = true <-> is_empty s = true ->
is_empty s = is_empty s'
destruct (is_empty s); destruct (is_empty s'); intuition.
Qed.

Instance mem_m : Proper (E.eq==>Equal==>Logic.eq) mem.Proper (E.eq ==> Equal ==> Logic.eq) mem
Proof.Proper (E.eq ==> Equal ==> Logic.eq) mem
intros x x' Hx s s' Hs.x, x':E.t
Hx:E.eq x x'
s, s':t
Hs:s [=] s'
mem x s = mem x' s'
generalize (mem_iff s x).x, x':E.t
Hx:E.eq x x'
s, s':t
Hs:s [=] s'
In x s <-> mem x s = true -> mem x s = mem x' s' rewrite Hs, Hx at 1; rewrite mem_iff.x, x':E.t
Hx:E.eq x x'
s, s':t
Hs:s [=] s'
mem x' s' = true <-> mem x s = true ->
mem x s = mem x' s'
destruct (mem x s), (mem x' s'); intuition.
Qed.

Instance singleton_m : Proper (E.eq==>Equal) singleton.Proper (E.eq ==> Equal) singleton
Proof.Proper (E.eq ==> Equal) singleton
intros x y H a.x, y:E.t
H:E.eq x y
a:elt
In a (singleton x) <-> In a (singleton y) rewrite !singleton_iff, H; intuition.
Qed.

Instance add_m : Proper (E.eq==>Equal==>Equal) add.Proper (E.eq ==> Equal ==> Equal) add
Proof.Proper (E.eq ==> Equal ==> Equal) add
intros x x' Hx s s' Hs a.x, x':E.t
Hx:E.eq x x'
s, s':t
Hs:s [=] s'
a:elt
In a (add x s) <-> In a (add x' s') rewrite !add_iff, Hx, Hs; intuition.
Qed.

Instance remove_m : Proper (E.eq==>Equal==>Equal) remove.Proper (E.eq ==> Equal ==> Equal) remove
Proof.Proper (E.eq ==> Equal ==> Equal) remove
intros x x' Hx s s' Hs a.x, x':E.t
Hx:E.eq x x'
s, s':t
Hs:s [=] s'
a:elt
In a (remove x s) <-> In a (remove x' s') rewrite !remove_iff, Hx, Hs; intuition.
Qed.

Instance union_m : Proper (Equal==>Equal==>Equal) union.Proper (Equal ==> Equal ==> Equal) union
Proof.Proper (Equal ==> Equal ==> Equal) union
intros s1 s1' Hs1 s2 s2' Hs2 a.s1, s1':t
Hs1:s1 [=] s1'
s2, s2':t
Hs2:s2 [=] s2'
a:elt
In a (union s1 s2) <-> In a (union s1' s2') rewrite !union_iff, Hs1, Hs2; intuition.
Qed.

Instance inter_m : Proper (Equal==>Equal==>Equal) inter.Proper (Equal ==> Equal ==> Equal) inter
Proof.Proper (Equal ==> Equal ==> Equal) inter
intros s1 s1' Hs1 s2 s2' Hs2 a.s1, s1':t
Hs1:s1 [=] s1'
s2, s2':t
Hs2:s2 [=] s2'
a:elt
In a (inter s1 s2) <-> In a (inter s1' s2') rewrite !inter_iff, Hs1, Hs2; intuition.
Qed.

Instance diff_m : Proper (Equal==>Equal==>Equal) diff.Proper (Equal ==> Equal ==> Equal) diff
Proof.Proper (Equal ==> Equal ==> Equal) diff
intros s1 s1' Hs1 s2 s2' Hs2 a.s1, s1':t
Hs1:s1 [=] s1'
s2, s2':t
Hs2:s2 [=] s2'
a:elt
In a (diff s1 s2) <-> In a (diff s1' s2') rewrite !diff_iff, Hs1, Hs2; intuition.
Qed.

Instance Subset_m : Proper (Equal==>Equal==>iff) Subset.Proper (Equal ==> Equal ==> iff) Subset
Proof.Proper (Equal ==> Equal ==> iff) Subset
unfold Equal, Subset; firstorder.
Qed.

Instance subset_m : Proper (Equal==>Equal==>Logic.eq) subset.Proper (Equal ==> Equal ==> Logic.eq) subset
Proof.Proper (Equal ==> Equal ==> Logic.eq) subset
intros s1 s1' Hs1 s2 s2' Hs2.s1, s1':t
Hs1:s1 [=] s1'
s2, s2':t
Hs2:s2 [=] s2'
subset s1 s2 = subset s1' s2'
generalize (subset_iff s1 s2).s1, s1':t
Hs1:s1 [=] s1'
s2, s2':t
Hs2:s2 [=] s2'
s1 [<=] s2 <-> subset s1 s2 = true ->
subset s1 s2 = subset s1' s2' rewrite Hs1, Hs2 at 1.s1, s1':t
Hs1:s1 [=] s1'
s2, s2':t
Hs2:s2 [=] s2'
s1' [<=] s2' <-> subset s1 s2 = true ->
subset s1 s2 = subset s1' s2' rewrite subset_iff.s1, s1':t
Hs1:s1 [=] s1'
s2, s2':t
Hs2:s2 [=] s2'
subset s1' s2' = true <-> subset s1 s2 = true ->
subset s1 s2 = subset s1' s2'
destruct (subset s1 s2); destruct (subset s1' s2'); intuition.
Qed.

Instance equal_m : Proper (Equal==>Equal==>Logic.eq) equal.Proper (Equal ==> Equal ==> Logic.eq) equal
Proof.Proper (Equal ==> Equal ==> Logic.eq) equal
intros s1 s1' Hs1 s2 s2' Hs2.s1, s1':t
Hs1:s1 [=] s1'
s2, s2':t
Hs2:s2 [=] s2'
equal s1 s2 = equal s1' s2'
generalize (equal_iff s1 s2).s1, s1':t
Hs1:s1 [=] s1'
s2, s2':t
Hs2:s2 [=] s2'
s1 [=] s2 <-> equal s1 s2 = true ->
equal s1 s2 = equal s1' s2' rewrite Hs1,Hs2 at 1.s1, s1':t
Hs1:s1 [=] s1'
s2, s2':t
Hs2:s2 [=] s2'
s1' [=] s2' <-> equal s1 s2 = true ->
equal s1 s2 = equal s1' s2' rewrite equal_iff.s1, s1':t
Hs1:s1 [=] s1'
s2, s2':t
Hs2:s2 [=] s2'
equal s1' s2' = true <-> equal s1 s2 = true ->
equal s1 s2 = equal s1' s2'
destruct (equal s1 s2); destruct (equal s1' s2'); intuition.
Qed.

Instance SubsetSetoid : PreOrder Subset. (* reflexive + transitive *)PreOrder Subset
Proof.PreOrder Subset firstorder. Qed.

Definition Subset_refl := @PreOrder_Reflexive _ _ SubsetSetoid.
Definition Subset_trans := @PreOrder_Transitive _ _ SubsetSetoid.

Instance In_s_m : Morphisms.Proper (E.eq ==> Subset ++> impl) In | 1.Proper (E.eq ==> Subset ==> impl) In
Proof.Proper (E.eq ==> Subset ==> impl) In
  simpl_relation.x, y:E.t
H:E.eq x y
x0, y0:t
H0:x0 [<=] y0
H1:In x x0
In y y0 eauto with set.
Qed.

Instance Empty_s_m : Proper (Subset-->impl) Empty.Proper (Subset --> impl) Empty
Proof.Proper (Subset --> impl) Empty firstorder. Qed.

Instance add_s_m : Proper (E.eq==>Subset++>Subset) add.Proper (E.eq ==> Subset ==> Subset) add
Proof.Proper (E.eq ==> Subset ==> Subset) add
intros x x' Hx s s' Hs a.x, x':E.t
Hx:E.eq x x'
s, s':t
Hs:s [<=] s'
a:elt
In a (add x s) -> In a (add x' s') rewrite !add_iff, Hx; intuition.
Qed.

Instance remove_s_m : Proper (E.eq==>Subset++>Subset) remove.Proper (E.eq ==> Subset ==> Subset) remove
Proof.Proper (E.eq ==> Subset ==> Subset) remove
intros x x' Hx s s' Hs a.x, x':E.t
Hx:E.eq x x'
s, s':t
Hs:s [<=] s'
a:elt
In a (remove x s) -> In a (remove x' s') rewrite !remove_iff, Hx; intuition.
Qed.

Instance union_s_m : Proper (Subset++>Subset++>Subset) union.Proper (Subset ==> Subset ==> Subset) union
Proof.Proper (Subset ==> Subset ==> Subset) union
intros s1 s1' Hs1 s2 s2' Hs2 a.s1, s1':t
Hs1:s1 [<=] s1'
s2, s2':t
Hs2:s2 [<=] s2'
a:elt
In a (union s1 s2) -> In a (union s1' s2') rewrite !union_iff, Hs1, Hs2; intuition.
Qed.

Instance inter_s_m : Proper (Subset++>Subset++>Subset) inter.Proper (Subset ==> Subset ==> Subset) inter
Proof.Proper (Subset ==> Subset ==> Subset) inter
intros s1 s1' Hs1 s2 s2' Hs2 a.s1, s1':t
Hs1:s1 [<=] s1'
s2, s2':t
Hs2:s2 [<=] s2'
a:elt
In a (inter s1 s2) -> In a (inter s1' s2') rewrite !inter_iff, Hs1, Hs2; intuition.
Qed.

Instance diff_s_m : Proper (Subset++>Subset-->Subset) diff.Proper (Subset ==> Subset --> Subset) diff
Proof.Proper (Subset ==> Subset --> Subset) diff
intros s1 s1' Hs1 s2 s2' Hs2 a.s1, s1':t
Hs1:s1 [<=] s1'
s2, s2':t
Hs2:flip Subset s2 s2'
a:elt
In a (diff s1 s2) -> In a (diff s1' s2') rewrite !diff_iff, Hs1, Hs2; intuition.
Qed.


(* [fold], [filter], [for_all], [exists_] and [partition] requires
  some knowledge on [f] in order to be known as morphisms. *)

Generalizable Variables f.

Instance filter_equal : forall `(Proper _ (E.eq==>Logic.eq) f),
 Proper (Equal==>Equal) (filter f).forall f : E.t -> bool,
Proper (E.eq ==> Logic.eq) f ->
Proper (Equal ==> Equal) (filter f)
Proof.forall f : E.t -> bool,
Proper (E.eq ==> Logic.eq) f ->
Proper (Equal ==> Equal) (filter f)
intros f Hf s s' Hs a.f:E.t -> bool
Hf:Proper (E.eq ==> Logic.eq) f
s, s':t
Hs:s [=] s'
a:elt
In a (filter f s) <-> In a (filter f s') rewrite !filter_iff, Hs by auto; intuition.
Qed.

Instance filter_subset : forall `(Proper _ (E.eq==>Logic.eq) f),
 Proper (Subset==>Subset) (filter f).forall f : E.t -> bool,
Proper (E.eq ==> Logic.eq) f ->
Proper (Subset ==> Subset) (filter f)
Proof.forall f : E.t -> bool,
Proper (E.eq ==> Logic.eq) f ->
Proper (Subset ==> Subset) (filter f)
intros f Hf s s' Hs a.f:E.t -> bool
Hf:Proper (E.eq ==> Logic.eq) f
s, s':t
Hs:s [<=] s'
a:elt
In a (filter f s) -> In a (filter f s') rewrite !filter_iff, Hs by auto; intuition.
Qed.

Lemma filter_ext : forall f f', Proper (E.eq==>Logic.eq) f -> (forall x, f x = f' x) ->
 forall s s', s[=]s' -> filter f s [=] filter f' s'.forall f f' : E.t -> bool,
Proper (E.eq ==> Logic.eq) f ->
(forall x : E.t, f x = f' x) ->
forall s s' : t,
s [=] s' -> filter f s [=] filter f' s'
Proof.forall f f' : E.t -> bool,
Proper (E.eq ==> Logic.eq) f ->
(forall x : E.t, f x = f' x) ->
forall s s' : t,
s [=] s' -> filter f s [=] filter f' s'
intros f f' Hf Hff' s s' Hss' x.f, f':E.t -> bool
Hf:Proper (E.eq ==> Logic.eq) f
Hff':forall x0 : E.t, f x0 = f' x0
s, s':t
Hss':s [=] s'
x:elt
In x (filter f s) <-> In x (filter f' s') rewrite 2 filter_iff; auto.f, f':E.t -> bool
Hf:Proper (E.eq ==> Logic.eq) f
Hff':forall x0 : E.t, f x0 = f' x0
s, s':t
Hss':s [=] s'
x:elt
In x s /\ f x = true <-> In x s' /\ f' x = true
f, f':E.t -> bool
Hf:Proper (E.eq ==> Logic.eq) f
Hff':forall x0 : E.t, f x0 = f' x0
s, s':t
Hss':s [=] s'
x:elt
Proper (E.eq ==> Logic.eq) f'
rewrite Hff', Hss'; intuition.f, f':E.t -> bool
Hf:Proper (E.eq ==> Logic.eq) f
Hff':forall x0 : E.t, f x0 = f' x0
s, s':t
Hss':s [=] s'
x:elt
Proper (E.eq ==> Logic.eq) f'
red; red; intros; rewrite <- 2 Hff'; auto.
Qed.

(* For [elements], [min_elt], [max_elt] and [choose], we would need setoid
   structures on [list elt] and [option elt]. *)

(* Later:
Add Morphism cardinal ; cardinal_m.
*)

End WFactsOn.

Now comes variants for self-contained weak sets and for full sets. For these variants, only one argument is necessary. Thanks to the subtyping WS≤S, the Facts functor which is meant to be used on modules (M:S) can simply be an alias of WFacts.

Module WFacts (M:WSets) := WFactsOn M.E M.
Module Facts := WFacts.