summaryrefslogtreecommitdiff
path: root/theories/Numbers
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers')
-rw-r--r--theories/Numbers/AltBinNotations.v69
-rw-r--r--theories/Numbers/BinNums.v14
-rw-r--r--theories/Numbers/Cyclic/Int31/Cyclic31.v20
-rw-r--r--theories/Numbers/Cyclic/Int31/Int31.v10
-rw-r--r--theories/Numbers/DecimalString.v20
-rw-r--r--theories/Numbers/Integer/Abstract/ZBits.v6
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivEucl.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NBits.v6
8 files changed, 110 insertions, 37 deletions
diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v
new file mode 100644
index 00000000..c7e39996
--- /dev/null
+++ b/theories/Numbers/AltBinNotations.v
@@ -0,0 +1,69 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(** * Alternative Binary Numeral Notations *)
+
+(** Faster but less safe parsers and printers of [positive], [N], [Z]. *)
+
+(** By default, literals in types [positive], [N], [Z] are parsed and
+ printed via the [Numeral Notation] command, by conversion from/to
+ the [Decimal.int] representation. When working with numbers with
+ thousands of digits and more, conversion from/to [Decimal.int] can
+ become significantly slow. If that becomes a problem for your
+ development, this file provides some alternative [Numeral
+ Notation] commmands that use [Z] as bridge type. To enable these
+ commands, just be sure to [Require] this file after other files
+ defining numeral notations.
+
+ Note: up to Coq 8.8, literals in types [positive], [N], [Z] were
+ parsed and printed using a native ML library of arbitrary
+ precision integers named bigint.ml. From 8.9, the default is to
+ parse and print using a Coq library converting sequences of
+ digits, hence reducing the amount of ML code to trust. But this
+ method is slower. This file then gives access to the legacy
+ method, trading efficiency against a larger ML trust base relying
+ on bigint.ml. *)
+
+Require Import BinNums.
+
+(** [positive] *)
+
+Definition pos_of_z z :=
+ match z with
+ | Zpos p => Some p
+ | _ => None
+ end.
+
+Definition pos_to_z p := Zpos p.
+
+Numeral Notation positive pos_of_z pos_to_z : positive_scope.
+
+(** [N] *)
+
+Definition n_of_z z :=
+ match z with
+ | Z0 => Some N0
+ | Zpos p => Some (Npos p)
+ | Zneg _ => None
+ end.
+
+Definition n_to_z n :=
+ match n with
+ | N0 => Z0
+ | Npos p => Zpos p
+ end.
+
+Numeral Notation N n_of_z n_to_z : N_scope.
+
+(** [Z] *)
+
+Definition z_of_z (z:Z) := z.
+
+Numeral Notation Z z_of_z z_of_z : Z_scope.
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v
index f8b3d9e1..3ba9d1f5 100644
--- a/theories/Numbers/BinNums.v
+++ b/theories/Numbers/BinNums.v
@@ -12,13 +12,11 @@
Set Implicit Arguments.
-Declare ML Module "z_syntax_plugin".
-
(** [positive] is a datatype representing the strictly positive integers
in a binary way. Starting from 1 (represented by [xH]), one can
add a new least significant digit via [xO] (digit 0) or [xI] (digit 1).
- Numbers in [positive] can also be denoted using a decimal notation;
- e.g. [6%positive] abbreviates [xO (xI xH)] *)
+ Numbers in [positive] will also be denoted using a decimal notation;
+ e.g. [6%positive] will abbreviate [xO (xI xH)] *)
Inductive positive : Set :=
| xI : positive -> positive
@@ -32,8 +30,8 @@ Arguments xI _%positive.
(** [N] is a datatype representing natural numbers in a binary way,
by extending the [positive] datatype with a zero.
- Numbers in [N] can also be denoted using a decimal notation;
- e.g. [6%N] abbreviates [Npos (xO (xI xH))] *)
+ Numbers in [N] will also be denoted using a decimal notation;
+ e.g. [6%N] will abbreviate [Npos (xO (xI xH))] *)
Inductive N : Set :=
| N0 : N
@@ -47,8 +45,8 @@ Arguments Npos _%positive.
An integer is either zero or a strictly positive number
(coded as a [positive]) or a strictly negative number
(whose opposite is stored as a [positive] value).
- Numbers in [Z] can also be denoted using a decimal notation;
- e.g. [(-6)%Z] abbreviates [Zneg (xO (xI xH))] *)
+ Numbers in [Z] will also be denoted using a decimal notation;
+ e.g. [(-6)%Z] will abbreviate [Zneg (xO (xI xH))] *)
Inductive Z : Set :=
| Z0 : Z
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index bd4f0279..4a1f24b9 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -21,9 +21,7 @@ Require Import Znumtheory.
Require Import Zgcd_alt.
Require Import Zpow_facts.
Require Import CyclicAxioms.
-Require Import ROmega.
-
-Declare ML Module "int31_syntax_plugin".
+Require Import Lia.
Local Open Scope nat_scope.
Local Open Scope int31_scope.
@@ -128,7 +126,7 @@ Section Basics.
Lemma nshiftl_S_tail :
forall n x, nshiftl x (S n) = nshiftl (shiftl x) n.
- Proof.
+ Proof.
intros n; elim n; simpl; intros; now f_equal.
Qed.
@@ -1239,7 +1237,7 @@ Section Int31_Specs.
destruct (Z_lt_le_dec (X+Y) wB).
contradict H1; auto using Zmod_small with zarith.
rewrite <- (Z_mod_plus_full (X+Y) (-1) wB).
- rewrite Zmod_small; romega.
+ rewrite Zmod_small; lia.
generalize (Z.compare_eq ((X+Y) mod wB) (X+Y)); intros Heq.
destruct Z.compare; intros;
@@ -1263,7 +1261,7 @@ Section Int31_Specs.
destruct (Z_lt_le_dec (X+Y+1) wB).
contradict H1; auto using Zmod_small with zarith.
rewrite <- (Z_mod_plus_full (X+Y+1) (-1) wB).
- rewrite Zmod_small; romega.
+ rewrite Zmod_small; lia.
generalize (Z.compare_eq ((X+Y+1) mod wB) (X+Y+1)); intros Heq.
destruct Z.compare; intros;
@@ -1301,8 +1299,8 @@ Section Int31_Specs.
unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros.
destruct (Z_lt_le_dec (X-Y) 0).
rewrite <- (Z_mod_plus_full (X-Y) 1 wB).
- rewrite Zmod_small; romega.
- contradict H1; apply Zmod_small; romega.
+ rewrite Zmod_small; lia.
+ contradict H1; apply Zmod_small; lia.
generalize (Z.compare_eq ((X-Y) mod wB) (X-Y)); intros Heq.
destruct Z.compare; intros;
@@ -1320,8 +1318,8 @@ Section Int31_Specs.
unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros.
destruct (Z_lt_le_dec (X-Y-1) 0).
rewrite <- (Z_mod_plus_full (X-Y-1) 1 wB).
- rewrite Zmod_small; romega.
- contradict H1; apply Zmod_small; romega.
+ rewrite Zmod_small; lia.
+ contradict H1; apply Zmod_small; lia.
generalize (Z.compare_eq ((X-Y-1) mod wB) (X-Y-1)); intros Heq.
destruct Z.compare; intros;
@@ -1358,7 +1356,7 @@ Section Int31_Specs.
change [|1|] with 1; change [|0|] with 0.
rewrite <- (Z_mod_plus_full (0-[|x|]) 1 wB).
rewrite Zminus_mod_idemp_l.
- rewrite Zmod_small; generalize (phi_bounded x); romega.
+ rewrite Zmod_small; generalize (phi_bounded x); lia.
Qed.
Lemma spec_pred_c : forall x, [-|sub31c x 1|] = [|x|] - 1.
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 9f8da831..927f430f 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -15,11 +15,15 @@ Require Import Wf_nat.
Require Export ZArith.
Require Export DoubleType.
+Declare ML Module "int31_syntax_plugin".
+
+Local Unset Elimination Schemes.
+
(** * 31-bit integers *)
(** This file contains basic definitions of a 31-bit integer
arithmetic. In fact it is more general than that. The only reason
- for this use of 31 is the underlying mecanism for hardware-efficient
+ for this use of 31 is the underlying mechanism for hardware-efficient
computations by A. Spiwack. Apart from this, a switch to, say,
63-bit integers is now just a matter of replacing every occurrences
of 31 by 63. This is actually made possible by the use of
@@ -48,6 +52,10 @@ Inductive int31 : Type := I31 : digits31 int31.
Register digits as int31 bits in "coq_int31" by True.
Register int31 as int31 type in "coq_int31" by True.
+Scheme int31_ind := Induction for int31 Sort Prop.
+Scheme int31_rec := Induction for int31 Sort Set.
+Scheme int31_rect := Induction for int31 Sort Type.
+
Delimit Scope int31_scope with int31.
Bind Scope int31_scope with int31.
Local Open Scope int31_scope.
diff --git a/theories/Numbers/DecimalString.v b/theories/Numbers/DecimalString.v
index 1a3220f6..591024ba 100644
--- a/theories/Numbers/DecimalString.v
+++ b/theories/Numbers/DecimalString.v
@@ -94,7 +94,7 @@ Definition int_of_string s :=
match s with
| EmptyString => Some (Pos Nil)
| String a s' =>
- if ascii_dec a "-" then option_map Neg (uint_of_string s')
+ if Ascii.eqb a "-" then option_map Neg (uint_of_string s')
else option_map Pos (uint_of_string s)
end.
@@ -131,8 +131,8 @@ Proof.
- unfold int_of_string.
destruct (string_of_uint d) eqn:Hd.
+ now destruct d.
- + destruct ascii_dec; subst.
- * now destruct d.
+ + case Ascii.eqb_spec.
+ * intros ->. now destruct d.
* rewrite <- Hd, usu; auto.
- rewrite usu; auto.
Qed.
@@ -141,8 +141,8 @@ Lemma sis s d :
int_of_string s = Some d -> string_of_int d = s.
Proof.
destruct s; [intros [= <-]| ]; simpl; trivial.
- destruct ascii_dec; subst; simpl.
- - destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-].
+ case Ascii.eqb_spec.
+ - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-].
simpl; f_equal. now apply sus.
- destruct d; [ | now destruct uint_of_char].
simpl string_of_int.
@@ -178,7 +178,7 @@ Definition int_of_string s :=
match s with
| EmptyString => None
| String a s' =>
- if ascii_dec a "-" then option_map Neg (uint_of_string s')
+ if Ascii.eqb a "-" then option_map Neg (uint_of_string s')
else option_map Pos (uint_of_string s)
end.
@@ -228,8 +228,8 @@ Proof.
unfold int_of_string.
destruct (string_of_uint d) eqn:Hd.
+ now destruct d.
- + destruct ascii_dec; subst.
- * now destruct d.
+ + case Ascii.eqb_spec.
+ * intros ->. now destruct d.
* rewrite <- Hd, usu; auto. now intros ->.
- intros _ H.
rewrite usu; auto. now intros ->.
@@ -253,8 +253,8 @@ Lemma sis s d :
int_of_string s = Some d -> string_of_int d = s.
Proof.
destruct s; [intros [=]| ]; simpl.
- destruct ascii_dec; subst; simpl.
- - destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-].
+ case Ascii.eqb_spec.
+ - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-].
simpl; f_equal. now apply sus.
- destruct d; [ | now destruct uint_of_char].
simpl string_of_int.
diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v
index 2da44528..4aabda77 100644
--- a/theories/Numbers/Integer/Abstract/ZBits.v
+++ b/theories/Numbers/Integer/Abstract/ZBits.v
@@ -80,7 +80,7 @@ Proof.
now apply testbit_even_succ.
Qed.
-(** Alternative caracterisations of [testbit] *)
+(** Alternative characterisations of [testbit] *)
(** This concise equation could have been taken as specification
for testbit in the interface, but it would have been hard to
@@ -102,10 +102,10 @@ Proof.
left. destruct b; split; simpl; order'.
Qed.
-(** This caracterisation that uses only basic operations and
+(** This characterisation that uses only basic operations and
power was initially taken as specification for testbit.
We describe [a] as having a low part and a high part, with
- the corresponding bit in the middle. This caracterisation
+ the corresponding bit in the middle. This characterisation
is moderatly complex to implement, but also moderately
usable... *)
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index d7f25a66..5a7bd9ab 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -13,7 +13,7 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv.
(** * Euclidean Division for integers, Euclid convention
We use here the "usual" formulation of the Euclid Theorem
- [forall a b, b<>0 -> exists b q, a = b*q+r /\ 0 < r < |b| ]
+ [forall a b, b<>0 -> exists r q, a = b*q+r /\ 0 <= r < |b| ]
The outcome of the modulo function is hence always positive.
This corresponds to convention "E" in the following paper:
diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v
index e1391f59..90663de3 100644
--- a/theories/Numbers/Natural/Abstract/NBits.v
+++ b/theories/Numbers/Natural/Abstract/NBits.v
@@ -78,7 +78,7 @@ Proof.
apply testbit_even_succ, le_0_l.
Qed.
-(** Alternative caracterisations of [testbit] *)
+(** Alternative characterisations of [testbit] *)
(** This concise equation could have been taken as specification
for testbit in the interface, but it would have been hard to
@@ -99,10 +99,10 @@ Proof.
destruct b; order'.
Qed.
-(** This caracterisation that uses only basic operations and
+(** This characterisation that uses only basic operations and
power was initially taken as specification for testbit.
We describe [a] as having a low part and a high part, with
- the corresponding bit in the middle. This caracterisation
+ the corresponding bit in the middle. This characterisation
is moderatly complex to implement, but also moderately
usable... *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 11:28:14 +0000