diff options
Diffstat (limited to 'theories/Numbers/Natural')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAxioms.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 9 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 60 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 29 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSig.v | 48 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 62 |
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. |