diff options
Diffstat (limited to 'theories/MSets')
| -rw-r--r-- | theories/MSets/MSetAVL.v | 18 | ||||
| -rw-r--r-- | theories/MSets/MSetPositive.v | 81 |
2 files changed, 13 insertions, 86 deletions
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index e1fc454a..cc023cc3 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -31,7 +31,7 @@ code after extraction. *) -Require Import MSetInterface MSetGenTree ZArith Int. +Require Import MSetInterface MSetGenTree BinInt Int. Set Implicit Arguments. Unset Strict Implicit. @@ -83,11 +83,11 @@ Definition assert_false := create. Definition bal l x r := let hl := height l in let hr := height r in - if gt_le_dec hl (hr+2) then + if (hr+2) <? hl then match l with | Leaf => assert_false l x r | Node _ ll lx lr => - if ge_lt_dec (height ll) (height lr) then + if (height lr) <=? (height ll) then create ll lx (create lr x r) else match lr with @@ -97,11 +97,11 @@ Definition bal l x r := end end else - if gt_le_dec hr (hl+2) then + if (hl+2) <? hr then match r with | Leaf => assert_false l x r | Node _ rl rx rr => - if ge_lt_dec (height rr) (height rl) then + if (height rl) <=? (height rr) then create (create l x rl) rx rr else match rl with @@ -138,8 +138,8 @@ Fixpoint join l : elt -> t -> t := fix join_aux (r:t) : t := match r with | Leaf => add x l | Node rh rl rx rr => - if gt_le_dec lh (rh+2) then bal ll lx (join lr x r) - else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rr + if (rh+2) <? lh then bal ll lx (join lr x r) + else if (lh+2) <? rh then bal (join_aux rl) rx rr else create l x r end end. @@ -419,12 +419,12 @@ Local Open Scope Int_scope. Ltac join_tac := intro l; induction l as [| lh ll _ lx lr Hlr]; [ | intros x r; induction r as [| rh rl Hrl rx rr _]; unfold join; - [ | destruct (gt_le_dec lh (rh+2)) as [GT|LE]; + [ | destruct ((rh+2) <? lh) eqn:LT; [ match goal with |- context b [ bal ?a ?b ?c] => replace (bal a b c) with (bal ll lx (join lr x (Node rh rl rx rr))); [ | auto] end - | destruct (gt_le_dec rh (lh+2)) as [GT'|LE']; + | destruct ((lh+2) <? rh) eqn:LT'; [ match goal with |- context b [ bal ?a ?b ?c] => replace (bal a b c) with (bal (join (Node lh ll lx lr) x rl) rx rr); [ | auto] diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v index 25a8c162..8dd240f4 100644 --- a/theories/MSets/MSetPositive.v +++ b/theories/MSets/MSetPositive.v @@ -16,79 +16,13 @@ Sandrine Blazy (used for building certified compilers). *) -Require Import Bool BinPos Orders MSetInterface. +Require Import Bool BinPos Orders OrdersEx MSetInterface. Set Implicit Arguments. Local Open Scope lazy_bool_scope. Local Open Scope positive_scope. Local Unset Elimination Schemes. -(** Even if [positive] can be seen as an ordered type with respect to the - usual order (see above), we can also use a lexicographic order over bits - (lower bits are considered first). This is more natural when using - [positive] as indexes for sets or maps (see FSetPositive and FMapPositive. *) - -Module PositiveOrderedTypeBits <: UsualOrderedType. - Definition t:=positive. - Include HasUsualEq <+ UsualIsEq. - Definition eqb := Pos.eqb. - Definition eqb_eq := Pos.eqb_eq. - Include HasEqBool2Dec. - - 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_antirefl : forall x : positive, ~ bits_lt x x. - Proof. - induction x; simpl; auto. - Qed. - - Lemma bits_lt_trans : - forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z. - Proof. - induction x; destruct y,z; simpl; eauto; intuition. - Qed. - - Instance lt_compat : Proper (eq==>eq==>iff) lt. - Proof. - intros x x' Hx y y' Hy. rewrite Hx, Hy; intuition. - Qed. - - Instance lt_strorder : StrictOrder lt. - Proof. - split; [ exact bits_lt_antirefl | exact bits_lt_trans ]. - Qed. - - Fixpoint compare x y := - match x, y with - | x~1, y~1 => compare x y - | x~1, _ => Gt - | x~0, y~0 => compare x y - | x~0, _ => Lt - | 1, y~1 => Lt - | 1, 1 => Eq - | 1, y~0 => Gt - end. - - Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). - Proof. - unfold eq, lt. - induction x; destruct y; try constructor; simpl; auto. - destruct (IHx y); subst; auto. - destruct (IHx y); subst; auto. - Qed. - -End PositiveOrderedTypeBits. - Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Module E:=PositiveOrderedTypeBits. @@ -303,12 +237,6 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. | 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 := @@ -316,7 +244,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. | Leaf => None | Node l o r => if o then Some 1 else match choose l with - | None => omap xI (choose r) + | None => option_map xI (choose r) | Some i => Some i~0 end end. @@ -326,7 +254,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. | Leaf => None | Node l o r => match min_elt l with - | None => if o then Some 1 else omap xI (min_elt r) + | None => if o then Some 1 else option_map xI (min_elt r) | Some i => Some i~0 end end. @@ -336,7 +264,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. | Leaf => None | Node l o r => match max_elt r with - | None => if o then Some 1 else omap xO (max_elt l) + | None => if o then Some 1 else option_map xO (max_elt l) | Some i => Some i~1 end end. @@ -967,7 +895,6 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Lemma elements_spec2w: forall s, NoDupA E.eq (elements s). Proof. intro. apply SortA_NoDupA with E.lt; auto with *. - apply E.eq_equiv. apply elements_spec2. Qed. |