aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Natural
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/Natural
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/Natural')
-rw-r--r--theories/Numbers/Natural/Abstract/NAxioms.v4
-rw-r--r--theories/Numbers/Natural/BigN/BigN.v9
-rw-r--r--theories/Numbers/Natural/BigN/NMake.v60
-rw-r--r--theories/Numbers/Natural/Peano/NPeano.v29
-rw-r--r--theories/Numbers/Natural/SpecViaZ/NSig.v48
-rw-r--r--theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v62
6 files changed, 153 insertions, 59 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 09438628d..45a2cf3e1 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -32,11 +32,11 @@ End NDivSpecific.
(** We now group everything together. *)
-Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ HasEqBool
+Module Type NAxiomsSig := NAxiomsMiniSig <+ OrderFunctions
<+ NZParity.NZParity <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2
<+ NZGcd.NZGcd <+ NZDiv.NZDiv <+ NZBits.NZBits.
-Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ HasEqBool
+Module Type NAxiomsSig' := NAxiomsMiniSig' <+ OrderFunctions'
<+ NZParity.NZParity <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2
<+ NZGcd.NZGcd' <+ NZDiv.NZDiv' <+ NZBits.NZBits'.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index d2c93bbfd..b06e42ca2 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -62,6 +62,9 @@ Infix "*" := BigN.mul : bigN_scope.
Infix "/" := BigN.div : bigN_scope.
Infix "^" := BigN.pow : bigN_scope.
Infix "?=" := BigN.compare : bigN_scope.
+Infix "=?" := BigN.eqb (at level 70, no associativity) : bigN_scope.
+Infix "<=?" := BigN.leb (at level 70, no associativity) : bigN_scope.
+Infix "<?" := BigN.ltb (at level 70, no associativity) : bigN_scope.
Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope.
Notation "x != y" := (~x==y) (at level 70, no associativity) : bigN_scope.
Infix "<" := BigN.lt : bigN_scope.
@@ -94,7 +97,7 @@ exact BigN.mul_1_l. exact BigN.mul_0_l. exact BigN.mul_comm.
exact BigN.mul_assoc. exact BigN.mul_add_distr_r.
Qed.
-Lemma BigNeqb_correct : forall x y, BigN.eq_bool x y = true -> x==y.
+Lemma BigNeqb_correct : forall x y, (x =? y) = true -> x==y.
Proof. now apply BigN.eqb_eq. Qed.
Lemma BigNpower : power_theory 1 BigN.mul BigN.eq BigN.of_N BigN.pow.
@@ -107,11 +110,11 @@ induction p; simpl; intros; BigN.zify; rewrite ?IHp; auto.
Qed.
Lemma BigNdiv : div_theory BigN.eq BigN.add BigN.mul (@id _)
- (fun a b => if BigN.eq_bool b 0 then (0,a) else BigN.div_eucl a b).
+ (fun a b => if b =? 0 then (0,a) else BigN.div_eucl a b).
Proof.
constructor. unfold id. intros a b.
BigN.zify.
-generalize (Zeq_bool_if [b] 0); destruct (Zeq_bool [b] 0).
+case Z.eqb_spec.
BigN.zify. auto with zarith.
intros NEQ.
generalize (BigN.spec_div_eucl a b).
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 23cfec5e9..aabbf87f2 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -301,20 +301,48 @@ Module Make (W0:CyclicType) <: NType.
intros. subst. apply Zcompare_antisym.
Qed.
- Definition eq_bool (x y : t) : bool :=
+ Definition eqb (x y : t) : bool :=
match compare x y with
| Eq => true
| _ => false
end.
- Theorem spec_eq_bool : forall x y, eq_bool x y = Zeq_bool [x] [y].
+ Theorem spec_eqb x y : eqb x y = Z.eqb [x] [y].
Proof.
- intros. unfold eq_bool, Zeq_bool. rewrite spec_compare; reflexivity.
+ apply 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 : t) := [n] < [m].
Definition le (n m : t) := [n] <= [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 [x] [y].
+ Proof.
+ apply 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 [x] [y].
+ Proof.
+ apply 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 : t) : t := match compare n m with Gt => m | _ => n end.
Definition max (n m : t) : t := match compare n m with Lt => m | _ => n end.
@@ -560,7 +588,7 @@ Module Make (W0:CyclicType) <: NType.
(** * General Division *)
Definition div_eucl (x y : t) : t * t :=
- if eq_bool y zero then (zero,zero) else
+ if eqb y zero then (zero,zero) else
match compare x y with
| Eq => (one, zero)
| Lt => (zero, x)
@@ -572,8 +600,8 @@ Module Make (W0:CyclicType) <: NType.
([q], [r]) = Zdiv_eucl [x] [y].
Proof.
intros x y. unfold div_eucl.
- rewrite spec_eq_bool, spec_compare, spec_0.
- generalize (Zeq_bool_if [y] 0); case Zeq_bool.
+ rewrite spec_eqb, spec_compare, spec_0.
+ case Z.eqb_spec.
intros ->. rewrite spec_0. destruct [x]; auto.
intros H'.
assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith).
@@ -685,7 +713,7 @@ Module Make (W0:CyclicType) <: NType.
(** * General Modulo *)
Definition modulo (x y : t) : t :=
- if eq_bool y zero then zero else
+ if eqb y zero then zero else
match compare x y with
| Eq => zero
| Lt => x
@@ -696,8 +724,8 @@ Module Make (W0:CyclicType) <: NType.
forall x y, [modulo x y] = [x] mod [y].
Proof.
intros x y. unfold modulo.
- rewrite spec_eq_bool, spec_compare, spec_0.
- generalize (Zeq_bool_if [y] 0). case Zeq_bool.
+ rewrite spec_eqb, spec_compare, spec_0.
+ case Z.eqb_spec.
intros ->; rewrite spec_0. destruct [x]; auto.
intro H'.
assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith).
@@ -1157,16 +1185,16 @@ Module Make (W0:CyclicType) <: NType.
Definition log2 : t -> t := Eval red_t in
let log2 := iter_t log2n in
- fun x => if eq_bool x zero then zero else log2 x.
+ fun x => if eqb x zero then zero else log2 x.
Lemma log2_fold :
- log2 = fun x => if eq_bool x zero then zero else iter_t log2n x.
+ log2 = fun x => if eqb x zero then zero else iter_t log2n x.
Proof. red_t; reflexivity. Qed.
Lemma spec_log2_0 : forall x, [x] = 0 -> [log2 x] = 0.
Proof.
intros x H. rewrite log2_fold.
- rewrite spec_eq_bool, H. rewrite spec_0. simpl. exact spec_0.
+ rewrite spec_eqb, H. rewrite spec_0. simpl. exact spec_0.
Qed.
Lemma head0_zdigits : forall n (x : dom_t n),
@@ -1193,8 +1221,8 @@ Module Make (W0:CyclicType) <: NType.
2^[log2 x] <= [x] < 2^([log2 x]+1).
Proof.
intros x H. rewrite log2_fold.
- rewrite spec_eq_bool. rewrite spec_0.
- generalize (Zeq_bool_if [x] 0). destruct Zeq_bool.
+ rewrite spec_eqb. rewrite spec_0.
+ case Z.eqb_spec.
auto with zarith.
clear H.
destr_t x as (n,x). intros H.
@@ -1229,8 +1257,8 @@ Module Make (W0:CyclicType) <: NType.
[log2 x] = Zpos (digits x) - [head0 x] - 1.
Proof.
intros. rewrite log2_fold.
- rewrite spec_eq_bool. rewrite spec_0.
- generalize (Zeq_bool_if [x] 0). destruct Zeq_bool.
+ rewrite spec_eqb. rewrite spec_0.
+ case Z.eqb_spec.
auto with zarith.
intros _. revert H. rewrite digits_fold, head0_fold. destr_t x as (n,x).
rewrite ZnZ.spec_sub_carry.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 0cf9ae441..8a26ec6e3 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -14,6 +14,31 @@ Require Import
(** Functions not already defined *)
+Fixpoint leb n m :=
+ match n, m with
+ | O, _ => true
+ | _, O => false
+ | S n', S m' => leb n' m'
+ end.
+
+Definition ltb n m := leb (S n) m.
+
+Infix "<=?" := leb (at level 70) : nat_scope.
+Infix "<?" := ltb (at level 70) : nat_scope.
+
+Lemma leb_le n m : (n <=? m) = true <-> n <= m.
+Proof.
+ revert m.
+ induction n. split; auto with arith.
+ destruct m; simpl. now split.
+ rewrite IHn. split; auto with arith.
+Qed.
+
+Lemma ltb_lt n m : (n <? m) = true <-> n < m.
+Proof.
+ unfold ltb, lt. apply leb_le.
+Qed.
+
Fixpoint pow n m :=
match m with
| O => 1
@@ -681,6 +706,8 @@ Definition sub := minus.
Definition mul := mult.
Definition lt := lt.
Definition le := le.
+Definition ltb := ltb.
+Definition leb := leb.
Definition min := min.
Definition max := max.
@@ -692,6 +719,8 @@ Definition min_r := min_r.
Definition eqb_eq := beq_nat_true_iff.
Definition compare_spec := nat_compare_spec.
Definition eq_dec := eq_nat_dec.
+Definition leb_le := leb_le.
+Definition ltb_lt := ltb_lt.
Definition Even := Even.
Definition Odd := Odd.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index f186c55b4..662648432 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -8,7 +8,7 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-Require Import ZArith Znumtheory.
+Require Import BinInt.
Open Scope Z_scope.
@@ -35,7 +35,9 @@ Module Type NType.
Definition le n m := [n] <= [m].
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 max : t -> t -> t.
Parameter min : t -> t -> t.
Parameter zero : t.
@@ -67,39 +69,41 @@ Module Type NType.
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_max : forall x y, [max x y] = Zmax [x] [y].
- Parameter spec_min : forall x y, [min x y] = Zmin [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_max : forall x y, [max x y] = Z.max [x] [y].
+ Parameter spec_min : forall x y, [min x y] = Z.min [x] [y].
Parameter spec_0: [zero] = 0.
Parameter spec_1: [one] = 1.
Parameter spec_2: [two] = 2.
Parameter spec_succ: forall n, [succ n] = [n] + 1.
Parameter spec_add: forall x y, [add x y] = [x] + [y].
- Parameter spec_pred: forall x, [pred x] = Zmax 0 ([x] - 1).
- Parameter spec_sub: forall x y, [sub x y] = Zmax 0 ([x] - [y]).
+ Parameter spec_pred: forall x, [pred x] = Z.max 0 ([x] - 1).
+ Parameter spec_sub: forall x y, [sub x y] = Z.max 0 ([x] - [y]).
Parameter spec_mul: forall x y, [mul x y] = [x] * [y].
Parameter spec_square: forall x, [square x] = [x] * [x].
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_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
- 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_gcd: forall a b, [gcd a b] = Z.gcd [a] [b].
+ 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 NType.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 84682820d..878e46fea 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-Require Import ZArith Nnat Ndigits NAxioms NDiv NSig.
+Require Import ZArith OrdersFacts Nnat Ndigits NAxioms NDiv NSig.
(** * The interface [NSig.NType] implies the interface [NAxiomsSig] *)
@@ -15,8 +15,8 @@ Module NTypeIsNAxioms (Import N : NType').
Hint Rewrite
spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub
- spec_div spec_modulo spec_gcd spec_compare spec_eq_bool spec_sqrt
- spec_log2 spec_max spec_min spec_pow_pos spec_pow_N spec_pow
+ spec_div spec_modulo spec_gcd spec_compare spec_eqb spec_ltb spec_leb
+ spec_sqrt spec_log2 spec_max spec_min spec_pow_pos spec_pow_N spec_pow
spec_even spec_odd spec_testbit spec_shiftl spec_shiftr
spec_land spec_lor spec_ldiff spec_lxor spec_div2 spec_of_N
: nsimpl.
@@ -126,36 +126,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 N N N [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.
@@ -474,5 +504,5 @@ Qed.
End NTypeIsNAxioms.
Module NType_NAxioms (N : NType)
- <: NAxiomsSig <: HasCompare N <: HasEqBool N <: HasMinMax N
+ <: NAxiomsSig <: OrderFunctions N <: HasMinMax N
:= N <+ NTypeIsNAxioms.