From f61a557fbbdb89a4c24a8050a67252c3ecda6ea7 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:09 +0000 Subject: Definitions of positive, N, Z moved in Numbers/BinNums.v In the coming reorganisation, the name Z in BinInt will be a module containing all code and properties about binary integers. The inductive type Z hence cannot be at the same location. Same for N and positive. Apart for this naming constraint, it also have advantages : presenting the three types at once is clearer, and we will be able to refer to N in BinPos (for instance for output type of a predecessor function on positive). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14097 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/coqlib.ml | 6 ++-- plugins/micromega/ZMicromega.v | 2 +- plugins/micromega/coq_micromega.ml | 41 +++++++++++-------------- plugins/nsatz/nsatz.ml4 | 27 +++++++++-------- plugins/rtauto/refl_tauto.ml | 2 +- plugins/syntax/z_syntax.ml | 25 ++++++++-------- theories/NArith/BinNat.v | 34 +++++++++------------ theories/NArith/NArith.v | 1 + theories/Numbers/BinNums.v | 61 ++++++++++++++++++++++++++++++++++++++ theories/Numbers/vo.itarget | 1 + theories/PArith/BinPos.v | 40 +++++++++++-------------- theories/PArith/PArith.v | 2 +- theories/ZArith/BinInt.v | 38 +++++++++++------------- theories/ZArith/ZArith_base.v | 1 + 14 files changed, 163 insertions(+), 118 deletions(-) create mode 100644 theories/Numbers/BinNums.v diff --git a/interp/coqlib.ml b/interp/coqlib.ml index ac1aa1879..0f3d1bab2 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -91,12 +91,12 @@ let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s let arith_dir = ["Coq";"Arith"] let arith_modules = [arith_dir] +let numbers_dir = [ "Coq";"Numbers"] let parith_dir = ["Coq";"PArith"] - let narith_dir = ["Coq";"NArith"] - let zarith_dir = ["Coq";"ZArith"] -let zarith_base_modules = [parith_dir;narith_dir;zarith_dir] + +let zarith_base_modules = [numbers_dir;parith_dir;narith_dir;zarith_dir] let init_dir = ["Coq";"Init"] let init_modules = [ diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index c8d324730..ab63f7bf0 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -194,7 +194,7 @@ Definition xnormalise (t:Formula Z) : list (NFormula Z) := | OpLe => (psub lhs (padd rhs (Pc 1)),NonStrict) :: nil end. -Require Import Tauto. +Require Import Tauto BinNums. Definition normalise (t:Formula Z) : cnf (NFormula Z) := List.map (fun x => x::nil) (xnormalise t). diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index d410d6a5c..877d468fd 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -220,6 +220,8 @@ struct ["Coq";"Reals" ; "Rpow_def"]; ["LRing_normalise"]] + let bin_module = [["Coq";"Numbers";"BinNums"]] + let r_modules = [["Coq";"Reals" ; "Rdefinitions"]; ["Coq";"Reals" ; "Rpow_def"]] @@ -231,6 +233,7 @@ struct let init_constant = gen_constant_in_modules "ZMicromega" init_modules let constant = gen_constant_in_modules "ZMicromega" coq_modules + let bin_constant = gen_constant_in_modules "ZMicromega" bin_module let r_constant = gen_constant_in_modules "ZMicromega" r_modules (* let constant = gen_constant_in_modules "Omicron" coq_modules *) @@ -249,31 +252,26 @@ struct let coq_S = lazy (init_constant "S") let coq_nat = lazy (init_constant "nat") - let coq_NO = lazy - (gen_constant_in_modules "N" [ ["Coq";"NArith";"BinNat" ]] "N0") - let coq_Npos = lazy - (gen_constant_in_modules "N" [ ["Coq";"NArith"; "BinNat"]] "Npos") - (* let coq_n = lazy (constant "N")*) + let coq_N0 = lazy (bin_constant "N0") + let coq_Npos = lazy (bin_constant "Npos") + + let coq_pair = lazy (init_constant "pair") + let coq_None = lazy (init_constant "None") + let coq_option = lazy (init_constant "option") - let coq_pair = lazy (constant "pair") - let coq_None = lazy (constant "None") - let coq_option = lazy (constant "option") - let coq_positive = lazy (constant "positive") - let coq_xH = lazy (constant "xH") - let coq_xO = lazy (constant "xO") - let coq_xI = lazy (constant "xI") + let coq_positive = lazy (bin_constant "positive") + let coq_xH = lazy (bin_constant "xH") + let coq_xO = lazy (bin_constant "xO") + let coq_xI = lazy (bin_constant "xI") - let coq_N0 = lazy (constant "N0") - let coq_N0 = lazy (constant "Npos") + let coq_Z = lazy (bin_constant "Z") + let coq_ZERO = lazy (bin_constant "Z0") + let coq_POS = lazy (bin_constant "Zpos") + let coq_NEG = lazy (bin_constant "Zneg") - let coq_Z = lazy (constant "Z") let coq_Q = lazy (constant "Q") let coq_R = lazy (constant "R") - let coq_ZERO = lazy (constant "Z0") - let coq_POS = lazy (constant "Zpos") - let coq_NEG = lazy (constant "Zneg") - let coq_Build_Witness = lazy (constant "Build_Witness") let coq_Qmake = lazy (constant "Qmake") @@ -496,11 +494,6 @@ struct let pp_index o x = Printf.fprintf o "%i" (CoqToCaml.index x) - let rec dump_n x = - match x with - | Mc.N0 -> Lazy.force coq_NO - | Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p |]) - let rec pp_n o x = output_string o (string_of_int (CoqToCaml.n x)) let dump_pair t1 t2 dump_t1 dump_t2 (x,y) = diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index 2b5a3e7c8..4b8b706d4 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -180,21 +180,24 @@ let ttmul = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEmul") let ttopp = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEopp") let ttpow = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEpow") -let tlist = lazy (gen_constant "CC" ["Lists";"List"] "list") -let lnil = lazy (gen_constant "CC" ["Lists";"List"] "nil") -let lcons = lazy (gen_constant "CC" ["Lists";"List"] "cons") +let datatypes = ["Init";"Datatypes"] +let binnums = ["Numbers";"BinNums"] -let tz = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Z") -let z0 = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Z0") -let zpos = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Zpos") -let zneg = lazy(gen_constant "CC" ["ZArith";"BinInt"] "Zneg") +let tlist = lazy (gen_constant "CC" datatypes "list") +let lnil = lazy (gen_constant "CC" datatypes "nil") +let lcons = lazy (gen_constant "CC" datatypes "cons") -let pxI = lazy(gen_constant "CC" ["PArith";"BinPos"] "xI") -let pxO = lazy(gen_constant "CC" ["PArith";"BinPos"] "xO") -let pxH = lazy(gen_constant "CC" ["PArith";"BinPos"] "xH") +let tz = lazy (gen_constant "CC" binnums "Z") +let z0 = lazy (gen_constant "CC" binnums "Z0") +let zpos = lazy (gen_constant "CC" binnums "Zpos") +let zneg = lazy(gen_constant "CC" binnums "Zneg") -let nN0 = lazy (gen_constant "CC" ["NArith";"BinNat"] "N0") -let nNpos = lazy(gen_constant "CC" ["NArith";"BinNat"] "Npos") +let pxI = lazy(gen_constant "CC" binnums "xI") +let pxO = lazy(gen_constant "CC" binnums "xO") +let pxH = lazy(gen_constant "CC" binnums "xH") + +let nN0 = lazy (gen_constant "CC" binnums "N0") +let nNpos = lazy(gen_constant "CC" binnums "Npos") let mkt_app name l = mkApp (Lazy.force name, Array.of_list l) diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index a520ce2d4..cddc5472d 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -36,7 +36,7 @@ let l_true_equals_true = [|data_constant "bool";data_constant "true"|])) let pos_constant = - Coqlib.gen_constant "refl_tauto" ["PArith";"BinPos"] + Coqlib.gen_constant "refl_tauto" ["Numbers";"BinNums"] let l_xI = lazy (pos_constant "xI") let l_xO = lazy (pos_constant "xO") diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index cf0253d1f..f8bce8f79 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -22,17 +22,18 @@ exception Non_closed_number open Libnames open Glob_term + +let binnums = ["Coq";"Numbers";"BinNums"] + let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) -let positive_module = ["Coq";"PArith";"BinPos"] let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id) -let positive_path = make_path positive_module "positive" +let positive_path = make_path binnums "positive" (* TODO: temporary hack *) let make_kn dir id = Libnames.encode_mind dir id -let positive_kn = - make_kn (make_dir positive_module) (id_of_string "positive") +let positive_kn = make_kn (make_dir binnums) (id_of_string "positive") let glob_positive = IndRef (positive_kn,0) let path_of_xI = ((positive_kn,0),1) let path_of_xO = ((positive_kn,0),2) @@ -82,7 +83,7 @@ let uninterp_positive p = (************************************************************************) let _ = Notation.declare_numeral_interpreter "positive_scope" - (positive_path,positive_module) + (positive_path,binnums) interp_positive ([GRef (dummy_loc, glob_xI); GRef (dummy_loc, glob_xO); @@ -94,15 +95,14 @@ let _ = Notation.declare_numeral_interpreter "positive_scope" (* Parsing N via scopes *) (**********************************************************************) -let binnat_module = ["Coq";"NArith";"BinNat"] -let n_kn = make_kn (make_dir binnat_module) (id_of_string "N") +let n_kn = make_kn (make_dir binnums) (id_of_string "N") let glob_n = IndRef (n_kn,0) let path_of_N0 = ((n_kn,0),1) let path_of_Npos = ((n_kn,0),2) let glob_N0 = ConstructRef path_of_N0 let glob_Npos = ConstructRef path_of_Npos -let n_path = make_path binnat_module "N" +let n_path = make_path binnums "N" let n_of_binnat dloc pos_or_neg n = if n <> zero then @@ -134,7 +134,7 @@ let uninterp_n p = (* Declaring interpreters and uninterpreters for N *) let _ = Notation.declare_numeral_interpreter "N_scope" - (n_path,binnat_module) + (n_path,binnums) n_of_int ([GRef (dummy_loc, glob_N0); GRef (dummy_loc, glob_Npos)], @@ -145,9 +145,8 @@ let _ = Notation.declare_numeral_interpreter "N_scope" (* Parsing Z via scopes *) (**********************************************************************) -let binint_module = ["Coq";"ZArith";"BinInt"] -let z_path = make_path binint_module "Z" -let z_kn = make_kn (make_dir binint_module) (id_of_string "Z") +let z_path = make_path binnums "Z" +let z_kn = make_kn (make_dir binnums) (id_of_string "Z") let glob_z = IndRef (z_kn,0) let path_of_ZERO = ((z_kn,0),1) let path_of_POS = ((z_kn,0),2) @@ -183,7 +182,7 @@ let uninterp_z p = (* Declaring interpreters and uninterpreters for Z *) let _ = Notation.declare_numeral_interpreter "Z_scope" - (z_path,binint_module) + (z_path,binnums) z_of_int ([GRef (dummy_loc, glob_ZERO); GRef (dummy_loc, glob_POS); diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 3f256b40f..3e576a08b 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -6,33 +6,18 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +Require Export BinNums. Require Import BinPos. (**********************************************************************) -(** Binary natural numbers *) - -Inductive N : Set := - | N0 : N - | Npos : positive -> N. - -(** Declare binding key for scope positive_scope *) - -Delimit Scope N_scope with N. - -(** Automatically open scope positive_scope for the constructors of N *) +(** * Binary natural numbers, operations and properties *) +(**********************************************************************) -Bind Scope N_scope with N. -Arguments Scope Npos [positive_scope]. +(** The type [N] and its constructors [N0] and [Npos] are now + defined in [BinNums.v] *) Local Open Scope N_scope. -(** Some local ad-hoc notation, since no interpretation of numerical - constants is available yet. *) - -Local Notation "0" := N0 : N_scope. -Local Notation "1" := (Npos 1) : N_scope. -Local Notation "2" := (Npos 2) : N_scope. - Definition Ndiscr : forall n:N, { p:positive | n = Npos p } + { n = N0 }. Proof. destruct n; auto. @@ -693,3 +678,12 @@ Proof. intros (m,H). now destruct m. exists 0. reflexivity. Qed. + +(** Compatibility notations *) + +Notation N := N (only parsing). +Notation N_rect := N_rect (only parsing). +Notation N_rec := N_rec (only parsing). +Notation N_ind := N_ind (only parsing). +Notation N0 := N0 (only parsing). +Notation Npos := Npos (only parsing). diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v index 22c9012a7..6bfc323d6 100644 --- a/theories/NArith/NArith.v +++ b/theories/NArith/NArith.v @@ -8,6 +8,7 @@ (** Library for binary natural numbers *) +Require Export BinNums. Require Export BinPos. Require Export BinNat. Require Export Nnat. diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v new file mode 100644 index 000000000..69754f144 --- /dev/null +++ b/theories/Numbers/BinNums.v @@ -0,0 +1,61 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* positive + | xO : positive -> positive + | xH : positive. + +Delimit Scope positive_scope with positive. +Bind Scope positive_scope with positive. +Arguments Scope xO [positive_scope]. +Arguments Scope xI [positive_scope]. + +(** [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))] *) + +Inductive N : Set := + | N0 : N + | Npos : positive -> N. + +Delimit Scope N_scope with N. +Bind Scope N_scope with N. +Arguments Scope Npos [positive_scope]. + +(** [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))] *) + +Inductive Z : Set := + | Z0 : Z + | Zpos : positive -> Z + | Zneg : positive -> Z. + +Delimit Scope Z_scope with Z. +Bind Scope Z_scope with Z. +Arguments Scope Zpos [positive_scope]. +Arguments Scope Zneg [positive_scope]. diff --git a/theories/Numbers/vo.itarget b/theories/Numbers/vo.itarget index baefbd252..c69af03fc 100644 --- a/theories/Numbers/vo.itarget +++ b/theories/Numbers/vo.itarget @@ -1,3 +1,4 @@ +BinNums.vo BigNumPrelude.vo Cyclic/Abstract/CyclicAxioms.vo Cyclic/Abstract/NZCyclic.vo diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index ec18d8dc5..badae225f 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -7,32 +7,20 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Declare ML Module "z_syntax_plugin". +Require Export BinNums. (**********************************************************************) -(** * Binary positive numbers *) +(** * Binary positive numbers, operations and properties *) (**********************************************************************) (** Initial development by Pierre Crégut, CNET, Lannion, France *) -Inductive positive : Set := -| xI : positive -> positive -| xO : positive -> positive -| xH : positive. - -(** Declare binding key for scope positive_scope *) - -Delimit Scope positive_scope with positive. - -(** Automatically open scope positive_scope for type positive, xO and xI *) - -Bind Scope positive_scope with positive. -Arguments Scope xO [positive_scope]. -Arguments Scope xI [positive_scope]. +(** The type [positive] and its constructors [xI] and [xO] and [xH] + are now defined in [BinNums.v] *) (** Postfix notation for positive numbers, allowing to mimic the position of bits in a big-endian representation. - For instance, we can write 1~1~0 instead of (xO (xI xH)) + For instance, we can write [1~1~0] instead of [(xO (xI xH))] for the number 6 (which is 110 in binary notation). *) @@ -42,12 +30,8 @@ Notation "p ~ 0" := (xO p) (at level 7, left associativity, format "p '~' '0'") : positive_scope. Local Open Scope positive_scope. - -(* In the current file, [xH] cannot yet be written as [1], since the - interpretation of positive numerical constants is not available - yet. We fix this here with an ad-hoc temporary notation. *) - -Local Notation "1" := xH (at level 7). +Local Unset Boolean Equality Schemes. +Local Unset Case Analysis Schemes. (**********************************************************************) (** * Operations over positive numbers *) @@ -1599,3 +1583,13 @@ Proof. apply Pmult_le_mono_l. apply Ple_lteq; left. rewrite xI_succ_xO. apply Plt_succ_r, IHp. Qed. + +(** Compatibility notations *) + +Notation positive := positive (only parsing). +Notation positive_rect := positive_rect (only parsing). +Notation positive_rec := positive_rec (only parsing). +Notation positive_ind := positive_ind (only parsing). +Notation xI := xI (only parsing). +Notation xO := xO (only parsing). +Notation xH := xH (only parsing). diff --git a/theories/PArith/PArith.v b/theories/PArith/PArith.v index 8688c5013..e2bec88af 100644 --- a/theories/PArith/PArith.v +++ b/theories/PArith/PArith.v @@ -8,4 +8,4 @@ (** Library for positive natural numbers *) -Require Export BinPos Pnat Pminmax Psqrt Pgcd POrderedType. +Require Export BinNums BinPos Pnat Pminmax Psqrt Pgcd POrderedType. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index ad3781832..6e5443e35 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -7,25 +7,19 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +Require Export BinNums BinPos Pnat. +Require Import BinNat Plus Mult. + (***********************************************************) (** * Binary Integers *) -(** Initial author: Pierre Crégut, CNET, Lannion, France *) (***********************************************************) -Require Export BinPos Pnat. -Require Import BinNat Plus Mult. - -Inductive Z : Set := - | Z0 : Z - | Zpos : positive -> Z - | Zneg : positive -> Z. +(** Initial author: Pierre Crégut, CNET, Lannion, France *) +(** The type [Z] and its constructors [Z0] and [Zpos] and [Zneg] + are now defined in [BinNums.v] *) -(** Automatically open scope positive_scope for the constructors of Z *) -Delimit Scope Z_scope with Z. -Bind Scope Z_scope with Z. -Arguments Scope Zpos [positive_scope]. -Arguments Scope Zneg [positive_scope]. +Local Open Scope Z_scope. (*************************************) (** * Basic operations *) @@ -53,8 +47,6 @@ Definition Zdouble (x:Z) := | Zneg p => Zneg p~0 end. -Open Local Scope positive_scope. - Fixpoint ZPminus (x y:positive) {struct y} : Z := match x, y with | p~1, q~1 => Zdouble (ZPminus p q) @@ -66,9 +58,7 @@ Fixpoint ZPminus (x y:positive) {struct y} : Z := | 1, q~1 => Zneg q~0 | 1, q~0 => Zneg (Pdouble_minus_one q) | 1, 1 => Z0 - end. - -Close Local Scope positive_scope. + end%positive. (** ** Addition on integers *) @@ -191,8 +181,6 @@ Definition Zplus' (x y:Z) := | Zneg x', Zneg y' => Zneg (x' + y') end. -Open Local Scope Z_scope. - (**********************************************************************) (** ** Inductive specification of Z *) @@ -1050,3 +1038,13 @@ Definition Z_of_N (x:N) := | N0 => Z0 | Npos p => Zpos p end. + +(** Compatibility Notations *) + +Notation Z := Z (only parsing). +Notation Z_rect := Z_rect (only parsing). +Notation Z_rec := Z_rec (only parsing). +Notation Z_ind := Z_ind (only parsing). +Notation Z0 := Z0 (only parsing). +Notation Zpos := Zpos (only parsing). +Notation Zneg := Zneg (only parsing). diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v index 10a071c80..05df86880 100644 --- a/theories/ZArith/ZArith_base.v +++ b/theories/ZArith/ZArith_base.v @@ -10,6 +10,7 @@ These are the basic modules, required by [Omega] and [Ring] for instance. The full library is [ZArith]. *) +Require Export BinNums. Require Export BinPos. Require Export BinNat. Require Export BinInt. -- cgit v1.2.3