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 file proposes an implementation of the non-dependent interface MSetWeakInterface.S using lists without redundancy.

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

Functions over lists

First, we provide sets as lists which are (morally) without redundancy. The specs are proved under the additional condition of no redundancy. And the functions returning sets are proved to preserve this invariant.

The set operations.

Module Ops (X: DecidableType) <: WOps X.

  Definition elt := X.t.
  Definition t := list elt.

  Definition empty : t := nil.

  Definition is_empty (l : t) : bool := if l then true else false.

  Fixpoint mem (x : elt) (s : t) : bool :=
    match s with
    | nil => false
    | y :: l =>
           if X.eq_dec x y then true else mem x l
    end.

  Fixpoint add (x : elt) (s : t) : t :=
    match s with
    | nil => x :: nil
    | y :: l =>
        if X.eq_dec x y then s else y :: add x l
    end.

  Definition singleton (x : elt) : t := x :: nil.

  Fixpoint remove (x : elt) (s : t) : t :=
    match s with
    | nil => nil
    | y :: l =>
        if X.eq_dec x y then l else y :: remove x l
    end.

  Definition fold (B : Type) (f : elt -> B -> B) : t -> B -> B :=
    fold_left (flip f).

  Definition union (s : t) : t -> t := fold add s.

  Definition diff (s s' : t) : t := fold remove s' s.

  Definition inter (s s': t) : t :=
    fold (fun x s => if mem x s' then add x s else s) s nil.

  Definition subset (s s' : t) : bool := is_empty (diff s s').

  Definition equal (s s' : t) : bool := andb (subset s s') (subset s' s).

  Fixpoint filter (f : elt -> bool) (s : t) : t :=
    match s with
    | nil => nil
    | x :: l => if f x then x :: filter f l else filter f l
    end.

  Fixpoint for_all (f : elt -> bool) (s : t) : bool :=
    match s with
    | nil => true
    | x :: l => if f x then for_all f l else false
    end.

  Fixpoint exists_ (f : elt -> bool) (s : t) : bool :=
    match s with
    | nil => false
    | x :: l => if f x then true else exists_ f l
    end.

  Fixpoint partition (f : elt -> bool) (s : t) : t * t :=
    match s with
    | nil => (nil, nil)
    | x :: l =>
        let (s1, s2) := partition f l in
        if f x then (x :: s1, s2) else (s1, x :: s2)
    end.

  Definition cardinal (s : t) : nat := length s.

  Definition elements (s : t) : list elt := s.

  Definition choose (s : t) : option elt :=
     match s with
      | nil => None
      | x::_ => Some x
     end.

End Ops.

Proofs of set operation specifications.

Module MakeRaw (X:DecidableType) <: WRawSets X.
  Include Ops X.

  Section ForNotations.
  Notation NoDup := (NoDupA X.eq).
  Notation In := (InA X.eq).

  (* TODO: modify proofs in order to avoid these hints *)
  Let eqr:= (@Equivalence_Reflexive _ _ X.eq_equiv).
  Let eqsym:= (@Equivalence_Symmetric _ _ X.eq_equiv).
  Let eqtrans:= (@Equivalence_Transitive _ _ X.eq_equiv).
  Hint Resolve eqr eqtrans : core.
  Hint Immediate eqsym : core.

  Definition IsOk := NoDup.

  Class Ok (s:t) : Prop := ok : NoDup s.

  Hint Unfold Ok : core.
  Hint Resolve ok : core.

  Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }.

  Ltac inv_ok := match goal with
   | H:Ok (_ :: _) |- _ => inversion_clear H; inv_ok
   | H:Ok nil |- _ => clear H; inv_ok
   | H:NoDup ?l |- _ => change (Ok l) in H; inv_ok
   | _ => idtac
  end.

  Ltac inv := invlist InA; inv_ok.
  Ltac constructors := repeat constructor.

  Fixpoint isok l := match l with
   | nil => true
   | a::l => negb (mem a l) && isok l
  end.

  Definition Equal s s' := forall a : elt, In a s <-> In a s'.
  Definition Subset s s' := forall a : elt, In a s -> In a s'.
  Definition Empty s := forall a : elt, ~ In a s.
  Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
  Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.

  Lemma In_compat : Proper (X.eq==>eq==>iff) In.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
Proper (X.eq ==> eq ==> iff) In
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
Proper (X.eq ==> eq ==> iff) In
  repeat red; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
x, y:X.t
H:X.eq x y
x0, y0:list X.t
H0:x0 = y0
(In x x0 -> In y y0) /\ (In y y0 -> In x x0) subst.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
x, y:X.t
H:X.eq x y
y0:list X.t
(In x y0 -> In y y0) /\ (In y y0 -> In x y0) rewrite H; auto.
  Qed.

  Lemma mem_spec : forall s x `{Ok s},
   mem x s = true <-> In x s.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (x : elt),
Ok s -> mem x s = true <-> In x s
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (x : elt),
Ok s -> mem x s = true <-> In x s
  induction s; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
x:elt
H:Ok nil
mem x nil = true <-> In x nil
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 : elt,
Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Ok (a :: s)
mem x (a :: s) = true <-> In x (a :: s)
  split; intros; inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
x:elt
H0:mem x nil = true
In x nil
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 : elt,
Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Ok (a :: s)
mem x (a :: s) = true <-> In x (a :: s) discriminate.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 : elt,
Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Ok (a :: s)
mem x (a :: s) = true <-> In x (a :: s)
  simpl; destruct (X.eq_dec x a); split; intros; inv; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 : elt,
Ok s -> mem x0 s = true <-> In x0 s
x:elt
n:~ X.eq x a
H0:mem x s = true
H1:~ In a s
H2:Ok s
In x (a :: s)
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 : elt,
Ok s -> mem x0 s = true <-> In x0 s
x:elt
n:~ X.eq x a
H1:In x s
H0:~ In a s
H2:Ok s
mem x s = true
  right; rewrite <- IHs; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 : elt,
Ok s -> mem x0 s = true <-> In x0 s
x:elt
n:~ X.eq x a
H1:In x s
H0:~ In a s
H2:Ok s
mem x s = true
  rewrite IHs; auto.
  Qed.

  Lemma isok_iff : forall l, Ok l <-> isok l = true.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall l : t, Ok l <-> isok l = true
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall l : t, Ok l <-> isok l = true
  induction l.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
Ok nil <-> isok nil = true
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
l:list elt
IHl:Ok l <-> isok l = true
Ok (a :: l) <-> isok (a :: l) = true
  intuition.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
l:list elt
IHl:Ok l <-> isok l = true
Ok (a :: l) <-> isok (a :: l) = true
  simpl.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
l:list elt
IHl:Ok l <-> isok l = true
Ok (a :: l) <-> negb (mem a l) && isok l = true
  rewrite andb_true_iff.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
l:list elt
IHl:Ok l <-> isok l = true
Ok (a :: l) <-> negb (mem a l) = true /\ isok l = true
  rewrite negb_true_iff.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
l:list elt
IHl:Ok l <-> isok l = true
Ok (a :: l) <-> mem a l = false /\ isok l = true
  rewrite <- IHl.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
l:list elt
IHl:Ok l <-> isok l = true
Ok (a :: l) <-> mem a l = false /\ Ok l
  split; intros H.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
l:list elt
IHl:Ok l <-> isok l = true
H:Ok (a :: l)
mem a l = false /\ Ok l
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
l:list elt
IHl:Ok l <-> isok l = true
H:mem a l = false /\ Ok l
Ok (a :: l) inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
l:list elt
IHl:Ok l <-> isok l = true
H0:~ In a l
H1:Ok l
mem a l = false /\ Ok l
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
l:list elt
IHl:Ok l <-> isok l = true
H:mem a l = false /\ Ok l
Ok (a :: l)
  split; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
l:list elt
IHl:Ok l <-> isok l = true
H0:~ In a l
H1:Ok l
mem a l = false
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
l:list elt
IHl:Ok l <-> isok l = true
H:mem a l = false /\ Ok l
Ok (a :: l)
  apply not_true_is_false.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
l:list elt
IHl:Ok l <-> isok l = true
H0:~ In a l
H1:Ok l
mem a l <> true
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
l:list elt
IHl:Ok l <-> isok l = true
H:mem a l = false /\ Ok l
Ok (a :: l) rewrite mem_spec; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
l:list elt
IHl:Ok l <-> isok l = true
H:mem a l = false /\ Ok l
Ok (a :: l)
  destruct H; constructors; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
l:list elt
IHl:Ok l <-> isok l = true
H:mem a l = false
H0:Ok l
~ In a l
  rewrite <- mem_spec; auto; congruence.
  Qed.

  Instance isok_Ok l : isok l = true -> Ok l | 10.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
l:list elt
isok l = true -> Ok l
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
l:list elt
isok l = true -> Ok l
  intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
l:list elt
H:isok l = true
Ok l apply <- isok_iff; auto.
  Qed.

  Lemma add_spec :
   forall (s : t) (x y : elt) {Hs : Ok s},
     In y (add x s) <-> X.eq y x \/ In y s.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (x y : elt),
Ok s -> In y (add x s) <-> X.eq y x \/ In y s
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (x y : elt),
Ok s -> In y (add x s) <-> X.eq y x \/ In y s
  induction s; simpl; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
x, y:elt
Hs:Ok nil
In y (x :: nil) <-> X.eq y x \/ In y nil
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (add x0 s) <-> X.eq y0 x0 \/ In y0 s
x, y:elt
Hs:Ok (a :: s)
In y (if X.eq_dec x a then a :: s else a :: add x s) <->
X.eq y x \/ In y (a :: s)
  intuition; inv; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (add x0 s) <-> X.eq y0 x0 \/ In y0 s
x, y:elt
Hs:Ok (a :: s)
In y (if X.eq_dec x a then a :: s else a :: add x s) <->
X.eq y x \/ In y (a :: s)
  destruct X.eq_dec; inv; rewrite InA_cons, ?IHs; intuition.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (add x0 s) <-> X.eq y0 x0 \/ In y0 s
x, y:elt
e:X.eq x a
H:In a s -> False
H0:Ok s
H2:X.eq y x
X.eq y a \/ In y s
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (add x0 s) <-> X.eq y0 x0 \/ In y0 s
x, y:elt
n:X.eq x a -> False
H:In a s -> False
H0:Ok s
H2:In y (a :: s)
X.eq y a \/ X.eq y x \/ In y s
  left; eauto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (add x0 s) <-> X.eq y0 x0 \/ In y0 s
x, y:elt
n:X.eq x a -> False
H:In a s -> False
H0:Ok s
H2:In y (a :: s)
X.eq y a \/ X.eq y x \/ In y s
  inv; auto.
  Qed.

  Instance add_ok s x `(Ok s) : Ok (add x s).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
x:elt
H:Ok s
Ok (add x s)
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
x:elt
H:Ok s
Ok (add x s)
  induction s.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
x:elt
H:Ok nil
Ok (add x nil)
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
x:elt
H:Ok (a :: s)
IHs:Ok s -> Ok (add x s)
Ok (add x (a :: s))
  simpl; intuition.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
x:elt
H:Ok (a :: s)
IHs:Ok s -> Ok (add x s)
Ok (add x (a :: s))
  intros; inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
x:elt
IHs:Ok s -> Ok (add x s)
H0:~ In a s
H1:Ok s
Ok (add x (a :: s)) simpl.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
x:elt
IHs:Ok s -> Ok (add x s)
H0:~ In a s
H1:Ok s
Ok (if X.eq_dec x a then a :: s else a :: add x s)
  destruct X.eq_dec; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
x:elt
IHs:Ok s -> Ok (add x s)
H0:~ In a s
H1:Ok s
n:~ X.eq x a
Ok (a :: add x s)
  constructors; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
x:elt
IHs:Ok s -> Ok (add x s)
H0:~ In a s
H1:Ok s
n:~ X.eq x a
~ In a (add x s)
  intro; inv; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
x:elt
IHs:Ok s -> Ok (add x s)
H0:~ In a s
H1:Ok s
n:~ X.eq x a
H:In a (add x s)
False
  rewrite add_spec in *; intuition.
  Qed.

  Lemma remove_spec :
   forall (s : t) (x y : elt) {Hs : Ok s},
     In y (remove x s) <-> In y s /\ ~X.eq y x.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (x y : elt),
Ok s -> In y (remove x s) <-> In y s /\ ~ X.eq y x
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (x y : elt),
Ok s -> In y (remove x s) <-> In y s /\ ~ X.eq y x
  induction s; simpl; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
x, y:elt
Hs:Ok nil
In y nil <-> In y nil /\ ~ X.eq y x
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (remove x0 s) <-> In y0 s /\ ~ X.eq y0 x0
x, y:elt
Hs:Ok (a :: s)
In y (if X.eq_dec x a then s else a :: remove x s) <->
In y (a :: s) /\ ~ X.eq y x
  intuition; inv; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (remove x0 s) <-> In y0 s /\ ~ X.eq y0 x0
x, y:elt
Hs:Ok (a :: s)
In y (if X.eq_dec x a then s else a :: remove x s) <->
In y (a :: s) /\ ~ X.eq y x
  destruct X.eq_dec as [|Hnot]; inv; rewrite !InA_cons, ?IHs; intuition.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (remove x0 s) <->
In y0 s /\ (X.eq y0 x0 -> False)
x, y:elt
e:X.eq x a
H:In a s -> False
H0:Ok s
H1:In y s
H2:X.eq y x
False
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (remove x0 s) <->
In y0 s /\ (X.eq y0 x0 -> False)
x, y:elt
e:X.eq x a
H:In a s -> False
H0:Ok s
H3:X.eq y x -> False
H1:X.eq y a
In y s
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (remove x0 s) <->
In y0 s /\ (X.eq y0 x0 -> False)
x, y:elt
Hnot:X.eq x a -> False
H:In a s -> False
H0:Ok s
H2:X.eq y a
H1:X.eq y x
False
  elim H.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (remove x0 s) <->
In y0 s /\ (X.eq y0 x0 -> False)
x, y:elt
e:X.eq x a
H:In a s -> False
H0:Ok s
H1:In y s
H2:X.eq y x
In a s
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (remove x0 s) <->
In y0 s /\ (X.eq y0 x0 -> False)
x, y:elt
e:X.eq x a
H:In a s -> False
H0:Ok s
H3:X.eq y x -> False
H1:X.eq y a
In y s
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (remove x0 s) <->
In y0 s /\ (X.eq y0 x0 -> False)
x, y:elt
Hnot:X.eq x a -> False
H:In a s -> False
H0:Ok s
H2:X.eq y a
H1:X.eq y x
False setoid_replace a with y; eauto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (remove x0 s) <->
In y0 s /\ (X.eq y0 x0 -> False)
x, y:elt
e:X.eq x a
H:In a s -> False
H0:Ok s
H3:X.eq y x -> False
H1:X.eq y a
In y s
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (remove x0 s) <->
In y0 s /\ (X.eq y0 x0 -> False)
x, y:elt
Hnot:X.eq x a -> False
H:In a s -> False
H0:Ok s
H2:X.eq y a
H1:X.eq y x
False
  elim H3.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (remove x0 s) <->
In y0 s /\ (X.eq y0 x0 -> False)
x, y:elt
e:X.eq x a
H:In a s -> False
H0:Ok s
H3:X.eq y x -> False
H1:X.eq y a
X.eq y x
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (remove x0 s) <->
In y0 s /\ (X.eq y0 x0 -> False)
x, y:elt
Hnot:X.eq x a -> False
H:In a s -> False
H0:Ok s
H2:X.eq y a
H1:X.eq y x
False setoid_replace x with y; eauto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (remove x0 s) <->
In y0 s /\ (X.eq y0 x0 -> False)
x, y:elt
Hnot:X.eq x a -> False
H:In a s -> False
H0:Ok s
H2:X.eq y a
H1:X.eq y x
False
  elim Hnot.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall x0 y0 : elt,
Ok s ->
In y0 (remove x0 s) <->
In y0 s /\ (X.eq y0 x0 -> False)
x, y:elt
Hnot:X.eq x a -> False
H:In a s -> False
H0:Ok s
H2:X.eq y a
H1:X.eq y x
X.eq x a eauto.
  Qed.

  Instance remove_ok s x `(Ok s) : Ok (remove x s).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
x:elt
H:Ok s
Ok (remove x s)
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
x:elt
H:Ok s
Ok (remove x s)
  induction s; simpl; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
x:elt
H:Ok nil
Ok nil
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
x:elt
H:Ok (a :: s)
IHs:Ok s -> Ok (remove x s)
Ok (if X.eq_dec x a then s else a :: remove x s)
  auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
x:elt
H:Ok (a :: s)
IHs:Ok s -> Ok (remove x s)
Ok (if X.eq_dec x a then s else a :: remove x s)
  destruct X.eq_dec; inv; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
x:elt
IHs:Ok s -> Ok (remove x s)
n:~ X.eq x a
H0:~ In a s
H1:Ok s
Ok (a :: remove x s)
  constructors; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
x:elt
IHs:Ok s -> Ok (remove x s)
n:~ X.eq x a
H0:~ In a s
H1:Ok s
~ In a (remove x s)
  rewrite remove_spec; intuition.
  Qed.

  Lemma singleton_ok : forall x : elt, Ok (singleton x).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall x : elt, Ok (singleton x)
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall x : elt, Ok (singleton x)
  unfold singleton; simpl; constructors; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
x:elt
~ In x nil intro; inv.
  Qed.

  Lemma singleton_spec : forall x y : elt, In y (singleton x) <-> X.eq y x.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall x y : elt, In y (singleton x) <-> X.eq y x
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall x y : elt, In y (singleton x) <-> X.eq y x
  unfold singleton; simpl; split; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
x, y:elt
H:In y (x :: nil)
X.eq y x
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
x, y:elt
H:X.eq y x
In y (x :: nil) inv; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
x, y:elt
H:X.eq y x
In y (x :: nil) left; auto.
  Qed.

  Lemma empty_ok : Ok empty.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
Ok empty
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
Ok empty
  unfold empty; constructors.
  Qed.

  Lemma empty_spec : Empty empty.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
Empty empty
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
Empty empty
  unfold Empty, empty; red; intros; inv.
  Qed.

  Lemma is_empty_spec : forall s : t, is_empty s = true <-> Empty s.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s : t, is_empty s = true <-> Empty s
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s : t, is_empty s = true <-> Empty s
  unfold Empty; destruct s; simpl; split; intros; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
H:true = true
a:elt
~ In a nil
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
e:elt
s:list elt
H:false = true
a:elt
~ In a (e :: s)
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
e:elt
s:list elt
H:forall a : elt, ~ In a (e :: s)
false = true
  intro; inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
e:elt
s:list elt
H:false = true
a:elt
~ In a (e :: s)
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
e:elt
s:list elt
H:forall a : elt, ~ In a (e :: s)
false = true
  discriminate.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
e:elt
s:list elt
H:forall a : elt, ~ In a (e :: s)
false = true
  elim (H e); auto.
  Qed.

  Lemma elements_spec1 : forall (s : t) (x : elt), In x (elements s) <-> In x s.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (x : elt), In x (elements s) <-> In x s
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (x : elt), In x (elements s) <-> In x s
  unfold elements; intuition.
  Qed.

  Lemma elements_spec2w : forall (s : t) {Hs : Ok s}, NoDup (elements s).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s : t, Ok s -> NoDup (elements s)
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s : t, Ok s -> NoDup (elements s)
  unfold elements; auto.
  Qed.

  Lemma fold_spec :
   forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
   fold f s i = fold_left (flip f) (elements s) i.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (flip f) (elements s) i
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (flip f) (elements s) i
  reflexivity.
  Qed.

  Instance union_ok : forall s s' `(Ok s, Ok s'), Ok (union s s').eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s s' : t, Ok s -> Ok s' -> Ok (union s s')
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s s' : t, Ok s -> Ok s' -> Ok (union s s')
  induction s; simpl; auto; intros; inv; unfold flip; auto with *.
  Qed.

  Lemma union_spec :
   forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'},
   In x (union s s') <-> In x s \/ In x s'.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s s' : t) (x : elt),
Ok s ->
Ok s' -> In x (union s s') <-> In x s \/ In x s'
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s s' : t) (x : elt),
Ok s ->
Ok s' -> In x (union s s') <-> In x s \/ In x s'
  induction s; simpl in *; unfold flip; intros; auto; inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s':t
x:elt
Hs':Ok s'
In x s' <-> In x nil \/ In x s'
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall (s'0 : t) (x0 : elt),
Ok s ->
Ok s'0 ->
In x0 (union s s'0) <-> In x0 s \/ In x0 s'0
s':t
x:elt
Hs':Ok s'
H:~ In a s
H0:Ok s
In x (union s (add a s')) <-> In x (a :: s) \/ In x s'
  intuition; inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall (s'0 : t) (x0 : elt),
Ok s ->
Ok s'0 ->
In x0 (union s s'0) <-> In x0 s \/ In x0 s'0
s':t
x:elt
Hs':Ok s'
H:~ In a s
H0:Ok s
In x (union s (add a s')) <-> In x (a :: s) \/ In x s'
  rewrite IHs, add_spec, InA_cons; intuition.
  Qed.

  Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s').eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
H:Ok s
H0:Ok s'
Ok (inter s s')
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
H:Ok s
H0:Ok s'
Ok (inter s s')
  unfold inter, fold, flip.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
H:Ok s
H0:Ok s'
Ok
  (fold_left
     (fun (x : t) (y : elt) =>
      if mem y s' then add y x else x) s nil)
  set (acc := nil (A:=elt)).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
H:Ok s
H0:Ok s'
acc:=nil:list elt
Ok
  (fold_left
     (fun (x : t) (y : elt) =>
      if mem y s' then add y x else x) s acc)
  assert (Hacc : Ok acc) by constructors.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
H:Ok s
H0:Ok s'
acc:=nil:list elt
Hacc:Ok acc
Ok
  (fold_left
     (fun (x : t) (y : elt) =>
      if mem y s' then add y x else x) s acc)
  clearbody acc; revert acc Hacc.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
H:Ok s
H0:Ok s'
forall acc : list elt,
Ok acc ->
Ok
  (fold_left
     (fun (x : t) (y : elt) =>
      if mem y s' then add y x else x) s acc)
  induction s; simpl; auto; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
s':t
H:Ok (a :: s)
H0:Ok s'
IHs:Ok s ->
forall acc0 : list elt,
Ok acc0 ->
Ok
  (fold_left
     (fun (x : t) (y : elt) =>
      if mem y s' then add y x else x) s acc0)
acc:list elt
Hacc:Ok acc
Ok
  (fold_left
     (fun (x : t) (y : elt) =>
      if mem y s' then add y x else x) s
     (if mem a s' then add a acc else acc)) inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
s':t
H0:Ok s'
IHs:Ok s ->
forall acc0 : list elt,
Ok acc0 ->
Ok
  (fold_left
     (fun (x : t) (y : elt) =>
      if mem y s' then add y x else x) s acc0)
acc:list elt
Hacc:Ok acc
H1:~ In a s
H2:Ok s
Ok
  (fold_left
     (fun (x : t) (y : elt) =>
      if mem y s' then add y x else x) s
     (if mem a s' then add a acc else acc))
  apply IHs; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
s':t
H0:Ok s'
IHs:Ok s ->
forall acc0 : list elt,
Ok acc0 ->
Ok
  (fold_left
     (fun (x : t) (y : elt) =>
      if mem y s' then add y x else x) s acc0)
acc:list elt
Hacc:Ok acc
H1:~ In a s
H2:Ok s
Ok (if mem a s' then add a acc else acc)
  destruct (mem a s'); auto with *.
  Qed.

  Lemma inter_spec  :
   forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'},
   In x (inter s s') <-> In x s /\ In x s'.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s s' : t) (x : elt),
Ok s ->
Ok s' -> In x (inter s s') <-> In x s /\ In x s'
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s s' : t) (x : elt),
Ok s ->
Ok s' -> In x (inter s s') <-> In x s /\ In x s'
  unfold inter, fold, flip; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
x:elt
Hs:Ok s
Hs':Ok s'
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s nil) <->
In x s /\ In x s'
  set (acc := nil (A:=elt)) in *.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
x:elt
Hs:Ok s
Hs':Ok s'
acc:=nil:list elt
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s acc) <->
In x s /\ In x s'
  assert (Hacc : Ok acc) by constructors.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
x:elt
Hs:Ok s
Hs':Ok s'
acc:=nil:list elt
Hacc:Ok acc
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s acc) <->
In x s /\ In x s'
  assert (IFF : (In x s /\ In x s') <-> (In x s /\ In x s') \/ In x acc).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
x:elt
Hs:Ok s
Hs':Ok s'
acc:=nil:list elt
Hacc:Ok acc
In x s /\ In x s' <-> In x s /\ In x s' \/ In x acc
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
x:elt
Hs:Ok s
Hs':Ok s'
acc:=nil:list elt
Hacc:Ok acc
IFF:In x s /\ In x s' <->
In x s /\ In x s' \/ In x acc
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s acc) <->
In x s /\ In x s'
   intuition; unfold acc in *; inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
x:elt
Hs:Ok s
Hs':Ok s'
acc:=nil:list elt
Hacc:Ok acc
IFF:In x s /\ In x s' <->
In x s /\ In x s' \/ In x acc
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s acc) <->
In x s /\ In x s'
  rewrite IFF; clear IFF.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
x:elt
Hs:Ok s
Hs':Ok s'
acc:=nil:list elt
Hacc:Ok acc
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s acc) <->
In x s /\ In x s' \/ In x acc clearbody acc.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
x:elt
Hs:Ok s
Hs':Ok s'
acc:list elt
Hacc:Ok acc
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s acc) <->
In x s /\ In x s' \/ In x acc
  revert acc Hacc x s' Hs Hs'.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
forall acc : list elt,
Ok acc ->
forall (x : elt) (s' : t),
Ok s ->
Ok s' ->
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s acc) <->
In x s /\ In x s' \/ In x acc
  induction s; simpl; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
acc:list elt
Hacc:Ok acc
x:elt
s':t
Hs:Ok nil
Hs':Ok s'
In x acc <-> In x nil /\ In x s' \/ In x acc
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall acc0 : list elt,
Ok acc0 ->
forall (x0 : elt) (s'0 : t),
Ok s ->
Ok s'0 ->
In x0
  (fold_left
     (fun (x1 : t) (y : elt) =>
      if mem y s'0 then add y x1 else x1) s acc0) <->
In x0 s /\ In x0 s'0 \/ In x0 acc0
acc:list elt
Hacc:Ok acc
x:elt
s':t
Hs:Ok (a :: s)
Hs':Ok s'
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s
     (if mem a s' then add a acc else acc)) <->
In x (a :: s) /\ In x s' \/ In x acc
  intuition; inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall acc0 : list elt,
Ok acc0 ->
forall (x0 : elt) (s'0 : t),
Ok s ->
Ok s'0 ->
In x0
  (fold_left
     (fun (x1 : t) (y : elt) =>
      if mem y s'0 then add y x1 else x1) s acc0) <->
In x0 s /\ In x0 s'0 \/ In x0 acc0
acc:list elt
Hacc:Ok acc
x:elt
s':t
Hs:Ok (a :: s)
Hs':Ok s'
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s
     (if mem a s' then add a acc else acc)) <->
In x (a :: s) /\ In x s' \/ In x acc
  inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall acc0 : list elt,
Ok acc0 ->
forall (x0 : elt) (s'0 : t),
Ok s ->
Ok s'0 ->
In x0
  (fold_left
     (fun (x1 : t) (y : elt) =>
      if mem y s'0 then add y x1 else x1) s acc0) <->
In x0 s /\ In x0 s'0 \/ In x0 acc0
acc:list elt
Hacc:Ok acc
x:elt
s':t
Hs':Ok s'
H:~ In a s
H0:Ok s
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s
     (if mem a s' then add a acc else acc)) <->
In x (a :: s) /\ In x s' \/ In x acc
  case_eq (mem a s'); intros Hm.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall acc0 : list elt,
Ok acc0 ->
forall (x0 : elt) (s'0 : t),
Ok s ->
Ok s'0 ->
In x0
  (fold_left
     (fun (x1 : t) (y : elt) =>
      if mem y s'0 then add y x1 else x1) s acc0) <->
In x0 s /\ In x0 s'0 \/ In x0 acc0
acc:list elt
Hacc:Ok acc
x:elt
s':t
Hs':Ok s'
H:~ In a s
H0:Ok s
Hm:mem a s' = true
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s (add a acc)) <->
In x (a :: s) /\ In x s' \/ In x acc
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall acc0 : list elt,
Ok acc0 ->
forall (x0 : elt) (s'0 : t),
Ok s ->
Ok s'0 ->
In x0
  (fold_left
     (fun (x1 : t) (y : elt) =>
      if mem y s'0 then add y x1 else x1) s acc0) <->
In x0 s /\ In x0 s'0 \/ In x0 acc0
acc:list elt
Hacc:Ok acc
x:elt
s':t
Hs':Ok s'
H:~ In a s
H0:Ok s
Hm:mem a s' = false
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s acc) <->
In x (a :: s) /\ In x s' \/ In x acc
  rewrite IHs, add_spec, InA_cons; intuition.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall acc0 : list elt,
Ok acc0 ->
forall (x0 : elt) (s'0 : t),
Ok s ->
Ok s'0 ->
In x0
  (fold_left
     (fun (x1 : t) (y : elt) =>
      if mem y s'0 then add y x1 else x1) s acc0) <->
In x0 s /\ In x0 s'0 \/ In x0 acc0
acc:list elt
Hacc:Ok acc
x:elt
s':t
Hs':Ok s'
H:In a s -> False
H0:Ok s
Hm:mem a s' = true
H1:X.eq x a
(X.eq x a \/ In x s) /\ In x s' \/ In x acc
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall acc0 : list elt,
Ok acc0 ->
forall (x0 : elt) (s'0 : t),
Ok s ->
Ok s'0 ->
In x0
  (fold_left
     (fun (x1 : t) (y : elt) =>
      if mem y s'0 then add y x1 else x1) s acc0) <->
In x0 s /\ In x0 s'0 \/ In x0 acc0
acc:list elt
Hacc:Ok acc
x:elt
s':t
Hs':Ok s'
H:~ In a s
H0:Ok s
Hm:mem a s' = false
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s acc) <->
In x (a :: s) /\ In x s' \/ In x acc
  rewrite mem_spec in Hm; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall acc0 : list elt,
Ok acc0 ->
forall (x0 : elt) (s'0 : t),
Ok s ->
Ok s'0 ->
In x0
  (fold_left
     (fun (x1 : t) (y : elt) =>
      if mem y s'0 then add y x1 else x1) s acc0) <->
In x0 s /\ In x0 s'0 \/ In x0 acc0
acc:list elt
Hacc:Ok acc
x:elt
s':t
Hs':Ok s'
H:In a s -> False
H0:Ok s
Hm:In a s'
H1:X.eq x a
(X.eq x a \/ In x s) /\ In x s' \/ In x acc
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall acc0 : list elt,
Ok acc0 ->
forall (x0 : elt) (s'0 : t),
Ok s ->
Ok s'0 ->
In x0
  (fold_left
     (fun (x1 : t) (y : elt) =>
      if mem y s'0 then add y x1 else x1) s acc0) <->
In x0 s /\ In x0 s'0 \/ In x0 acc0
acc:list elt
Hacc:Ok acc
x:elt
s':t
Hs':Ok s'
H:~ In a s
H0:Ok s
Hm:mem a s' = false
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s acc) <->
In x (a :: s) /\ In x s' \/ In x acc
  left; split; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall acc0 : list elt,
Ok acc0 ->
forall (x0 : elt) (s'0 : t),
Ok s ->
Ok s'0 ->
In x0
  (fold_left
     (fun (x1 : t) (y : elt) =>
      if mem y s'0 then add y x1 else x1) s acc0) <->
In x0 s /\ In x0 s'0 \/ In x0 acc0
acc:list elt
Hacc:Ok acc
x:elt
s':t
Hs':Ok s'
H:In a s -> False
H0:Ok s
Hm:In a s'
H1:X.eq x a
In x s'
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall acc0 : list elt,
Ok acc0 ->
forall (x0 : elt) (s'0 : t),
Ok s ->
Ok s'0 ->
In x0
  (fold_left
     (fun (x1 : t) (y : elt) =>
      if mem y s'0 then add y x1 else x1) s acc0) <->
In x0 s /\ In x0 s'0 \/ In x0 acc0
acc:list elt
Hacc:Ok acc
x:elt
s':t
Hs':Ok s'
H:~ In a s
H0:Ok s
Hm:mem a s' = false
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s acc) <->
In x (a :: s) /\ In x s' \/ In x acc rewrite H1; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall acc0 : list elt,
Ok acc0 ->
forall (x0 : elt) (s'0 : t),
Ok s ->
Ok s'0 ->
In x0
  (fold_left
     (fun (x1 : t) (y : elt) =>
      if mem y s'0 then add y x1 else x1) s acc0) <->
In x0 s /\ In x0 s'0 \/ In x0 acc0
acc:list elt
Hacc:Ok acc
x:elt
s':t
Hs':Ok s'
H:~ In a s
H0:Ok s
Hm:mem a s' = false
In x
  (fold_left
     (fun (x0 : t) (y : elt) =>
      if mem y s' then add y x0 else x0) s acc) <->
In x (a :: s) /\ In x s' \/ In x acc
  rewrite IHs, InA_cons; intuition.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall acc0 : list elt,
Ok acc0 ->
forall (x0 : elt) (s'0 : t),
Ok s ->
Ok s'0 ->
In x0
  (fold_left
     (fun (x1 : t) (y : elt) =>
      if mem y s'0 then add y x1 else x1) s acc0) <->
In x0 s /\ In x0 s'0 \/ In x0 acc0
acc:list elt
Hacc:Ok acc
x:elt
s':t
Hs':Ok s'
H:In a s -> False
H0:Ok s
Hm:mem a s' = false
H3:In x s'
H2:X.eq x a
In x s /\ In x s' \/ In x acc
  rewrite H2, <- mem_spec in H3; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall acc0 : list elt,
Ok acc0 ->
forall (x0 : elt) (s'0 : t),
Ok s ->
Ok s'0 ->
In x0
  (fold_left
     (fun (x1 : t) (y : elt) =>
      if mem y s'0 then add y x1 else x1) s acc0) <->
In x0 s /\ In x0 s'0 \/ In x0 acc0
acc:list elt
Hacc:Ok acc
x:elt
s':t
Hs':Ok s'
H:In a s -> False
H0:Ok s
Hm:mem a s' = false
H3:mem a s' = true
H2:X.eq x a
In x s /\ In x s' \/ In x acc congruence.
  Qed.

  Instance diff_ok : forall s s' `(Ok s, Ok s'), Ok (diff s s').eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s s' : t, Ok s -> Ok s' -> Ok (diff s s')
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s s' : t, Ok s -> Ok s' -> Ok (diff s s')
  unfold diff; intros s s'; revert s.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s':t
forall s : t, Ok s -> Ok s' -> Ok (fold remove s' s)
  induction s'; simpl; unfold flip; auto; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s':list elt
IHs':forall s0 : t,
Ok s0 -> Ok s' -> Ok (fold remove s' s0)
s:t
H:Ok s
H0:Ok (a :: s')
Ok (fold remove s' (remove a s)) inv; auto with *.
  Qed.

  Lemma diff_spec  :
   forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'},
   In x (diff s s') <-> In x s /\ ~In x s'.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s s' : t) (x : elt),
Ok s ->
Ok s' -> In x (diff s s') <-> In x s /\ ~ In x s'
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s s' : t) (x : elt),
Ok s ->
Ok s' -> In x (diff s s') <-> In x s /\ ~ In x s'
  unfold diff; intros s s'; revert s.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s':t
forall (s : t) (x : elt),
Ok s ->
Ok s' ->
In x (fold remove s' s) <-> In x s /\ ~ In x s'
  induction s'; simpl; unfold flip.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (x : elt),
Ok s -> Ok nil -> In x s <-> In x s /\ ~ In x nil
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s':list elt
IHs':forall (s : t) (x : elt),
Ok s ->
Ok s' ->
In x (fold remove s' s) <-> In x s /\ ~ In x s'
forall (s : t) (x : elt),
Ok s ->
Ok (a :: s') ->
In x (fold remove s' (remove a s)) <->
In x s /\ ~ In x (a :: s')
  intuition; inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s':list elt
IHs':forall (s : t) (x : elt),
Ok s ->
Ok s' ->
In x (fold remove s' s) <-> In x s /\ ~ In x s'
forall (s : t) (x : elt),
Ok s ->
Ok (a :: s') ->
In x (fold remove s' (remove a s)) <->
In x s /\ ~ In x (a :: s')
  intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s':list elt
IHs':forall (s0 : t) (x0 : elt),
Ok s0 ->
Ok s' ->
In x0 (fold remove s' s0) <->
In x0 s0 /\ ~ In x0 s'
s:t
x:elt
Hs:Ok s
Hs':Ok (a :: s')
In x (fold remove s' (remove a s)) <->
In x s /\ ~ In x (a :: s') inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s':list elt
IHs':forall (s0 : t) (x0 : elt),
Ok s0 ->
Ok s' ->
In x0 (fold remove s' s0) <->
In x0 s0 /\ ~ In x0 s'
s:t
x:elt
Hs:Ok s
H:~ In a s'
H0:Ok s'
In x (fold remove s' (remove a s)) <->
In x s /\ ~ In x (a :: s')
  rewrite IHs', remove_spec, InA_cons; intuition.
  Qed.

  Lemma subset_spec :
   forall (s s' : t) {Hs : Ok s} {Hs' : Ok s'},
   subset s s' = true <-> Subset s s'.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s s' : t,
Ok s -> Ok s' -> subset s s' = true <-> Subset s s'
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s s' : t,
Ok s -> Ok s' -> subset s s' = true <-> Subset s s'
  unfold subset, Subset; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
is_empty (diff s s') = true <->
(forall a : elt, In a s -> In a s')
  rewrite is_empty_spec.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
Empty (diff s s') <->
(forall a : elt, In a s -> In a s')
  unfold Empty; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
(forall a : elt, ~ In a (diff s s')) <->
(forall a : elt, In a s -> In a s')
  intuition.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
H:forall a0 : elt, In a0 (diff s s') -> False
a:elt
H0:In a s
In a s'
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
H:forall a0 : elt, In a0 s -> In a0 s'
a:elt
H0:In a (diff s s')
False
  specialize (H a).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
a:elt
H:In a (diff s s') -> False
H0:In a s
In a s'
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
H:forall a0 : elt, In a0 s -> In a0 s'
a:elt
H0:In a (diff s s')
False rewrite diff_spec in H; intuition.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
a:elt
H0:In a s
H:(In a s' -> False) -> False
In a s'
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
H:forall a0 : elt, In a0 s -> In a0 s'
a:elt
H0:In a (diff s s')
False
  rewrite <- (mem_spec a) in H |- *.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
a:elt
H0:In a s
H:(mem a s' = true -> False) -> False
mem a s' = true
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
H:forall a0 : elt, In a0 s -> In a0 s'
a:elt
H0:In a (diff s s')
False destruct (mem a s'); intuition.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
H:forall a0 : elt, In a0 s -> In a0 s'
a:elt
H0:In a (diff s s')
False
  rewrite diff_spec in H0; intuition.
  Qed.

  Lemma equal_spec :
   forall (s s' : t) {Hs : Ok s} {Hs' : Ok s'},
   equal s s' = true <-> Equal s s'.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s s' : t,
Ok s -> Ok s' -> equal s s' = true <-> Equal s s'
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s s' : t,
Ok s -> Ok s' -> equal s s' = true <-> Equal s s'
  unfold Equal, equal; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
subset s s' && subset s' s = true <->
(forall a : elt, In a s <-> In a s')
  rewrite andb_true_iff, !subset_spec.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
Subset s s' /\ Subset s' s <->
(forall a : elt, In a s <-> In a s')
  unfold Subset; intuition.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
H:forall a0 : elt, In a0 s <-> In a0 s'
a:elt
H0:In a s
In a s'
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
H:forall a0 : elt, In a0 s <-> In a0 s'
a:elt
H0:In a s'
In a s rewrite <- H; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s, s':t
Hs:Ok s
Hs':Ok s'
H:forall a0 : elt, In a0 s <-> In a0 s'
a:elt
H0:In a s'
In a s rewrite H; auto.
  Qed.

  Definition choose_spec1 :
    forall (s : t) (x : elt), choose s = Some x -> In x s.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (x : elt), choose s = Some x -> In x s
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (x : elt), choose s = Some x -> In x s
  destruct s; simpl; intros; inversion H; auto.
  Qed.

  Definition choose_spec2 : forall s : t, choose s = None -> Empty s.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s : t, choose s = None -> Empty s
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s : t, choose s = None -> Empty s
  destruct s; simpl; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
H:None = None
Empty nil
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
e:elt
s:list elt
H:Some e = None
Empty (e :: s)
  intros x H0; inversion H0.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
e:elt
s:list elt
H:Some e = None
Empty (e :: s)
  inversion H.
  Qed.

  Lemma cardinal_spec :
   forall (s : t) {Hs : Ok s}, cardinal s = length (elements s).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s : t, Ok s -> cardinal s = length (elements s)
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s : t, Ok s -> cardinal s = length (elements s)
  auto.
  Qed.

  Lemma filter_spec' : forall s x f,
   In x (filter f s) -> In x s.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (x : X.t) (f : elt -> bool),
In x (filter f s) -> In x s
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (x : X.t) (f : elt -> bool),
In x (filter f s) -> In x s
  induction s; simpl.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall x : X.t, (elt -> bool) -> In x nil -> In x nil
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall (x : X.t) (f : elt -> bool),
In x (filter f s) -> In x s
forall (x : X.t) (f : elt -> bool),
In x (if f a then a :: filter f s else filter f s) ->
In x (a :: s)
  intuition; inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall (x : X.t) (f : elt -> bool),
In x (filter f s) -> In x s
forall (x : X.t) (f : elt -> bool),
In x (if f a then a :: filter f s else filter f s) ->
In x (a :: s)
  intros; destruct (f a); inv; intuition; right; eauto.
  Qed.

  Lemma filter_spec :
   forall (s : t) (x : elt) (f : elt -> bool),
   Proper (X.eq==>eq) f ->
   (In x (filter f s) <-> In x s /\ f x = true).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (x : elt) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
In x (filter f s) <-> In x s /\ f x = true
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (x : elt) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
In x (filter f s) <-> In x s /\ f x = true
  induction s; simpl.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (x : elt) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
In x nil <-> In x nil /\ f x = true
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall (x : elt) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
In x (filter f s) <-> In x s /\ f x = true
forall (x : elt) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
In x (if f a then a :: filter f s else filter f s) <->
In x (a :: s) /\ f x = true
  intuition; inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall (x : elt) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
In x (filter f s) <-> In x s /\ f x = true
forall (x : elt) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
In x (if f a then a :: filter f s else filter f s) <->
In x (a :: s) /\ f x = true
  intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall (x0 : elt) (f0 : elt -> bool),
Proper (X.eq ==> eq) f0 ->
In x0 (filter f0 s) <-> In x0 s /\ f0 x0 = true
x:elt
f:elt -> bool
H:Proper (X.eq ==> eq) f
In x (if f a then a :: filter f s else filter f s) <->
In x (a :: s) /\ f x = true
  destruct (f a) eqn:E; rewrite ?InA_cons, IHs; intuition.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall (x0 : elt) (f0 : elt -> bool),
Proper (X.eq ==> eq) f0 ->
In x0 (filter f0 s) <-> In x0 s /\ f0 x0 = true
x:elt
f:elt -> bool
H:Proper (X.eq ==> eq) f
E:f a = true
H1:X.eq x a
f x = true
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall (x0 : elt) (f0 : elt -> bool),
Proper (X.eq ==> eq) f0 ->
In x0 (filter f0 s) <-> In x0 s /\ f0 x0 = true
x:elt
f:elt -> bool
H:Proper (X.eq ==> eq) f
E:f a = false
H2:f x = true
H0:X.eq x a
In x s
  setoid_replace x with a; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall (x0 : elt) (f0 : elt -> bool),
Proper (X.eq ==> eq) f0 ->
In x0 (filter f0 s) <-> In x0 s /\ f0 x0 = true
x:elt
f:elt -> bool
H:Proper (X.eq ==> eq) f
E:f a = false
H2:f x = true
H0:X.eq x a
In x s
  setoid_replace a with x in E; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall (x0 : elt) (f0 : elt -> bool),
Proper (X.eq ==> eq) f0 ->
In x0 (filter f0 s) <-> In x0 s /\ f0 x0 = true
x:elt
f:elt -> bool
H:Proper (X.eq ==> eq) f
E:f x = false
H2:f x = true
H0:X.eq x a
In x s congruence.
  Qed.

  Instance filter_ok s f `(Ok s) : Ok (filter f s).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
f:elt -> bool
H:Ok s
Ok (filter f s)
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
f:elt -> bool
H:Ok s
Ok (filter f s)
  induction s; simpl.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
f:elt -> bool
H:Ok nil
Ok nil
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
f:elt -> bool
H:Ok (a :: s)
IHs:Ok s -> Ok (filter f s)
Ok (if f a then a :: filter f s else filter f s)
  auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
f:elt -> bool
H:Ok (a :: s)
IHs:Ok s -> Ok (filter f s)
Ok (if f a then a :: filter f s else filter f s)
  intros; inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
f:elt -> bool
IHs:Ok s -> Ok (filter f s)
H0:~ In a s
H1:Ok s
Ok (if f a then a :: filter f s else filter f s)
  case (f a); auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
f:elt -> bool
IHs:Ok s -> Ok (filter f s)
H0:~ In a s
H1:Ok s
Ok (a :: filter f s)
  constructors; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
f:elt -> bool
IHs:Ok s -> Ok (filter f s)
H0:~ In a s
H1:Ok s
~ In a (filter f s)
  contradict H0.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
f:elt -> bool
IHs:Ok s -> Ok (filter f s)
H1:Ok s
H0:In a (filter f s)
In a s
  eapply filter_spec'; eauto.
  Qed.

  Lemma for_all_spec :
   forall (s : t) (f : elt -> bool),
   Proper (X.eq==>eq) f ->
   (for_all f s = true <-> For_all (fun x => f x = true) s).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
for_all f s = true <->
For_all (fun x : elt => f x = true) s
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
for_all f s = true <->
For_all (fun x : elt => f x = true) s
  unfold For_all; induction s; simpl.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
true = true <->
(forall x : X.t, In x nil -> f x = true)
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
for_all f s = true <->
(forall x : X.t, In x s -> f x = true)
forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
(if f a then for_all f s else false) = true <->
(forall x : X.t, In x (a :: s) -> f x = true)
  intuition.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
f:elt -> bool
H:Proper (X.eq ==> eq) f
H0:true = true
x:X.t
H1:In x nil
f x = true
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
for_all f s = true <->
(forall x : X.t, In x s -> f x = true)
forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
(if f a then for_all f s else false) = true <->
(forall x : X.t, In x (a :: s) -> f x = true) inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
for_all f s = true <->
(forall x : X.t, In x s -> f x = true)
forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
(if f a then for_all f s else false) = true <->
(forall x : X.t, In x (a :: s) -> f x = true)
  intros; inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
for_all f0 s = true <->
(forall x : X.t, In x s -> f0 x = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
(if f a then for_all f s else false) = true <->
(forall x : X.t, In x (a :: s) -> f x = true)
  destruct (f a) eqn:F.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
for_all f0 s = true <->
(forall x : X.t, In x s -> f0 x = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = true
for_all f s = true <->
(forall x : X.t, In x (a :: s) -> f x = true)
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
for_all f0 s = true <->
(forall x : X.t, In x s -> f0 x = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = false
false = true <->
(forall x : X.t, In x (a :: s) -> f x = true)
  rewrite IHs; intuition.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
for_all f0 s = true <->
(forall x0 : X.t, In x0 s -> f0 x0 = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = true
H0:forall x0 : X.t, In x0 s -> f x0 = true
x:X.t
H1:In x (a :: s)
f x = true
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
for_all f0 s = true <->
(forall x : X.t, In x s -> f0 x = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = false
false = true <->
(forall x : X.t, In x (a :: s) -> f x = true) inv; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
for_all f0 s = true <->
(forall x0 : X.t, In x0 s -> f0 x0 = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = true
H0:forall x0 : X.t, In x0 s -> f x0 = true
x:X.t
H2:X.eq x a
f x = true
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
for_all f0 s = true <->
(forall x : X.t, In x s -> f0 x = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = false
false = true <->
(forall x : X.t, In x (a :: s) -> f x = true)
  setoid_replace x with a; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
for_all f0 s = true <->
(forall x : X.t, In x s -> f0 x = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = false
false = true <->
(forall x : X.t, In x (a :: s) -> f x = true)
  split; intros H'; try discriminate.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
for_all f0 s = true <->
(forall x : X.t, In x s -> f0 x = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = false
H':forall x : X.t, In x (a :: s) -> f x = true
false = true
  intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
for_all f0 s = true <->
(forall x : X.t, In x s -> f0 x = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = false
H':forall x : X.t, In x (a :: s) -> f x = true
false = true
  rewrite <- F, <- (H' a); auto.
  Qed.

  Lemma exists_spec :
   forall (s : t) (f : elt -> bool),
   Proper (X.eq==>eq) f ->
   (exists_ f s = true <-> Exists (fun x => f x = true) s).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
exists_ f s = true <->
Exists (fun x : elt => f x = true) s
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
exists_ f s = true <->
Exists (fun x : elt => f x = true) s
  unfold Exists; induction s; simpl.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
false = true <->
(exists x : X.t, In x nil /\ f x = true)
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
exists_ f s = true <->
(exists x : X.t, In x s /\ f x = true)
forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
(if f a then true else exists_ f s) = true <->
(exists x : X.t, In x (a :: s) /\ f x = true)
  split; [discriminate| intros (x & Hx & _); inv].eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
exists_ f s = true <->
(exists x : X.t, In x s /\ f x = true)
forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
(if f a then true else exists_ f s) = true <->
(exists x : X.t, In x (a :: s) /\ f x = true)
  intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
exists_ f0 s = true <->
(exists x : X.t, In x s /\ f0 x = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
(if f a then true else exists_ f s) = true <->
(exists x : X.t, In x (a :: s) /\ f x = true)
  destruct (f a) eqn:F.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
exists_ f0 s = true <->
(exists x : X.t, In x s /\ f0 x = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = true
true = true <->
(exists x : X.t, In x (a :: s) /\ f x = true)
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
exists_ f0 s = true <->
(exists x : X.t, In x s /\ f0 x = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = false
exists_ f s = true <->
(exists x : X.t, In x (a :: s) /\ f x = true)
  split; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
exists_ f0 s = true <->
(exists x : X.t, In x s /\ f0 x = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = true
true = true ->
exists x : X.t, In x (a :: s) /\ f x = true
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
exists_ f0 s = true <->
(exists x : X.t, In x s /\ f0 x = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = false
exists_ f s = true <->
(exists x : X.t, In x (a :: s) /\ f x = true)
  exists a; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
exists_ f0 s = true <->
(exists x : X.t, In x s /\ f0 x = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = false
exists_ f s = true <->
(exists x : X.t, In x (a :: s) /\ f x = true)
  rewrite IHs; firstorder.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
exists_ f0 s = true <->
(exists x0 : X.t, In x0 s /\ f0 x0 = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = false
x:X.t
H0:In x (a :: s)
H1:f x = true
exists x0 : X.t, In x0 s /\ f x0 = true
  inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
exists_ f0 s = true <->
(exists x0 : X.t, In x0 s /\ f0 x0 = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = false
x:X.t
H1:f x = true
H2:X.eq x a
exists x0 : X.t, In x0 s /\ f x0 = true
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
exists_ f0 s = true <->
(exists x0 : X.t, In x0 s /\ f0 x0 = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = false
x:X.t
H1:f x = true
H2:In x s
exists x0 : X.t, In x0 s /\ f x0 = true
  setoid_replace a with x in F; auto; congruence.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
exists_ f0 s = true <->
(exists x0 : X.t, In x0 s /\ f0 x0 = true)
f:elt -> bool
H:Proper (X.eq ==> eq) f
F:f a = false
x:X.t
H1:f x = true
H2:In x s
exists x0 : X.t, In x0 s /\ f x0 = true
  exists x; auto.
  Qed.

  Lemma partition_spec1 :
   forall (s : t) (f : elt -> bool),
   Proper (X.eq==>eq) f ->
   Equal (fst (partition f s)) (filter f s).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
Equal (fst (partition f s)) (filter f s)
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
Equal (fst (partition f s)) (filter f s)
  simple induction s; simpl; auto; unfold Equal.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
forall a : elt, In a nil <-> In a nil
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
forall (a : elt) (l : list elt),
(forall f : elt -> bool,
 Proper (X.eq ==> eq) f ->
 forall a0 : elt,
 In a0 (fst (partition f l)) <-> In a0 (filter f l)) ->
forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
forall a0 : elt,
In a0
  (fst
     (let (s1, s2) := partition f l in
      if f a then (a :: s1, s2) else (s1, a :: s2))) <->
In a0 (if f a then a :: filter f l else filter f l)
  firstorder.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
forall (a : elt) (l : list elt),
(forall f : elt -> bool,
 Proper (X.eq ==> eq) f ->
 forall a0 : elt,
 In a0 (fst (partition f l)) <-> In a0 (filter f l)) ->
forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
forall a0 : elt,
In a0
  (fst
     (let (s1, s2) := partition f l in
      if f a then (a :: s1, s2) else (s1, a :: s2))) <->
In a0 (if f a then a :: filter f l else filter f l)
  intros x l Hrec f Hf.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
x:elt
l:list elt
Hrec:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
forall a : elt,
In a (fst (partition f0 l)) <->
In a (filter f0 l)
f:elt -> bool
Hf:Proper (X.eq ==> eq) f
forall a : elt,
In a
  (fst
     (let (s1, s2) := partition f l in
      if f x then (x :: s1, s2) else (s1, x :: s2))) <->
In a (if f x then x :: filter f l else filter f l)
  generalize (Hrec f Hf); clear Hrec.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
x:elt
l:list elt
f:elt -> bool
Hf:Proper (X.eq ==> eq) f
(forall a : elt,
 In a (fst (partition f l)) <-> In a (filter f l)) ->
forall a : elt,
In a
  (fst
     (let (s1, s2) := partition f l in
      if f x then (x :: s1, s2) else (s1, x :: s2))) <->
In a (if f x then x :: filter f l else filter f l)
  case (partition f l); intros s1 s2; simpl; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
x:elt
l:list elt
f:elt -> bool
Hf:Proper (X.eq ==> eq) f
s1, s2:t
H:forall a0 : elt, In a0 s1 <-> In a0 (filter f l)
a:elt
In a
  (fst (if f x then (x :: s1, s2) else (s1, x :: s2))) <->
In a (if f x then x :: filter f l else filter f l)
  case (f x); simpl; firstorder; inversion H0; intros; firstorder.
  Qed.

  Lemma partition_spec2 :
   forall (s : t) (f : elt -> bool),
   Proper (X.eq==>eq) f ->
   Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
Equal (snd (partition f s))
  (filter (fun x : elt => negb (f x)) s)
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
Equal (snd (partition f s))
  (filter (fun x : elt => negb (f x)) s)
  simple induction s; simpl; auto; unfold Equal.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
forall a : elt, In a nil <-> In a nil
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
forall (a : elt) (l : list elt),
(forall f : elt -> bool,
 Proper (X.eq ==> eq) f ->
 forall a0 : elt,
 In a0 (snd (partition f l)) <->
 In a0 (filter (fun x : elt => negb (f x)) l)) ->
forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
forall a0 : elt,
In a0
  (snd
     (let (s1, s2) := partition f l in
      if f a then (a :: s1, s2) else (s1, a :: s2))) <->
In a0
  (if negb (f a)
   then a :: filter (fun x : elt => negb (f x)) l
   else filter (fun x : elt => negb (f x)) l)
  firstorder.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
forall (a : elt) (l : list elt),
(forall f : elt -> bool,
 Proper (X.eq ==> eq) f ->
 forall a0 : elt,
 In a0 (snd (partition f l)) <->
 In a0 (filter (fun x : elt => negb (f x)) l)) ->
forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
forall a0 : elt,
In a0
  (snd
     (let (s1, s2) := partition f l in
      if f a then (a :: s1, s2) else (s1, a :: s2))) <->
In a0
  (if negb (f a)
   then a :: filter (fun x : elt => negb (f x)) l
   else filter (fun x : elt => negb (f x)) l)
  intros x l Hrec f Hf.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
x:elt
l:list elt
Hrec:forall f0 : elt -> bool,
Proper (X.eq ==> eq) f0 ->
forall a : elt,
In a (snd (partition f0 l)) <->
In a (filter (fun x0 : elt => negb (f0 x0)) l)
f:elt -> bool
Hf:Proper (X.eq ==> eq) f
forall a : elt,
In a
  (snd
     (let (s1, s2) := partition f l in
      if f x then (x :: s1, s2) else (s1, x :: s2))) <->
In a
  (if negb (f x)
   then x :: filter (fun x0 : elt => negb (f x0)) l
   else filter (fun x0 : elt => negb (f x0)) l)
  generalize (Hrec f Hf); clear Hrec.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
x:elt
l:list elt
f:elt -> bool
Hf:Proper (X.eq ==> eq) f
(forall a : elt,
 In a (snd (partition f l)) <->
 In a (filter (fun x0 : elt => negb (f x0)) l)) ->
forall a : elt,
In a
  (snd
     (let (s1, s2) := partition f l in
      if f x then (x :: s1, s2) else (s1, x :: s2))) <->
In a
  (if negb (f x)
   then x :: filter (fun x0 : elt => negb (f x0)) l
   else filter (fun x0 : elt => negb (f x0)) l)
  case (partition f l); intros s1 s2; simpl; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
x:elt
l:list elt
f:elt -> bool
Hf:Proper (X.eq ==> eq) f
s1, s2:t
H:forall a0 : elt,
In a0 s2 <->
In a0 (filter (fun x0 : elt => negb (f x0)) l)
a:elt
In a
  (snd (if f x then (x :: s1, s2) else (s1, x :: s2))) <->
In a
  (if negb (f x)
   then x :: filter (fun x0 : elt => negb (f x0)) l
   else filter (fun x0 : elt => negb (f x0)) l)
  case (f x); simpl; firstorder; inversion H0; intros; firstorder.
  Qed.

  Lemma partition_ok1' :
   forall (s : t) {Hs : Ok s} (f : elt -> bool)(x:elt),
    In x (fst (partition f s)) -> In x s.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s : t,
Ok s ->
forall (f : elt -> bool) (x : elt),
In x (fst (partition f s)) -> In x s
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s : t,
Ok s ->
forall (f : elt -> bool) (x : elt),
In x (fst (partition f s)) -> In x s
  induction s; simpl; auto; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:Ok s ->
forall (f0 : elt -> bool) (x0 : elt),
In x0 (fst (partition f0 s)) -> In x0 s
Hs:Ok (a :: s)
f:elt -> bool
x:elt
H:In x
  (fst
     (let (s1, s2) := partition f s in
      if f a then (a :: s1, s2) else (s1, a :: s2)))
In x (a :: s) inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:Ok s ->
forall (f0 : elt -> bool) (x0 : elt),
In x0 (fst (partition f0 s)) -> In x0 s
f:elt -> bool
x:elt
H:In x
  (fst
     (let (s1, s2) := partition f s in
      if f a then (a :: s1, s2) else (s1, a :: s2)))
H0:~ In a s
H1:Ok s
In x (a :: s)
  generalize (IHs H1 f x).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:Ok s ->
forall (f0 : elt -> bool) (x0 : elt),
In x0 (fst (partition f0 s)) -> In x0 s
f:elt -> bool
x:elt
H:In x
  (fst
     (let (s1, s2) := partition f s in
      if f a then (a :: s1, s2) else (s1, a :: s2)))
H0:~ In a s
H1:Ok s
(In x (fst (partition f s)) -> In x s) ->
In x (a :: s)
  destruct (f a); destruct (partition f s); simpl in *; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:Ok s ->
forall (f0 : elt -> bool) (x0 : elt),
In x0 (fst (partition f0 s)) -> In x0 s
f:elt -> bool
x:elt
t0, t1:t
H:In x (a :: t0)
H0:~ In a s
H1:Ok s
(In x t0 -> In x s) -> In x (a :: s)
  inversion_clear H; auto.
  Qed.

  Lemma partition_ok2' :
   forall (s : t) {Hs : Ok s} (f : elt -> bool)(x:elt),
    In x (snd (partition f s)) -> In x s.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s : t,
Ok s ->
forall (f : elt -> bool) (x : elt),
In x (snd (partition f s)) -> In x s
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall s : t,
Ok s ->
forall (f : elt -> bool) (x : elt),
In x (snd (partition f s)) -> In x s
  induction s; simpl; auto; intros.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:Ok s ->
forall (f0 : elt -> bool) (x0 : elt),
In x0 (snd (partition f0 s)) -> In x0 s
Hs:Ok (a :: s)
f:elt -> bool
x:elt
H:In x
  (snd
     (let (s1, s2) := partition f s in
      if f a then (a :: s1, s2) else (s1, a :: s2)))
In x (a :: s) inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:Ok s ->
forall (f0 : elt -> bool) (x0 : elt),
In x0 (snd (partition f0 s)) -> In x0 s
f:elt -> bool
x:elt
H:In x
  (snd
     (let (s1, s2) := partition f s in
      if f a then (a :: s1, s2) else (s1, a :: s2)))
H0:~ In a s
H1:Ok s
In x (a :: s)
  generalize (IHs H1 f x).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:Ok s ->
forall (f0 : elt -> bool) (x0 : elt),
In x0 (snd (partition f0 s)) -> In x0 s
f:elt -> bool
x:elt
H:In x
  (snd
     (let (s1, s2) := partition f s in
      if f a then (a :: s1, s2) else (s1, a :: s2)))
H0:~ In a s
H1:Ok s
(In x (snd (partition f s)) -> In x s) ->
In x (a :: s)
  destruct (f a); destruct (partition f s); simpl in *; auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
a:elt
s:list elt
IHs:Ok s ->
forall (f0 : elt -> bool) (x0 : elt),
In x0 (snd (partition f0 s)) -> In x0 s
f:elt -> bool
x:elt
t0, t1:t
H:In x (a :: t1)
H0:~ In a s
H1:Ok s
(In x t1 -> In x s) -> In x (a :: s)
  inversion_clear H; auto.
  Qed.

  Instance partition_ok1 : forall s f `(Ok s), Ok (fst (partition f s)).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (f : elt -> bool),
Ok s -> Ok (fst (partition f s))
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (f : elt -> bool),
Ok s -> Ok (fst (partition f s))
  simple induction s; simpl.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
(elt -> bool) -> Ok nil -> Ok nil
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
forall (a : elt) (l : list elt),
(forall f : elt -> bool,
 Ok l -> Ok (fst (partition f l))) ->
forall f : elt -> bool,
Ok (a :: l) ->
Ok
  (fst
     (let (s1, s2) := partition f l in
      if f a then (a :: s1, s2) else (s1, a :: s2)))
  auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
forall (a : elt) (l : list elt),
(forall f : elt -> bool,
 Ok l -> Ok (fst (partition f l))) ->
forall f : elt -> bool,
Ok (a :: l) ->
Ok
  (fst
     (let (s1, s2) := partition f l in
      if f a then (a :: s1, s2) else (s1, a :: s2)))
  intros x l Hrec f Hs; inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
x:elt
l:list elt
Hrec:forall f0 : elt -> bool,
Ok l -> Ok (fst (partition f0 l))
f:elt -> bool
H:~ In x l
H0:Ok l
Ok
  (fst
     (let (s1, s2) := partition f l in
      if f x then (x :: s1, s2) else (s1, x :: s2)))
  generalize (@partition_ok1' _ _ f x).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
x:elt
l:list elt
Hrec:forall f0 : elt -> bool,
Ok l -> Ok (fst (partition f0 l))
f:elt -> bool
H:~ In x l
H0:Ok l
(In x (fst (partition f l)) -> In x l) ->
Ok
  (fst
     (let (s1, s2) := partition f l in
      if f x then (x :: s1, s2) else (s1, x :: s2)))
  generalize (Hrec f H0).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
x:elt
l:list elt
Hrec:forall f0 : elt -> bool,
Ok l -> Ok (fst (partition f0 l))
f:elt -> bool
H:~ In x l
H0:Ok l
Ok (fst (partition f l)) ->
(In x (fst (partition f l)) -> In x l) ->
Ok
  (fst
     (let (s1, s2) := partition f l in
      if f x then (x :: s1, s2) else (s1, x :: s2)))
  case (f x); case (partition f l); simpl; constructors; auto.
  Qed.

  Instance partition_ok2 : forall s f `(Ok s), Ok (snd (partition f s)).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (f : elt -> bool),
Ok s -> Ok (snd (partition f s))
  Proof.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
forall (s : t) (f : elt -> bool),
Ok s -> Ok (snd (partition f s))
  simple induction s; simpl.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
(elt -> bool) -> Ok nil -> Ok nil
eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
forall (a : elt) (l : list elt),
(forall f : elt -> bool,
 Ok l -> Ok (snd (partition f l))) ->
forall f : elt -> bool,
Ok (a :: l) ->
Ok
  (snd
     (let (s1, s2) := partition f l in
      if f a then (a :: s1, s2) else (s1, a :: s2)))
  auto.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
forall (a : elt) (l : list elt),
(forall f : elt -> bool,
 Ok l -> Ok (snd (partition f l))) ->
forall f : elt -> bool,
Ok (a :: l) ->
Ok
  (snd
     (let (s1, s2) := partition f l in
      if f a then (a :: s1, s2) else (s1, a :: s2)))
  intros x l Hrec f Hs; inv.eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
x:elt
l:list elt
Hrec:forall f0 : elt -> bool,
Ok l -> Ok (snd (partition f0 l))
f:elt -> bool
H:~ In x l
H0:Ok l
Ok
  (snd
     (let (s1, s2) := partition f l in
      if f x then (x :: s1, s2) else (s1, x :: s2)))
  generalize (@partition_ok2' _ _ f x).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
x:elt
l:list elt
Hrec:forall f0 : elt -> bool,
Ok l -> Ok (snd (partition f0 l))
f:elt -> bool
H:~ In x l
H0:Ok l
(In x (snd (partition f l)) -> In x l) ->
Ok
  (snd
     (let (s1, s2) := partition f l in
      if f x then (x :: s1, s2) else (s1, x :: s2)))
  generalize (Hrec f H0).eqr:=Equivalence_Reflexive:Reflexive X.eq
eqsym:=Equivalence_Symmetric:Symmetric X.eq
eqtrans:=Equivalence_Transitive:Transitive X.eq
s:t
x:elt
l:list elt
Hrec:forall f0 : elt -> bool,
Ok l -> Ok (snd (partition f0 l))
f:elt -> bool
H:~ In x l
H0:Ok l
Ok (snd (partition f l)) ->
(In x (snd (partition f l)) -> In x l) ->
Ok
  (snd
     (let (s1, s2) := partition f l in
      if f x then (x :: s1, s2) else (s1, x :: s2)))
  case (f x); case (partition f l); simpl; constructors; auto.
  Qed.

  End ForNotations.

  Definition In := InA X.eq.
  Definition eq := Equal.
  Instance eq_equiv : Equivalence eq := _.

End MakeRaw.

Encapsulation

Now, in order to really provide a functor implementing S, we need to encapsulate everything into a type of lists without redundancy.

Module Make (X: DecidableType) <: WSets with Module E := X.
 Module Raw := MakeRaw X.
 Include WRaw2Sets X Raw.
End Make.