summaryrefslogtreecommitdiff
path: root/theories/FSets/FSetPositive.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FSetPositive.v')
-rw-r--r--theories/FSets/FSetPositive.v1173
1 files changed, 1173 insertions, 0 deletions
diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v
new file mode 100644
index 00000000..e5d55ac5
--- /dev/null
+++ b/theories/FSets/FSetPositive.v
@@ -0,0 +1,1173 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(** 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).
+*)
+
+Require Import Bool BinPos OrderedType OrderedTypeEx FSetInterface.
+
+Set Implicit Arguments.
+
+Local Open Scope lazy_bool_scope.
+Local Open Scope positive_scope.
+
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+Local Unset Boolean Equality Schemes.
+
+
+Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
+
+ Module E:=PositiveOrderedTypeBits.
+
+ Definition elt := positive.
+
+ Inductive tree :=
+ | Leaf : tree
+ | Node : tree -> bool -> tree -> tree.
+
+ Scheme tree_ind := Induction for tree Sort Prop.
+
+ Definition t := tree.
+
+ Definition empty := 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 : positive) (m : t) : 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 : positive) (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 (b: bool) r :=
+ if b then Node l b r else
+ match l,r with
+ | Leaf,Leaf => Leaf
+ | _,_ => Node l false r end.
+
+ Fixpoint remove (i : positive) (m : t) : 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) :=
+ 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) :=
+ 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) :=
+ 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 :=
+ 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.
+
+ Variables B : Type.
+ Variable f : positive -> 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 : positive) :=
+ 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 : positive -> bool.
+
+ Fixpoint xforall (m : t) (i : positive) :=
+ 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 : positive) :=
+ 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 : positive) :=
+ 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 : positive) :=
+ 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 : positive) (a: list positive) :=
+ 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) :=
+ 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) :=
+ 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) :=
+ 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.
+ 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.
+ symmetry. destruct x.
+ apply mem_Leaf.
+ apply mem_Leaf.
+ reflexivity.
+ 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.
+ setoid_rewrite mem_Leaf. firstorder.
+ 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, Plus.plus_assoc. reflexivity.
+ rewrite <- IHl, <- IHr. rewrite Plus.plus_assoc. reflexivity.
+
+ intros. rewrite <- H. simpl. rewrite Plus.plus_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 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 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 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.
+ setoid_rewrite mem_Leaf. intuition discriminate.
+ 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 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 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.
+ setoid_rewrite mem_Leaf. firstorder.
+ 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 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 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 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 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. elim (empty_1 Hx').
+
+ 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.
+ intros ? ? <- ? ? <-. reflexivity.
+ 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 H. injection H; intros; subst; clear H. apply Hp.
+ reflexivity.
+ intros _ x. revert IHr. case choose.
+ intros p Hp H. injection H; intros; subst; clear H. 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. intros <-. apply IHl. reflexivity.
+ destruct o; simpl.
+ injection H. intros <-. reflexivity.
+ destruct (min_elt r); simpl in *.
+ injection H. intros <-. 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; intros <-.
+ 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. intros <- Hl. clear H.
+ destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
+
+ destruct (min_elt r).
+ injection H. intros <-. clear H.
+ destruct y as [z|z|].
+ apply (IHr p 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. intros <-. apply IHr. reflexivity.
+ destruct o; simpl.
+ injection H. intros <-. reflexivity.
+ destruct (max_elt l); simpl in *.
+ injection H. intros <-. 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; intros <-.
+ 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. intros <- Hl. clear H.
+ destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
+
+ destruct (max_elt l).
+ injection H. intros <-. clear H.
+ destruct y as [z|z|].
+ elim (Hp _ H').
+ apply (IHl p z); trivial.
+ discriminate.
+ discriminate.
+ Qed.
+
+End PositiveSet.