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 module proves many properties of finite sets that are consequences of the axiomatization in FsetInterface Contrary to the functor in FsetProperties it uses sets operations instead of predicates over sets, i.e. mem x s=true instead of In x s, equal s s'=true instead of Equal s s', etc.

Require Import FSetProperties Zerob Sumbool Omega DecidableTypeEx.

Module WEqProperties_fun (Import E:DecidableType)(M:WSfun E).
Module Import MP := WProperties_fun E M.
Import FM Dec.F.
Import M.

Definition Add := MP.Add.

Section BasicProperties.

Some old specifications written with boolean equalities.

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

Lemma mem_eq:
  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
intro H; rewrite H; auto.
Qed.

Lemma equal_mem_1:
  (forall a, mem a s=mem a s') -> equal s s'=true.s, s', s'':t
x, y, z:elt
(forall a : elt, mem a s = mem a s') ->
equal s s' = true
Proof.s, s', s'':t
x, y, z:elt
(forall a : elt, mem a s = mem a s') ->
equal s s' = true
intros; apply equal_1; unfold Equal; intros.s, s', s'':t
x, y, z:elt
H:forall a0 : elt, mem a0 s = mem a0 s'
a:elt
In a s <-> In a s'
do 2 rewrite mem_iff; rewrite H; tauto.
Qed.

Lemma equal_mem_2:
  equal s s'=true -> forall a, mem a s=mem a s'.s, s', s'':t
x, y, z:elt
equal s s' = true ->
forall a : elt, mem a s = mem a s'
Proof.s, s', s'':t
x, y, z:elt
equal s s' = true ->
forall a : elt, mem a s = mem a s'
intros; rewrite (equal_2 H); auto.
Qed.

Lemma subset_mem_1:
  (forall a, mem a s=true->mem a s'=true) -> subset s s'=true.s, s', s'':t
x, y, z:elt
(forall a : elt, mem a s = true -> mem a s' = true) ->
subset s s' = true
Proof.s, s', s'':t
x, y, z:elt
(forall a : elt, mem a s = true -> mem a s' = true) ->
subset s s' = true
intros; apply subset_1; unfold Subset; intros a.s, s', s'':t
x, y, z:elt
H:forall a0 : elt,
mem a0 s = true -> mem a0 s' = true
a:elt
In a s -> In a s'
do 2 rewrite mem_iff; auto.
Qed.

Lemma subset_mem_2:
  subset s s'=true -> forall a, mem a s=true -> mem a s'=true.s, s', s'':t
x, y, z:elt
subset s s' = true ->
forall a : elt, mem a s = true -> mem a s' = true
Proof.s, s', s'':t
x, y, z:elt
subset s s' = true ->
forall a : elt, mem a s = true -> mem a s' = true
intros H a; do 2 rewrite <- mem_iff; apply subset_2; auto.
Qed.

Lemma empty_mem: mem x empty=false.s, s', s'':t
x, y, z:elt
mem x empty = false
Proof.s, s', s'':t
x, y, z:elt
mem x empty = false
rewrite <- not_mem_iff; auto with set.
Qed.

Lemma is_empty_equal_empty: is_empty s = equal s empty.s, s', s'':t
x, y, z:elt
is_empty s = equal s empty
Proof.s, s', s'':t
x, y, z:elt
is_empty s = equal s empty
apply bool_1; split; intros.s, s', s'':t
x, y, z:elt
H:is_empty s = true
equal s empty = true
s, s', s'':t
x, y, z:elt
H:equal s empty = true
is_empty s = true
auto with set.s, s', s'':t
x, y, z:elt
H:equal s empty = true
is_empty s = true
rewrite <- is_empty_iff; auto with set.
Qed.

Lemma choose_mem_1: choose s=Some x -> mem x s=true.s, s', s'':t
x, y, z:elt
choose s = Some x -> mem x s = true
Proof.s, s', s'':t
x, y, z:elt
choose s = Some x -> mem x s = true
auto with set.
Qed.

Lemma choose_mem_2: choose s=None -> is_empty s=true.s, s', s'':t
x, y, z:elt
choose s = None -> is_empty s = true
Proof.s, s', s'':t
x, y, z:elt
choose s = None -> is_empty s = true
auto with set.
Qed.

Lemma add_mem_1: mem x (add x s)=true.s, s', s'':t
x, y, z:elt
mem x (add x s) = true
Proof.s, s', s'':t
x, y, z:elt
mem x (add x s) = true
auto with set.
Qed.

Lemma add_mem_2: ~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
apply add_neq_b.
Qed.

Lemma remove_mem_1: mem x (remove x s)=false.s, s', s'':t
x, y, z:elt
mem x (remove x s) = false
Proof.s, s', s'':t
x, y, z:elt
mem x (remove x s) = false
rewrite <- not_mem_iff; auto with set.
Qed.

Lemma remove_mem_2: ~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
apply remove_neq_b.
Qed.

Lemma singleton_equal_add:
  equal (singleton x) (add x empty)=true.s, s', s'':t
x, y, z:elt
equal (singleton x) (add x empty) = true
Proof.s, s', s'':t
x, y, z:elt
equal (singleton x) (add x empty) = true
rewrite (singleton_equal_add x); auto with set.
Qed.

Lemma union_mem:
  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'
apply union_b.
Qed.

Lemma inter_mem:
  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'
apply inter_b.
Qed.

Lemma diff_mem:
  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')
apply diff_b.
Qed.

properties of mem

Lemma mem_3 : ~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
intros; rewrite <- not_mem_iff; auto.
Qed.

Lemma mem_4 : mem x s=false -> ~In x s.s, s', s'':t
x, y, z:elt
mem x s = false -> ~ In x s
Proof.s, s', s'':t
x, y, z:elt
mem x s = false -> ~ In x s
intros; rewrite not_mem_iff; auto.
Qed.

Properties of equal

Lemma equal_refl: equal s s=true.s, s', s'':t
x, y, z:elt
equal s s = true
Proof.s, s', s'':t
x, y, z:elt
equal s s = true
auto with set.
Qed.

Lemma equal_sym: equal s s'=equal s' s.s, s', s'':t
x, y, z:elt
equal s s' = equal s' s
Proof.s, s', s'':t
x, y, z:elt
equal s s' = equal s' s
intros; apply bool_1; do 2 rewrite <- equal_iff; intuition.
Qed.

Lemma equal_trans:
 equal s s'=true -> equal s' s''=true -> equal s s''=true.s, s', s'':t
x, y, z:elt
equal s s' = true ->
equal s' s'' = true -> equal s s'' = true
Proof.s, s', s'':t
x, y, z:elt
equal s s' = true ->
equal s' s'' = true -> equal s s'' = true
intros; rewrite (equal_2 H); auto.
Qed.

Lemma equal_equal:
 equal s s'=true -> equal s s''=equal s' s''.s, s', s'':t
x, y, z:elt
equal s s' = true -> equal s s'' = equal s' s''
Proof.s, s', s'':t
x, y, z:elt
equal s s' = true -> equal s s'' = equal s' s''
intros; rewrite (equal_2 H); auto.
Qed.

Lemma equal_cardinal:
 equal s s'=true -> cardinal s=cardinal s'.s, s', s'':t
x, y, z:elt
equal s s' = true -> cardinal s = cardinal s'
Proof.s, s', s'':t
x, y, z:elt
equal s s' = true -> cardinal s = cardinal s'
auto with set fset.
Qed.

(* Properties of [subset] *)

Lemma subset_refl: subset s s=true.s, s', s'':t
x, y, z:elt
subset s s = true
Proof.s, s', s'':t
x, y, z:elt
subset s s = true
auto with set.
Qed.

Lemma subset_antisym:
 subset s s'=true -> subset s' s=true -> equal s s'=true.s, s', s'':t
x, y, z:elt
subset s s' = true ->
subset s' s = true -> equal s s' = true
Proof.s, s', s'':t
x, y, z:elt
subset s s' = true ->
subset s' s = true -> equal s s' = true
auto with set.
Qed.

Lemma subset_trans:
 subset s s'=true -> subset s' s''=true -> subset s s''=true.s, s', s'':t
x, y, z:elt
subset s s' = true ->
subset s' s'' = true -> subset s s'' = true
Proof.s, s', s'':t
x, y, z:elt
subset s s' = true ->
subset s' s'' = true -> subset s s'' = true
do 3 rewrite <- subset_iff; intros.s, s', s'':t
x, y, z:elt
H:s [<=] s'
H0:s' [<=] s''
s [<=] s''
apply subset_trans with s'; auto.
Qed.

Lemma subset_equal:
 equal s s'=true -> subset s s'=true.s, s', s'':t
x, y, z:elt
equal s s' = true -> subset s s' = true
Proof.s, s', s'':t
x, y, z:elt
equal s s' = true -> subset s s' = true
auto with set.
Qed.

Properties of choose

Lemma choose_mem_3:
 is_empty s=false -> {x:elt|choose s=Some x /\ mem x s=true}.s, s', s'':t
x, y, z:elt
is_empty s = false ->
{x0 : elt | choose s = Some x0 /\ mem x0 s = true}
Proof.s, s', s'':t
x, y, z:elt
is_empty s = false ->
{x0 : elt | choose s = Some x0 /\ mem x0 s = true}
intros.s, s', s'':t
x, y, z:elt
H:is_empty s = false
{x0 : elt | choose s = Some x0 /\ mem x0 s = true}
generalize (@choose_1 s) (@choose_2 s).s, s', s'':t
x, y, z:elt
H:is_empty s = false
(forall x0 : elt, choose s = Some x0 -> In x0 s) ->
(choose s = None -> Empty s) ->
{x0 : elt | choose s = Some x0 /\ mem x0 s = true}
destruct (choose s);intros.s, s', s'':t
x, y, z:elt
H:is_empty s = false
e:elt
H0:forall x0 : elt, Some e = Some x0 -> In x0 s
H1:Some e = None -> Empty s
{x0 : elt | Some e = Some x0 /\ mem x0 s = true}
s, s', s'':t
x, y, z:elt
H:is_empty s = false
H0:forall x0 : elt, None = Some x0 -> In x0 s
H1:None = None -> Empty s
{x0 : elt | None = Some x0 /\ mem x0 s = true}
exists e;auto with set.s, s', s'':t
x, y, z:elt
H:is_empty s = false
H0:forall x0 : elt, None = Some x0 -> In x0 s
H1:None = None -> Empty s
{x0 : elt | None = Some x0 /\ mem x0 s = true}
generalize (H1 Logic.eq_refl); clear H1.s, s', s'':t
x, y, z:elt
H:is_empty s = false
H0:forall x0 : elt, None = Some x0 -> In x0 s
Empty s ->
{x0 : elt | None = Some x0 /\ mem x0 s = true}
intros; rewrite (is_empty_1 H1) in H; discriminate.
Qed.

Lemma choose_mem_4: choose empty=None.s, s', s'':t
x, y, z:elt
choose empty = None
Proof.s, s', s'':t
x, y, z:elt
choose empty = None
generalize (@choose_1 empty).s, s', s'':t
x, y, z:elt
(forall x0 : elt,
 choose empty = Some x0 -> In x0 empty) ->
choose empty = None
case (@choose empty);intros;auto.s, s', s'':t
x, y, z, e:elt
H:forall x0 : elt, Some e = Some x0 -> In x0 empty
Some e = None
elim (@empty_1 e); auto.
Qed.

Properties of add

Lemma add_mem_3:
 mem y s=true -> mem y (add x s)=true.s, s', s'':t
x, y, z:elt
mem y s = true -> mem y (add x s) = true
Proof.s, s', s'':t
x, y, z:elt
mem y s = true -> mem y (add x s) = true
auto with set.
Qed.

Lemma add_equal:
 mem x s=true -> equal (add x s) s=true.s, s', s'':t
x, y, z:elt
mem x s = true -> equal (add x s) s = true
Proof.s, s', s'':t
x, y, z:elt
mem x s = true -> equal (add x s) s = true
auto with set.
Qed.

Properties of remove

Lemma remove_mem_3:
 mem y (remove x s)=true -> mem y s=true.s, s', s'':t
x, y, z:elt
mem y (remove x s) = true -> mem y s = true
Proof.s, s', s'':t
x, y, z:elt
mem y (remove x s) = true -> mem y s = true
rewrite remove_b; intros H;destruct (andb_prop _ _ H); auto.
Qed.

Lemma remove_equal:
 mem x s=false -> equal (remove x s) s=true.s, s', s'':t
x, y, z:elt
mem x s = false -> equal (remove x s) s = true
Proof.s, s', s'':t
x, y, z:elt
mem x s = false -> equal (remove x s) s = true
intros; apply equal_1; apply remove_equal.s, s', s'':t
x, y, z:elt
H:mem x s = false
~ In x s
rewrite not_mem_iff; auto.
Qed.

Lemma add_remove:
 mem x s=true -> equal (add x (remove x s)) s=true.s, s', s'':t
x, y, z:elt
mem x s = true -> equal (add x (remove x s)) s = true
Proof.s, s', s'':t
x, y, z:elt
mem x s = true -> equal (add x (remove x s)) s = true
intros; apply equal_1; apply add_remove; auto with set.
Qed.

Lemma remove_add:
 mem x s=false -> equal (remove x (add x s)) s=true.s, s', s'':t
x, y, z:elt
mem x s = false -> equal (remove x (add x s)) s = true
Proof.s, s', s'':t
x, y, z:elt
mem x s = false -> equal (remove x (add x s)) s = true
intros; apply equal_1; apply remove_add; auto.s, s', s'':t
x, y, z:elt
H:mem x s = false
~ In x s
rewrite not_mem_iff; auto.
Qed.

Properties of is_empty

Lemma is_empty_cardinal: is_empty s = zerob (cardinal s).s, s', s'':t
x, y, z:elt
is_empty s = zerob (cardinal s)
Proof.s, s', s'':t
x, y, z:elt
is_empty s = zerob (cardinal s)
intros; apply bool_1; split; intros.s, s', s'':t
x, y, z:elt
H:is_empty s = true
zerob (cardinal s) = true
s, s', s'':t
x, y, z:elt
H:zerob (cardinal s) = true
is_empty s = true
rewrite MP.cardinal_1; simpl; auto with set.s, s', s'':t
x, y, z:elt
H:zerob (cardinal s) = true
is_empty s = true
assert (cardinal s = 0) by (apply zerob_true_elim; auto).s, s', s'':t
x, y, z:elt
H:zerob (cardinal s) = true
H0:cardinal s = 0
is_empty s = true
auto with set fset.
Qed.

Properties of singleton

Lemma singleton_mem_1: mem x (singleton x)=true.s, s', s'':t
x, y, z:elt
mem x (singleton x) = true
Proof.s, s', s'':t
x, y, z:elt
mem x (singleton x) = true
auto with set.
Qed.

Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false.s, s', s'':t
x, y, z:elt
~ E.eq x y -> mem y (singleton x) = false
Proof.s, s', s'':t
x, y, z:elt
~ E.eq x y -> mem y (singleton x) = false
intros; rewrite singleton_b.s, s', s'':t
x, y, z:elt
H:~ E.eq x y
eqb x y = false
unfold eqb; destruct (E.eq_dec x y); intuition.
Qed.

Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y.s, s', s'':t
x, y, z:elt
mem y (singleton x) = true -> E.eq x y
Proof.s, s', s'':t
x, y, z:elt
mem y (singleton x) = true -> E.eq x y
intros; apply singleton_1; auto with set.
Qed.

Properties of union

Lemma union_sym:
 equal (union s s') (union s' s)=true.s, s', s'':t
x, y, z:elt
equal (union s s') (union s' s) = true
Proof.s, s', s'':t
x, y, z:elt
equal (union s s') (union s' s) = true
auto with set.
Qed.

Lemma union_subset_equal:
 subset s s'=true -> equal (union s s') s'=true.s, s', s'':t
x, y, z:elt
subset s s' = true -> equal (union s s') s' = true
Proof.s, s', s'':t
x, y, z:elt
subset s s' = true -> equal (union s s') s' = true
auto with set.
Qed.

Lemma union_equal_1:
 equal s s'=true-> equal (union s s'') (union s' s'')=true.s, s', s'':t
x, y, z:elt
equal s s' = true ->
equal (union s s'') (union s' s'') = true
Proof.s, s', s'':t
x, y, z:elt
equal s s' = true ->
equal (union s s'') (union s' s'') = true
auto with set.
Qed.

Lemma union_equal_2:
 equal s' s''=true-> equal (union s s') (union s s'')=true.s, s', s'':t
x, y, z:elt
equal s' s'' = true ->
equal (union s s') (union s s'') = true
Proof.s, s', s'':t
x, y, z:elt
equal s' s'' = true ->
equal (union s s') (union s s'') = true
auto with set.
Qed.

Lemma union_assoc:
 equal (union (union s s') s'') (union s (union s' s''))=true.s, s', s'':t
x, y, z:elt
equal (union (union s s') s'')
  (union s (union s' s'')) = true
Proof.s, s', s'':t
x, y, z:elt
equal (union (union s s') s'')
  (union s (union s' s'')) = true
auto with set.
Qed.

Lemma add_union_singleton:
 equal (add x s) (union (singleton x) s)=true.s, s', s'':t
x, y, z:elt
equal (add x s) (union (singleton x) s) = true
Proof.s, s', s'':t
x, y, z:elt
equal (add x s) (union (singleton x) s) = true
auto with set.
Qed.

Lemma union_add:
 equal (union (add x s) s') (add x (union s s'))=true.s, s', s'':t
x, y, z:elt
equal (union (add x s) s') (add x (union s s')) = true
Proof.s, s', s'':t
x, y, z:elt
equal (union (add x s) s') (add x (union s s')) = true
auto with set.
Qed.

(* characterisation of [union] via [subset] *)

Lemma union_subset_1: subset s (union s s')=true.s, s', s'':t
x, y, z:elt
subset s (union s s') = true
Proof.s, s', s'':t
x, y, z:elt
subset s (union s s') = true
auto with set.
Qed.

Lemma union_subset_2: subset s' (union s s')=true.s, s', s'':t
x, y, z:elt
subset s' (union s s') = true
Proof.s, s', s'':t
x, y, z:elt
subset s' (union s s') = true
auto with set.
Qed.

Lemma union_subset_3:
 subset s s''=true -> subset s' s''=true ->
  subset (union s s') s''=true.s, s', s'':t
x, y, z:elt
subset s s'' = true ->
subset s' s'' = true -> subset (union s s') s'' = true
Proof.s, s', s'':t
x, y, z:elt
subset s s'' = true ->
subset s' s'' = true -> subset (union s s') s'' = true
intros; apply subset_1; apply union_subset_3; auto with set.
Qed.

Properties of inter

Lemma inter_sym: equal (inter s s') (inter s' s)=true.s, s', s'':t
x, y, z:elt
equal (inter s s') (inter s' s) = true
Proof.s, s', s'':t
x, y, z:elt
equal (inter s s') (inter s' s) = true
auto with set.
Qed.

Lemma inter_subset_equal:
 subset s s'=true -> equal (inter s s') s=true.s, s', s'':t
x, y, z:elt
subset s s' = true -> equal (inter s s') s = true
Proof.s, s', s'':t
x, y, z:elt
subset s s' = true -> equal (inter s s') s = true
auto with set.
Qed.

Lemma inter_equal_1:
 equal s s'=true -> equal (inter s s'') (inter s' s'')=true.s, s', s'':t
x, y, z:elt
equal s s' = true ->
equal (inter s s'') (inter s' s'') = true
Proof.s, s', s'':t
x, y, z:elt
equal s s' = true ->
equal (inter s s'') (inter s' s'') = true
auto with set.
Qed.

Lemma inter_equal_2:
 equal s' s''=true -> equal (inter s s') (inter s s'')=true.s, s', s'':t
x, y, z:elt
equal s' s'' = true ->
equal (inter s s') (inter s s'') = true
Proof.s, s', s'':t
x, y, z:elt
equal s' s'' = true ->
equal (inter s s') (inter s s'') = true
auto with set.
Qed.

Lemma inter_assoc:
 equal (inter (inter s s') s'') (inter s (inter s' s''))=true.s, s', s'':t
x, y, z:elt
equal (inter (inter s s') s'')
  (inter s (inter s' s'')) = true
Proof.s, s', s'':t
x, y, z:elt
equal (inter (inter s s') s'')
  (inter s (inter s' s'')) = true
auto with set.
Qed.

Lemma union_inter_1:
 equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))=true.s, s', s'':t
x, y, z:elt
equal (inter (union s s') s'')
  (union (inter s s'') (inter s' s'')) = true
Proof.s, s', s'':t
x, y, z:elt
equal (inter (union s s') s'')
  (union (inter s s'') (inter s' s'')) = true
auto with set.
Qed.

Lemma union_inter_2:
 equal (union (inter s s') s'') (inter (union s s'') (union s' s''))=true.s, s', s'':t
x, y, z:elt
equal (union (inter s s') s'')
  (inter (union s s'') (union s' s'')) = true
Proof.s, s', s'':t
x, y, z:elt
equal (union (inter s s') s'')
  (inter (union s s'') (union s' s'')) = true
auto with set.
Qed.

Lemma inter_add_1: mem x s'=true ->
 equal (inter (add x s) s') (add x (inter s s'))=true.s, s', s'':t
x, y, z:elt
mem x s' = true ->
equal (inter (add x s) s') (add x (inter s s')) = true
Proof.s, s', s'':t
x, y, z:elt
mem x s' = true ->
equal (inter (add x s) s') (add x (inter s s')) = true
auto with set.
Qed.

Lemma inter_add_2: mem x s'=false ->
 equal (inter (add x s) s') (inter s s')=true.s, s', s'':t
x, y, z:elt
mem x s' = false ->
equal (inter (add x s) s') (inter s s') = true
Proof.s, s', s'':t
x, y, z:elt
mem x s' = false ->
equal (inter (add x s) s') (inter s s') = true
intros; apply equal_1; apply inter_add_2.s, s', s'':t
x, y, z:elt
H:mem x s' = false
~ In x s'
rewrite not_mem_iff; auto.
Qed.

(* characterisation of [union] via [subset] *)

Lemma inter_subset_1: subset (inter s s') s=true.s, s', s'':t
x, y, z:elt
subset (inter s s') s = true
Proof.s, s', s'':t
x, y, z:elt
subset (inter s s') s = true
auto with set.
Qed.

Lemma inter_subset_2: subset (inter s s') s'=true.s, s', s'':t
x, y, z:elt
subset (inter s s') s' = true
Proof.s, s', s'':t
x, y, z:elt
subset (inter s s') s' = true
auto with set.
Qed.

Lemma inter_subset_3:
 subset s'' s=true -> subset s'' s'=true ->
  subset s'' (inter s s')=true.s, s', s'':t
x, y, z:elt
subset s'' s = true ->
subset s'' s' = true -> subset s'' (inter s s') = true
Proof.s, s', s'':t
x, y, z:elt
subset s'' s = true ->
subset s'' s' = true -> subset s'' (inter s s') = true
intros; apply subset_1; apply inter_subset_3; auto with set.
Qed.

Properties of diff

Lemma diff_subset: subset (diff s s') s=true.s, s', s'':t
x, y, z:elt
subset (diff s s') s = true
Proof.s, s', s'':t
x, y, z:elt
subset (diff s s') s = true
auto with set.
Qed.

Lemma diff_subset_equal:
 subset s s'=true -> equal (diff s s') empty=true.s, s', s'':t
x, y, z:elt
subset s s' = true -> equal (diff s s') empty = true
Proof.s, s', s'':t
x, y, z:elt
subset s s' = true -> equal (diff s s') empty = true
auto with set.
Qed.

Lemma remove_inter_singleton:
 equal (remove x s) (diff s (singleton x))=true.s, s', s'':t
x, y, z:elt
equal (remove x s) (diff s (singleton x)) = true
Proof.s, s', s'':t
x, y, z:elt
equal (remove x s) (diff s (singleton x)) = true
auto with set.
Qed.

Lemma diff_inter_empty:
 equal (inter (diff s s') (inter s s')) empty=true.s, s', s'':t
x, y, z:elt
equal (inter (diff s s') (inter s s')) empty = true
Proof.s, s', s'':t
x, y, z:elt
equal (inter (diff s s') (inter s s')) empty = true
auto with set.
Qed.

Lemma diff_inter_all:
 equal (union (diff s s') (inter s s')) s=true.s, s', s'':t
x, y, z:elt
equal (union (diff s s') (inter s s')) s = true
Proof.s, s', s'':t
x, y, z:elt
equal (union (diff s s') (inter s s')) s = true
auto with set.
Qed.

End BasicProperties.

Hint Immediate empty_mem is_empty_equal_empty add_mem_1
   remove_mem_1 singleton_equal_add union_mem inter_mem
   diff_mem equal_sym add_remove remove_add : set.
Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
   choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal
   subset_refl subset_equal subset_antisym
   add_mem_3 add_equal remove_mem_3 remove_equal : set.

General recursion principle

Lemma set_rec:  forall (P:t->Type),
 (forall s s', equal s s'=true -> P s -> P s') ->
 (forall s x, mem x s=false -> P s -> P (add x s)) ->
 P empty -> forall s, P s.forall P : t -> Type,
(forall s s' : t, equal s s' = true -> P s -> P s') ->
(forall (s : t) (x : elt),
 mem x s = false -> P s -> P (add x s)) ->
P empty -> forall s : t, P s
Proof.forall P : t -> Type,
(forall s s' : t, equal s s' = true -> P s -> P s') ->
(forall (s : t) (x : elt),
 mem x s = false -> P s -> P (add x s)) ->
P empty -> forall s : t, P s
intros.P:t -> Type
X:forall s0 s' : t,
equal s0 s' = true -> P s0 -> P s'
X0:forall (s0 : t) (x : elt),
mem x s0 = false -> P s0 -> P (add x s0)
X1:P empty
s:t
P s
apply set_induction; auto; intros.P:t -> Type
X:forall s1 s' : t,
equal s1 s' = true -> P s1 -> P s'
X0:forall (s1 : t) (x : elt),
mem x s1 = false -> P s1 -> P (add x s1)
X1:P empty
s, s0:t
H:Empty s0
P s0
P:t -> Type
X:forall s1 s'0 : t,
equal s1 s'0 = true -> P s1 -> P s'0
X0:forall (s1 : t) (x0 : elt),
mem x0 s1 = false -> P s1 -> P (add x0 s1)
X1:P empty
s, s0, s':t
X2:P s0
x:elt
H:~ In x s0
H0:MP.Add x s0 s'
P s'
apply X with empty; auto with set.P:t -> Type
X:forall s1 s'0 : t,
equal s1 s'0 = true -> P s1 -> P s'0
X0:forall (s1 : t) (x0 : elt),
mem x0 s1 = false -> P s1 -> P (add x0 s1)
X1:P empty
s, s0, s':t
X2:P s0
x:elt
H:~ In x s0
H0:MP.Add x s0 s'
P s'
apply X with (add x s0); auto with set.P:t -> Type
X:forall s1 s'0 : t,
equal s1 s'0 = true -> P s1 -> P s'0
X0:forall (s1 : t) (x0 : elt),
mem x0 s1 = false -> P s1 -> P (add x0 s1)
X1:P empty
s, s0, s':t
X2:P s0
x:elt
H:~ In x s0
H0:MP.Add x s0 s'
equal (add x s0) s' = true
P:t -> Type
X:forall s1 s'0 : t,
equal s1 s'0 = true -> P s1 -> P s'0
X0:forall (s1 : t) (x0 : elt),
mem x0 s1 = false -> P s1 -> P (add x0 s1)
X1:P empty
s, s0, s':t
X2:P s0
x:elt
H:~ In x s0
H0:MP.Add x s0 s'
P (add x s0)
apply equal_1; intro a; rewrite add_iff; rewrite (H0 a); tauto.P:t -> Type
X:forall s1 s'0 : t,
equal s1 s'0 = true -> P s1 -> P s'0
X0:forall (s1 : t) (x0 : elt),
mem x0 s1 = false -> P s1 -> P (add x0 s1)
X1:P empty
s, s0, s':t
X2:P s0
x:elt
H:~ In x s0
H0:MP.Add x s0 s'
P (add x s0)
apply X0; auto with set; apply mem_3; auto.
Qed.

Properties of fold

Lemma exclusive_set : forall s s' x,
 ~(In x s/\In x s') <-> mem x s && mem x s'=false.forall (s s' : t) (x : elt),
~ (In x s /\ In x s') <-> mem x s && mem x s' = false
Proof.forall (s s' : t) (x : elt),
~ (In x s /\ In x s') <-> mem x s && mem x s' = false
intros; do 2 rewrite mem_iff.s, s':t
x:elt
~ (mem x s = true /\ mem x s' = true) <->
mem x s && mem x s' = false
destruct (mem x s); destruct (mem x s'); intuition.
Qed.

Section Fold.
Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
Variables (i:A).
Variables (s s':t)(x:elt).

Lemma fold_empty: (fold f empty i) = i.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
fold f empty i = i
Proof.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
fold f empty i = i
apply fold_empty; auto.
Qed.

Lemma fold_equal:
 equal s s'=true -> eqA (fold f s i) (fold f s' i).A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
equal s s' = true -> eqA (fold f s i) (fold f s' i)
Proof.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
equal s s' = true -> eqA (fold f s i) (fold f s' i)
intros; apply fold_equal with (eqA:=eqA); auto with set.
Qed.

Lemma fold_add:
 mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)).A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
mem x s = false ->
eqA (fold f (add x s) i) (f x (fold f s i))
Proof.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
mem x s = false ->
eqA (fold f (add x s) i) (f x (fold f s i))
intros; apply fold_add with (eqA:=eqA); auto.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
H:mem x s = false
~ In x s
rewrite not_mem_iff; auto.
Qed.

Lemma add_fold:
  mem x s=true -> eqA (fold f (add x s) i) (fold f s i).A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
mem x s = true ->
eqA (fold f (add x s) i) (fold f s i)
Proof.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
mem x s = true ->
eqA (fold f (add x s) i) (fold f s i)
intros; apply add_fold with (eqA:=eqA); auto with set.
Qed.

Lemma remove_fold_1:
 mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i).A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
mem x s = true ->
eqA (f x (fold f (remove x s) i)) (fold f s i)
Proof.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
mem x s = true ->
eqA (f x (fold f (remove x s) i)) (fold f s i)
intros; apply remove_fold_1 with (eqA:=eqA); auto with set.
Qed.

Lemma remove_fold_2:
 mem x s=false -> eqA (fold f (remove x s) i) (fold f s i).A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
mem x s = false ->
eqA (fold f (remove x s) i) (fold f s i)
Proof.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
mem x s = false ->
eqA (fold f (remove x s) i) (fold f s i)
intros; apply remove_fold_2 with (eqA:=eqA); auto.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
H:mem x s = false
~ In x s
rewrite not_mem_iff; auto.
Qed.

Lemma fold_union:
 (forall x, mem x s && mem x s'=false) ->
 eqA (fold f (union s s') i) (fold f s (fold f s' i)).A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
(forall x0 : elt, mem x0 s && mem x0 s' = false) ->
eqA (fold f (union s s') i) (fold f s (fold f s' i))
Proof.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
(forall x0 : elt, mem x0 s && mem x0 s' = false) ->
eqA (fold f (union s s') i) (fold f s (fold f s' i))
intros; apply fold_union with (eqA:=eqA); auto.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
Ass:transpose eqA f
i:A
s, s':t
x:elt
H:forall x0 : elt, mem x0 s && mem x0 s' = false
forall x0 : elt, ~ (In x0 s /\ In x0 s')
intros; rewrite exclusive_set; auto.
Qed.

End Fold.

Properties of cardinal

Lemma add_cardinal_1:
 forall s x, mem x s=true -> cardinal (add x s)=cardinal s.forall (s : t) (x : elt),
mem x s = true -> cardinal (add x s) = cardinal s
Proof.forall (s : t) (x : elt),
mem x s = true -> cardinal (add x s) = cardinal s
auto with set fset.
Qed.

Lemma add_cardinal_2:
 forall s x, mem x s=false -> cardinal (add x s)=S (cardinal s).forall (s : t) (x : elt),
mem x s = false -> cardinal (add x s) = S (cardinal s)
Proof.forall (s : t) (x : elt),
mem x s = false -> cardinal (add x s) = S (cardinal s)
intros; apply add_cardinal_2; auto.s:t
x:elt
H:mem x s = false
~ In x s
rewrite not_mem_iff; auto.
Qed.

Lemma remove_cardinal_1:
 forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s.forall (s : t) (x : elt),
mem x s = true ->
S (cardinal (remove x s)) = cardinal s
Proof.forall (s : t) (x : elt),
mem x s = true ->
S (cardinal (remove x s)) = cardinal s
intros; apply remove_cardinal_1; auto with set.
Qed.

Lemma remove_cardinal_2:
 forall s x, mem x s=false -> cardinal (remove x s)=cardinal s.forall (s : t) (x : elt),
mem x s = false -> cardinal (remove x s) = cardinal s
Proof.forall (s : t) (x : elt),
mem x s = false -> cardinal (remove x s) = cardinal s
intros; apply Equal_cardinal; apply equal_2; auto with set.
Qed.

Lemma union_cardinal:
 forall s s', (forall x, mem x s && mem x s'=false) ->
 cardinal (union s s')=cardinal s+cardinal s'.forall s s' : t,
(forall x : elt, mem x s && mem x s' = false) ->
cardinal (union s s') = cardinal s + cardinal s'
Proof.forall s s' : t,
(forall x : elt, mem x s && mem x s' = false) ->
cardinal (union s s') = cardinal s + cardinal s'
intros; apply union_cardinal; auto; intros.s, s':t
H:forall x0 : elt, mem x0 s && mem x0 s' = false
x:elt
~ (In x s /\ In x s')
rewrite exclusive_set; auto.
Qed.

Lemma subset_cardinal:
 forall s s', subset s s'=true -> cardinal s<=cardinal s'.forall s s' : t,
subset s s' = true -> cardinal s <= cardinal s'
Proof.forall s s' : t,
subset s s' = true -> cardinal s <= cardinal s'
intros; apply subset_cardinal; auto with set.
Qed.

Section Bool.

Properties of filter

Variable f:elt->bool.
Variable Comp: Proper (E.eq==>Logic.eq) f.

Let Comp' : Proper (E.eq==>Logic.eq) (fun x =>negb (f x)).f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Proper (E.eq ==> Logic.eq) (fun x : E.t => negb (f x))
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Proper (E.eq ==> Logic.eq) (fun x : E.t => negb (f x))
repeat red; intros; f_equal; auto.
Qed.

Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall (s : t) (x : elt),
mem x (filter f s) = mem x s && f x
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall (s : t) (x : elt),
mem x (filter f s) = mem x s && f x
intros; apply filter_b; auto.
Qed.

Lemma for_all_filter:
 forall s, for_all f s=is_empty (filter (fun x => negb (f x)) s).f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s : t,
for_all f s =
is_empty (filter (fun x : elt => negb (f x)) s)
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s : t,
for_all f s =
is_empty (filter (fun x : elt => negb (f x)) s)
intros; apply bool_1; split; intros.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:for_all f s = true
is_empty (filter (fun x : elt => negb (f x)) s) = true
f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:is_empty (filter (fun x : elt => negb (f x)) s) =
true
for_all f s = true
apply is_empty_1.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:for_all f s = true
Empty (filter (fun x : elt => negb (f x)) s)
f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:is_empty (filter (fun x : elt => negb (f x)) s) =
true
for_all f s = true
unfold Empty; intros.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:for_all f s = true
a:elt
~ In a (filter (fun x : elt => negb (f x)) s)
f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:is_empty (filter (fun x : elt => negb (f x)) s) =
true
for_all f s = true
rewrite filter_iff; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:for_all f s = true
a:elt
~ (In a s /\ negb (f a) = true)
f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:is_empty (filter (fun x : elt => negb (f x)) s) =
true
for_all f s = true
red; destruct 1.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:for_all f s = true
a:elt
H0:In a s
H1:negb (f a) = true
False
f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:is_empty (filter (fun x : elt => negb (f x)) s) =
true
for_all f s = true
rewrite <- (@for_all_iff s f) in H; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:For_all (fun x : elt => f x = true) s
a:elt
H0:In a s
H1:negb (f a) = true
False
f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:is_empty (filter (fun x : elt => negb (f x)) s) =
true
for_all f s = true
rewrite (H a H0) in H1; discriminate.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:is_empty (filter (fun x : elt => negb (f x)) s) =
true
for_all f s = true
apply for_all_1; auto; red; intros.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
H:is_empty (filter (fun x0 : elt => negb (f x0)) s) =
true
x:elt
H0:In x s
f x = true
revert H; rewrite <- is_empty_iff.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H0:In x s
Empty (filter (fun x0 : elt => negb (f x0)) s) ->
f x = true
unfold Empty; intro H; generalize (H x); clear H.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H0:In x s
~ In x (filter (fun x0 : elt => negb (f x0)) s) ->
f x = true
rewrite filter_iff; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H0:In x s
~ (In x s /\ negb (f x) = true) -> f x = true
destruct (f x); auto.
Qed.

Lemma exists_filter :
 forall s, exists_ f s=negb (is_empty (filter f s)).f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s : t,
exists_ f s = negb (is_empty (filter f s))
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s : t,
exists_ f s = negb (is_empty (filter f s))
intros; apply bool_1; split; intros.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:exists_ f s = true
negb (is_empty (filter f s)) = true
f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:negb (is_empty (filter f s)) = true
exists_ f s = true
destruct (exists_2 Comp H) as (a,(Ha1,Ha2)).f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:exists_ f s = true
a:elt
Ha1:In a s
Ha2:f a = true
negb (is_empty (filter f s)) = true
f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:negb (is_empty (filter f s)) = true
exists_ f s = true
apply bool_6.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:exists_ f s = true
a:elt
Ha1:In a s
Ha2:f a = true
is_empty (filter f s) <> true
f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:negb (is_empty (filter f s)) = true
exists_ f s = true
red; intros; apply (@is_empty_2 _ H0 a); auto with set.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:negb (is_empty (filter f s)) = true
exists_ f s = true
generalize (@choose_1 (filter f s)) (@choose_2 (filter f s)).f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:negb (is_empty (filter f s)) = true
(forall x : elt,
 choose (filter f s) = Some x -> In x (filter f s)) ->
(choose (filter f s) = None -> Empty (filter f s)) ->
exists_ f s = true
destruct (choose (filter f s)).f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:negb (is_empty (filter f s)) = true
e:elt
(forall x : elt, Some e = Some x -> In x (filter f s)) ->
(Some e = None -> Empty (filter f s)) ->
exists_ f s = true
f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:negb (is_empty (filter f s)) = true
(forall x : elt, None = Some x -> In x (filter f s)) ->
(None = None -> Empty (filter f s)) ->
exists_ f s = true
intros H0 _; apply exists_1; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:negb (is_empty (filter f s)) = true
e:elt
H0:forall x : elt,
Some e = Some x -> In x (filter f s)
Exists (fun x : elt => f x = true) s
f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:negb (is_empty (filter f s)) = true
(forall x : elt, None = Some x -> In x (filter f s)) ->
(None = None -> Empty (filter f s)) ->
exists_ f s = true
exists e; generalize (H0 e); rewrite filter_iff; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:negb (is_empty (filter f s)) = true
(forall x : elt, None = Some x -> In x (filter f s)) ->
(None = None -> Empty (filter f s)) ->
exists_ f s = true
intros _ H0.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:negb (is_empty (filter f s)) = true
H0:None = None -> Empty (filter f s)
exists_ f s = true
rewrite (is_empty_1 (H0 Logic.eq_refl)) in H; auto; discriminate.
Qed.

Lemma partition_filter_1:
 forall s, equal (fst (partition f s)) (filter f s)=true.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s : t,
equal (fst (partition f s)) (filter f s) = true
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s : t,
equal (fst (partition f s)) (filter f s) = true
auto with set.
Qed.

Lemma partition_filter_2:
 forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s : t,
equal (snd (partition f s))
  (filter (fun x : elt => negb (f x)) s) = true
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s : t,
equal (snd (partition f s))
  (filter (fun x : elt => negb (f x)) s) = true
auto with set.
Qed.

Lemma filter_add_1 : forall s x, f x = true ->
 filter f (add x s) [=] add x (filter f s).f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall (s : t) (x : elt),
f x = true ->
filter f (add x s) [=] add x (filter f s)
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall (s : t) (x : elt),
f x = true ->
filter f (add x s) [=] add x (filter f s)
red; intros; set_iff; do 2 (rewrite filter_iff; auto); set_iff.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:f x = true
a:elt
(E.eq x a \/ In a s) /\ f a = true <->
E.eq x a \/ In a s /\ f a = true
intuition.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:f x = true
a:elt
H1:E.eq x a
f a = true
rewrite <- H; apply Comp; auto.
Qed.

Lemma filter_add_2 : forall s x, f x = false ->
 filter f (add x s) [=] filter f s.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall (s : t) (x : elt),
f x = false -> filter f (add x s) [=] filter f s
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall (s : t) (x : elt),
f x = false -> filter f (add x s) [=] filter f s
red; intros; do 2 (rewrite filter_iff; auto); set_iff.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:f x = false
a:elt
(E.eq x a \/ In a s) /\ f a = true <->
In a s /\ f a = true
intuition.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:f x = false
a:elt
H2:f a = true
H0:E.eq x a
In a s
assert (f x = f a) by (apply Comp; auto).f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:f x = false
a:elt
H2:f a = true
H0:E.eq x a
H1:f x = f a
In a s
rewrite H in H1; rewrite H2 in H1; discriminate.
Qed.

Lemma add_filter_1 : forall s s' x,
 f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')).f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall (s s' : t) (x : elt),
f x = true ->
Add x s s' -> Add x (filter f s) (filter f s')
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall (s s' : t) (x : elt),
f x = true ->
Add x s s' -> Add x (filter f s) (filter f s')
unfold Add, MP.Add; intros.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s, s':t
x:elt
H:f x = true
H0:forall y0 : elt,
In y0 s' <-> E.eq x y0 \/ In y0 s
y:elt
In y (filter f s') <-> E.eq x y \/ In y (filter f s)
repeat rewrite filter_iff; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s, s':t
x:elt
H:f x = true
H0:forall y0 : elt,
In y0 s' <-> E.eq x y0 \/ In y0 s
y:elt
In y s' /\ f y = true <->
E.eq x y \/ In y s /\ f y = true
rewrite H0; clear H0.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s, s':t
x:elt
H:f x = true
y:elt
(E.eq x y \/ In y s) /\ f y = true <->
E.eq x y \/ In y s /\ f y = true
assert (E.eq x y -> f y = true) by
 (intro H0; rewrite <- (Comp _ _ H0); auto).f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s, s':t
x:elt
H:f x = true
y:elt
H0:E.eq x y -> f y = true
(E.eq x y \/ In y s) /\ f y = true <->
E.eq x y \/ In y s /\ f y = true
tauto.
Qed.

Lemma add_filter_2 : forall s s' x,
 f x=false -> (Add x s s') -> filter f s [=] filter f s'.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall (s s' : t) (x : elt),
f x = false ->
Add x s s' -> filter f s [=] filter f s'
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall (s s' : t) (x : elt),
f x = false ->
Add x s s' -> filter f s [=] filter f s'
unfold Add, MP.Add, Equal; intros.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s, s':t
x:elt
H:f x = false
H0:forall y : elt, In y s' <-> E.eq x y \/ In y s
a:elt
In a (filter f s) <-> In a (filter f s')
repeat rewrite filter_iff; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s, s':t
x:elt
H:f x = false
H0:forall y : elt, In y s' <-> E.eq x y \/ In y s
a:elt
In a s /\ f a = true <-> In a s' /\ f a = true
rewrite H0; clear H0.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s, s':t
x:elt
H:f x = false
a:elt
In a s /\ f a = true <->
(E.eq x a \/ In a s) /\ f a = true
assert (f a = true -> ~E.eq x a).f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s, s':t
x:elt
H:f x = false
a:elt
f a = true -> ~ E.eq x a
f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s, s':t
x:elt
H:f x = false
a:elt
H0:f a = true -> ~ E.eq x a
In a s /\ f a = true <->
(E.eq x a \/ In a s) /\ f a = true
 intros H0 H1.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s, s':t
x:elt
H:f x = false
a:elt
H0:f a = true
H1:E.eq x a
False
f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s, s':t
x:elt
H:f x = false
a:elt
H0:f a = true -> ~ E.eq x a
In a s /\ f a = true <->
(E.eq x a \/ In a s) /\ f a = true
 rewrite (Comp _ _ H1) in H.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s, s':t
x, a:elt
H:f a = false
H0:f a = true
H1:E.eq x a
False
f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s, s':t
x:elt
H:f x = false
a:elt
H0:f a = true -> ~ E.eq x a
In a s /\ f a = true <->
(E.eq x a \/ In a s) /\ f a = true
 rewrite H in H0; discriminate.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s, s':t
x:elt
H:f x = false
a:elt
H0:f a = true -> ~ E.eq x a
In a s /\ f a = true <->
(E.eq x a \/ In a s) /\ f a = true
tauto.
Qed.

Lemma union_filter: forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) ->
  forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall f0 g : E.t -> bool,
compat_bool E.eq f0 ->
compat_bool E.eq g ->
forall s : t,
union (filter f0 s) (filter g s) [=]
filter (fun x : elt => f0 x || g x) s
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall f0 g : E.t -> bool,
compat_bool E.eq f0 ->
compat_bool E.eq g ->
forall s : t,
union (filter f0 s) (filter g s) [=]
filter (fun x : elt => f0 x || g x) s
clear Comp' Comp f.forall f g : E.t -> bool,
compat_bool E.eq f ->
compat_bool E.eq g ->
forall s : t,
union (filter f s) (filter g s) [=]
filter (fun x : elt => f x || g x) s
intros.f, g:E.t -> bool
H:compat_bool E.eq f
H0:compat_bool E.eq g
s:t
union (filter f s) (filter g s) [=]
filter (fun x : elt => f x || g x) s
assert (compat_bool E.eq (fun x => orb (f x) (g x))).f, g:E.t -> bool
H:compat_bool E.eq f
H0:compat_bool E.eq g
s:t
compat_bool E.eq (fun x : E.t => f x || g x)
f, g:E.t -> bool
H:compat_bool E.eq f
H0:compat_bool E.eq g
s:t
H1:compat_bool E.eq (fun x : E.t => f x || g x)
union (filter f s) (filter g s) [=]
filter (fun x : elt => f x || g x) s
  unfold compat_bool, Proper, respectful; intros.f, g:E.t -> bool
H:compat_bool E.eq f
H0:compat_bool E.eq g
s:t
x, y:E.t
H1:E.eq x y
f x || g x = f y || g y
f, g:E.t -> bool
H:compat_bool E.eq f
H0:compat_bool E.eq g
s:t
H1:compat_bool E.eq (fun x : E.t => f x || g x)
union (filter f s) (filter g s) [=]
filter (fun x : elt => f x || g x) s
  rewrite (H x y H1);  rewrite (H0 x y H1); auto.f, g:E.t -> bool
H:compat_bool E.eq f
H0:compat_bool E.eq g
s:t
H1:compat_bool E.eq (fun x : E.t => f x || g x)
union (filter f s) (filter g s) [=]
filter (fun x : elt => f x || g x) s
unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto.f, g:E.t -> bool
H:compat_bool E.eq f
H0:compat_bool E.eq g
s:t
H1:compat_bool E.eq (fun x : E.t => f x || g x)
a:elt
In a s /\ f a = true \/ In a s /\ g a = true <->
In a s /\ f a || g a = true
assert (f a || g a = true <-> f a = true \/ g a = true).f, g:E.t -> bool
H:compat_bool E.eq f
H0:compat_bool E.eq g
s:t
H1:compat_bool E.eq (fun x : E.t => f x || g x)
a:elt
f a || g a = true <-> f a = true \/ g a = true
f, g:E.t -> bool
H:compat_bool E.eq f
H0:compat_bool E.eq g
s:t
H1:compat_bool E.eq (fun x : E.t => f x || g x)
a:elt
H2:f a || g a = true <-> f a = true \/ g a = true
In a s /\ f a = true \/ In a s /\ g a = true <->
In a s /\ f a || g a = true
  split; auto with bool.f, g:E.t -> bool
H:compat_bool E.eq f
H0:compat_bool E.eq g
s:t
H1:compat_bool E.eq (fun x : E.t => f x || g x)
a:elt
f a || g a = true -> f a = true \/ g a = true
f, g:E.t -> bool
H:compat_bool E.eq f
H0:compat_bool E.eq g
s:t
H1:compat_bool E.eq (fun x : E.t => f x || g x)
a:elt
H2:f a || g a = true <-> f a = true \/ g a = true
In a s /\ f a = true \/ In a s /\ g a = true <->
In a s /\ f a || g a = true
  intro H3; destruct (orb_prop _ _ H3); auto.f, g:E.t -> bool
H:compat_bool E.eq f
H0:compat_bool E.eq g
s:t
H1:compat_bool E.eq (fun x : E.t => f x || g x)
a:elt
H2:f a || g a = true <-> f a = true \/ g a = true
In a s /\ f a = true \/ In a s /\ g a = true <->
In a s /\ f a || g a = true
tauto.
Qed.

Lemma filter_union: forall s s', filter f (union s s') [=] union (filter f s) (filter f s').f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s s' : t,
filter f (union s s') [=]
union (filter f s) (filter f s')
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s s' : t,
filter f (union s s') [=]
union (filter f s) (filter f s')
unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto; set_iff; tauto.
Qed.

Properties of for_all

Lemma for_all_mem_1: forall s,
 (forall x, (mem x s)=true->(f x)=true) -> (for_all f s)=true.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s : t,
(forall x : elt, mem x s = true -> f x = true) ->
for_all f s = true
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s : t,
(forall x : elt, mem x s = true -> f x = true) ->
for_all f s = true
intros.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:forall x : elt, mem x s = true -> f x = true
for_all f s = true
rewrite for_all_filter; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:forall x : elt, mem x s = true -> f x = true
is_empty (filter (fun x : elt => negb (f x)) s) = true
rewrite is_empty_equal_empty.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:forall x : elt, mem x s = true -> f x = true
equal (filter (fun x : elt => negb (f x)) s) empty =
true
apply equal_mem_1;intros.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:forall x : elt, mem x s = true -> f x = true
a:elt
mem a (filter (fun x : elt => negb (f x)) s) =
mem a empty
rewrite filter_b; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:forall x : elt, mem x s = true -> f x = true
a:elt
mem a s && negb (f a) = mem a empty
rewrite empty_mem.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:forall x : elt, mem x s = true -> f x = true
a:elt
mem a s && negb (f a) = false
generalize (H a); case (mem a s);intros;auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:forall x : elt, mem x s = true -> f x = true
a:elt
H0:true = true -> f a = true
true && negb (f a) = false
rewrite H0;auto.
Qed.

Lemma for_all_mem_2: forall s,
 (for_all f s)=true -> forall x,(mem x s)=true -> (f x)=true.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s : t,
for_all f s = true ->
forall x : elt, mem x s = true -> f x = true
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s : t,
for_all f s = true ->
forall x : elt, mem x s = true -> f x = true
intros.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
H:for_all f s = true
x:elt
H0:mem x s = true
f x = true
rewrite for_all_filter in H; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
H:is_empty (filter (fun x0 : elt => negb (f x0)) s) =
true
x:elt
H0:mem x s = true
f x = true
rewrite is_empty_equal_empty in H.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
H:equal (filter (fun x0 : elt => negb (f x0)) s)
  empty = true
x:elt
H0:mem x s = true
f x = true
generalize (equal_mem_2 _ _ H x).f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
H:equal (filter (fun x0 : elt => negb (f x0)) s)
  empty = true
x:elt
H0:mem x s = true
mem x (filter (fun x0 : elt => negb (f x0)) s) =
mem x empty -> f x = true
rewrite filter_b; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
H:equal (filter (fun x0 : elt => negb (f x0)) s)
  empty = true
x:elt
H0:mem x s = true
mem x s && negb (f x) = mem x empty -> f x = true
rewrite empty_mem.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
H:equal (filter (fun x0 : elt => negb (f x0)) s)
  empty = true
x:elt
H0:mem x s = true
mem x s && negb (f x) = false -> f x = true
rewrite H0; simpl;intros.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
H:equal (filter (fun x0 : elt => negb (f x0)) s)
  empty = true
x:elt
H0:mem x s = true
H1:negb (f x) = false
f x = true
rewrite <- negb_false_iff; auto.
Qed.

Lemma for_all_mem_3:
 forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall (s : t) (x : elt),
mem x s = true -> f x = false -> for_all f s = false
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall (s : t) (x : elt),
mem x s = true -> f x = false -> for_all f s = false
intros.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:mem x s = true
H0:f x = false
for_all f s = false
apply (bool_eq_ind (for_all f s));intros;auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:mem x s = true
H0:f x = false
H1:for_all f s = true
true = false
rewrite for_all_filter in H1; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:mem x s = true
H0:f x = false
H1:is_empty (filter (fun x0 : elt => negb (f x0)) s) =
true
true = false
rewrite is_empty_equal_empty in H1.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:mem x s = true
H0:f x = false
H1:equal (filter (fun x0 : elt => negb (f x0)) s)
  empty = true
true = false
generalize (equal_mem_2 _ _ H1 x).f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:mem x s = true
H0:f x = false
H1:equal (filter (fun x0 : elt => negb (f x0)) s)
  empty = true
mem x (filter (fun x0 : elt => negb (f x0)) s) =
mem x empty -> true = false
rewrite filter_b; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:mem x s = true
H0:f x = false
H1:equal (filter (fun x0 : elt => negb (f x0)) s)
  empty = true
mem x s && negb (f x) = mem x empty -> true = false
rewrite empty_mem.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:mem x s = true
H0:f x = false
H1:equal (filter (fun x0 : elt => negb (f x0)) s)
  empty = true
mem x s && negb (f x) = false -> true = false
rewrite H.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:mem x s = true
H0:f x = false
H1:equal (filter (fun x0 : elt => negb (f x0)) s)
  empty = true
true && negb (f x) = false -> true = false
rewrite H0.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:mem x s = true
H0:f x = false
H1:equal (filter (fun x0 : elt => negb (f x0)) s)
  empty = true
true && negb false = false -> true = false
simpl;auto.
Qed.

Lemma for_all_mem_4:
 forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false}.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s : t,
for_all f s = false ->
{x : elt | mem x s = true /\ f x = false}
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s : t,
for_all f s = false ->
{x : elt | mem x s = true /\ f x = false}
intros.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:for_all f s = false
{x : elt | mem x s = true /\ f x = false}
rewrite for_all_filter in H; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
H:is_empty (filter (fun x : elt => negb (f x)) s) =
false
{x : elt | mem x s = true /\ f x = false}
destruct (choose_mem_3 _ H) as (x,(H0,H1));intros.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
H:is_empty (filter (fun x0 : elt => negb (f x0)) s) =
false
x:elt
H0:choose (filter (fun x0 : elt => negb (f x0)) s) =
Some x
H1:mem x (filter (fun x0 : elt => negb (f x0)) s) =
true
{x0 : elt | mem x0 s = true /\ f x0 = false}
exists x.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
H:is_empty (filter (fun x0 : elt => negb (f x0)) s) =
false
x:elt
H0:choose (filter (fun x0 : elt => negb (f x0)) s) =
Some x
H1:mem x (filter (fun x0 : elt => negb (f x0)) s) =
true
mem x s = true /\ f x = false
rewrite filter_b in H1; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
H:is_empty (filter (fun x0 : elt => negb (f x0)) s) =
false
x:elt
H0:choose (filter (fun x0 : elt => negb (f x0)) s) =
Some x
H1:mem x s && negb (f x) = true
mem x s = true /\ f x = false
elim (andb_prop _ _ H1).f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
H:is_empty (filter (fun x0 : elt => negb (f x0)) s) =
false
x:elt
H0:choose (filter (fun x0 : elt => negb (f x0)) s) =
Some x
H1:mem x s && negb (f x) = true
mem x s = true ->
negb (f x) = true -> mem x s = true /\ f x = false
split;auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x0 : E.t => negb (f x0))
s:t
H:is_empty (filter (fun x0 : elt => negb (f x0)) s) =
false
x:elt
H0:choose (filter (fun x0 : elt => negb (f x0)) s) =
Some x
H1:mem x s && negb (f x) = true
H2:mem x s = true
H3:negb (f x) = true
f x = false
rewrite <- negb_true_iff; auto.
Qed.

Properties of ∃

Lemma for_all_exists:
 forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s).f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s : t,
exists_ f s =
negb (for_all (fun x : elt => negb (f x)) s)
Proof.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
forall s : t,
exists_ f s =
negb (for_all (fun x : elt => negb (f x)) s)
intros.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
exists_ f s =
negb (for_all (fun x : elt => negb (f x)) s)
rewrite for_all_b; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
exists_ f s =
negb
  (forallb (fun x : elt => negb (f x)) (elements s))
rewrite exists_b; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
existsb f (elements s) =
negb
  (forallb (fun x : elt => negb (f x)) (elements s))
induction (elements s); simpl; auto.f:elt -> bool
Comp:Proper (E.eq ==> Logic.eq) f
Comp':Proper (E.eq ==> Logic.eq)
  (fun x : E.t => negb (f x))
s:t
a:elt
l:list elt
IHl:existsb f l =
negb (forallb (fun x : elt => negb (f x)) l)
f a || existsb f l =
negb
  (negb (f a) && forallb (fun x : elt => negb (f x)) l)
destruct (f a); simpl; auto.
Qed.

End Bool.
Section Bool'.

Variable f:elt->bool.
Variable Comp: compat_bool E.eq f.

Let Comp' : compat_bool E.eq (fun x =>negb (f x)).f:elt -> bool
Comp:compat_bool E.eq f
compat_bool E.eq (fun x : E.t => negb (f x))
Proof.f:elt -> bool
Comp:compat_bool E.eq f
compat_bool E.eq (fun x : E.t => negb (f x))
unfold compat_bool, Proper, respectful in *; intros; f_equal; auto.
Qed.

Lemma exists_mem_1:
 forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x : E.t => negb (f x))
forall s : t,
(forall x : elt, mem x s = true -> f x = false) ->
exists_ f s = false
Proof.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x : E.t => negb (f x))
forall s : t,
(forall x : elt, mem x s = true -> f x = false) ->
exists_ f s = false
intros.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x : E.t => negb (f x))
s:t
H:forall x : elt, mem x s = true -> f x = false
exists_ f s = false
rewrite for_all_exists; auto.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x : E.t => negb (f x))
s:t
H:forall x : elt, mem x s = true -> f x = false
negb (for_all (fun x : elt => negb (f x)) s) = false
rewrite for_all_mem_1;auto with bool.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x : E.t => negb (f x))
s:t
H:forall x : elt, mem x s = true -> f x = false
forall x : elt, mem x s = true -> negb (f x) = true
intros;generalize (H x H0);intros.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x0 : E.t => negb (f x0))
s:t
H:forall x0 : elt, mem x0 s = true -> f x0 = false
x:elt
H0:mem x s = true
H1:f x = false
negb (f x) = true
rewrite negb_true_iff; auto.
Qed.

Lemma exists_mem_2:
 forall s, exists_ f s=false -> forall x, mem x s=true -> f x=false.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x : E.t => negb (f x))
forall s : t,
exists_ f s = false ->
forall x : elt, mem x s = true -> f x = false
Proof.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x : E.t => negb (f x))
forall s : t,
exists_ f s = false ->
forall x : elt, mem x s = true -> f x = false
intros.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x0 : E.t => negb (f x0))
s:t
H:exists_ f s = false
x:elt
H0:mem x s = true
f x = false
rewrite for_all_exists in H; auto.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x0 : E.t => negb (f x0))
s:t
H:negb (for_all (fun x0 : elt => negb (f x0)) s) =
false
x:elt
H0:mem x s = true
f x = false
rewrite negb_false_iff in H.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x0 : E.t => negb (f x0))
s:t
H:for_all (fun x0 : elt => negb (f x0)) s = true
x:elt
H0:mem x s = true
f x = false
rewrite <- negb_true_iff.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x0 : E.t => negb (f x0))
s:t
H:for_all (fun x0 : elt => negb (f x0)) s = true
x:elt
H0:mem x s = true
negb (f x) = true
apply for_all_mem_2 with (2:=H); auto.
Qed.

Lemma exists_mem_3:
 forall s x, mem x s=true -> f x=true -> exists_ f s=true.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x : E.t => negb (f x))
forall (s : t) (x : elt),
mem x s = true -> f x = true -> exists_ f s = true
Proof.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x : E.t => negb (f x))
forall (s : t) (x : elt),
mem x s = true -> f x = true -> exists_ f s = true
intros.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:mem x s = true
H0:f x = true
exists_ f s = true
rewrite for_all_exists; auto.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:mem x s = true
H0:f x = true
negb (for_all (fun x0 : elt => negb (f x0)) s) = true
rewrite negb_true_iff.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:mem x s = true
H0:f x = true
for_all (fun x0 : elt => negb (f x0)) s = false
apply for_all_mem_3 with x;auto.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x0 : E.t => negb (f x0))
s:t
x:elt
H:mem x s = true
H0:f x = true
negb (f x) = false
rewrite negb_false_iff; auto.
Qed.

Lemma exists_mem_4:
 forall s, exists_ f s=true -> {x:elt | (mem x s)=true /\ (f x)=true}.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x : E.t => negb (f x))
forall s : t,
exists_ f s = true ->
{x : elt | mem x s = true /\ f x = true}
Proof.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x : E.t => negb (f x))
forall s : t,
exists_ f s = true ->
{x : elt | mem x s = true /\ f x = true}
intros.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x : E.t => negb (f x))
s:t
H:exists_ f s = true
{x : elt | mem x s = true /\ f x = true}
rewrite for_all_exists in H; auto.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x : E.t => negb (f x))
s:t
H:negb (for_all (fun x : elt => negb (f x)) s) =
true
{x : elt | mem x s = true /\ f x = true}
rewrite negb_true_iff in H.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x : E.t => negb (f x))
s:t
H:for_all (fun x : elt => negb (f x)) s = false
{x : elt | mem x s = true /\ f x = true}
destruct (for_all_mem_4 (fun x =>negb (f x)) Comp' s) as (x,p); auto.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x0 : E.t => negb (f x0))
s:t
H:for_all (fun x0 : elt => negb (f x0)) s = false
x:elt
p:mem x s = true /\ negb (f x) = false
{x0 : elt | mem x0 s = true /\ f x0 = true}
elim p;intros.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x0 : E.t => negb (f x0))
s:t
H:for_all (fun x0 : elt => negb (f x0)) s = false
x:elt
p:mem x s = true /\ negb (f x) = false
H0:mem x s = true
H1:negb (f x) = false
{x0 : elt | mem x0 s = true /\ f x0 = true}
exists x;split;auto.f:elt -> bool
Comp:compat_bool E.eq f
Comp':compat_bool E.eq (fun x0 : E.t => negb (f x0))
s:t
H:for_all (fun x0 : elt => negb (f x0)) s = false
x:elt
p:mem x s = true /\ negb (f x) = false
H0:mem x s = true
H1:negb (f x) = false
f x = true
rewrite <-negb_false_iff; auto.
Qed.

End Bool'.

Section Sum.

Adding a valuation function on all elements of a set.

Definition sum (f:elt -> nat)(s:t) := fold (fun x => plus (f x)) s 0.
Notation compat_opL := (compat_op E.eq Logic.eq).
Notation transposeL := (transpose Logic.eq).

Lemma sum_plus :
  forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g ->
    forall s, sum (fun x =>f x+g x) s = sum f s + sum g s.forall f g : E.t -> nat,
Proper (E.eq ==> Logic.eq) f ->
Proper (E.eq ==> Logic.eq) g ->
forall s : t,
sum (fun x : elt => f x + g x) s = sum f s + sum g s
Proof.forall f g : E.t -> nat,
Proper (E.eq ==> Logic.eq) f ->
Proper (E.eq ==> Logic.eq) g ->
forall s : t,
sum (fun x : elt => f x + g x) s = sum f s + sum g s
unfold sum.forall f g : E.t -> nat,
Proper (E.eq ==> Logic.eq) f ->
Proper (E.eq ==> Logic.eq) g ->
forall s : t,
fold (fun x : elt => Init.Nat.add (f x + g x)) s 0 =
fold (fun x : elt => Init.Nat.add (f x)) s 0 +
fold (fun x : elt => Init.Nat.add (g x)) s 0
intros f g Hf Hg.f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
forall s : t,
fold (fun x : elt => Init.Nat.add (f x + g x)) s 0 =
fold (fun x : elt => Init.Nat.add (f x)) s 0 +
fold (fun x : elt => Init.Nat.add (g x)) s 0
assert (fc : compat_opL (fun x:elt =>plus (f x))).f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
compat_opL (fun x : elt => Init.Nat.add (f x))
f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
forall s : t,
fold (fun x : elt => Init.Nat.add (f x + g x)) s 0 =
fold (fun x : elt => Init.Nat.add (f x)) s 0 +
fold (fun x : elt => Init.Nat.add (g x)) s 0  red; auto with fset.f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
forall s : t,
fold (fun x : elt => Init.Nat.add (f x + g x)) s 0 =
fold (fun x : elt => Init.Nat.add (f x)) s 0 +
fold (fun x : elt => Init.Nat.add (g x)) s 0
assert (ft : transposeL (fun x:elt =>plus (f x))).f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
transposeL (fun x : elt => Init.Nat.add (f x))
f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
forall s : t,
fold (fun x : elt => Init.Nat.add (f x + g x)) s 0 =
fold (fun x : elt => Init.Nat.add (f x)) s 0 +
fold (fun x : elt => Init.Nat.add (g x)) s 0 red; intros; omega.f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
forall s : t,
fold (fun x : elt => Init.Nat.add (f x + g x)) s 0 =
fold (fun x : elt => Init.Nat.add (f x)) s 0 +
fold (fun x : elt => Init.Nat.add (g x)) s 0
assert (gc : compat_opL (fun x:elt => plus (g x))).f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
compat_opL (fun x : elt => Init.Nat.add (g x))
f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
forall s : t,
fold (fun x : elt => Init.Nat.add (f x + g x)) s 0 =
fold (fun x : elt => Init.Nat.add (f x)) s 0 +
fold (fun x : elt => Init.Nat.add (g x)) s 0 red; auto with fset.f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
forall s : t,
fold (fun x : elt => Init.Nat.add (f x + g x)) s 0 =
fold (fun x : elt => Init.Nat.add (f x)) s 0 +
fold (fun x : elt => Init.Nat.add (g x)) s 0
assert (gt : transposeL (fun x:elt =>plus (g x))).f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
transposeL (fun x : elt => Init.Nat.add (g x))
f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
forall s : t,
fold (fun x : elt => Init.Nat.add (f x + g x)) s 0 =
fold (fun x : elt => Init.Nat.add (f x)) s 0 +
fold (fun x : elt => Init.Nat.add (g x)) s 0 red; intros; omega.f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
forall s : t,
fold (fun x : elt => Init.Nat.add (f x + g x)) s 0 =
fold (fun x : elt => Init.Nat.add (f x)) s 0 +
fold (fun x : elt => Init.Nat.add (g x)) s 0
assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))).f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
compat_opL (fun x : elt => Init.Nat.add (f x + g x))
f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
forall s : t,
fold (fun x : elt => Init.Nat.add (f x + g x)) s 0 =
fold (fun x : elt => Init.Nat.add (f x)) s 0 +
fold (fun x : elt => Init.Nat.add (g x)) s 0 repeat red; auto.f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
forall s : t,
fold (fun x : elt => Init.Nat.add (f x + g x)) s 0 =
fold (fun x : elt => Init.Nat.add (f x)) s 0 +
fold (fun x : elt => Init.Nat.add (g x)) s 0
assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))).f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
transposeL (fun x : elt => Init.Nat.add (f x + g x))
f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
forall s : t,
fold (fun x : elt => Init.Nat.add (f x + g x)) s 0 =
fold (fun x : elt => Init.Nat.add (f x)) s 0 +
fold (fun x : elt => Init.Nat.add (g x)) s 0 red; intros; omega.f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
forall s : t,
fold (fun x : elt => Init.Nat.add (f x + g x)) s 0 =
fold (fun x : elt => Init.Nat.add (f x)) s 0 +
fold (fun x : elt => Init.Nat.add (g x)) s 0
assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
forall s : t,
fold (fun x : elt => Init.Nat.add (f x + g x)) s 0 =
fold (fun x : elt => Init.Nat.add (f x)) s 0 +
fold (fun x : elt => Init.Nat.add (g x)) s 0
intros s;pattern s; apply set_rec.f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
s:t
forall s0 s' : t,
equal s0 s' = true ->
fold (fun x : elt => Init.Nat.add (f x + g x)) s0 0 =
fold (fun x : elt => Init.Nat.add (f x)) s0 0 +
fold (fun x : elt => Init.Nat.add (g x)) s0 0 ->
fold (fun x : elt => Init.Nat.add (f x + g x)) s' 0 =
fold (fun x : elt => Init.Nat.add (f x)) s' 0 +
fold (fun x : elt => Init.Nat.add (g x)) s' 0
f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
s:t
forall (s0 : t) (x : elt),
mem x s0 = false ->
fold (fun x0 : elt => Init.Nat.add (f x0 + g x0)) s0 0 =
fold (fun x0 : elt => Init.Nat.add (f x0)) s0 0 +
fold (fun x0 : elt => Init.Nat.add (g x0)) s0 0 ->
fold (fun x0 : elt => Init.Nat.add (f x0 + g x0))
  (add x s0) 0 =
fold (fun x0 : elt => Init.Nat.add (f x0)) (add x s0)
  0 +
fold (fun x0 : elt => Init.Nat.add (g x0)) (add x s0)
  0
f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
s:t
fold (fun x : elt => Init.Nat.add (f x + g x)) empty 0 =
fold (fun x : elt => Init.Nat.add (f x)) empty 0 +
fold (fun x : elt => Init.Nat.add (g x)) empty 0
intros.f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
s, s0, s':t
H:equal s0 s' = true
H0:fold (fun x : elt => Init.Nat.add (f x + g x)) s0
  0 =
fold (fun x : elt => Init.Nat.add (f x)) s0 0 +
fold (fun x : elt => Init.Nat.add (g x)) s0 0
fold (fun x : elt => Init.Nat.add (f x + g x)) s' 0 =
fold (fun x : elt => Init.Nat.add (f x)) s' 0 +
fold (fun x : elt => Init.Nat.add (g x)) s' 0
f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
s:t
forall (s0 : t) (x : elt),
mem x s0 = false ->
fold (fun x0 : elt => Init.Nat.add (f x0 + g x0)) s0 0 =
fold (fun x0 : elt => Init.Nat.add (f x0)) s0 0 +
fold (fun x0 : elt => Init.Nat.add (g x0)) s0 0 ->
fold (fun x0 : elt => Init.Nat.add (f x0 + g x0))
  (add x s0) 0 =
fold (fun x0 : elt => Init.Nat.add (f x0)) (add x s0)
  0 +
fold (fun x0 : elt => Init.Nat.add (g x0)) (add x s0)
  0
f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
s:t
fold (fun x : elt => Init.Nat.add (f x + g x)) empty 0 =
fold (fun x : elt => Init.Nat.add (f x)) empty 0 +
fold (fun x : elt => Init.Nat.add (g x)) empty 0
rewrite <- (fold_equal _ _ st _ fc ft 0 _ _ H).f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
s, s0, s':t
H:equal s0 s' = true
H0:fold (fun x : elt => Init.Nat.add (f x + g x)) s0
  0 =
fold (fun x : elt => Init.Nat.add (f x)) s0 0 +
fold (fun x : elt => Init.Nat.add (g x)) s0 0
fold (fun x : elt => Init.Nat.add (f x + g x)) s' 0 =
fold (fun x : elt => Init.Nat.add (f x)) s0 0 +
fold (fun x : elt => Init.Nat.add (g x)) s' 0
f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
s:t
forall (s0 : t) (x : elt),
mem x s0 = false ->
fold (fun x0 : elt => Init.Nat.add (f x0 + g x0)) s0 0 =
fold (fun x0 : elt => Init.Nat.add (f x0)) s0 0 +
fold (fun x0 : elt => Init.Nat.add (g x0)) s0 0 ->
fold (fun x0 : elt => Init.Nat.add (f x0 + g x0))
  (add x s0) 0 =
fold (fun x0 : elt => Init.Nat.add (f x0)) (add x s0)
  0 +
fold (fun x0 : elt => Init.Nat.add (g x0)) (add x s0)
  0
f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
s:t
fold (fun x : elt => Init.Nat.add (f x + g x)) empty 0 =
fold (fun x : elt => Init.Nat.add (f x)) empty 0 +
fold (fun x : elt => Init.Nat.add (g x)) empty 0
rewrite <- (fold_equal _ _ st _ gc gt 0 _ _ H).f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
s, s0, s':t
H:equal s0 s' = true
H0:fold (fun x : elt => Init.Nat.add (f x + g x)) s0
  0 =
fold (fun x : elt => Init.Nat.add (f x)) s0 0 +
fold (fun x : elt => Init.Nat.add (g x)) s0 0
fold (fun x : elt => Init.Nat.add (f x + g x)) s' 0 =
fold (fun x : elt => Init.Nat.add (f x)) s0 0 +
fold (fun x : elt => Init.Nat.add (g x)) s0 0
f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
s:t
forall (s0 : t) (x : elt),
mem x s0 = false ->
fold (fun x0 : elt => Init.Nat.add (f x0 + g x0)) s0 0 =
fold (fun x0 : elt => Init.Nat.add (f x0)) s0 0 +
fold (fun x0 : elt => Init.Nat.add (g x0)) s0 0 ->
fold (fun x0 : elt => Init.Nat.add (f x0 + g x0))
  (add x s0) 0 =
fold (fun x0 : elt => Init.Nat.add (f x0)) (add x s0)
  0 +
fold (fun x0 : elt => Init.Nat.add (g x0)) (add x s0)
  0
f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
s:t
fold (fun x : elt => Init.Nat.add (f x + g x)) empty 0 =
fold (fun x : elt => Init.Nat.add (f x)) empty 0 +
fold (fun x : elt => Init.Nat.add (g x)) empty 0
rewrite <- (fold_equal _ _ st _ fgc fgt 0 _ _ H); auto.f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
s:t
forall (s0 : t) (x : elt),
mem x s0 = false ->
fold (fun x0 : elt => Init.Nat.add (f x0 + g x0)) s0 0 =
fold (fun x0 : elt => Init.Nat.add (f x0)) s0 0 +
fold (fun x0 : elt => Init.Nat.add (g x0)) s0 0 ->
fold (fun x0 : elt => Init.Nat.add (f x0 + g x0))
  (add x s0) 0 =
fold (fun x0 : elt => Init.Nat.add (f x0)) (add x s0)
  0 +
fold (fun x0 : elt => Init.Nat.add (g x0)) (add x s0)
  0
f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
s:t
fold (fun x : elt => Init.Nat.add (f x + g x)) empty 0 =
fold (fun x : elt => Init.Nat.add (f x)) empty 0 +
fold (fun x : elt => Init.Nat.add (g x)) empty 0
intros; do 3 (rewrite (fold_add _ _ st);auto).f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x0 : elt => Init.Nat.add (f x0))
ft:transposeL (fun x0 : elt => Init.Nat.add (f x0))
gc:compat_opL (fun x0 : elt => Init.Nat.add (g x0))
gt:transposeL (fun x0 : elt => Init.Nat.add (g x0))
fgc:compat_opL (fun x0 : elt => Init.Nat.add (f x0 + g x0))
fgt:transposeL (fun x0 : elt => Init.Nat.add (f x0 + g x0))
st:Equivalence Logic.eq
s, s0:t
x:elt
H:mem x s0 = false
H0:fold (fun x0 : elt => Init.Nat.add (f x0 + g x0))
  s0 0 =
fold (fun x0 : elt => Init.Nat.add (f x0)) s0 0 +
fold (fun x0 : elt => Init.Nat.add (g x0)) s0 0
f x + g x +
fold (fun x0 : elt => Init.Nat.add (f x0 + g x0)) s0 0 =
f x + fold (fun x0 : elt => Init.Nat.add (f x0)) s0 0 +
(g x + fold (fun x0 : elt => Init.Nat.add (g x0)) s0 0)
f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
s:t
fold (fun x : elt => Init.Nat.add (f x + g x)) empty 0 =
fold (fun x : elt => Init.Nat.add (f x)) empty 0 +
fold (fun x : elt => Init.Nat.add (g x)) empty 0
rewrite H0;simpl;omega.f, g:E.t -> nat
Hf:Proper (E.eq ==> Logic.eq) f
Hg:Proper (E.eq ==> Logic.eq) g
fc:compat_opL (fun x : elt => Init.Nat.add (f x))
ft:transposeL (fun x : elt => Init.Nat.add (f x))
gc:compat_opL (fun x : elt => Init.Nat.add (g x))
gt:transposeL (fun x : elt => Init.Nat.add (g x))
fgc:compat_opL (fun x : elt => Init.Nat.add (f x + g x))
fgt:transposeL (fun x : elt => Init.Nat.add (f x + g x))
st:Equivalence Logic.eq
s:t
fold (fun x : elt => Init.Nat.add (f x + g x)) empty 0 =
fold (fun x : elt => Init.Nat.add (f x)) empty 0 +
fold (fun x : elt => Init.Nat.add (g x)) empty 0
do 3 rewrite fold_empty;auto.
Qed.

Lemma sum_filter : forall f, (compat_bool E.eq f) ->
  forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)).forall f : E.t -> bool,
compat_bool E.eq f ->
forall s : t,
sum (fun x : elt => if f x then 1 else 0) s =
cardinal (filter f s)
Proof.forall f : E.t -> bool,
compat_bool E.eq f ->
forall s : t,
sum (fun x : elt => if f x then 1 else 0) s =
cardinal (filter f s)
unfold sum; intros f Hf.f:E.t -> bool
Hf:compat_bool E.eq f
forall s : t,
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  s 0 = cardinal (filter f s)
assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
forall s : t,
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  s 0 = cardinal (filter f s)
assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))).f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
compat_opL
  (fun x : E.t => Init.Nat.add (if f x then 1 else 0))
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
forall s : t,
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  s 0 = cardinal (filter f s)
 repeat red; intros.f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
x, y:E.t
H:E.eq x y
x0, y0:nat
H0:x0 = y0
(if f x then 1 else 0) + x0 =
(if f y then 1 else 0) + y0
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
forall s : t,
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  s 0 = cardinal (filter f s)
 rewrite (Hf _ _ H); auto.f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
forall s : t,
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  s 0 = cardinal (filter f s)
assert (ct : transposeL (fun x => plus (if f x then 1 else 0))).f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
transposeL
  (fun x : E.t => Init.Nat.add (if f x then 1 else 0))
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
forall s : t,
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  s 0 = cardinal (filter f s)
 red; intros; omega.f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
forall s : t,
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  s 0 = cardinal (filter f s)
intros s;pattern s; apply set_rec.f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
forall s0 s' : t,
equal s0 s' = true ->
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  s0 0 = cardinal (filter f s0) ->
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  s' 0 = cardinal (filter f s')
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
forall (s0 : t) (x : elt),
mem x s0 = false ->
fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f s0) ->
fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) (add x s0) 0 =
cardinal (filter f (add x s0))
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  empty 0 = cardinal (filter f empty)
intros.f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s, s0, s':t
H:equal s0 s' = true
H0:fold
  (fun x : elt =>
   Init.Nat.add (if f x then 1 else 0)) s0 0 =
cardinal (filter f s0)
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  s' 0 = cardinal (filter f s')
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
forall (s0 : t) (x : elt),
mem x s0 = false ->
fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f s0) ->
fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) (add x s0) 0 =
cardinal (filter f (add x s0))
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  empty 0 = cardinal (filter f empty)
change elt with E.t.f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s, s0, s':t
H:equal s0 s' = true
H0:fold
  (fun x : elt =>
   Init.Nat.add (if f x then 1 else 0)) s0 0 =
cardinal (filter f s0)
fold
  (fun x : E.t => Init.Nat.add (if f x then 1 else 0))
  s' 0 = cardinal (filter f s')
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
forall (s0 : t) (x : elt),
mem x s0 = false ->
fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f s0) ->
fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) (add x s0) 0 =
cardinal (filter f (add x s0))
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  empty 0 = cardinal (filter f empty)
rewrite <- (fold_equal _ _ st _ cc ct 0 _ _ H).f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s, s0, s':t
H:equal s0 s' = true
H0:fold
  (fun x : elt =>
   Init.Nat.add (if f x then 1 else 0)) s0 0 =
cardinal (filter f s0)
fold
  (fun x : E.t => Init.Nat.add (if f x then 1 else 0))
  s0 0 = cardinal (filter f s')
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
forall (s0 : t) (x : elt),
mem x s0 = false ->
fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f s0) ->
fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) (add x s0) 0 =
cardinal (filter f (add x s0))
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  empty 0 = cardinal (filter f empty)
rewrite <- (MP.Equal_cardinal (filter_equal Hf (equal_2 H))); auto.f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
forall (s0 : t) (x : elt),
mem x s0 = false ->
fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f s0) ->
fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) (add x s0) 0 =
cardinal (filter f (add x s0))
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  empty 0 = cardinal (filter f empty)
intros; rewrite (fold_add _ _ st _ cc ct); auto.f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0))
ct:transposeL
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0))
s, s0:t
x:elt
H:mem x s0 = false
H0:fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f s0)
(if f x then 1 else 0) +
fold
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f (add x s0))
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  empty 0 = cardinal (filter f empty)
generalize (@add_filter_1 f Hf s0 (add x s0) x) (@add_filter_2 f Hf s0 (add x s0) x) .f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0))
ct:transposeL
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0))
s, s0:t
x:elt
H:mem x s0 = false
H0:fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f s0)
(f x = true ->
 Add x s0 (add x s0) ->
 Add x (filter f s0) (filter f (add x s0))) ->
(f x = false ->
 Add x s0 (add x s0) ->
 filter f s0 [=] filter f (add x s0)) ->
(if f x then 1 else 0) +
fold
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f (add x s0))
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  empty 0 = cardinal (filter f empty)
assert (~ In x (filter f s0)).f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0))
ct:transposeL
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0))
s, s0:t
x:elt
H:mem x s0 = false
H0:fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f s0)
~ In x (filter f s0)
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0))
ct:transposeL
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0))
s, s0:t
x:elt
H:mem x s0 = false
H0:fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f s0)
H1:~ In x (filter f s0)
(f x = true ->
 Add x s0 (add x s0) ->
 Add x (filter f s0) (filter f (add x s0))) ->
(f x = false ->
 Add x s0 (add x s0) ->
 filter f s0 [=] filter f (add x s0)) ->
(if f x then 1 else 0) +
fold
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f (add x s0))
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  empty 0 = cardinal (filter f empty)
 intro H1; rewrite (mem_1 (filter_1 Hf H1)) in H; discriminate H.f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0))
ct:transposeL
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0))
s, s0:t
x:elt
H:mem x s0 = false
H0:fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f s0)
H1:~ In x (filter f s0)
(f x = true ->
 Add x s0 (add x s0) ->
 Add x (filter f s0) (filter f (add x s0))) ->
(f x = false ->
 Add x s0 (add x s0) ->
 filter f s0 [=] filter f (add x s0)) ->
(if f x then 1 else 0) +
fold
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f (add x s0))
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  empty 0 = cardinal (filter f empty)
case (f x); simpl; intros.f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0))
ct:transposeL
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0))
s, s0:t
x:elt
H:mem x s0 = false
H0:fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f s0)
H1:~ In x (filter f s0)
H2:true = true ->
Add x s0 (add x s0) ->
Add x (filter f s0) (filter f (add x s0))
H3:true = false ->
Add x s0 (add x s0) ->
filter f s0 [=] filter f (add x s0)
S
  (fold
     (fun x0 : E.t =>
      Init.Nat.add (if f x0 then 1 else 0)) s0 0) =
cardinal (filter f (add x s0))
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0))
ct:transposeL
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0))
s, s0:t
x:elt
H:mem x s0 = false
H0:fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f s0)
H1:~ In x (filter f s0)
H2:false = true ->
Add x s0 (add x s0) ->
Add x (filter f s0) (filter f (add x s0))
H3:false = false ->
Add x s0 (add x s0) ->
filter f s0 [=] filter f (add x s0)
fold
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f (add x s0))
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  empty 0 = cardinal (filter f empty)
rewrite (MP.cardinal_2 H1 (H2 Logic.eq_refl (MP.Add_add s0 x))); auto.f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0))
ct:transposeL
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0))
s, s0:t
x:elt
H:mem x s0 = false
H0:fold
  (fun x0 : elt =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f s0)
H1:~ In x (filter f s0)
H2:false = true ->
Add x s0 (add x s0) ->
Add x (filter f s0) (filter f (add x s0))
H3:false = false ->
Add x s0 (add x s0) ->
filter f s0 [=] filter f (add x s0)
fold
  (fun x0 : E.t =>
   Init.Nat.add (if f x0 then 1 else 0)) s0 0 =
cardinal (filter f (add x s0))
f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  empty 0 = cardinal (filter f empty)
rewrite <- (MP.Equal_cardinal (H3 Logic.eq_refl (MP.Add_add s0 x))); auto.f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
fold
  (fun x : elt => Init.Nat.add (if f x then 1 else 0))
  empty 0 = cardinal (filter f empty)
intros; rewrite fold_empty;auto.f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
0 = cardinal (filter f empty)
rewrite MP.cardinal_1; auto.f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
Empty (filter f empty)
unfold Empty; intros.f:E.t -> bool
Hf:compat_bool E.eq f
st:Equivalence Logic.eq
cc:compat_opL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
ct:transposeL
  (fun x : E.t =>
   Init.Nat.add (if f x then 1 else 0))
s:t
a:elt
~ In a (filter f empty)
rewrite filter_iff; auto; set_iff; tauto.
Qed.

Lemma fold_compat :
  forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)
  (f g:elt->A->A),
  (compat_op E.eq eqA f) -> (transpose eqA f) ->
  (compat_op E.eq eqA g) -> (transpose eqA g) ->
  forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) ->
  (eqA (fold f s i) (fold g s i)).forall (A : Type) (eqA : A -> A -> Prop),
Equivalence eqA ->
forall f g : elt -> A -> A,
compat_op E.eq eqA f ->
transpose eqA f ->
compat_op E.eq eqA g ->
transpose eqA g ->
forall (i : A) (s : t),
(forall x : elt,
 In x s -> forall y : A, eqA (f x y) (g x y)) ->
eqA (fold f s i) (fold g s i)
Proof.forall (A : Type) (eqA : A -> A -> Prop),
Equivalence eqA ->
forall f g : elt -> A -> A,
compat_op E.eq eqA f ->
transpose eqA f ->
compat_op E.eq eqA g ->
transpose eqA g ->
forall (i : A) (s : t),
(forall x : elt,
 In x s -> forall y : A, eqA (f x y) (g x y)) ->
eqA (fold f s i) (fold g s i)
intros A eqA st f g fc ft gc gt i.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
forall s : t,
(forall x : elt,
 In x s -> forall y : A, eqA (f x y) (g x y)) ->
eqA (fold f s i) (fold g s i)
intro s; pattern s; apply set_rec; intros.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0, s':t
H:equal s0 s' = true
H0:(forall x : elt,
 In x s0 -> forall y : A, eqA (f x y) (g x y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x : elt,
In x s' -> forall y : A, eqA (f x y) (g x y)
eqA (fold f s' i) (fold g s' i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0:t
x:elt
H:mem x s0 = false
H0:(forall x0 : elt,
 In x0 s0 -> forall y : A, eqA (f x0 y) (g x0 y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x0 : elt,
In x0 (add x s0) ->
forall y : A, eqA (f x0 y) (g x0 y)
eqA (fold f (add x s0) i) (fold g (add x s0) i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s:t
H:forall x : elt,
In x empty -> forall y : A, eqA (f x y) (g x y)
eqA (fold f empty i) (fold g empty i)
transitivity (fold f s0 i).A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0, s':t
H:equal s0 s' = true
H0:(forall x : elt,
 In x s0 -> forall y : A, eqA (f x y) (g x y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x : elt,
In x s' -> forall y : A, eqA (f x y) (g x y)
eqA (fold f s' i) (fold f s0 i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0, s':t
H:equal s0 s' = true
H0:(forall x : elt,
 In x s0 -> forall y : A, eqA (f x y) (g x y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x : elt,
In x s' -> forall y : A, eqA (f x y) (g x y)
eqA (fold f s0 i) (fold g s' i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0:t
x:elt
H:mem x s0 = false
H0:(forall x0 : elt,
 In x0 s0 -> forall y : A, eqA (f x0 y) (g x0 y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x0 : elt,
In x0 (add x s0) ->
forall y : A, eqA (f x0 y) (g x0 y)
eqA (fold f (add x s0) i) (fold g (add x s0) i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s:t
H:forall x : elt,
In x empty -> forall y : A, eqA (f x y) (g x y)
eqA (fold f empty i) (fold g empty i)
apply fold_equal with (eqA:=eqA); auto.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0, s':t
H:equal s0 s' = true
H0:(forall x : elt,
 In x s0 -> forall y : A, eqA (f x y) (g x y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x : elt,
In x s' -> forall y : A, eqA (f x y) (g x y)
equal s' s0 = true
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0, s':t
H:equal s0 s' = true
H0:(forall x : elt,
 In x s0 -> forall y : A, eqA (f x y) (g x y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x : elt,
In x s' -> forall y : A, eqA (f x y) (g x y)
eqA (fold f s0 i) (fold g s' i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0:t
x:elt
H:mem x s0 = false
H0:(forall x0 : elt,
 In x0 s0 -> forall y : A, eqA (f x0 y) (g x0 y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x0 : elt,
In x0 (add x s0) ->
forall y : A, eqA (f x0 y) (g x0 y)
eqA (fold f (add x s0) i) (fold g (add x s0) i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s:t
H:forall x : elt,
In x empty -> forall y : A, eqA (f x y) (g x y)
eqA (fold f empty i) (fold g empty i)
rewrite equal_sym; auto.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0, s':t
H:equal s0 s' = true
H0:(forall x : elt,
 In x s0 -> forall y : A, eqA (f x y) (g x y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x : elt,
In x s' -> forall y : A, eqA (f x y) (g x y)
eqA (fold f s0 i) (fold g s' i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0:t
x:elt
H:mem x s0 = false
H0:(forall x0 : elt,
 In x0 s0 -> forall y : A, eqA (f x0 y) (g x0 y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x0 : elt,
In x0 (add x s0) ->
forall y : A, eqA (f x0 y) (g x0 y)
eqA (fold f (add x s0) i) (fold g (add x s0) i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s:t
H:forall x : elt,
In x empty -> forall y : A, eqA (f x y) (g x y)
eqA (fold f empty i) (fold g empty i)
transitivity (fold g s0 i).A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0, s':t
H:equal s0 s' = true
H0:(forall x : elt,
 In x s0 -> forall y : A, eqA (f x y) (g x y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x : elt,
In x s' -> forall y : A, eqA (f x y) (g x y)
eqA (fold f s0 i) (fold g s0 i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0, s':t
H:equal s0 s' = true
H0:(forall x : elt,
 In x s0 -> forall y : A, eqA (f x y) (g x y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x : elt,
In x s' -> forall y : A, eqA (f x y) (g x y)
eqA (fold g s0 i) (fold g s' i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0:t
x:elt
H:mem x s0 = false
H0:(forall x0 : elt,
 In x0 s0 -> forall y : A, eqA (f x0 y) (g x0 y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x0 : elt,
In x0 (add x s0) ->
forall y : A, eqA (f x0 y) (g x0 y)
eqA (fold f (add x s0) i) (fold g (add x s0) i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s:t
H:forall x : elt,
In x empty -> forall y : A, eqA (f x y) (g x y)
eqA (fold f empty i) (fold g empty i)
apply H0; intros; apply H1; auto with set.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0, s':t
H:equal s0 s' = true
H0:(forall x0 : elt,
 In x0 s0 ->
 forall y0 : A, eqA (f x0 y0) (g x0 y0)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x0 : elt,
In x0 s' ->
forall y0 : A, eqA (f x0 y0) (g x0 y0)
x:elt
H2:In x s0
y:A
In x s'
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0, s':t
H:equal s0 s' = true
H0:(forall x : elt,
 In x s0 -> forall y : A, eqA (f x y) (g x y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x : elt,
In x s' -> forall y : A, eqA (f x y) (g x y)
eqA (fold g s0 i) (fold g s' i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0:t
x:elt
H:mem x s0 = false
H0:(forall x0 : elt,
 In x0 s0 -> forall y : A, eqA (f x0 y) (g x0 y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x0 : elt,
In x0 (add x s0) ->
forall y : A, eqA (f x0 y) (g x0 y)
eqA (fold f (add x s0) i) (fold g (add x s0) i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s:t
H:forall x : elt,
In x empty -> forall y : A, eqA (f x y) (g x y)
eqA (fold f empty i) (fold g empty i)
elim  (equal_2 H x); auto with set; intros.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0, s':t
H:equal s0 s' = true
H0:(forall x : elt,
 In x s0 -> forall y : A, eqA (f x y) (g x y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x : elt,
In x s' -> forall y : A, eqA (f x y) (g x y)
eqA (fold g s0 i) (fold g s' i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0:t
x:elt
H:mem x s0 = false
H0:(forall x0 : elt,
 In x0 s0 -> forall y : A, eqA (f x0 y) (g x0 y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x0 : elt,
In x0 (add x s0) ->
forall y : A, eqA (f x0 y) (g x0 y)
eqA (fold f (add x s0) i) (fold g (add x s0) i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s:t
H:forall x : elt,
In x empty -> forall y : A, eqA (f x y) (g x y)
eqA (fold f empty i) (fold g empty i)
apply fold_equal with (eqA:=eqA); auto with set.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0:t
x:elt
H:mem x s0 = false
H0:(forall x0 : elt,
 In x0 s0 -> forall y : A, eqA (f x0 y) (g x0 y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x0 : elt,
In x0 (add x s0) ->
forall y : A, eqA (f x0 y) (g x0 y)
eqA (fold f (add x s0) i) (fold g (add x s0) i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s:t
H:forall x : elt,
In x empty -> forall y : A, eqA (f x y) (g x y)
eqA (fold f empty i) (fold g empty i)
transitivity (f x (fold f s0 i)).A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0:t
x:elt
H:mem x s0 = false
H0:(forall x0 : elt,
 In x0 s0 -> forall y : A, eqA (f x0 y) (g x0 y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x0 : elt,
In x0 (add x s0) ->
forall y : A, eqA (f x0 y) (g x0 y)
eqA (fold f (add x s0) i) (f x (fold f s0 i))
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0:t
x:elt
H:mem x s0 = false
H0:(forall x0 : elt,
 In x0 s0 -> forall y : A, eqA (f x0 y) (g x0 y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x0 : elt,
In x0 (add x s0) ->
forall y : A, eqA (f x0 y) (g x0 y)
eqA (f x (fold f s0 i)) (fold g (add x s0) i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s:t
H:forall x : elt,
In x empty -> forall y : A, eqA (f x y) (g x y)
eqA (fold f empty i) (fold g empty i)
apply fold_add with (eqA:=eqA); auto with set.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0:t
x:elt
H:mem x s0 = false
H0:(forall x0 : elt,
 In x0 s0 -> forall y : A, eqA (f x0 y) (g x0 y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x0 : elt,
In x0 (add x s0) ->
forall y : A, eqA (f x0 y) (g x0 y)
eqA (f x (fold f s0 i)) (fold g (add x s0) i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s:t
H:forall x : elt,
In x empty -> forall y : A, eqA (f x y) (g x y)
eqA (fold f empty i) (fold g empty i)
transitivity (g x (fold f s0 i)); auto with set.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0:t
x:elt
H:mem x s0 = false
H0:(forall x0 : elt,
 In x0 s0 -> forall y : A, eqA (f x0 y) (g x0 y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x0 : elt,
In x0 (add x s0) ->
forall y : A, eqA (f x0 y) (g x0 y)
eqA (g x (fold f s0 i)) (fold g (add x s0) i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s:t
H:forall x : elt,
In x empty -> forall y : A, eqA (f x y) (g x y)
eqA (fold f empty i) (fold g empty i)
transitivity (g x (fold g s0 i)); auto with set.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0:t
x:elt
H:mem x s0 = false
H0:(forall x0 : elt,
 In x0 s0 -> forall y : A, eqA (f x0 y) (g x0 y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x0 : elt,
In x0 (add x s0) ->
forall y : A, eqA (f x0 y) (g x0 y)
eqA (g x (fold f s0 i)) (g x (fold g s0 i))
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0:t
x:elt
H:mem x s0 = false
H0:(forall x0 : elt,
 In x0 s0 -> forall y : A, eqA (f x0 y) (g x0 y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x0 : elt,
In x0 (add x s0) ->
forall y : A, eqA (f x0 y) (g x0 y)
eqA (g x (fold g s0 i)) (fold g (add x s0) i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s:t
H:forall x : elt,
In x empty -> forall y : A, eqA (f x y) (g x y)
eqA (fold f empty i) (fold g empty i)
apply gc; auto with *.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s, s0:t
x:elt
H:mem x s0 = false
H0:(forall x0 : elt,
 In x0 s0 -> forall y : A, eqA (f x0 y) (g x0 y)) ->
eqA (fold f s0 i) (fold g s0 i)
H1:forall x0 : elt,
In x0 (add x s0) ->
forall y : A, eqA (f x0 y) (g x0 y)
eqA (g x (fold g s0 i)) (fold g (add x s0) i)
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s:t
H:forall x : elt,
In x empty -> forall y : A, eqA (f x y) (g x y)
eqA (fold f empty i) (fold g empty i)
symmetry; apply fold_add with (eqA:=eqA); auto.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f, g:elt -> A -> A
fc:compat_op E.eq eqA f
ft:transpose eqA f
gc:compat_op E.eq eqA g
gt:transpose eqA g
i:A
s:t
H:forall x : elt,
In x empty -> forall y : A, eqA (f x y) (g x y)
eqA (fold f empty i) (fold g empty i)
do 2 rewrite fold_empty; reflexivity.
Qed.

Lemma sum_compat :
  forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g ->
  forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s.forall f g : E.t -> nat,
Proper (E.eq ==> Logic.eq) f ->
Proper (E.eq ==> Logic.eq) g ->
forall s : t,
(forall x : elt, In x s -> f x = g x) ->
sum f s = sum g s
intros.f, g:E.t -> nat
H:Proper (E.eq ==> Logic.eq) f
H0:Proper (E.eq ==> Logic.eq) g
s:t
H1:forall x : elt, In x s -> f x = g x
sum f s = sum g s
unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto with *.f, g:E.t -> nat
H:Proper (E.eq ==> Logic.eq) f
H0:Proper (E.eq ==> Logic.eq) g
s:t
H1:forall x : elt, In x s -> f x = g x
compat_opL (fun x : elt => Init.Nat.add (f x))
f, g:E.t -> nat
H:Proper (E.eq ==> Logic.eq) f
H0:Proper (E.eq ==> Logic.eq) g
s:t
H1:forall x : elt, In x s -> f x = g x
compat_opL (fun x : elt => Init.Nat.add (g x))
intros x x' Hx y y' Hy.f, g:E.t -> nat
H:Proper (E.eq ==> Logic.eq) f
H0:Proper (E.eq ==> Logic.eq) g
s:t
H1:forall x0 : elt, In x0 s -> f x0 = g x0
x, x':E.t
Hx:E.eq x x'
y, y':nat
Hy:y = y'
f x + y = f x' + y'
f, g:E.t -> nat
H:Proper (E.eq ==> Logic.eq) f
H0:Proper (E.eq ==> Logic.eq) g
s:t
H1:forall x : elt, In x s -> f x = g x
compat_opL (fun x : elt => Init.Nat.add (g x)) rewrite Hx, Hy; auto.f, g:E.t -> nat
H:Proper (E.eq ==> Logic.eq) f
H0:Proper (E.eq ==> Logic.eq) g
s:t
H1:forall x : elt, In x s -> f x = g x
compat_opL (fun x : elt => Init.Nat.add (g x))
intros x x' Hx y y' Hy.f, g:E.t -> nat
H:Proper (E.eq ==> Logic.eq) f
H0:Proper (E.eq ==> Logic.eq) g
s:t
H1:forall x0 : elt, In x0 s -> f x0 = g x0
x, x':E.t
Hx:E.eq x x'
y, y':nat
Hy:y = y'
g x + y = g x' + y' rewrite Hx, Hy; auto.
Qed.

End Sum.

End WEqProperties_fun.

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 EqProperties functor which is meant to be used on modules (M:S) can simply be an alias of WEqProperties.

Module WEqProperties (M:WS) := WEqProperties_fun M.E M.
Module EqProperties := WEqProperties.