(************************************************************************)
(*         *   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)         *)
(************************************************************************)

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

Module WFacts_fun (Import E : DecidableType)(Import M : WSfun E).

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

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
split; apply In_1; auto.
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
split; [apply mem_1|apply mem_2].
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_iff; 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
split; [apply equal_1|apply equal_2].
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
split; [apply subset_1|apply subset_2].
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_1 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
split; [apply is_empty_1|apply is_empty_2].
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
split; [apply singleton_1|apply singleton_2].
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
split; [ | destruct 1; [apply add_1|apply add_2]]; auto.
s, s', s'':t
x, y, z:elt
In y (add x s) -> E.eq x y \/ In y s
destruct (eq_dec x y) as [E|E]; auto.
s, s', s'':t
x, y, z:elt
E:~ E.eq x y
In y (add x s) -> E.eq x y \/ In y s
intro H; right; exact (add_3 E H).
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
split; [apply add_3|apply add_2]; auto.
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
split; [split; [apply remove_3 with x |] | destruct 1; apply remove_2]; auto.
s, s', s'':t
x, y, z:elt
H:In y (remove x s)
~ E.eq x y
intro.
s, s', s'':t
x, y, z:elt
H:In y (remove x s)
H0:E.eq x y
False
apply (remove_1 H0 H).
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
split; [apply remove_3|apply remove_2]; auto.
Qed.

Lemma union_iff : In x (union s s') <-> In x s \/ In x s'.
s, s', s'':t
x, y, z:elt
In x (union s s') <-> In x s \/ In x s'
Proof.
s, s', s'':t
x, y, z:elt
In x (union s s') <-> In x s \/ In x s'
split; [apply union_1 | destruct 1; [apply union_2|apply union_3]]; auto.
Qed.

Lemma inter_iff : In x (inter s s') <-> In x s /\ In x s'.
s, s', s'':t
x, y, z:elt
In x (inter s s') <-> In x s /\ In x s'
Proof.
s, s', s'':t
x, y, z:elt
In x (inter s s') <-> In x s /\ In x s'
split; [split; [apply inter_1 with s' | apply inter_2 with s] | destruct 1; apply inter_3]; auto.
Qed.

Lemma diff_iff : In x (diff s s') <-> In x s /\ ~ In x s'.
s, s', s'':t
x, y, z:elt
In x (diff s s') <-> In x s /\ ~ In x s'
Proof.
s, s', s'':t
x, y, z:elt
In x (diff s s') <-> In x s /\ ~ In x s'
split; [split; [apply diff_1 with s' | apply diff_2 with s] | destruct 1; apply diff_3]; auto.
Qed.

Variable f : elt->bool.

Lemma filter_iff :  compat_bool E.eq f -> (In x (filter f s) <-> In x s /\ f x = true).
s, s', s'':t
x, y, z:elt
f:elt -> bool
compat_bool E.eq f ->
In x (filter f s) <-> In x s /\ f x = true
Proof.
s, s', s'':t
x, y, z:elt
f:elt -> bool
compat_bool E.eq f ->
In x (filter f s) <-> In x s /\ f x = true
split; [split; [apply filter_1 with f | apply filter_2 with s] | destruct 1; apply filter_3]; auto.
Qed.

Lemma for_all_iff : compat_bool E.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
compat_bool E.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
compat_bool E.eq f ->
For_all (fun x0 : elt => f x0 = true) s <->
for_all f s = true
split; [apply for_all_1 | apply for_all_2]; auto.
Qed.

Lemma exists_iff : compat_bool E.eq f ->
  (Exists (fun x => f x = true) s <-> exists_ f s = true).
s, s', s'':t
x, y, z:elt
f:elt -> bool
compat_bool E.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
compat_bool E.eq f ->
Exists (fun x0 : elt => f x0 = true) s <->
exists_ f s = true
split; [apply exists_1 | apply exists_2]; 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)
split; [apply elements_1 | apply elements_2].
Qed.

End IffSpec.

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)).

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 : compat_bool E.eq f -> mem x (filter f s) = mem x s && f x.
s, s', s'':t
x, y, z:elt
f:elt -> bool
compat_bool E.eq f ->
mem x (filter f s) = mem x s && f x
Proof.
s, s', s'':t
x, y, z:elt
f:elt -> bool
compat_bool E.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:compat_bool E.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:compat_bool E.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 : compat_bool E.eq f ->
  for_all f s = forallb f (elements s).
s, s', s'':t
x, y, z:elt
f:elt -> bool
compat_bool E.eq f ->
for_all f s = forallb f (elements s)
Proof.
s, s', s'':t
x, y, z:elt
f:elt -> bool
compat_bool E.eq f ->
for_all f s = forallb f (elements s)
intros.
s, s', s'':t
x, y, z:elt
f:elt -> bool
H:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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; eauto.
Qed.

Lemma exists_b : compat_bool E.eq f ->
  exists_ f s = existsb f (elements s).
s, s', s'':t
x, y, z:elt
f:elt -> bool
compat_bool E.eq f ->
exists_ f s = existsb f (elements s)
Proof.
s, s', s'':t
x, y, z:elt
f:elt -> bool
compat_bool E.eq f ->
exists_ f s = existsb f (elements s)
intros.
s, s', s'':t
x, y, z:elt
f:elt -> bool
H:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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; eauto.
s, s', s'':t
x, y, z:elt
f:elt -> bool
H:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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:compat_bool E.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.

Instance E_ST : Equivalence E.eq.
Equivalence E.eq
Proof.
Equivalence E.eq
constructor ; red; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans].
Qed.

Instance Equal_ST : Equivalence Equal.
Equivalence Equal
Proof.
Equivalence Equal
constructor ; red; [apply eq_refl | apply eq_sym | apply eq_trans].
Qed.

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 is_empty_m : Proper (Equal==> Logic.eq) is_empty.
Proper (Equal ==> Logic.eq) is_empty
Proof.
Proper (Equal ==> Logic.eq) is_empty
unfold Equal; intros s s' H.
s, s':t
H:forall a : elt, In a s <-> In a s'
is_empty s = is_empty s'
generalize (is_empty_iff s)(is_empty_iff s').
s, s':t
H:forall a : elt, In a s <-> In a s'
Empty s <-> is_empty s = true ->
Empty s' <-> is_empty s' = true ->
is_empty s = is_empty s'
destruct (is_empty s); destruct (is_empty s');
 unfold Empty; auto; intros.
s, s':t
H:forall a : elt, In a s <-> In a s'
H0:(forall a : elt, ~ In a s) <-> true = true
H1:(forall a : elt, ~ In a s') <-> false = true
true = false
s, s':t
H:forall a : elt, In a s <-> In a s'
H0:(forall a : elt, ~ In a s) <-> false = true
H1:(forall a : elt, ~ In a s') <-> true = true
false = true
symmetry.
s, s':t
H:forall a : elt, In a s <-> In a s'
H0:(forall a : elt, ~ In a s) <-> true = true
H1:(forall a : elt, ~ In a s') <-> false = true
false = true
s, s':t
H:forall a : elt, In a s <-> In a s'
H0:(forall a : elt, ~ In a s) <-> false = true
H1:(forall a : elt, ~ In a s') <-> true = true
false = true
rewrite <- H1; intros a Ha.
s, s':t
H:forall a0 : elt, In a0 s <-> In a0 s'
H0:(forall a0 : elt, ~ In a0 s) <-> true = true
H1:(forall a0 : elt, ~ In a0 s') <-> false = true
a:elt
Ha:In a s'
False
s, s':t
H:forall a : elt, In a s <-> In a s'
H0:(forall a : elt, ~ In a s) <-> false = true
H1:(forall a : elt, ~ In a s') <-> true = true
false = true
rewrite <- (H a) in Ha.
s, s':t
H:forall a0 : elt, In a0 s <-> In a0 s'
H0:(forall a0 : elt, ~ In a0 s) <-> true = true
H1:(forall a0 : elt, ~ In a0 s') <-> false = true
a:elt
Ha:In a s
False
s, s':t
H:forall a : elt, In a s <-> In a s'
H0:(forall a : elt, ~ In a s) <-> false = true
H1:(forall a : elt, ~ In a s') <-> true = true
false = true
destruct H0 as (_,H0).
s, s':t
H:forall a0 : elt, In a0 s <-> In a0 s'
H0:true = true -> forall a0 : elt, ~ In a0 s
H1:(forall a0 : elt, ~ In a0 s') <-> false = true
a:elt
Ha:In a s
False
s, s':t
H:forall a : elt, In a s <-> In a s'
H0:(forall a : elt, ~ In a s) <-> false = true
H1:(forall a : elt, ~ In a s') <-> true = true
false = true
exact (H0 Logic.eq_refl _ Ha).
s, s':t
H:forall a : elt, In a s <-> In a s'
H0:(forall a : elt, ~ In a s) <-> false = true
H1:(forall a : elt, ~ In a s') <-> true = true
false = true
rewrite <- H0; intros a Ha.
s, s':t
H:forall a0 : elt, In a0 s <-> In a0 s'
H0:(forall a0 : elt, ~ In a0 s) <-> false = true
H1:(forall a0 : elt, ~ In a0 s') <-> true = true
a:elt
Ha:In a s
False
rewrite (H a) in Ha.
s, s':t
H:forall a0 : elt, In a0 s <-> In a0 s'
H0:(forall a0 : elt, ~ In a0 s) <-> false = true
H1:(forall a0 : elt, ~ In a0 s') <-> true = true
a:elt
Ha:In a s'
False
destruct H1 as (_,H1).
s, s':t
H:forall a0 : elt, In a0 s <-> In a0 s'
H0:(forall a0 : elt, ~ In a0 s) <-> false = true
H1:true = true -> forall a0 : elt, ~ In a0 s'
a:elt
Ha:In a s'
False
exact (H1 Logic.eq_refl _ Ha).
Qed.

Instance Empty_m : Proper (Equal ==> iff) Empty.
Proper (Equal ==> iff) Empty
Proof.
Proper (Equal ==> iff) Empty
repeat red; intros; do 2 rewrite is_empty_iff; rewrite H; 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
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'
mem x s = mem y s'
generalize (H0 x); clear H0; rewrite (In_eq_iff s' H).
x, y:E.t
H:E.eq x y
s, s':t
In x s <-> In y s' -> mem x s = mem y s'
generalize (mem_iff s x)(mem_iff s' y).
x, y:E.t
H:E.eq x y
s, s':t
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.

Instance singleton_m : Proper (E.eq ==> Equal) singleton.
Proper (E.eq ==> Equal) singleton
Proof.
Proper (E.eq ==> Equal) singleton
unfold Equal; intros x y H a.
x, y:E.t
H:E.eq x y
a:elt
In a (singleton x) <-> In a (singleton y)
do 2 rewrite singleton_iff; split; intros.
x, y:E.t
H:E.eq x y
a:elt
H0:E.eq x a
E.eq y a
x, y:E.t
H:E.eq x y
a:elt
H0:E.eq y a
E.eq x a
apply E.eq_trans with x; auto.
x, y:E.t
H:E.eq x y
a:elt
H0:E.eq y a
E.eq x a
apply E.eq_trans with y; auto.
Qed.

Instance add_m : Proper (E.eq==>Equal==>Equal) add.
Proper (E.eq ==> Equal ==> Equal) add
Proof.
Proper (E.eq ==> Equal ==> Equal) add
unfold Equal; intros x y H s s' H0 a.
x, y:E.t
H:E.eq x y
s, s':t
H0:forall a0 : elt, In a0 s <-> In a0 s'
a:elt
In a (add x s) <-> In a (add y s')
do 2 rewrite add_iff; rewrite H; rewrite H0; intuition.
Qed.

Instance remove_m : Proper (E.eq==>Equal==>Equal) remove.
Proper (E.eq ==> Equal ==> Equal) remove
Proof.
Proper (E.eq ==> Equal ==> Equal) remove
unfold Equal; intros x y H s s' H0 a.
x, y:E.t
H:E.eq x y
s, s':t
H0:forall a0 : elt, In a0 s <-> In a0 s'
a:elt
In a (remove x s) <-> In a (remove y s')
do 2 rewrite remove_iff; rewrite H; rewrite H0; intuition.
Qed.

Instance union_m : Proper (Equal==>Equal==>Equal) union.
Proper (Equal ==> Equal ==> Equal) union
Proof.
Proper (Equal ==> Equal ==> Equal) union
unfold Equal; intros s s' H s'' s''' H0 a.
s, s':t
H:forall a0 : elt, In a0 s <-> In a0 s'
s'', s''':t
H0:forall a0 : elt, In a0 s'' <-> In a0 s'''
a:elt
In a (union s s'') <-> In a (union s' s''')
do 2 rewrite union_iff; rewrite H; rewrite H0; intuition.
Qed.

Instance inter_m : Proper (Equal==>Equal==>Equal) inter.
Proper (Equal ==> Equal ==> Equal) inter
Proof.
Proper (Equal ==> Equal ==> Equal) inter
unfold Equal; intros s s' H s'' s''' H0 a.
s, s':t
H:forall a0 : elt, In a0 s <-> In a0 s'
s'', s''':t
H0:forall a0 : elt, In a0 s'' <-> In a0 s'''
a:elt
In a (inter s s'') <-> In a (inter s' s''')
do 2 rewrite inter_iff; rewrite H; rewrite H0; intuition.
Qed.

Instance diff_m : Proper (Equal==>Equal==>Equal) diff.
Proper (Equal ==> Equal ==> Equal) diff
Proof.
Proper (Equal ==> Equal ==> Equal) diff
unfold Equal; intros s s' H s'' s''' H0 a.
s, s':t
H:forall a0 : elt, In a0 s <-> In a0 s'
s'', s''':t
H0:forall a0 : elt, In a0 s'' <-> In a0 s'''
a:elt
In a (diff s s'') <-> In a (diff s' s''')
do 2 rewrite diff_iff; rewrite H; rewrite H0; 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 s s' H s'' s''' H0.
s, s':t
H:s [=] s'
s'', s''':t
H0:s'' [=] s'''
subset s s'' = subset s' s'''
generalize (subset_iff s s'') (subset_iff s' s''').
s, s':t
H:s [=] s'
s'', s''':t
H0:s'' [=] s'''
s [<=] s'' <-> subset s s'' = true ->
s' [<=] s''' <-> subset s' s''' = true ->
subset s s'' = subset s' s'''
destruct (subset s s''); destruct (subset s' s'''); auto; intros.
s, s':t
H:s [=] s'
s'', s''':t
H0:s'' [=] s'''
H1:s [<=] s'' <-> true = true
H2:s' [<=] s''' <-> false = true
true = false
s, s':t
H:s [=] s'
s'', s''':t
H0:s'' [=] s'''
H1:s [<=] s'' <-> false = true
H2:s' [<=] s''' <-> true = true
false = true
rewrite H in H1; rewrite H0 in H1; intuition.
s, s':t
H:s [=] s'
s'', s''':t
H0:s'' [=] s'''
H1:s [<=] s'' <-> false = true
H2:s' [<=] s''' <-> true = true
false = true
rewrite H in H1; rewrite H0 in H1; 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 s s' H s'' s''' H0.
s, s':t
H:s [=] s'
s'', s''':t
H0:s'' [=] s'''
equal s s'' = equal s' s'''
generalize (equal_iff s s'') (equal_iff s' s''').
s, s':t
H:s [=] s'
s'', s''':t
H0:s'' [=] s'''
s [=] s'' <-> equal s s'' = true ->
s' [=] s''' <-> equal s' s''' = true ->
equal s s'' = equal s' s'''
destruct (equal s s''); destruct (equal s' s'''); auto; intros.
s, s':t
H:s [=] s'
s'', s''':t
H0:s'' [=] s'''
H1:s [=] s'' <-> true = true
H2:s' [=] s''' <-> false = true
true = false
s, s':t
H:s [=] s'
s'', s''':t
H0:s'' [=] s'''
H1:s [=] s'' <-> false = true
H2:s' [=] s''' <-> true = true
false = true
rewrite H in H1; rewrite H0 in H1; intuition.
s, s':t
H:s [=] s'
s'', s''':t
H0:s'' [=] s'''
H1:s [=] s'' <-> false = true
H2:s' [=] s''' <-> true = true
false = true
rewrite H in H1; rewrite H0 in H1; intuition.
Qed.


(* [Subset] is a setoid order *)

Lemma Subset_refl : forall s, s[<=]s.
forall s : t, s [<=] s
Proof.
forall s : t, s [<=] s red; auto. Qed.

Lemma Subset_trans : forall s s' s'', s[<=]s'->s'[<=]s''->s[<=]s''.
forall s s' s'' : t,
s [<=] s' -> s' [<=] s'' -> s [<=] s''
Proof.
forall s s' s'' : t,
s [<=] s' -> s' [<=] s'' -> s [<=] s'' unfold Subset; eauto. Qed.

Add Relation t Subset
 reflexivity proved by Subset_refl
 transitivity proved by Subset_trans
 as SubsetSetoid.

Instance In_s_m : Morphisms.Proper (E.eq ==> Subset ++> Basics.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.

Add Morphism Empty with signature Subset --> Basics.impl as Empty_s_m.
forall x y : t, y [<=] x -> impl (Empty x) (Empty y)
Proof.
forall x y : t, y [<=] x -> impl (Empty x) (Empty y)
unfold Subset, Empty, Basics.impl; firstorder.
Qed.

Add Morphism add with signature E.eq ==> Subset ++> Subset as add_s_m.
forall x y : E.t,
E.eq x y ->
forall x0 y0 : t, x0 [<=] y0 -> add x x0 [<=] add y y0
Proof.
forall x y : E.t,
E.eq x y ->
forall x0 y0 : t, x0 [<=] y0 -> add x x0 [<=] add y y0
unfold Subset; intros x y H s s' H0 a.
x, y:E.t
H:E.eq x y
s, s':t
H0:forall a0 : elt, In a0 s -> In a0 s'
a:elt
In a (add x s) -> In a (add y s')
do 2 rewrite add_iff; rewrite H; intuition.
Qed.

Add Morphism remove with signature E.eq ==> Subset ++> Subset as remove_s_m.
forall x y : E.t,
E.eq x y ->
forall x0 y0 : t,
x0 [<=] y0 -> remove x x0 [<=] remove y y0
Proof.
forall x y : E.t,
E.eq x y ->
forall x0 y0 : t,
x0 [<=] y0 -> remove x x0 [<=] remove y y0
unfold Subset; intros x y H s s' H0 a.
x, y:E.t
H:E.eq x y
s, s':t
H0:forall a0 : elt, In a0 s -> In a0 s'
a:elt
In a (remove x s) -> In a (remove y s')
do 2 rewrite remove_iff; rewrite H; intuition.
Qed.

Add Morphism union with signature Subset ++> Subset ++> Subset as union_s_m.
forall x y : t,
x [<=] y ->
forall x0 y0 : t,
x0 [<=] y0 -> union x x0 [<=] union y y0
Proof.
forall x y : t,
x [<=] y ->
forall x0 y0 : t,
x0 [<=] y0 -> union x x0 [<=] union y y0
unfold Equal; intros s s' H s'' s''' H0 a.
s, s':t
H:s [<=] s'
s'', s''':t
H0:s'' [<=] s'''
a:elt
In a (union s s'') -> In a (union s' s''')
do 2 rewrite union_iff; intuition.
Qed.

Add Morphism inter with signature Subset ++> Subset ++> Subset as inter_s_m.
forall x y : t,
x [<=] y ->
forall x0 y0 : t,
x0 [<=] y0 -> inter x x0 [<=] inter y y0
Proof.
forall x y : t,
x [<=] y ->
forall x0 y0 : t,
x0 [<=] y0 -> inter x x0 [<=] inter y y0
unfold Equal; intros s s' H s'' s''' H0 a.
s, s':t
H:s [<=] s'
s'', s''':t
H0:s'' [<=] s'''
a:elt
In a (inter s s'') -> In a (inter s' s''')
do 2 rewrite inter_iff; intuition.
Qed.

Add Morphism diff with signature Subset ++> Subset --> Subset as diff_s_m.
forall x y : t,
x [<=] y ->
forall x0 y0 : t,
y0 [<=] x0 -> diff x x0 [<=] diff y y0
Proof.
forall x y : t,
x [<=] y ->
forall x0 y0 : t,
y0 [<=] x0 -> diff x x0 [<=] diff y y0
unfold Subset; intros s s' H s'' s''' H0 a.
s, s':t
H:forall a0 : elt, In a0 s -> In a0 s'
s'', s''':t
H0:forall a0 : elt, In a0 s''' -> In a0 s''
a:elt
In a (diff s s'') -> In a (diff s' s''')
do 2 rewrite diff_iff; intuition.
Qed.

(* [fold], [filter], [for_all], [exists_] and [partition] cannot be proved morphism
   without additional hypothesis on [f]. For instance: *)

Lemma filter_equal : forall f, compat_bool E.eq f ->
  forall s s', s[=]s' -> filter f s [=] filter f s'.
forall f : E.t -> bool,
compat_bool E.eq f ->
forall s s' : t,
s [=] s' -> filter f s [=] filter f s'
Proof.
forall f : E.t -> bool,
compat_bool E.eq f ->
forall s s' : t,
s [=] s' -> filter f s [=] filter f s'
unfold Equal; intros; repeat rewrite filter_iff; auto; rewrite H0; tauto.
Qed.

Lemma filter_ext : forall f f', compat_bool E.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,
compat_bool E.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,
compat_bool E.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:compat_bool E.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') do 2 (rewrite filter_iff; auto).
f, f':E.t -> bool
Hf:compat_bool E.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:compat_bool E.eq f
Hff':forall x0 : E.t, f x0 = f' x0
s, s':t
Hss':s [=] s'
x:elt
compat_bool E.eq f'
rewrite Hff', Hss'; intuition.
f, f':E.t -> bool
Hf:compat_bool E.eq f
Hff':forall x0 : E.t, f x0 = f' x0
s, s':t
Hss':s [=] s'
x:elt
compat_bool E.eq f'
repeat red; intros; rewrite <- 2 Hff'; auto.
Qed.

Lemma filter_subset : forall f, compat_bool E.eq f ->
  forall s s', s[<=]s' -> filter f s [<=] filter f s'.
forall f : E.t -> bool,
compat_bool E.eq f ->
forall s s' : t,
s [<=] s' -> filter f s [<=] filter f s'
Proof.
forall f : E.t -> bool,
compat_bool E.eq f ->
forall s s' : t,
s [<=] s' -> filter f s [<=] filter f s'
unfold Subset; intros; rewrite filter_iff in *; intuition.
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 WFacts_fun.