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 MSetInterface.S using strictly ordered list.

Require Export MSetInterface OrdersFacts OrdersLists.
Set Implicit Arguments.
Unset Strict Implicit.

Functions over lists

First, we provide sets as lists which are not necessarily sorted. The specs are proved under the additional condition of being sorted. And the functions returning sets are proved to preserve this invariant.

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

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

  Definition empty : t := nil.

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

The set operations.

  Fixpoint mem x s :=
    match s with
    | nil => false
    | y :: l =>
        match X.compare x y with
        | Lt => false
        | Eq => true
        | Gt => mem x l
        end
    end.

  Fixpoint add x s :=
    match s with
    | nil => x :: nil
    | y :: l =>
        match X.compare x y with
        | Lt => x :: s
        | Eq => s
        | Gt => y :: add x l
        end
    end.

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

  Fixpoint remove x s : t :=
    match s with
    | nil => nil
    | y :: l =>
        match X.compare x y with
        | Lt => s
        | Eq => l
        | Gt => y :: remove x l
        end
    end.

  Fixpoint union (s : t) : t -> t :=
    match s with
    | nil => fun s' => s'
    | x :: l =>
        (fix union_aux (s' : t) : t :=
           match s' with
           | nil => s
           | x' :: l' =>
               match X.compare x x' with
               | Lt => x :: union l s'
               | Eq => x :: union l l'
               | Gt => x' :: union_aux l'
               end
           end)
    end.

  Fixpoint inter (s : t) : t -> t :=
    match s with
    | nil => fun _ => nil
    | x :: l =>
        (fix inter_aux (s' : t) : t :=
           match s' with
           | nil => nil
           | x' :: l' =>
               match X.compare x x' with
               | Lt => inter l s'
               | Eq => x :: inter l l'
               | Gt => inter_aux l'
               end
           end)
    end.

  Fixpoint diff (s : t) : t -> t :=
    match s with
    | nil => fun _ => nil
    | x :: l =>
        (fix diff_aux (s' : t) : t :=
           match s' with
           | nil => s
           | x' :: l' =>
               match X.compare x x' with
               | Lt => x :: diff l s'
               | Eq => diff l l'
               | Gt => diff_aux l'
               end
           end)
    end.

  Fixpoint equal (s : t) : t -> bool :=
    fun s' : t =>
    match s, s' with
    | nil, nil => true
    | x :: l, x' :: l' =>
        match X.compare x x' with
        | Eq => equal l l'
        | _ => false
        end
    | _, _ => false
    end.

  Fixpoint subset s s' :=
    match s, s' with
    | nil, _ => true
    | x :: l, x' :: l' =>
        match X.compare x x' with
        | Lt => false
        | Eq => subset l l'
        | Gt => subset s l'
        end
    | _, _ => false
    end.

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

  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 (x : t) : list elt := x.

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

  Fixpoint max_elt (s : t) : option elt :=
    match s with
    | nil => None
    | x :: nil => Some x
    | _ :: l => max_elt l
    end.

  Definition choose := min_elt.

  Fixpoint compare s s' :=
   match s, s' with
    | nil, nil => Eq
    | nil, _ => Lt
    | _, nil => Gt
    | x::s, x'::s' =>
      match X.compare x x' with
       | Eq => compare s s'
       | Lt => Lt
       | Gt => Gt
      end
   end.

End Ops.

Module MakeRaw (X: OrderedType) <: RawSets X.
  Module Import MX := OrderedTypeFacts X.
  Module Import ML := OrderedTypeLists X.

  Include Ops X.

Proofs of set operation specifications.

  Section ForNotations.

  Definition inf x l :=
   match l with
   | nil => true
   | y::_ => match X.compare x y with Lt => true | _ => false end
   end.

  Fixpoint isok l :=
   match l with
   | nil => true
   | x::l => inf x l && isok l
   end.

  Notation Sort l := (isok l = true).
  Notation Inf := (lelistA X.lt).
  Notation In := (InA X.eq).

  Existing Instance X.eq_equiv.
  Hint Extern 20 => solve [order] : core.

  Definition IsOk s := Sort s.

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

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

  Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }.

  Lemma inf_iff : forall x l, Inf x l <-> inf x l = true.forall (x : X.t) (l : list X.t),
Inf x l <-> inf x l = true
  Proof.forall (x : X.t) (l : list X.t),
Inf x l <-> inf x l = true
    intros x l; split; intro H.x:X.t
l:list X.t
H:Inf x l
inf x l = true
x:X.t
l:list X.t
H:inf x l = true
Inf x l
    (* -> *)
    destruct H; simpl in *.x:X.t
true = true
x, b:X.t
l:list X.t
H:X.lt x b
match X.compare x b with
| Lt => true
| _ => false
end = true
x:X.t
l:list X.t
H:inf x l = true
Inf x l
      reflexivity.x, b:X.t
l:list X.t
H:X.lt x b
match X.compare x b with
| Lt => true
| _ => false
end = true
x:X.t
l:list X.t
H:inf x l = true
Inf x l
    rewrite <- compare_lt_iff in H; rewrite H; reflexivity.x:X.t
l:list X.t
H:inf x l = true
Inf x l
    (* <- *)
    destruct l as [|y ys]; simpl in *.x:X.t
H:true = true
Inf x nil
x, y:X.t
ys:list X.t
H:match X.compare x y with
| Lt => true
| _ => false
end = true
Inf x (y :: ys)
      constructor; fail.x, y:X.t
ys:list X.t
H:match X.compare x y with
| Lt => true
| _ => false
end = true
Inf x (y :: ys)
    revert H; case_eq (X.compare x y); try discriminate; [].x, y:X.t
ys:list X.t
X.compare x y = Lt -> true = true -> Inf x (y :: ys)
    intros Ha _.x, y:X.t
ys:list X.t
Ha:X.compare x y = Lt
Inf x (y :: ys)
    rewrite compare_lt_iff in Ha.x, y:X.t
ys:list X.t
Ha:X.lt x y
Inf x (y :: ys)
    constructor; assumption.
  Qed.

  Lemma isok_iff : forall l, sort X.lt l <-> Ok l.forall l : list X.t, Sorted X.lt l <-> Ok l
  Proof.forall l : list X.t, Sorted X.lt l <-> Ok l
    intro l; split; intro H.l:list X.t
H:Sorted X.lt l
Ok l
l:list X.t
H:Ok l
Sorted X.lt l
    (* -> *)
    elim H.l:list X.t
H:Sorted X.lt l
Ok nil
l:list X.t
H:Sorted X.lt l
forall (a : X.t) (l0 : list X.t),
Sorted X.lt l0 -> Ok l0 -> Inf a l0 -> Ok (a :: l0)
l:list X.t
H:Ok l
Sorted X.lt l
      constructor; fail.l:list X.t
H:Sorted X.lt l
forall (a : X.t) (l0 : list X.t),
Sorted X.lt l0 -> Ok l0 -> Inf a l0 -> Ok (a :: l0)
l:list X.t
H:Ok l
Sorted X.lt l
    intros y ys Ha Hb Hc.l:list X.t
H:Sorted X.lt l
y:X.t
ys:list X.t
Ha:Sorted X.lt ys
Hb:Ok ys
Hc:Inf y ys
Ok (y :: ys)
l:list X.t
H:Ok l
Sorted X.lt l
    change (inf y ys && isok ys = true).l:list X.t
H:Sorted X.lt l
y:X.t
ys:list X.t
Ha:Sorted X.lt ys
Hb:Ok ys
Hc:Inf y ys
inf y ys && isok ys = true
l:list X.t
H:Ok l
Sorted X.lt l
    rewrite inf_iff in Hc.l:list X.t
H:Sorted X.lt l
y:X.t
ys:list X.t
Ha:Sorted X.lt ys
Hb:Ok ys
Hc:inf y ys = true
inf y ys && isok ys = true
l:list X.t
H:Ok l
Sorted X.lt l
    rewrite andb_true_iff; tauto.l:list X.t
H:Ok l
Sorted X.lt l
    (* <- *)
    induction l as [|x xs].H:Ok nil
Sorted X.lt nil
x:X.t
xs:list X.t
H:Ok (x :: xs)
IHxs:Ok xs -> Sorted X.lt xs
Sorted X.lt (x :: xs)
      constructor.x:X.t
xs:list X.t
H:Ok (x :: xs)
IHxs:Ok xs -> Sorted X.lt xs
Sorted X.lt (x :: xs)
    change (inf x xs && isok xs = true) in H.x:X.t
xs:list X.t
H:inf x xs && isok xs = true
IHxs:Ok xs -> Sorted X.lt xs
Sorted X.lt (x :: xs)
    rewrite andb_true_iff, <- inf_iff in H.x:X.t
xs:list X.t
H:Inf x xs /\ Sort xs
IHxs:Ok xs -> Sorted X.lt xs
Sorted X.lt (x :: xs)
    destruct H; constructor; tauto.
  Qed.

  Hint Extern 1 (Ok _) => rewrite <- isok_iff : core.

  Ltac inv_ok := match goal with
   | H:sort X.lt (_ :: _) |- _ => inversion_clear H; inv_ok
   | H:sort X.lt nil |- _ => clear H; inv_ok
   | H:sort X.lt ?l |- _ => change (Ok l) in H; inv_ok
   | H:Ok _ |- _ => rewrite <- isok_iff in H; inv_ok
   | |- Ok _ => rewrite <- isok_iff
   | _ => idtac
  end.

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

  Ltac sort_inf_in := match goal with
   | H:Inf ?x ?l, H':In ?y ?l |- _ =>
     cut (X.lt x y); [ intro | apply Sort_Inf_In with l; auto]
   | _ => fail
  end.

  Instance isok_Ok s `(isok s = true) : Ok s | 10.s:list X.t
H:Sort s
Ok s
  Proof.s:list X.t
H:Sort s
Ok s
  intros.s:list X.t
H:Sort s
Ok s assumption.
  Qed.

  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 : t) := exists x, In x s /\ P x.

  Lemma mem_spec :
   forall (s : t) (x : elt) (Hs : Ok s), mem x s = true <-> In x s.forall (s : t) (x : elt),
Ok s -> mem x s = true <-> In x s
  Proof.forall (s : t) (x : elt),
Ok s -> mem x s = true <-> In x s
  induction s; intros x Hs; inv; simpl.x:elt
false = true <-> In x nil
a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
match X.compare x a with
| Eq => true
| Lt => false
| Gt => mem x s
end = true <-> In x (a :: s)
  intuition.x:elt
H:false = true
In x nil
x:elt
H:In x nil
false = true
a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
match X.compare x a with
| Eq => true
| Lt => false
| Gt => mem x s
end = true <-> In x (a :: s) discriminate.x:elt
H:In x nil
false = true
a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
match X.compare x a with
| Eq => true
| Lt => false
| Gt => mem x s
end = true <-> In x (a :: s) inv.a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
match X.compare x a with
| Eq => true
| Lt => false
| Gt => mem x s
end = true <-> In x (a :: s)
  elim_compare x a; rewrite InA_cons; intuition; try order.a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
H1:X.lt x a
H2:false = true
X.eq x a \/ In x s
a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
H1:X.lt x a
H3:In x s
false = true
a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
H1:X.lt a x
H2:mem x s = true
X.eq x a \/ In x s
a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
H1:X.lt a x
H3:In x s
mem x s = true
  discriminate.a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
H1:X.lt x a
H3:In x s
false = true
a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
H1:X.lt a x
H2:mem x s = true
X.eq x a \/ In x s
a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
H1:X.lt a x
H3:In x s
mem x s = true
  sort_inf_in.a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
H1:X.lt x a
H3:In x s
H2:X.lt a x
false = true
a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
H1:X.lt a x
H2:mem x s = true
X.eq x a \/ In x s
a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
H1:X.lt a x
H3:In x s
mem x s = true order.a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
H1:X.lt a x
H2:mem x s = true
X.eq x a \/ In x s
a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
H1:X.lt a x
H3:In x s
mem x s = true
  rewrite <- IHs; auto.a:elt
s:list elt
IHs:forall x0 : elt, Ok s -> mem x0 s = true <-> In x0 s
x:elt
H:Sorted X.lt s
H0:Inf a s
H1:X.lt a x
H3:In x s
mem x s = true
  rewrite IHs; auto.
  Qed.

  Lemma add_inf :
   forall (s : t) (x a : elt), Inf a s -> X.lt a x -> Inf a (add x s).forall (s : t) (x a : elt),
Inf a s -> X.lt a x -> Inf a (add x s)
  Proof.forall (s : t) (x a : elt),
Inf a s -> X.lt a x -> Inf a (add x s)
  simple induction s; simpl.s:t
forall x a : elt,
Inf a nil -> X.lt a x -> Inf a (x :: nil)
s:t
forall (a : elt) (l : list elt),
(forall x a0 : elt,
 Inf a0 l -> X.lt a0 x -> Inf a0 (add x l)) ->
forall x a0 : elt,
Inf a0 (a :: l) ->
X.lt a0 x ->
Inf a0
  match X.compare x a with
  | Eq => a :: l
  | Lt => x :: a :: l
  | Gt => a :: add x l
  end
  intuition.s:t
forall (a : elt) (l : list elt),
(forall x a0 : elt,
 Inf a0 l -> X.lt a0 x -> Inf a0 (add x l)) ->
forall x a0 : elt,
Inf a0 (a :: l) ->
X.lt a0 x ->
Inf a0
  match X.compare x a with
  | Eq => a :: l
  | Lt => x :: a :: l
  | Gt => a :: add x l
  end
  intros; elim_compare x a; inv; intuition.
  Qed.
  Hint Resolve add_inf : core.

  Instance add_ok s x : forall `(Ok s), Ok (add x s).s:t
x:X.t
Ok s -> Ok (add x s)
  Proof.s:t
x:X.t
Ok s -> Ok (add x s)
  repeat rewrite <- isok_iff; revert s x.forall (s : t) (x : X.t),
Sorted X.lt s -> Sorted X.lt (add x s)
  simple induction s; simpl.s:t
forall x : X.t,
Sorted X.lt nil -> Sorted X.lt (x :: nil)
s:t
forall (a : elt) (l : list elt),
(forall x : X.t,
 Sorted X.lt l -> Sorted X.lt (add x l)) ->
forall x : X.t,
Sorted X.lt (a :: l) ->
Sorted X.lt
  match X.compare x a with
  | Eq => a :: l
  | Lt => x :: a :: l
  | Gt => a :: add x l
  end
  intuition.s:t
forall (a : elt) (l : list elt),
(forall x : X.t,
 Sorted X.lt l -> Sorted X.lt (add x l)) ->
forall x : X.t,
Sorted X.lt (a :: l) ->
Sorted X.lt
  match X.compare x a with
  | Eq => a :: l
  | Lt => x :: a :: l
  | Gt => a :: add x l
  end
  intros; elim_compare x a; inv; 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.forall (s : t) (x y : elt),
Ok s -> In y (add x s) <-> X.eq y x \/ In y s
  Proof.forall (s : t) (x y : elt),
Ok s -> In y (add x s) <-> X.eq y x \/ In y s
  induction s; simpl; intros.x, y:elt
Hs:Ok nil
In y (x :: nil) <-> X.eq y x \/ In y nil
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
  match X.compare x a with
  | Eq => a :: s
  | Lt => x :: a :: s
  | Gt => a :: add x s
  end <-> X.eq y x \/ In y (a :: s)
  intuition.x, y:elt
Hs:Ok nil
H:In y (x :: nil)
X.eq y x \/ In y nil
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
  match X.compare x a with
  | Eq => a :: s
  | Lt => x :: a :: s
  | Gt => a :: add x s
  end <-> X.eq y x \/ In y (a :: s) inv; auto.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
  match X.compare x a with
  | Eq => a :: s
  | Lt => x :: a :: s
  | Gt => a :: add x s
  end <-> X.eq y x \/ In y (a :: s)
  elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition.
  Qed.

  Lemma remove_inf :
   forall (s : t) (x a : elt) (Hs : Ok s), Inf a s -> Inf a (remove x s).forall (s : t) (x a : elt),
Ok s -> Inf a s -> Inf a (remove x s)
  Proof.forall (s : t) (x a : elt),
Ok s -> Inf a s -> Inf a (remove x s)
  induction s; simpl.elt ->
forall a : elt, Ok nil -> Inf a nil -> Inf a nil
a:elt
s:list elt
IHs:forall x a0 : elt, Ok s -> Inf a0 s -> Inf a0 (remove x s)
forall x a0 : elt,
Ok (a :: s) ->
Inf a0 (a :: s) ->
Inf a0
  match X.compare x a with
  | Eq => s
  | Lt => a :: s
  | Gt => a :: remove x s
  end
  intuition.a:elt
s:list elt
IHs:forall x a0 : elt, Ok s -> Inf a0 s -> Inf a0 (remove x s)
forall x a0 : elt,
Ok (a :: s) ->
Inf a0 (a :: s) ->
Inf a0
  match X.compare x a with
  | Eq => s
  | Lt => a :: s
  | Gt => a :: remove x s
  end
  intros; elim_compare x a; inv; auto.a:elt
s:list elt
IHs:forall x0 a1 : elt, Ok s -> Inf a1 s -> Inf a1 (remove x0 s)
x, a0:elt
H0:X.eq x a
H1:Sorted X.lt s
H2:Inf a s
H3:X.lt a0 a
Inf a0 s
  apply Inf_lt with a; auto.
  Qed.
  Hint Resolve remove_inf : core.

  Instance remove_ok s x : forall `(Ok s), Ok (remove x s).s:t
x:X.t
Ok s -> Ok (remove x s)
  Proof.s:t
x:X.t
Ok s -> Ok (remove x s)
  repeat rewrite <- isok_iff; revert s x.forall (s : t) (x : X.t),
Sorted X.lt s -> Sorted X.lt (remove x s)
  induction s; simpl.X.t -> Sorted X.lt nil -> Sorted X.lt nil
a:elt
s:list elt
IHs:forall x : X.t, Sorted X.lt s -> Sorted X.lt (remove x s)
forall x : X.t,
Sorted X.lt (a :: s) ->
Sorted X.lt
  match X.compare x a with
  | Eq => s
  | Lt => a :: s
  | Gt => a :: remove x s
  end
  intuition.a:elt
s:list elt
IHs:forall x : X.t, Sorted X.lt s -> Sorted X.lt (remove x s)
forall x : X.t,
Sorted X.lt (a :: s) ->
Sorted X.lt
  match X.compare x a with
  | Eq => s
  | Lt => a :: s
  | Gt => a :: remove x s
  end
  intros; elim_compare x a; inv; auto.
  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.forall (s : t) (x y : elt),
Ok s -> In y (remove x s) <-> In y s /\ ~ X.eq y x
  Proof.forall (s : t) (x y : elt),
Ok s -> In y (remove x s) <-> In y s /\ ~ X.eq y x
  induction s; simpl; intros.x, y:elt
Hs:Ok nil
In y nil <-> In y nil /\ ~ X.eq y x
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
  match X.compare x a with
  | Eq => s
  | Lt => a :: s
  | Gt => a :: remove x s
  end <-> In y (a :: s) /\ ~ X.eq y x
  intuition; inv; auto.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
  match X.compare x a with
  | Eq => s
  | Lt => a :: s
  | Gt => a :: remove x s
  end <-> In y (a :: s) /\ ~ X.eq y x
  elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition;
   try sort_inf_in; try order.
  Qed.

  Instance singleton_ok x : Ok (singleton x).x:elt
Ok (singleton x)
  Proof.x:elt
Ok (singleton x)
  unfold singleton; simpl; auto.
  Qed.

  Lemma singleton_spec : forall x y : elt, In y (singleton x) <-> X.eq y x.forall x y : elt, In y (singleton x) <-> X.eq y x
  Proof.forall x y : elt, In y (singleton x) <-> X.eq y x
  unfold singleton; simpl; split; intros; inv; auto.
  Qed.

  Ltac induction2 :=
    simple induction s;
     [ simpl; auto; try solve [ intros; inv ]
     | intros x l Hrec; simple induction s';
        [ simpl; auto; try solve [ intros; inv ]
        | intros x' l' Hrec'; simpl; elim_compare x x'; intros; inv; auto ]].

  Lemma union_inf :
   forall (s s' : t) (a : elt) (Hs : Ok s) (Hs' : Ok s'),
   Inf a s -> Inf a s' -> Inf a (union s s').forall (s s' : t) (a : elt),
Ok s ->
Ok s' -> Inf a s -> Inf a s' -> Inf a (union s s')
  Proof.forall (s s' : t) (a : elt),
Ok s ->
Ok s' -> Inf a s -> Inf a s' -> Inf a (union s s')
  induction2.
  Qed.
  Hint Resolve union_inf : core.

  Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s').s, s':t
Ok s -> Ok s' -> Ok (union s s')
  Proof.s, s':t
Ok s -> Ok s' -> Ok (union s s')
  repeat rewrite <- isok_iff; revert s s'.forall s s' : t,
Sorted X.lt s ->
Sorted X.lt s' -> Sorted X.lt (union s s')
  induction2; constructors; try apply @ok; auto.s:t
x:elt
l:list elt
Hrec:forall s'0 : t,
Sorted X.lt l ->
Sorted X.lt s'0 -> Sorted X.lt (union l s'0)
s':t
x':elt
l':list elt
Hrec':Sorted X.lt (x :: l) ->
Sorted X.lt l' ->
Sorted X.lt (union (x :: l) l')
H:X.eq x x'
H2:Sorted X.lt l'
H3:Inf x' l'
H1:Sorted X.lt l
H4:Inf x l
Inf x (union l l')
s:t
x:elt
l:list elt
Hrec:forall s'0 : t,
Sorted X.lt l ->
Sorted X.lt s'0 -> Sorted X.lt (union l s'0)
s':t
x':elt
l':list elt
Hrec':Sorted X.lt (x :: l) ->
Sorted X.lt l' ->
Sorted X.lt (union (x :: l) l')
H:X.lt x' x
H2:Sorted X.lt l'
H3:Inf x' l'
H1:Sorted X.lt l
H4:Inf x l
Inf x'
  ((fix union_aux (s'0 : t) : t :=
      match s'0 with
      | nil => x :: l
      | x'0 :: l'0 =>
          match X.compare x x'0 with
          | Eq => x :: union l l'0
          | Lt => x :: union l s'0
          | Gt => x'0 :: union_aux l'0
          end
      end) l') 
  apply Inf_eq with x'; auto; apply union_inf; auto; apply Inf_eq with x; auto; order.s:t
x:elt
l:list elt
Hrec:forall s'0 : t,
Sorted X.lt l ->
Sorted X.lt s'0 -> Sorted X.lt (union l s'0)
s':t
x':elt
l':list elt
Hrec':Sorted X.lt (x :: l) ->
Sorted X.lt l' ->
Sorted X.lt (union (x :: l) l')
H:X.lt x' x
H2:Sorted X.lt l'
H3:Inf x' l'
H1:Sorted X.lt l
H4:Inf x l
Inf x'
  ((fix union_aux (s'0 : t) : t :=
      match s'0 with
      | nil => x :: l
      | x'0 :: l'0 =>
          match X.compare x x'0 with
          | Eq => x :: union l l'0
          | Lt => x :: union l s'0
          | Gt => x'0 :: union_aux l'0
          end
      end) l')
  change (Inf x' (union (x :: l) l')); auto.
  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'.forall (s s' : t) (x : elt),
Ok s ->
Ok s' -> In x (union s s') <-> In x s \/ In x s'
  Proof.forall (s s' : t) (x : elt),
Ok s ->
Ok s' -> In x (union s s') <-> In x s \/ In x s'
  induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto.
  Qed.

  Lemma inter_inf :
   forall (s s' : t) (a : elt) (Hs : Ok s) (Hs' : Ok s'),
   Inf a s -> Inf a s' -> Inf a (inter s s').forall (s s' : t) (a : elt),
Ok s ->
Ok s' -> Inf a s -> Inf a s' -> Inf a (inter s s')
  Proof.forall (s s' : t) (a : elt),
Ok s ->
Ok s' -> Inf a s -> Inf a s' -> Inf a (inter s s')
  induction2.s:t
x:elt
l:list elt
Hrec:forall (s'0 : t) (a0 : elt),
Ok l ->
Ok s'0 ->
Inf a0 l -> Inf a0 s'0 -> Inf a0 (inter l s'0)
s':t
x':elt
l':list elt
Hrec':forall a0 : elt,
Ok (x :: l) ->
Ok l' ->
Inf a0 (x :: l) ->
Inf a0 l' -> Inf a0 (inter (x :: l) l')
H:X.lt x x'
a:elt
H2:Sorted X.lt l'
H3:Inf x' l'
H4:Sorted X.lt l
H5:Inf x l
H6:X.lt a x'
H1:X.lt a x
Inf a (inter l (x' :: l'))
s:t
x:elt
l:list elt
Hrec:forall (s'0 : t) (a0 : elt),
Ok l ->
Ok s'0 ->
Inf a0 l -> Inf a0 s'0 -> Inf a0 (inter l s'0)
s':t
x':elt
l':list elt
Hrec':forall a0 : elt,
Ok (x :: l) ->
Ok l' ->
Inf a0 (x :: l) ->
Inf a0 l' -> Inf a0 (inter (x :: l) l')
H:X.lt x' x
a:elt
H2:Sorted X.lt l'
H3:Inf x' l'
H4:Sorted X.lt l
H5:Inf x l
H6:X.lt a x'
H1:X.lt a x
Inf a
  ((fix inter_aux (s'0 : t) : t :=
      match s'0 with
      | nil => nil
      | x'0 :: l'0 =>
          match X.compare x x'0 with
          | Eq => x :: inter l l'0
          | Lt => inter l s'0
          | Gt => inter_aux l'0
          end
      end) l')
  apply Inf_lt with x; auto.s:t
x:elt
l:list elt
Hrec:forall (s'0 : t) (a0 : elt),
Ok l ->
Ok s'0 ->
Inf a0 l -> Inf a0 s'0 -> Inf a0 (inter l s'0)
s':t
x':elt
l':list elt
Hrec':forall a0 : elt,
Ok (x :: l) ->
Ok l' ->
Inf a0 (x :: l) ->
Inf a0 l' -> Inf a0 (inter (x :: l) l')
H:X.lt x' x
a:elt
H2:Sorted X.lt l'
H3:Inf x' l'
H4:Sorted X.lt l
H5:Inf x l
H6:X.lt a x'
H1:X.lt a x
Inf a
  ((fix inter_aux (s'0 : t) : t :=
      match s'0 with
      | nil => nil
      | x'0 :: l'0 =>
          match X.compare x x'0 with
          | Eq => x :: inter l l'0
          | Lt => inter l s'0
          | Gt => inter_aux l'0
          end
      end) l')
  apply Hrec'; auto.s:t
x:elt
l:list elt
Hrec:forall (s'0 : t) (a0 : elt),
Ok l ->
Ok s'0 ->
Inf a0 l -> Inf a0 s'0 -> Inf a0 (inter l s'0)
s':t
x':elt
l':list elt
Hrec':forall a0 : elt,
Ok (x :: l) ->
Ok l' ->
Inf a0 (x :: l) ->
Inf a0 l' -> Inf a0 (inter (x :: l) l')
H:X.lt x' x
a:elt
H2:Sorted X.lt l'
H3:Inf x' l'
H4:Sorted X.lt l
H5:Inf x l
H6:X.lt a x'
H1:X.lt a x
Inf a l'
  apply Inf_lt with x'; auto.
  Qed.
  Hint Resolve inter_inf : core.

  Instance inter_ok s s' : forall `(Ok s, Ok s'), Ok (inter s s').s, s':t
Ok s -> Ok s' -> Ok (inter s s')
  Proof.s, s':t
Ok s -> Ok s' -> Ok (inter s s')
  repeat rewrite <- isok_iff; revert s s'.forall s s' : t,
Sorted X.lt s ->
Sorted X.lt s' -> Sorted X.lt (inter s s')
  induction2.s:t
x:elt
l:list elt
Hrec:forall s'0 : t,
Sorted X.lt l ->
Sorted X.lt s'0 -> Sorted X.lt (inter l s'0)
s':t
x':elt
l':list elt
Hrec':Sorted X.lt (x :: l) ->
Sorted X.lt l' ->
Sorted X.lt (inter (x :: l) l')
H:X.eq x x'
H2:Sorted X.lt l'
H3:Inf x' l'
H1:Sorted X.lt l
H4:Inf x l
Sorted X.lt (x :: inter l l')
  constructors; auto.s:t
x:elt
l:list elt
Hrec:forall s'0 : t,
Sorted X.lt l ->
Sorted X.lt s'0 -> Sorted X.lt (inter l s'0)
s':t
x':elt
l':list elt
Hrec':Sorted X.lt (x :: l) ->
Sorted X.lt l' ->
Sorted X.lt (inter (x :: l) l')
H:X.eq x x'
H2:Sorted X.lt l'
H3:Inf x' l'
H1:Sorted X.lt l
H4:Inf x l
Inf x (inter l l')
  apply Inf_eq with x'; auto; apply inter_inf; auto; apply Inf_eq with x; auto.
  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'.forall (s s' : t) (x : elt),
Ok s ->
Ok s' -> In x (inter s s') <-> In x s /\ In x s'
  Proof.forall (s s' : t) (x : elt),
Ok s ->
Ok s' -> In x (inter s s') <-> In x s /\ In x s'
  induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto;
   try sort_inf_in; try order.
  Qed.

  Lemma diff_inf :
   forall (s s' : t) (Hs : Ok s) (Hs' : Ok s') (a : elt),
   Inf a s -> Inf a s' -> Inf a (diff s s').forall s s' : t,
Ok s ->
Ok s' ->
forall a : elt,
Inf a s -> Inf a s' -> Inf a (diff s s')
  Proof.forall s s' : t,
Ok s ->
Ok s' ->
forall a : elt,
Inf a s -> Inf a s' -> Inf a (diff s s')
  intros s s'; repeat rewrite <- isok_iff; revert s s'.forall s s' : t,
Sorted X.lt s ->
Sorted X.lt s' ->
forall a : elt,
Inf a s -> Inf a s' -> Inf a (diff s s')
  induction2.s:t
x:elt
l:list elt
Hrec:forall s'0 : t,
Sorted X.lt l ->
Sorted X.lt s'0 ->
forall a0 : elt,
Inf a0 l -> Inf a0 s'0 -> Inf a0 (diff l s'0)
s':t
x':elt
l':list elt
Hrec':Sorted X.lt (x :: l) ->
Sorted X.lt l' ->
forall a0 : elt,
Inf a0 (x :: l) ->
Inf a0 l' -> Inf a0 (diff (x :: l) l')
H:X.eq x x'
a:elt
H4:Sorted X.lt l'
H5:Inf x' l'
H1:Sorted X.lt l
H6:Inf x l
H0:X.lt a x'
H3:X.lt a x
Inf a (diff l l')
s:t
x:elt
l:list elt
Hrec:forall s'0 : t,
Sorted X.lt l ->
Sorted X.lt s'0 ->
forall a0 : elt,
Inf a0 l -> Inf a0 s'0 -> Inf a0 (diff l s'0)
s':t
x':elt
l':list elt
Hrec':Sorted X.lt (x :: l) ->
Sorted X.lt l' ->
forall a0 : elt,
Inf a0 (x :: l) ->
Inf a0 l' -> Inf a0 (diff (x :: l) l')
H:X.lt x' x
a:elt
H4:Sorted X.lt l'
H5:Inf x' l'
H1:Sorted X.lt l
H6:Inf x l
H0:X.lt a x'
H3:X.lt a x
Inf a
  ((fix diff_aux (s'0 : t) : t :=
      match s'0 with
      | nil => x :: l
      | x'0 :: l'0 =>
          match X.compare x x'0 with
          | Eq => diff l l'0
          | Lt => x :: diff l s'0
          | Gt => diff_aux l'0
          end
      end) l')
  apply Hrec; trivial.s:t
x:elt
l:list elt
Hrec:forall s'0 : t,
Sorted X.lt l ->
Sorted X.lt s'0 ->
forall a0 : elt,
Inf a0 l -> Inf a0 s'0 -> Inf a0 (diff l s'0)
s':t
x':elt
l':list elt
Hrec':Sorted X.lt (x :: l) ->
Sorted X.lt l' ->
forall a0 : elt,
Inf a0 (x :: l) ->
Inf a0 l' -> Inf a0 (diff (x :: l) l')
H:X.eq x x'
a:elt
H4:Sorted X.lt l'
H5:Inf x' l'
H1:Sorted X.lt l
H6:Inf x l
H0:X.lt a x'
H3:X.lt a x
Inf a l
s:t
x:elt
l:list elt
Hrec:forall s'0 : t,
Sorted X.lt l ->
Sorted X.lt s'0 ->
forall a0 : elt,
Inf a0 l -> Inf a0 s'0 -> Inf a0 (diff l s'0)
s':t
x':elt
l':list elt
Hrec':Sorted X.lt (x :: l) ->
Sorted X.lt l' ->
forall a0 : elt,
Inf a0 (x :: l) ->
Inf a0 l' -> Inf a0 (diff (x :: l) l')
H:X.eq x x'
a:elt
H4:Sorted X.lt l'
H5:Inf x' l'
H1:Sorted X.lt l
H6:Inf x l
H0:X.lt a x'
H3:X.lt a x
Inf a l'
s:t
x:elt
l:list elt
Hrec:forall s'0 : t,
Sorted X.lt l ->
Sorted X.lt s'0 ->
forall a0 : elt,
Inf a0 l -> Inf a0 s'0 -> Inf a0 (diff l s'0)
s':t
x':elt
l':list elt
Hrec':Sorted X.lt (x :: l) ->
Sorted X.lt l' ->
forall a0 : elt,
Inf a0 (x :: l) ->
Inf a0 l' -> Inf a0 (diff (x :: l) l')
H:X.lt x' x
a:elt
H4:Sorted X.lt l'
H5:Inf x' l'
H1:Sorted X.lt l
H6:Inf x l
H0:X.lt a x'
H3:X.lt a x
Inf a
  ((fix diff_aux (s'0 : t) : t :=
      match s'0 with
      | nil => x :: l
      | x'0 :: l'0 =>
          match X.compare x x'0 with
          | Eq => diff l l'0
          | Lt => x :: diff l s'0
          | Gt => diff_aux l'0
          end
      end) l')
  apply Inf_lt with x; auto.s:t
x:elt
l:list elt
Hrec:forall s'0 : t,
Sorted X.lt l ->
Sorted X.lt s'0 ->
forall a0 : elt,
Inf a0 l -> Inf a0 s'0 -> Inf a0 (diff l s'0)
s':t
x':elt
l':list elt
Hrec':Sorted X.lt (x :: l) ->
Sorted X.lt l' ->
forall a0 : elt,
Inf a0 (x :: l) ->
Inf a0 l' -> Inf a0 (diff (x :: l) l')
H:X.eq x x'
a:elt
H4:Sorted X.lt l'
H5:Inf x' l'
H1:Sorted X.lt l
H6:Inf x l
H0:X.lt a x'
H3:X.lt a x
Inf a l'
s:t
x:elt
l:list elt
Hrec:forall s'0 : t,
Sorted X.lt l ->
Sorted X.lt s'0 ->
forall a0 : elt,
Inf a0 l -> Inf a0 s'0 -> Inf a0 (diff l s'0)
s':t
x':elt
l':list elt
Hrec':Sorted X.lt (x :: l) ->
Sorted X.lt l' ->
forall a0 : elt,
Inf a0 (x :: l) ->
Inf a0 l' -> Inf a0 (diff (x :: l) l')
H:X.lt x' x
a:elt
H4:Sorted X.lt l'
H5:Inf x' l'
H1:Sorted X.lt l
H6:Inf x l
H0:X.lt a x'
H3:X.lt a x
Inf a
  ((fix diff_aux (s'0 : t) : t :=
      match s'0 with
      | nil => x :: l
      | x'0 :: l'0 =>
          match X.compare x x'0 with
          | Eq => diff l l'0
          | Lt => x :: diff l s'0
          | Gt => diff_aux l'0
          end
      end) l')
  apply Inf_lt with x'; auto.s:t
x:elt
l:list elt
Hrec:forall s'0 : t,
Sorted X.lt l ->
Sorted X.lt s'0 ->
forall a0 : elt,
Inf a0 l -> Inf a0 s'0 -> Inf a0 (diff l s'0)
s':t
x':elt
l':list elt
Hrec':Sorted X.lt (x :: l) ->
Sorted X.lt l' ->
forall a0 : elt,
Inf a0 (x :: l) ->
Inf a0 l' -> Inf a0 (diff (x :: l) l')
H:X.lt x' x
a:elt
H4:Sorted X.lt l'
H5:Inf x' l'
H1:Sorted X.lt l
H6:Inf x l
H0:X.lt a x'
H3:X.lt a x
Inf a
  ((fix diff_aux (s'0 : t) : t :=
      match s'0 with
      | nil => x :: l
      | x'0 :: l'0 =>
          match X.compare x x'0 with
          | Eq => diff l l'0
          | Lt => x :: diff l s'0
          | Gt => diff_aux l'0
          end
      end) l')
  apply Hrec'; auto.s:t
x:elt
l:list elt
Hrec:forall s'0 : t,
Sorted X.lt l ->
Sorted X.lt s'0 ->
forall a0 : elt,
Inf a0 l -> Inf a0 s'0 -> Inf a0 (diff l s'0)
s':t
x':elt
l':list elt
Hrec':Sorted X.lt (x :: l) ->
Sorted X.lt l' ->
forall a0 : elt,
Inf a0 (x :: l) ->
Inf a0 l' -> Inf a0 (diff (x :: l) l')
H:X.lt x' x
a:elt
H4:Sorted X.lt l'
H5:Inf x' l'
H1:Sorted X.lt l
H6:Inf x l
H0:X.lt a x'
H3:X.lt a x
Inf a l'
  apply Inf_lt with x'; auto.
  Qed.
  Hint Resolve diff_inf : core.

  Instance diff_ok s s' : forall `(Ok s, Ok s'), Ok (diff s s').s, s':t
Ok s -> Ok s' -> Ok (diff s s')
  Proof.s, s':t
Ok s -> Ok s' -> Ok (diff s s')
  repeat rewrite <- isok_iff; revert s s'.forall s s' : t,
Sorted X.lt s ->
Sorted X.lt s' -> Sorted X.lt (diff s s')
  induction2.
  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'.forall (s s' : t) (x : elt),
Ok s ->
Ok s' -> In x (diff s s') <-> In x s /\ ~ In x s'
  Proof.forall (s s' : t) (x : elt),
Ok s ->
Ok s' -> In x (diff s s') <-> In x s /\ ~ In x s'
  induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto;
   try sort_inf_in; try order.s:t
x:elt
l:list elt
Hrec:forall (s'0 : t) (x1 : elt),
Ok l ->
Ok s'0 ->
In x1 (diff l s'0) <->
In x1 l /\ (In x1 s'0 -> False)
s':t
x':elt
l':list elt
Hrec':forall x1 : elt,
Ok (x :: l) ->
Ok l' ->
In x1 (diff (x :: l) l') <->
In x1 (x :: l) /\ (In x1 l' -> False)
H:X.lt x x'
x0:elt
H0:Sorted X.lt l'
H1:Inf x' l'
H2:Sorted X.lt l
H3:Inf x l
H4:In x0 l
H5:X.eq x0 x' -> False
H7:In x0 l' -> False
H6:X.lt x x0
X.eq x0 x \/ In x0 l /\ (In x0 (x' :: l') -> False)
  right; intuition; inv; auto.
  Qed.

  Lemma equal_spec :
   forall (s s' : t) (Hs : Ok s) (Hs' : Ok s'),
   equal s s' = true <-> Equal s s'.forall s s' : t,
Ok s -> Ok s' -> equal s s' = true <-> Equal s s'
  Proof.forall s s' : t,
Ok s -> Ok s' -> equal s s' = true <-> Equal s s'
  induction s as [ | x s IH]; intros [ | x' s'] Hs Hs'; simpl.Hs, Hs':Ok nil
true = true <-> Equal nil nil
x':elt
s':list elt
Hs:Ok nil
Hs':Ok (x' :: s')
false = true <-> Equal nil (x' :: s')
x:elt
s:list elt
IH:forall s' : t,
Ok s -> Ok s' -> equal s s' = true <-> Equal s s'
Hs:Ok (x :: s)
Hs':Ok nil
false = true <-> Equal (x :: s) nil
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => equal s s'
| _ => false
end = true <-> Equal (x :: s) (x' :: s')
  intuition reflexivity.x':elt
s':list elt
Hs:Ok nil
Hs':Ok (x' :: s')
false = true <-> Equal nil (x' :: s')
x:elt
s:list elt
IH:forall s' : t,
Ok s -> Ok s' -> equal s s' = true <-> Equal s s'
Hs:Ok (x :: s)
Hs':Ok nil
false = true <-> Equal (x :: s) nil
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => equal s s'
| _ => false
end = true <-> Equal (x :: s) (x' :: s') 
  split; intros H.x':elt
s':list elt
Hs:Ok nil
Hs':Ok (x' :: s')
H:false = true
Equal nil (x' :: s')
x':elt
s':list elt
Hs:Ok nil
Hs':Ok (x' :: s')
H:Equal nil (x' :: s')
false = true
x:elt
s:list elt
IH:forall s' : t,
Ok s -> Ok s' -> equal s s' = true <-> Equal s s'
Hs:Ok (x :: s)
Hs':Ok nil
false = true <-> Equal (x :: s) nil
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => equal s s'
| _ => false
end = true <-> Equal (x :: s) (x' :: s') discriminate.x':elt
s':list elt
Hs:Ok nil
Hs':Ok (x' :: s')
H:Equal nil (x' :: s')
false = true
x:elt
s:list elt
IH:forall s' : t,
Ok s -> Ok s' -> equal s s' = true <-> Equal s s'
Hs:Ok (x :: s)
Hs':Ok nil
false = true <-> Equal (x :: s) nil
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => equal s s'
| _ => false
end = true <-> Equal (x :: s) (x' :: s') assert (In x' nil) by (rewrite H; auto).x':elt
s':list elt
Hs:Ok nil
Hs':Ok (x' :: s')
H:Equal nil (x' :: s')
H0:In x' nil
false = true
x:elt
s:list elt
IH:forall s' : t,
Ok s -> Ok s' -> equal s s' = true <-> Equal s s'
Hs:Ok (x :: s)
Hs':Ok nil
false = true <-> Equal (x :: s) nil
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => equal s s'
| _ => false
end = true <-> Equal (x :: s) (x' :: s') inv.x:elt
s:list elt
IH:forall s' : t,
Ok s -> Ok s' -> equal s s' = true <-> Equal s s'
Hs:Ok (x :: s)
Hs':Ok nil
false = true <-> Equal (x :: s) nil
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => equal s s'
| _ => false
end = true <-> Equal (x :: s) (x' :: s')
  split; intros H.x:elt
s:list elt
IH:forall s' : t,
Ok s -> Ok s' -> equal s s' = true <-> Equal s s'
Hs:Ok (x :: s)
Hs':Ok nil
H:false = true
Equal (x :: s) nil
x:elt
s:list elt
IH:forall s' : t,
Ok s -> Ok s' -> equal s s' = true <-> Equal s s'
Hs:Ok (x :: s)
Hs':Ok nil
H:Equal (x :: s) nil
false = true
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => equal s s'
| _ => false
end = true <-> Equal (x :: s) (x' :: s') discriminate.x:elt
s:list elt
IH:forall s' : t,
Ok s -> Ok s' -> equal s s' = true <-> Equal s s'
Hs:Ok (x :: s)
Hs':Ok nil
H:Equal (x :: s) nil
false = true
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => equal s s'
| _ => false
end = true <-> Equal (x :: s) (x' :: s') assert (In x nil) by (rewrite <-H; auto).x:elt
s:list elt
IH:forall s' : t,
Ok s -> Ok s' -> equal s s' = true <-> Equal s s'
Hs:Ok (x :: s)
Hs':Ok nil
H:Equal (x :: s) nil
H0:In x nil
false = true
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => equal s s'
| _ => false
end = true <-> Equal (x :: s) (x' :: s') inv.x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => equal s s'
| _ => false
end = true <-> Equal (x :: s) (x' :: s')
  inv.x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
match X.compare x x' with
| Eq => equal s s'
| _ => false
end = true <-> Equal (x :: s) (x' :: s')
  elim_compare x x' as C; try discriminate.x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.eq x x'
equal s s' = true <-> Equal (x :: s) (x' :: s')
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
false = true <-> Equal (x :: s) (x' :: s')
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
false = true <-> Equal (x :: s) (x' :: s')
  (* x=x' *)
  rewrite IH; auto.x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.eq x x'
Equal s s' <-> Equal (x :: s) (x' :: s')
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
false = true <-> Equal (x :: s) (x' :: s')
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
false = true <-> Equal (x :: s) (x' :: s')
  split; intros E y; specialize (E y).x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.eq x x'
y:elt
E:In y s <-> In y s'
In y (x :: s) <-> In y (x' :: s')
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.eq x x'
y:elt
E:In y (x :: s) <-> In y (x' :: s')
In y s <-> In y s'
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
false = true <-> Equal (x :: s) (x' :: s')
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
false = true <-> Equal (x :: s) (x' :: s')
  rewrite !InA_cons, E, C; intuition.x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.eq x x'
y:elt
E:In y (x :: s) <-> In y (x' :: s')
In y s <-> In y s'
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
false = true <-> Equal (x :: s) (x' :: s')
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
false = true <-> Equal (x :: s) (x' :: s')
  rewrite !InA_cons, C in E.x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.eq x x'
y:elt
E:X.eq y x' \/ In y s <-> X.eq y x' \/ In y s'
In y s <-> In y s'
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
false = true <-> Equal (x :: s) (x' :: s')
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
false = true <-> Equal (x :: s) (x' :: s') intuition; try sort_inf_in; order.x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
false = true <-> Equal (x :: s) (x' :: s')
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
false = true <-> Equal (x :: s) (x' :: s')
  (* x<x' *)
  split; intros E.x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
E:false = true
Equal (x :: s) (x' :: s')
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
E:Equal (x :: s) (x' :: s')
false = true
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
false = true <-> Equal (x :: s) (x' :: s') discriminate.x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
E:Equal (x :: s) (x' :: s')
false = true
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
false = true <-> Equal (x :: s) (x' :: s')
  assert (In x (x'::s')) by (rewrite <- E; auto).x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
E:Equal (x :: s) (x' :: s')
H3:In x (x' :: s')
false = true
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
false = true <-> Equal (x :: s) (x' :: s')
  inv; try sort_inf_in; order.x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
false = true <-> Equal (x :: s) (x' :: s')
  (* x>x' *)
  split; intros E.x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
E:false = true
Equal (x :: s) (x' :: s')
x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
E:Equal (x :: s) (x' :: s')
false = true discriminate.x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
E:Equal (x :: s) (x' :: s')
false = true
  assert (In x' (x::s)) by (rewrite E; auto).x:elt
s:list elt
IH:forall s'0 : t,
Ok s ->
Ok s'0 -> equal s s'0 = true <-> Equal s s'0
x':elt
s':list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
E:Equal (x :: s) (x' :: s')
H3:In x' (x :: s)
false = true
  inv; try sort_inf_in; order.
  Qed.

  Lemma subset_spec :
   forall (s s' : t) (Hs : Ok s) (Hs' : Ok s'),
   subset s s' = true <-> Subset s s'.forall s s' : t,
Ok s -> Ok s' -> subset s s' = true <-> Subset s s'
  Proof.forall s s' : t,
Ok s -> Ok s' -> subset s s' = true <-> Subset s s'
  intros s s'; revert s.s':t
forall s : t,
Ok s -> Ok s' -> subset s s' = true <-> Subset s s'
  induction s' as [ | x' s' IH]; intros [ | x s] Hs Hs'; simpl; auto.Hs, Hs':Ok nil
true = true <-> Subset nil nil
x:elt
s:list elt
Hs:Ok (x :: s)
Hs':Ok nil
false = true <-> Subset (x :: s) nil
x':elt
s':list elt
IH:forall s : t,
Ok s ->
Ok s' -> subset s s' = true <-> Subset s s'
Hs:Ok nil
Hs':Ok (x' :: s')
true = true <-> Subset nil (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => subset s s'
| Lt => false
| Gt => subset (x :: s) s'
end = true <-> Subset (x :: s) (x' :: s')
  split; try red; intros; auto.x:elt
s:list elt
Hs:Ok (x :: s)
Hs':Ok nil
false = true <-> Subset (x :: s) nil
x':elt
s':list elt
IH:forall s : t,
Ok s ->
Ok s' -> subset s s' = true <-> Subset s s'
Hs:Ok nil
Hs':Ok (x' :: s')
true = true <-> Subset nil (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => subset s s'
| Lt => false
| Gt => subset (x :: s) s'
end = true <-> Subset (x :: s) (x' :: s')
  split; intros H.x:elt
s:list elt
Hs:Ok (x :: s)
Hs':Ok nil
H:false = true
Subset (x :: s) nil
x:elt
s:list elt
Hs:Ok (x :: s)
Hs':Ok nil
H:Subset (x :: s) nil
false = true
x':elt
s':list elt
IH:forall s : t,
Ok s ->
Ok s' -> subset s s' = true <-> Subset s s'
Hs:Ok nil
Hs':Ok (x' :: s')
true = true <-> Subset nil (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => subset s s'
| Lt => false
| Gt => subset (x :: s) s'
end = true <-> Subset (x :: s) (x' :: s') discriminate.x:elt
s:list elt
Hs:Ok (x :: s)
Hs':Ok nil
H:Subset (x :: s) nil
false = true
x':elt
s':list elt
IH:forall s : t,
Ok s ->
Ok s' -> subset s s' = true <-> Subset s s'
Hs:Ok nil
Hs':Ok (x' :: s')
true = true <-> Subset nil (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => subset s s'
| Lt => false
| Gt => subset (x :: s) s'
end = true <-> Subset (x :: s) (x' :: s') assert (In x nil) by (apply H; auto).x:elt
s:list elt
Hs:Ok (x :: s)
Hs':Ok nil
H:Subset (x :: s) nil
H0:In x nil
false = true
x':elt
s':list elt
IH:forall s : t,
Ok s ->
Ok s' -> subset s s' = true <-> Subset s s'
Hs:Ok nil
Hs':Ok (x' :: s')
true = true <-> Subset nil (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => subset s s'
| Lt => false
| Gt => subset (x :: s) s'
end = true <-> Subset (x :: s) (x' :: s') inv.x':elt
s':list elt
IH:forall s : t,
Ok s ->
Ok s' -> subset s s' = true <-> Subset s s'
Hs:Ok nil
Hs':Ok (x' :: s')
true = true <-> Subset nil (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => subset s s'
| Lt => false
| Gt => subset (x :: s) s'
end = true <-> Subset (x :: s) (x' :: s')
  split; try red; intros; auto.x':elt
s':list elt
IH:forall s : t,
Ok s ->
Ok s' -> subset s s' = true <-> Subset s s'
Hs:Ok nil
Hs':Ok (x' :: s')
H:true = true
a:elt
H0:In a nil
In a (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => subset s s'
| Lt => false
| Gt => subset (x :: s) s'
end = true <-> Subset (x :: s) (x' :: s') inv.x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
Hs:Ok (x :: s)
Hs':Ok (x' :: s')
match X.compare x x' with
| Eq => subset s s'
| Lt => false
| Gt => subset (x :: s) s'
end = true <-> Subset (x :: s) (x' :: s')
  inv.x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
match X.compare x x' with
| Eq => subset s s'
| Lt => false
| Gt => subset (x :: s) s'
end = true <-> Subset (x :: s) (x' :: s') elim_compare x x' as C.x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.eq x x'
subset s s' = true <-> Subset (x :: s) (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
false = true <-> Subset (x :: s) (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
subset (x :: s) s' = true <->
Subset (x :: s) (x' :: s')
  (* x=x' *)
  rewrite IH; auto.x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.eq x x'
Subset s s' <-> Subset (x :: s) (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
false = true <-> Subset (x :: s) (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
subset (x :: s) s' = true <->
Subset (x :: s) (x' :: s')
  split; intros S y; specialize (S y).x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.eq x x'
y:elt
S:In y s -> In y s'
In y (x :: s) -> In y (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.eq x x'
y:elt
S:In y (x :: s) -> In y (x' :: s')
In y s -> In y s'
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
false = true <-> Subset (x :: s) (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
subset (x :: s) s' = true <->
Subset (x :: s) (x' :: s')
  rewrite !InA_cons, C.x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.eq x x'
y:elt
S:In y s -> In y s'
X.eq y x' \/ In y s -> X.eq y x' \/ In y s'
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.eq x x'
y:elt
S:In y (x :: s) -> In y (x' :: s')
In y s -> In y s'
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
false = true <-> Subset (x :: s) (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
subset (x :: s) s' = true <->
Subset (x :: s) (x' :: s') intuition.x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.eq x x'
y:elt
S:In y (x :: s) -> In y (x' :: s')
In y s -> In y s'
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
false = true <-> Subset (x :: s) (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
subset (x :: s) s' = true <->
Subset (x :: s) (x' :: s')
  rewrite !InA_cons, C in S.x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.eq x x'
y:elt
S:X.eq y x' \/ In y s -> X.eq y x' \/ In y s'
In y s -> In y s'
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
false = true <-> Subset (x :: s) (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
subset (x :: s) s' = true <->
Subset (x :: s) (x' :: s') intuition; try sort_inf_in; order.x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
false = true <-> Subset (x :: s) (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
subset (x :: s) s' = true <->
Subset (x :: s) (x' :: s')
  (* x<x' *)
  split; intros S.x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
S:false = true
Subset (x :: s) (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
S:Subset (x :: s) (x' :: s')
false = true
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
subset (x :: s) s' = true <->
Subset (x :: s) (x' :: s') discriminate.x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
S:Subset (x :: s) (x' :: s')
false = true
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
subset (x :: s) s' = true <->
Subset (x :: s) (x' :: s')
  assert (In x (x'::s')) by (apply S; auto).x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x x'
S:Subset (x :: s) (x' :: s')
H3:In x (x' :: s')
false = true
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
subset (x :: s) s' = true <->
Subset (x :: s) (x' :: s')
  inv; try sort_inf_in; order.x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
subset (x :: s) s' = true <->
Subset (x :: s) (x' :: s')
  (* x>x' *)
  rewrite IH; auto.x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
Subset (x :: s) s' <-> Subset (x :: s) (x' :: s')
  split; intros S y; specialize (S y).x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
y:elt
S:In y (x :: s) -> In y s'
In y (x :: s) -> In y (x' :: s')
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
y:elt
S:In y (x :: s) -> In y (x' :: s')
In y (x :: s) -> In y s'
  rewrite !InA_cons.x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
y:elt
S:In y (x :: s) -> In y s'
X.eq y x \/ In y s -> X.eq y x' \/ In y s'
x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
y:elt
S:In y (x :: s) -> In y (x' :: s')
In y (x :: s) -> In y s' intuition.x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
y:elt
S:In y (x :: s) -> In y (x' :: s')
In y (x :: s) -> In y s'
  rewrite !InA_cons in S.x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
y:elt
S:X.eq y x \/ In y s -> X.eq y x' \/ In y s'
In y (x :: s) -> In y s' rewrite !InA_cons.x':elt
s':list elt
IH:forall s0 : t,
Ok s0 ->
Ok s' -> subset s0 s' = true <-> Subset s0 s'
x:elt
s:list elt
H:Sorted X.lt s'
H0:Inf x' s'
H1:Sorted X.lt s
H2:Inf x s
C:X.lt x' x
y:elt
S:X.eq y x \/ In y s -> X.eq y x' \/ In y s'
X.eq y x \/ In y s -> In y s' intuition; try sort_inf_in; order.
  Qed.

  Instance empty_ok : Ok empty.Ok empty
  Proof.Ok empty
  constructors.
  Qed.

  Lemma empty_spec : Empty empty.Empty empty
  Proof.Empty empty
  unfold Empty, empty; intuition; inv.
  Qed.

  Lemma is_empty_spec : forall s : t, is_empty s = true <-> Empty s.forall s : t, is_empty s = true <-> Empty s
  Proof.forall s : t, is_empty s = true <-> Empty s
  intros [ | x s]; simpl.true = true <-> Empty nil
x:elt
s:list elt
false = true <-> Empty (x :: s)
  split; auto.true = true -> Empty nil
x:elt
s:list elt
false = true <-> Empty (x :: s) intros _ x H.x:elt
H:In x nil
False
x:elt
s:list elt
false = true <-> Empty (x :: s) inv.x:elt
s:list elt
false = true <-> Empty (x :: s)
  split.x:elt
s:list elt
false = true -> Empty (x :: s)
x:elt
s:list elt
Empty (x :: s) -> false = true discriminate.x:elt
s:list elt
Empty (x :: s) -> false = true intros H.x:elt
s:list elt
H:Empty (x :: s)
false = true elim (H x); auto.
  Qed.

  Lemma elements_spec1 : forall (s : t) (x : elt), In x (elements s) <-> In x s.forall (s : t) (x : elt), In x (elements s) <-> In x s
  Proof.forall (s : t) (x : elt), In x (elements s) <-> In x s
  intuition.
  Qed.

  Lemma elements_spec2 : forall (s : t) (Hs : Ok s), sort X.lt (elements s).forall s : t, Ok s -> Sorted X.lt (elements s)
  Proof.forall s : t, Ok s -> Sorted X.lt (elements s)
  intro s; repeat rewrite <- isok_iff; auto.
  Qed.

  Lemma elements_spec2w : forall (s : t) (Hs : Ok s), NoDupA X.eq (elements s).forall s : t, Ok s -> NoDupA X.eq (elements s)
  Proof.forall s : t, Ok s -> NoDupA X.eq (elements s)
  intro s; repeat rewrite <- isok_iff; auto.
  Qed.

  Lemma min_elt_spec1 : forall (s : t) (x : elt), min_elt s = Some x -> In x s.forall (s : t) (x : elt), min_elt s = Some x -> In x s
  Proof.forall (s : t) (x : elt), min_elt s = Some x -> In x s
  destruct s; simpl; inversion 1; auto.
  Qed.

  Lemma min_elt_spec2 :
   forall (s : t) (x y : elt) (Hs : Ok s),
   min_elt s = Some x -> In y s -> ~ X.lt y x.forall (s : t) (x y : elt),
Ok s -> min_elt s = Some x -> In y s -> ~ X.lt y x
  Proof.forall (s : t) (x y : elt),
Ok s -> min_elt s = Some x -> In y s -> ~ X.lt y x
  induction s as [ | x s IH]; simpl; inversion 2; subst.s:list elt
IH:forall x y0 : elt,
Ok s ->
min_elt s = Some x -> In y0 s -> ~ X.lt y0 x
x0, y:elt
H:Some x0 = Some x0
Hs:Ok (x0 :: s)
In y (x0 :: s) -> ~ X.lt y x0
  intros; inv; try sort_inf_in; order.
  Qed.

  Lemma min_elt_spec3 : forall s : t, min_elt s = None -> Empty s.forall s : t, min_elt s = None -> Empty s
  Proof.forall s : t, min_elt s = None -> Empty s
  destruct s; simpl; red; intuition.H:None = None
a:elt
H0:In a nil
False
e:elt
s:list elt
H:Some e = None
a:elt
H0:In a (e :: s)
False inv.e:elt
s:list elt
H:Some e = None
a:elt
H0:In a (e :: s)
False discriminate.
  Qed.

  Lemma max_elt_spec1 : forall (s : t) (x : elt), max_elt s = Some x -> In x s.forall (s : t) (x : elt), max_elt s = Some x -> In x s
  Proof.forall (s : t) (x : elt), max_elt s = Some x -> In x s
  induction s as [ | x s IH].forall x : elt, max_elt nil = Some x -> In x nil
x:elt
s:list elt
IH:forall x0 : elt, max_elt s = Some x0 -> In x0 s
forall x0 : elt,
max_elt (x :: s) = Some x0 -> In x0 (x :: s) inversion 1.x:elt
s:list elt
IH:forall x0 : elt, max_elt s = Some x0 -> In x0 s
forall x0 : elt,
max_elt (x :: s) = Some x0 -> In x0 (x :: s)
  destruct s as [ | y s].x:elt
IH:forall x0 : elt,
max_elt nil = Some x0 -> In x0 nil
forall x0 : elt,
max_elt (x :: nil) = Some x0 -> In x0 (x :: nil)
x, y:elt
s:list elt
IH:forall x0 : elt,
max_elt (y :: s) = Some x0 -> In x0 (y :: s)
forall x0 : elt,
max_elt (x :: y :: s) = Some x0 -> In x0 (x :: y :: s) simpl.x:elt
IH:forall x0 : elt,
max_elt nil = Some x0 -> In x0 nil
forall x0 : elt, Some x = Some x0 -> In x0 (x :: nil)
x, y:elt
s:list elt
IH:forall x0 : elt,
max_elt (y :: s) = Some x0 -> In x0 (y :: s)
forall x0 : elt,
max_elt (x :: y :: s) = Some x0 -> In x0 (x :: y :: s) inversion 1; subst; auto.x, y:elt
s:list elt
IH:forall x0 : elt,
max_elt (y :: s) = Some x0 -> In x0 (y :: s)
forall x0 : elt,
max_elt (x :: y :: s) = Some x0 -> In x0 (x :: y :: s)
  right; apply IH; auto.
  Qed.

  Lemma max_elt_spec2 :
   forall (s : t) (x y : elt) (Hs : Ok s),
   max_elt s = Some x -> In y s -> ~ X.lt x y.forall (s : t) (x y : elt),
Ok s -> max_elt s = Some x -> In y s -> ~ X.lt x y
  Proof.forall (s : t) (x y : elt),
Ok s -> max_elt s = Some x -> In y s -> ~ X.lt x y
  induction s as [ | a s IH].forall x y : elt,
Ok nil ->
max_elt nil = Some x -> In y nil -> ~ X.lt x y
a:elt
s:list elt
IH:forall x y : elt,
Ok s ->
max_elt s = Some x -> In y s -> ~ X.lt x y
forall x y : elt,
Ok (a :: s) ->
max_elt (a :: s) = Some x ->
In y (a :: s) -> ~ X.lt x y inversion 2.a:elt
s:list elt
IH:forall x y : elt,
Ok s ->
max_elt s = Some x -> In y s -> ~ X.lt x y
forall x y : elt,
Ok (a :: s) ->
max_elt (a :: s) = Some x ->
In y (a :: s) -> ~ X.lt x y
  destruct s as [ | b s].a:elt
IH:forall x y : elt,
Ok nil ->
max_elt nil = Some x -> In y nil -> ~ X.lt x y
forall x y : elt,
Ok (a :: nil) ->
max_elt (a :: nil) = Some x ->
In y (a :: nil) -> ~ X.lt x y
a, b:elt
s:list elt
IH:forall x y : elt,
Ok (b :: s) ->
max_elt (b :: s) = Some x ->
In y (b :: s) -> ~ X.lt x y
forall x y : elt,
Ok (a :: b :: s) ->
max_elt (a :: b :: s) = Some x ->
In y (a :: b :: s) -> ~ X.lt x y inversion 2; subst.IH:forall x0 y0 : elt,
Ok nil ->
max_elt nil = Some x0 ->
In y0 nil -> ~ X.lt x0 y0
x, y:elt
H:max_elt (x :: nil) = Some x
Hs:Ok (x :: nil)
In y (x :: nil) -> ~ X.lt x y
a, b:elt
s:list elt
IH:forall x y : elt,
Ok (b :: s) ->
max_elt (b :: s) = Some x ->
In y (b :: s) -> ~ X.lt x y
forall x y : elt,
Ok (a :: b :: s) ->
max_elt (a :: b :: s) = Some x ->
In y (a :: b :: s) -> ~ X.lt x y intros; inv; order.a, b:elt
s:list elt
IH:forall x y : elt,
Ok (b :: s) ->
max_elt (b :: s) = Some x ->
In y (b :: s) -> ~ X.lt x y
forall x y : elt,
Ok (a :: b :: s) ->
max_elt (a :: b :: s) = Some x ->
In y (a :: b :: s) -> ~ X.lt x y
  intros.a, b:elt
s:list elt
IH:forall x0 y0 : elt,
Ok (b :: s) ->
max_elt (b :: s) = Some x0 ->
In y0 (b :: s) -> ~ X.lt x0 y0
x, y:elt
Hs:Ok (a :: b :: s)
H:max_elt (a :: b :: s) = Some x
H0:In y (a :: b :: s)
~ X.lt x y inv; auto.a, b:elt
s:list elt
IH:forall x0 y0 : elt,
Ok (b :: s) ->
max_elt (b :: s) = Some x0 ->
In y0 (b :: s) -> ~ X.lt x0 y0
x, y:elt
H:max_elt (a :: b :: s) = Some x
H1:X.eq y a
H3:Sorted X.lt s
H4:Inf b s
H0:X.lt a b
~ X.lt x y
  assert (~X.lt x b) by (apply IH; auto).a, b:elt
s:list elt
IH:forall x0 y0 : elt,
Ok (b :: s) ->
max_elt (b :: s) = Some x0 ->
In y0 (b :: s) -> ~ X.lt x0 y0
x, y:elt
H:max_elt (a :: b :: s) = Some x
H1:X.eq y a
H3:Sorted X.lt s
H4:Inf b s
H0:X.lt a b
H2:~ X.lt x b
~ X.lt x y
  assert (X.lt a b) by auto.a, b:elt
s:list elt
IH:forall x0 y0 : elt,
Ok (b :: s) ->
max_elt (b :: s) = Some x0 ->
In y0 (b :: s) -> ~ X.lt x0 y0
x, y:elt
H:max_elt (a :: b :: s) = Some x
H1:X.eq y a
H3:Sorted X.lt s
H4:Inf b s
H0:X.lt a b
H2:~ X.lt x b
H5:X.lt a b
~ X.lt x y
  order.
  Qed.

  Lemma max_elt_spec3 : forall s : t, max_elt s = None -> Empty s.forall s : t, max_elt s = None -> Empty s
  Proof.forall s : t, max_elt s = None -> Empty s
  induction s as [ | a s IH].max_elt nil = None -> Empty nil
a:elt
s:list elt
IH:max_elt s = None -> Empty s
max_elt (a :: s) = None -> Empty (a :: s) red; intuition; inv.a:elt
s:list elt
IH:max_elt s = None -> Empty s
max_elt (a :: s) = None -> Empty (a :: s)
  destruct s as [ | b s].a:elt
IH:max_elt nil = None -> Empty nil
max_elt (a :: nil) = None -> Empty (a :: nil)
a, b:elt
s:list elt
IH:max_elt (b :: s) = None -> Empty (b :: s)
max_elt (a :: b :: s) = None -> Empty (a :: b :: s) inversion 1.a, b:elt
s:list elt
IH:max_elt (b :: s) = None -> Empty (b :: s)
max_elt (a :: b :: s) = None -> Empty (a :: b :: s)
  intros; elim IH with b; auto.
  Qed.

  Definition choose_spec1 :
    forall (s : t) (x : elt), choose s = Some x -> In x s := min_elt_spec1.

  Definition choose_spec2 :
    forall s : t, choose s = None -> Empty s := min_elt_spec3.

  Lemma choose_spec3: forall s s' x x', Ok s -> Ok s' ->
   choose s = Some x -> choose s' = Some x' -> Equal s s' -> X.eq x x'.forall (s s' : t) (x x' : elt),
Ok s ->
Ok s' ->
choose s = Some x ->
choose s' = Some x' -> Equal s s' -> X.eq x x'
  Proof.forall (s s' : t) (x x' : elt),
Ok s ->
Ok s' ->
choose s = Some x ->
choose s' = Some x' -> Equal s s' -> X.eq x x'
   unfold choose; intros s s' x x' Hs Hs' Hx Hx' H.s, s':t
x, x':elt
Hs:Ok s
Hs':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:Equal s s'
X.eq x x'
   assert (~X.lt x x').s, s':t
x, x':elt
Hs:Ok s
Hs':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:Equal s s'
~ X.lt x x'
s, s':t
x, x':elt
Hs:Ok s
Hs':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:Equal s s'
H0:~ X.lt x x'
X.eq x x'
    apply min_elt_spec2 with s'; auto.s, s':t
x, x':elt
Hs:Ok s
Hs':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:Equal s s'
In x s'
s, s':t
x, x':elt
Hs:Ok s
Hs':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:Equal s s'
H0:~ X.lt x x'
X.eq x x'
    rewrite <-H; auto using min_elt_spec1.s, s':t
x, x':elt
Hs:Ok s
Hs':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:Equal s s'
H0:~ X.lt x x'
X.eq x x'
   assert (~X.lt x' x).s, s':t
x, x':elt
Hs:Ok s
Hs':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:Equal s s'
H0:~ X.lt x x'
~ X.lt x' x
s, s':t
x, x':elt
Hs:Ok s
Hs':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:Equal s s'
H0:~ X.lt x x'
H1:~ X.lt x' x
X.eq x x'
    apply min_elt_spec2 with s; auto.s, s':t
x, x':elt
Hs:Ok s
Hs':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:Equal s s'
H0:~ X.lt x x'
In x' s
s, s':t
x, x':elt
Hs:Ok s
Hs':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:Equal s s'
H0:~ X.lt x x'
H1:~ X.lt x' x
X.eq x x'
    rewrite H; auto using min_elt_spec1.s, s':t
x, x':elt
Hs:Ok s
Hs':Ok s'
Hx:min_elt s = Some x
Hx':min_elt s' = Some x'
H:Equal s s'
H0:~ X.lt x x'
H1:~ X.lt x' x
X.eq x x'
   order.
  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.forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (flip f) (elements s) i
  Proof.forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (flip f) (elements s) i
  reflexivity.
  Qed.

  Lemma cardinal_spec :
   forall (s : t) (Hs : Ok s),
   cardinal s = length (elements s).forall s : t, Ok s -> cardinal s = length (elements s)
  Proof.forall s : t, Ok s -> cardinal s = length (elements s)
  auto.
  Qed.

  Lemma filter_inf :
   forall (s : t) (x : elt) (f : elt -> bool) (Hs : Ok s),
   Inf x s -> Inf x (filter f s).forall (s : t) (x : elt) (f : elt -> bool),
Ok s -> Inf x s -> Inf x (filter f s)
  Proof.forall (s : t) (x : elt) (f : elt -> bool),
Ok s -> Inf x s -> Inf x (filter f s)
  simple induction s; simpl.s:t
forall x : elt,
(elt -> bool) -> Ok nil -> Inf x nil -> Inf x nil
s:t
forall (a : elt) (l : list elt),
(forall (x : elt) (f : elt -> bool),
 Ok l -> Inf x l -> Inf x (filter f l)) ->
forall (x : elt) (f : elt -> bool),
Ok (a :: l) ->
Inf x (a :: l) ->
Inf x (if f a then a :: filter f l else filter f l)
  intuition.s:t
forall (a : elt) (l : list elt),
(forall (x : elt) (f : elt -> bool),
 Ok l -> Inf x l -> Inf x (filter f l)) ->
forall (x : elt) (f : elt -> bool),
Ok (a :: l) ->
Inf x (a :: l) ->
Inf x (if f a then a :: filter f l else filter f l)
  intros x l Hrec a f Hs Ha; inv.s:t
x:elt
l:list elt
Hrec:forall (x0 : elt) (f0 : elt -> bool),
Ok l -> Inf x0 l -> Inf x0 (filter f0 l)
a:elt
f:elt -> bool
H:Sorted X.lt l
H0:Inf x l
H1:X.lt a x
Inf a (if f x then x :: filter f l else filter f l)
  case (f x); auto.s:t
x:elt
l:list elt
Hrec:forall (x0 : elt) (f0 : elt -> bool),
Ok l -> Inf x0 l -> Inf x0 (filter f0 l)
a:elt
f:elt -> bool
H:Sorted X.lt l
H0:Inf x l
H1:X.lt a x
Inf a (filter f l)
  apply Hrec; auto.s:t
x:elt
l:list elt
Hrec:forall (x0 : elt) (f0 : elt -> bool),
Ok l -> Inf x0 l -> Inf x0 (filter f0 l)
a:elt
f:elt -> bool
H:Sorted X.lt l
H0:Inf x l
H1:X.lt a x
Inf a l
  apply Inf_lt with x; auto.
  Qed.

  Instance filter_ok s f : forall `(Ok s), Ok (filter f s).s:t
f:elt -> bool
Ok s -> Ok (filter f s)
  Proof.s:t
f:elt -> bool
Ok s -> Ok (filter f s)
  repeat rewrite <- isok_iff; revert s f.forall (s : t) (f : elt -> bool),
Sorted X.lt s -> Sorted X.lt (filter f s)
  simple induction s; simpl.s:t
(elt -> bool) -> Sorted X.lt nil -> Sorted X.lt nil
s:t
forall (a : elt) (l : list elt),
(forall f : elt -> bool,
 Sorted X.lt l -> Sorted X.lt (filter f l)) ->
forall f : elt -> bool,
Sorted X.lt (a :: l) ->
Sorted X.lt
  (if f a then a :: filter f l else filter f l)
  auto.s:t
forall (a : elt) (l : list elt),
(forall f : elt -> bool,
 Sorted X.lt l -> Sorted X.lt (filter f l)) ->
forall f : elt -> bool,
Sorted X.lt (a :: l) ->
Sorted X.lt
  (if f a then a :: filter f l else filter f l)
  intros x l Hrec f Hs; inv.s:t
x:elt
l:list elt
Hrec:forall f0 : elt -> bool,
Sorted X.lt l -> Sorted X.lt (filter f0 l)
f:elt -> bool
H:Sorted X.lt l
H0:Inf x l
Sorted X.lt
  (if f x then x :: filter f l else filter f l)
  case (f x); auto.s:t
x:elt
l:list elt
Hrec:forall f0 : elt -> bool,
Sorted X.lt l -> Sorted X.lt (filter f0 l)
f:elt -> bool
H:Sorted X.lt l
H0:Inf x l
Sorted X.lt (x :: filter f l)
  constructors; auto.s:t
x:elt
l:list elt
Hrec:forall f0 : elt -> bool,
Sorted X.lt l -> Sorted X.lt (filter f0 l)
f:elt -> bool
H:Sorted X.lt l
H0:Inf x l
Inf x (filter f l)
  apply filter_inf; auto.
  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).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.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; intros.x:elt
f:elt -> bool
H:Proper (X.eq ==> eq) f
In x nil <-> In x nil /\ f x = true
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
  split; intuition; inv.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:F; rewrite !InA_cons, ?IHs; intuition.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
F:f a = true
H1:X.eq x a
f x = true
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
F:f a = false
H2:f x = true
H0:X.eq x a
In x s
  setoid_replace x with a; auto.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
F:f a = false
H2:f x = true
H0:X.eq x a
In x s
  setoid_replace a with x in F; auto; congruence.
  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).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.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; intros.f:elt -> bool
H:Proper (X.eq ==> eq) f
true = true <->
(forall x : X.t, In x nil -> f x = true)
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)
  split; intros; auto.f:elt -> bool
H:Proper (X.eq ==> eq) f
H0:true = true
x:X.t
H1:In x nil
f x = true
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) inv.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.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)
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; auto.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
(forall x : X.t, In x s -> f x = true) <->
(forall x : X.t, In x (a :: s) -> f x = true)
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) firstorder.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
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.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
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.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'.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':false = true
forall x : X.t, In x (a :: s) -> f x = true
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 discriminate.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 H' in F; 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).forall (s : t) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
exists_ f s = true <->
Exists (fun x : elt => f x = true) s
  Proof.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; intros.f:elt -> bool
H:Proper (X.eq ==> eq) f
false = true <->
(exists x : X.t, In x nil /\ f x = true)
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)
  firstorder.f:elt -> bool
H:Proper (X.eq ==> eq) f
H0:false = true
exists x : X.t, In x nil /\ f x = true
f:elt -> bool
H:Proper (X.eq ==> eq) f
x:X.t
H0:In x nil
H1:f x = true
false = true
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) discriminate.f:elt -> bool
H:Proper (X.eq ==> eq) f
x:X.t
H0:In x nil
H1:f x = true
false = true
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) inv.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.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)
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)
  firstorder.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; auto.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 x : X.t, In x s /\ f x = true) <->
(exists x : X.t, In x (a :: s) /\ f x = true)
  firstorder.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.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
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.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_inf1 :
   forall (s : t) (f : elt -> bool) (x : elt) (Hs : Ok s),
   Inf x s -> Inf x (fst (partition f s)).forall (s : t) (f : elt -> bool) (x : elt),
Ok s -> Inf x s -> Inf x (fst (partition f s))
  Proof.forall (s : t) (f : elt -> bool) (x : elt),
Ok s -> Inf x s -> Inf x (fst (partition f s))
  intros s f x; repeat rewrite <- isok_iff; revert s f x.forall (s : t) (f : elt -> bool) (x : elt),
Sorted X.lt s ->
Inf x s -> Inf x (fst (partition f s))
  simple induction s; simpl.s:t
(elt -> bool) ->
forall x : elt,
Sorted X.lt nil -> Inf x nil -> Inf x nil
s:t
forall (a : elt) (l : list elt),
(forall (f : elt -> bool) (x : elt),
 Sorted X.lt l ->
 Inf x l -> Inf x (fst (partition f l))) ->
forall (f : elt -> bool) (x : elt),
Sorted X.lt (a :: l) ->
Inf x (a :: l) ->
Inf x
  (fst
     (let (s1, s2) := partition f l in
      if f a then (a :: s1, s2) else (s1, a :: s2)))
  intuition.s:t
forall (a : elt) (l : list elt),
(forall (f : elt -> bool) (x : elt),
 Sorted X.lt l ->
 Inf x l -> Inf x (fst (partition f l))) ->
forall (f : elt -> bool) (x : elt),
Sorted X.lt (a :: l) ->
Inf x (a :: l) ->
Inf x
  (fst
     (let (s1, s2) := partition f l in
      if f a then (a :: s1, s2) else (s1, a :: s2)))
  intros x l Hrec f a Hs Ha; inv.s:t
x:elt
l:list elt
Hrec:forall (f0 : elt -> bool) (x0 : elt),
Sorted X.lt l ->
Inf x0 l -> Inf x0 (fst (partition f0 l))
f:elt -> bool
a:elt
H:Sorted X.lt l
H0:Inf x l
H1:X.lt a x
Inf a
  (fst
     (let (s1, s2) := partition f l in
      if f x then (x :: s1, s2) else (s1, x :: s2)))
  generalize (Hrec f a H).s:t
x:elt
l:list elt
Hrec:forall (f0 : elt -> bool) (x0 : elt),
Sorted X.lt l ->
Inf x0 l -> Inf x0 (fst (partition f0 l))
f:elt -> bool
a:elt
H:Sorted X.lt l
H0:Inf x l
H1:X.lt a x
(Inf a l -> Inf a (fst (partition f l))) ->
Inf a
  (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.s:t
x:elt
l:list elt
Hrec:forall (f0 : elt -> bool) (x0 : elt),
Sorted X.lt l ->
Inf x0 l -> Inf x0 (fst (partition f0 l))
f:elt -> bool
a:elt
H:Sorted X.lt l
H0:Inf x l
H1:X.lt a x
forall t0 : t,
t -> (Inf a l -> Inf a t0) -> Inf a (x :: t0)
s:t
x:elt
l:list elt
Hrec:forall (f0 : elt -> bool) (x0 : elt),
Sorted X.lt l ->
Inf x0 l -> Inf x0 (fst (partition f0 l))
f:elt -> bool
a:elt
H:Sorted X.lt l
H0:Inf x l
H1:X.lt a x
forall t0 : t, t -> (Inf a l -> Inf a t0) -> Inf a t0
  auto.s:t
x:elt
l:list elt
Hrec:forall (f0 : elt -> bool) (x0 : elt),
Sorted X.lt l ->
Inf x0 l -> Inf x0 (fst (partition f0 l))
f:elt -> bool
a:elt
H:Sorted X.lt l
H0:Inf x l
H1:X.lt a x
forall t0 : t, t -> (Inf a l -> Inf a t0) -> Inf a t0
  intros; apply H2; apply Inf_lt with x; auto.
  Qed.

  Lemma partition_inf2 :
   forall (s : t) (f : elt -> bool) (x : elt) (Hs : Ok s),
   Inf x s -> Inf x (snd (partition f s)).forall (s : t) (f : elt -> bool) (x : elt),
Ok s -> Inf x s -> Inf x (snd (partition f s))
  Proof.forall (s : t) (f : elt -> bool) (x : elt),
Ok s -> Inf x s -> Inf x (snd (partition f s))
  intros s f x; repeat rewrite <- isok_iff; revert s f x.forall (s : t) (f : elt -> bool) (x : elt),
Sorted X.lt s ->
Inf x s -> Inf x (snd (partition f s))
  simple induction s; simpl.s:t
(elt -> bool) ->
forall x : elt,
Sorted X.lt nil -> Inf x nil -> Inf x nil
s:t
forall (a : elt) (l : list elt),
(forall (f : elt -> bool) (x : elt),
 Sorted X.lt l ->
 Inf x l -> Inf x (snd (partition f l))) ->
forall (f : elt -> bool) (x : elt),
Sorted X.lt (a :: l) ->
Inf x (a :: l) ->
Inf x
  (snd
     (let (s1, s2) := partition f l in
      if f a then (a :: s1, s2) else (s1, a :: s2)))
  intuition.s:t
forall (a : elt) (l : list elt),
(forall (f : elt -> bool) (x : elt),
 Sorted X.lt l ->
 Inf x l -> Inf x (snd (partition f l))) ->
forall (f : elt -> bool) (x : elt),
Sorted X.lt (a :: l) ->
Inf x (a :: l) ->
Inf x
  (snd
     (let (s1, s2) := partition f l in
      if f a then (a :: s1, s2) else (s1, a :: s2)))
  intros x l Hrec f a Hs Ha; inv.s:t
x:elt
l:list elt
Hrec:forall (f0 : elt -> bool) (x0 : elt),
Sorted X.lt l ->
Inf x0 l -> Inf x0 (snd (partition f0 l))
f:elt -> bool
a:elt
H:Sorted X.lt l
H0:Inf x l
H1:X.lt a x
Inf a
  (snd
     (let (s1, s2) := partition f l in
      if f x then (x :: s1, s2) else (s1, x :: s2)))
  generalize (Hrec f a H).s:t
x:elt
l:list elt
Hrec:forall (f0 : elt -> bool) (x0 : elt),
Sorted X.lt l ->
Inf x0 l -> Inf x0 (snd (partition f0 l))
f:elt -> bool
a:elt
H:Sorted X.lt l
H0:Inf x l
H1:X.lt a x
(Inf a l -> Inf a (snd (partition f l))) ->
Inf a
  (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.s:t
x:elt
l:list elt
Hrec:forall (f0 : elt -> bool) (x0 : elt),
Sorted X.lt l ->
Inf x0 l -> Inf x0 (snd (partition f0 l))
f:elt -> bool
a:elt
H:Sorted X.lt l
H0:Inf x l
H1:X.lt a x
t -> forall t1 : t, (Inf a l -> Inf a t1) -> Inf a t1
s:t
x:elt
l:list elt
Hrec:forall (f0 : elt -> bool) (x0 : elt),
Sorted X.lt l ->
Inf x0 l -> Inf x0 (snd (partition f0 l))
f:elt -> bool
a:elt
H:Sorted X.lt l
H0:Inf x l
H1:X.lt a x
t ->
forall t1 : t,
(Inf a l -> Inf a t1) -> Inf a (x :: t1)
  intros; apply H2; apply Inf_lt with x; auto.s:t
x:elt
l:list elt
Hrec:forall (f0 : elt -> bool) (x0 : elt),
Sorted X.lt l ->
Inf x0 l -> Inf x0 (snd (partition f0 l))
f:elt -> bool
a:elt
H:Sorted X.lt l
H0:Inf x l
H1:X.lt a x
t ->
forall t1 : t,
(Inf a l -> Inf a t1) -> Inf a (x :: t1)
  auto.
  Qed.

  Instance partition_ok1 s f : forall `(Ok s), Ok (fst (partition f s)).s:t
f:elt -> bool
Ok s -> Ok (fst (partition f s))
  Proof.s:t
f:elt -> bool
Ok s -> Ok (fst (partition f s))
  repeat rewrite <- isok_iff; revert s f.forall (s : t) (f : elt -> bool),
Sorted X.lt s -> Sorted X.lt (fst (partition f s))
  simple induction s; simpl.s:t
(elt -> bool) -> Sorted X.lt nil -> Sorted X.lt nil
s:t
forall (a : elt) (l : list elt),
(forall f : elt -> bool,
 Sorted X.lt l -> Sorted X.lt (fst (partition f l))) ->
forall f : elt -> bool,
Sorted X.lt (a :: l) ->
Sorted X.lt
  (fst
     (let (s1, s2) := partition f l in
      if f a then (a :: s1, s2) else (s1, a :: s2)))
  auto.s:t
forall (a : elt) (l : list elt),
(forall f : elt -> bool,
 Sorted X.lt l -> Sorted X.lt (fst (partition f l))) ->
forall f : elt -> bool,
Sorted X.lt (a :: l) ->
Sorted X.lt
  (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.s:t
x:elt
l:list elt
Hrec:forall f0 : elt -> bool,
Sorted X.lt l ->
Sorted X.lt (fst (partition f0 l))
f:elt -> bool
H:Sorted X.lt l
H0:Inf x l
Sorted X.lt
  (fst
     (let (s1, s2) := partition f l in
      if f x then (x :: s1, s2) else (s1, x :: s2)))
  generalize (Hrec f H); generalize (@partition_inf1 l f x).s:t
x:elt
l:list elt
Hrec:forall f0 : elt -> bool,
Sorted X.lt l ->
Sorted X.lt (fst (partition f0 l))
f:elt -> bool
H:Sorted X.lt l
H0:Inf x l
(Ok l -> Inf x l -> Inf x (fst (partition f l))) ->
Sorted X.lt (fst (partition f l)) ->
Sorted X.lt
  (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; auto.
  Qed.

  Instance partition_ok2 s f : forall `(Ok s), Ok (snd (partition f s)).s:t
f:elt -> bool
Ok s -> Ok (snd (partition f s))
  Proof.s:t
f:elt -> bool
Ok s -> Ok (snd (partition f s))
  repeat rewrite <- isok_iff; revert s f.forall (s : t) (f : elt -> bool),
Sorted X.lt s -> Sorted X.lt (snd (partition f s))
  simple induction s; simpl.s:t
(elt -> bool) -> Sorted X.lt nil -> Sorted X.lt nil
s:t
forall (a : elt) (l : list elt),
(forall f : elt -> bool,
 Sorted X.lt l -> Sorted X.lt (snd (partition f l))) ->
forall f : elt -> bool,
Sorted X.lt (a :: l) ->
Sorted X.lt
  (snd
     (let (s1, s2) := partition f l in
      if f a then (a :: s1, s2) else (s1, a :: s2)))
  auto.s:t
forall (a : elt) (l : list elt),
(forall f : elt -> bool,
 Sorted X.lt l -> Sorted X.lt (snd (partition f l))) ->
forall f : elt -> bool,
Sorted X.lt (a :: l) ->
Sorted X.lt
  (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.s:t
x:elt
l:list elt
Hrec:forall f0 : elt -> bool,
Sorted X.lt l ->
Sorted X.lt (snd (partition f0 l))
f:elt -> bool
H:Sorted X.lt l
H0:Inf x l
Sorted X.lt
  (snd
     (let (s1, s2) := partition f l in
      if f x then (x :: s1, s2) else (s1, x :: s2)))
  generalize (Hrec f H); generalize (@partition_inf2 l f x).s:t
x:elt
l:list elt
Hrec:forall f0 : elt -> bool,
Sorted X.lt l ->
Sorted X.lt (snd (partition f0 l))
f:elt -> bool
H:Sorted X.lt l
H0:Inf x l
(Ok l -> Inf x l -> Inf x (snd (partition f l))) ->
Sorted X.lt (snd (partition f l)) ->
Sorted X.lt
  (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; auto.
  Qed.

  Lemma partition_spec1 :
   forall (s : t) (f : elt -> bool),
   Proper (X.eq==>eq) f -> Equal (fst (partition f s)) (filter f s).forall (s : t) (f : elt -> bool),
Proper (X.eq ==> eq) f ->
Equal (fst (partition f s)) (filter f s)
  Proof.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.s:t
forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
forall a : elt, In a nil <-> In a nil
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)
  split; auto.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.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.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)
  destruct (partition f l) as [s1 s2]; simpl; intros.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; auto.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 (x :: s1) <-> In a (x :: filter f l)
  split; inversion_clear 1; auto.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
H1:In a s1
In a (x :: filter f l)
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
H1:In a (filter f l)
In a (x :: s1)
  constructor 2; rewrite <- H; auto.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
H1:In a (filter f l)
In a (x :: s1)
  constructor 2; rewrite H; auto.
  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).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.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.s:t
forall f : elt -> bool,
Proper (X.eq ==> eq) f ->
forall a : elt, In a nil <-> In a nil
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)
  split; auto.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.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.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)
  destruct (partition f l) as [s1 s2]; simpl; intros.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; auto.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 (x :: s2) <->
In a (x :: filter (fun x0 : elt => negb (f x0)) l)
  split; inversion_clear 1; auto.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
H1:In a s2
In a (x :: filter (fun x0 : elt => negb (f x0)) l)
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
H1:In a (filter (fun x0 : elt => negb (f x0)) l)
In a (x :: s2)
  constructor 2; rewrite <- H; auto.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
H1:In a (filter (fun x0 : elt => negb (f x0)) l)
In a (x :: s2)
  constructor 2; rewrite H; auto.
  Qed.

  End ForNotations.

  Definition In := InA X.eq.
  Instance In_compat : Proper (X.eq==>eq==> iff) In.Proper (X.eq ==> eq ==> iff) In
  Proof.Proper (X.eq ==> eq ==> iff) In repeat red; intros; rewrite H, H0; auto. Qed.

  Module L := MakeListOrdering X.
  Definition eq := L.eq.
  Definition eq_equiv := L.eq_equiv.
  Definition lt l1 l2 :=
    exists l1' l2', Ok l1' /\ Ok l2' /\ eq l1 l1' /\ eq l2 l2' /\ L.lt l1' l2'.

  Instance lt_strorder : StrictOrder lt.StrictOrder lt
  Proof.StrictOrder lt
  split.Irreflexive lt
Transitive lt
  intros s (s1 & s2 & B1 & B2 & E1 & E2 & L).s:list X.t
s1, s2:t
B1:Ok s1
B2:Ok s2
E1:eq s s1
E2:eq s s2
L:L.lt s1 s2
False
Transitive lt
  repeat rewrite <- isok_iff in *.s:list X.t
s1, s2:t
B1:Sorted X.lt s1
B2:Sorted X.lt s2
E1:eq s s1
E2:eq s s2
L:L.lt s1 s2
False
Transitive lt
  assert (eqlistA X.eq s1 s2).s:list X.t
s1, s2:t
B1:Sorted X.lt s1
B2:Sorted X.lt s2
E1:eq s s1
E2:eq s s2
L:L.lt s1 s2
eqlistA X.eq s1 s2
s:list X.t
s1, s2:t
B1:Sorted X.lt s1
B2:Sorted X.lt s2
E1:eq s s1
E2:eq s s2
L:L.lt s1 s2
H:eqlistA X.eq s1 s2
False
Transitive lt
   apply SortA_equivlistA_eqlistA with (ltA:=X.lt); auto using @ok with *.s:list X.t
s1, s2:t
B1:Sorted X.lt s1
B2:Sorted X.lt s2
E1:eq s s1
E2:eq s s2
L:L.lt s1 s2
equivlistA X.eq s1 s2
s:list X.t
s1, s2:t
B1:Sorted X.lt s1
B2:Sorted X.lt s2
E1:eq s s1
E2:eq s s2
L:L.lt s1 s2
H:eqlistA X.eq s1 s2
False
Transitive lt
   transitivity s; auto.s:list X.t
s1, s2:t
B1:Sorted X.lt s1
B2:Sorted X.lt s2
E1:eq s s1
E2:eq s s2
L:L.lt s1 s2
equivlistA X.eq s1 s
s:list X.t
s1, s2:t
B1:Sorted X.lt s1
B2:Sorted X.lt s2
E1:eq s s1
E2:eq s s2
L:L.lt s1 s2
H:eqlistA X.eq s1 s2
False
Transitive lt symmetry; auto.s:list X.t
s1, s2:t
B1:Sorted X.lt s1
B2:Sorted X.lt s2
E1:eq s s1
E2:eq s s2
L:L.lt s1 s2
H:eqlistA X.eq s1 s2
False
Transitive lt
  rewrite H in L.s:list X.t
s1, s2:t
B1:Sorted X.lt s1
B2:Sorted X.lt s2
E1:eq s s1
E2:eq s s2
L:L.lt s2 s2
H:eqlistA X.eq s1 s2
False
Transitive lt
  apply (StrictOrder_Irreflexive s2); auto.Transitive lt
  intros s1 s2 s3 (s1' & s2' & B1 & B2 & E1 & E2 & L12)
                  (s2'' & s3' & B2' & B3 & E2' & E3 & L23).s1, s2, s3:list X.t
s1', s2':t
B1:Ok s1'
B2:Ok s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt s1' s2'
s2'', s3':t
B2':Ok s2''
B3:Ok s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt s2'' s3'
lt s1 s3
  exists s1', s3'.s1, s2, s3:list X.t
s1', s2':t
B1:Ok s1'
B2:Ok s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt s1' s2'
s2'', s3':t
B2':Ok s2''
B3:Ok s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt s2'' s3'
Ok s1' /\
Ok s3' /\ eq s1 s1' /\ eq s3 s3' /\ L.lt s1' s3'
  repeat rewrite <- isok_iff in *.s1, s2, s3:list X.t
s1', s2':t
B1:Sorted X.lt s1'
B2:Sorted X.lt s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt s1' s2'
s2'', s3':t
B2':Sorted X.lt s2''
B3:Sorted X.lt s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt s2'' s3'
Sorted X.lt s1' /\
Sorted X.lt s3' /\
eq s1 s1' /\ eq s3 s3' /\ L.lt s1' s3'
  do 4 (split; trivial).s1, s2, s3:list X.t
s1', s2':t
B1:Sorted X.lt s1'
B2:Sorted X.lt s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt s1' s2'
s2'', s3':t
B2':Sorted X.lt s2''
B3:Sorted X.lt s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt s2'' s3'
L.lt s1' s3'
  assert (eqlistA X.eq s2' s2'').s1, s2, s3:list X.t
s1', s2':t
B1:Sorted X.lt s1'
B2:Sorted X.lt s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt s1' s2'
s2'', s3':t
B2':Sorted X.lt s2''
B3:Sorted X.lt s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt s2'' s3'
eqlistA X.eq s2' s2''
s1, s2, s3:list X.t
s1', s2':t
B1:Sorted X.lt s1'
B2:Sorted X.lt s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt s1' s2'
s2'', s3':t
B2':Sorted X.lt s2''
B3:Sorted X.lt s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt s2'' s3'
H:eqlistA X.eq s2' s2''
L.lt s1' s3'
   apply SortA_equivlistA_eqlistA with (ltA:=X.lt); auto using @ok with *.s1, s2, s3:list X.t
s1', s2':t
B1:Sorted X.lt s1'
B2:Sorted X.lt s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt s1' s2'
s2'', s3':t
B2':Sorted X.lt s2''
B3:Sorted X.lt s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt s2'' s3'
equivlistA X.eq s2' s2''
s1, s2, s3:list X.t
s1', s2':t
B1:Sorted X.lt s1'
B2:Sorted X.lt s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt s1' s2'
s2'', s3':t
B2':Sorted X.lt s2''
B3:Sorted X.lt s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt s2'' s3'
H:eqlistA X.eq s2' s2''
L.lt s1' s3'
   transitivity s2; auto.s1, s2, s3:list X.t
s1', s2':t
B1:Sorted X.lt s1'
B2:Sorted X.lt s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt s1' s2'
s2'', s3':t
B2':Sorted X.lt s2''
B3:Sorted X.lt s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt s2'' s3'
equivlistA X.eq s2' s2
s1, s2, s3:list X.t
s1', s2':t
B1:Sorted X.lt s1'
B2:Sorted X.lt s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt s1' s2'
s2'', s3':t
B2':Sorted X.lt s2''
B3:Sorted X.lt s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt s2'' s3'
H:eqlistA X.eq s2' s2''
L.lt s1' s3' symmetry; auto.s1, s2, s3:list X.t
s1', s2':t
B1:Sorted X.lt s1'
B2:Sorted X.lt s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt s1' s2'
s2'', s3':t
B2':Sorted X.lt s2''
B3:Sorted X.lt s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt s2'' s3'
H:eqlistA X.eq s2' s2''
L.lt s1' s3'
  transitivity s2'; auto.s1, s2, s3:list X.t
s1', s2':t
B1:Sorted X.lt s1'
B2:Sorted X.lt s2'
E1:eq s1 s1'
E2:eq s2 s2'
L12:L.lt s1' s2'
s2'', s3':t
B2':Sorted X.lt s2''
B3:Sorted X.lt s3'
E2':eq s2 s2''
E3:eq s3 s3'
L23:L.lt s2'' s3'
H:eqlistA X.eq s2' s2''
L.lt s2' s3'
  rewrite H; auto.
  Qed.

  Instance lt_compat : Proper (eq==>eq==>iff) lt.Proper (eq ==> eq ==> iff) lt
  Proof.Proper (eq ==> eq ==> iff) lt
  intros s1 s2 E12 s3 s4 E34.s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
lt s1 s3 <-> lt s2 s4 split.s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
lt s1 s3 -> lt s2 s4
s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
lt s2 s4 -> lt s1 s3
  intros (s1' & s3' & B1 & B3 & E1 & E3 & LT).s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
s1', s3':t
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt s1' s3'
lt s2 s4
s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
lt s2 s4 -> lt s1 s3
  exists s1', s3'; do 2 (split; trivial).s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
s1', s3':t
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt s1' s3'
eq s2 s1' /\ eq s4 s3' /\ L.lt s1' s3'
s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
lt s2 s4 -> lt s1 s3
   split.s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
s1', s3':t
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt s1' s3'
eq s2 s1'
s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
s1', s3':t
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt s1' s3'
eq s4 s3' /\ L.lt s1' s3'
s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
lt s2 s4 -> lt s1 s3 transitivity s1; auto.s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
s1', s3':t
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt s1' s3'
eq s2 s1
s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
s1', s3':t
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt s1' s3'
eq s4 s3' /\ L.lt s1' s3'
s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
lt s2 s4 -> lt s1 s3 symmetry; auto.s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
s1', s3':t
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt s1' s3'
eq s4 s3' /\ L.lt s1' s3'
s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
lt s2 s4 -> lt s1 s3
   split; auto.s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
s1', s3':t
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt s1' s3'
eq s4 s3'
s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
lt s2 s4 -> lt s1 s3 transitivity s3; auto.s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
s1', s3':t
B1:Ok s1'
B3:Ok s3'
E1:eq s1 s1'
E3:eq s3 s3'
LT:L.lt s1' s3'
eq s4 s3
s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
lt s2 s4 -> lt s1 s3 symmetry; auto.s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
lt s2 s4 -> lt s1 s3
  intros (s1' & s3' & B1 & B3 & E1 & E3 & LT).s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
s1', s3':t
B1:Ok s1'
B3:Ok s3'
E1:eq s2 s1'
E3:eq s4 s3'
LT:L.lt s1' s3'
lt s1 s3
  exists s1', s3'; do 2 (split; trivial).s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
s1', s3':t
B1:Ok s1'
B3:Ok s3'
E1:eq s2 s1'
E3:eq s4 s3'
LT:L.lt s1' s3'
eq s1 s1' /\ eq s3 s3' /\ L.lt s1' s3'
   split.s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
s1', s3':t
B1:Ok s1'
B3:Ok s3'
E1:eq s2 s1'
E3:eq s4 s3'
LT:L.lt s1' s3'
eq s1 s1'
s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
s1', s3':t
B1:Ok s1'
B3:Ok s3'
E1:eq s2 s1'
E3:eq s4 s3'
LT:L.lt s1' s3'
eq s3 s3' /\ L.lt s1' s3' transitivity s2; auto.s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
s1', s3':t
B1:Ok s1'
B3:Ok s3'
E1:eq s2 s1'
E3:eq s4 s3'
LT:L.lt s1' s3'
eq s3 s3' /\ L.lt s1' s3'
   split; auto.s1, s2:list X.t
E12:eq s1 s2
s3, s4:list X.t
E34:eq s3 s4
s1', s3':t
B1:Ok s1'
B3:Ok s3'
E1:eq s2 s1'
E3:eq s4 s3'
LT:L.lt s1' s3'
eq s3 s3' transitivity s4; auto.
  Qed.

  Lemma compare_spec_aux : forall s s', CompSpec eq L.lt s s' (compare s s').forall s s' : list X.t,
CompSpec eq L.lt s s' (compare s s')
  Proof.forall s s' : list X.t,
CompSpec eq L.lt s s' (compare s s')
  induction s as [|x s IH]; intros [|x' s']; simpl; intuition.x:X.t
s:list X.t
IH:forall s'0 : list X.t,
CompSpec eq L.lt s s'0 (compare s s'0)
x':X.t
s':list X.t
CompSpec eq L.lt (x :: s) (x' :: s')
  match X.compare x x' with
  | Eq => compare s s'
  | Lt => Lt
  | Gt => Gt
  end 
  elim_compare x x'; auto.
  Qed.

  Lemma compare_spec : forall s s', Ok s -> Ok s' ->
   CompSpec eq lt s s' (compare s s').forall s s' : t,
Ok s -> Ok s' -> CompSpec eq lt s s' (compare s s')
  Proof.forall s s' : t,
Ok s -> Ok s' -> CompSpec eq lt s s' (compare s s')
  intros s s' Hs Hs'.s, s':t
Hs:Ok s
Hs':Ok s'
CompSpec eq lt s s' (compare s s')
  destruct (compare_spec_aux s s'); constructor; auto.s, s':t
Hs:Ok s
Hs':Ok s'
H:L.lt s s'
lt s s'
s, s':t
Hs:Ok s
Hs':Ok s'
H:L.lt s' s
lt s' s
  exists s, s'; repeat split; auto using @ok.s, s':t
Hs:Ok s
Hs':Ok s'
H:L.lt s' s
lt s' s
  exists s', s; repeat split; auto using @ok.
  Qed.

End MakeRaw.

Encapsulation

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

Module Make (X: OrderedType) <: S with Module E := X.
 Module Raw := MakeRaw X.
 Include Raw2Sets X Raw.
End Make.

For this specific implementation, eq coincides with Leibniz equality

Require Eqdep_dec.

Module Type OrderedTypeWithLeibniz.
  Include OrderedType.
  Parameter eq_leibniz : forall x y, eq x y -> x = y.
End OrderedTypeWithLeibniz.

Module Type SWithLeibniz.
  Declare Module E : OrderedTypeWithLeibniz.
  Include SetsOn E.
  Parameter eq_leibniz : forall x y, eq x y -> x = y.
End SWithLeibniz.

Module MakeWithLeibniz (X: OrderedTypeWithLeibniz) <: SWithLeibniz with Module E := X.
  Module E := X.
  Module Raw := MakeRaw X.
  Include Raw2SetsOn X Raw.

  Lemma eq_leibniz_list : forall xs ys, eqlistA X.eq xs ys -> xs = ys.forall xs ys : list X.t, eqlistA X.eq xs ys -> xs = ys
  Proof.forall xs ys : list X.t, eqlistA X.eq xs ys -> xs = ys
    induction xs as [|x xs]; intros [|y ys] H; inversion H; [ | ].H:eqlistA X.eq nil nil
nil = nil
x:X.t
xs:list X.t
IHxs:forall ys0 : list X.t,
eqlistA X.eq xs ys0 -> xs = ys0
y:X.t
ys:list X.t
H:eqlistA X.eq (x :: xs) (y :: ys)
x0, x':X.t
l, l':list X.t
H3:X.eq x y
H5:eqlistA X.eq xs ys
H0:x0 = x
H1:l = xs
H2:x' = y
H4:l' = ys
x :: xs = y :: ys
    reflexivity.x:X.t
xs:list X.t
IHxs:forall ys0 : list X.t,
eqlistA X.eq xs ys0 -> xs = ys0
y:X.t
ys:list X.t
H:eqlistA X.eq (x :: xs) (y :: ys)
x0, x':X.t
l, l':list X.t
H3:X.eq x y
H5:eqlistA X.eq xs ys
H0:x0 = x
H1:l = xs
H2:x' = y
H4:l' = ys
x :: xs = y :: ys
    f_equal.x:X.t
xs:list X.t
IHxs:forall ys0 : list X.t,
eqlistA X.eq xs ys0 -> xs = ys0
y:X.t
ys:list X.t
H:eqlistA X.eq (x :: xs) (y :: ys)
x0, x':X.t
l, l':list X.t
H3:X.eq x y
H5:eqlistA X.eq xs ys
H0:x0 = x
H1:l = xs
H2:x' = y
H4:l' = ys
x = y
x:X.t
xs:list X.t
IHxs:forall ys0 : list X.t,
eqlistA X.eq xs ys0 -> xs = ys0
y:X.t
ys:list X.t
H:eqlistA X.eq (x :: xs) (y :: ys)
x0, x':X.t
l, l':list X.t
H3:X.eq x y
H5:eqlistA X.eq xs ys
H0:x0 = x
H1:l = xs
H2:x' = y
H4:l' = ys
xs = ys
    apply X.eq_leibniz; congruence.x:X.t
xs:list X.t
IHxs:forall ys0 : list X.t,
eqlistA X.eq xs ys0 -> xs = ys0
y:X.t
ys:list X.t
H:eqlistA X.eq (x :: xs) (y :: ys)
x0, x':X.t
l, l':list X.t
H3:X.eq x y
H5:eqlistA X.eq xs ys
H0:x0 = x
H1:l = xs
H2:x' = y
H4:l' = ys
xs = ys
    apply IHxs; subst; assumption.
  Qed.

  Lemma eq_leibniz : forall s s', eq s s' -> s = s'.forall s s' : t, eq s s' -> s = s'
  Proof.forall s s' : t, eq s s' -> s = s'
    intros [xs Hxs] [ys Hys] Heq.xs:Raw.t
Hxs:Raw.Ok xs
ys:Raw.t
Hys:Raw.Ok ys
Heq:eq {| this := xs; is_ok := Hxs |} {| this := ys; is_ok := Hys |}
{| this := xs; is_ok := Hxs |} =
{| this := ys; is_ok := Hys |}
    change (equivlistA X.eq xs ys) in Heq.xs:Raw.t
Hxs:Raw.Ok xs
ys:Raw.t
Hys:Raw.Ok ys
Heq:equivlistA X.eq xs ys
{| this := xs; is_ok := Hxs |} =
{| this := ys; is_ok := Hys |}
    assert (H : eqlistA X.eq xs ys).xs:Raw.t
Hxs:Raw.Ok xs
ys:Raw.t
Hys:Raw.Ok ys
Heq:equivlistA X.eq xs ys
eqlistA X.eq xs ys
xs:Raw.t
Hxs:Raw.Ok xs
ys:Raw.t
Hys:Raw.Ok ys
Heq:equivlistA X.eq xs ys
H:eqlistA X.eq xs ys
{| this := xs; is_ok := Hxs |} =
{| this := ys; is_ok := Hys |}
      rewrite <- Raw.isok_iff in Hxs, Hys.xs:Raw.t
Hxs:Sorted X.lt xs
ys:Raw.t
Hys:Sorted X.lt ys
Heq:equivlistA X.eq xs ys
eqlistA X.eq xs ys
xs:Raw.t
Hxs:Raw.Ok xs
ys:Raw.t
Hys:Raw.Ok ys
Heq:equivlistA X.eq xs ys
H:eqlistA X.eq xs ys
{| this := xs; is_ok := Hxs |} =
{| this := ys; is_ok := Hys |}
      apply SortA_equivlistA_eqlistA with X.lt; auto with *.xs:Raw.t
Hxs:Raw.Ok xs
ys:Raw.t
Hys:Raw.Ok ys
Heq:equivlistA X.eq xs ys
H:eqlistA X.eq xs ys
{| this := xs; is_ok := Hxs |} =
{| this := ys; is_ok := Hys |}
    apply eq_leibniz_list in H.xs:Raw.t
Hxs:Raw.Ok xs
ys:Raw.t
Hys:Raw.Ok ys
Heq:equivlistA X.eq xs ys
H:xs = ys
{| this := xs; is_ok := Hxs |} =
{| this := ys; is_ok := Hys |}
    subst ys.xs:Raw.t
Hxs:Raw.Ok xs
Heq:equivlistA X.eq xs xs
Hys:Raw.Ok xs
{| this := xs; is_ok := Hxs |} =
{| this := xs; is_ok := Hys |}
    f_equal.xs:Raw.t
Hxs:Raw.Ok xs
Heq:equivlistA X.eq xs xs
Hys:Raw.Ok xs
Hxs = Hys
    apply Eqdep_dec.eq_proofs_unicity.xs:Raw.t
Hxs:Raw.Ok xs
Heq:equivlistA X.eq xs xs
Hys:Raw.Ok xs
forall x y : bool, x = y \/ x <> y
    intros x y; destruct (bool_dec x y); tauto.
  Qed.

End MakeWithLeibniz.