File: FSetPositive.v

package info (click to toggle)
rocq-stdlib 9.0.0-3
links: PTS, VCS
area: main
in suites: experimental
size: 11,828 kB
sloc: python: 2,928; sh: 444; makefile: 319; javascript: 24; ml: 2
file content (1197 lines) | stat: -rw-r--r-- 38,480 bytes
(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \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)         *)
(************************************************************************)

(** Efficient implementation of [FSetInterface.S] for positive keys,
    inspired from the [FMapPositive] module.

   This module was adapted by Alexandre Ren, Damien Pous, and Thomas
   Braibant (2010, LIG, CNRS, UMR 5217), from the [FMapPositive]
   module of Pierre Letouzey and Jean-Christophe Filliâtre, which in
   turn comes from the [FMap] framework of a work by Xavier Leroy and
   Sandrine Blazy (used for building certified compilers).
*)

From Stdlib Require Import Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface.

Set Implicit Arguments.
Local Open Scope lazy_bool_scope.
Local Open Scope positive_scope.
Local Unset Elimination Schemes.

Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.

  Module E:=PositiveOrderedTypeBits.

  Definition elt := positive : Type.

  Inductive tree :=
    | Leaf : tree
    | Node : tree -> bool -> tree -> tree.

  Scheme tree_ind := Induction for tree Sort Prop.

  Definition t := tree : Type.

  Definition empty : t := Leaf.

  Fixpoint is_empty (m : t) : bool :=
   match m with
    | Leaf => true
    | Node l b r => negb b &&& is_empty l &&& is_empty r
   end.

  Fixpoint mem (i : elt) (m : t) {struct m} : bool :=
    match m with
    | Leaf => false
    | Node l o r =>
        match i with
        | 1 => o
        | i~0 => mem i l
        | i~1 => mem i r
        end
    end.

  Fixpoint add (i : elt) (m : t) : t :=
    match m with
    | Leaf =>
        match i with
        | 1 => Node Leaf true Leaf
        | i~0 => Node (add i Leaf) false Leaf
        | i~1 => Node Leaf false (add i Leaf)
        end
    | Node l o r =>
        match i with
        | 1 => Node l true r
        | i~0 => Node (add i l) o r
        | i~1 => Node l o (add i r)
        end
    end.

  Definition singleton i := add i empty.

  (** helper function to avoid creating empty trees that are not leaves *)

  Definition node (l : t) (b: bool) (r : t) : t :=
    if b then Node l b r else
     match l,r with
       | Leaf,Leaf => Leaf
       | _,_ => Node l false r end.

  Fixpoint remove (i : elt) (m : t) {struct m} : t :=
    match m with
      | Leaf => Leaf
      | Node l o r =>
        match i with
          | 1 => node l false r
          | i~0 => node (remove i l) o r
          | i~1 => node l o (remove i r)
        end
    end.

  Fixpoint union (m m': t) : t :=
    match m with
      | Leaf => m'
      | Node l o r =>
        match m' with
          | Leaf => m
          | Node l' o' r' => Node (union l l') (o||o') (union r r')
        end
    end.

  Fixpoint inter (m m': t) : t :=
    match m with
      | Leaf => Leaf
      | Node l o r =>
        match m' with
          | Leaf => Leaf
          | Node l' o' r' => node (inter l l') (o&&o') (inter r r')
        end
    end.

  Fixpoint diff (m m': t) : t :=
    match m with
      | Leaf => Leaf
      | Node l o r =>
        match m' with
          | Leaf => m
          | Node l' o' r' => node (diff l l') (o&&negb o') (diff r r')
        end
    end.

  Fixpoint equal (m m': t): bool :=
    match m with
      | Leaf => is_empty m'
      | Node l o r =>
        match m' with
          | Leaf => is_empty m
          | Node l' o' r' => eqb o o' &&& equal l l' &&& equal r r'
        end
    end.

  Fixpoint subset (m m': t): bool :=
    match m with
      | Leaf => true
      | Node l o r =>
        match m' with
          | Leaf => is_empty m
          | Node l' o' r' => (negb o ||| o') &&& subset l l' &&& subset r r'
        end
    end.

  (** reverses [y] and concatenate it with [x] *)

  Fixpoint rev_append (y x : elt) : elt :=
    match y with
      | 1 => x
      | y~1 => rev_append y x~1
      | y~0 => rev_append y x~0
    end.
  Infix "@" := rev_append (at level 60).
  Definition rev x := x@1.

  Section Fold.

    Variable B : Type.
    Variable f : elt -> B -> B.

    (** the additional argument, [i], records the current path, in
       reverse order (this should be more efficient: we reverse this argument
       only at present nodes only, rather than at each node of the tree).
       we also use this convention in all functions below
     *)

    Fixpoint xfold (m : t) (v : B) (i : elt) :=
      match m with
        | Leaf => v
        | Node l true r =>
          xfold r (f (rev i) (xfold l v i~0)) i~1
        | Node l false r =>
          xfold r (xfold l v i~0) i~1
      end.
    Definition fold m i := xfold m i 1.

  End Fold.

  Section Quantifiers.

    Variable f : elt -> bool.

    Fixpoint xforall (m : t) (i : elt) :=
      match m with
        | Leaf => true
        | Node l o r =>
          (negb o ||| f (rev i)) &&& xforall r i~1 &&& xforall l i~0
      end.
    Definition for_all m := xforall m 1.

    Fixpoint xexists (m : t) (i : elt) :=
      match m with
        | Leaf => false
        | Node l o r => (o &&& f (rev i)) ||| xexists r i~1 ||| xexists l i~0
      end.
    Definition exists_ m := xexists m 1.

    Fixpoint xfilter (m : t) (i : elt) : t :=
      match m with
        | Leaf => Leaf
        | Node l o r => node (xfilter l i~0) (o &&& f (rev i)) (xfilter r i~1)
      end.
    Definition filter m := xfilter m 1.

    Fixpoint xpartition (m : t) (i : elt) : t * t :=
      match m with
        | Leaf => (Leaf,Leaf)
        | Node l o r =>
          let (lt,lf) := xpartition l i~0 in
          let (rt,rf) := xpartition r i~1 in
             if o then
               let fi := f (rev i) in
                 (node lt fi rt, node lf (negb fi) rf)
             else
                 (node lt false rt, node lf false rf)
      end.
    Definition partition m := xpartition m 1.

  End Quantifiers.

  (** uses [a] to accumulate values rather than doing a lot of concatenations *)

  Fixpoint xelements (m : t) (i : elt) (a: list elt) :=
    match m with
      | Leaf => a
      | Node l false r => xelements l i~0 (xelements r i~1 a)
      | Node l true r => xelements l i~0 (rev i :: xelements r i~1 a)
    end.

  Definition elements (m : t) := xelements m 1 nil.

  Fixpoint cardinal (m : t) : nat :=
    match m with
      | Leaf => O
      | Node l false r => (cardinal l + cardinal r)%nat
      | Node l true r => S (cardinal l + cardinal r)
    end.

  Definition omap (f: elt -> elt) x :=
    match x with
      | None => None
      | Some i => Some (f i)
    end.

  (** would it be more efficient to use a path like in the above functions ? *)

  Fixpoint choose (m: t) : option elt :=
    match m with
      | Leaf => None
      | Node l o r => if o then Some 1 else
        match choose l with
          | None => omap xI (choose r)
          | Some i => Some i~0
        end
    end.

  Fixpoint min_elt (m: t) : option elt :=
    match m with
      | Leaf => None
      | Node l o r =>
        match min_elt l with
          | None => if o then Some 1 else omap xI (min_elt r)
          | Some i => Some i~0
        end
    end.

  Fixpoint max_elt (m: t) : option elt :=
    match m with
      | Leaf => None
      | Node l o r =>
        match max_elt r with
          | None => if o then Some 1 else omap xO (max_elt l)
          | Some i => Some i~1
        end
    end.

  (** lexicographic product, defined using a notation to keep things lazy *)

  Notation lex u v := match u with Eq => v | Lt => Lt | Gt => Gt end.

  Definition compare_bool a b :=
    match a,b with
      | false, true => Lt
      | true, false => Gt
      | _,_ => Eq
    end.

  Fixpoint compare_fun (m m': t): comparison :=
    match m,m' with
      | Leaf,_ => if is_empty m' then Eq else Lt
      | _,Leaf => if is_empty m then Eq else Gt
      | Node l o r,Node l' o' r' =>
        lex (compare_bool o o') (lex (compare_fun l l') (compare_fun r r'))
    end.


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

  Notation "s  [=]  t" := (Equal s t) (at level 70, no associativity).
  Notation "s  [<=]  t" := (Subset s t) (at level 70, no associativity).

  Definition eq := Equal.

  Declare Equivalent Keys Equal eq.

  Definition lt m m' := compare_fun m m' = Lt.

  (** Specification of [In] *)

  Lemma In_1: forall s x y, E.eq x y -> In x s -> In y s.
  Proof. intros s x y ->. trivial. Qed.

  (** Specification of [eq] *)

  Lemma eq_refl: forall s, eq s s.
  Proof. unfold eq, Equal. reflexivity. Qed.

  Lemma eq_sym: forall s s', eq s s' -> eq s' s.
  Proof. unfold eq, Equal. intros. symmetry. trivial. Qed.

  Lemma eq_trans: forall s s' s'', eq s s' -> eq s' s'' -> eq s s''.
  Proof. unfold eq, Equal. intros ? ? ? H ? ?. rewrite H. trivial. Qed.

  (** Specification of [mem] *)

  Lemma mem_1: forall s x, In x s -> mem x s = true.
  Proof. unfold In. trivial. Qed.

  Lemma mem_2: forall s x, mem x s = true -> In x s.
  Proof. unfold In. trivial. Qed.

  (** Additional lemmas for mem  *)

  Lemma mem_Leaf: forall x, mem x Leaf = false.
  Proof. destruct x; trivial. Qed.

  (** Specification of [empty] *)

  Lemma empty_1 : Empty empty.
  Proof. unfold Empty, In. intro. rewrite mem_Leaf. discriminate. Qed.

  (** Specification of node  *)

  Lemma mem_node: forall x l o r, mem x (node l o r) = mem x (Node l o r).
  Proof.
    intros x l o r.
    case o; trivial.
    destruct l; trivial.
    destruct r; trivial.
    now destruct x.
  Qed.
  Local Opaque node.

  (** Specification of [is_empty] *)

  Lemma is_empty_spec: forall s, Empty s <-> is_empty s = true.
  Proof.
    unfold Empty, In.
    induction s as [|l IHl o r IHr]; simpl.
    - now split.
    - rewrite <- 2andb_lazy_alt, 2andb_true_iff, <- IHl, <- IHr. clear IHl IHr.
      destruct o; simpl; split.
      + intro H. elim (H 1). reflexivity.
      + intuition discriminate.
      + intro H. split.
        * split.
          -- reflexivity.
          -- intro a. apply (H a~0).
        * intro a. apply (H a~1).
      + intros H [a|a|]; apply H || intro; discriminate.
  Qed.

  Lemma is_empty_1: forall s, Empty s -> is_empty s = true.
  Proof. intro. rewrite is_empty_spec. trivial. Qed.

  Lemma is_empty_2: forall s, is_empty s = true -> Empty s.
  Proof. intro. rewrite is_empty_spec. trivial. Qed.

  (** Specification of [subset] *)

  Lemma subset_Leaf_s: forall s, Leaf [<=] s.
  Proof. intros s i Hi. elim (empty_1 Hi). Qed.

  Lemma subset_spec: forall s s', s [<=] s' <-> subset s s' = true.
  Proof.
    induction s as [|l IHl o r IHr]; intros [|l' o' r']; simpl.
    - split; intros.
      + reflexivity.
      + apply subset_Leaf_s.

    - split; intros.
      + reflexivity.
      + apply subset_Leaf_s.

    - rewrite <- 2andb_lazy_alt, 2andb_true_iff, <- 2is_empty_spec.
      destruct o; simpl.
      + split.
        * intro H. elim (@empty_1 1). apply H. reflexivity.
        * intuition discriminate.
      + split; intro H.
        * split.
          -- split.
             ++ reflexivity.
             ++ unfold Empty. intros a H1. apply (@empty_1 (a~0)). apply H. assumption.
          -- unfold Empty. intros a H1. apply (@empty_1 (a~1)). apply H. assumption.
        * destruct H as [[_ Hl] Hr].
          intros [i|i|] Hi.
          -- elim (Hr i Hi).
          -- elim (Hl i Hi).
          -- discriminate.

    - rewrite <- 2andb_lazy_alt, 2andb_true_iff, <- IHl, <- IHr. clear.
      destruct o; simpl.
      + split; intro H.
        * split.
          -- split.
             ++ destruct o'; trivial.
                specialize (H 1). unfold In in H. simpl in H. apply H. reflexivity.
             ++ intros i Hi. apply (H i~0). apply Hi.
          -- intros i Hi. apply (H i~1). apply Hi.
        * destruct H as [[Ho' Hl] Hr]. rewrite Ho'.
          intros i Hi. destruct i.
          -- apply (Hr i). assumption.
          -- apply (Hl i). assumption.
          -- assumption.
      + split; intros.
        * split.
          -- split.
             ++ reflexivity.
             ++ intros i Hi. apply (H i~0). apply Hi.
          -- intros i Hi. apply (H i~1). apply Hi.
        * intros i Hi. destruct i; destruct H as [[H Hl] Hr].
          -- apply (Hr i). assumption.
          -- apply (Hl i). assumption.
          -- discriminate Hi.
  Qed.


  Lemma subset_1: forall s s', Subset s s' -> subset s s' = true.
  Proof. intros s s'. apply -> subset_spec; trivial. Qed.

  Lemma subset_2: forall s s', subset s s' = true -> Subset s s'.
  Proof. intros s s'. apply <- subset_spec; trivial. Qed.

  (** Specification of [equal] (via subset) *)

  Lemma equal_subset: forall s s', equal s s' = subset s s' && subset s' s.
  Proof.
    induction s as [|l IHl o r IHr]; intros [|l' o' r']; simpl; trivial.
    - destruct o.
      + reflexivity.
      + rewrite andb_comm. reflexivity.
    - rewrite <- 6andb_lazy_alt. rewrite eq_iff_eq_true.
      rewrite 7andb_true_iff, eqb_true_iff.
      rewrite IHl, IHr, 2andb_true_iff. clear IHl IHr. intuition subst.
      + destruct o'; reflexivity.
      + destruct o'; reflexivity.
      + destruct o; auto. destruct o'; trivial.
  Qed.

  Lemma equal_spec: forall s s', Equal s s' <-> equal s s' = true.
  Proof.
    intros. rewrite equal_subset. rewrite andb_true_iff.
    rewrite <- 2subset_spec. unfold Equal, Subset. firstorder.
  Qed.

  Lemma equal_1: forall s s', Equal s s' -> equal s s' = true.
  Proof. intros s s'. apply -> equal_spec; trivial. Qed.

  Lemma equal_2: forall s s', equal s s' = true -> Equal s s'.
  Proof. intros s s'. apply <- equal_spec; trivial. Qed.

  Lemma eq_dec : forall s s', { eq s s' } + { ~ eq s s' }.
  Proof.
    unfold eq.
    intros. case_eq (equal s s'); intro H.
    - left. apply equal_2, H.
    - right. abstract (intro H'; rewrite (equal_1 H') in H; discriminate).
  Defined.

  (** (Specified) definition of [compare] *)

  Lemma lex_Opp: forall u v u' v', u = CompOpp u' -> v = CompOpp v' ->
    lex u v = CompOpp (lex u' v').
  Proof. intros ? ? u' ? -> ->. case u'; reflexivity. Qed.

  Lemma compare_bool_inv: forall b b',
    compare_bool b b' = CompOpp (compare_bool b' b).
  Proof. intros [|] [|]; reflexivity. Qed.

  Lemma compare_inv: forall s s', compare_fun s s' = CompOpp (compare_fun s' s).
  Proof.
    induction s as [|l IHl o r IHr]; destruct s' as [|l' o' r']; trivial.
    - unfold compare_fun. case is_empty; reflexivity.
    - unfold compare_fun. case is_empty; reflexivity.
    - simpl. rewrite compare_bool_inv.
      case compare_bool; simpl; trivial; apply lex_Opp; auto.
  Qed.

  Lemma lex_Eq: forall u v, lex u v = Eq <-> u=Eq /\ v=Eq.
  Proof. intros u v; destruct u; intuition discriminate. Qed.

  Lemma compare_bool_Eq: forall b1 b2,
    compare_bool b1 b2 = Eq <-> eqb b1 b2 = true.
  Proof. intros [|] [|]; intuition discriminate. Qed.

  Lemma compare_equal: forall s s', compare_fun s s' = Eq <-> equal s s' = true.
  Proof.
    induction s as [|l IHl o r IHr]; destruct s' as [|l' o' r'].
    - simpl. tauto.
    - unfold compare_fun, equal. case is_empty; intuition discriminate.
    - unfold compare_fun, equal. case is_empty; intuition discriminate.
    - simpl. rewrite <- 2andb_lazy_alt, 2andb_true_iff.
      rewrite <- IHl, <- IHr, <- compare_bool_Eq. clear IHl IHr.
      rewrite and_assoc. rewrite <- 2lex_Eq. reflexivity.
  Qed.


  Lemma compare_gt: forall s s', compare_fun s s' = Gt -> lt s' s.
  Proof.
    unfold lt. intros s s'. rewrite compare_inv.
     case compare_fun; trivial; intros; discriminate.
  Qed.

  Lemma compare_eq: forall s s', compare_fun s s' = Eq -> eq s s'.
  Proof.
    unfold eq. intros s s'. rewrite compare_equal, equal_spec. trivial.
  Qed.

  Lemma compare : forall s s' : t, Compare lt eq s s'.
  Proof.
    intros. case_eq (compare_fun s s'); intro H.
    - apply EQ. apply compare_eq, H.
    - apply LT. assumption.
    - apply GT. apply compare_gt, H.
  Defined.

  Section lt_spec.

  Inductive ct: comparison -> comparison -> comparison -> Prop :=
  | ct_xxx: forall x, ct x  x  x
  | ct_xex: forall x, ct x  Eq x
  | ct_exx: forall x, ct Eq x  x
  | ct_glx: forall x, ct Gt Lt x
  | ct_lgx: forall x, ct Lt Gt x.

  Lemma ct_cxe: forall x, ct (CompOpp x) x Eq.
  Proof. destruct x; constructor. Qed.

  Lemma ct_xce: forall x, ct x (CompOpp x) Eq.
  Proof. destruct x; constructor. Qed.

  Lemma ct_lxl: forall x, ct Lt x Lt.
  Proof. destruct x; constructor. Qed.

  Lemma ct_gxg: forall x, ct Gt x Gt.
  Proof. destruct x; constructor. Qed.

  Lemma ct_xll: forall x, ct x Lt Lt.
  Proof. destruct x; constructor. Qed.

  Lemma ct_xgg: forall x, ct x Gt Gt.
  Proof. destruct x; constructor. Qed.

  Local Hint Constructors ct: ct.
  Local Hint Resolve ct_cxe ct_xce ct_lxl ct_xll ct_gxg ct_xgg: ct.
  Ltac ct := trivial with ct.

  Lemma ct_lex: forall u v w u' v' w',
    ct u v w -> ct u' v' w' -> ct (lex u u') (lex v v') (lex w w').
  Proof.
    intros u v w u' v' w' H H'.
    inversion_clear H; inversion_clear H'; ct; destruct w; ct; destruct w'; ct.
  Qed.

  Lemma ct_compare_bool:
    forall a b c, ct (compare_bool a b) (compare_bool b c) (compare_bool a c).
  Proof.
    intros [|] [|] [|]; constructor.
  Qed.

  Lemma compare_x_Leaf: forall s,
    compare_fun s Leaf = if is_empty s then Eq else Gt.
  Proof.
    intros. rewrite compare_inv. simpl. case (is_empty s); reflexivity.
  Qed.

  Lemma compare_empty_x: forall a, is_empty a = true ->
    forall b, compare_fun a b = if is_empty b then Eq else Lt.
  Proof.
    induction a as [|l IHl o r IHr]; trivial.
    destruct o.
    - intro; discriminate.
    - simpl is_empty. rewrite <- andb_lazy_alt, andb_true_iff.
      intros [Hl Hr].
      destruct b as [|l' [|] r']; simpl compare_fun; trivial.
      + rewrite Hl, Hr. trivial.
      + rewrite (IHl Hl), (IHr Hr). simpl.
        case (is_empty l'); case (is_empty r'); trivial.
  Qed.

  Lemma compare_x_empty: forall a, is_empty a = true ->
    forall b, compare_fun b a = if is_empty b then Eq else Gt.
  Proof.
    setoid_rewrite <- compare_x_Leaf.
    intros. rewrite 2(compare_inv b), (compare_empty_x _ H). reflexivity.
  Qed.

  Lemma ct_compare_fun:
    forall a b c, ct (compare_fun a b) (compare_fun b c) (compare_fun a c).
  Proof.
    induction a as [|l IHl o r IHr]; intros s' s''.
    - destruct s' as [|l' o' r']; destruct s'' as [|l'' o'' r'']; ct.
      + rewrite compare_inv. ct.
      + unfold compare_fun at 1. case_eq (is_empty (Node l' o' r')); intro H'.
        * rewrite (compare_empty_x _ H'). ct.
        * unfold compare_fun at 2. case_eq (is_empty (Node l'' o'' r'')); intro H''.
          -- rewrite (compare_x_empty _ H''), H'. ct.
          -- ct.

    - destruct s' as [|l' o' r']; destruct s'' as [|l'' o'' r''].
      + ct.
      + unfold compare_fun at 2. rewrite compare_x_Leaf.
        case_eq (is_empty (Node l o r)); intro H.
        * rewrite (compare_empty_x _ H). ct.
        * case_eq (is_empty (Node l'' o'' r'')); intro H''.
          -- rewrite (compare_x_empty _ H''), H. ct.
          -- ct.

      + rewrite 2 compare_x_Leaf.
        case_eq (is_empty (Node l o r)); intro H.
        * rewrite compare_inv, (compare_x_empty _ H). ct.
        * case_eq (is_empty (Node l' o' r')); intro H'.
          -- rewrite (compare_x_empty _ H'), H. ct.
          -- ct.

      + simpl compare_fun. apply ct_lex.
        * apply ct_compare_bool.
        * apply ct_lex; trivial.
  Qed.

  End lt_spec.

  Lemma lt_trans: forall s s' s'', lt s s' -> lt s' s'' -> lt s s''.
  Proof.
    unfold lt. intros a b c. assert (H := ct_compare_fun a b c).
    inversion_clear H; trivial; intros; discriminate.
  Qed.

  Lemma lt_not_eq: forall s s', lt s s' -> ~ eq s s'.
  Proof.
    unfold lt, eq. intros s s' H H'.
     rewrite equal_spec, <- compare_equal in H'. congruence.
  Qed.

  (** Specification of [add] *)

  Lemma add_spec: forall x y s, In y (add x s) <-> x=y \/ In y s.
  Proof.
    unfold In. induction x; intros [y|y|] [|l o r]; simpl mem;
    try (rewrite IHx; clear IHx); rewrite ?mem_Leaf; intuition congruence.
  Qed.

  Lemma add_1: forall s x y, x = y -> In y (add x s).
  Proof. intros. apply <- add_spec. left. assumption. Qed.

  Lemma add_2: forall s x y, In y s -> In y (add x s).
  Proof. intros. apply <- add_spec. right. assumption. Qed.

  Lemma add_3: forall s x y, x<>y -> In y (add x s) -> In y s.
  Proof.
    intros s x y H. rewrite add_spec. intros [->|?]; trivial. elim H; trivial.
  Qed.

  (** Specification of [remove] *)

  Lemma remove_spec: forall x y s, In y (remove x s) <-> x<>y /\ In y s.
  Proof.
    unfold In.
    induction x; intros [y|y|] [|l o r]; simpl remove; rewrite ?mem_node;
     simpl mem; try (rewrite IHx; clear IHx); rewrite ?mem_Leaf;
     intuition congruence.
  Qed.

  Lemma remove_1: forall s x y, x=y -> ~ In y (remove x s).
  Proof. intros. rewrite remove_spec. tauto. Qed.

  Lemma remove_2: forall s x y, x<>y -> In y s -> In y (remove x s).
  Proof. intros. rewrite remove_spec. split; assumption. Qed.

  Lemma remove_3: forall s x y, In y (remove x s) -> In y s.
  Proof. intros s x y. rewrite remove_spec. tauto. Qed.

  (** Specification of [singleton] *)

  Lemma singleton_1: forall x y, In y (singleton x) -> x=y.
  Proof.
    unfold singleton. intros x y. rewrite add_spec.
    unfold In. rewrite mem_Leaf. intuition discriminate.
  Qed.

  Lemma singleton_2: forall x y, x = y -> In y (singleton x).
  Proof.
    unfold singleton. intros. apply add_1. assumption.
  Qed.

  (** Specification of [union] *)

  Lemma union_spec: forall x s s', In x (union s s') <-> In x s \/ In x s'.
  Proof.
    unfold In.
    induction x; destruct s; destruct s'; simpl union; simpl mem;
      try (rewrite IHx; clear IHx); try intuition congruence.
      apply orb_true_iff.
  Qed.

  Lemma union_1: forall s s' x, In x (union s s') -> In x s \/ In x s'.
  Proof. intros. apply -> union_spec. assumption. Qed.

  Lemma union_2: forall s s' x, In x s -> In x (union s s').
  Proof. intros. apply <- union_spec. left. assumption. Qed.

  Lemma union_3: forall s s' x, In x s' -> In x (union s s').
  Proof. intros. apply <- union_spec. right. assumption. Qed.

  (** Specification of [inter] *)

  Lemma inter_spec: forall x s s', In x (inter s s') <-> In x s /\ In x s'.
  Proof.
    unfold In.
    induction x; destruct s; destruct s'; simpl inter; rewrite ?mem_node;
     simpl mem; try (rewrite IHx; clear IHx); try intuition congruence.
     apply andb_true_iff.
  Qed.

  Lemma inter_1: forall s s' x, In x (inter s s') -> In x s.
  Proof. intros s s' x. rewrite inter_spec. tauto. Qed.

  Lemma inter_2: forall s s' x, In x (inter s s') -> In x s'.
  Proof. intros s s' x. rewrite inter_spec. tauto. Qed.

  Lemma inter_3: forall s s' x, In x s -> In x s' -> In x (inter s s').
  Proof. intros. rewrite inter_spec. split; assumption. Qed.

  (** Specification of [diff] *)

  Lemma diff_spec: forall x s s', In x (diff s s') <-> In x s /\ ~ In x s'.
  Proof.
    unfold In.
    induction x; destruct s; destruct s' as [|l' o' r']; simpl diff;
     rewrite ?mem_node; simpl mem;
      try (rewrite IHx; clear IHx); try intuition congruence.
      rewrite andb_true_iff. destruct o'; intuition discriminate.
  Qed.

  Lemma diff_1: forall s s' x, In x (diff s s') -> In x s.
  Proof. intros s s' x. rewrite diff_spec. tauto. Qed.

  Lemma diff_2: forall s s' x, In x (diff s s') -> ~ In x s'.
  Proof. intros s s' x. rewrite diff_spec. tauto. Qed.

  Lemma diff_3: forall s s' x, In x s -> ~ In x s' -> In x (diff s s').
  Proof. intros. rewrite diff_spec. split; assumption. Qed.

  (** Specification of [fold] *)

  Lemma fold_1: forall s (A : Type) (i : A) (f : elt -> A -> A),
      fold f s i = fold_left (fun a e => f e a) (elements s) i.
  Proof.
    unfold fold, elements. intros s A i f. revert s i.
    set (f' := fun a e => f e a).
    assert (H: forall s i j acc,
      fold_left f' acc (xfold f s i j) =
      fold_left f' (xelements s j acc) i).

    - induction s as [|l IHl o r IHr]; intros; trivial.
      destruct o; simpl xelements; simpl xfold.
      + rewrite IHr, <- IHl. reflexivity.
      + rewrite IHr. apply IHl.

    - intros. exact (H s i 1 nil).
  Qed.

  (** Specification of [cardinal] *)

  Lemma cardinal_1: forall s, cardinal s = length (elements s).
  Proof.
    unfold elements.
    assert (H: forall s j acc,
                (cardinal s + length acc)%nat = length (xelements s j acc)).

    - induction s as [|l IHl b r IHr]; intros j acc; simpl; trivial. destruct b.
      + rewrite <- IHl. simpl. rewrite <- IHr.
        rewrite <- plus_n_Sm, Nat.add_assoc. reflexivity.
      + rewrite <- IHl, <- IHr. rewrite Nat.add_assoc. reflexivity.

    - intros. rewrite <- H. simpl. rewrite Nat.add_comm. reflexivity.
  Qed.

  (** Specification of [filter] *)

  Lemma xfilter_spec: forall f s x i,
    In x (xfilter f s i) <-> In x s /\ f (i@x) = true.
  Proof.
    intro f. unfold In.
    induction s as [|l IHl o r IHr]; intros x i; simpl xfilter.
    - rewrite mem_Leaf. intuition discriminate.
    - rewrite mem_node. destruct x; simpl.
      + rewrite IHr. reflexivity.
      + rewrite IHl. reflexivity.
      + rewrite <- andb_lazy_alt. apply andb_true_iff.
  Qed.

  Lemma filter_1 : forall s x f, @compat_bool elt E.eq f ->
    In x (filter f s) -> In x s.
  Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed.

  Lemma filter_2 : forall s x f, @compat_bool elt E.eq f ->
    In x (filter f s) -> f x = true.
  Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed.

  Lemma filter_3 : forall s x f, @compat_bool elt E.eq f -> In x s ->
    f x = true -> In x (filter f s).
  Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed.


  (** Specification of [for_all] *)

  Lemma xforall_spec: forall f s i,
    xforall f s i = true <-> For_all (fun x => f (i@x) = true) s.
  Proof.
    unfold For_all, In. intro f.
    induction s as [|l IHl o r IHr]; intros i; simpl.
    - now split.
    - rewrite <- 2andb_lazy_alt, <- orb_lazy_alt, 2 andb_true_iff.
      rewrite IHl, IHr. clear IHl IHr.
      split.
      + intros [[Hi Hr] Hl] x. destruct x; simpl; intro H.
        * apply Hr, H.
        * apply Hl, H.
        * rewrite H in Hi. assumption.
      + intro H; intuition.
        * specialize (H 1). destruct o.
          -- apply H. reflexivity.
          -- reflexivity.
        * apply H. assumption.
        * apply H. assumption.
  Qed.

  Lemma for_all_1 : forall s f, @compat_bool elt E.eq f ->
    For_all (fun x => f x = true) s -> for_all f s = true.
  Proof. intros s f _. unfold for_all. rewrite xforall_spec. trivial. Qed.

  Lemma for_all_2 : forall s f, @compat_bool elt E.eq f ->
    for_all f s = true -> For_all (fun x => f x = true) s.
  Proof. intros s f _. unfold for_all. rewrite xforall_spec. trivial. Qed.


  (** Specification of [exists] *)

  Lemma xexists_spec: forall f s i,
    xexists f s i = true <-> Exists (fun x => f (i@x) = true) s.
  Proof.
    unfold Exists, In. intro f.
    induction s as [|l IHl o r IHr]; intros i; simpl.
    - split; [ discriminate | now intros  [ _ [? _]]].
    - rewrite <- 2orb_lazy_alt, 2orb_true_iff, <- andb_lazy_alt, andb_true_iff.
      rewrite IHl, IHr. clear IHl IHr.
      split.
      + intros [[Hi|[x Hr]]|[x Hl]].
        * exists 1. exact Hi.
        * exists x~1. exact Hr.
        * exists x~0. exact Hl.
      + intros [[x|x|] H]; eauto.
  Qed.

  Lemma exists_1 : forall s f, @compat_bool elt E.eq f ->
      Exists (fun x => f x = true) s -> exists_ f s = true.
  Proof. intros s f _. unfold exists_. rewrite xexists_spec. trivial. Qed.

  Lemma exists_2 : forall s f, @compat_bool elt E.eq f ->
      exists_ f s = true -> Exists (fun x => f x = true) s.
  Proof. intros s f _. unfold exists_. rewrite xexists_spec. trivial. Qed.


  (** Specification of [partition] *)

  Lemma partition_filter : forall s f,
    partition f s = (filter f s, filter (fun x => negb (f x)) s).
  Proof.
    unfold partition, filter. intros s f. generalize 1 as j.
    induction s as [|l IHl o r IHr]; intro j.
    - reflexivity.
    - destruct o; simpl; rewrite IHl, IHr; reflexivity.
  Qed.

  Lemma partition_1 : forall s f, @compat_bool elt E.eq f ->
      Equal (fst (partition f s)) (filter f s).
  Proof. intros. rewrite partition_filter. apply eq_refl. Qed.

  Lemma partition_2 : forall s f, @compat_bool elt E.eq f ->
      Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
  Proof. intros. rewrite partition_filter. apply eq_refl. Qed.


  (** Specification of [elements] *)

  Notation InL := (InA E.eq).

  Lemma xelements_spec: forall s j acc y,
    InL y (xelements s j acc)
    <->
    InL y acc \/ exists x, y=(j@x) /\ mem x s = true.
  Proof.
    induction s as [|l IHl o r IHr]; simpl.
    - intros. split; intro H.
      + left. assumption.
      + destruct H as [H|[x [Hx Hx']]].
        * assumption.
        * discriminate.

    - intros j acc y. case o.
      + rewrite IHl. rewrite InA_cons. rewrite IHr. clear IHl IHr. split.
        * intros [[H|[H|[x [-> H]]]]|[x [-> H]]]; eauto.
          -- right. exists x~1. auto.
          -- right. exists x~0. auto.
        * intros [H|[x [-> H]]].
          -- eauto.
          -- destruct x.
             ++ left. right. right. exists x; auto.
             ++ right. exists x; auto.
             ++ left. left. reflexivity.

      + rewrite IHl, IHr. clear IHl IHr. split.
        * intros [[H|[x [-> H]]]|[x [-> H]]].
          -- eauto.
          -- right. exists x~1. auto.
          -- right. exists x~0. auto.
        * intros [H|[x [-> H]]].
          -- eauto.
          -- destruct x.
             ++ left. right.  exists x; auto.
             ++ right. exists x; auto.
             ++ discriminate.
  Qed.

  Lemma elements_1: forall s x, In x s -> InL x (elements s).
  Proof.
    unfold elements, In. intros.
    rewrite xelements_spec. right. exists x. auto.
  Qed.

  Lemma elements_2: forall s x, InL x (elements s) -> In x s.
  Proof.
    unfold elements, In. intros s x H.
    rewrite xelements_spec in H. destruct H as [H|[y [H H']]].
    - inversion_clear H.
    - rewrite H. assumption.
  Qed.

  Lemma lt_rev_append: forall j x y, E.lt x y -> E.lt (j@x) (j@y).
  Proof. induction j; intros; simpl; auto. Qed.

  Lemma elements_3: forall s, sort E.lt (elements s).
  Proof.
    unfold elements.
    assert (H: forall s j acc,
      sort E.lt acc ->
      (forall x y, In x s ->  InL y acc -> E.lt (j@x) y) ->
      sort E.lt (xelements s j acc)). {

    induction s as [|l IHl o r IHr]; simpl; trivial.
    intros j acc Hacc Hsacc. destruct o.
    - apply IHl.
      + constructor.
        * apply IHr.
          -- apply Hacc.
          -- intros x y Hx Hy. apply Hsacc; assumption.
        * case_eq (xelements r j~1 acc).
          -- constructor.
          -- intros z q H. constructor.
             assert (H': InL z (xelements r j~1 acc)). {
               rewrite H. constructor. reflexivity.
             }
             clear H q. rewrite xelements_spec in H'. destruct H' as [Hy|[x [-> Hx]]].
             ++ apply (Hsacc 1 z); trivial. reflexivity.
             ++ simpl. apply lt_rev_append. exact I.
      + intros x y Hx Hy. inversion_clear Hy.
        * rewrite H. simpl. apply lt_rev_append. exact I.
        * rewrite xelements_spec in H. destruct H as [Hy|[z [-> Hy]]].
          -- apply Hsacc; assumption.
          -- simpl. apply lt_rev_append. exact I.

    - apply IHl.
      + apply IHr.
        * apply Hacc.
        * intros x y Hx Hy. apply Hsacc; assumption.
      + intros x y Hx Hy. rewrite xelements_spec in Hy.
        destruct Hy as [Hy|[z [-> Hy]]].
        * apply Hsacc; assumption.
        * simpl. apply lt_rev_append. exact I.
    }

    intros. apply H.
    - constructor.
    - intros x y _ H'. inversion H'.
  Qed.

  Lemma elements_3w: forall s, NoDupA E.eq (elements s).
  Proof.
    intro. apply SortA_NoDupA with E.lt.
    - constructor.
      + intro. apply E.eq_refl.
      + intro. apply E.eq_sym.
      + intro. apply E.eq_trans.
    - constructor.
      + intros x H. apply E.lt_not_eq in H. apply H. reflexivity.
      + intro. apply E.lt_trans.
    - solve_proper.
    - apply elements_3.
  Qed.


  (** Specification of [choose] *)

  Lemma choose_1: forall s x, choose s = Some x -> In x s.
  Proof.
    induction s as [| l IHl o r IHr]; simpl.
    - intros. discriminate.
    - destruct o.
      + intros x H. injection H; intros; subst. reflexivity.
      + revert IHl. case choose.
        * intros p Hp x [= <-]. apply Hp.
          reflexivity.
        * intros _ x. revert IHr. case choose.
          -- intros p Hp [= <-]. apply Hp.
             reflexivity.
          -- intros. discriminate.
  Qed.

  Lemma choose_2: forall s, choose s = None -> Empty s.
  Proof.
    unfold Empty, In. intros s H.
    induction s as [|l IHl o r IHr].
    - intro. apply empty_1.
    - destruct o.
      + discriminate.
      + simpl in H. destruct (choose l).
        * discriminate.
        * destruct (choose r).
          -- discriminate.
          -- intros [a|a|].
             ++ apply IHr. reflexivity.
             ++ apply IHl. reflexivity.
             ++ discriminate.
  Qed.

  Lemma choose_empty: forall s, is_empty s = true -> choose s = None.
  Proof.
    intros s Hs. case_eq (choose s); trivial.
    intros p Hp. apply choose_1 in Hp. apply is_empty_2 in Hs. elim (Hs _ Hp).
  Qed.

  Lemma choose_3': forall s s', Equal s s' -> choose s = choose s'.
  Proof.
    setoid_rewrite equal_spec.
    induction s as [|l IHl o r IHr].
    - intros. symmetry. apply choose_empty. assumption.

    - destruct s' as [|l' o' r'].
      + generalize (Node l o r) as s. simpl. intros. apply choose_empty.
        rewrite <- equal_spec in H. apply eq_sym in H. rewrite equal_spec in H.
        assumption.

      + simpl. rewrite <- 2andb_lazy_alt, 2andb_true_iff, eqb_true_iff.
        intros [[<- Hl] Hr]. rewrite (IHl _ Hl), (IHr _ Hr). reflexivity.
  Qed.

  Lemma choose_3: forall s s' x y,
    choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y.
  Proof. intros s s' x y Hx Hy H. apply choose_3' in H. congruence. Qed.


  (** Specification of [min_elt] *)

  Lemma min_elt_1: forall s x, min_elt s = Some x -> In x s.
  Proof.
   unfold In.
   induction s as [| l IHl o r IHr]; simpl.
   - intros. discriminate.
   - intros x. destruct (min_elt l); intros.
     + injection H as [= <-]. apply IHl. reflexivity.
     + destruct o; simpl.
       * injection H as [= <-]. reflexivity.
       * destruct (min_elt r); simpl in *.
         -- injection H as [= <-]. apply IHr. reflexivity.
         -- discriminate.
  Qed.

  Lemma min_elt_3: forall s, min_elt s = None -> Empty s.
  Proof.
    unfold Empty, In. intros s H.
    induction s as [|l IHl o r IHr].
    - intro. apply empty_1.
    - intros [a|a|].
      + apply IHr. revert H. clear. simpl. destruct (min_elt r); trivial.
        case min_elt; intros; try discriminate. destruct o; discriminate.
      + apply IHl. revert H. clear. simpl. destruct (min_elt l); trivial.
        intro; discriminate.
      + revert H. clear. simpl. case min_elt; intros; try discriminate.
        destruct o; discriminate.
  Qed.

  Lemma min_elt_2: forall s x y, min_elt s = Some x -> In y s -> ~ E.lt y x.
  Proof.
    unfold In.
    induction s as [|l IHl o r IHr]; intros x y H H'.
    - discriminate.
    - simpl in H. case_eq (min_elt l).
      + intros p Hp. rewrite Hp in H. injection H as [= <-].
        destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial.
      + intro Hp; rewrite Hp in H. apply min_elt_3 in Hp.
        destruct o.
        * injection H as [= <-]. intros Hl.
          destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').

        * destruct (min_elt r).
          -- injection H as [= <-].
             destruct y as [z|z|].
             ++ apply (IHr e z); trivial.
             ++ elim (Hp _ H').
             ++ discriminate.
          -- discriminate.
  Qed.


  (** Specification of [max_elt] *)

  Lemma max_elt_1: forall s x, max_elt s = Some x -> In x s.
  Proof.
   unfold In.
   induction s as [| l IHl o r IHr]; simpl.
   - intros. discriminate.
   - intros x. destruct (max_elt r); intros.
     + injection H as [= <-]. apply IHr. reflexivity.
     + destruct o; simpl.
       * injection H as [= <-]. reflexivity.
       * destruct (max_elt l); simpl in *.
         -- injection H as [= <-]. apply IHl. reflexivity.
         -- discriminate.
  Qed.

  Lemma max_elt_3: forall s, max_elt s = None -> Empty s.
  Proof.
    unfold Empty, In. intros s H.
    induction s as [|l IHl o r IHr].
    - intro. apply empty_1.
    - intros [a|a|].
      + apply IHr. revert H. clear. simpl. destruct (max_elt r); trivial.
        intro; discriminate.
      + apply IHl. revert H. clear. simpl. destruct (max_elt l); trivial.
        case max_elt; intros; try discriminate. destruct o; discriminate.
      + revert H. clear. simpl. case max_elt; intros; try discriminate.
        destruct o; discriminate.
  Qed.

  Lemma max_elt_2: forall s x y, max_elt s = Some x -> In y s -> ~ E.lt x y.
  Proof.
    unfold In.
    induction s as [|l IHl o r IHr]; intros x y H H'.
    - discriminate.
    - simpl in H. case_eq (max_elt r).
      + intros p Hp. rewrite Hp in H. injection H as [= <-].
        destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial.
      + intro Hp; rewrite Hp in H. apply max_elt_3 in Hp.
        destruct o.
        * injection H as [= <-]. intros Hl.
          destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').

        * destruct (max_elt l).
          -- injection H as [= <-].
             destruct y as [z|z|].
             ++ elim (Hp _ H').
             ++ apply (IHl e z); trivial.
             ++ discriminate.
          -- discriminate.
  Qed.

End PositiveSet.