FSetPositive: sets of positive inspired by FMapPositive.

 Contributed by Alexandre Ren, Damien Pous, and Thomas Braibant.

 I've also included a MSets version, hence FSetPositive might become
 soon a mere wrapper for MSetPositive, as for other FSets
 implementations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13287 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 94 deletions

diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index e85cc283e..c81a72f89 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -8,15 +8,14 @@
 
 (** * FMapPositive : an implementation of FMapInterface for [positive] keys. *)
 
-Require Import Bool.
-Require Import ZArith.
-Require Import OrderedType.
-Require Import OrderedTypeEx.
-Require Import FMapInterface.
+Require Import Bool ZArith OrderedType OrderedTypeEx FMapInterface.
 
 Set Implicit Arguments.
 Open Local Scope positive_scope.
 
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
 (** This file is an adaptation to the [FMap] framework of a work by
   Xavier Leroy and Sandrine Blazy (used for building certified compilers).
   Keys are of type [positive], and maps are binary trees: the sequence
@@ -25,95 +24,7 @@ Open Local Scope positive_scope.
   compression is implemented, and that the current file is simple enough to be
   self-contained. *)
 
-(** Even if [positive] can be seen as an ordered type with respect to the
-  usual order (see [OrderedTypeEx]), we use here a lexicographic order
-  over bits, which is more natural here (lower bits are considered first). *)
-
-Module PositiveOrderedTypeBits <: UsualOrderedType.
-  Definition t:=positive.
-  Definition eq:=@eq positive.
-  Definition eq_refl := @refl_equal t.
-  Definition eq_sym := @sym_eq t.
-  Definition eq_trans := @trans_eq t.
-
-  Fixpoint bits_lt (p q:positive) : Prop :=
-   match p, q with
-   | xH, xI _ => True
-   | xH, _ => False
-   | xO p, xO q => bits_lt p q
-   | xO _, _ => True
-   | xI p, xI q => bits_lt p q
-   | xI _, _ => False
-   end.
-
-  Definition lt:=bits_lt.
-
-  Lemma bits_lt_trans : forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z.
-  Proof.
-  induction x.
-  induction y; destruct z; simpl; eauto; intuition.
-  induction y; destruct z; simpl; eauto; intuition.
-  induction y; destruct z; simpl; eauto; intuition.
-  Qed.
-
-  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
-  Proof.
-  exact bits_lt_trans.
-  Qed.
-
-  Lemma bits_lt_antirefl : forall x : positive, ~ bits_lt x x.
-  Proof.
-  induction x; simpl; auto.
-  Qed.
-
-  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
-  Proof.
-  intros; intro.
-  rewrite <- H0 in H; clear H0 y.
-  unfold lt in H.
-  exact (bits_lt_antirefl x H).
-  Qed.
-
-  Definition compare : forall x y : t, Compare lt eq x y.
-  Proof.
-  induction x; destruct y.
-  (* I I *)
-  destruct (IHx y).
-  apply LT; auto.
-  apply EQ; rewrite e; red; auto.
-  apply GT; auto.
-  (* I O *)
-  apply GT; simpl; auto.
-  (* I H *)
-  apply GT; simpl; auto.
-  (* O I *)
-  apply LT; simpl; auto.
-  (* O O *)
-  destruct (IHx y).
-  apply LT; auto.
-  apply EQ; rewrite e; red; auto.
-  apply GT; auto.
-  (* O H *)
-  apply LT; simpl; auto.
-  (* H I *)
-  apply LT; simpl; auto.
-  (* H O *)
-  apply GT; simpl; auto.
-  (* H H *)
-  apply EQ; red; auto.
-  Qed.
-
-  Lemma eq_dec (x y: positive): {x = y} + {x <> y}.
-  Proof.
-  intros. case_eq ((x ?= y) Eq); intros.
-  left. apply Pcompare_Eq_eq; auto.
-  right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
-  right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
-  Qed.
-
-End PositiveOrderedTypeBits.
-
-(** Other positive stuff *)
+(** First, some stuff about [positive] *)
 
 Fixpoint append (i j : positive) : positive :=
     match i with
@@ -166,6 +77,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     | Leaf : tree A
     | Node : tree A -> option A -> tree A -> tree A.
 
+  Scheme tree_ind := Induction for tree Sort Prop.
+
   Definition t := tree.
 
   Section A.