aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Integer
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-20 17:18:39 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-20 17:18:39 +0000
commitca96d3477993d102d6cc42166eab52516630d181 (patch)
tree073b17efe149637da819caf527b23cf09f15865d /theories/Numbers/Integer
parentca1848177a50e51bde0736e51f506e06efc81b1d (diff)
Arithemtic: more concerning compare, eqb, leb, ltb
Start of a uniform treatment of compare, eqb, leb, ltb: - We now ensure that they are provided by N,Z,BigZ,BigN,Nat and Pos - Some generic properties are derived in OrdersFacts.BoolOrderFacts In BinPos, more work about sub_mask with nice implications on compare (e.g. simplier proof of lt_trans). In BinNat/BinPos, for uniformity, compare_antisym is now (y ?= x) = CompOpp (x ?=y) instead of the symmetrical result. In BigN / BigZ, eq_bool is now eqb In BinIntDef, gtb and geb are kept for the moment, but a comment advise to rather use ltb and leb. Z.div now uses Z.ltb and Z.leb. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14227 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer')
-rw-r--r--theories/Numbers/Integer/Abstract/ZAxioms.v10
-rw-r--r--theories/Numbers/Integer/BigZ/BigZ.v9
-rw-r--r--theories/Numbers/Integer/BigZ/ZMake.v72
-rw-r--r--theories/Numbers/Integer/SpecViaZ/ZSig.v50
-rw-r--r--theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v64
5 files changed, 133 insertions, 72 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 237ac93ef..a5be98aab 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -111,14 +111,12 @@ Module Type ZQuot' (Z:ZAxiomsMiniSig) := QuotRem' Z <+ QuotRemSpec Z.
(** Let's group everything *)
-Module Type ZAxiomsSig :=
- ZAxiomsMiniSig <+ HasCompare <+ HasEqBool <+ HasAbs <+ HasSgn
- <+ NZParity.NZParity
+Module Type ZAxiomsSig := ZAxiomsMiniSig <+ OrderFunctions
+ <+ HasAbs <+ HasSgn <+ NZParity.NZParity
<+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd
<+ ZDiv <+ ZQuot <+ NZBits.NZBits.
-Module Type ZAxiomsSig' :=
- ZAxiomsMiniSig' <+ HasCompare <+ HasEqBool <+ HasAbs <+ HasSgn
- <+ NZParity.NZParity
+Module Type ZAxiomsSig' := ZAxiomsMiniSig' <+ OrderFunctions'
+ <+ HasAbs <+ HasSgn <+ NZParity.NZParity
<+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd'
<+ ZDiv' <+ ZQuot' <+ NZBits.NZBits'.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 236c56b9f..71d275601 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -56,6 +56,9 @@ Infix "*" := BigZ.mul : bigZ_scope.
Infix "/" := BigZ.div : bigZ_scope.
Infix "^" := BigZ.pow : bigZ_scope.
Infix "?=" := BigZ.compare : bigZ_scope.
+Infix "=?" := BigZ.eqb (at level 70, no associativity) : bigZ_scope.
+Infix "<=?" := BigZ.leb (at level 70, no associativity) : bigZ_scope.
+Infix "<?" := BigZ.ltb (at level 70, no associativity) : bigZ_scope.
Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
Notation "x != y" := (~x==y) (at level 70, no associativity) : bigZ_scope.
Infix "<" := BigZ.lt : bigZ_scope.
@@ -112,7 +115,7 @@ symmetry. apply BigZ.add_opp_r.
exact BigZ.add_opp_diag_r.
Qed.
-Lemma BigZeqb_correct : forall x y, BigZ.eq_bool x y = true -> x==y.
+Lemma BigZeqb_correct : forall x y, (x =? y) = true -> x==y.
Proof. now apply BigZ.eqb_eq. Qed.
Definition BigZ_of_N n := BigZ.of_Z (Z_of_N n).
@@ -127,11 +130,11 @@ induction p; simpl; intros; BigZ.zify; rewrite ?IHp; auto.
Qed.
Lemma BigZdiv : div_theory BigZ.eq BigZ.add BigZ.mul (@id _)
- (fun a b => if BigZ.eq_bool b 0 then (0,a) else BigZ.div_eucl a b).
+ (fun a b => if b =? 0 then (0,a) else BigZ.div_eucl a b).
Proof.
constructor. unfold id. intros a b.
BigZ.zify.
-generalize (Zeq_bool_if [b] 0); destruct (Zeq_bool [b] 0).
+case Z.eqb_spec.
BigZ.zify. auto with zarith.
intros NEQ.
generalize (BigZ.spec_div_eucl a b).
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index da501e9ef..8e53e4d62 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -109,21 +109,49 @@ Module Make (N:NType) <: ZType.
exfalso. omega.
Qed.
- Definition eq_bool x y :=
+ Definition eqb x y :=
match compare x y with
| Eq => true
| _ => false
end.
- Theorem spec_eq_bool:
- forall x y, eq_bool x y = Zeq_bool (to_Z x) (to_Z y).
+ Theorem spec_eqb x y : eqb x y = Z.eqb (to_Z x) (to_Z y).
Proof.
- unfold eq_bool, Zeq_bool; intros; rewrite spec_compare; reflexivity.
+ apply Bool.eq_iff_eq_true.
+ unfold eqb. rewrite Z.eqb_eq, <- Z.compare_eq_iff, spec_compare.
+ split; [now destruct Z.compare | now intros ->].
Qed.
Definition lt n m := to_Z n < to_Z m.
Definition le n m := to_Z n <= to_Z m.
+
+ Definition ltb (x y : t) : bool :=
+ match compare x y with
+ | Lt => true
+ | _ => false
+ end.
+
+ Theorem spec_ltb x y : ltb x y = Z.ltb (to_Z x) (to_Z y).
+ Proof.
+ apply Bool.eq_iff_eq_true.
+ rewrite Z.ltb_lt. unfold Z.lt, ltb. rewrite spec_compare.
+ split; [now destruct Z.compare | now intros ->].
+ Qed.
+
+ Definition leb (x y : t) : bool :=
+ match compare x y with
+ | Gt => false
+ | _ => true
+ end.
+
+ Theorem spec_leb x y : leb x y = Z.leb (to_Z x) (to_Z y).
+ Proof.
+ apply Bool.eq_iff_eq_true.
+ rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare.
+ destruct Z.compare; split; try easy. now destruct 1.
+ Qed.
+
Definition min n m := match compare n m with Gt => m | _ => n end.
Definition max n m := match compare n m with Lt => m | _ => n end.
@@ -372,12 +400,12 @@ Module Make (N:NType) <: ZType.
(Pos q, Pos r)
| Pos nx, Neg ny =>
let (q, r) := N.div_eucl nx ny in
- if N.eq_bool N.zero r
+ if N.eqb N.zero r
then (Neg q, zero)
else (Neg (N.succ q), Neg (N.sub ny r))
| Neg nx, Pos ny =>
let (q, r) := N.div_eucl nx ny in
- if N.eq_bool N.zero r
+ if N.eqb N.zero r
then (Neg q, zero)
else (Neg (N.succ q), Pos (N.sub ny r))
| Neg nx, Neg ny =>
@@ -401,32 +429,32 @@ Module Make (N:NType) <: ZType.
(* Pos Neg *)
generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite N.spec_eq_bool, N.spec_0, Hr;
+ try (injection 1; intros Hr Hq; rewrite N.spec_eqb, N.spec_0, Hr;
simpl; rewrite Hq, N.spec_0; auto).
change (- Zpos py) with (Zneg py).
assert (GT : Zpos py > 0) by (compute; auto).
generalize (Z_div_mod (Zpos px) (Zpos py) GT).
unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r').
intros (EQ,MOD). injection 1. intros Hr' Hq'.
- rewrite N.spec_eq_bool, N.spec_0, Hr'.
+ rewrite N.spec_eqb, N.spec_0, Hr'.
break_nonneg r pr EQr.
subst; simpl. rewrite N.spec_0; auto.
- subst. lazy iota beta delta [Zeq_bool Zcompare].
+ subst. lazy iota beta delta [Z.eqb].
rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *.
(* Neg Pos *)
generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite N.spec_eq_bool, N.spec_0, Hr;
+ try (injection 1; intros Hr Hq; rewrite N.spec_eqb, N.spec_0, Hr;
simpl; rewrite Hq, N.spec_0; auto).
change (- Zpos px) with (Zneg px).
assert (GT : Zpos py > 0) by (compute; auto).
generalize (Z_div_mod (Zpos px) (Zpos py) GT).
unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r').
intros (EQ,MOD). injection 1. intros Hr' Hq'.
- rewrite N.spec_eq_bool, N.spec_0, Hr'.
+ rewrite N.spec_eqb, N.spec_0, Hr'.
break_nonneg r pr EQr.
subst; simpl. rewrite N.spec_0; auto.
- subst. lazy iota beta delta [Zeq_bool Zcompare].
+ subst. lazy iota beta delta [Z.eqb].
rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *.
(* Neg Neg *)
generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
@@ -464,7 +492,7 @@ Module Make (N:NType) <: ZType.
end.
Definition rem x y :=
- if eq_bool y zero then x
+ if eqb y zero then x
else
match x, y with
| Pos nx, Pos ny => Pos (N.modulo nx ny)
@@ -483,8 +511,8 @@ Module Make (N:NType) <: ZType.
Lemma spec_rem : forall x y,
to_Z (rem x y) = Zrem (to_Z x) (to_Z y).
Proof.
- intros x y. unfold rem. rewrite spec_eq_bool, spec_0.
- assert (Hy := Zeq_bool_if (to_Z y) 0). destruct Zeq_bool.
+ intros x y. unfold rem. rewrite spec_eqb, spec_0.
+ case Z.eqb_spec; intros Hy.
now rewrite Hy, Zrem_0_r.
destruct x as [x|x], y as [y|y]; simpl in *; symmetry;
rewrite N.spec_modulo, ?Zrem_opp_r, ?Zrem_opp_l, ?Zopp_involutive;
@@ -551,7 +579,7 @@ Module Make (N:NType) <: ZType.
Definition norm_pos z :=
match z with
| Pos _ => z
- | Neg n => if N.eq_bool n N.zero then Pos n else z
+ | Neg n => if N.eqb n N.zero then Pos n else z
end.
Definition testbit a n :=
@@ -623,19 +651,17 @@ Module Make (N:NType) <: ZType.
Lemma spec_norm_pos : forall x, to_Z (norm_pos x) = to_Z x.
Proof.
intros [x|x]; simpl; trivial.
- rewrite N.spec_eq_bool, N.spec_0.
- assert (H := Zeq_bool_if (N.to_Z x) 0).
- destruct Zeq_bool; simpl; auto with zarith.
+ rewrite N.spec_eqb, N.spec_0.
+ case Z.eqb_spec; simpl; auto with zarith.
Qed.
Lemma spec_norm_pos_pos : forall x y, norm_pos x = Neg y ->
0 < N.to_Z y.
Proof.
intros [x|x] y; simpl; try easy.
- rewrite N.spec_eq_bool, N.spec_0.
- assert (H := Zeq_bool_if (N.to_Z x) 0).
- destruct Zeq_bool; simpl; try easy.
- inversion 1; subst. generalize (N.spec_pos y); auto with zarith.
+ rewrite N.spec_eqb, N.spec_0.
+ case Z.eqb_spec; simpl; try easy.
+ inversion 2. subst. generalize (N.spec_pos y); auto with zarith.
Qed.
Ltac destr_norm_pos x :=
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index 9981fab71..0f2862df7 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -8,7 +8,7 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-Require Import ZArith Znumtheory.
+Require Import BinInt.
Open Scope Z_scope.
@@ -33,7 +33,9 @@ Module Type ZType.
Parameter spec_of_Z: forall x, to_Z (of_Z x) = x.
Parameter compare : t -> t -> comparison.
- Parameter eq_bool : t -> t -> bool.
+ Parameter eqb : t -> t -> bool.
+ Parameter ltb : t -> t -> bool.
+ Parameter leb : t -> t -> bool.
Parameter min : t -> t -> t.
Parameter max : t -> t -> t.
Parameter zero : t.
@@ -71,10 +73,12 @@ Module Type ZType.
Parameter lxor : t -> t -> t.
Parameter div2 : t -> t.
- Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y].
- Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y].
- Parameter spec_min : forall x y, [min x y] = Zmin [x] [y].
- Parameter spec_max : forall x y, [max x y] = Zmax [x] [y].
+ Parameter spec_compare: forall x y, compare x y = ([x] ?= [y]).
+ Parameter spec_eqb : forall x y, eqb x y = ([x] =? [y]).
+ Parameter spec_ltb : forall x y, ltb x y = ([x] <? [y]).
+ Parameter spec_leb : forall x y, leb x y = ([x] <=? [y]).
+ Parameter spec_min : forall x y, [min x y] = Z.min [x] [y].
+ Parameter spec_max : forall x y, [max x y] = Z.max [x] [y].
Parameter spec_0: [zero] = 0.
Parameter spec_1: [one] = 1.
Parameter spec_2: [two] = 2.
@@ -89,27 +93,27 @@ Module Type ZType.
Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n.
Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n.
Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n].
- Parameter spec_sqrt: forall x, [sqrt x] = Zsqrt [x].
- Parameter spec_log2: forall x, [log2 x] = Zlog2 [x].
+ Parameter spec_sqrt: forall x, [sqrt x] = Z.sqrt [x].
+ Parameter spec_log2: forall x, [log2 x] = Z.log2 [x].
Parameter spec_div_eucl: forall x y,
- let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
+ let (q,r) := div_eucl x y in ([q], [r]) = Z.div_eucl [x] [y].
Parameter spec_div: forall x y, [div x y] = [x] / [y].
Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
Parameter spec_quot: forall x y, [quot x y] = [x] รท [y].
- Parameter spec_rem: forall x y, [rem x y] = Zrem [x] [y].
- Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
- Parameter spec_sgn : forall x, [sgn x] = Zsgn [x].
- Parameter spec_abs : forall x, [abs x] = Zabs [x].
- Parameter spec_even : forall x, even x = Zeven_bool [x].
- Parameter spec_odd : forall x, odd x = Zodd_bool [x].
- Parameter spec_testbit: forall x p, testbit x p = Ztestbit [x] [p].
- Parameter spec_shiftr: forall x p, [shiftr x p] = Zshiftr [x] [p].
- Parameter spec_shiftl: forall x p, [shiftl x p] = Zshiftl [x] [p].
- Parameter spec_land: forall x y, [land x y] = Zand [x] [y].
- Parameter spec_lor: forall x y, [lor x y] = Zor [x] [y].
- Parameter spec_ldiff: forall x y, [ldiff x y] = Zdiff [x] [y].
- Parameter spec_lxor: forall x y, [lxor x y] = Zxor [x] [y].
- Parameter spec_div2: forall x, [div2 x] = Zdiv2 [x].
+ Parameter spec_rem: forall x y, [rem x y] = Z.rem [x] [y].
+ Parameter spec_gcd: forall a b, [gcd a b] = Z.gcd [a] [b].
+ Parameter spec_sgn : forall x, [sgn x] = Z.sgn [x].
+ Parameter spec_abs : forall x, [abs x] = Z.abs [x].
+ Parameter spec_even : forall x, even x = Z.even [x].
+ Parameter spec_odd : forall x, odd x = Z.odd [x].
+ Parameter spec_testbit: forall x p, testbit x p = Z.testbit [x] [p].
+ Parameter spec_shiftr: forall x p, [shiftr x p] = Z.shiftr [x] [p].
+ Parameter spec_shiftl: forall x p, [shiftl x p] = Z.shiftl [x] [p].
+ Parameter spec_land: forall x y, [land x y] = Z.land [x] [y].
+ Parameter spec_lor: forall x y, [lor x y] = Z.lor [x] [y].
+ Parameter spec_ldiff: forall x y, [ldiff x y] = Z.ldiff [x] [y].
+ Parameter spec_lxor: forall x y, [lxor x y] = Z.lxor [x] [y].
+ Parameter spec_div2: forall x, [div2 x] = Z.div2 [x].
End ZType.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index a055007f4..e3fc512e7 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-Require Import Bool ZArith Nnat ZAxioms ZSig.
+Require Import Bool ZArith OrdersFacts Nnat ZAxioms ZSig.
(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *)
@@ -15,9 +15,9 @@ Module ZTypeIsZAxioms (Import Z : ZType').
Hint Rewrite
spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt
- spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
- spec_pow spec_log2 spec_even spec_odd spec_gcd spec_quot spec_rem
- spec_testbit spec_shiftl spec_shiftr
+ spec_compare spec_eqb spec_ltb spec_leb spec_max spec_min
+ spec_abs spec_sgn spec_pow spec_log2 spec_even spec_odd spec_gcd
+ spec_quot spec_rem spec_testbit spec_shiftl spec_shiftr
spec_land spec_lor spec_ldiff spec_lxor spec_div2
: zsimpl.
@@ -138,36 +138,66 @@ Qed.
(** Order *)
-Lemma compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y).
+Lemma eqb_eq x y : eqb x y = true <-> x == y.
Proof.
- intros. zify. destruct (Zcompare_spec [x] [y]); auto.
+ zify. apply Z.eqb_eq.
Qed.
-Definition eqb := eq_bool.
+Lemma leb_le x y : leb x y = true <-> x <= y.
+Proof.
+ zify. apply Z.leb_le.
+Qed.
+
+Lemma ltb_lt x y : ltb x y = true <-> x < y.
+Proof.
+ zify. apply Z.ltb_lt.
+Qed.
+
+Lemma compare_eq_iff n m : compare n m = Eq <-> n == m.
+Proof.
+ intros. zify. apply Z.compare_eq_iff.
+Qed.
+
+Lemma compare_lt_iff n m : compare n m = Lt <-> n < m.
+Proof.
+ intros. zify. reflexivity.
+Qed.
+
+Lemma compare_le_iff n m : compare n m <> Gt <-> n <= m.
+Proof.
+ intros. zify. reflexivity.
+Qed.
-Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y.
+Lemma compare_antisym n m : compare m n = CompOpp (compare n m).
Proof.
- intros. zify. symmetry. apply Zeq_is_eq_bool.
+ intros. zify. apply Z.compare_antisym.
Qed.
+Include BoolOrderFacts Z Z Z [no inline].
+
Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare.
Proof.
-intros x x' Hx y y' Hy. rewrite 2 spec_compare, Hx, Hy; intuition.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
Qed.
-Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+Instance eqb_wd : Proper (eq ==> eq ==> Logic.eq) eqb.
Proof.
-intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
Qed.
-Theorem lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
+Instance ltb_wd : Proper (eq ==> eq ==> Logic.eq) ltb.
Proof.
-intros. zify. omega.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
Qed.
-Theorem lt_irrefl : forall n, ~ n < n.
+Instance leb_wd : Proper (eq ==> eq ==> Logic.eq) leb.
Proof.
-intros. zify. omega.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
+Qed.
+
+Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+Proof.
+intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition.
Qed.
Theorem lt_succ_r : forall n m, n < (succ m) <-> n <= m.
@@ -491,5 +521,5 @@ Qed.
End ZTypeIsZAxioms.
Module ZType_ZAxioms (Z : ZType)
- <: ZAxiomsSig <: HasCompare Z <: HasEqBool Z <: HasMinMax Z
+ <: ZAxiomsSig <: OrderFunctions Z <: HasMinMax Z
:= Z <+ ZTypeIsZAxioms.