diff options
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/AltBinNotations.v | 69 | ||||
| -rw-r--r-- | theories/Numbers/BinNums.v | 30 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 20 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 48 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/DecimalString.v | 20 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZBits.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivEucl.v | 3 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZDomain.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBits.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NDefOps.v | 2 |
12 files changed, 158 insertions, 62 deletions
diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v new file mode 100644 index 0000000000..c7e3999691 --- /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 f8b3d9e1d9..ef2c688759 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -12,50 +12,64 @@ 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 | xO : positive -> positive | xH : positive. +Declare Scope positive_scope. Delimit Scope positive_scope with positive. Bind Scope positive_scope with positive. Arguments xO _%positive. Arguments xI _%positive. +Register xI as num.pos.xI. +Register xO as num.pos.xO. +Register xH as num.pos.xH. + (** [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 | Npos : positive -> N. +Declare Scope N_scope. Delimit Scope N_scope with N. Bind Scope N_scope with N. Arguments Npos _%positive. +Register N as num.N.type. +Register N0 as num.N.N0. +Register Npos as num.N.Npos. + (** [Z] is a datatype representing the integers in a binary way. 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 | Zpos : positive -> Z | Zneg : positive -> Z. +Declare Scope Z_scope. Delimit Scope Z_scope with Z. Bind Scope Z_scope with Z. Arguments Zpos _%positive. Arguments Zneg _%positive. + +Register Z as num.Z.type. +Register Z0 as num.Z.Z0. +Register Zpos as num.Z.Zpos. +Register Zneg as num.Z.Zneg. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index bd4f0279d4..4a1f24b95e 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 9f8da831d8..ce540775e3 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -15,11 +15,13 @@ Require Import Wf_nat. Require Export ZArith. Require Export DoubleType. +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 @@ -45,9 +47,15 @@ Inductive int31 : Type := I31 : digits31 int31. (* spiwack: Registration of the type of integers, so that the matchs in the functions below perform dynamic decompilation (otherwise some segfault occur when they are applied to one non-closed term and one closed term). *) -Register digits as int31 bits in "coq_int31" by True. -Register int31 as int31 type in "coq_int31" by True. +Register digits as int31.bits. +Register int31 as int31.type. + +Scheme int31_ind := Induction for int31 Sort Prop. +Scheme int31_rec := Induction for int31 Sort Set. +Scheme int31_rect := Induction for int31 Sort Type. +Declare Scope int31_scope. +Declare ML Module "int31_syntax_plugin". Delimit Scope int31_scope with int31. Bind Scope int31_scope with int31. Local Open Scope int31_scope. @@ -343,21 +351,21 @@ Definition lor31 n m := phi_inv (Z.lor (phi n) (phi m)). Definition land31 n m := phi_inv (Z.land (phi n) (phi m)). Definition lxor31 n m := phi_inv (Z.lxor (phi n) (phi m)). -Register add31 as int31 plus in "coq_int31" by True. -Register add31c as int31 plusc in "coq_int31" by True. -Register add31carryc as int31 pluscarryc in "coq_int31" by True. -Register sub31 as int31 minus in "coq_int31" by True. -Register sub31c as int31 minusc in "coq_int31" by True. -Register sub31carryc as int31 minuscarryc in "coq_int31" by True. -Register mul31 as int31 times in "coq_int31" by True. -Register mul31c as int31 timesc in "coq_int31" by True. -Register div3121 as int31 div21 in "coq_int31" by True. -Register div31 as int31 diveucl in "coq_int31" by True. -Register compare31 as int31 compare in "coq_int31" by True. -Register addmuldiv31 as int31 addmuldiv in "coq_int31" by True. -Register lor31 as int31 lor in "coq_int31" by True. -Register land31 as int31 land in "coq_int31" by True. -Register lxor31 as int31 lxor in "coq_int31" by True. +Register add31 as int31.plus. +Register add31c as int31.plusc. +Register add31carryc as int31.pluscarryc. +Register sub31 as int31.minus. +Register sub31c as int31.minusc. +Register sub31carryc as int31.minuscarryc. +Register mul31 as int31.times. +Register mul31c as int31.timesc. +Register div3121 as int31.div21. +Register div31 as int31.diveucl. +Register compare31 as int31.compare. +Register addmuldiv31 as int31.addmuldiv. +Register lor31 as int31.lor. +Register land31 as int31.land. +Register lxor31 as int31.lxor. Definition lnot31 n := lxor31 Tn n. Definition ldiff31 n m := land31 n (lnot31 m). @@ -483,5 +491,5 @@ Definition tail031 (i:int31) := end) i On. -Register head031 as int31 head0 in "coq_int31" by True. -Register tail031 as int31 tail0 in "coq_int31" by True. +Register head031 as int31.head0. +Register tail031 as int31.tail0. diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 784e81758c..4bcd22543f 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -60,7 +60,7 @@ Section ZModulo. apply Z.lt_gt. unfold wB, base; auto with zarith. Qed. - Hint Resolve wB_pos. + Hint Resolve wB_pos : core. Lemma spec_to_Z_1 : forall x, 0 <= [|x|]. Proof. @@ -71,7 +71,7 @@ Section ZModulo. Proof. unfold to_Z; intros; destruct (Z_mod_lt x wB wB_pos); auto. Qed. - Hint Resolve spec_to_Z_1 spec_to_Z_2. + Hint Resolve spec_to_Z_1 spec_to_Z_2 : core. Lemma spec_to_Z : forall x, 0 <= [|x|] < wB. Proof. @@ -732,7 +732,7 @@ Section ZModulo. Proof. induction p; simpl; auto with zarith. Qed. - Hint Resolve Ptail_pos. + Hint Resolve Ptail_pos : core. Lemma Ptail_bounded : forall p d, Zpos p < 2^(Zpos d) -> Ptail p < Zpos d. Proof. diff --git a/theories/Numbers/DecimalString.v b/theories/Numbers/DecimalString.v index 1a3220f63a..591024baec 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 2da4452819..4aabda77ee 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 d7f25a6613..a70ecd19d8 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: @@ -46,6 +46,7 @@ Module ZEuclidProp (** We put notations in a scope, to avoid warnings about redefinitions of notations *) + Declare Scope euclid. Infix "/" := D.div : euclid. Infix "mod" := D.modulo : euclid. Local Open Scope euclid. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 4b2d5c13b5..995d96b314 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -13,15 +13,18 @@ Require Import NSub ZAxioms. Require Export Ring. +Declare Scope pair_scope. +Local Open Scope pair_scope. + Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. -Local Open Scope pair_scope. Module ZPairsAxiomsMod (Import N : NAxiomsMiniSig) <: ZAxiomsMiniSig. Module Import NProp. Include NSubProp N. End NProp. +Declare Scope NScope. Delimit Scope NScope with N. Bind Scope NScope with N.t. Infix "==" := N.eq (at level 70) : NScope. @@ -73,6 +76,7 @@ Definition max (n m : t) : t := (max (n#1 + m#2) (m#1 + n#2), n#2 + m#2). End Z. +Declare Scope ZScope. Delimit Scope ZScope with Z. Bind Scope ZScope with Z.t. Infix "==" := Z.eq (at level 70) : ZScope. diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index 3d0c005fd1..acebfcf1d2 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -220,8 +220,10 @@ End NZDomainProp. Module NZOfNat (Import NZ:NZDomainSig'). Definition ofnat (n : nat) : t := (S^n) 0. -Notation "[ n ]" := (ofnat n) (at level 7) : ofnat. + +Declare Scope ofnat. Local Open Scope ofnat. +Notation "[ n ]" := (ofnat n) (at level 7) : ofnat. Lemma ofnat_zero : [O] == 0. Proof. diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index e1391f5990..90663de3f2 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... *) diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 8e1be0d702..4539dea276 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -383,7 +383,7 @@ f_equiv. apply E, half_decrease. rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H. order'. Qed. -Hint Resolve log_good_step. +Hint Resolve log_good_step : core. Theorem log_init : forall n, n < 2 -> log n == 0. Proof. |