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

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

Finite sets library

This functor derives additional properties from FSetInterface.S. Contrary to the functor in FSetEqProperties it uses predicates over sets instead of sets operations, i.e. In x s instead of mem x s=true, Equal s s' instead of equal s s'=true, etc.

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

Hint Unfold transpose compat_op Proper respectful : fset.
Hint Extern 1 (Equivalence _) => constructor; congruence : fset.

First, a functor for Weak Sets in functorial version.

Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
  Module Import Dec := WDecide_fun E M.
  Module Import FM := Dec.F (* FSetFacts.WFacts_fun E M *).
  Import M.

  Lemma In_dec : forall x s, {In x s} + {~ In x s}.forall (x : elt) (s : t), {In x s} + {~ In x s}
  Proof.forall (x : elt) (s : t), {In x s} + {~ In x s}
  intros; generalize (mem_iff s x); case (mem x s); intuition.
  Qed.

  Definition Add x s s' := forall y, In y s' <-> E.eq x y \/ In y s.

  Lemma Add_Equal : forall x s s', Add x s s' <-> s' [=] add x s.forall (x : E.t) (s s' : t),
Add x s s' <-> s' [=] add x s
  Proof.forall (x : E.t) (s s' : t),
Add x s s' <-> s' [=] add x s
  unfold Add.forall (x : E.t) (s s' : t),
(forall y : elt, In y s' <-> E.eq x y \/ In y s) <->
s' [=] add x s
  split; intros.x:E.t
s, s':t
H:forall y : elt, In y s' <-> E.eq x y \/ In y s
s' [=] add x s
x:E.t
s, s':t
H:s' [=] add x s
y:elt
In y s' <-> E.eq x y \/ In y s
  red; intros.x:E.t
s, s':t
H:forall y : elt, In y s' <-> E.eq x y \/ In y s
a:elt
In a s' <-> In a (add x s)
x:E.t
s, s':t
H:s' [=] add x s
y:elt
In y s' <-> E.eq x y \/ In y s
  rewrite H; clear H.x:E.t
s, s':t
a:elt
E.eq x a \/ In a s <-> In a (add x s)
x:E.t
s, s':t
H:s' [=] add x s
y:elt
In y s' <-> E.eq x y \/ In y s
  fsetdec.x:E.t
s, s':t
H:s' [=] add x s
y:elt
In y s' <-> E.eq x y \/ In y s
  fsetdec.
  Qed.

  Ltac expAdd := repeat rewrite Add_Equal.

  Section BasicProperties.

  Variable s s' s'' s1 s2 s3 : t.
  Variable x x' : elt.

  Lemma equal_refl : s[=]s.s, s', s'', s1, s2, s3:t
x, x':elt
s [=] s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s [=] s fsetdec. Qed.

  Lemma equal_sym : s[=]s' -> s'[=]s.s, s', s'', s1, s2, s3:t
x, x':elt
s [=] s' -> s' [=] s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s [=] s' -> s' [=] s fsetdec. Qed.

  Lemma equal_trans : s1[=]s2 -> s2[=]s3 -> s1[=]s3.s, s', s'', s1, s2, s3:t
x, x':elt
s1 [=] s2 -> s2 [=] s3 -> s1 [=] s3
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s1 [=] s2 -> s2 [=] s3 -> s1 [=] s3 fsetdec. Qed.

  Lemma subset_refl : s[<=]s.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] s fsetdec. Qed.

  Lemma subset_trans : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3.s, s', s'', s1, s2, s3:t
x, x':elt
s1 [<=] s2 -> s2 [<=] s3 -> s1 [<=] s3
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s1 [<=] s2 -> s2 [<=] s3 -> s1 [<=] s3 fsetdec. Qed.

  Lemma subset_antisym : s[<=]s' -> s'[<=]s -> s[=]s'.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] s' -> s' [<=] s -> s [=] s'
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] s' -> s' [<=] s -> s [=] s' fsetdec. Qed.

  Lemma subset_equal : s[=]s' -> s[<=]s'.s, s', s'', s1, s2, s3:t
x, x':elt
s [=] s' -> s [<=] s'
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s [=] s' -> s [<=] s' fsetdec. Qed.

  Lemma subset_empty : empty[<=]s.s, s', s'', s1, s2, s3:t
x, x':elt
empty [<=] s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
empty [<=] s fsetdec. Qed.

  Lemma subset_remove_3 : s1[<=]s2 -> remove x s1 [<=] s2.s, s', s'', s1, s2, s3:t
x, x':elt
s1 [<=] s2 -> remove x s1 [<=] s2
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s1 [<=] s2 -> remove x s1 [<=] s2 fsetdec. Qed.

  Lemma subset_diff : s1[<=]s3 -> diff s1 s2 [<=] s3.s, s', s'', s1, s2, s3:t
x, x':elt
s1 [<=] s3 -> diff s1 s2 [<=] s3
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s1 [<=] s3 -> diff s1 s2 [<=] s3 fsetdec. Qed.

  Lemma subset_add_3 : In x s2 -> s1[<=]s2 -> add x s1 [<=] s2.s, s', s'', s1, s2, s3:t
x, x':elt
In x s2 -> s1 [<=] s2 -> add x s1 [<=] s2
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
In x s2 -> s1 [<=] s2 -> add x s1 [<=] s2 fsetdec. Qed.

  Lemma subset_add_2 : s1[<=]s2 -> s1[<=] add x s2.s, s', s'', s1, s2, s3:t
x, x':elt
s1 [<=] s2 -> s1 [<=] add x s2
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s1 [<=] s2 -> s1 [<=] add x s2 fsetdec. Qed.

  Lemma in_subset : In x s1 -> s1[<=]s2 -> In x s2.s, s', s'', s1, s2, s3:t
x, x':elt
In x s1 -> s1 [<=] s2 -> In x s2
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
In x s1 -> s1 [<=] s2 -> In x s2 fsetdec. Qed.

  Lemma double_inclusion : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1.s, s', s'', s1, s2, s3:t
x, x':elt
s1 [=] s2 <-> s1 [<=] s2 /\ s2 [<=] s1
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s1 [=] s2 <-> s1 [<=] s2 /\ s2 [<=] s1 intuition fsetdec. Qed.

  Lemma empty_is_empty_1 : Empty s -> s[=]empty.s, s', s'', s1, s2, s3:t
x, x':elt
Empty s -> s [=] empty
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
Empty s -> s [=] empty fsetdec. Qed.

  Lemma empty_is_empty_2 : s[=]empty -> Empty s.s, s', s'', s1, s2, s3:t
x, x':elt
s [=] empty -> Empty s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s [=] empty -> Empty s fsetdec. Qed.

  Lemma add_equal : In x s -> add x s [=] s.s, s', s'', s1, s2, s3:t
x, x':elt
In x s -> add x s [=] s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
In x s -> add x s [=] s fsetdec. Qed.

  Lemma add_add : add x (add x' s) [=] add x' (add x s).s, s', s'', s1, s2, s3:t
x, x':elt
add x (add x' s) [=] add x' (add x s)
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
add x (add x' s) [=] add x' (add x s) fsetdec. Qed.

  Lemma remove_equal : ~ In x s -> remove x s [=] s.s, s', s'', s1, s2, s3:t
x, x':elt
~ In x s -> remove x s [=] s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
~ In x s -> remove x s [=] s fsetdec. Qed.

  Lemma Equal_remove : s[=]s' -> remove x s [=] remove x s'.s, s', s'', s1, s2, s3:t
x, x':elt
s [=] s' -> remove x s [=] remove x s'
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s [=] s' -> remove x s [=] remove x s' fsetdec. Qed.

  Lemma add_remove : In x s -> add x (remove x s) [=] s.s, s', s'', s1, s2, s3:t
x, x':elt
In x s -> add x (remove x s) [=] s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
In x s -> add x (remove x s) [=] s fsetdec. Qed.

  Lemma remove_add : ~In x s -> remove x (add x s) [=] s.s, s', s'', s1, s2, s3:t
x, x':elt
~ In x s -> remove x (add x s) [=] s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
~ In x s -> remove x (add x s) [=] s fsetdec. Qed.

  Lemma singleton_equal_add : singleton x [=] add x empty.s, s', s'', s1, s2, s3:t
x, x':elt
singleton x [=] add x empty
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
singleton x [=] add x empty fsetdec. Qed.

  Lemma remove_singleton_empty :
   In x s -> remove x s [=] empty -> singleton x [=] s.s, s', s'', s1, s2, s3:t
x, x':elt
In x s -> remove x s [=] empty -> singleton x [=] s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
In x s -> remove x s [=] empty -> singleton x [=] s fsetdec. Qed.

  Lemma union_sym : union s s' [=] union s' s.s, s', s'', s1, s2, s3:t
x, x':elt
union s s' [=] union s' s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
union s s' [=] union s' s fsetdec. Qed.

  Lemma union_subset_equal : s[<=]s' -> union s s' [=] s'.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] s' -> union s s' [=] s'
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] s' -> union s s' [=] s' fsetdec. Qed.

  Lemma union_equal_1 : s[=]s' -> union s s'' [=] union s' s''.s, s', s'', s1, s2, s3:t
x, x':elt
s [=] s' -> union s s'' [=] union s' s''
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s [=] s' -> union s s'' [=] union s' s'' fsetdec. Qed.

  Lemma union_equal_2 : s'[=]s'' -> union s s' [=] union s s''.s, s', s'', s1, s2, s3:t
x, x':elt
s' [=] s'' -> union s s' [=] union s s''
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s' [=] s'' -> union s s' [=] union s s'' fsetdec. Qed.

  Lemma union_assoc : union (union s s') s'' [=] union s (union s' s'').s, s', s'', s1, s2, s3:t
x, x':elt
union (union s s') s'' [=] union s (union s' s'')
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
union (union s s') s'' [=] union s (union s' s'') fsetdec. Qed.

  Lemma add_union_singleton : add x s [=] union (singleton x) s.s, s', s'', s1, s2, s3:t
x, x':elt
add x s [=] union (singleton x) s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
add x s [=] union (singleton x) s fsetdec. Qed.

  Lemma union_add : union (add x s) s' [=] add x (union s s').s, s', s'', s1, s2, s3:t
x, x':elt
union (add x s) s' [=] add x (union s s')
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
union (add x s) s' [=] add x (union s s') fsetdec. Qed.

  Lemma union_remove_add_1 :
   union (remove x s) (add x s') [=] union (add x s) (remove x s').s, s', s'', s1, s2, s3:t
x, x':elt
union (remove x s) (add x s') [=]
union (add x s) (remove x s')
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
union (remove x s) (add x s') [=]
union (add x s) (remove x s') fsetdec. Qed.

  Lemma union_remove_add_2 : In x s ->
   union (remove x s) (add x s') [=] union s s'.s, s', s'', s1, s2, s3:t
x, x':elt
In x s -> union (remove x s) (add x s') [=] union s s'
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
In x s -> union (remove x s) (add x s') [=] union s s' fsetdec. Qed.

  Lemma union_subset_1 : s [<=] union s s'.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] union s s'
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] union s s' fsetdec. Qed.

  Lemma union_subset_2 : s' [<=] union s s'.s, s', s'', s1, s2, s3:t
x, x':elt
s' [<=] union s s'
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s' [<=] union s s' fsetdec. Qed.

  Lemma union_subset_3 : s[<=]s'' -> s'[<=]s'' -> union s s' [<=] s''.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] s'' -> s' [<=] s'' -> union s s' [<=] s''
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] s'' -> s' [<=] s'' -> union s s' [<=] s'' fsetdec. Qed.

  Lemma union_subset_4 : s[<=]s' -> union s s'' [<=] union s' s''.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] s' -> union s s'' [<=] union s' s''
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] s' -> union s s'' [<=] union s' s'' fsetdec. Qed.

  Lemma union_subset_5 : s[<=]s' -> union s'' s [<=] union s'' s'.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] s' -> union s'' s [<=] union s'' s'
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] s' -> union s'' s [<=] union s'' s' fsetdec. Qed.

  Lemma empty_union_1 : Empty s -> union s s' [=] s'.s, s', s'', s1, s2, s3:t
x, x':elt
Empty s -> union s s' [=] s'
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
Empty s -> union s s' [=] s' fsetdec. Qed.

  Lemma empty_union_2 : Empty s -> union s' s [=] s'.s, s', s'', s1, s2, s3:t
x, x':elt
Empty s -> union s' s [=] s'
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
Empty s -> union s' s [=] s' fsetdec. Qed.

  Lemma not_in_union : ~In x s -> ~In x s' -> ~In x (union s s').s, s', s'', s1, s2, s3:t
x, x':elt
~ In x s -> ~ In x s' -> ~ In x (union s s')
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
~ In x s -> ~ In x s' -> ~ In x (union s s') fsetdec. Qed.

  Lemma inter_sym : inter s s' [=] inter s' s.s, s', s'', s1, s2, s3:t
x, x':elt
inter s s' [=] inter s' s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
inter s s' [=] inter s' s fsetdec. Qed.

  Lemma inter_subset_equal : s[<=]s' -> inter s s' [=] s.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] s' -> inter s s' [=] s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] s' -> inter s s' [=] s fsetdec. Qed.

  Lemma inter_equal_1 : s[=]s' -> inter s s'' [=] inter s' s''.s, s', s'', s1, s2, s3:t
x, x':elt
s [=] s' -> inter s s'' [=] inter s' s''
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s [=] s' -> inter s s'' [=] inter s' s'' fsetdec. Qed.

  Lemma inter_equal_2 : s'[=]s'' -> inter s s' [=] inter s s''.s, s', s'', s1, s2, s3:t
x, x':elt
s' [=] s'' -> inter s s' [=] inter s s''
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s' [=] s'' -> inter s s' [=] inter s s'' fsetdec. Qed.

  Lemma inter_assoc : inter (inter s s') s'' [=] inter s (inter s' s'').s, s', s'', s1, s2, s3:t
x, x':elt
inter (inter s s') s'' [=] inter s (inter s' s'')
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
inter (inter s s') s'' [=] inter s (inter s' s'') fsetdec. Qed.

  Lemma union_inter_1 : inter (union s s') s'' [=] union (inter s s'') (inter s' s'').s, s', s'', s1, s2, s3:t
x, x':elt
inter (union s s') s'' [=]
union (inter s s'') (inter s' s'')
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
inter (union s s') s'' [=]
union (inter s s'') (inter s' s'') fsetdec. Qed.

  Lemma union_inter_2 : union (inter s s') s'' [=] inter (union s s'') (union s' s'').s, s', s'', s1, s2, s3:t
x, x':elt
union (inter s s') s'' [=]
inter (union s s'') (union s' s'')
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
union (inter s s') s'' [=]
inter (union s s'') (union s' s'') fsetdec. Qed.

  Lemma inter_add_1 : In x s' -> inter (add x s) s' [=] add x (inter s s').s, s', s'', s1, s2, s3:t
x, x':elt
In x s' -> inter (add x s) s' [=] add x (inter s s')
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
In x s' -> inter (add x s) s' [=] add x (inter s s') fsetdec. Qed.

  Lemma inter_add_2 : ~ In x s' -> inter (add x s) s' [=] inter s s'.s, s', s'', s1, s2, s3:t
x, x':elt
~ In x s' -> inter (add x s) s' [=] inter s s'
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
~ In x s' -> inter (add x s) s' [=] inter s s' fsetdec. Qed.

  Lemma empty_inter_1 : Empty s -> Empty (inter s s').s, s', s'', s1, s2, s3:t
x, x':elt
Empty s -> Empty (inter s s')
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
Empty s -> Empty (inter s s') fsetdec. Qed.

  Lemma empty_inter_2 : Empty s' -> Empty (inter s s').s, s', s'', s1, s2, s3:t
x, x':elt
Empty s' -> Empty (inter s s')
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
Empty s' -> Empty (inter s s') fsetdec. Qed.

  Lemma inter_subset_1 : inter s s' [<=] s.s, s', s'', s1, s2, s3:t
x, x':elt
inter s s' [<=] s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
inter s s' [<=] s fsetdec. Qed.

  Lemma inter_subset_2 : inter s s' [<=] s'.s, s', s'', s1, s2, s3:t
x, x':elt
inter s s' [<=] s'
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
inter s s' [<=] s' fsetdec. Qed.

  Lemma inter_subset_3 :
   s''[<=]s -> s''[<=]s' -> s''[<=] inter s s'.s, s', s'', s1, s2, s3:t
x, x':elt
s'' [<=] s -> s'' [<=] s' -> s'' [<=] inter s s'
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s'' [<=] s -> s'' [<=] s' -> s'' [<=] inter s s' fsetdec. Qed.

  Lemma empty_diff_1 : Empty s -> Empty (diff s s').s, s', s'', s1, s2, s3:t
x, x':elt
Empty s -> Empty (diff s s')
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
Empty s -> Empty (diff s s') fsetdec. Qed.

  Lemma empty_diff_2 : Empty s -> diff s' s [=] s'.s, s', s'', s1, s2, s3:t
x, x':elt
Empty s -> diff s' s [=] s'
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
Empty s -> diff s' s [=] s' fsetdec. Qed.

  Lemma diff_subset : diff s s' [<=] s.s, s', s'', s1, s2, s3:t
x, x':elt
diff s s' [<=] s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
diff s s' [<=] s fsetdec. Qed.

  Lemma diff_subset_equal : s[<=]s' -> diff s s' [=] empty.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] s' -> diff s s' [=] empty
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
s [<=] s' -> diff s s' [=] empty fsetdec. Qed.

  Lemma remove_diff_singleton :
   remove x s [=] diff s (singleton x).s, s', s'', s1, s2, s3:t
x, x':elt
remove x s [=] diff s (singleton x)
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
remove x s [=] diff s (singleton x) fsetdec. Qed.

  Lemma diff_inter_empty : inter (diff s s') (inter s s') [=] empty.s, s', s'', s1, s2, s3:t
x, x':elt
inter (diff s s') (inter s s') [=] empty
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
inter (diff s s') (inter s s') [=] empty fsetdec. Qed.

  Lemma diff_inter_all : union (diff s s') (inter s s') [=] s.s, s', s'', s1, s2, s3:t
x, x':elt
union (diff s s') (inter s s') [=] s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
union (diff s s') (inter s s') [=] s fsetdec. Qed.

  Lemma Add_add : Add x s (add x s).s, s', s'', s1, s2, s3:t
x, x':elt
Add x s (add x s)
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
Add x s (add x s) expAdd; fsetdec. Qed.

  Lemma Add_remove : In x s -> Add x (remove x s) s.s, s', s'', s1, s2, s3:t
x, x':elt
In x s -> Add x (remove x s) s
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
In x s -> Add x (remove x s) s expAdd; fsetdec. Qed.

  Lemma union_Add : Add x s s' -> Add x (union s s'') (union s' s'').s, s', s'', s1, s2, s3:t
x, x':elt
Add x s s' -> Add x (union s s'') (union s' s'')
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
Add x s s' -> Add x (union s s'') (union s' s'') expAdd; fsetdec. Qed.

  Lemma inter_Add :
   In x s'' -> Add x s s' -> Add x (inter s s'') (inter s' s'').s, s', s'', s1, s2, s3:t
x, x':elt
In x s'' ->
Add x s s' -> Add x (inter s s'') (inter s' s'')
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
In x s'' ->
Add x s s' -> Add x (inter s s'') (inter s' s'') expAdd; fsetdec. Qed.

  Lemma union_Equal :
   In x s'' -> Add x s s' -> union s s'' [=] union s' s''.s, s', s'', s1, s2, s3:t
x, x':elt
In x s'' -> Add x s s' -> union s s'' [=] union s' s''
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
In x s'' -> Add x s s' -> union s s'' [=] union s' s'' expAdd; fsetdec. Qed.

  Lemma inter_Add_2 :
   ~In x s'' -> Add x s s' -> inter s s'' [=] inter s' s''.s, s', s'', s1, s2, s3:t
x, x':elt
~ In x s'' ->
Add x s s' -> inter s s'' [=] inter s' s''
  Proof.s, s', s'', s1, s2, s3:t
x, x':elt
~ In x s'' ->
Add x s s' -> inter s s'' [=] inter s' s'' expAdd; fsetdec. Qed.

  End BasicProperties.

  Hint Immediate equal_sym add_remove remove_add union_sym inter_sym: set.
  Hint Resolve equal_refl equal_trans subset_refl subset_equal subset_antisym
    subset_trans subset_empty subset_remove_3 subset_diff subset_add_3
    subset_add_2 in_subset empty_is_empty_1 empty_is_empty_2 add_equal
    remove_equal singleton_equal_add union_subset_equal union_equal_1
    union_equal_2 union_assoc add_union_singleton union_add union_subset_1
    union_subset_2 union_subset_3 inter_subset_equal inter_equal_1 inter_equal_2
    inter_assoc union_inter_1 union_inter_2 inter_add_1 inter_add_2
    empty_inter_1 empty_inter_2 empty_union_1 empty_union_2 empty_diff_1
    empty_diff_2 union_Add inter_Add union_Equal inter_Add_2 not_in_union
    inter_subset_1 inter_subset_2 inter_subset_3 diff_subset diff_subset_equal
    remove_diff_singleton diff_inter_empty diff_inter_all Add_add Add_remove
    Equal_remove add_add : set.

Properties of elements

  Lemma elements_Empty : forall s, Empty s <-> elements s = nil.forall s : t, Empty s <-> elements s = nil
  Proof.forall s : t, Empty s <-> elements s = nil
  intros.s:t
Empty s <-> elements s = nil
  unfold Empty.s:t
(forall a : elt, ~ In a s) <-> elements s = nil
  split; intros.s:t
H:forall a : elt, ~ In a s
elements s = nil
s:t
H:elements s = nil
a:elt
~ In a s
  assert (forall a, ~ List.In a (elements s)).s:t
H:forall a : elt, ~ In a s
forall a : elt, ~ List.In a (elements s)
s:t
H:forall a : elt, ~ In a s
H0:forall a : elt, ~ List.In a (elements s)
elements s = nil
s:t
H:elements s = nil
a:elt
~ In a s
   red; intros.s:t
H:forall a0 : elt, ~ In a0 s
a:elt
H0:List.In a (elements s)
False
s:t
H:forall a : elt, ~ In a s
H0:forall a : elt, ~ List.In a (elements s)
elements s = nil
s:t
H:elements s = nil
a:elt
~ In a s
   apply (H a).s:t
H:forall a0 : elt, ~ In a0 s
a:elt
H0:List.In a (elements s)
In a s
s:t
H:forall a : elt, ~ In a s
H0:forall a : elt, ~ List.In a (elements s)
elements s = nil
s:t
H:elements s = nil
a:elt
~ In a s
   rewrite elements_iff.s:t
H:forall a0 : elt, ~ In a0 s
a:elt
H0:List.In a (elements s)
InA E.eq a (elements s)
s:t
H:forall a : elt, ~ In a s
H0:forall a : elt, ~ List.In a (elements s)
elements s = nil
s:t
H:elements s = nil
a:elt
~ In a s
   rewrite InA_alt; exists a; auto.s:t
H:forall a : elt, ~ In a s
H0:forall a : elt, ~ List.In a (elements s)
elements s = nil
s:t
H:elements s = nil
a:elt
~ In a s
  destruct (elements s); auto.s:t
H:forall a : elt, ~ In a s
e:elt
l:list elt
H0:forall a : elt, ~ List.In a (e :: l)
e :: l = nil
s:t
H:elements s = nil
a:elt
~ In a s
  elim (H0 e); simpl; auto.s:t
H:elements s = nil
a:elt
~ In a s
  red; intros.s:t
H:elements s = nil
a:elt
H0:In a s
False
  rewrite elements_iff in H0.s:t
H:elements s = nil
a:elt
H0:InA E.eq a (elements s)
False
  rewrite InA_alt in H0; destruct H0.s:t
H:elements s = nil
a:elt
x:E.t
H0:E.eq a x /\ List.In x (elements s)
False
  rewrite H in H0; destruct H0 as (_,H0); inversion H0.
  Qed.

  Lemma elements_empty : elements empty = nil.elements empty = nil
  Proof.elements empty = nil
  rewrite <-elements_Empty; auto with set.
  Qed.

Conversions between lists and sets

  Definition of_list (l : list elt) := List.fold_right add empty l.

  Definition to_list := elements.

  Lemma of_list_1 : forall l x, In x (of_list l) <-> InA E.eq x l.forall (l : list elt) (x : elt),
In x (of_list l) <-> InA E.eq x l
  Proof.forall (l : list elt) (x : elt),
In x (of_list l) <-> InA E.eq x l
  induction l; simpl; intro x.x:elt
In x empty <-> InA E.eq x nil
a:elt
l:list elt
IHl:forall x0 : elt, In x0 (of_list l) <-> InA E.eq x0 l
x:elt
In x (add a (of_list l)) <-> InA E.eq x (a :: l)
  rewrite empty_iff, InA_nil.x:elt
False <-> False
a:elt
l:list elt
IHl:forall x0 : elt, In x0 (of_list l) <-> InA E.eq x0 l
x:elt
In x (add a (of_list l)) <-> InA E.eq x (a :: l) intuition.a:elt
l:list elt
IHl:forall x0 : elt, In x0 (of_list l) <-> InA E.eq x0 l
x:elt
In x (add a (of_list l)) <-> InA E.eq x (a :: l)
  rewrite add_iff, InA_cons, IHl.a:elt
l:list elt
IHl:forall x0 : elt, In x0 (of_list l) <-> InA E.eq x0 l
x:elt
E.eq a x \/ InA E.eq x l <-> E.eq x a \/ InA E.eq x l intuition.
  Qed.

  Lemma of_list_2 : forall l, equivlistA E.eq (to_list (of_list l)) l.forall l : list elt,
equivlistA E.eq (to_list (of_list l)) l
  Proof.forall l : list elt,
equivlistA E.eq (to_list (of_list l)) l
  unfold to_list; red; intros.l:list elt
x:E.t
InA E.eq x (elements (of_list l)) <-> InA E.eq x l
  rewrite <- elements_iff; apply of_list_1.
  Qed.

  Lemma of_list_3 : forall s, of_list (to_list s) [=] s.forall s : t, of_list (to_list s) [=] s
  Proof.forall s : t, of_list (to_list s) [=] s
  unfold to_list; red; intros.s:t
a:elt
In a (of_list (elements s)) <-> In a s
  rewrite of_list_1; symmetry; apply elements_iff.
  Qed.

Fold

  Section Fold.

Alternative specification via fold_right

  Lemma fold_spec_right (s:t)(A:Type)(i:A)(f : elt -> A -> A) :
    fold f s i = List.fold_right f i (rev (elements s)).s:t
A:Type
i:A
f:elt -> A -> A
fold f s i = fold_right f i (rev (elements s))
  Proof.s:t
A:Type
i:A
f:elt -> A -> A
fold f s i = fold_right f i (rev (elements s))
   rewrite fold_1.s:t
A:Type
i:A
f:elt -> A -> A
fold_left (fun (a : A) (e : elt) => f e a)
  (elements s) i = fold_right f i (rev (elements s)) symmetry.s:t
A:Type
i:A
f:elt -> A -> A
fold_right f i (rev (elements s)) =
fold_left (fun (a : A) (e : elt) => f e a)
  (elements s) i apply fold_left_rev_right.
  Qed.

  Notation NoDup := (NoDupA E.eq).
  Notation InA := (InA E.eq).

Induction principles for fold (contributed by S. Lescuyer)

In the following lemma, the step hypothesis is deliberately restricted to the precise set s we are considering.

  Theorem fold_rec :
    forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A)(s:t),
     (forall s', Empty s' -> P s' i) ->
     (forall x a s' s'', In x s -> ~In x s' -> Add x s' s'' ->
       P s' a -> P s'' (f x a)) ->
     P s (fold f s i).forall (A : Type) (P : t -> A -> Type)
  (f : elt -> A -> A) (i : A) (s : t),
(forall s' : t, Empty s' -> P s' i) ->
(forall (x : elt) (a : A) (s' s'' : t),
 In x s ->
 ~ In x s' -> Add x s' s'' -> P s' a -> P s'' (f x a)) ->
P s (fold f s i)
  Proof.forall (A : Type) (P : t -> A -> Type)
  (f : elt -> A -> A) (i : A) (s : t),
(forall s' : t, Empty s' -> P s' i) ->
(forall (x : elt) (a : A) (s' s'' : t),
 In x s ->
 ~ In x s' -> Add x s' s'' -> P s' a -> P s'' (f x a)) ->
P s (fold f s i)
  intros A P f i s Pempty Pstep.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
s:t
Pempty:forall s' : t, Empty s' -> P s' i
Pstep:forall (x : elt) (a : A) (s' s'' : t),
In x s ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
P s (fold f s i)
  rewrite fold_spec_right.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
s:t
Pempty:forall s' : t, Empty s' -> P s' i
Pstep:forall (x : elt) (a : A) (s' s'' : t),
In x s ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
P s (fold_right f i (rev (elements s))) set (l:=rev (elements s)).A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
s:t
Pempty:forall s' : t, Empty s' -> P s' i
Pstep:forall (x : elt) (a : A) (s' s'' : t),
In x s ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
l:=rev (elements s):list elt
P s (fold_right f i l)
  assert (Pstep' : forall x a s' s'', InA x l -> ~In x s' -> Add x s' s'' ->
           P s' a -> P s'' (f x a)).A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
s:t
Pempty:forall s' : t, Empty s' -> P s' i
Pstep:forall (x : elt) (a : A) (s' s'' : t),
In x s ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
l:=rev (elements s):list elt
forall (x : E.t) (a : A) (s' s'' : t),
InA x l ->
~ In x s' -> Add x s' s'' -> P s' a -> P s'' (f x a)
A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
s:t
Pempty:forall s' : t, Empty s' -> P s' i
Pstep:forall (x : elt) (a : A) (s' s'' : t),
In x s ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
l:=rev (elements s):list elt
Pstep':forall (x : E.t) (a : A) (s' s'' : t),
InA x l ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
P s (fold_right f i l)
   intros; eapply Pstep; eauto.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
s:t
Pempty:forall s'0 : t, Empty s'0 -> P s'0 i
Pstep:forall (x0 : elt) (a0 : A) (s'0 s''0 : t),
In x0 s ->
~ In x0 s'0 ->
Add x0 s'0 s''0 ->
P s'0 a0 -> P s''0 (f x0 a0)
l:=rev (elements s):list elt
x:E.t
a:A
s', s'':t
H:InA x l
H0:~ In x s'
H1:Add x s' s''
X:P s' a
In x s
A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
s:t
Pempty:forall s' : t, Empty s' -> P s' i
Pstep:forall (x : elt) (a : A) (s' s'' : t),
In x s ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
l:=rev (elements s):list elt
Pstep':forall (x : E.t) (a : A) (s' s'' : t),
InA x l ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
P s (fold_right f i l)
   rewrite elements_iff, <- InA_rev; auto with *.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
s:t
Pempty:forall s' : t, Empty s' -> P s' i
Pstep:forall (x : elt) (a : A) (s' s'' : t),
In x s ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
l:=rev (elements s):list elt
Pstep':forall (x : E.t) (a : A) (s' s'' : t),
InA x l ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
P s (fold_right f i l)
  assert (Hdup : NoDup l) by
    (unfold l; eauto using elements_3w, NoDupA_rev with *).A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
s:t
Pempty:forall s' : t, Empty s' -> P s' i
Pstep:forall (x : elt) (a : A) (s' s'' : t),
In x s ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
l:=rev (elements s):list elt
Pstep':forall (x : E.t) (a : A) (s' s'' : t),
InA x l ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
Hdup:NoDup l
P s (fold_right f i l)
  assert (Hsame : forall x, In x s <-> InA x l) by
    (unfold l; intros; rewrite elements_iff, InA_rev; intuition).A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
s:t
Pempty:forall s' : t, Empty s' -> P s' i
Pstep:forall (x : elt) (a : A) (s' s'' : t),
In x s ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
l:=rev (elements s):list elt
Pstep':forall (x : E.t) (a : A) (s' s'' : t),
InA x l ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
Hdup:NoDup l
Hsame:forall x : elt, In x s <-> InA x l
P s (fold_right f i l)
  clear Pstep; clearbody l; revert s Hsame; induction l.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
Pstep':forall (x : E.t) (a : A) (s' s'' : t),
InA x nil ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
Hdup:NoDup nil
forall s : t,
(forall x : elt, In x s <-> InA x nil) ->
P s (fold_right f i nil)
A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s : t,
(forall x : elt, In x s <-> InA x l) ->
P s (fold_right f i l)
forall s : t,
(forall x : elt, In x s <-> InA x (a :: l)) ->
P s (fold_right f i (a :: l))
  (* empty *)
  intros s Hsame; simpl.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
Pstep':forall (x : E.t) (a : A) (s' s'' : t),
InA x nil ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
Hdup:NoDup nil
s:t
Hsame:forall x : elt, In x s <-> InA x nil
P s i
A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s : t,
(forall x : elt, In x s <-> InA x l) ->
P s (fold_right f i l)
forall s : t,
(forall x : elt, In x s <-> InA x (a :: l)) ->
P s (fold_right f i (a :: l))
  apply Pempty.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
Pstep':forall (x : E.t) (a : A) (s' s'' : t),
InA x nil ->
~ In x s' ->
Add x s' s'' -> P s' a -> P s'' (f x a)
Hdup:NoDup nil
s:t
Hsame:forall x : elt, In x s <-> InA x nil
Empty s
A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s : t,
(forall x : elt, In x s <-> InA x l) ->
P s (fold_right f i l)
forall s : t,
(forall x : elt, In x s <-> InA x (a :: l)) ->
P s (fold_right f i (a :: l)) intro x.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
Pstep':forall (x0 : E.t) (a : A) (s' s'' : t),
InA x0 nil ->
~ In x0 s' ->
Add x0 s' s'' -> P s' a -> P s'' (f x0 a)
Hdup:NoDup nil
s:t
Hsame:forall x0 : elt, In x0 s <-> InA x0 nil
x:elt
~ In x s
A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s : t,
(forall x : elt, In x s <-> InA x l) ->
P s (fold_right f i l)
forall s : t,
(forall x : elt, In x s <-> InA x (a :: l)) ->
P s (fold_right f i (a :: l)) rewrite Hsame, InA_nil; intuition.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s : t,
(forall x : elt, In x s <-> InA x l) ->
P s (fold_right f i l)
forall s : t,
(forall x : elt, In x s <-> InA x (a :: l)) ->
P s (fold_right f i (a :: l))
  (* step *)
  intros s Hsame; simpl.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
P s (f a (fold_right f i l))
  apply Pstep' with (of_list l); auto.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
~ In a (of_list l)
A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
Add a (of_list l) s
A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
P (of_list l) (fold_right f i l)
   inversion_clear Hdup; rewrite of_list_1; auto.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
Add a (of_list l) s
A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
P (of_list l) (fold_right f i l)
   red.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
forall y : elt,
In y s <-> E.eq a y \/ In y (of_list l)
A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
P (of_list l) (fold_right f i l) intros.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
y:elt
In y s <-> E.eq a y \/ In y (of_list l)
A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
P (of_list l) (fold_right f i l) rewrite Hsame, of_list_1, InA_cons; intuition.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
P (of_list l) (fold_right f i l)
  apply IHl.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
forall (x : E.t) (a0 : A) (s' s'' : t),
InA x l ->
~ In x s' -> Add x s' s'' -> P s' a0 -> P s'' (f x a0)
A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
NoDup l
A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
forall x : elt, In x (of_list l) <-> InA x l
   intros; eapply Pstep'; eauto.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
NoDup l
A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
forall x : elt, In x (of_list l) <-> InA x l
   inversion_clear Hdup; auto.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
Pempty:forall s' : t, Empty s' -> P s' i
a:elt
l:list elt
Pstep':forall (x : E.t) (a0 : A) (s' s'' : t),
InA x (a :: l) ->
~ In x s' ->
Add x s' s'' -> P s' a0 -> P s'' (f x a0)
Hdup:NoDup (a :: l)
IHl:(forall (x : E.t) (a0 : A) (s' s'' : t),
 InA x l ->
 ~ In x s' ->
 Add x s' s'' -> P s' a0 -> P s'' (f x a0)) ->
NoDup l ->
forall s0 : t,
(forall x : elt, In x s0 <-> InA x l) ->
P s0 (fold_right f i l)
s:t
Hsame:forall x : elt, In x s <-> InA x (a :: l)
forall x : elt, In x (of_list l) <-> InA x l
   exact (of_list_1 l).
  Qed.

Same, with empty and add instead of Empty and Add. In this case, P must be compatible with equality of sets

  Theorem fold_rec_bis :
    forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A)(s:t),
     (forall s s' a, s[=]s' -> P s a -> P s' a) ->
     (P empty i) ->
     (forall x a s', In x s -> ~In x s' -> P s' a -> P (add x s') (f x a)) ->
     P s (fold f s i).forall (A : Type) (P : t -> A -> Type)
  (f : elt -> A -> A) (i : A) (s : t),
(forall (s0 s' : t) (a : A),
 s0 [=] s' -> P s0 a -> P s' a) ->
P empty i ->
(forall (x : elt) (a : A) (s' : t),
 In x s -> ~ In x s' -> P s' a -> P (add x s') (f x a)) ->
P s (fold f s i)
  Proof.forall (A : Type) (P : t -> A -> Type)
  (f : elt -> A -> A) (i : A) (s : t),
(forall (s0 s' : t) (a : A),
 s0 [=] s' -> P s0 a -> P s' a) ->
P empty i ->
(forall (x : elt) (a : A) (s' : t),
 In x s -> ~ In x s' -> P s' a -> P (add x s') (f x a)) ->
P s (fold f s i)
  intros A P f i s Pmorphism Pempty Pstep.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
s:t
Pmorphism:forall (s0 s' : t) (a : A),
s0 [=] s' -> P s0 a -> P s' a
Pempty:P empty i
Pstep:forall (x : elt) (a : A) (s' : t),
In x s ->
~ In x s' -> P s' a -> P (add x s') (f x a)
P s (fold f s i)
  apply fold_rec; intros.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
s:t
Pmorphism:forall (s0 s'0 : t) (a : A),
s0 [=] s'0 -> P s0 a -> P s'0 a
Pempty:P empty i
Pstep:forall (x : elt) (a : A) (s'0 : t),
In x s ->
~ In x s'0 -> P s'0 a -> P (add x s'0) (f x a)
s':t
H:Empty s'
P s' i
A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
s:t
Pmorphism:forall (s0 s'0 : t) (a0 : A),
s0 [=] s'0 -> P s0 a0 -> P s'0 a0
Pempty:P empty i
Pstep:forall (x0 : elt) (a0 : A) (s'0 : t),
In x0 s ->
~ In x0 s'0 ->
P s'0 a0 -> P (add x0 s'0) (f x0 a0)
x:elt
a:A
s', s'':t
H:In x s
H0:~ In x s'
H1:Add x s' s''
X:P s' a
P s'' (f x a)
  apply Pmorphism with empty; auto with set.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
s:t
Pmorphism:forall (s0 s'0 : t) (a0 : A),
s0 [=] s'0 -> P s0 a0 -> P s'0 a0
Pempty:P empty i
Pstep:forall (x0 : elt) (a0 : A) (s'0 : t),
In x0 s ->
~ In x0 s'0 ->
P s'0 a0 -> P (add x0 s'0) (f x0 a0)
x:elt
a:A
s', s'':t
H:In x s
H0:~ In x s'
H1:Add x s' s''
X:P s' a
P s'' (f x a)
  rewrite Add_Equal in H1; auto with set.A:Type
P:t -> A -> Type
f:elt -> A -> A
i:A
s:t
Pmorphism:forall (s0 s'0 : t) (a0 : A),
s0 [=] s'0 -> P s0 a0 -> P s'0 a0
Pempty:P empty i
Pstep:forall (x0 : elt) (a0 : A) (s'0 : t),
In x0 s ->
~ In x0 s'0 ->
P s'0 a0 -> P (add x0 s'0) (f x0 a0)
x:elt
a:A
s', s'':t
H:In x s
H0:~ In x s'
H1:s'' [=] add x s'
X:P s' a
P s'' (f x a)
  apply Pmorphism with (add x s'); auto with set.
  Qed.

  Lemma fold_rec_nodep :
    forall (A:Type)(P : A -> Type)(f : elt -> A -> A)(i:A)(s:t),
     P i -> (forall x a, In x s -> P a -> P (f x a)) ->
     P (fold f s i).forall (A : Type) (P : A -> Type) (f : elt -> A -> A)
  (i : A) (s : t),
P i ->
(forall (x : elt) (a : A), In x s -> P a -> P (f x a)) ->
P (fold f s i)
  Proof.forall (A : Type) (P : A -> Type) (f : elt -> A -> A)
  (i : A) (s : t),
P i ->
(forall (x : elt) (a : A), In x s -> P a -> P (f x a)) ->
P (fold f s i)
  intros; apply fold_rec_bis with (P:=fun _ => P); auto.
  Qed.

fold_rec_weak is a weaker principle than fold_rec_bis : the step hypothesis must here be applicable to any x. At the same time, it looks more like an induction principle, and hence can be easier to use.

  Lemma fold_rec_weak :
    forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A),
    (forall s s' a, s[=]s' -> P s a -> P s' a) ->
    P empty i ->
    (forall x a s, ~In x s -> P s a -> P (add x s) (f x a)) ->
    forall s, P s (fold f s i).forall (A : Type) (P : t -> A -> Type)
  (f : elt -> A -> A) (i : A),
(forall (s s' : t) (a : A),
 s [=] s' -> P s a -> P s' a) ->
P empty i ->
(forall (x : elt) (a : A) (s : t),
 ~ In x s -> P s a -> P (add x s) (f x a)) ->
forall s : t, P s (fold f s i)
  Proof.forall (A : Type) (P : t -> A -> Type)
  (f : elt -> A -> A) (i : A),
(forall (s s' : t) (a : A),
 s [=] s' -> P s a -> P s' a) ->
P empty i ->
(forall (x : elt) (a : A) (s : t),
 ~ In x s -> P s a -> P (add x s) (f x a)) ->
forall s : t, P s (fold f s i)
  intros; apply fold_rec_bis; auto.
  Qed.

  Lemma fold_rel :
    forall (A B:Type)(R : A -> B -> Type)
     (f : elt -> A -> A)(g : elt -> B -> B)(i : A)(j : B)(s : t),
     R i j ->
     (forall x a b, In x s -> R a b -> R (f x a) (g x b)) ->
     R (fold f s i) (fold g s j).forall (A B : Type) (R : A -> B -> Type)
  (f : elt -> A -> A) (g : elt -> B -> B) (i : A)
  (j : B) (s : t),
R i j ->
(forall (x : elt) (a : A) (b : B),
 In x s -> R a b -> R (f x a) (g x b)) ->
R (fold f s i) (fold g s j)
  Proof.forall (A B : Type) (R : A -> B -> Type)
  (f : elt -> A -> A) (g : elt -> B -> B) (i : A)
  (j : B) (s : t),
R i j ->
(forall (x : elt) (a : A) (b : B),
 In x s -> R a b -> R (f x a) (g x b)) ->
R (fold f s i) (fold g s j)
  intros A B R f g i j s Rempty Rstep.A, B:Type
R:A -> B -> Type
f:elt -> A -> A
g:elt -> B -> B
i:A
j:B
s:t
Rempty:R i j
Rstep:forall (x : elt) (a : A) (b : B),
In x s -> R a b -> R (f x a) (g x b)
R (fold f s i) (fold g s j)
  rewrite 2 fold_spec_right.A, B:Type
R:A -> B -> Type
f:elt -> A -> A
g:elt -> B -> B
i:A
j:B
s:t
Rempty:R i j
Rstep:forall (x : elt) (a : A) (b : B),
In x s -> R a b -> R (f x a) (g x b)
R (fold_right f i (rev (elements s)))
  (fold_right g j (rev (elements s))) set (l:=rev (elements s)).A, B:Type
R:A -> B -> Type
f:elt -> A -> A
g:elt -> B -> B
i:A
j:B
s:t
Rempty:R i j
Rstep:forall (x : elt) (a : A) (b : B),
In x s -> R a b -> R (f x a) (g x b)
l:=rev (elements s):list elt
R (fold_right f i l) (fold_right g j l)
  assert (Rstep' : forall x a b, InA x l -> R a b -> R (f x a) (g x b)) by
    (intros; apply Rstep; auto; rewrite elements_iff, <- InA_rev; auto with *).A, B:Type
R:A -> B -> Type
f:elt -> A -> A
g:elt -> B -> B
i:A
j:B
s:t
Rempty:R i j
Rstep:forall (x : elt) (a : A) (b : B),
In x s -> R a b -> R (f x a) (g x b)
l:=rev (elements s):list elt
Rstep':forall (x : E.t) (a : A) (b : B),
InA x l -> R a b -> R (f x a) (g x b)
R (fold_right f i l) (fold_right g j l)
  clearbody l; clear Rstep s.A, B:Type
R:A -> B -> Type
f:elt -> A -> A
g:elt -> B -> B
i:A
j:B
Rempty:R i j
l:list elt
Rstep':forall (x : E.t) (a : A) (b : B),
InA x l -> R a b -> R (f x a) (g x b)
R (fold_right f i l) (fold_right g j l)
  induction l; simpl; auto.
  Qed.

From the induction principle on fold, we can deduce some general induction principles on sets.

  Lemma set_induction :
   forall P : t -> Type,
   (forall s, Empty s -> P s) ->
   (forall s s', P s -> forall x, ~In x s -> Add x s s' -> P s') ->
   forall s, P s.forall P : t -> Type,
(forall s : t, Empty s -> P s) ->
(forall s s' : t,
 P s -> forall x : elt, ~ In x s -> Add x s s' -> P s') ->
forall s : t, P s
  Proof.forall P : t -> Type,
(forall s : t, Empty s -> P s) ->
(forall s s' : t,
 P s -> forall x : elt, ~ In x s -> Add x s s' -> P s') ->
forall s : t, P s
  intros.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : elt, ~ In x s0 -> Add x s0 s' -> P s'
s:t
P s apply (@fold_rec _ (fun s _ => P s) (fun _ _ => tt) tt s); eauto.
  Qed.

  Lemma set_induction_bis :
   forall P : t -> Type,
   (forall s s', s [=] s' -> P s -> P s') ->
   P empty ->
   (forall x s, ~In x s -> P s -> P (add x s)) ->
   forall s, P s.forall P : t -> Type,
(forall s s' : t, s [=] s' -> P s -> P s') ->
P empty ->
(forall (x : elt) (s : t),
 ~ In x s -> P s -> P (add x s)) -> forall s : t, P s
  Proof.forall P : t -> Type,
(forall s s' : t, s [=] s' -> P s -> P s') ->
P empty ->
(forall (x : elt) (s : t),
 ~ In x s -> P s -> P (add x s)) -> forall s : t, P s
  intros.P:t -> Type
X:forall s0 s' : t, s0 [=] s' -> P s0 -> P s'
X0:P empty
X1:forall (x : elt) (s0 : t),
~ In x s0 -> P s0 -> P (add x s0)
s:t
P s
  apply (@fold_rec_bis _ (fun s _ => P s) (fun _ _ => tt) tt s); eauto.
  Qed.

fold can be used to reconstruct the same initial set.

  Lemma fold_identity : forall s, fold add s empty [=] s.forall s : t, fold add s empty [=] s
  Proof.forall s : t, fold add s empty [=] s
  intros.s:t
fold add s empty [=] s
  apply fold_rec with (P:=fun s acc => acc[=]s); auto with set.s:t
forall (x : elt) (a s' s'' : t),
In x s ->
~ In x s' ->
Add x s' s'' -> a [=] s' -> add x a [=] s''
  intros.s:t
x:elt
a, s', s'':t
H:In x s
H0:~ In x s'
H1:Add x s' s''
H2:a [=] s'
add x a [=] s'' rewrite H2; rewrite Add_Equal in H1; auto with set.
  Qed.

Alternative (weaker) specifications for fold

When FSets was first designed, the order in which Ocaml's Set.fold takes the set elements was unspecified. This specification reflects this fact:

  Lemma fold_0 :
      forall s (A : Type) (i : A) (f : elt -> A -> A),
      exists l : list elt,
        NoDup l /\
        (forall x : elt, In x s <-> InA x l) /\
        fold f s i = fold_right f i l.forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
exists l : list elt,
  NoDup l /\
  (forall x : elt, In x s <-> InA x l) /\
  fold f s i = fold_right f i l
  Proof.forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
exists l : list elt,
  NoDup l /\
  (forall x : elt, In x s <-> InA x l) /\
  fold f s i = fold_right f i l
  intros; exists (rev (elements s)); split.s:t
A:Type
i:A
f:elt -> A -> A
NoDup (rev (elements s))
s:t
A:Type
i:A
f:elt -> A -> A
(forall x : elt, In x s <-> InA x (rev (elements s))) /\
fold f s i = fold_right f i (rev (elements s))
  apply NoDupA_rev; auto with *.s:t
A:Type
i:A
f:elt -> A -> A
(forall x : elt, In x s <-> InA x (rev (elements s))) /\
fold f s i = fold_right f i (rev (elements s))
  split; intros.s:t
A:Type
i:A
f:elt -> A -> A
x:elt
In x s <-> InA x (rev (elements s))
s:t
A:Type
i:A
f:elt -> A -> A
fold f s i = fold_right f i (rev (elements s))
  rewrite elements_iff; do 2 rewrite InA_alt.s:t
A:Type
i:A
f:elt -> A -> A
x:elt
(exists y : E.t, E.eq x y /\ List.In y (elements s)) <->
(exists y : E.t,
   E.eq x y /\ List.In y (rev (elements s)))
s:t
A:Type
i:A
f:elt -> A -> A
fold f s i = fold_right f i (rev (elements s))
  split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition.s:t
A:Type
i:A
f:elt -> A -> A
fold f s i = fold_right f i (rev (elements s))
  apply fold_spec_right.
  Qed.

An alternate (and previous) specification for fold was based on the recursive structure of a set. It is now lemmas fold_1 and fold_2.

  Lemma fold_1 :
   forall s (A : Type) (eqA : A -> A -> Prop)
     (st : Equivalence eqA) (i : A) (f : elt -> A -> A),
   Empty s -> eqA (fold f s i) i.forall (s : t) (A : Type) (eqA : A -> A -> Prop),
Equivalence eqA ->
forall (i : A) (f : elt -> A -> A),
Empty s -> eqA (fold f s i) i
  Proof.forall (s : t) (A : Type) (eqA : A -> A -> Prop),
Equivalence eqA ->
forall (i : A) (f : elt -> A -> A),
Empty s -> eqA (fold f s i) i
  unfold Empty; intros; destruct (fold_0 s i f) as (l,(H1, (H2, H3))).s:t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:forall a : elt, ~ In a s
l:list elt
H1:NoDup l
H2:forall x : elt, In x s <-> InA x l
H3:fold f s i = fold_right f i l
eqA (fold f s i) i
  rewrite H3; clear H3.s:t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:forall a : elt, ~ In a s
l:list elt
H1:NoDup l
H2:forall x : elt, In x s <-> InA x l
eqA (fold_right f i l) i
  generalize H H2; clear H H2; case l; simpl; intros.s:t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
l:list elt
H1:NoDup l
H:forall a : elt, ~ In a s
H2:forall x : elt, In x s <-> InA x nil
eqA i i
s:t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
l:list elt
H1:NoDup l
e:elt
l0:list elt
H:forall a : elt, ~ In a s
H2:forall x : elt, In x s <-> InA x (e :: l0)
eqA (f e (fold_right f i l0)) i
  reflexivity.s:t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
l:list elt
H1:NoDup l
e:elt
l0:list elt
H:forall a : elt, ~ In a s
H2:forall x : elt, In x s <-> InA x (e :: l0)
eqA (f e (fold_right f i l0)) i
  elim (H e).s:t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
l:list elt
H1:NoDup l
e:elt
l0:list elt
H:forall a : elt, ~ In a s
H2:forall x : elt, In x s <-> InA x (e :: l0)
In e s
  elim (H2 e); intuition.
  Qed.

  Lemma fold_2 :
   forall s s' x (A : Type) (eqA : A -> A -> Prop)
     (st : Equivalence eqA) (i : A) (f : elt -> A -> A),
   compat_op E.eq eqA f ->
   transpose eqA f ->
   ~ In x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).forall (s s' : t) (x : elt) (A : Type)
  (eqA : A -> A -> Prop),
Equivalence eqA ->
forall (i : A) (f : elt -> A -> A),
compat_op E.eq eqA f ->
transpose eqA f ->
~ In x s ->
Add x s s' -> eqA (fold f s' i) (f x (fold f s i))
  Proof.forall (s s' : t) (x : elt) (A : Type)
  (eqA : A -> A -> Prop),
Equivalence eqA ->
forall (i : A) (f : elt -> A -> A),
compat_op E.eq eqA f ->
transpose eqA f ->
~ In x s ->
Add x s s' -> eqA (fold f s' i) (f x (fold f s i))
  intros; destruct (fold_0 s i f) as (l,(Hl, (Hl1, Hl2)));
    destruct (fold_0 s' i f) as (l',(Hl', (Hl'1, Hl'2))).s, s':t
x:elt
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:transpose eqA f
H1:~ In x s
H2:Add x s s'
l:list elt
Hl:NoDup l
Hl1:forall x0 : elt, In x0 s <-> InA x0 l
Hl2:fold f s i = fold_right f i l
l':list elt
Hl':NoDup l'
Hl'1:forall x0 : elt, In x0 s' <-> InA x0 l'
Hl'2:fold f s' i = fold_right f i l'
eqA (fold f s' i) (f x (fold f s i))
  rewrite Hl2; rewrite Hl'2; clear Hl2 Hl'2.s, s':t
x:elt
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:transpose eqA f
H1:~ In x s
H2:Add x s s'
l:list elt
Hl:NoDup l
Hl1:forall x0 : elt, In x0 s <-> InA x0 l
l':list elt
Hl':NoDup l'
Hl'1:forall x0 : elt, In x0 s' <-> InA x0 l'
eqA (fold_right f i l') (f x (fold_right f i l))
  apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto with *.s, s':t
x:elt
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:transpose eqA f
H1:~ In x s
H2:Add x s s'
l:list elt
Hl:NoDup l
Hl1:forall x0 : elt, In x0 s <-> InA x0 l
l':list elt
Hl':NoDup l'
Hl'1:forall x0 : elt, In x0 s' <-> InA x0 l'
~ InA x l
s, s':t
x:elt
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:transpose eqA f
H1:~ In x s
H2:Add x s s'
l:list elt
Hl:NoDup l
Hl1:forall x0 : elt, In x0 s <-> InA x0 l
l':list elt
Hl':NoDup l'
Hl'1:forall x0 : elt, In x0 s' <-> InA x0 l'
equivlistA E.eq l' (x :: l)
  rewrite <- Hl1; auto.s, s':t
x:elt
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:transpose eqA f
H1:~ In x s
H2:Add x s s'
l:list elt
Hl:NoDup l
Hl1:forall x0 : elt, In x0 s <-> InA x0 l
l':list elt
Hl':NoDup l'
Hl'1:forall x0 : elt, In x0 s' <-> InA x0 l'
equivlistA E.eq l' (x :: l)
  intros a; rewrite InA_cons; rewrite <- Hl1; rewrite <- Hl'1;
   rewrite (H2 a); intuition.
  Qed.

In fact, fold on empty sets is more than equivalent to the initial element, it is Leibniz-equal to it.

  Lemma fold_1b :
   forall s (A : Type)(i : A) (f : elt -> A -> A),
   Empty s -> (fold f s i) = i.forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
Empty s -> fold f s i = i
  Proof.forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
Empty s -> fold f s i = i
  intros.s:t
A:Type
i:A
f:elt -> A -> A
H:Empty s
fold f s i = i
  rewrite M.fold_1.s:t
A:Type
i:A
f:elt -> A -> A
H:Empty s
fold_left (fun (a : A) (e : elt) => f e a)
  (elements s) i = i
  rewrite elements_Empty in H; rewrite H; simpl; auto.
  Qed.

  Section Fold_More.

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

  Lemma fold_commutes : forall i s x,
   eqA (fold f s (f x 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
forall (i : A) (s : t) (x : elt),
eqA (fold f s (f x 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
forall (i : A) (s : t) (x : elt),
eqA (fold f s (f x i)) (f x (fold f s i))
  intros.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:t
x:elt
eqA (fold f s (f x i)) (f x (fold f s i))
  apply fold_rel with (R:=fun u v => eqA u (f x v)); intros.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:t
x:elt
eqA (f x i) (f x 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:t
x, x0:elt
a, b:A
H:In x0 s
H0:eqA a (f x b)
eqA (f x0 a) (f x (f x0 b))
  reflexivity.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:t
x, x0:elt
a, b:A
H:In x0 s
H0:eqA a (f x b)
eqA (f x0 a) (f x (f x0 b))
  transitivity (f x0 (f x b)); 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:t
x, x0:elt
a, b:A
H:In x0 s
H0:eqA a (f x b)
eqA (f x0 a) (f x0 (f x b)) apply Comp; auto with *.
  Qed.

Fold is a morphism

  Lemma fold_init : forall i i' s, eqA i i' ->
   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
forall (i i' : A) (s : t),
eqA i i' -> 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
forall (i i' : A) (s : t),
eqA i i' -> eqA (fold f s i) (fold f s i')
  intros.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, i':A
s:t
H:eqA i i'
eqA (fold f s i) (fold f s i') apply fold_rel with (R:=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, i':A
s:t
H:eqA i i'
forall (x : elt) (a b : A),
In x s -> eqA a b -> eqA (f x a) (f x b)
   intros; apply Comp; auto with *.
  Qed.

  Lemma fold_equal :
   forall i s s', s[=]s' -> 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
forall (i : A) (s s' : t),
s [=] s' -> 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
forall (i : A) (s s' : t),
s [=] s' -> eqA (fold f s i) (fold f s' i)
  intros i s; pattern s; apply set_induction; clear s; intros.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:t
H:Empty s
s':t
H0:s [=] s'
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
H:forall s'1 : t,
s [=] s'1 -> eqA (fold f s i) (fold f s'1 i)
x:elt
H0:~ In x s
H1:Add x s s'
s'0:t
H2:s' [=] s'0
eqA (fold f s' i) (fold f s'0 i)
  transitivity 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:t
H:Empty s
s':t
H0:s [=] s'
eqA (fold f s 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:t
H:Empty s
s':t
H0:s [=] s'
eqA 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
H:forall s'1 : t,
s [=] s'1 -> eqA (fold f s i) (fold f s'1 i)
x:elt
H0:~ In x s
H1:Add x s s'
s'0:t
H2:s' [=] s'0
eqA (fold f s' i) (fold f s'0 i)
  apply fold_1; 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:t
H:Empty s
s':t
H0:s [=] s'
eqA 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
H:forall s'1 : t,
s [=] s'1 -> eqA (fold f s i) (fold f s'1 i)
x:elt
H0:~ In x s
H1:Add x s s'
s'0:t
H2:s' [=] s'0
eqA (fold f s' i) (fold f s'0 i)
  symmetry; apply fold_1; 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:t
H:Empty s
s':t
H0:s [=] s'
Empty s'
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
H:forall s'1 : t,
s [=] s'1 -> eqA (fold f s i) (fold f s'1 i)
x:elt
H0:~ In x s
H1:Add x s s'
s'0:t
H2:s' [=] s'0
eqA (fold f s' i) (fold f s'0 i)
  rewrite <- H0; 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
H:forall s'1 : t,
s [=] s'1 -> eqA (fold f s i) (fold f s'1 i)
x:elt
H0:~ In x s
H1:Add x s s'
s'0:t
H2:s' [=] s'0
eqA (fold f s' i) (fold f s'0 i)
  transitivity (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
H:forall s'1 : t,
s [=] s'1 -> eqA (fold f s i) (fold f s'1 i)
x:elt
H0:~ In x s
H1:Add x s s'
s'0:t
H2:s' [=] s'0
eqA (fold f 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
H:forall s'1 : t,
s [=] s'1 -> eqA (fold f s i) (fold f s'1 i)
x:elt
H0:~ In x s
H1:Add x s s'
s'0:t
H2:s' [=] s'0
eqA (f x (fold f s i)) (fold f s'0 i)
  apply 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
H:forall s'1 : t,
s [=] s'1 -> eqA (fold f s i) (fold f s'1 i)
x:elt
H0:~ In x s
H1:Add x s s'
s'0:t
H2:s' [=] s'0
eqA (f x (fold f s i)) (fold f s'0 i)
  symmetry; apply 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
H:forall s'1 : t,
s [=] s'1 -> eqA (fold f s i) (fold f s'1 i)
x:elt
H0:~ In x s
H1:Add x s s'
s'0:t
H2:s' [=] s'0
Add x s s'0
  unfold Add in *; intros.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
H:forall s'1 : t,
s [=] s'1 -> eqA (fold f s i) (fold f s'1 i)
x:elt
H0:~ In x s
H1:forall y0 : elt,
In y0 s' <-> E.eq x y0 \/ In y0 s
s'0:t
H2:s' [=] s'0
y:elt
In y s'0 <-> E.eq x y \/ In y s
  rewrite <- H2; auto.
  Qed.

Fold and other set operators

  Lemma fold_empty : forall i, 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
forall i : A, 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
forall i : A, fold f empty i = i
  intros i; apply fold_1b; auto with set.
  Qed.

  Lemma fold_add : forall i s x, ~In x s ->
   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
forall (i : A) (s : t) (x : elt),
~ In x s ->
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
forall (i : A) (s : t) (x : elt),
~ In x s ->
eqA (fold f (add x s) i) (f x (fold f s i))
  intros; apply fold_2 with (eqA := eqA); auto with set.
  Qed.

  Lemma add_fold : forall i s x, In x s ->
   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
forall (i : A) (s : t) (x : elt),
In x s -> 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
forall (i : A) (s : t) (x : elt),
In x s -> eqA (fold f (add x s) i) (fold f s i)
  intros; apply fold_equal; auto with set.
  Qed.

  Lemma remove_fold_1: forall i s x, In x s ->
   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
forall (i : A) (s : t) (x : elt),
In x s ->
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
forall (i : A) (s : t) (x : elt),
In x s ->
eqA (f x (fold f (remove x s) i)) (fold f s i)
  intros.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:t
x:elt
H:In x s
eqA (f x (fold f (remove x s) i)) (fold f s i)
  symmetry.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:t
x:elt
H:In x s
eqA (fold f s i) (f x (fold f (remove x s) i))
  apply fold_2 with (eqA:=eqA); auto with set.
  Qed.

  Lemma remove_fold_2: forall i s x, ~In x s ->
   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
forall (i : A) (s : t) (x : elt),
~ In x s -> 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
forall (i : A) (s : t) (x : elt),
~ In x s -> eqA (fold f (remove x s) i) (fold f s i)
  intros.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:t
x:elt
H:~ In x s
eqA (fold f (remove x s) i) (fold f s i)
  apply fold_equal; auto with set.
  Qed.

  Lemma fold_union_inter : forall i s s',
   eqA (fold f (union s s') (fold f (inter 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
forall (i : A) (s s' : t),
eqA (fold f (union s s') (fold f (inter 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
forall (i : A) (s s' : t),
eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
  intros; pattern s; apply set_induction; clear s; intros.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
H:Empty s
eqA (fold f (union s s') (fold f (inter 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, s'0:t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s'0
eqA (fold f (union s'0 s') (fold f (inter s'0 s') i))
  (fold f s'0 (fold f s' i))
  transitivity (fold f s' (fold f (inter s 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
H:Empty s
eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s' (fold f (inter s 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
H:Empty s
eqA (fold f s' (fold f (inter 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, s'0:t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s'0
eqA (fold f (union s'0 s') (fold f (inter s'0 s') i))
  (fold f s'0 (fold f s' i))
  apply fold_equal; auto with set.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
H:Empty s
eqA (fold f s' (fold f (inter 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, s'0:t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s'0
eqA (fold f (union s'0 s') (fold f (inter s'0 s') i))
  (fold f s'0 (fold f s' i))
  transitivity (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
H:Empty s
eqA (fold f s' (fold f (inter s 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
H:Empty s
eqA (fold f 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, s'0:t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s'0
eqA (fold f (union s'0 s') (fold f (inter s'0 s') i))
  (fold f s'0 (fold f s' i))
  apply fold_init; 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
H:Empty s
eqA (fold f (inter s s') 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
H:Empty s
eqA (fold f 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, s'0:t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s'0
eqA (fold f (union s'0 s') (fold f (inter s'0 s') i))
  (fold f s'0 (fold f s' i))
  apply fold_1; auto with set.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
H:Empty s
eqA (fold f 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, s'0:t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s'0
eqA (fold f (union s'0 s') (fold f (inter s'0 s') i))
  (fold f s'0 (fold f s' i))
  symmetry; apply fold_1; 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, s'0:t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s'0
eqA (fold f (union s'0 s') (fold f (inter s'0 s') i))
  (fold f s'0 (fold f s' i))
  rename s'0 into s''.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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
eqA (fold f (union s'' s') (fold f (inter s'' s') i))
  (fold f s'' (fold f s' i))
  destruct (In_dec x s').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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA (fold f (union s'' s') (fold f (inter 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (fold f (union s'' s') (fold f (inter s'' s') i))
  (fold f s'' (fold f s' i))
  (* In x s' *)
  transitivity (fold f (union s'' s') (f x (fold f (inter s s') i))); auto with set.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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA (fold f (union s'' s') (fold f (inter s'' s') i))
  (fold f (union s'' s') (f x (fold f (inter s 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA
  (fold f (union s'' s') (f x (fold f (inter 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (fold f (union s'' s') (fold f (inter s'' s') i))
  (fold f s'' (fold f s' i))
  apply fold_init; 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA (fold f (inter s'' s') i)
  (f x (fold f (inter s 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA
  (fold f (union s'' s') (f x (fold f (inter 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (fold f (union s'' s') (fold f (inter s'' s') i))
  (fold f s'' (fold f s' i))
  apply fold_2 with (eqA:=eqA); auto with set.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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
~ In x (inter s s')
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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA
  (fold f (union s'' s') (f x (fold f (inter 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (fold f (union s'' s') (fold f (inter s'' s') i))
  (fold f s'' (fold f s' i))
  rewrite inter_iff; intuition.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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA
  (fold f (union s'' s') (f x (fold f (inter 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (fold f (union s'' s') (fold f (inter s'' s') i))
  (fold f s'' (fold f s' i))
  transitivity (f x (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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA
  (fold f (union s'' s') (f x (fold f (inter s s') i)))
  (f x (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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA (f x (fold f s (fold f 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (fold f (union s'' s') (fold f (inter s'' s') i))
  (fold f s'' (fold f s' i))
  transitivity (fold f (union s s') (f x (fold f (inter s 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA
  (fold f (union s'' s') (f x (fold f (inter s s') i)))
  (fold f (union s s') (f x (fold f (inter s 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA
  (fold f (union s s') (f x (fold f (inter s s') i)))
  (f x (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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA (f x (fold f s (fold f 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (fold f (union s'' s') (fold f (inter s'' s') i))
  (fold f s'' (fold f s' i))
  apply fold_equal; 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
union s'' s' [=] union s s'
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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA
  (fold f (union s s') (f x (fold f (inter s s') i)))
  (f x (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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA (f x (fold f s (fold f 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (fold f (union s'' s') (fold f (inter s'' s') i))
  (fold f s'' (fold f s' i))
  apply equal_sym; apply union_Equal with x; auto with set.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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA
  (fold f (union s s') (f x (fold f (inter s s') i)))
  (f x (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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA (f x (fold f s (fold f 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (fold f (union s'' s') (fold f (inter s'' s') i))
  (fold f s'' (fold f s' i))
  transitivity (f x (fold f (union s s') (fold f (inter s 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA
  (fold f (union s s') (f x (fold f (inter s s') i)))
  (f x (fold f (union s s') (fold f (inter s 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA
  (f x (fold f (union s s') (fold f (inter s s') i)))
  (f x (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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA (f x (fold f s (fold f 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (fold f (union s'' s') (fold f (inter s'' s') i))
  (fold f s'' (fold f s' i))
  apply fold_commutes; 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA
  (f x (fold f (union s s') (fold f (inter s s') i)))
  (f x (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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA (f x (fold f s (fold f 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (fold f (union s'' s') (fold f (inter s'' s') i))
  (fold f s'' (fold f s' i))
  apply Comp; 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
i0:In x s'
eqA (f x (fold f s (fold f 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (fold f (union s'' s') (fold f (inter s'' s') i))
  (fold f s'' (fold f s' i))
  symmetry; apply 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (fold f (union s'' s') (fold f (inter s'' s') i))
  (fold f s'' (fold f s' i))
  (* ~(In x s') *)
  transitivity (f x (fold f (union s s') (fold f (inter s'' 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (fold f (union s'' s') (fold f (inter s'' s') i))
  (f x (fold f (union s s') (fold f (inter s'' 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA
  (f x (fold f (union s s') (fold f (inter s'' s') i)))
  (fold f s'' (fold f s' i))
  apply fold_2 with (eqA:=eqA); auto with set.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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA
  (f x (fold f (union s s') (fold f (inter s'' s') i)))
  (fold f s'' (fold f s' i))
  transitivity (f x (fold f (union s s') (fold f (inter s 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA
  (f x (fold f (union s s') (fold f (inter s'' s') i)))
  (f x (fold f (union s s') (fold f (inter s 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA
  (f x (fold f (union s s') (fold f (inter s s') i)))
  (fold f s'' (fold f s' i))
  apply Comp;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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (fold f (union s s') (fold f (inter s'' s') i))
  (fold f (union s s') (fold f (inter s 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA
  (f x (fold f (union s s') (fold f (inter s s') i)))
  (fold f s'' (fold f s' i))
  apply fold_init;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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (fold f (inter s'' s') i) (fold f (inter s 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA
  (f x (fold f (union s s') (fold f (inter s s') i)))
  (fold f s'' (fold f s' i))
  apply fold_equal;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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
inter s'' s' [=] inter s s'
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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA
  (f x (fold f (union s s') (fold f (inter s s') i)))
  (fold f s'' (fold f s' i))
  apply equal_sym; apply inter_Add_2 with x; auto with set.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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA
  (f x (fold f (union s s') (fold f (inter s s') i)))
  (fold f s'' (fold f s' i))
  transitivity (f x (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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA
  (f x (fold f (union s s') (fold f (inter s s') i)))
  (f x (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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (f x (fold f s (fold f s' i)))
  (fold f s'' (fold f s' i))
  apply Comp; 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, s'':t
H:eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
x:elt
H0:~ In x s
H1:Add x s s''
n:~ In x s'
eqA (f x (fold f s (fold f s' i)))
  (fold f s'' (fold f s' i))
  symmetry; apply fold_2 with (eqA:=eqA); auto.
  Qed.

  Lemma fold_diff_inter : forall i s s',
   eqA (fold f (diff s s') (fold f (inter s 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
forall (i : A) (s s' : t),
eqA (fold f (diff s s') (fold f (inter s 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
forall (i : A) (s s' : t),
eqA (fold f (diff s s') (fold f (inter s s') i))
  (fold f s i)
  intros.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
eqA (fold f (diff s s') (fold f (inter s s') i))
  (fold f s i)
  transitivity (fold f (union (diff s s') (inter s s'))
               (fold f (inter (diff s s') (inter s 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
eqA (fold f (diff s s') (fold f (inter s s') i))
  (fold f (union (diff s s') (inter s s'))
     (fold f (inter (diff s s') (inter s 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
eqA
  (fold f (union (diff s s') (inter s s'))
     (fold f (inter (diff s s') (inter s s')) i))
  (fold f s i)
  symmetry; apply fold_union_inter; 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
eqA
  (fold f (union (diff s s') (inter s s'))
     (fold f (inter (diff s s') (inter s s')) i))
  (fold f s i)
  transitivity (fold f s (fold f (inter (diff s s') (inter s 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
eqA
  (fold f (union (diff s s') (inter s s'))
     (fold f (inter (diff s s') (inter s s')) i))
  (fold f s
     (fold f (inter (diff s s') (inter s 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
eqA
  (fold f s
     (fold f (inter (diff s s') (inter s s')) i))
  (fold f s i)
  apply fold_equal; auto with set.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
eqA
  (fold f s
     (fold f (inter (diff s s') (inter s s')) i))
  (fold f s i)
  apply fold_init; 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
eqA (fold f (inter (diff s s') (inter s s')) i) i
  apply fold_1; auto with set.
  Qed.

  Lemma fold_union: forall i s s',
   (forall x, ~(In x s/\In x s')) ->
   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
forall (i : A) (s s' : t),
(forall x : elt, ~ (In x s /\ In x s')) ->
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
forall (i : A) (s s' : t),
(forall x : elt, ~ (In x s /\ In x s')) ->
eqA (fold f (union s s') i) (fold f s (fold f s' i))
  intros.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
H:forall x : elt, ~ (In x s /\ In x s')
eqA (fold f (union s s') i) (fold f s (fold f s' i))
  transitivity (fold f (union s s') (fold f (inter s 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
H:forall x : elt, ~ (In x s /\ In x s')
eqA (fold f (union s s') i)
  (fold f (union s s') (fold f (inter s 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
H:forall x : elt, ~ (In x s /\ In x s')
eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
  apply fold_init; 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
H:forall x : elt, ~ (In x s /\ In x s')
eqA i (fold f (inter s 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
H:forall x : elt, ~ (In x s /\ In x s')
eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
  symmetry; apply fold_1; auto with set.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
H:forall x : elt, ~ (In x s /\ In x s')
Empty (inter s s')
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
H:forall x : elt, ~ (In x s /\ In x s')
eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
  unfold Empty; intro a; generalize (H a); set_iff; tauto.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
H:forall x : elt, ~ (In x s /\ In x s')
eqA (fold f (union s s') (fold f (inter s s') i))
  (fold f s (fold f s' i))
  apply fold_union_inter; auto.
  Qed.

  End Fold_More.

  Lemma fold_plus :
   forall s p, fold (fun _ => S) s p = fold (fun _ => S) s 0 + p.forall (s : t) (p : nat),
fold (fun _ : elt => S) s p =
fold (fun _ : elt => S) s 0 + p
  Proof.forall (s : t) (p : nat),
fold (fun _ : elt => S) s p =
fold (fun _ : elt => S) s 0 + p
  intros.s:t
p:nat
fold (fun _ : elt => S) s p =
fold (fun _ : elt => S) s 0 + p apply fold_rel with (R:=fun u v => u = v + p); simpl; auto.
  Qed.

  End Fold.

Cardinal

Characterization of cardinal in terms of fold

  Lemma cardinal_fold : forall s, cardinal s = fold (fun _ => S) s 0.forall s : t, cardinal s = fold (fun _ : elt => S) s 0
  Proof.forall s : t, cardinal s = fold (fun _ : elt => S) s 0
  intros; rewrite cardinal_1; rewrite M.fold_1.s:t
length (elements s) =
fold_left (fun (a : nat) (_ : elt) => S a)
  (elements s) 0
  symmetry; apply fold_left_length; auto.
  Qed.

Old specifications for cardinal.

  Lemma cardinal_0 :
     forall s, exists l : list elt,
        NoDupA E.eq l /\
        (forall x : elt, In x s <-> InA E.eq x l) /\
        cardinal s = length l.forall s : t,
exists l : list elt,
  NoDupA E.eq l /\
  (forall x : elt, In x s <-> InA E.eq x l) /\
  cardinal s = length l
  Proof.forall s : t,
exists l : list elt,
  NoDupA E.eq l /\
  (forall x : elt, In x s <-> InA E.eq x l) /\
  cardinal s = length l
  intros; exists (elements s); intuition; apply cardinal_1.
  Qed.

  Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0.forall s : t, Empty s -> cardinal s = 0
  Proof.forall s : t, Empty s -> cardinal s = 0
  intros; rewrite cardinal_fold; apply fold_1; auto with fset.
  Qed.

  Lemma cardinal_2 :
    forall s s' x, ~ In x s -> Add x s s' -> cardinal s' = S (cardinal s).forall (s s' : t) (x : elt),
~ In x s -> Add x s s' -> cardinal s' = S (cardinal s)
  Proof.forall (s s' : t) (x : elt),
~ In x s -> Add x s s' -> cardinal s' = S (cardinal s)
  intros; do 2 rewrite cardinal_fold.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
fold (fun _ : elt => S) s' 0 =
S (fold (fun _ : elt => S) s 0)
  change S with ((fun _ => S) x).s, s':t
x:elt
H:~ In x s
H0:Add x s s'
fold (fun _ : elt => (fun _ : elt => S) x) s' 0 =
(fun _ : elt => S) x
  (fold (fun _ : elt => (fun _ : elt => S) x) s 0)
  apply fold_2; auto with fset.
  Qed.

Cardinal and (non-)emptiness

  Lemma cardinal_Empty : forall s, Empty s <-> cardinal s = 0.forall s : t, Empty s <-> cardinal s = 0
  Proof.forall s : t, Empty s <-> cardinal s = 0
  intros.s:t
Empty s <-> cardinal s = 0
  rewrite elements_Empty, M.cardinal_1.s:t
elements s = nil <-> length (elements s) = 0
  destruct (elements s); intuition; discriminate.
  Qed.

  Lemma cardinal_inv_1 : forall s, cardinal s = 0 -> Empty s.forall s : t, cardinal s = 0 -> Empty s
  Proof.forall s : t, cardinal s = 0 -> Empty s
  intros; rewrite cardinal_Empty; auto.
  Qed.
  Hint Resolve cardinal_inv_1 : fset.

  Lemma cardinal_inv_2 :
   forall s n, cardinal s = S n -> { x : elt | In x s }.forall (s : t) (n : nat),
cardinal s = S n -> {x : elt | In x s}
  Proof.forall (s : t) (n : nat),
cardinal s = S n -> {x : elt | In x s}
  intros; rewrite M.cardinal_1 in H.s:t
n:nat
H:length (elements s) = S n
{x : elt | In x s}
  generalize (elements_2 (s:=s)).s:t
n:nat
H:length (elements s) = S n
(forall x : elt, InA E.eq x (elements s) -> In x s) ->
{x : elt | In x s}
  destruct (elements s); try discriminate.s:t
n:nat
e:elt
l:list elt
H:length (e :: l) = S n
(forall x : elt, InA E.eq x (e :: l) -> In x s) ->
{x : elt | In x s}
  exists e; auto.
  Qed.

  Lemma cardinal_inv_2b :
   forall s, cardinal s <> 0 -> { x : elt | In x s }.forall s : t, cardinal s <> 0 -> {x : elt | In x s}
  Proof.forall s : t, cardinal s <> 0 -> {x : elt | In x s}
  intro; generalize (@cardinal_inv_2 s); destruct cardinal;
   [intuition|eauto].
  Qed.

Cardinal is a morphism

  Lemma Equal_cardinal : forall s s', s[=]s' -> cardinal s = cardinal s'.forall s s' : t, s [=] s' -> cardinal s = cardinal s'
  Proof.forall s s' : t, s [=] s' -> cardinal s = cardinal s'
  symmetry.s, s':t
H:s [=] s'
cardinal s' = cardinal s
  remember (cardinal s) as n; symmetry in Heqn; revert s s' Heqn H.n:nat
forall s s' : t,
cardinal s = n -> s [=] s' -> cardinal s' = n
  induction n; intros.s, s':t
Heqn:cardinal s = 0
H:s [=] s'
cardinal s' = 0
n:nat
IHn:forall s0 s'0 : t,
cardinal s0 = n ->
s0 [=] s'0 -> cardinal s'0 = n
s, s':t
Heqn:cardinal s = S n
H:s [=] s'
cardinal s' = S n
  apply cardinal_1; rewrite <- H; auto with fset.n:nat
IHn:forall s0 s'0 : t, cardinal s0 = n -> s0 [=] s'0 -> cardinal s'0 = n
s, s':t
Heqn:cardinal s = S n
H:s [=] s'
cardinal s' = S n
  destruct (cardinal_inv_2 Heqn) as (x,H2).n:nat
IHn:forall s0 s'0 : t, cardinal s0 = n -> s0 [=] s'0 -> cardinal s'0 = n
s, s':t
Heqn:cardinal s = S n
H:s [=] s'
x:elt
H2:In x s
cardinal s' = S n
  revert Heqn.n:nat
IHn:forall s0 s'0 : t, cardinal s0 = n -> s0 [=] s'0 -> cardinal s'0 = n
s, s':t
H:s [=] s'
x:elt
H2:In x s
cardinal s = S n -> cardinal s' = S n
  rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); auto with set.n:nat
IHn:forall s0 s'0 : t, cardinal s0 = n -> s0 [=] s'0 -> cardinal s'0 = n
s, s':t
H:s [=] s'
x:elt
H2:In x s
S (cardinal (remove x s)) = S n -> cardinal s' = S n
  rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); eauto with set.
  Qed.

  Add Morphism cardinal with signature (Equal ==> Logic.eq) as cardinal_m.forall x y : t, x [=] y -> cardinal x = cardinal y
  Proof.forall x y : t, x [=] y -> cardinal x = cardinal y
  exact Equal_cardinal.
  Qed.

  Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : fset.

Cardinal and set operators

  Lemma empty_cardinal : cardinal empty = 0.cardinal empty = 0
  Proof.cardinal empty = 0
  rewrite cardinal_fold; apply fold_1; auto with set fset.
  Qed.

  Hint Immediate empty_cardinal cardinal_1 : set.

  Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1.forall x : elt, cardinal (singleton x) = 1
  Proof.forall x : elt, cardinal (singleton x) = 1
  intros.x:elt
cardinal (singleton x) = 1
  rewrite (singleton_equal_add x).x:elt
cardinal (add x empty) = 1
  replace 0 with (cardinal empty); auto with set.x:elt
cardinal (add x empty) = S (cardinal empty)
  apply cardinal_2 with x; auto with set.
  Qed.

  Hint Resolve singleton_cardinal: set.

  Lemma diff_inter_cardinal :
   forall s s', cardinal (diff s s') + cardinal (inter s s') = cardinal s .forall s s' : t,
cardinal (diff s s') + cardinal (inter s s') =
cardinal s
  Proof.forall s s' : t,
cardinal (diff s s') + cardinal (inter s s') =
cardinal s
  intros; do 3 rewrite cardinal_fold.s, s':t
fold (fun _ : elt => S) (diff s s') 0 +
fold (fun _ : elt => S) (inter s s') 0 =
fold (fun _ : elt => S) s 0
  rewrite <- fold_plus.s, s':t
fold (fun _ : elt => S) (diff s s')
  (fold (fun _ : elt => S) (inter s s') 0) =
fold (fun _ : elt => S) s 0
  apply fold_diff_inter with (eqA:=@Logic.eq nat); auto with fset.
  Qed.

  Lemma union_cardinal:
   forall s s', (forall x, ~(In x s/\In x s')) ->
   cardinal (union s s')=cardinal s+cardinal s'.forall s s' : t,
(forall x : elt, ~ (In x s /\ In x s')) ->
cardinal (union s s') = cardinal s + cardinal s'
  Proof.forall s s' : t,
(forall x : elt, ~ (In x s /\ In x s')) ->
cardinal (union s s') = cardinal s + cardinal s'
  intros; do 3 rewrite cardinal_fold.s, s':t
H:forall x : elt, ~ (In x s /\ In x s')
fold (fun _ : elt => S) (union s s') 0 =
fold (fun _ : elt => S) s 0 +
fold (fun _ : elt => S) s' 0
  rewrite <- fold_plus.s, s':t
H:forall x : elt, ~ (In x s /\ In x s')
fold (fun _ : elt => S) (union s s') 0 =
fold (fun _ : elt => S) s
  (fold (fun _ : elt => S) s' 0)
  apply fold_union; auto with fset.
  Qed.

  Lemma subset_cardinal :
   forall s s', s[<=]s' -> cardinal s <= cardinal s' .forall s s' : t,
s [<=] s' -> cardinal s <= cardinal s'
  Proof.forall s s' : t,
s [<=] s' -> cardinal s <= cardinal s'
  intros.s, s':t
H:s [<=] s'
cardinal s <= cardinal s'
  rewrite <- (diff_inter_cardinal s' s).s, s':t
H:s [<=] s'
cardinal s <=
cardinal (diff s' s) + cardinal (inter s' s)
  rewrite (inter_sym s' s).s, s':t
H:s [<=] s'
cardinal s <=
cardinal (diff s' s) + cardinal (inter s s')
  rewrite (inter_subset_equal H); auto with arith.
  Qed.

  Lemma subset_cardinal_lt :
   forall s s' x, s[<=]s' -> In x s' -> ~In x s -> cardinal s < cardinal s'.forall (s s' : t) (x : elt),
s [<=] s' ->
In x s' -> ~ In x s -> cardinal s < cardinal s'
  Proof.forall (s s' : t) (x : elt),
s [<=] s' ->
In x s' -> ~ In x s -> cardinal s < cardinal s'
  intros.s, s':t
x:elt
H:s [<=] s'
H0:In x s'
H1:~ In x s
cardinal s < cardinal s'
  rewrite <- (diff_inter_cardinal s' s).s, s':t
x:elt
H:s [<=] s'
H0:In x s'
H1:~ In x s
cardinal s <
cardinal (diff s' s) + cardinal (inter s' s)
  rewrite (inter_sym s' s).s, s':t
x:elt
H:s [<=] s'
H0:In x s'
H1:~ In x s
cardinal s <
cardinal (diff s' s) + cardinal (inter s s')
  rewrite (inter_subset_equal H).s, s':t
x:elt
H:s [<=] s'
H0:In x s'
H1:~ In x s
cardinal s < cardinal (diff s' s) + cardinal s
  generalize (@cardinal_inv_1 (diff s' s)).s, s':t
x:elt
H:s [<=] s'
H0:In x s'
H1:~ In x s
(cardinal (diff s' s) = 0 -> Empty (diff s' s)) ->
cardinal s < cardinal (diff s' s) + cardinal s
  destruct (cardinal (diff s' s)).s, s':t
x:elt
H:s [<=] s'
H0:In x s'
H1:~ In x s
(0 = 0 -> Empty (diff s' s)) ->
cardinal s < 0 + cardinal s
s, s':t
x:elt
H:s [<=] s'
H0:In x s'
H1:~ In x s
n:nat
(S n = 0 -> Empty (diff s' s)) ->
cardinal s < S n + cardinal s
  intro H2; destruct (H2 Logic.eq_refl x).s, s':t
x:elt
H:s [<=] s'
H0:In x s'
H1:~ In x s
H2:0 = 0 -> Empty (diff s' s)
In x (diff s' s)
s, s':t
x:elt
H:s [<=] s'
H0:In x s'
H1:~ In x s
n:nat
(S n = 0 -> Empty (diff s' s)) ->
cardinal s < S n + cardinal s
  set_iff; auto.s, s':t
x:elt
H:s [<=] s'
H0:In x s'
H1:~ In x s
n:nat
(S n = 0 -> Empty (diff s' s)) ->
cardinal s < S n + cardinal s
  intros _.s, s':t
x:elt
H:s [<=] s'
H0:In x s'
H1:~ In x s
n:nat
cardinal s < S n + cardinal s
  change (0 + cardinal s < S n + cardinal s).s, s':t
x:elt
H:s [<=] s'
H0:In x s'
H1:~ In x s
n:nat
0 + cardinal s < S n + cardinal s
  apply Plus.plus_lt_le_compat; auto with arith.
  Qed.

  Theorem union_inter_cardinal :
   forall s s', cardinal (union s s') + cardinal (inter s s')  = cardinal s  + cardinal s' .forall s s' : t,
cardinal (union s s') + cardinal (inter s s') =
cardinal s + cardinal s'
  Proof.forall s s' : t,
cardinal (union s s') + cardinal (inter s s') =
cardinal s + cardinal s'
  intros.s, s':t
cardinal (union s s') + cardinal (inter s s') =
cardinal s + cardinal s'
  do 4 rewrite cardinal_fold.s, s':t
fold (fun _ : elt => S) (union s s') 0 +
fold (fun _ : elt => S) (inter s s') 0 =
fold (fun _ : elt => S) s 0 +
fold (fun _ : elt => S) s' 0
  do 2 rewrite <- fold_plus.s, s':t
fold (fun _ : elt => S) (union s s')
  (fold (fun _ : elt => S) (inter s s') 0) =
fold (fun _ : elt => S) s
  (fold (fun _ : elt => S) s' 0)
  apply fold_union_inter with (eqA:=@Logic.eq nat); auto with fset.
  Qed.

  Lemma union_cardinal_inter :
   forall s s', cardinal (union s s') = cardinal s + cardinal s' - cardinal (inter s s').forall s s' : t,
cardinal (union s s') =
cardinal s + cardinal s' - cardinal (inter s s')
  Proof.forall s s' : t,
cardinal (union s s') =
cardinal s + cardinal s' - cardinal (inter s s')
  intros.s, s':t
cardinal (union s s') =
cardinal s + cardinal s' - cardinal (inter s s')
  rewrite <- union_inter_cardinal.s, s':t
cardinal (union s s') =
cardinal (union s s') + cardinal (inter s s') -
cardinal (inter s s')
  rewrite Plus.plus_comm.s, s':t
cardinal (union s s') =
cardinal (inter s s') + cardinal (union s s') -
cardinal (inter s s')
  auto with arith.
  Qed.

  Lemma union_cardinal_le :
   forall s s', cardinal (union s s') <= cardinal s  + cardinal s'.forall s s' : t,
cardinal (union s s') <= cardinal s + cardinal s'
  Proof.forall s s' : t,
cardinal (union s s') <= cardinal s + cardinal s'
   intros; generalize (union_inter_cardinal s s').s, s':t
cardinal (union s s') + cardinal (inter s s') =
cardinal s + cardinal s' ->
cardinal (union s s') <= cardinal s + cardinal s'
   intros; rewrite <- H; auto with arith.
  Qed.

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

  Lemma add_cardinal_2 :
   forall s x, ~In x s -> cardinal (add x s) = S (cardinal s).forall (s : t) (x : elt),
~ In x s -> cardinal (add x s) = S (cardinal s)
  Proof.forall (s : t) (x : elt),
~ In x s -> cardinal (add x s) = S (cardinal s)
  intros.s:t
x:elt
H:~ In x s
cardinal (add x s) = S (cardinal s)
  do 2 rewrite cardinal_fold.s:t
x:elt
H:~ In x s
fold (fun _ : elt => S) (add x s) 0 =
S (fold (fun _ : elt => S) s 0)
  change S with ((fun _ => S) x);
   apply fold_add with (eqA:=@Logic.eq nat); auto with fset.
  Qed.

  Lemma remove_cardinal_1 :
   forall s x, In x s -> S (cardinal (remove x s)) = cardinal s.forall (s : t) (x : elt),
In x s -> S (cardinal (remove x s)) = cardinal s
  Proof.forall (s : t) (x : elt),
In x s -> S (cardinal (remove x s)) = cardinal s
  intros.s:t
x:elt
H:In x s
S (cardinal (remove x s)) = cardinal s
  do 2 rewrite cardinal_fold.s:t
x:elt
H:In x s
S (fold (fun _ : elt => S) (remove x s) 0) =
fold (fun _ : elt => S) s 0
  change S with ((fun _ =>S) x).s:t
x:elt
H:In x s
(fun _ : elt => S) x
  (fold (fun _ : elt => (fun _ : elt => S) x)
     (remove x s) 0) =
fold (fun _ : elt => (fun _ : elt => S) x) s 0
  apply remove_fold_1 with (eqA:=@Logic.eq nat); auto with fset.
  Qed.

  Lemma remove_cardinal_2 :
   forall s x, ~In x s -> cardinal (remove x s) = cardinal s.forall (s : t) (x : elt),
~ In x s -> cardinal (remove x s) = cardinal s
  Proof.forall (s : t) (x : elt),
~ In x s -> cardinal (remove x s) = cardinal s
  auto with set fset.
  Qed.

  Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : fset.

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

Module WProperties (M:WS) := WProperties_fun M.E M.
Module Properties := WProperties.

Now comes some properties specific to the element ordering, invalid for Weak Sets.

Module OrdProperties (M:S).
  Module ME:=OrderedTypeFacts(M.E).
  Module Import P := Properties M.
  Import FM.
  Import M.E.
  Import M.

First, a specialized version of SortA_equivlistA_eqlistA:

  Lemma sort_equivlistA_eqlistA : forall l l' : list elt,
   sort E.lt l -> sort E.lt l' -> equivlistA E.eq l l' -> eqlistA E.eq l l'.forall l l' : list elt,
Sorted E.lt l ->
Sorted E.lt l' ->
equivlistA E.eq l l' -> eqlistA E.eq l l'
  Proof.forall l l' : list elt,
Sorted E.lt l ->
Sorted E.lt l' ->
equivlistA E.eq l l' -> eqlistA E.eq l l'
  apply SortA_equivlistA_eqlistA; eauto with *.
  Qed.

  Definition gtb x y := match E.compare x y with GT _ => true | _ => false end.
  Definition leb x := fun y => negb (gtb x y).

  Definition elements_lt x s := List.filter (gtb x) (elements s).
  Definition elements_ge x s := List.filter (leb x) (elements s).

  Lemma gtb_1 : forall x y, gtb x y = true <-> E.lt y x.forall x y : E.t, gtb x y = true <-> E.lt y x
  Proof.forall x y : E.t, gtb x y = true <-> E.lt y x
   intros; unfold gtb; destruct (E.compare x y); intuition; try discriminate; ME.order.
  Qed.

  Lemma leb_1 : forall x y, leb x y = true <-> ~E.lt y x.forall x y : E.t, leb x y = true <-> ~ E.lt y x
  Proof.forall x y : E.t, leb x y = true <-> ~ E.lt y x
   intros; unfold leb, gtb; destruct (E.compare x y); intuition; try discriminate; ME.order.
  Qed.

  Lemma gtb_compat : forall x, Proper (E.eq==>Logic.eq) (gtb x).forall x : E.t, Proper (E.eq ==> Logic.eq) (gtb x)
  Proof.forall x : E.t, Proper (E.eq ==> Logic.eq) (gtb x)
   red; intros x a b H.x, a, b:E.t
H:E.eq a b
gtb x a = gtb x b
   generalize (gtb_1 x a)(gtb_1 x b); destruct (gtb x a); destruct (gtb x b); auto.x, a, b:E.t
H:E.eq a b
true = true <-> E.lt a x ->
false = true <-> E.lt b x -> true = false
x, a, b:E.t
H:E.eq a b
false = true <-> E.lt a x ->
true = true <-> E.lt b x -> false = true
   intros.x, a, b:E.t
H:E.eq a b
H0:true = true <-> E.lt a x
H1:false = true <-> E.lt b x
true = false
x, a, b:E.t
H:E.eq a b
false = true <-> E.lt a x ->
true = true <-> E.lt b x -> false = true
   symmetry; rewrite H1.x, a, b:E.t
H:E.eq a b
H0:true = true <-> E.lt a x
H1:false = true <-> E.lt b x
E.lt b x
x, a, b:E.t
H:E.eq a b
false = true <-> E.lt a x ->
true = true <-> E.lt b x -> false = true
   apply ME.eq_lt with a; auto.x, a, b:E.t
H:E.eq a b
H0:true = true <-> E.lt a x
H1:false = true <-> E.lt b x
E.lt a x
x, a, b:E.t
H:E.eq a b
false = true <-> E.lt a x ->
true = true <-> E.lt b x -> false = true
   rewrite <- H0; auto.x, a, b:E.t
H:E.eq a b
false = true <-> E.lt a x ->
true = true <-> E.lt b x -> false = true
   intros.x, a, b:E.t
H:E.eq a b
H0:false = true <-> E.lt a x
H1:true = true <-> E.lt b x
false = true
   rewrite H0.x, a, b:E.t
H:E.eq a b
H0:false = true <-> E.lt a x
H1:true = true <-> E.lt b x
E.lt a x
   apply ME.eq_lt with b; auto.x, a, b:E.t
H:E.eq a b
H0:false = true <-> E.lt a x
H1:true = true <-> E.lt b x
E.lt b x
   rewrite <- H1; auto.
  Qed.

  Lemma leb_compat : forall x, Proper (E.eq==>Logic.eq) (leb x).forall x : E.t, Proper (E.eq ==> Logic.eq) (leb x)
  Proof.forall x : E.t, Proper (E.eq ==> Logic.eq) (leb x)
   red; intros x a b H; unfold leb.x, a, b:E.t
H:E.eq a b
negb (gtb x a) = negb (gtb x b)
   f_equal; apply gtb_compat; auto.
  Qed.
  Hint Resolve gtb_compat leb_compat : fset.

  Lemma elements_split : forall x s,
   elements s = elements_lt x s ++ elements_ge x s.forall (x : E.t) (s : t),
elements s = elements_lt x s ++ elements_ge x s
  Proof.forall (x : E.t) (s : t),
elements s = elements_lt x s ++ elements_ge x s
  unfold elements_lt, elements_ge, leb; intros.x:E.t
s:t
elements s =
List.filter (gtb x) (elements s) ++
List.filter (fun y : E.t => negb (gtb x y))
  (elements s)
  eapply (@filter_split _ E.eq _ E.lt); auto with *.x:E.t
s:t
forall x0 y : E.t,
gtb x x0 = true -> gtb x y = false -> E.lt x0 y
  intros.x:E.t
s:t
x0, y:E.t
H:gtb x x0 = true
H0:gtb x y = false
E.lt x0 y
  rewrite gtb_1 in H.x:E.t
s:t
x0, y:E.t
H:E.lt x0 x
H0:gtb x y = false
E.lt x0 y
  assert (~E.lt y x).x:E.t
s:t
x0, y:E.t
H:E.lt x0 x
H0:gtb x y = false
~ E.lt y x
x:E.t
s:t
x0, y:E.t
H:E.lt x0 x
H0:gtb x y = false
H1:~ E.lt y x
E.lt x0 y
   unfold gtb in *; destruct (E.compare x y); intuition;
   try discriminate; ME.order.x:E.t
s:t
x0, y:E.t
H:E.lt x0 x
H0:gtb x y = false
H1:~ E.lt y x
E.lt x0 y
  ME.order.
  Qed.

  Lemma elements_Add : forall s s' x, ~In x s -> Add x s s' ->
    eqlistA E.eq (elements s') (elements_lt x s ++ x :: elements_ge x s).forall (s s' : t) (x : elt),
~ In x s ->
Add x s s' ->
eqlistA E.eq (elements s')
  (elements_lt x s ++ x :: elements_ge x s)
  Proof.forall (s s' : t) (x : elt),
~ In x s ->
Add x s s' ->
eqlistA E.eq (elements s')
  (elements_lt x s ++ x :: elements_ge x s)
  intros; unfold elements_ge, elements_lt.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
eqlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  apply sort_equivlistA_eqlistA; auto with set.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
Sorted E.lt
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  apply (@SortA_app _ E.eq); auto with *.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
Sorted E.lt (List.filter (gtb x) (elements s))
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
Sorted E.lt (x :: List.filter (leb x) (elements s))
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
forall x0 y : E.t,
InA E.eq x0 (List.filter (gtb x) (elements s)) ->
InA E.eq y (x :: List.filter (leb x) (elements s)) ->
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  apply (@filter_sort _ E.eq); auto with *.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
Sorted E.lt (x :: List.filter (leb x) (elements s))
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
forall x0 y : E.t,
InA E.eq x0 (List.filter (gtb x) (elements s)) ->
InA E.eq y (x :: List.filter (leb x) (elements s)) ->
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  constructor; auto.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
Sorted E.lt (List.filter (leb x) (elements s))
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
HdRel E.lt x (List.filter (leb x) (elements s))
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
forall x0 y : E.t,
InA E.eq x0 (List.filter (gtb x) (elements s)) ->
InA E.eq y (x :: List.filter (leb x) (elements s)) ->
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  apply (@filter_sort _ E.eq); auto with *.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
HdRel E.lt x (List.filter (leb x) (elements s))
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
forall x0 y : E.t,
InA E.eq x0 (List.filter (gtb x) (elements s)) ->
InA E.eq y (x :: List.filter (leb x) (elements s)) ->
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  rewrite ME.Inf_alt by (apply (@filter_sort _ E.eq); eauto with *).s, s':t
x:elt
H:~ In x s
H0:Add x s s'
forall y : E.t,
InA E.eq y (List.filter (leb x) (elements s)) ->
E.lt x y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
forall x0 y : E.t,
InA E.eq x0 (List.filter (gtb x) (elements s)) ->
InA E.eq y (x :: List.filter (leb x) (elements s)) ->
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  intros.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
y:E.t
H1:InA E.eq y (List.filter (leb x) (elements s))
E.lt x y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
forall x0 y : E.t,
InA E.eq x0 (List.filter (gtb x) (elements s)) ->
InA E.eq y (x :: List.filter (leb x) (elements s)) ->
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  rewrite filter_InA in H1; auto with *; destruct H1.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
y:E.t
H1:InA E.eq y (elements s)
H2:leb x y = true
E.lt x y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
forall x0 y : E.t,
InA E.eq x0 (List.filter (gtb x) (elements s)) ->
InA E.eq y (x :: List.filter (leb x) (elements s)) ->
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  rewrite leb_1 in H2.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
y:E.t
H1:InA E.eq y (elements s)
H2:~ E.lt y x
E.lt x y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
forall x0 y : E.t,
InA E.eq x0 (List.filter (gtb x) (elements s)) ->
InA E.eq y (x :: List.filter (leb x) (elements s)) ->
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  rewrite <- elements_iff in H1.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
y:E.t
H1:In y s
H2:~ E.lt y x
E.lt x y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
forall x0 y : E.t,
InA E.eq x0 (List.filter (gtb x) (elements s)) ->
InA E.eq y (x :: List.filter (leb x) (elements s)) ->
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  assert (~E.eq x y).s, s':t
x:elt
H:~ In x s
H0:Add x s s'
y:E.t
H1:In y s
H2:~ E.lt y x
~ E.eq x y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
y:E.t
H1:In y s
H2:~ E.lt y x
H3:~ E.eq x y
E.lt x y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
forall x0 y : E.t,
InA E.eq x0 (List.filter (gtb x) (elements s)) ->
InA E.eq y (x :: List.filter (leb x) (elements s)) ->
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
   contradict H; rewrite H; auto.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
y:E.t
H1:In y s
H2:~ E.lt y x
H3:~ E.eq x y
E.lt x y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
forall x0 y : E.t,
InA E.eq x0 (List.filter (gtb x) (elements s)) ->
InA E.eq y (x :: List.filter (leb x) (elements s)) ->
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  ME.order.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
forall x0 y : E.t,
InA E.eq x0 (List.filter (gtb x) (elements s)) ->
InA E.eq y (x :: List.filter (leb x) (elements s)) ->
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  intros.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
x0, y:E.t
H1:InA E.eq x0 (List.filter (gtb x) (elements s))
H2:InA E.eq y
  (x :: List.filter (leb x) (elements s))
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  rewrite filter_InA in H1; auto with *; destruct H1.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
x0, y:E.t
H1:InA E.eq x0 (elements s)
H3:gtb x x0 = true
H2:InA E.eq y
  (x :: List.filter (leb x) (elements s))
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  rewrite gtb_1 in H3.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
x0, y:E.t
H1:InA E.eq x0 (elements s)
H3:E.lt x0 x
H2:InA E.eq y
  (x :: List.filter (leb x) (elements s))
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  inversion_clear H2.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
x0, y:E.t
H1:InA E.eq x0 (elements s)
H3:E.lt x0 x
H4:E.eq y x
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
x0, y:E.t
H1:InA E.eq x0 (elements s)
H3:E.lt x0 x
H4:InA E.eq y (List.filter (leb x) (elements s))
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  ME.order.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
x0, y:E.t
H1:InA E.eq x0 (elements s)
H3:E.lt x0 x
H4:InA E.eq y (List.filter (leb x) (elements s))
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  rewrite filter_InA in H4; auto with *; destruct H4.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
x0, y:E.t
H1:InA E.eq x0 (elements s)
H3:E.lt x0 x
H2:InA E.eq y (elements s)
H4:leb x y = true
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  rewrite leb_1 in H4.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
x0, y:E.t
H1:InA E.eq x0 (elements s)
H3:E.lt x0 x
H2:InA E.eq y (elements s)
H4:~ E.lt y x
E.lt x0 y
s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  ME.order.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
equivlistA E.eq (elements s')
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  red; intros a.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
a:E.t
InA E.eq a (elements s') <->
InA E.eq a
  (List.filter (gtb x) (elements s) ++
   x :: List.filter (leb x) (elements s))
  rewrite InA_app_iff, InA_cons, !filter_InA, <-elements_iff,
   leb_1, gtb_1, (H0 a) by auto with *.s, s':t
x:elt
H:~ In x s
H0:Add x s s'
a:E.t
E.eq x a \/ In a s <->
InA E.eq a (elements s) /\ E.lt a x \/
E.eq a x \/ InA E.eq a (elements s) /\ ~ E.lt a x
  intuition.s, s':t
x:elt
H:In x s -> False
H0:Add x s s'
a:E.t
H2:In a s
InA E.eq a (elements s) /\ E.lt a x \/
E.eq a x \/
InA E.eq a (elements s) /\ (E.lt a x -> False)
  destruct (E.compare a x); intuition.s, s':t
x:elt
H:In x s -> False
H0:Add x s s'
a:E.t
H2:In a s
l:E.lt x a
InA E.eq a (elements s) /\ E.lt a x \/
E.eq a x \/
InA E.eq a (elements s) /\ (E.lt a x -> False)
  fold (~E.lt a x); auto with *.
  Qed.

  Definition Above x s := forall y, In y s -> E.lt y x.
  Definition Below x s := forall y, In y s -> E.lt x y.

  Lemma elements_Add_Above : forall s s' x,
   Above x s -> Add x s s' ->
     eqlistA E.eq (elements s') (elements s ++ x::nil).forall (s s' : t) (x : E.t),
Above x s ->
Add x s s' ->
eqlistA E.eq (elements s') (elements s ++ x :: nil)
  Proof.forall (s s' : t) (x : E.t),
Above x s ->
Add x s s' ->
eqlistA E.eq (elements s') (elements s ++ x :: nil)
  intros.s, s':t
x:E.t
H:Above x s
H0:Add x s s'
eqlistA E.eq (elements s') (elements s ++ x :: nil)
  apply sort_equivlistA_eqlistA; auto with *.s, s':t
x:E.t
H:Above x s
H0:Add x s s'
Sorted E.lt (elements s ++ x :: nil)
s, s':t
x:E.t
H:Above x s
H0:Add x s s'
equivlistA E.eq (elements s') (elements s ++ x :: nil)
  apply (@SortA_app _ E.eq); auto with *.s, s':t
x:E.t
H:Above x s
H0:Add x s s'
forall x0 y : E.t,
InA E.eq x0 (elements s) ->
InA E.eq y (x :: nil) -> E.lt x0 y
s, s':t
x:E.t
H:Above x s
H0:Add x s s'
equivlistA E.eq (elements s') (elements s ++ x :: nil)
  intros.s, s':t
x:E.t
H:Above x s
H0:Add x s s'
x0, y:E.t
H1:InA E.eq x0 (elements s)
H2:InA E.eq y (x :: nil)
E.lt x0 y
s, s':t
x:E.t
H:Above x s
H0:Add x s s'
equivlistA E.eq (elements s') (elements s ++ x :: nil)
  inversion_clear H2.s, s':t
x:E.t
H:Above x s
H0:Add x s s'
x0, y:E.t
H1:InA E.eq x0 (elements s)
H3:E.eq y x
E.lt x0 y
s, s':t
x:E.t
H:Above x s
H0:Add x s s'
x0, y:E.t
H1:InA E.eq x0 (elements s)
H3:InA E.eq y nil
E.lt x0 y
s, s':t
x:E.t
H:Above x s
H0:Add x s s'
equivlistA E.eq (elements s') (elements s ++ x :: nil)
  rewrite <- elements_iff in H1.s, s':t
x:E.t
H:Above x s
H0:Add x s s'
x0, y:E.t
H1:In x0 s
H3:E.eq y x
E.lt x0 y
s, s':t
x:E.t
H:Above x s
H0:Add x s s'
x0, y:E.t
H1:InA E.eq x0 (elements s)
H3:InA E.eq y nil
E.lt x0 y
s, s':t
x:E.t
H:Above x s
H0:Add x s s'
equivlistA E.eq (elements s') (elements s ++ x :: nil)
  apply ME.lt_eq with x; auto.s, s':t
x:E.t
H:Above x s
H0:Add x s s'
x0, y:E.t
H1:InA E.eq x0 (elements s)
H3:InA E.eq y nil
E.lt x0 y
s, s':t
x:E.t
H:Above x s
H0:Add x s s'
equivlistA E.eq (elements s') (elements s ++ x :: nil)
  inversion H3.s, s':t
x:E.t
H:Above x s
H0:Add x s s'
equivlistA E.eq (elements s') (elements s ++ x :: nil)
  red; intros a.s, s':t
x:E.t
H:Above x s
H0:Add x s s'
a:E.t
InA E.eq a (elements s') <->
InA E.eq a (elements s ++ x :: nil)
  rewrite InA_app_iff, InA_cons, InA_nil by auto with *.s, s':t
x:E.t
H:Above x s
H0:Add x s s'
a:E.t
InA E.eq a (elements s') <->
InA E.eq a (elements s) \/ E.eq a x \/ False
  do 2 rewrite <- elements_iff; rewrite (H0 a); intuition.
  Qed.

  Lemma elements_Add_Below : forall s s' x,
   Below x s -> Add x s s' ->
     eqlistA E.eq (elements s') (x::elements s).forall (s s' : t) (x : E.t),
Below x s ->
Add x s s' ->
eqlistA E.eq (elements s') (x :: elements s)
  Proof.forall (s s' : t) (x : E.t),
Below x s ->
Add x s s' ->
eqlistA E.eq (elements s') (x :: elements s)
  intros.s, s':t
x:E.t
H:Below x s
H0:Add x s s'
eqlistA E.eq (elements s') (x :: elements s)
  apply sort_equivlistA_eqlistA; auto with *.s, s':t
x:E.t
H:Below x s
H0:Add x s s'
Sorted E.lt (x :: elements s)
s, s':t
x:E.t
H:Below x s
H0:Add x s s'
equivlistA E.eq (elements s') (x :: elements s)
  change (sort E.lt ((x::nil) ++ elements s)).s, s':t
x:E.t
H:Below x s
H0:Add x s s'
Sorted E.lt ((x :: nil) ++ elements s)
s, s':t
x:E.t
H:Below x s
H0:Add x s s'
equivlistA E.eq (elements s') (x :: elements s)
  apply (@SortA_app _ E.eq); auto with *.s, s':t
x:E.t
H:Below x s
H0:Add x s s'
forall x0 y : E.t,
InA E.eq x0 (x :: nil) ->
InA E.eq y (elements s) -> E.lt x0 y
s, s':t
x:E.t
H:Below x s
H0:Add x s s'
equivlistA E.eq (elements s') (x :: elements s)
  intros.s, s':t
x:E.t
H:Below x s
H0:Add x s s'
x0, y:E.t
H1:InA E.eq x0 (x :: nil)
H2:InA E.eq y (elements s)
E.lt x0 y
s, s':t
x:E.t
H:Below x s
H0:Add x s s'
equivlistA E.eq (elements s') (x :: elements s)
  inversion_clear H1.s, s':t
x:E.t
H:Below x s
H0:Add x s s'
x0, y:E.t
H2:InA E.eq y (elements s)
H3:E.eq x0 x
E.lt x0 y
s, s':t
x:E.t
H:Below x s
H0:Add x s s'
x0, y:E.t
H2:InA E.eq y (elements s)
H3:InA E.eq x0 nil
E.lt x0 y
s, s':t
x:E.t
H:Below x s
H0:Add x s s'
equivlistA E.eq (elements s') (x :: elements s)
  rewrite <- elements_iff in H2.s, s':t
x:E.t
H:Below x s
H0:Add x s s'
x0, y:E.t
H2:In y s
H3:E.eq x0 x
E.lt x0 y
s, s':t
x:E.t
H:Below x s
H0:Add x s s'
x0, y:E.t
H2:InA E.eq y (elements s)
H3:InA E.eq x0 nil
E.lt x0 y
s, s':t
x:E.t
H:Below x s
H0:Add x s s'
equivlistA E.eq (elements s') (x :: elements s)
  apply ME.eq_lt with x; auto.s, s':t
x:E.t
H:Below x s
H0:Add x s s'
x0, y:E.t
H2:InA E.eq y (elements s)
H3:InA E.eq x0 nil
E.lt x0 y
s, s':t
x:E.t
H:Below x s
H0:Add x s s'
equivlistA E.eq (elements s') (x :: elements s)
  inversion H3.s, s':t
x:E.t
H:Below x s
H0:Add x s s'
equivlistA E.eq (elements s') (x :: elements s)
  red; intros a.s, s':t
x:E.t
H:Below x s
H0:Add x s s'
a:E.t
InA E.eq a (elements s') <->
InA E.eq a (x :: elements s)
  rewrite InA_cons.s, s':t
x:E.t
H:Below x s
H0:Add x s s'
a:E.t
InA E.eq a (elements s') <->
E.eq a x \/ InA E.eq a (elements s)
  do 2 rewrite <- elements_iff; rewrite (H0 a); intuition.
  Qed.

Two other induction principles on sets: we can be more restrictive on the element we add at each step.

  Lemma set_induction_max :
   forall P : t -> Type,
   (forall s : t, Empty s -> P s) ->
   (forall s s', P s -> forall x, Above x s -> Add x s s' -> P s') ->
   forall s : t, P s.forall P : t -> Type,
(forall s : t, Empty s -> P s) ->
(forall s s' : t,
 P s ->
 forall x : E.t, Above x s -> Add x s s' -> P s') ->
forall s : t, P s
  Proof.forall P : t -> Type,
(forall s : t, Empty s -> P s) ->
(forall s s' : t,
 P s ->
 forall x : E.t, Above x s -> Add x s s' -> P s') ->
forall s : t, P s
  intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto with fset.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
P s
  case_eq (max_elt s); intros.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:max_elt s = Some e
P s
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:max_elt s = None
P s
  apply X0 with (remove e s) e; auto with set.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:max_elt s = Some e
P (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:max_elt s = Some e
Above e (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:max_elt s = None
P s
  apply IHn.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:max_elt s = Some e
n = cardinal (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:max_elt s = Some e
Above e (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:max_elt s = None
P s
  assert (S n = S (cardinal (remove e s))).P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:max_elt s = Some e
S n = S (cardinal (remove e s))
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:max_elt s = Some e
H0:S n = S (cardinal (remove e s))
n = cardinal (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:max_elt s = Some e
Above e (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:max_elt s = None
P s
   rewrite Heqn; apply cardinal_2 with e; auto with set.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:max_elt s = Some e
H0:S n = S (cardinal (remove e s))
n = cardinal (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:max_elt s = Some e
Above e (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:max_elt s = None
P s
  inversion H0; auto.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:max_elt s = Some e
Above e (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:max_elt s = None
P s
  red; intros.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:max_elt s = Some e
y:elt
H0:In y (remove e s)
E.lt y e
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:max_elt s = None
P s
  rewrite remove_iff in H0; destruct H0.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:max_elt s = Some e
y:elt
H0:In y s
H1:~ E.eq e y
E.lt y e
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:max_elt s = None
P s
  generalize (@max_elt_2 s e y H H0); ME.order.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:max_elt s = None
P s

  assert (H0:=max_elt_3 H).P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Above x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:max_elt s = None
H0:Empty s
P s
  rewrite cardinal_Empty in H0; rewrite H0 in Heqn; inversion Heqn.
  Qed.

  Lemma set_induction_min :
   forall P : t -> Type,
   (forall s : t, Empty s -> P s) ->
   (forall s s', P s -> forall x, Below x s -> Add x s s' -> P s') ->
   forall s : t, P s.forall P : t -> Type,
(forall s : t, Empty s -> P s) ->
(forall s s' : t,
 P s ->
 forall x : E.t, Below x s -> Add x s s' -> P s') ->
forall s : t, P s
  Proof.forall P : t -> Type,
(forall s : t, Empty s -> P s) ->
(forall s s' : t,
 P s ->
 forall x : E.t, Below x s -> Add x s s' -> P s') ->
forall s : t, P s
  intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto with fset.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
P s
  case_eq (min_elt s); intros.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:min_elt s = Some e
P s
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:min_elt s = None
P s
  apply X0 with (remove e s) e; auto with set.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:min_elt s = Some e
P (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:min_elt s = Some e
Below e (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:min_elt s = None
P s
  apply IHn.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:min_elt s = Some e
n = cardinal (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:min_elt s = Some e
Below e (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:min_elt s = None
P s
  assert (S n = S (cardinal (remove e s))).P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:min_elt s = Some e
S n = S (cardinal (remove e s))
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:min_elt s = Some e
H0:S n = S (cardinal (remove e s))
n = cardinal (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:min_elt s = Some e
Below e (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:min_elt s = None
P s
   rewrite Heqn; apply cardinal_2 with e; auto with set.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:min_elt s = Some e
H0:S n = S (cardinal (remove e s))
n = cardinal (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:min_elt s = Some e
Below e (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:min_elt s = None
P s
  inversion H0; auto.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:min_elt s = Some e
Below e (remove e s)
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:min_elt s = None
P s
  red; intros.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:min_elt s = Some e
y:elt
H0:In y (remove e s)
E.lt e y
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:min_elt s = None
P s
  rewrite remove_iff in H0; destruct H0.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
e:elt
H:min_elt s = Some e
y:elt
H0:In y s
H1:~ E.eq e y
E.lt e y
P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:min_elt s = None
P s
  generalize (@min_elt_2 s e y H H0); ME.order.P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:min_elt s = None
P s

  assert (H0:=min_elt_3 H).P:t -> Type
X:forall s0 : t, Empty s0 -> P s0
X0:forall s0 s' : t,
P s0 ->
forall x : E.t, Below x s0 -> Add x s0 s' -> P s'
n:nat
IHn:forall s0 : t, n = cardinal s0 -> P s0
s:t
Heqn:S n = cardinal s
H:min_elt s = None
H0:Empty s
P s
  rewrite cardinal_Empty in H0; auto; rewrite H0 in Heqn; inversion Heqn.
  Qed.

More properties of fold : behavior with respect to Above/Below

  Lemma fold_3 :
   forall s s' x (A : Type) (eqA : A -> A -> Prop)
     (st : Equivalence eqA) (i : A) (f : elt -> A -> A),
   compat_op E.eq eqA f ->
   Above x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).forall (s s' : t) (x : E.t) (A : Type)
  (eqA : A -> A -> Prop),
Equivalence eqA ->
forall (i : A) (f : elt -> A -> A),
compat_op E.eq eqA f ->
Above x s ->
Add x s s' -> eqA (fold f s' i) (f x (fold f s i))
  Proof.forall (s s' : t) (x : E.t) (A : Type)
  (eqA : A -> A -> Prop),
Equivalence eqA ->
forall (i : A) (f : elt -> A -> A),
compat_op E.eq eqA f ->
Above x s ->
Add x s s' -> eqA (fold f s' i) (f x (fold f s i))
  intros.s, s':t
x:E.t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:Above x s
H1:Add x s s'
eqA (fold f s' i) (f x (fold f s i))
  rewrite 2 fold_spec_right.s, s':t
x:E.t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:Above x s
H1:Add x s s'
eqA (fold_right f i (rev (elements s')))
  (f x (fold_right f i (rev (elements s))))
  change (f x (fold_right f i (rev (elements s)))) with
    (fold_right f i (rev (x::nil)++rev (elements s))).s, s':t
x:E.t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:Above x s
H1:Add x s s'
eqA (fold_right f i (rev (elements s')))
  (fold_right f i (rev (x :: nil) ++ rev (elements s)))
  apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.s, s':t
x:E.t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:Above x s
H1:Add x s s'
eqlistA E.eq (rev (elements s'))
  (rev (x :: nil) ++ rev (elements s))
  rewrite <- distr_rev.s, s':t
x:E.t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:Above x s
H1:Add x s s'
eqlistA E.eq (rev (elements s'))
  (rev (elements s ++ x :: nil))
  apply eqlistA_rev.s, s':t
x:E.t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:Above x s
H1:Add x s s'
eqlistA E.eq (elements s') (elements s ++ x :: nil)
  apply elements_Add_Above; auto.
  Qed.

  Lemma fold_4 :
   forall s s' x (A : Type) (eqA : A -> A -> Prop)
     (st : Equivalence eqA) (i : A) (f : elt -> A -> A),
   compat_op E.eq eqA f ->
   Below x s -> Add x s s' -> eqA (fold f s' i) (fold f s (f x i)).forall (s s' : t) (x : E.t) (A : Type)
  (eqA : A -> A -> Prop),
Equivalence eqA ->
forall (i : A) (f : elt -> A -> A),
compat_op E.eq eqA f ->
Below x s ->
Add x s s' -> eqA (fold f s' i) (fold f s (f x i))
  Proof.forall (s s' : t) (x : E.t) (A : Type)
  (eqA : A -> A -> Prop),
Equivalence eqA ->
forall (i : A) (f : elt -> A -> A),
compat_op E.eq eqA f ->
Below x s ->
Add x s s' -> eqA (fold f s' i) (fold f s (f x i))
  intros.s, s':t
x:E.t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:Below x s
H1:Add x s s'
eqA (fold f s' i) (fold f s (f x i))
  rewrite 2 M.fold_1.s, s':t
x:E.t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:Below x s
H1:Add x s s'
eqA
  (fold_left (fun (a : A) (e : elt) => f e a)
     (elements s') i)
  (fold_left (fun (a : A) (e : elt) => f e a)
     (elements s) (f x i))
  set (g:=fun (a : A) (e : elt) => f e a).s, s':t
x:E.t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:Below x s
H1:Add x s s'
g:=fun (a : A) (e : elt) => f e a:A -> elt -> A
eqA (fold_left g (elements s') i)
  (fold_left g (elements s) (f x i))
  change (eqA (fold_left g (elements s') i) (fold_left g (x::elements s) i)).s, s':t
x:E.t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:Below x s
H1:Add x s s'
g:=fun (a : A) (e : elt) => f e a:A -> elt -> A
eqA (fold_left g (elements s') i)
  (fold_left g (x :: elements s) i)
  unfold g.s, s':t
x:E.t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:Below x s
H1:Add x s s'
g:=fun (a : A) (e : elt) => f e a:A -> elt -> A
eqA
  (fold_left (fun (a : A) (e : elt) => f e a)
     (elements s') i)
  (fold_left (fun (a : A) (e : elt) => f e a)
     (x :: elements s) i)
  rewrite <- 2 fold_left_rev_right.s, s':t
x:E.t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:Below x s
H1:Add x s s'
g:=fun (a : A) (e : elt) => f e a:A -> elt -> A
eqA (fold_right f i (rev (elements s')))
  (fold_right f i (rev (x :: elements s)))
  apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.s, s':t
x:E.t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:Below x s
H1:Add x s s'
g:=fun (a : A) (e : elt) => f e a:A -> elt -> A
eqlistA E.eq (rev (elements s'))
  (rev (x :: elements s))
  apply eqlistA_rev.s, s':t
x:E.t
A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
i:A
f:elt -> A -> A
H:compat_op E.eq eqA f
H0:Below x s
H1:Add x s s'
g:=fun (a : A) (e : elt) => f e a:A -> elt -> A
eqlistA E.eq (elements s') (x :: elements s)
  apply elements_Add_Below; auto.
  Qed.

The following results have already been proved earlier, but we can now prove them with one hypothesis less: no need for (transpose eqA f).

  Section FoldOpt.
  Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
  Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f).

  Lemma fold_equal :
   forall i s s', s[=]s' -> 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
forall (i : A) (s s' : t),
s [=] s' -> 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
forall (i : A) (s s' : t),
s [=] s' -> eqA (fold f s i) (fold f s' i)
  intros.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
i:A
s, s':t
H:s [=] s'
eqA (fold f s i) (fold f s' i) rewrite 2 fold_spec_right.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
i:A
s, s':t
H:s [=] s'
eqA (fold_right f i (rev (elements s)))
  (fold_right f i (rev (elements s')))
  apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
i:A
s, s':t
H:s [=] s'
eqlistA E.eq (rev (elements s)) (rev (elements s'))
  apply eqlistA_rev.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
i:A
s, s':t
H:s [=] s'
eqlistA E.eq (elements s) (elements s')
  apply sort_equivlistA_eqlistA; auto with set.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
i:A
s, s':t
H:s [=] s'
equivlistA E.eq (elements s) (elements s')
  red; intro a; do 2 rewrite <- elements_iff; auto.
  Qed.

  Lemma add_fold : forall i s x, In x s ->
   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
forall (i : A) (s : t) (x : elt),
In x s -> 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
forall (i : A) (s : t) (x : elt),
In x s -> eqA (fold f (add x s) i) (fold f s i)
  intros; apply fold_equal; auto with set.
  Qed.

  Lemma remove_fold_2: forall i s x, ~In x s ->
   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
forall (i : A) (s : t) (x : elt),
~ In x s -> 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
forall (i : A) (s : t) (x : elt),
~ In x s -> eqA (fold f (remove x s) i) (fold f s i)
  intros.A:Type
eqA:A -> A -> Prop
st:Equivalence eqA
f:elt -> A -> A
Comp:compat_op E.eq eqA f
i:A
s:t
x:elt
H:~ In x s
eqA (fold f (remove x s) i) (fold f s i)
  apply fold_equal; auto with set.
  Qed.

  End FoldOpt.

An alternative version of choose_3

  Lemma choose_equal : forall s s', Equal s s' ->
    match choose s, choose s' with
      | Some x, Some x' => E.eq x x'
      | None, None => True
      | _, _ => False
     end.forall s s' : t,
s [=] s' ->
match choose s with
| Some x =>
    match choose s' with
    | Some x' => E.eq x x'
    | None => False
    end
| None =>
    match choose s' with
    | Some _ => False
    | None => True
    end
end
  Proof.forall s s' : t,
s [=] s' ->
match choose s with
| Some x =>
    match choose s' with
    | Some x' => E.eq x x'
    | None => False
    end
| None =>
    match choose s' with
    | Some _ => False
    | None => True
    end
end
  intros s s' H;
  generalize (@choose_1 s)(@choose_2 s)
             (@choose_1 s')(@choose_2 s')(@choose_3 s s');
  destruct (choose s); destruct (choose s'); simpl; intuition.s, s':t
H:s [=] s'
e:elt
H0:forall x : elt, Some e = Some x -> In x s
H1:Some e = None -> Empty s
H2:forall x : elt, None = Some x -> In x s'
H4:forall x y : elt,
Some e = Some x ->
None = Some y -> s [=] s' -> E.eq x y
H5:Empty s'
False
s, s':t
H:s [=] s'
e:elt
H0:forall x : elt, None = Some x -> In x s
H2:forall x : elt, Some e = Some x -> In x s'
H3:Some e = None -> Empty s'
H4:forall x y : elt,
None = Some x ->
Some e = Some y -> s [=] s' -> E.eq x y
H5:Empty s
False
  apply H5 with e; rewrite <-H; auto.s, s':t
H:s [=] s'
e:elt
H0:forall x : elt, None = Some x -> In x s
H2:forall x : elt, Some e = Some x -> In x s'
H3:Some e = None -> Empty s'
H4:forall x y : elt,
None = Some x ->
Some e = Some y -> s [=] s' -> E.eq x y
H5:Empty s
False
  apply H5 with e; rewrite H; auto.
  Qed.

End OrdProperties.