aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2015-03-08 19:27:09 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2015-04-02 11:44:18 +0200
commit47e2247fe47dafe834855dd61e7b14b30c57f70d (patch)
treeefe7c096c10d22ad7b409398e6a2be89a1525e56
parentc356a3b01a428504f66f027802b7b19f0761203e (diff)
ZArith/Int.v: some modernizations
-rw-r--r--theories/MSets/MSetAVL.v18
-rw-r--r--theories/ZArith/Int.v193
2 files changed, 140 insertions, 71 deletions
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index e1fc454ae..cc023cc3f 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/ZArith/Int.v b/theories/ZArith/Int.v
index 99ecd150b..d210792f9 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(** * An light axiomatization of integers (used in FSetAVL). *)
+(** * An light axiomatization of integers (used in MSetAVL). *)
(** We define a signature for an integer datatype based on [Z].
The goal is to allow a switch after extraction to ocaml's
@@ -14,11 +14,11 @@
(typically : when mesuring the height of an AVL tree).
*)
-Require Import ZArith.
+Require Import BinInt.
Delimit Scope Int_scope with I.
Local Open Scope Int_scope.
-(** * a specification of integers *)
+(** * A specification of integers *)
Module Type Int.
@@ -31,19 +31,19 @@ Module Type Int.
Parameter _1 : t.
Parameter _2 : t.
Parameter _3 : t.
- Parameter plus : t -> t -> t.
+ Parameter add : t -> t -> t.
Parameter opp : t -> t.
- Parameter minus : t -> t -> t.
- Parameter mult : t -> t -> t.
+ Parameter sub : t -> t -> t.
+ Parameter mul : t -> t -> t.
Parameter max : t -> t -> t.
Notation "0" := _0 : Int_scope.
Notation "1" := _1 : Int_scope.
Notation "2" := _2 : Int_scope.
Notation "3" := _3 : Int_scope.
- Infix "+" := plus : Int_scope.
- Infix "-" := minus : Int_scope.
- Infix "*" := mult : Int_scope.
+ Infix "+" := add : Int_scope.
+ Infix "-" := sub : Int_scope.
+ Infix "*" := mul : Int_scope.
Notation "- x" := (opp x) : Int_scope.
(** For logical relations, we can rely on their counterparts in Z,
@@ -61,7 +61,17 @@ Module Type Int.
Notation "x < y < z" := (x < y /\ y < z) : Int_scope.
Notation "x < y <= z" := (x < y /\ y <= z) : Int_scope.
- (** Some decidability fonctions (informative). *)
+ (** Informative comparisons. *)
+
+ Axiom eqb : t -> t -> bool.
+ Axiom ltb : t -> t -> bool.
+ Axiom leb : t -> t -> bool.
+
+ Infix "=?" := eqb.
+ Infix "<?" := ltb.
+ Infix "<=?" := leb.
+
+ (** For compatibility, some decidability fonctions (informative). *)
Axiom gt_le_dec : forall x y : t, {x > y} + {x <= y}.
Axiom ge_lt_dec : forall x y : t, {x >= y} + {x < y}.
@@ -83,11 +93,14 @@ Module Type Int.
Axiom i2z_1 : i2z _1 = 1%Z.
Axiom i2z_2 : i2z _2 = 2%Z.
Axiom i2z_3 : i2z _3 = 3%Z.
- Axiom i2z_plus : forall n p, i2z (n + p) = (i2z n + i2z p)%Z.
+ Axiom i2z_add : forall n p, i2z (n + p) = (i2z n + i2z p)%Z.
Axiom i2z_opp : forall n, i2z (-n) = (-i2z n)%Z.
- Axiom i2z_minus : forall n p, i2z (n - p) = (i2z n - i2z p)%Z.
- Axiom i2z_mult : forall n p, i2z (n * p) = (i2z n * i2z p)%Z.
+ Axiom i2z_sub : forall n p, i2z (n - p) = (i2z n - i2z p)%Z.
+ Axiom i2z_mul : forall n p, i2z (n * p) = (i2z n * i2z p)%Z.
Axiom i2z_max : forall n p, i2z (max n p) = Z.max (i2z n) (i2z p).
+ Axiom i2z_eqb : forall n p, eqb n p = Z.eqb (i2z n) (i2z p).
+ Axiom i2z_ltb : forall n p, ltb n p = Z.ltb (i2z n) (i2z p).
+ Axiom i2z_leb : forall n p, leb n p = Z.leb (i2z n) (i2z p).
End Int.
@@ -97,11 +110,42 @@ End Int.
Module MoreInt (Import I:Int).
Local Notation int := I.t.
+ Lemma eqb_eq n p : (n =? p) = true <-> n == p.
+ Proof.
+ now rewrite i2z_eqb, Z.eqb_eq.
+ Qed.
+
+ Lemma eqb_neq n p : (n =? p) = false <-> ~(n == p).
+ Proof.
+ rewrite <- eqb_eq. destruct (n =? p); intuition.
+ Qed.
+
+ Lemma ltb_lt n p : (n <? p) = true <-> n < p.
+ Proof.
+ now rewrite i2z_ltb, Z.ltb_lt.
+ Qed.
+
+ Lemma ltb_nlt n p : (n <? p) = false <-> ~(n < p).
+ Proof.
+ rewrite <- ltb_lt. destruct (n <? p); intuition.
+ Qed.
+
+ Lemma leb_le n p : (n <=? p) = true <-> n <= p.
+ Proof.
+ now rewrite i2z_leb, Z.leb_le.
+ Qed.
+
+ Lemma leb_nle n p : (n <=? p) = false <-> ~(n <= p).
+ Proof.
+ rewrite <- leb_le. destruct (n <=? p); intuition.
+ Qed.
+
(** A magic (but costly) tactic that goes from [int] back to the [Z]
friendly world ... *)
Hint Rewrite ->
- i2z_0 i2z_1 i2z_2 i2z_3 i2z_plus i2z_opp i2z_minus i2z_mult i2z_max : i2z.
+ i2z_0 i2z_1 i2z_2 i2z_3 i2z_add i2z_opp i2z_sub i2z_mul i2z_max
+ i2z_eqb i2z_ltb i2z_leb : i2z.
Ltac i2z := match goal with
| H : ?a = ?b |- _ =>
@@ -149,18 +193,18 @@ Module MoreInt (Import I:Int).
| EI1 : ExprI
| EI2 : ExprI
| EI3 : ExprI
- | EIplus : ExprI -> ExprI -> ExprI
+ | EIadd : ExprI -> ExprI -> ExprI
| EIopp : ExprI -> ExprI
- | EIminus : ExprI -> ExprI -> ExprI
- | EImult : ExprI -> ExprI -> ExprI
+ | EIsub : ExprI -> ExprI -> ExprI
+ | EImul : ExprI -> ExprI -> ExprI
| EImax : ExprI -> ExprI -> ExprI
| EIraw : int -> ExprI.
Inductive ExprZ : Set :=
- | EZplus : ExprZ -> ExprZ -> ExprZ
+ | EZadd : ExprZ -> ExprZ -> ExprZ
| EZopp : ExprZ -> ExprZ
- | EZminus : ExprZ -> ExprZ -> ExprZ
- | EZmult : ExprZ -> ExprZ -> ExprZ
+ | EZsub : ExprZ -> ExprZ -> ExprZ
+ | EZmul : ExprZ -> ExprZ -> ExprZ
| EZmax : ExprZ -> ExprZ -> ExprZ
| EZofI : ExprI -> ExprZ
| EZraw : Z -> ExprZ.
@@ -186,9 +230,9 @@ Module MoreInt (Import I:Int).
| 1 => constr:EI1
| 2 => constr:EI2
| 3 => constr:EI3
- | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIplus ex ey)
- | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIminus ex ey)
- | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImult ex ey)
+ | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIadd ex ey)
+ | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIsub ex ey)
+ | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImul ex ey)
| max ?x ?y => let ex := i2ei x with ey := i2ei y in constr:(EImax ex ey)
| - ?x => let ex := i2ei x in constr:(EIopp ex)
| ?x => constr:(EIraw x)
@@ -198,9 +242,9 @@ Module MoreInt (Import I:Int).
with z2ez trm :=
match constr:trm with
- | (?x + ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZplus ex ey)
- | (?x - ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZminus ex ey)
- | (?x * ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmult ex ey)
+ | (?x + ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZadd ex ey)
+ | (?x - ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZsub ex ey)
+ | (?x * ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmul ex ey)
| (Z.max ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EZmax ex ey)
| (- ?x)%Z => let ex := z2ez x in constr:(EZopp ex)
| i2z ?x => let ex := i2ei x in constr:(EZofI ex)
@@ -232,9 +276,9 @@ Module MoreInt (Import I:Int).
| EI1 => 1
| EI2 => 2
| EI3 => 3
- | EIplus e1 e2 => (ei2i e1)+(ei2i e2)
- | EIminus e1 e2 => (ei2i e1)-(ei2i e2)
- | EImult e1 e2 => (ei2i e1)*(ei2i e2)
+ | EIadd e1 e2 => (ei2i e1)+(ei2i e2)
+ | EIsub e1 e2 => (ei2i e1)-(ei2i e2)
+ | EImul e1 e2 => (ei2i e1)*(ei2i e2)
| EImax e1 e2 => max (ei2i e1) (ei2i e2)
| EIopp e => -(ei2i e)
| EIraw i => i
@@ -244,9 +288,9 @@ Module MoreInt (Import I:Int).
Fixpoint ez2z (e:ExprZ) : Z :=
match e with
- | EZplus e1 e2 => ((ez2z e1)+(ez2z e2))%Z
- | EZminus e1 e2 => ((ez2z e1)-(ez2z e2))%Z
- | EZmult e1 e2 => ((ez2z e1)*(ez2z e2))%Z
+ | EZadd e1 e2 => ((ez2z e1)+(ez2z e2))%Z
+ | EZsub e1 e2 => ((ez2z e1)-(ez2z e2))%Z
+ | EZmul e1 e2 => ((ez2z e1)*(ez2z e2))%Z
| EZmax e1 e2 => Z.max (ez2z e1) (ez2z e2)
| EZopp e => (-(ez2z e))%Z
| EZofI e => i2z (ei2i e)
@@ -278,9 +322,9 @@ Module MoreInt (Import I:Int).
| EI1 => EZraw (1%Z)
| EI2 => EZraw (2%Z)
| EI3 => EZraw (3%Z)
- | EIplus e1 e2 => EZplus (norm_ei e1) (norm_ei e2)
- | EIminus e1 e2 => EZminus (norm_ei e1) (norm_ei e2)
- | EImult e1 e2 => EZmult (norm_ei e1) (norm_ei e2)
+ | EIadd e1 e2 => EZadd (norm_ei e1) (norm_ei e2)
+ | EIsub e1 e2 => EZsub (norm_ei e1) (norm_ei e2)
+ | EImul e1 e2 => EZmul (norm_ei e1) (norm_ei e2)
| EImax e1 e2 => EZmax (norm_ei e1) (norm_ei e2)
| EIopp e => EZopp (norm_ei e)
| EIraw i => EZofI (EIraw i)
@@ -290,9 +334,9 @@ Module MoreInt (Import I:Int).
Fixpoint norm_ez (e:ExprZ) : ExprZ :=
match e with
- | EZplus e1 e2 => EZplus (norm_ez e1) (norm_ez e2)
- | EZminus e1 e2 => EZminus (norm_ez e1) (norm_ez e2)
- | EZmult e1 e2 => EZmult (norm_ez e1) (norm_ez e2)
+ | EZadd e1 e2 => EZadd (norm_ez e1) (norm_ez e2)
+ | EZsub e1 e2 => EZsub (norm_ez e1) (norm_ez e2)
+ | EZmul e1 e2 => EZmul (norm_ez e1) (norm_ez e2)
| EZmax e1 e2 => EZmax (norm_ez e1) (norm_ez e2)
| EZopp e => EZopp (norm_ez e)
| EZofI e => norm_ei e
@@ -316,24 +360,22 @@ Module MoreInt (Import I:Int).
| EPraw p => EPraw p
end.
- Lemma norm_ei_correct : forall e:ExprI, ez2z (norm_ei e) = i2z (ei2i e).
+ Lemma norm_ei_correct (e:ExprI) : ez2z (norm_ei e) = i2z (ei2i e).
Proof.
- induction e; simpl; intros; i2z; auto; try congruence.
+ induction e; simpl; i2z; auto; try congruence.
Qed.
- Lemma norm_ez_correct : forall e:ExprZ, ez2z (norm_ez e) = ez2z e.
+ Lemma norm_ez_correct (e:ExprZ) : ez2z (norm_ez e) = ez2z e.
Proof.
- induction e; simpl; intros; i2z; auto; try congruence; apply norm_ei_correct.
+ induction e; simpl; i2z; auto; try congruence; apply norm_ei_correct.
Qed.
- Lemma norm_ep_correct :
- forall e:ExprP, ep2p (norm_ep e) <-> ep2p e.
+ Lemma norm_ep_correct (e:ExprP) : ep2p (norm_ep e) <-> ep2p e.
Proof.
- induction e; simpl; repeat (rewrite norm_ez_correct); intuition.
+ induction e; simpl; rewrite ?norm_ez_correct; intuition.
Qed.
- Lemma norm_ep_correct2 :
- forall e:ExprP, ep2p (norm_ep e) -> ep2p e.
+ Lemma norm_ep_correct2 (e:ExprP) : ep2p (norm_ep e) -> ep2p e.
Proof.
intros; destruct (norm_ep_correct e); auto.
Qed.
@@ -363,23 +405,50 @@ Module Z_as_Int <: Int.
Definition _1 := 1.
Definition _2 := 2.
Definition _3 := 3.
- Definition plus := Z.add.
+ Definition add := Z.add.
Definition opp := Z.opp.
- Definition minus := Z.sub.
- Definition mult := Z.mul.
+ Definition sub := Z.sub.
+ Definition mul := Z.mul.
Definition max := Z.max.
- Definition gt_le_dec := Z_gt_le_dec.
- Definition ge_lt_dec := Z_ge_lt_dec.
+ Definition eqb := Z.eqb.
+ Definition ltb := Z.ltb.
+ Definition leb := Z.leb.
+
Definition eq_dec := Z.eq_dec.
+ Definition gt_le_dec i j : {i > j} + { i <= j }.
+ Proof.
+ generalize (Z.ltb_spec j i).
+ destruct (j <? i); [left|right]; inversion H; trivial.
+ now apply Z.lt_gt.
+ Defined.
+ Definition ge_lt_dec i j : {i >= j} + { i < j }.
+ Proof.
+ generalize (Z.ltb_spec i j).
+ destruct (i <? j); [right|left]; inversion H; trivial.
+ now apply Z.le_ge.
+ Defined.
+
Definition i2z : t -> Z := fun n => n.
- Lemma i2z_eq : forall n p, i2z n=i2z p -> n = p. Proof. auto. Qed.
- Lemma i2z_0 : i2z _0 = 0. Proof. auto. Qed.
- Lemma i2z_1 : i2z _1 = 1. Proof. auto. Qed.
- Lemma i2z_2 : i2z _2 = 2. Proof. auto. Qed.
- Lemma i2z_3 : i2z _3 = 3. Proof. auto. Qed.
- Lemma i2z_plus n p : i2z (n + p) = i2z n + i2z p. Proof. auto. Qed.
- Lemma i2z_opp n : i2z (- n) = - i2z n. Proof. auto. Qed.
- Lemma i2z_minus n p : i2z (n - p) = i2z n - i2z p. Proof. auto. Qed.
- Lemma i2z_mult n p : i2z (n * p) = i2z n * i2z p. Proof. auto. Qed.
- Lemma i2z_max n p : i2z (max n p) = Z.max (i2z n) (i2z p). Proof. auto. Qed.
+ Lemma i2z_eq n p : i2z n = i2z p -> n = p. Proof. trivial. Qed.
+ Lemma i2z_0 : i2z _0 = 0. Proof. reflexivity. Qed.
+ Lemma i2z_1 : i2z _1 = 1. Proof. reflexivity. Qed.
+ Lemma i2z_2 : i2z _2 = 2. Proof. reflexivity. Qed.
+ Lemma i2z_3 : i2z _3 = 3. Proof. reflexivity. Qed.
+ Lemma i2z_add n p : i2z (n + p) = i2z n + i2z p.
+ Proof. reflexivity. Qed.
+ Lemma i2z_opp n : i2z (- n) = - i2z n.
+ Proof. reflexivity. Qed.
+ Lemma i2z_sub n p : i2z (n - p) = i2z n - i2z p.
+ Proof. reflexivity. Qed.
+ Lemma i2z_mul n p : i2z (n * p) = i2z n * i2z p.
+ Proof. reflexivity. Qed.
+ Lemma i2z_max n p : i2z (max n p) = Z.max (i2z n) (i2z p).
+ Proof. reflexivity. Qed.
+ Lemma i2z_eqb n p : eqb n p = Z.eqb (i2z n) (i2z p).
+ Proof. reflexivity. Qed.
+ Lemma i2z_leb n p : leb n p = Z.leb (i2z n) (i2z p).
+ Proof. reflexivity. Qed.
+ Lemma i2z_ltb n p : ltb n p = Z.ltb (i2z n) (i2z p).
+ Proof. reflexivity. Qed.
+
End Z_as_Int.