From 40bd00ad005033f188e12629b5141e95c1bfb476 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 30 Oct 2024 20:25:20 +0000 Subject: [PATCH 1/5] ZMicromega depends on BinInt not ZArith_base; deprecate Ztac --- .../19792-zmicromega-without-zarith.rst | 4 + plugins/micromega/certificate.ml | 4 +- plugins/micromega/coq_micromega.ml | 2 +- plugins/micromega/micromega.ml | 53 ++-- plugins/micromega/micromega.mli | 4 +- stdlib/test-suite/bugs/bug_4187.v | 2 + stdlib/test-suite/bugs/bug_5359.v | 2 + stdlib/test-suite/output/Fixpoint.v | 2 +- stdlib/test-suite/output/Intuition.v | 2 +- stdlib/test-suite/output/MExtraction.out | 53 ++-- stdlib/test-suite/output/MExtraction.v | 2 +- stdlib/test-suite/success/Nsatz.v | 1 + stdlib/theories/Reals/R_Ifp.v | 17 +- stdlib/theories/Reals/Rfunctions.v | 8 +- stdlib/theories/micromega/Lia.v | 2 +- stdlib/theories/micromega/RMicromega.v | 2 +- stdlib/theories/micromega/ZMicromega.v | 232 +++++++----------- stdlib/theories/micromega/Ztac.v | 82 +++---- 18 files changed, 227 insertions(+), 247 deletions(-) create mode 100644 doc/changelog/11-standard-library/19792-zmicromega-without-zarith.rst diff --git a/doc/changelog/11-standard-library/19792-zmicromega-without-zarith.rst b/doc/changelog/11-standard-library/19792-zmicromega-without-zarith.rst new file mode 100644 index 000000000000..aa975eb38bc4 --- /dev/null +++ b/doc/changelog/11-standard-library/19792-zmicromega-without-zarith.rst @@ -0,0 +1,4 @@ +- **Deprecated:** internal-to-be-internal module :g:`Ztac`; use `Lia` instead. + **Changed:** :g:`ZMicromega` to use :g:`Z.eqb` instead of :g:`Zeq_bool` + (`#19792 `_, + by Andres Erbsen). diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index e952fed7a68c..f5d0b3b6fb7e 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -53,7 +53,7 @@ let z_spec = ; zero = Mc.Z0 ; unit = Mc.Zpos Mc.XH ; mult = Mc.Z.mul - ; eqb = Mc.zeq_bool } + ; eqb = Mc.Z.eqb } let q_spec = { bigint_to_number = (fun x -> {Mc.qnum = Ml2C.bigint x; Mc.qden = Mc.XH}) @@ -677,7 +677,7 @@ let rec term_to_z_expr = function let term_to_z_pol e = Mc.norm_aux (Ml2C.z 0) (Ml2C.z 1) Mc.Z.add Mc.Z.mul Mc.Z.sub Mc.Z.opp - Mc.zeq_bool (term_to_z_expr e) + Mc.Z.eqb (term_to_z_expr e) let z_cert_of_pos pos = let s, pos = scale_certificate pos in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 410983326c37..5558a7e7397e 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1509,7 +1509,7 @@ let zz_domain_spec = ; undump_coeff = parse_z ; proof_typ = Lazy.force rocq_proofTerm ; dump_proof = dump_proof_term - ; coeff_eq = Mc.zeq_bool } + ; coeff_eq = Mc.Z.eqb } let qq_domain_spec = lazy diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index fe63c077a919..ede8497a9ec3 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -292,6 +292,20 @@ module Coq_Pos = | Gt -> p | _ -> p' + (** val eqb : positive -> positive -> bool **) + + let rec eqb p q0 = + match p with + | XI p2 -> (match q0 with + | XI q1 -> eqb p2 q1 + | _ -> false) + | XO p2 -> (match q0 with + | XO q1 -> eqb p2 q1 + | _ -> false) + | XH -> (match q0 with + | XH -> true + | _ -> false) + (** val leb : positive -> positive -> bool **) let leb x y = @@ -486,6 +500,20 @@ module Z = | Gt -> true | _ -> false + (** val eqb : z -> z -> bool **) + + let eqb x y = + match x with + | Z0 -> (match y with + | Z0 -> true + | _ -> false) + | Zpos p -> (match y with + | Zpos q0 -> Coq_Pos.eqb p q0 + | _ -> false) + | Zneg p -> (match y with + | Zneg q0 -> Coq_Pos.eqb p q0 + | _ -> false) + (** val max : z -> z -> z **) let max n0 m = @@ -581,13 +609,6 @@ module Z = | Zneg b0 -> Zpos (Coq_Pos.gcd a0 b0)) end -(** val zeq_bool : z -> z -> bool **) - -let zeq_bool x y = - match Z.compare x y with - | Eq -> true - | _ -> false - type 'c pExpr = | PEc of 'c | PEX of positive @@ -2045,7 +2066,7 @@ type q = { qnum : z; qden : positive } (** val qeq_bool : q -> q -> bool **) let qeq_bool x y = - zeq_bool (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden)) + Z.eqb (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden)) (** val qle_bool : q -> q -> bool **) @@ -2153,12 +2174,12 @@ type zWitness = z psatz (** val zWeakChecker : z nFormula list -> z psatz -> bool **) let zWeakChecker = - check_normalised_formulas Z0 (Zpos XH) Z.add Z.mul zeq_bool Z.leb + check_normalised_formulas Z0 (Zpos XH) Z.add Z.mul Z.eqb Z.leb (** val psub1 : z pol -> z pol -> z pol **) let psub1 = - psub0 Z0 Z.add Z.sub Z.opp zeq_bool + psub0 Z0 Z.add Z.sub Z.opp Z.eqb (** val popp1 : z pol -> z pol **) @@ -2168,22 +2189,22 @@ let popp1 = (** val padd1 : z pol -> z pol -> z pol **) let padd1 = - padd0 Z0 Z.add zeq_bool + padd0 Z0 Z.add Z.eqb (** val normZ : z pExpr -> z pol **) let normZ = - norm Z0 (Zpos XH) Z.add Z.mul Z.sub Z.opp zeq_bool + norm Z0 (Zpos XH) Z.add Z.mul Z.sub Z.opp Z.eqb (** val zunsat : z nFormula -> bool **) let zunsat = - check_inconsistent Z0 zeq_bool Z.leb + check_inconsistent Z0 Z.eqb Z.leb (** val zdeduce : z nFormula -> z nFormula -> z nFormula option **) let zdeduce = - nformula_plus_nformula Z0 Z.add zeq_bool + nformula_plus_nformula Z0 Z.add Z.eqb (** val xnnormalise : z formula -> z nFormula **) @@ -2300,7 +2321,7 @@ let genCuttingPlane = function | Equal -> let g,c = zgcd_pol e in if (&&) (Z.gtb g Z0) - ((&&) (negb (zeq_bool c Z0)) (negb (zeq_bool (Z.gcd g c) g))) + ((&&) (negb (Z.eqb c Z0)) (negb (Z.eqb (Z.gcd g c) g))) then None else Some ((makeCuttingPlane e),Equal) | NonEqual -> Some ((e,Z0),op) @@ -2323,7 +2344,7 @@ let is_pol_Z0 = function (** val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option **) let eval_Psatz0 = - eval_Psatz Z0 (Zpos XH) Z.add Z.mul zeq_bool Z.leb + eval_Psatz Z0 (Zpos XH) Z.add Z.mul Z.eqb Z.leb (** val valid_cut_sign : op1 -> bool **) diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli index 770d55df439a..7d817fbaaf0d 100644 --- a/plugins/micromega/micromega.mli +++ b/plugins/micromega/micromega.mli @@ -143,6 +143,8 @@ module Z : val compare : z -> z -> comparison + val eqb : z -> z -> bool + val leb : z -> z -> bool val ltb : z -> z -> bool @@ -168,8 +170,6 @@ module Z : val gcd : z -> z -> z end -val zeq_bool : z -> z -> bool - type 'c pExpr = | PEc of 'c | PEX of positive diff --git a/stdlib/test-suite/bugs/bug_4187.v b/stdlib/test-suite/bugs/bug_4187.v index 9783319cedc3..58e782f4af16 100644 --- a/stdlib/test-suite/bugs/bug_4187.v +++ b/stdlib/test-suite/bugs/bug_4187.v @@ -7,6 +7,8 @@ Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. From Stdlib Require Import List. From Stdlib Require Import Setoid. +From Stdlib Require Import BinNat. +From Stdlib Require Import Sumbool. Global Set Implicit Arguments. Global Generalizable All Variables. Coercion is_true : bool >-> Sortclass. diff --git a/stdlib/test-suite/bugs/bug_5359.v b/stdlib/test-suite/bugs/bug_5359.v index ba79b2c41cca..eb8205940f88 100644 --- a/stdlib/test-suite/bugs/bug_5359.v +++ b/stdlib/test-suite/bugs/bug_5359.v @@ -1,4 +1,6 @@ From Stdlib Require Import Nsatz. +From Stdlib Require Import BinNat. + Goal False. (* the first (succeeding) goal was reached by clearing one hypothesis in the second goal which overflows 6GB of stack space *) diff --git a/stdlib/test-suite/output/Fixpoint.v b/stdlib/test-suite/output/Fixpoint.v index 292e57a6acd9..d9231be879f4 100644 --- a/stdlib/test-suite/output/Fixpoint.v +++ b/stdlib/test-suite/output/Fixpoint.v @@ -16,7 +16,7 @@ Check end in f 0. -From Stdlib Require Import ZArith_base Lia. +From Stdlib Require Import BinInt Lia. Open Scope Z_scope. Inductive even: Z -> Prop := diff --git a/stdlib/test-suite/output/Intuition.v b/stdlib/test-suite/output/Intuition.v index 6600899e96a0..b42a021b9961 100644 --- a/stdlib/test-suite/output/Intuition.v +++ b/stdlib/test-suite/output/Intuition.v @@ -1,4 +1,4 @@ -From Stdlib Require Import ZArith_base. +From Stdlib Require Import BinInt. Goal forall m n : Z, (m >= n)%Z -> (m >= m)%Z /\ (m >= n)%Z. intros; intuition. Show. diff --git a/stdlib/test-suite/output/MExtraction.out b/stdlib/test-suite/output/MExtraction.out index 6a7c72d6f73f..179e588c09d7 100644 --- a/stdlib/test-suite/output/MExtraction.out +++ b/stdlib/test-suite/output/MExtraction.out @@ -206,6 +206,20 @@ module Pos = let compare = compare_cont Eq + (** val eqb : positive -> positive -> bool **) + + let rec eqb p q0 = + match p with + | XI p2 -> (match q0 with + | XI q1 -> eqb p2 q1 + | _ -> false) + | XO p2 -> (match q0 with + | XO q1 -> eqb p2 q1 + | _ -> false) + | XH -> (match q0 with + | XH -> true + | _ -> false) + (** val of_succ_nat : nat -> positive **) let rec of_succ_nat = function @@ -560,6 +574,20 @@ module Z = | Lt -> true | _ -> false + (** val eqb : z -> z -> bool **) + + let eqb x y = + match x with + | Z0 -> (match y with + | Z0 -> true + | _ -> false) + | Zpos p -> (match y with + | Zpos q0 -> Pos.eqb p q0 + | _ -> false) + | Zneg p -> (match y with + | Zneg q0 -> Pos.eqb p q0 + | _ -> false) + (** val max : z -> z -> z **) let max n0 m = @@ -662,13 +690,6 @@ module Z = | Zneg b0 -> Zpos (Coq_Pos.gcd a0 b0)) end -(** val zeq_bool : z -> z -> bool **) - -let zeq_bool x y = - match Z.compare x y with - | Eq -> true - | _ -> false - type 'c pExpr = | PEc of 'c | PEX of positive @@ -2126,7 +2147,7 @@ type q = { qnum : z; qden : positive } (** val qeq_bool : q -> q -> bool **) let qeq_bool x y = - zeq_bool (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden)) + Z.eqb (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden)) (** val qle_bool : q -> q -> bool **) @@ -2234,12 +2255,12 @@ type zWitness = z psatz (** val zWeakChecker : z nFormula list -> z psatz -> bool **) let zWeakChecker = - check_normalised_formulas Z0 (Zpos XH) Z.add Z.mul zeq_bool Z.leb + check_normalised_formulas Z0 (Zpos XH) Z.add Z.mul Z.eqb Z.leb (** val psub1 : z pol -> z pol -> z pol **) let psub1 = - psub0 Z0 Z.add Z.sub Z.opp zeq_bool + psub0 Z0 Z.add Z.sub Z.opp Z.eqb (** val popp1 : z pol -> z pol **) @@ -2249,22 +2270,22 @@ let popp1 = (** val padd1 : z pol -> z pol -> z pol **) let padd1 = - padd0 Z0 Z.add zeq_bool + padd0 Z0 Z.add Z.eqb (** val normZ : z pExpr -> z pol **) let normZ = - norm Z0 (Zpos XH) Z.add Z.mul Z.sub Z.opp zeq_bool + norm Z0 (Zpos XH) Z.add Z.mul Z.sub Z.opp Z.eqb (** val zunsat : z nFormula -> bool **) let zunsat = - check_inconsistent Z0 zeq_bool Z.leb + check_inconsistent Z0 Z.eqb Z.leb (** val zdeduce : z nFormula -> z nFormula -> z nFormula option **) let zdeduce = - nformula_plus_nformula Z0 Z.add zeq_bool + nformula_plus_nformula Z0 Z.add Z.eqb (** val xnnormalise : z formula -> z nFormula **) @@ -2381,7 +2402,7 @@ let genCuttingPlane = function | Equal -> let g,c = zgcd_pol e in if (&&) (Z.gtb g Z0) - ((&&) (negb (zeq_bool c Z0)) (negb (zeq_bool (Z.gcd g c) g))) + ((&&) (negb (Z.eqb c Z0)) (negb (Z.eqb (Z.gcd g c) g))) then None else Some ((makeCuttingPlane e),Equal) | NonEqual -> Some ((e,Z0),op) @@ -2404,7 +2425,7 @@ let is_pol_Z0 = function (** val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option **) let eval_Psatz0 = - eval_Psatz Z0 (Zpos XH) Z.add Z.mul zeq_bool Z.leb + eval_Psatz Z0 (Zpos XH) Z.add Z.mul Z.eqb Z.leb (** val valid_cut_sign : op1 -> bool **) diff --git a/stdlib/test-suite/output/MExtraction.v b/stdlib/test-suite/output/MExtraction.v index b870c1427f3b..a31c99366664 100644 --- a/stdlib/test-suite/output/MExtraction.v +++ b/stdlib/test-suite/output/MExtraction.v @@ -61,7 +61,7 @@ Recursive Extraction ZMicromega.cnfZ ZMicromega.Zeval_const QMicromega.cnfQ List.map simpl_cone (*map_cone indexes*) denorm QArith_base.Qpower vm_add - normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. + normZ normQ normQ Z.to_N N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. (* Local Variables: *) (* coding: utf-8 *) diff --git a/stdlib/test-suite/success/Nsatz.v b/stdlib/test-suite/success/Nsatz.v index 021f5181b36c..e6516770eab4 100644 --- a/stdlib/test-suite/success/Nsatz.v +++ b/stdlib/test-suite/success/Nsatz.v @@ -1,5 +1,6 @@ (* compile en user 3m39.915s sur cachalot *) +From Stdlib Require Import BinNat. From Stdlib Require Import Nsatz. From Stdlib Require List. Import List.ListNotations. diff --git a/stdlib/theories/Reals/R_Ifp.v b/stdlib/theories/Reals/R_Ifp.v index 859f8290dc5d..62da97bab415 100644 --- a/stdlib/theories/Reals/R_Ifp.v +++ b/stdlib/theories/Reals/R_Ifp.v @@ -14,7 +14,7 @@ (**********************************************************) Require Import Rdefinitions Raxioms RIneq. -Require Import ZArith Ztac. +Require Import ZArith. Local Open Scope R_scope. (*********************************************************) @@ -72,9 +72,7 @@ Proof. apply lt_IZR in H1. rewrite <- minus_IZR in H2. apply le_IZR in H2. - normZ. - + slia H2 HZ. - + slia H1 HZ. + Lia.lia. Qed. (**********) @@ -313,9 +311,7 @@ Proof. rewrite <- (plus_IZR (Int_part r1 + Int_part r2 + 1) 1) in H0; generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2 + 1) H H0); intro; clear H H0; unfold Int_part at 1. - normZ. - - slia H HZ. - - slia H0 HZ. + Lia.lia. Qed. (**********) @@ -377,9 +373,7 @@ Proof. rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1; generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2) H0 H1); intro; clear H0 H1; unfold Int_part at 1. - normZ. - - slia H HZ. - - slia H0 HZ. + Lia.lia. Qed. (**********) @@ -422,3 +416,6 @@ Proof. rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2))); unfold Rminus; trivial with zarith real. Qed. + +Local Set Warnings "-deprecated". +Require Ztac. (* deprecated since 9.0 *) diff --git a/stdlib/theories/Reals/Rfunctions.v b/stdlib/theories/Reals/Rfunctions.v index 3f5b230767bb..9b0b235f488f 100644 --- a/stdlib/theories/Reals/Rfunctions.v +++ b/stdlib/theories/Reals/Rfunctions.v @@ -26,7 +26,6 @@ Require Export SplitAbsolu. Require Export SplitRmult. Require Export ArithProp. Require Import Zpower. -Require Import Ztac. Local Open Scope nat_scope. Local Open Scope R_scope. @@ -265,12 +264,12 @@ Proof. + elim (IZN (up (b * / (Rabs x - 1))) H2); intros; exists x0; apply (Rge_trans (INR x0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))). - * rewrite INR_IZR_INZ; apply IZR_ge. normZ. slia H3 H5. + * rewrite INR_IZR_INZ; apply IZR_ge. Lia.lia. * unfold Rge; left; assumption. + exists 0%nat; apply (Rge_trans (INR 0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))). - * rewrite INR_IZR_INZ; apply IZR_ge; simpl. normZ. slia H2 H3. + * rewrite INR_IZR_INZ; apply IZR_ge; simpl. Lia.lia. * unfold Rge; left; assumption. Qed. @@ -938,3 +937,6 @@ Definition infinite_sum (s:nat -> R) (l:R) : Prop := (** Compatibility with previous versions *) Notation infinit_sum := infinite_sum (only parsing). + +Local Set Warnings "-deprecated". +Require Ztac. (* deprecated since 9.0 *) diff --git a/stdlib/theories/micromega/Lia.v b/stdlib/theories/micromega/Lia.v index 89aa88b4de08..a0389e2da618 100644 --- a/stdlib/theories/micromega/Lia.v +++ b/stdlib/theories/micromega/Lia.v @@ -14,7 +14,7 @@ (* *) (************************************************************************) -Require Import ZMicromega RingMicromega VarMap DeclConstant. +Require Import PreOmega ZMicromega RingMicromega VarMap DeclConstant. Require Import BinNums. Require Stdlib.micromega.Tauto. Declare ML Module "rocq-runtime.plugins.micromega_core". diff --git a/stdlib/theories/micromega/RMicromega.v b/stdlib/theories/micromega/RMicromega.v index 41ceb8a33220..58c6dcd36d56 100644 --- a/stdlib/theories/micromega/RMicromega.v +++ b/stdlib/theories/micromega/RMicromega.v @@ -352,7 +352,7 @@ Proof. * rewrite andb_false_iff in C. destruct C. -- simpl. apply Z.ltb_ge in H. - right. Ztac.normZ. Ztac.slia H H0. + auto using Z.le_ge. -- left ; apply Qeq_bool_neq; auto. + simpl. rewrite <- IHc. diff --git a/stdlib/theories/micromega/ZMicromega.v b/stdlib/theories/micromega/ZMicromega.v index d3323459225e..c863394e43fd 100644 --- a/stdlib/theories/micromega/ZMicromega.v +++ b/stdlib/theories/micromega/ZMicromega.v @@ -20,10 +20,9 @@ Require Import OrderedRing. Require Import RingMicromega. Require Import ZCoeff. Require Import Refl. -Require Import ZArith_base. -Require Import ZArithRing. -Require Import Ztac. -Require PreOmega. +Require Import BinInt. +Require InitialRing. +Require Import micromega.Tauto. Local Open Scope Z_scope. Ltac flatten_bool := @@ -39,60 +38,29 @@ Proof. intros. split ; intros H. - subst. - compute. intuition congruence. + split; reflexivity. - destruct H. apply Z.le_antisymm; auto. Qed. -Lemma lt_le_iff : forall x, - 0 < x <-> 0 <= x - 1. -Proof. - split ; intros H. - - apply Zlt_succ_le. - ring_simplify. - auto. - - apply Zle_lt_succ in H. - ring_simplify in H. - auto. -Qed. +Lemma lt_le_iff x : 0 < x <-> 0 <= x - 1. +Proof. rewrite <-Z.lt_succ_r, Z.sub_1_r, Z.succ_pred; reflexivity. Qed. -Lemma le_0_iff : forall x y, - x <= y <-> 0 <= y - x. -Proof. - split ; intros. - - apply Zle_minus_le_0; auto. - - apply Zle_0_minus_le; auto. -Qed. +Lemma le_0_iff x y : x <= y <-> 0 <= y - x. +Proof. symmetry. apply Z.le_0_sub. Qed. -Lemma le_neg : forall x, - ((0 <= x) -> False) <-> 0 < -x. -Proof. - intro. - rewrite lt_le_iff. - split ; intros H. - - apply Znot_le_gt in H. - apply Zgt_le_succ in H. - rewrite le_0_iff in H. - ring_simplify in H; auto. - - intro H0. - assert (C := (Z.add_le_mono _ _ _ _ H H0)). - ring_simplify in C. - compute in C. - apply C ; reflexivity. -Qed. +Lemma le_neg x : ((0 <= x) -> False) <-> 0 < -x. +Proof. setoid_rewrite Z.nle_gt. rewrite Z.opp_pos_neg. reflexivity. Qed. -Lemma eq_cnf : forall x, - (0 <= x - 1 -> False) /\ (0 <= -1 - x -> False) <-> x = 0. +Lemma eq_cnf x : (0 <= x - 1 -> False) /\ (0 <= -1 - x -> False) <-> x = 0. Proof. - intros x. - rewrite Z.eq_sym_iff. - rewrite eq_le_iff. - rewrite (le_0_iff x 0). - rewrite !le_neg. - rewrite !lt_le_iff. - replace (- (x - 1) -1) with (-x) by ring. - replace (- (-1 - x) -1) with x by ring. - split ; intros (H1 & H2); auto. + rewrite (Z.sub_opp_l 1). + setoid_rewrite <-lt_le_iff. + rewrite Z.opp_pos_neg. + setoid_rewrite Z.nlt_ge. + split; intros. + { apply Z.le_antisymm; try apply H. } + { subst x. split; reflexivity. } Qed. @@ -103,8 +71,8 @@ Require Import EnvRing. Lemma Zsor : SOR 0 1 Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt. Proof. constructor ; intros ; subst; try reflexivity. - - apply Zsth. - - apply Zth. + - apply InitialRing.Zsth. + - apply InitialRing.Zth. - auto using Z.le_antisymm. - eauto using Z.le_trans. - apply Z.le_neq. @@ -117,17 +85,17 @@ Qed. Lemma ZSORaddon : SORaddon 0 1 Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le (* ring elements *) 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (* coefficients *) - Zeq_bool Z.leb + Z.eqb Z.leb (fun x => x) (fun x => x) (pow_N 1 Z.mul). Proof. constructor. - constructor ; intros ; try reflexivity. - apply Zeq_bool_eq ; auto. + apply Z.eqb_eq ; auto. - constructor. reflexivity. - intros x y. - apply Zeq_bool_neq ; auto. - - apply Zle_bool_imp_le. + rewrite <-Z.eqb_eq. congruence. + - apply Z.leb_le. Qed. Fixpoint Zeval_expr (env : PolEnv Z) (e: PExpr Z) : Z := @@ -166,9 +134,10 @@ Proof. - reflexivity. - simpl. unfold Z.pow_pos. - replace (pow_pos Z.mul r p) with (1 * (pow_pos Z.mul r p)) by ring. + rewrite <-Z.mul_1_l. generalize 1. - induction p as [p IHp|p IHp|]; simpl ; intros ; repeat rewrite IHp ; ring. + induction p as [p IHp|p IHp|]; simpl; intros ; + rewrite ?IHp, ?Z.mul_assoc; auto using Z.mul_comm, f_equal2. Qed. Lemma Zeval_expr_compat : forall env e, Zeval_expr env e = eval_expr env e. @@ -211,7 +180,7 @@ Proof. - apply Z.leb_le. - rewrite Z.geb_le. rewrite Z.ge_le_iff. tauto. - apply Z.ltb_lt. - - rewrite <- Zgt_is_gt_bool; tauto. + - rewrite <- Z.gtb_gt; tauto. Qed. Definition Zeval_op2 (k: Tauto.kind) : Op2 -> Z -> Z -> Tauto.rtyp k:= @@ -281,7 +250,7 @@ Qed. Definition ZWitness := Psatz Z. -Definition ZWeakChecker := check_normalised_formulas 0 1 Z.add Z.mul Zeq_bool Z.leb. +Definition ZWeakChecker := check_normalised_formulas 0 1 Z.add Z.mul Z.eqb Z.leb. Lemma ZWeakChecker_sound : forall (l : list (NFormula Z)) (cm : ZWitness), ZWeakChecker l cm = true -> @@ -295,18 +264,18 @@ Proof. exact H. Qed. -Definition psub := psub Z0 Z.add Z.sub Z.opp Zeq_bool. +Definition psub := psub Z0 Z.add Z.sub Z.opp Z.eqb. Declare Equivalent Keys psub RingMicromega.psub. Definition popp := popp Z.opp. Declare Equivalent Keys popp RingMicromega.popp. -Definition padd := padd Z0 Z.add Zeq_bool. +Definition padd := padd Z0 Z.add Z.eqb. Declare Equivalent Keys padd RingMicromega.padd. -Definition pmul := pmul 0 1 Z.add Z.mul Zeq_bool. +Definition pmul := pmul 0 1 Z.add Z.mul Z.eqb. -Definition normZ := norm 0 1 Z.add Z.mul Z.sub Z.opp Zeq_bool. +Definition normZ := norm 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb. Declare Equivalent Keys normZ RingMicromega.norm. Definition eval_pol := eval_pol Z.add Z.mul (fun x => x). @@ -337,9 +306,9 @@ Proof. apply (eval_pol_norm Zsor ZSORaddon). Qed. -Definition Zunsat := check_inconsistent 0 Zeq_bool Z.leb. +Definition Zunsat := check_inconsistent 0 Z.eqb Z.leb. -Definition Zdeduce := nformula_plus_nformula 0 Z.add Zeq_bool. +Definition Zdeduce := nformula_plus_nformula 0 Z.add Z.eqb. Lemma Zunsat_sound : forall f, Zunsat f = true -> forall env, eval_nformula env f -> False. @@ -382,30 +351,20 @@ Proof. + assert (z0 + (z - z0) = z0 + 0) as H0 by congruence. rewrite Z.add_0_r in H0. rewrite <- H0. - ring. + rewrite Z.add_sub_assoc, Z.add_comm, <-Z.add_sub_assoc, Z.sub_diag; apply Z.add_0_r. + subst. - ring. + apply Z.sub_diag. - split ; intros H H0. - + subst. apply H. ring. + + subst. apply H. apply Z.sub_diag. + apply H. assert (z0 + (z - z0) = z0 + 0) as H1 by congruence. rewrite Z.add_0_r in H1. rewrite <- H1. - ring. - - split ; intros. - + apply Zle_0_minus_le; auto. - + apply Zle_minus_le_0; auto. - - split ; intros. - + apply Zle_0_minus_le; auto. - + apply Zle_minus_le_0; auto. - - split ; intros H. - + apply Zlt_0_minus_lt; auto. - + apply Zlt_left_lt in H. - apply H. - - split ; intros H. - + apply Zlt_0_minus_lt ; auto. - + apply Zlt_left_lt in H. - apply H. + rewrite Z.add_sub_assoc, Z.add_comm, <-Z.add_sub_assoc, Z.sub_diag; apply Z.add_0_r. + - symmetry. apply le_0_iff. + - symmetry. apply le_0_iff. + - apply Z.lt_0_sub. + - apply Z.lt_0_sub. Qed. Definition xnormalise (f: NFormula Z) : list (NFormula Z) := @@ -423,12 +382,6 @@ Proof. reflexivity. Qed. -Ltac iff_ring := - match goal with - | |- ?F 0 ?X <-> ?F 0 ?Y => replace X with Y by ring ; tauto - end. - - Lemma xnormalise_correct : forall env f, (make_conj (fun x => eval_nformula env x -> False) (xnormalise f)) <-> eval_nformula env f. Proof. @@ -438,11 +391,9 @@ Proof. generalize (eval_pol env e) as x; intro. - apply eq_cnf. - unfold not. tauto. - - rewrite le_neg. - iff_ring. - - rewrite le_neg. - rewrite lt_le_iff. - iff_ring. + - rewrite le_neg. rewrite (Z.sub_0_l x), Z.opp_involutive; reflexivity. + - rewrite le_neg, lt_le_iff. + rewrite Z.sub_opp_l, Z.sub_sub_distr. reflexivity. Qed. @@ -854,7 +805,7 @@ Definition genCuttingPlane (f : NFormula Z) : option (PolC Z * Z * Op1) := let (e,op) := f in match op with | Equal => let (g,c) := Zgcd_pol e in - if andb (Z.gtb g Z0) (andb (negb (Zeq_bool c Z0)) (negb (Zeq_bool (Z.gcd g c) g))) + if andb (Z.gtb g Z0) (andb (negb (Z.eqb c Z0)) (negb (Z.eqb (Z.gcd g c) g))) then None (* inconsistent *) else (* Could be optimised Zgcd_pol is recomputed *) let (p,c) := makeCuttingPlane e in @@ -887,7 +838,7 @@ Qed. Definition eval_Psatz : list (NFormula Z) -> ZWitness -> option (NFormula Z) := - eval_Psatz 0 1 Z.add Z.mul Zeq_bool Z.leb. + eval_Psatz 0 1 Z.add Z.mul Z.eqb Z.leb. Definition valid_cut_sign (op:Op1) := @@ -1043,7 +994,7 @@ Qed. Fixpoint max_var_psatz (w : Psatz Z) : positive := match w with | PsatzIn _ n => xH - | PsatzSquare p => max_var xH (Psquare 0 1 Z.add Z.mul Zeq_bool p) + | PsatzSquare p => max_var xH (Psquare 0 1 Z.add Z.mul Z.eqb p) | PsatzMulC p w => Pos.max (max_var xH p) (max_var_psatz w) | PsatzMulE w1 w2 => Pos.max (max_var_psatz w1) (max_var_psatz w2) | PsatzAdd w1 w2 => Pos.max (max_var_psatz w1) (max_var_psatz w2) @@ -1235,7 +1186,7 @@ Proof. - (* Equal *) intros p; destruct p as [[e' z] op]. case_eq (Zgcd_pol e) ; intros g c. - case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))) ; [discriminate|]. + case_eq (Z.gtb g 0 && (negb (Z.eqb c 0) && negb (Z.eqb (Z.gcd g c) g))) ; [discriminate|]. case_eq (makeCuttingPlane e). intros ? ? H H0 H1 H2 H3. inv H3. @@ -1259,17 +1210,14 @@ Proof. * rewrite andb_false_iff in H0. destruct H0 as [H0|H0]. -- rewrite negb_false_iff in H0. - apply Zeq_bool_eq in H0. + apply Z.eqb_eq in H0. subst. simpl. rewrite Z.add_0_r, Z.mul_eq_0 in H2. intuition subst; easy. -- rewrite negb_false_iff in H0. - apply Zeq_bool_eq in H0. - assert (HH := Zgcd_is_gcd g c). - rewrite H0 in HH. - destruct HH as [H3 H4 ?]. - apply Zdivide_opp_r in H4. - rewrite Zdivide_ceiling ; auto. + apply Z.eqb_eq in H0. + rewrite Zdivide_ceiling; cycle 1. + { apply Z.divide_opp_r. rewrite <-H0. apply Z.gcd_divide_r. } apply Z.sub_move_0_r. apply Z.div_unique_exact. ++ now intros ->. @@ -1316,17 +1264,17 @@ Proof. intros env f; destruct f as [p o]. destruct o. - case_eq (Zgcd_pol p) ; intros g c. - case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))). + case_eq (Z.gtb g 0 && (negb (Z.eqb c 0) && negb (Z.eqb (Z.gcd g c) g))). + intros H H0 H1 H2. flatten_bool. match goal with [ H' : (g >? 0) = true |- ?G ] => rename H' into H3 end. - match goal with [ H' : negb (Zeq_bool c 0) = true |- ?G ] => rename H' into H end. - match goal with [ H' : negb (Zeq_bool (Z.gcd g c) g) = true |- ?G ] => rename H' into H5 end. + match goal with [ H' : negb (Z.eqb c 0) = true |- ?G ] => rename H' into H end. + match goal with [ H' : negb (Z.eqb (Z.gcd g c) g) = true |- ?G ] => rename H' into H5 end. rewrite negb_true_iff in H5. - apply Zeq_bool_neq in H5. + apply Z.eqb_neq in H5. rewrite <- Zgt_is_gt_bool in H3. rewrite negb_true_iff in H. - apply Zeq_bool_neq in H. + apply Z.eqb_neq in H. change (eval_pol env p = 0) in H2. rewrite Zgcd_pol_correct_lt with (1:= H0) in H2. 2: auto using Z.gt_lt. set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub p c) g)) in *; clearbody x. @@ -1506,17 +1454,6 @@ Proof. intros b1 b2; destruct b1,b2 ; intuition congruence. Qed. -Ltac pos_tac := - repeat - match goal with - | |- false = _ => symmetry - | |- Pos.eqb ?X ?Y = false => rewrite Pos.eqb_neq ; intro - | H : @eq positive ?X ?Y |- _ => apply Zpos_eq in H - | H : context[Z.pos (Pos.succ ?X)] |- _ => rewrite (Pos2Z.inj_succ X) in H - | H : Pos.leb ?X ?Y = true |- _ => rewrite Pos.leb_le in H ; - apply (Pos2Z.pos_le_pos X Y) in H - end. - Lemma eval_nformula_split : forall env p, eval_nformula env (p,NonStrict) \/ eval_nformula env (popp p,NonStrict). Proof. @@ -1687,14 +1624,9 @@ Proof. exists x0 ; split;tauto. + intros until 1. apply H ; auto. - unfold ltof in *. - simpl in *. - Zify.zify. - intuition subst. - * assumption. - * eapply Z.lt_le_trans. - -- eassumption. - -- apply Z.add_le_mono_r. assumption. + cbv [ltof] in *. + cbn [bdepth] in *. + eauto using Nat.lt_le_trans, le_n_S, Nat.le_max_r. } (*/asser *) destruct (HH _ H1) as [pr [Hin Hcheker]]. @@ -1751,18 +1683,19 @@ Proof. 1:replace (t1=?z1)%positive with false. 1:destruct (env x <=? 0); ring. { unfold t1. - pos_tac; normZ. - lia (Hyp (e := Z.pos z1 - Z.succ (Z.pos z1)) ltac:(assumption)). + symmetry; apply not_true_iff_false; rewrite Pos.eqb_eq; symmetry; apply Pos.succ_discr. } { unfold t1, z1. - pos_tac; normZ. - lia (Add (Hyp LE) (Hyp (e := Z.pos x - Z.succ (Z.succ (Z.pos fr))) ltac:(assumption))). + symmetry; apply not_true_iff_false; rewrite Pos.eqb_eq; intros ->. + apply Pos.leb_le, Pos.lt_succ_r in LE; rewrite <-?Pos.succ_lt_mono in *. + pose proof Pos.lt_not_add_l fr 1; rewrite Pos.add_1_r in *; contradiction. } { unfold z1. - pos_tac; normZ. - lia (Add (Hyp LE) (Hyp (e := Z.pos x - Z.succ (Z.pos fr)) ltac:(assumption))). + symmetry; apply not_true_iff_false; rewrite Pos.eqb_eq; intros ->. + apply Pos.leb_le, Pos.lt_succ_r in LE; rewrite <-?Pos.succ_lt_mono in *. + case (Pos.lt_irrefl _ LE). } * apply eval_nformula_bound_var. @@ -1771,8 +1704,7 @@ Proof. destruct (env x <=? 0) eqn:EQ. -- compute. congruence. -- rewrite Z.leb_gt in EQ. - normZ. - lia (Add (Hyp EQ) (Hyp (e := 0 - (env x + 1)) ltac:(assumption))). + apply Z.ge_le_iff, Z.lt_le_incl; trivial. * apply eval_nformula_bound_var. unfold env'. @@ -1780,13 +1712,11 @@ Proof. replace (t1 =? z1)%positive with false. -- destruct (env x <=? 0) eqn:EQ. ++ rewrite Z.leb_le in EQ. - normZ. - lia (Add (Hyp EQ) (Hyp (e := 0 - (- env x + 1)) ltac:(assumption))). + apply Z.ge_le_iff. rewrite Z.opp_le_mono, Z.opp_involutive; trivial. ++ compute; congruence. -- unfold t1. clear. - pos_tac; normZ. - lia (Hyp (e := Z.pos z1 - Z.succ (Z.pos z1)) ltac:(assumption)). + symmetry; apply not_true_iff_false; rewrite Pos.eqb_eq; symmetry; apply Pos.succ_discr. * rewrite (agree_env_eval_nformulae _ env') in H1;auto. unfold agree_env; intros x0 H2. @@ -1796,16 +1726,15 @@ Proof. 1:reflexivity. { unfold t1, z1. - unfold fr in *. - apply Pos2Z.pos_le_pos in H2. - pos_tac; normZ. - lia (Add (Hyp H2) (Hyp (e := Z.pos x0 - Z.succ (Z.succ (Z.pos (max_var_nformulae l)))) ltac:(assumption))). + symmetry; apply not_true_iff_false; rewrite Pos.eqb_eq; intros ->. + apply Pos.lt_succ_r in H2; rewrite <-?Pos.succ_lt_mono in *. + pose proof Pos.lt_not_add_l (max_var_nformulae l) 1; rewrite Pos.add_1_r in *; contradiction. } { unfold z1, fr in *. - apply Pos2Z.pos_le_pos in H2. - pos_tac; normZ. - lia (Add (Hyp H2) (Hyp (e := Z.pos x0 - Z.succ (Z.pos (max_var_nformulae l))) ltac:(assumption))). + symmetry; apply not_true_iff_false; rewrite Pos.eqb_eq; intros ->. + apply Pos.lt_succ_r in H2; rewrite <-?Pos.succ_lt_mono in *. + case (Pos.lt_irrefl _ H2). } + unfold ltof. simpl. @@ -1875,6 +1804,11 @@ Definition coneMember := ZWitness. Definition eval := eval_formula. +#[deprecated(note="Use [prod positive nat]", since="9.0")] Definition prod_pos_nat := prod positive nat. +#[deprecated(use=Z.to_N, since="9.0")] Notation n_of_Z := Z.to_N (only parsing). + +Local Set Warnings "-deprecated". +Require Ztac. (* deprecated since 9.0 *) diff --git a/stdlib/theories/micromega/Ztac.v b/stdlib/theories/micromega/Ztac.v index ad9653fbddc0..6c19a04ce1f1 100644 --- a/stdlib/theories/micromega/Ztac.v +++ b/stdlib/theories/micromega/Ztac.v @@ -8,6 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +Attributes deprecated(since="9.0", note="use lia instead"). +Local Set Warnings "-deprecated". + (** Tactics for doing arithmetic proofs. Useful to bootstrap lia. *) @@ -16,48 +19,31 @@ Require Import ZArithRing. Require Import ZArith_base. Local Open Scope Z_scope. +#[deprecated(use=Z.eq_le_incl, since="9.0")] Lemma eq_incl : forall (x y:Z), x = y -> x <= y /\ y <= x. -Proof. - intros; split; - apply Z.eq_le_incl; auto. -Qed. +Proof. split; apply Z.eq_le_incl; auto 1 using eq_sym. Qed. +#[deprecated(use=Z.lt_trichotomy, since="9.0")] Lemma elim_concl_eq : forall x y, (x < y \/ y < x -> False) -> x = y. -Proof. - intros x y H. - destruct (Z_lt_le_dec x y). - - exfalso. apply H ; auto. - - destruct (Zle_lt_or_eq y x);auto. - exfalso. - apply H ; auto. -Qed. +Proof. intros; pose proof Z.lt_trichotomy x y; intuition idtac. Qed. +#[deprecated(use=Z.nlt_ge, since="9.0")] Lemma elim_concl_le : forall x y, (y < x -> False) -> x <= y. -Proof. - intros x y H. - destruct (Z_lt_le_dec y x). - - exfalso ; auto. - - auto. -Qed. +Proof. intros *. apply Z.nlt_ge. Qed. +#[deprecated(use=Z.nle_gt, since="9.0")] Lemma elim_concl_lt : forall x y, (y <= x -> False) -> x < y. -Proof. - intros x y H. - destruct (Z_lt_le_dec x y). - - auto. - - exfalso ; auto. -Qed. - - +Proof. intros *. apply Z.nle_gt. Qed. +#[deprecated(use=Z.le_succ_l, since="9.0")] Lemma Zlt_le_add_1 : forall n m : Z, n < m -> n + 1 <= m. -Proof. exact (Zlt_le_succ). Qed. - +Proof. apply Z.le_succ_l. Qed. +#[deprecated(since="9.0")] Ltac normZ := repeat match goal with @@ -77,27 +63,33 @@ Ltac normZ := end. -Inductive proof := -| Hyp (e : Z) (prf : 0 <= e) -| Add (p1 p2: proof) -| Mul (p1 p2: proof) -| Cst (c : Z) +Inductive proof_deprecated := +| Hyp_deprecated (e : Z) (prf : 0 <= e) +| Add_deprecated (p1 p2: proof_deprecated) +| Mul_deprecated (p1 p2: proof_deprecated) +| Cst_deprecated (c : Z) . +#[deprecated(since="9.0")] +Notation proof := proof_deprecated (only parsing). +#[deprecated(since="9.0")] +Notation Hyp := Hyp_deprecated (only parsing). +#[deprecated(since="9.0")] +Notation Add := Add_deprecated (only parsing). +#[deprecated(since="9.0")] +Notation Mul := Mul_deprecated (only parsing). +#[deprecated(since="9.0")] +Notation Cst := Cst_deprecated (only parsing). + +#[deprecated(use=Z.add_nonneg_nonneg, since="9.0")] Lemma add_le : forall e1 e2, 0 <= e1 -> 0 <= e2 -> 0 <= e1+e2. -Proof. - intros. - change 0 with (0+ 0). - apply Z.add_le_mono; auto. -Qed. +Proof. apply Z.add_nonneg_nonneg. Qed. +#[deprecated(use=Z.mul_nonneg_nonneg, since="9.0")] Lemma mul_le : forall e1 e2, 0 <= e1 -> 0 <= e2 -> 0 <= e1*e2. -Proof. - intros e1 e2 H H0. - change 0 with (0* e2). - apply Zmult_le_compat_r; auto. -Qed. +Proof. apply Z.mul_nonneg_nonneg. Qed. +#[deprecated(since="9.0")] Fixpoint eval_proof (p : proof) : { e : Z | 0 <= e} := match p with | Hyp e prf => exist _ e prf @@ -113,6 +105,7 @@ Fixpoint eval_proof (p : proof) : { e : Z | 0 <= e} := end end. +#[deprecated(since="9.0")] Ltac lia_step p := let H := fresh in let prf := (eval cbn - [Z.le Z.mul Z.opp Z.sub Z.add] in (eval_proof p)) in @@ -120,6 +113,7 @@ Ltac lia_step p := | @exist _ _ _ ?P => pose proof P as H end ; ring_simplify in H. +#[deprecated(since="9.0")] Ltac lia_contr := match goal with | H : 0 <= - (Zpos _) |- _ => @@ -131,9 +125,11 @@ Ltac lia_contr := end. +#[deprecated(since="9.0")] Ltac lia p := lia_step p ; lia_contr. +#[deprecated(since="9.0")] Ltac slia H1 H2 := normZ ; lia (Add (Hyp _ H1) (Hyp _ H2)). From beeb71a7ef078d490b97655332c3a5092ef649b4 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 31 Oct 2024 14:05:46 +0000 Subject: [PATCH 2/5] ZArithRing without ZArith_base --- stdlib/theories/Lists/ListTactics.v | 2 +- stdlib/theories/Reals/RIneq.v | 9 ++++++--- stdlib/theories/micromega/RingMicromega.v | 5 +++-- stdlib/theories/micromega/ZCoeff.v | 4 ++-- stdlib/theories/micromega/ZifyInst.v | 2 +- stdlib/theories/micromega/Ztac.v | 22 ++++++++++++++++------ stdlib/theories/nsatz/NsatzTactic.v | 8 ++++---- stdlib/theories/setoid_ring/Field_theory.v | 12 ++++++------ stdlib/theories/setoid_ring/InitialRing.v | 17 ++++++----------- stdlib/theories/setoid_ring/RealField.v | 2 +- stdlib/theories/setoid_ring/Ring_tac.v | 3 --- stdlib/theories/setoid_ring/ZArithRing.v | 7 +++++-- 12 files changed, 51 insertions(+), 42 deletions(-) diff --git a/stdlib/theories/Lists/ListTactics.v b/stdlib/theories/Lists/ListTactics.v index f0fec83ba1dd..ddc311e69f7f 100644 --- a/stdlib/theories/Lists/ListTactics.v +++ b/stdlib/theories/Lists/ListTactics.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import BinPos. +Require Import BinPosDef. Require Import List. Ltac list_fold_right fcons fnil l := diff --git a/stdlib/theories/Reals/RIneq.v b/stdlib/theories/Reals/RIneq.v index 5b6eeac3a231..1a986958b0a0 100644 --- a/stdlib/theories/Reals/RIneq.v +++ b/stdlib/theories/Reals/RIneq.v @@ -2672,22 +2672,25 @@ Qed. Lemma R_rm : ring_morph 0%R 1%R Rplus Rmult Rminus Ropp eq - 0%Z 1%Z Zplus Zmult Zminus Z.opp Zeq_bool IZR. + 0%Z 1%Z Zplus Zmult Zminus Z.opp Z.eqb IZR. Proof. constructor; try easy. - exact plus_IZR. - exact minus_IZR. - exact mult_IZR. - exact opp_IZR. - - now intros x y H; f_equal; apply Zeq_bool_eq. + - now intros x y H; f_equal; apply Z.eqb_eq. Qed. (* NOTE: keeping inconsistent variable names for backward compatibility. *) Lemma Zeq_bool_IZR : forall x y:Z, IZR x = IZR y -> Zeq_bool x y = true. Proof. now intros n m H; apply Zeq_is_eq_bool, eq_IZR. Qed. +Local Lemma Private_Zeqb_IZR : forall x y:Z, IZR x = IZR y -> Z.eqb x y = true. +Proof. intros. apply Z.eqb_eq, eq_IZR; trivial. Qed. + Add Field RField : Rfield - (completeness Zeq_bool_IZR, morphism R_rm, constants [IZR_tac], power_tac R_power_theory [Rpow_tac]). + (completeness Private_Zeqb_IZR, morphism R_rm, constants [IZR_tac], power_tac R_power_theory [Rpow_tac]). (*********************************************************) (** * Definitions of new types *) diff --git a/stdlib/theories/micromega/RingMicromega.v b/stdlib/theories/micromega/RingMicromega.v index efb2da0d7ee5..81bffebb5bc0 100644 --- a/stdlib/theories/micromega/RingMicromega.v +++ b/stdlib/theories/micromega/RingMicromega.v @@ -10,6 +10,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) +Require Import PeanoNat. Require Import NArith. Require Import Relation_Definitions. Require Import Setoid. @@ -499,8 +500,8 @@ Lemma ge_bool_cases : forall n m, (if ge_bool n m then n >= m else n < m)%nat. Proof. intros n; induction n as [|n IHn]; - intros m; destruct m as [|m]; simpl; auto with arith. - specialize (IHn m). destruct (ge_bool); auto with arith. + intros m; destruct m as [|m]; simpl; auto using Nat.le_add_r, Nat.le_0_l. + specialize (IHn m). destruct (ge_bool); auto using le_n_S. Qed. diff --git a/stdlib/theories/micromega/ZCoeff.v b/stdlib/theories/micromega/ZCoeff.v index 20ec0d138755..d1f4a2e04c5a 100644 --- a/stdlib/theories/micromega/ZCoeff.v +++ b/stdlib/theories/micromega/ZCoeff.v @@ -114,7 +114,7 @@ Qed. Lemma Zring_morph : ring_morph 0 1 rplus rtimes rminus ropp req 0%Z 1%Z Z.add Z.mul Z.sub Z.opp - Zeq_bool gen_order_phi_Z. + Z.eqb gen_order_phi_Z. Proof. exact (gen_phiZ_morph (SORsetoid sor) ring_ops_wd (SORrt sor)). Qed. @@ -159,7 +159,7 @@ Lemma Zcleb_morph : forall x y : Z, Z.leb x y = true -> [x] <= [y]. Proof. unfold Z.leb; intros x y H. case_eq (x ?= y)%Z; intro H1; rewrite H1 in H. -- le_equal. apply (morph_eq Zring_morph). unfold Zeq_bool; now rewrite H1. +- le_equal. apply (morph_eq Zring_morph). apply Z.eqb_eq; auto using Z.compare_eq. - le_less. now apply clt_morph. - discriminate. Qed. diff --git a/stdlib/theories/micromega/ZifyInst.v b/stdlib/theories/micromega/ZifyInst.v index d1561b3f60e9..8f892ed2eeef 100644 --- a/stdlib/theories/micromega/ZifyInst.v +++ b/stdlib/theories/micromega/ZifyInst.v @@ -12,7 +12,7 @@ Each instance is registered using a Add 'class' 'name_of_instance'. *) -Require Import Arith BinInt BinNat Znat Nnat. +Require Import Arith BinInt BinNat Zeven Znat Nnat. Require Import ZifyClasses. Declare ML Module "rocq-runtime.plugins.zify". Local Open Scope Z_scope. diff --git a/stdlib/theories/micromega/Ztac.v b/stdlib/theories/micromega/Ztac.v index 6c19a04ce1f1..b8d73b4b6e52 100644 --- a/stdlib/theories/micromega/Ztac.v +++ b/stdlib/theories/micromega/Ztac.v @@ -15,8 +15,8 @@ Local Set Warnings "-deprecated". Useful to bootstrap lia. *) -Require Import ZArithRing. -Require Import ZArith_base. +Require Import BinInt. +Require Import (ltac.notations) Ring_tac. Local Open Scope Z_scope. #[deprecated(use=Z.eq_le_incl, since="9.0")] @@ -43,6 +43,12 @@ Proof. intros *. apply Z.nle_gt. Qed. Lemma Zlt_le_add_1 : forall n m : Z, n < m -> n + 1 <= m. Proof. apply Z.le_succ_l. Qed. +#[deprecated(since="9.0")] +Local Lemma Private_Zle_minus_le_0 n m : m <= n -> 0 <= n - m. +Proof. + apply Z.le_0_sub. +Qed. + #[deprecated(since="9.0")] Ltac normZ := repeat @@ -51,7 +57,7 @@ Ltac normZ := | H : ?Y <= _ |- _ => lazymatch Y with | 0 => fail - | _ => apply Zle_minus_le_0 in H + | _ => apply Private_Zle_minus_le_0 in H end | H : _ >= _ |- _ => apply Z.ge_le in H | H : _ > _ |- _ => apply Z.gt_lt in H @@ -62,7 +68,6 @@ Ltac normZ := | |- _ >= _ => apply Z.le_ge end. - Inductive proof_deprecated := | Hyp_deprecated (e : Z) (prf : 0 <= e) | Add_deprecated (p1 p2: proof_deprecated) @@ -89,6 +94,12 @@ Proof. apply Z.add_nonneg_nonneg. Qed. Lemma mul_le : forall e1 e2, 0 <= e1 -> 0 <= e2 -> 0 <= e1*e2. Proof. apply Z.mul_nonneg_nonneg. Qed. +#[deprecated(since="9.0")] +Local Definition Private_Z_le_dec x y : {x <= y} + {~ x <= y}. +Proof. + unfold Z.le; case Z.compare; (now left) || (right; tauto). +Defined. + #[deprecated(since="9.0")] Fixpoint eval_proof (p : proof) : { e : Z | 0 <= e} := match p with @@ -99,7 +110,7 @@ Fixpoint eval_proof (p : proof) : { e : Z | 0 <= e} := | Mul p1 p2 => let (e1,p1) := eval_proof p1 in let (e2,p2) := eval_proof p2 in exist _ _ (mul_le _ _ p1 p2) - | Cst c => match Z_le_dec 0 c with + | Cst c => match Private_Z_le_dec 0 c with | left prf => exist _ _ prf | _ => exist _ _ Z.le_0_1 end @@ -124,7 +135,6 @@ Ltac lia_contr := compute in H ; discriminate end. - #[deprecated(since="9.0")] Ltac lia p := lia_step p ; lia_contr. diff --git a/stdlib/theories/nsatz/NsatzTactic.v b/stdlib/theories/nsatz/NsatzTactic.v index 176f674da4e9..ebf01357bd67 100644 --- a/stdlib/theories/nsatz/NsatzTactic.v +++ b/stdlib/theories/nsatz/NsatzTactic.v @@ -70,15 +70,15 @@ Definition PEZ := PExpr Z. Definition P0Z : PolZ := P0 (C:=Z) 0%Z. Definition PolZadd : PolZ -> PolZ -> PolZ := - @Padd Z 0%Z Z.add Zeq_bool. + @Padd Z 0%Z Z.add Z.eqb. Definition PolZmul : PolZ -> PolZ -> PolZ := - @Pmul Z 0%Z 1%Z Z.add Z.mul Zeq_bool. + @Pmul Z 0%Z 1%Z Z.add Z.mul Z.eqb. -Definition PolZeq := @Peq Z Zeq_bool. +Definition PolZeq := @Peq Z Z.eqb. Definition norm := - @norm_aux Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool. + @norm_aux Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb. Fixpoint mult_l (la : list PEZ) (lp: list PolZ) : PolZ := match la, lp with diff --git a/stdlib/theories/setoid_ring/Field_theory.v b/stdlib/theories/setoid_ring/Field_theory.v index 22db1a87a809..df708bc2a149 100644 --- a/stdlib/theories/setoid_ring/Field_theory.v +++ b/stdlib/theories/setoid_ring/Field_theory.v @@ -10,7 +10,7 @@ Require Ring. Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List Morphisms. -Require Import ZArith_base. +Require Import BinNat BinInt. Set Implicit Arguments. (* Set Universe Polymorphism. *) @@ -915,7 +915,8 @@ induction e2 as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe2_1 ? IHe2_2|? IHe|? IH destruct isIn as [([|p'],e')|]. * destruct IHe2_1 as (IH1,GT1). destruct IHe2_2 as (IH2,GT2). - split; [|simpl; apply Zgt_trans with (Z.pos p); trivial]. + split; cycle 1. + { rewrite Z.gt_lt_iff in *; eauto 1 using Z.lt_trans. } npe_simpl. rewrite IH1, IH2. simpl. simpl_pos_sub. simpl. replace (N.pos p1) with (N.pos p + N.pos (p1 - p))%N. { rewrite PEpow_add_r; npe_ring. } @@ -925,7 +926,7 @@ induction e2 as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe2_1 ? IHe2_2|? IHe|? IH } * destruct IHe2_1 as (IH1,GT1). destruct IHe2_2 as (IH2,GT2). - assert (Z.pos p1 > Z.pos p')%Z by (now apply Zgt_trans with (Zpos p)). + assert (Z.pos p1 > Z.pos p')%Z by (rewrite Z.gt_lt_iff in *; eauto 2 using Z.lt_trans). split; [|simpl; trivial]. npe_simpl. rewrite IH1, IH2. simpl. simpl_pos_sub. simpl. replace (N.pos (p1 - p')) with (N.pos (p1 - p) + N.pos (p - p'))%N. @@ -1813,12 +1814,11 @@ Qed. Lemma gen_phiZ_complete x y : gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y -> - Zeq_bool x y = true. + Z.eqb x y = true. Proof. intros. replace y with x. -- unfold Zeq_bool. - rewrite Z.compare_refl; trivial. +- apply Z.eqb_refl. - apply gen_phiZ_inj; trivial. Qed. diff --git a/stdlib/theories/setoid_ring/InitialRing.v b/stdlib/theories/setoid_ring/InitialRing.v index aa0eb7358ed1..61f047550c41 100644 --- a/stdlib/theories/setoid_ring/InitialRing.v +++ b/stdlib/theories/setoid_ring/InitialRing.v @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Zbool. Require Import BinInt. Require Import BinNat. Require Import Setoid. @@ -108,12 +107,12 @@ Section ZMORPHISM. | _ => None end. - Lemma get_signZ_th : sign_theory Z.opp Zeq_bool get_signZ. + Lemma get_signZ_th : sign_theory Z.opp Z.eqb get_signZ. Proof. constructor. intros c;destruct c;intros ? H;try discriminate. injection H as [= <-]. - simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial. + simpl. apply Pos.eqb_refl. Qed. @@ -181,12 +180,8 @@ Section ZMORPHISM. Qed. Lemma gen_Zeqb_ok : forall x y, - Zeq_bool x y = true -> [x] == [y]. - Proof. - intros x y H. - assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1. - rewrite H1;rrefl. - Qed. + Z.eqb x y = true -> [x] == [y]. + Proof. intros x y ->%Z.eqb_eq; reflexivity. Qed. Lemma gen_phiZ1_pos_sub : forall x y, gen_phiZ1 (Z.pos_sub x y) == gen_phiPOS1 x + -gen_phiPOS1 y. @@ -227,10 +222,10 @@ Section ZMORPHISM. (*proof that [.] satisfies morphism specifications*) Lemma gen_phiZ_morph : ring_morph 0 1 radd rmul rsub ropp req Z0 (Zpos xH) - Z.add Z.mul Z.sub Z.opp Zeq_bool gen_phiZ. + Z.add Z.mul Z.sub Z.opp Z.eqb gen_phiZ. Proof. assert ( SRmorph : semi_morph 0 1 radd rmul req Z0 (Zpos xH) - Z.add Z.mul Zeq_bool gen_phiZ). + Z.add Z.mul Z.eqb gen_phiZ). - apply mkRmorph;simpl;try rrefl. + apply gen_phiZ_add. + apply gen_phiZ_mul. diff --git a/stdlib/theories/setoid_ring/RealField.v b/stdlib/theories/setoid_ring/RealField.v index d5d9d9f87ae5..492db8c87bd7 100644 --- a/stdlib/theories/setoid_ring/RealField.v +++ b/stdlib/theories/setoid_ring/RealField.v @@ -113,7 +113,7 @@ Qed. Lemma Zeq_bool_complete : forall x y, InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp x = InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp y -> - Zeq_bool x y = true. + Z.eqb x y = true. Proof gen_phiZ_complete Rset Rext Rfield Rgen_phiPOS_not_0. Lemma Rdef_pow_add : forall (x:R) (n m:nat), pow x (n + m) = pow x n * pow x m. diff --git a/stdlib/theories/setoid_ring/Ring_tac.v b/stdlib/theories/setoid_ring/Ring_tac.v index 605e901d3720..577cf7e72df4 100644 --- a/stdlib/theories/setoid_ring/Ring_tac.v +++ b/stdlib/theories/setoid_ring/Ring_tac.v @@ -9,10 +9,7 @@ (************************************************************************) Set Implicit Arguments. -Require Import Setoid. -Require Import BinPos. Require Import Ring_polynom. -Require Import BinList. Require Export ListTactics. Require Import InitialRing. Declare ML Module "rocq-runtime.plugins.ring". diff --git a/stdlib/theories/setoid_ring/ZArithRing.v b/stdlib/theories/setoid_ring/ZArithRing.v index f22bee34054f..9aea3ff172ca 100644 --- a/stdlib/theories/setoid_ring/ZArithRing.v +++ b/stdlib/theories/setoid_ring/ZArithRing.v @@ -9,7 +9,7 @@ (************************************************************************) Require Export Ring. -Require Import ZArith_base. +Require Import BinInt. Require Import Zpow_def. Import InitialRing. @@ -47,8 +47,11 @@ Ltac Zpower_neg := end end. +Local Lemma Private_proj1_eqb_eq x y : Z.eqb x y = true -> x = y. +Proof. apply Z.eqb_eq. Qed. + Add Ring Zr : Zth - (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Z.succ], + (decidable Private_proj1_eqb_eq, constants [Zcst], preprocess [Zpower_neg;unfold Z.succ], power_tac Zpower_theory [Zpow_tac], (* The following two options are not needed; they are the default choice when the set of coefficient is the usual ring Z *) From 7e7d354b49e48d05626cc3cb431b2914403b19ff Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 2 Nov 2024 20:19:09 +0000 Subject: [PATCH 3/5] deprecate ZArith_base and Zeq_bool --- stdlib/theories/Floats/FloatLemmas.v | 3 +- stdlib/theories/Numbers/DecimalQ.v | 1 + stdlib/theories/Numbers/DecimalR.v | 1 + stdlib/theories/Numbers/HexadecimalQ.v | 1 + stdlib/theories/Numbers/HexadecimalR.v | 1 + stdlib/theories/QArith/QArith_base.v | 43 ++++---- stdlib/theories/QArith/Qpower.v | 4 +- .../theories/Reals/Abstract/ConstructiveLUB.v | 2 +- .../Reals/Abstract/ConstructiveLimits.v | 2 +- .../Reals/Abstract/ConstructivePower.v | 1 + .../Reals/Abstract/ConstructiveReals.v | 2 +- .../Abstract/ConstructiveRealsMorphisms.v | 1 + .../theories/Reals/Abstract/ConstructiveSum.v | 1 + stdlib/theories/Reals/Alembert.v | 1 + stdlib/theories/Reals/AltSeries.v | 1 + stdlib/theories/Reals/ArithProp.v | 1 + stdlib/theories/Reals/Binomial.v | 1 + .../Cauchy/ConstructiveCauchyRealsMult.v | 2 + .../Reals/Cauchy/ConstructiveRcomplete.v | 8 +- stdlib/theories/Reals/Cauchy/QExtra.v | 3 +- .../Reals/ClassicalConstructiveReals.v | 1 + .../theories/Reals/ClassicalDedekindReals.v | 2 + stdlib/theories/Reals/Cos_plus.v | 1 + stdlib/theories/Reals/Cos_rel.v | 1 + stdlib/theories/Reals/DiscrR.v | 2 +- stdlib/theories/Reals/Exp_prop.v | 1 + stdlib/theories/Reals/PartSum.v | 2 + stdlib/theories/Reals/RIneq.v | 9 +- stdlib/theories/Reals/RList.v | 1 + stdlib/theories/Reals/Ratan.v | 1 + stdlib/theories/Reals/Raxioms.v | 3 +- stdlib/theories/Reals/Rdefinitions.v | 3 +- stdlib/theories/Reals/Rfunctions.v | 2 + stdlib/theories/Reals/RiemannInt_SF.v | 1 + stdlib/theories/Reals/Rlogic.v | 3 + stdlib/theories/Reals/Rpower.v | 1 + stdlib/theories/Reals/Rprod.v | 2 + stdlib/theories/Reals/Rtrigo.v | 2 +- stdlib/theories/Reals/Rtrigo1.v | 4 +- stdlib/theories/Reals/Rtrigo_alt.v | 1 + stdlib/theories/Reals/Rtrigo_def.v | 1 + stdlib/theories/Reals/Rtrigo_fun.v | 1 + stdlib/theories/Reals/Rtrigo_reg.v | 1 + stdlib/theories/Reals/SeqProp.v | 1 + stdlib/theories/Reals/SeqSeries.v | 1 + stdlib/theories/Structures/OrderedTypeEx.v | 2 +- stdlib/theories/ZArith/ZArith.v | 25 ++++- stdlib/theories/ZArith/ZArith_base.v | 4 +- stdlib/theories/ZArith/Zbool.v | 100 ++++++++++-------- stdlib/theories/ZArith/Zcomplements.v | 46 ++++---- stdlib/theories/ZArith/Zdiv.v | 28 ++--- stdlib/theories/ZArith/Zgcd_alt.v | 3 +- stdlib/theories/ZArith/Znumtheory.v | 1 + stdlib/theories/ZArith/Zpow_facts.v | 4 +- stdlib/theories/ZArith/Zpower.v | 6 +- stdlib/theories/ZArith/Zquot.v | 7 +- stdlib/theories/ZArith/Zwf.v | 2 +- stdlib/theories/micromega/RMicromega.v | 13 ++- stdlib/theories/micromega/VarMap.v | 2 +- stdlib/theories/micromega/ZArith_hints.v | 2 +- stdlib/theories/micromega/ZCoeff.v | 10 +- stdlib/theories/micromega/ZMicromega.v | 26 ++--- stdlib/theories/setoid_ring/Cring.v | 22 ++-- stdlib/theories/setoid_ring/Integral_domain.v | 2 +- stdlib/theories/setoid_ring/Ncring.v | 2 +- stdlib/theories/setoid_ring/Ncring_initial.v | 17 ++- stdlib/theories/setoid_ring/Ncring_tac.v | 13 ++- stdlib/theories/setoid_ring/RealField.v | 2 + stdlib/theories/setoid_ring/Ring_base.v | 2 +- 69 files changed, 276 insertions(+), 193 deletions(-) diff --git a/stdlib/theories/Floats/FloatLemmas.v b/stdlib/theories/Floats/FloatLemmas.v index 713dc7143261..ae8149b10a2b 100644 --- a/stdlib/theories/Floats/FloatLemmas.v +++ b/stdlib/theories/Floats/FloatLemmas.v @@ -55,8 +55,7 @@ Proof. rewrite Bool.andb_true_iff. intro H'. destruct H' as (H1,H2). - rewrite Z.eqb_compare in H1. - apply Zeq_bool_eq in H1. + apply Z.eqb_eq in H1. apply Z.max_case_strong. 1:apply Z.min_case_strong. - reflexivity. diff --git a/stdlib/theories/Numbers/DecimalQ.v b/stdlib/theories/Numbers/DecimalQ.v index f67b3b965799..bc9f0b1b2dab 100644 --- a/stdlib/theories/Numbers/DecimalQ.v +++ b/stdlib/theories/Numbers/DecimalQ.v @@ -14,6 +14,7 @@ are bijections. *) Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith. +Import PeanoNat. Lemma of_IQmake_to_decimal num den : match IQmake_to_decimal num den with diff --git a/stdlib/theories/Numbers/DecimalR.v b/stdlib/theories/Numbers/DecimalR.v index 34d4c637c16f..e34c3efaeef4 100644 --- a/stdlib/theories/Numbers/DecimalR.v +++ b/stdlib/theories/Numbers/DecimalR.v @@ -14,6 +14,7 @@ are bijections. *) Require Import Decimal DecimalFacts DecimalPos DecimalZ DecimalQ Rdefinitions. +Require Import PeanoNat. Lemma of_IQmake_to_decimal num den : match IQmake_to_decimal num den with diff --git a/stdlib/theories/Numbers/HexadecimalQ.v b/stdlib/theories/Numbers/HexadecimalQ.v index f450c8b0849c..7c57fb8f21f9 100644 --- a/stdlib/theories/Numbers/HexadecimalQ.v +++ b/stdlib/theories/Numbers/HexadecimalQ.v @@ -15,6 +15,7 @@ Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ. Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN HexadecimalZ QArith. +Import PeanoNat. Lemma of_IQmake_to_hexadecimal num den : match IQmake_to_hexadecimal num den with diff --git a/stdlib/theories/Numbers/HexadecimalR.v b/stdlib/theories/Numbers/HexadecimalR.v index 961067c1dcb6..8293e848a1a5 100644 --- a/stdlib/theories/Numbers/HexadecimalR.v +++ b/stdlib/theories/Numbers/HexadecimalR.v @@ -13,6 +13,7 @@ Proofs that conversions between hexadecimal numbers and [R] are bijections. *) +Require Import PeanoNat. Require Import Decimal DecimalFacts. Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalZ. Require Import HexadecimalQ Rdefinitions. diff --git a/stdlib/theories/QArith/QArith_base.v b/stdlib/theories/QArith/QArith_base.v index e5de73a126c5..82ba82c101e1 100644 --- a/stdlib/theories/QArith/QArith_base.v +++ b/stdlib/theories/QArith/QArith_base.v @@ -8,11 +8,14 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Export ZArith_base. +Require Export BinInt. Require Export ZArithRing. Require Export ZArith.BinInt. Require Export Morphisms Setoid Bool. +Require ZArith.Zcompare. +Require ZArith_dec. + (** * Definition of [Q] and basic properties *) (** Rationals are pairs of [Z] and [positive] numbers. *) @@ -175,15 +178,13 @@ Proof. Defined. Definition Qeq_bool x y := - (Zeq_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z. + (Z.eqb (Qnum x * QDen y) (Qnum y * QDen x))%Z. Definition Qle_bool x y := (Z.leb (Qnum x * QDen y) (Qnum y * QDen x))%Z. Lemma Qeq_bool_iff x y : Qeq_bool x y = true <-> x == y. -Proof. - symmetry; apply Zeq_is_eq_bool. -Qed. +Proof. apply Z.eqb_eq. Qed. Lemma Qeq_bool_eq x y : Qeq_bool x y = true -> x == y. Proof. @@ -201,9 +202,7 @@ Proof. Qed. Lemma Qle_bool_iff x y : Qle_bool x y = true <-> x <= y. -Proof. - symmetry; apply Zle_is_le_bool. -Qed. +Proof. apply Z.leb_le. Qed. Lemma Qle_bool_imp_le x y : Qle_bool x y = true -> x <= y. Proof. @@ -540,8 +539,8 @@ Proof. unfold Qeq, Qcompare. Open Scope Z_scope. intros (p1,p2) (q1,q2) H (r1,r2) (s1,s2) H'; simpl in *. - rewrite <- (Zcompare_mult_compat (q2*s2) (p1*Zpos r2)). - rewrite <- (Zcompare_mult_compat (p2*r2) (q1*Zpos s2)). + rewrite <- (Zcompare.Zcompare_mult_compat (q2*s2) (p1*Zpos r2)). + rewrite <- (Zcompare.Zcompare_mult_compat (p2*r2) (q1*Zpos s2)). change (Zpos (q2*s2)) with (Zpos q2 * Zpos s2). change (Zpos (p2*r2)) with (Zpos p2 * Zpos r2). replace (Zpos q2 * Zpos s2 * (p1*Zpos r2)) with ((p1*Zpos q2)*Zpos r2*Zpos s2) by ring. @@ -937,7 +936,7 @@ Qed. Lemma Qle_refl x : x<=x. Proof. - unfold Qle; auto with zarith. + unfold Qle; reflexivity. Qed. Lemma Qle_antisym x y : x<=y -> y<=x -> x==y. @@ -1076,13 +1075,13 @@ Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le Lemma Q_dec : forall x y, {x ring_simplify z1 t1 (Zpos z2) (Zpos t2) a b end. - auto with zarith. + auto using Z.mul_le_mono_nonneg_r, Pos2Z.is_nonneg. - match goal with |- ?a <= ?b => ring_simplify x1 y1 (Zpos x2) (Zpos y2) a b end. - auto with zarith. + auto using Z.mul_le_mono_nonneg_r, Pos2Z.is_nonneg. Close Scope Z_scope. Qed. @@ -1166,7 +1159,7 @@ Proof. rewrite Z.add_comm. apply Z.add_le_lt_mono. - match goal with |- ?a <= ?b => ring_simplify z1 t1 (Zpos z2) (Zpos t2) a b end. - auto with zarith. + auto using Z.mul_le_mono_nonneg_r, Pos2Z.is_nonneg. - match goal with |- ?a < ?b => ring_simplify x1 y1 (Zpos x2) (Zpos y2) a b end. do 2 (apply Z.mul_lt_mono_pos_r;try easy). Close Scope Z_scope. @@ -1289,7 +1282,7 @@ intros a b Ha Hb. unfold Qle in *. simpl in *. rewrite Z.mul_1_r in *. -auto with *. +auto using Z.mul_nonneg_nonneg. Qed. Lemma Qmult_lt_0_compat : forall a b : Q, 0 < a -> 0 < b -> 0 < a * b. @@ -1345,7 +1338,7 @@ Proof. do 2 rewrite Pos2Z.inj_mul. setoid_replace (xn * zn * (Z.pos yd * Z.pos td))%Z with ((xn * Z.pos yd) * (zn * Z.pos td))%Z by ring. setoid_replace (yn * tn * (Z.pos xd * Z.pos zd))%Z with ((yn * Z.pos xd) * (tn * Z.pos zd))%Z by ring. - apply Zmult_lt_compat2; split. + apply Zorder.Zmult_lt_compat2; split. 2,4 : assumption. 1,2 : rewrite <- (Z.mul_0_l 0); apply Z.mul_lt_mono_nonneg; [reflexivity|assumption|reflexivity|apply Pos2Z.is_pos]. diff --git a/stdlib/theories/QArith/Qpower.v b/stdlib/theories/QArith/Qpower.v index 6f7260b8dfae..5f2bc55eece3 100644 --- a/stdlib/theories/QArith/Qpower.v +++ b/stdlib/theories/QArith/Qpower.v @@ -410,7 +410,7 @@ Lemma Qpower_lt_compat_l_inv: forall (q : Q) (n m : Z), (q ^ n < q ^ m)%Q -> (1 (n < m)%Z. Proof. intros q n m Hnm Hq. - destruct (Z_lt_le_dec n m) as [Hd|Hd]. + destruct (Z.ltb_spec n m) as [Hd|Hd]. - assumption. - pose proof Qpower_le_compat_l q m n Hd (Qlt_le_weak _ _ Hq) as Hnm'. pose proof Qlt_le_trans _ _ _ Hnm Hnm' as Habsurd. @@ -421,7 +421,7 @@ Lemma Qpower_le_compat_l_inv: forall (q : Q) (n m : Z), (q ^ n <= q ^ m)%Q -> (1 (n <= m)%Z. Proof. intros q n m Hnm Hq. - destruct (Z_lt_le_dec m n) as [Hd|Hd]. + destruct (Z.ltb_spec m n) as [Hd|Hd]. - pose proof Qpower_lt_compat_l q m n Hd Hq as Hnm'. pose proof Qle_lt_trans _ _ _ Hnm Hnm' as Habsurd. destruct (Qlt_irrefl _ Habsurd). diff --git a/stdlib/theories/Reals/Abstract/ConstructiveLUB.v b/stdlib/theories/Reals/Abstract/ConstructiveLUB.v index 0d8597e27524..c3126b4fdb44 100644 --- a/stdlib/theories/Reals/Abstract/ConstructiveLUB.v +++ b/stdlib/theories/Reals/Abstract/ConstructiveLUB.v @@ -16,7 +16,7 @@ WARNING: this file is experimental and likely to change in future releases. *) -Require Import QArith_base Qabs. +Require Import Znat QArith_base Qabs. Require Import ConstructiveReals. Require Import ConstructiveAbs. Require Import ConstructiveLimits. diff --git a/stdlib/theories/Reals/Abstract/ConstructiveLimits.v b/stdlib/theories/Reals/Abstract/ConstructiveLimits.v index 0a526fc61f8b..8a90c73ca4a4 100644 --- a/stdlib/theories/Reals/Abstract/ConstructiveLimits.v +++ b/stdlib/theories/Reals/Abstract/ConstructiveLimits.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import QArith Qabs. +Require Import PeanoNat QArith Qabs. Require Import ConstructiveReals. Require Import ConstructiveAbs. diff --git a/stdlib/theories/Reals/Abstract/ConstructivePower.v b/stdlib/theories/Reals/Abstract/ConstructivePower.v index 9bca72b6fc8b..0b9ce492a5dd 100644 --- a/stdlib/theories/Reals/Abstract/ConstructivePower.v +++ b/stdlib/theories/Reals/Abstract/ConstructivePower.v @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +Require Import Znat. Require Import QArith Qabs. Require Import ConstructiveReals. Require Import ConstructiveRealsMorphisms. diff --git a/stdlib/theories/Reals/Abstract/ConstructiveReals.v b/stdlib/theories/Reals/Abstract/ConstructiveReals.v index 839cfbc02ba0..76f92e9d6a16 100644 --- a/stdlib/theories/Reals/Abstract/ConstructiveReals.v +++ b/stdlib/theories/Reals/Abstract/ConstructiveReals.v @@ -1156,7 +1156,7 @@ Definition CRup_nat {R : ConstructiveReals} (x : CRcarrier R) : { n : nat & x < CR_of_Q R (Z.of_nat n #1) }. Proof. destruct (CR_archimedean R x). exists (Pos.to_nat x0). - rewrite positive_nat_Z. exact c. + rewrite Znat.positive_nat_Z. exact c. Qed. Definition CRfloor {R : ConstructiveReals} (a : CRcarrier R) diff --git a/stdlib/theories/Reals/Abstract/ConstructiveRealsMorphisms.v b/stdlib/theories/Reals/Abstract/ConstructiveRealsMorphisms.v index e1521aa6e7de..85aa2d482fe8 100644 --- a/stdlib/theories/Reals/Abstract/ConstructiveRealsMorphisms.v +++ b/stdlib/theories/Reals/Abstract/ConstructiveRealsMorphisms.v @@ -30,6 +30,7 @@ Require Import QArith. Require Import Qabs. +Require Import Znat. Require Import ConstructiveReals. Require Import ConstructiveLimits. Require Import ConstructiveAbs. diff --git a/stdlib/theories/Reals/Abstract/ConstructiveSum.v b/stdlib/theories/Reals/Abstract/ConstructiveSum.v index 41e9403d72bd..55097468682a 100644 --- a/stdlib/theories/Reals/Abstract/ConstructiveSum.v +++ b/stdlib/theories/Reals/Abstract/ConstructiveSum.v @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +Require Import Znat. Require Import QArith Qabs. Require Import ConstructiveReals. Require Import ConstructiveRealsMorphisms. diff --git a/stdlib/theories/Reals/Alembert.v b/stdlib/theories/Reals/Alembert.v index 23cec1859b9f..f3319c057407 100644 --- a/stdlib/theories/Reals/Alembert.v +++ b/stdlib/theories/Reals/Alembert.v @@ -14,6 +14,7 @@ Require Import Rseries. Require Import SeqProp. Require Import PartSum. Require Import Lra. +Require Import Compare_dec. Local Open Scope R_scope. diff --git a/stdlib/theories/Reals/AltSeries.v b/stdlib/theories/Reals/AltSeries.v index 3c9dcc4192ab..36379576028f 100644 --- a/stdlib/theories/Reals/AltSeries.v +++ b/stdlib/theories/Reals/AltSeries.v @@ -14,6 +14,7 @@ Require Import Rseries. Require Import SeqProp. Require Import PartSum. Require Import Lra. +Require Import Compare_dec. Local Open Scope R_scope. (**********) diff --git a/stdlib/theories/Reals/ArithProp.v b/stdlib/theories/Reals/ArithProp.v index 5fcf4b805a27..30d1fdb0730d 100644 --- a/stdlib/theories/Reals/ArithProp.v +++ b/stdlib/theories/Reals/ArithProp.v @@ -11,6 +11,7 @@ Require Import Rdefinitions Raxioms RIneq. Require Import Rbasic_fun. Require Import ArithRing. +Require Import PeanoNat. Local Open Scope Z_scope. Local Open Scope R_scope. diff --git a/stdlib/theories/Reals/Binomial.v b/stdlib/theories/Reals/Binomial.v index 88477fd4dc7d..0d968410de2d 100644 --- a/stdlib/theories/Reals/Binomial.v +++ b/stdlib/theories/Reals/Binomial.v @@ -11,6 +11,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import PartSum. +Require Import Arith.Factorial. Local Open Scope R_scope. Definition C (n p:nat) : R := diff --git a/stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v b/stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v index 7b4462d4cdb0..6dc1654d1852 100644 --- a/stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v +++ b/stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v @@ -18,6 +18,8 @@ Require Import QArith Qabs Qround Qpower. Require Import Logic.ConstructiveEpsilon. Require Export ConstructiveCauchyReals. Require CMorphisms. +Require Import Znat. +Require Import Zorder. Require Import Lia. Require Import Lqa. Require Import QExtra. diff --git a/stdlib/theories/Reals/Cauchy/ConstructiveRcomplete.v b/stdlib/theories/Reals/Cauchy/ConstructiveRcomplete.v index 87e710ac3cc9..d9b0157f631a 100644 --- a/stdlib/theories/Reals/Cauchy/ConstructiveRcomplete.v +++ b/stdlib/theories/Reals/Cauchy/ConstructiveRcomplete.v @@ -9,6 +9,7 @@ (************************************************************************) (************************************************************************) +Require Import PeanoNat. Require Import QArith_base. Require Import Qabs. Require Import ConstructiveReals. @@ -215,7 +216,7 @@ Proof. destruct (xcau (4 * p)%positive) as [i imaj], (xcau (4 * q)%positive) as [j jmaj]. assert (CReal_abs (xn i - xn j) <= inject_Q (1 # 4 * n)). - { destruct (le_lt_dec i j). + { destruct (Nat.leb_spec i j) as [l|l]. - apply (CReal_le_trans _ _ _ (imaj i j (Nat.le_refl _) l)). apply inject_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos. @@ -296,8 +297,7 @@ Proof. destruct (xcau (4 * 2^p')%positive) as [i imaj]. destruct (xcau (4 * 2^q')%positive) as [j jmaj]. assert (CReal_abs (xn i - xn j) <= inject_Q (1 # 4 * 2^n')). - { - destruct (le_lt_dec i j). + { destruct (Nat.leb_spec i j) as [l|l]. - apply (CReal_le_trans _ _ _ (imaj i j (Nat.le_refl _) l)). apply inject_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos. @@ -510,7 +510,7 @@ Proof. assert (CReal_abs (xn i' - xn j') <= inject_Q (1#4)) as Hxij. { - destruct (le_lt_dec i' j'). + destruct (Nat.leb_spec i' j') as [l|l]. - apply (CReal_le_trans _ _ _ (imaj i' j' (Nat.le_refl _) l)). apply inject_Q_le; unfold Qle, Qnum, Qden; ring_simplify. apply Pos2Z_pos_is_pos. diff --git a/stdlib/theories/Reals/Cauchy/QExtra.v b/stdlib/theories/Reals/Cauchy/QExtra.v index 28c36377595b..190c9b38dcc6 100644 --- a/stdlib/theories/Reals/Cauchy/QExtra.v +++ b/stdlib/theories/Reals/Cauchy/QExtra.v @@ -2,6 +2,7 @@ Require Import QArith. Require Import Qpower. Require Import Qabs. Require Import Qround. +Require Import Zorder. Require Import Lia. Require Import Lqa. (* This is only used in a few places and could be avoided *) Require Import PosExtra. @@ -86,7 +87,7 @@ Proof. pose proof Pos_log2ceil_plus1_spec p as Hnom. pose proof Pos_log2floor_plus1_spec den as Hden. - apply (Zmult_le_reg_r _ _ 2). + apply (Zorder.Zmult_le_reg_r _ _ 2). * lia. * replace (Z.pos p * 2 ^ Z.pos (Pos_log2floor_plus1 den) * 2)%Z with ((Z.pos p * 2) * 2 ^ Z.pos (Pos_log2floor_plus1 den))%Z by ring. diff --git a/stdlib/theories/Reals/ClassicalConstructiveReals.v b/stdlib/theories/Reals/ClassicalConstructiveReals.v index e1d33f28580c..b48d5e55780a 100644 --- a/stdlib/theories/Reals/ClassicalConstructiveReals.v +++ b/stdlib/theories/Reals/ClassicalConstructiveReals.v @@ -22,6 +22,7 @@ classical reals. *) Require Import QArith_base. +Require Import Znat. Require Import Rdefinitions. Require Import Raxioms. Require Import ConstructiveReals. diff --git a/stdlib/theories/Reals/ClassicalDedekindReals.v b/stdlib/theories/Reals/ClassicalDedekindReals.v index b0b36f6a2c71..9b6317cd8358 100644 --- a/stdlib/theories/Reals/ClassicalDedekindReals.v +++ b/stdlib/theories/Reals/ClassicalDedekindReals.v @@ -19,6 +19,8 @@ Require Import Lia. Require Import Lqa. Require Import Qpower. Require Import QExtra. +Require Import Znat. +Require Import ZArith_dec. Require CMorphisms. (*****************************************************************************) diff --git a/stdlib/theories/Reals/Cos_plus.v b/stdlib/theories/Reals/Cos_plus.v index fa4805c99665..17f01634b02f 100644 --- a/stdlib/theories/Reals/Cos_plus.v +++ b/stdlib/theories/Reals/Cos_plus.v @@ -14,6 +14,7 @@ Require Import SeqSeries. Require Import Rtrigo_def. Require Import Cos_rel. Require Import Lia Lra. +Require Import Arith.Factorial. Local Open Scope nat_scope. Local Open Scope R_scope. diff --git a/stdlib/theories/Reals/Cos_rel.v b/stdlib/theories/Reals/Cos_rel.v index a2ea12edda63..e32b124f32e8 100644 --- a/stdlib/theories/Reals/Cos_rel.v +++ b/stdlib/theories/Reals/Cos_rel.v @@ -13,6 +13,7 @@ Require Import Rfunctions. Require Import SeqSeries. Require Import Rtrigo_def. Require Import Lia Lra. +Require Import Arith.Factorial. Local Open Scope R_scope. Definition A1 (x:R) (N:nat) : R := diff --git a/stdlib/theories/Reals/DiscrR.v b/stdlib/theories/Reals/DiscrR.v index 190d76ee3080..333a97ad86c8 100644 --- a/stdlib/theories/Reals/DiscrR.v +++ b/stdlib/theories/Reals/DiscrR.v @@ -14,7 +14,7 @@ Local Open Scope R_scope. Lemma Rlt_R0_R2 : 0 < 2. Proof. -change 2 with (INR 2); apply lt_INR_0; apply Nat.lt_0_succ. +change 2 with (INR 2); apply lt_INR_0; apply PeanoNat.Nat.lt_0_succ. Qed. Notation Rplus_lt_pos := Rplus_lt_0_compat (only parsing). diff --git a/stdlib/theories/Reals/Exp_prop.v b/stdlib/theories/Reals/Exp_prop.v index 5a5fac5d90e3..45ffc363d917 100644 --- a/stdlib/theories/Reals/Exp_prop.v +++ b/stdlib/theories/Reals/Exp_prop.v @@ -15,6 +15,7 @@ Require Import Rtrigo1. Require Import Ranalysis1. Require Import PSeries_reg. Require Import Lia Lra. +Require Import Arith.Factorial. Local Open Scope nat_scope. Local Open Scope R_scope. diff --git a/stdlib/theories/Reals/PartSum.v b/stdlib/theories/Reals/PartSum.v index fab0526e0e19..202f8e0faf00 100644 --- a/stdlib/theories/Reals/PartSum.v +++ b/stdlib/theories/Reals/PartSum.v @@ -9,6 +9,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +Require Import Peano_dec. +Require Import Compare_dec. Require Import Rbase. Require Import Rfunctions. Require Import Rseries. diff --git a/stdlib/theories/Reals/RIneq.v b/stdlib/theories/Reals/RIneq.v index 1a986958b0a0..eaeebc28a9d7 100644 --- a/stdlib/theories/Reals/RIneq.v +++ b/stdlib/theories/Reals/RIneq.v @@ -2624,8 +2624,10 @@ Hint Extern 0 (IZR _ >= IZR _) => apply Rle_ge, IZR_le, Zle_bool_imp_le, eq_refl Hint Extern 0 (IZR _ < IZR _) => apply IZR_lt, eq_refl : real. #[global] Hint Extern 0 (IZR _ > IZR _) => apply IZR_lt, eq_refl : real. +Lemma Private_Zeq_bool_neq : forall x y : Z, (x =? y) = false -> x <> y. +Proof. intros. rewrite <-Z.eqb_eq. congruence. Qed. #[global] -Hint Extern 0 (IZR _ <> IZR _) => apply eq_IZR_contrapositive, Zeq_bool_neq, eq_refl : real. +Hint Extern 0 (IZR _ <> IZR _) => apply eq_IZR_contrapositive, Private_Zeq_bool_neq, eq_refl : real. Lemma one_IZR_lt1 : forall n:Z, -1 < IZR n < 1 -> n = 0%Z. Proof. @@ -2683,8 +2685,9 @@ Proof. Qed. (* NOTE: keeping inconsistent variable names for backward compatibility. *) -Lemma Zeq_bool_IZR : forall x y:Z, IZR x = IZR y -> Zeq_bool x y = true. -Proof. now intros n m H; apply Zeq_is_eq_bool, eq_IZR. Qed. +#[deprecated(use=Z.eqb_eq, since="9.0")] +Lemma Zeq_bool_IZR : forall x y:Z, IZR x = IZR y -> Z.eqb x y = true. +Proof. now intros n m H; apply Z.eqb_eq, eq_IZR. Qed. Local Lemma Private_Zeqb_IZR : forall x y:Z, IZR x = IZR y -> Z.eqb x y = true. Proof. intros. apply Z.eqb_eq, eq_IZR; trivial. Qed. diff --git a/stdlib/theories/Reals/RList.v b/stdlib/theories/Reals/RList.v index 6c0c38221f02..8563c6854844 100644 --- a/stdlib/theories/Reals/RList.v +++ b/stdlib/theories/Reals/RList.v @@ -9,6 +9,7 @@ (************************************************************************) Require Import List. +Require Import Compare_dec. Require Import Rbase. Require Import Rfunctions. Local Open Scope R_scope. diff --git a/stdlib/theories/Reals/Ratan.v b/stdlib/theories/Reals/Ratan.v index f65f7934a777..f03a91382643 100644 --- a/stdlib/theories/Reals/Ratan.v +++ b/stdlib/theories/Reals/Ratan.v @@ -22,6 +22,7 @@ Require Import Ranalysis5. Require Import SeqSeries. Require Import PartSum. Require Import Lia. +Require Import Znat. Local Open Scope R_scope. Local Ltac Tauto.intuition_solver ::= auto with rorders real arith. diff --git a/stdlib/theories/Reals/Raxioms.v b/stdlib/theories/Reals/Raxioms.v index 4e4225e774c8..6f9bc76f1b4b 100644 --- a/stdlib/theories/Reals/Raxioms.v +++ b/stdlib/theories/Reals/Raxioms.v @@ -19,7 +19,8 @@ (** Lifts of basic operations for classical reals *) (*********************************************************) -Require Export ZArith_base. +Require Export BinInt. +Require Import Znat. Require Import ClassicalDedekindReals. Require Import ConstructiveCauchyReals. Require Import ConstructiveCauchyRealsMult. diff --git a/stdlib/theories/Reals/Rdefinitions.v b/stdlib/theories/Reals/Rdefinitions.v index 37472220f3a4..4e349753047f 100644 --- a/stdlib/theories/Reals/Rdefinitions.v +++ b/stdlib/theories/Reals/Rdefinitions.v @@ -14,7 +14,8 @@ This file also contains the proof that classical reals are a quotient of constructive Cauchy reals. *) -Require Export ZArith_base. +Require Export PeanoNat. +Require Export BinInt. Require Import QArith_base. Require Import ConstructiveCauchyReals. Require Import ConstructiveCauchyRealsMult. diff --git a/stdlib/theories/Reals/Rfunctions.v b/stdlib/theories/Reals/Rfunctions.v index 9b0b235f488f..d38638e27e38 100644 --- a/stdlib/theories/Reals/Rfunctions.v +++ b/stdlib/theories/Reals/Rfunctions.v @@ -26,6 +26,8 @@ Require Export SplitAbsolu. Require Export SplitRmult. Require Export ArithProp. Require Import Zpower. +Require Import Znat. +Require Import Arith.Factorial. Local Open Scope nat_scope. Local Open Scope R_scope. diff --git a/stdlib/theories/Reals/RiemannInt_SF.v b/stdlib/theories/Reals/RiemannInt_SF.v index a42f00e4a270..d2aa2e963258 100644 --- a/stdlib/theories/Reals/RiemannInt_SF.v +++ b/stdlib/theories/Reals/RiemannInt_SF.v @@ -15,6 +15,7 @@ Require Import Classical_Prop. Require Import List. Require Import RList. Require Import Lia Lra. +Require Import Wf_Z. Local Open Scope R_scope. Set Implicit Arguments. diff --git a/stdlib/theories/Reals/Rlogic.v b/stdlib/theories/Reals/Rlogic.v index 58e907a40095..94ec98a326c6 100644 --- a/stdlib/theories/Reals/Rlogic.v +++ b/stdlib/theories/Reals/Rlogic.v @@ -15,6 +15,9 @@ - Decidability of negated formulas. *) +Require Import PeanoNat. +Require Import Zabs. +Require Import Zorder. Require Import RIneq. (** * Decidability of arithmetical statements *) diff --git a/stdlib/theories/Reals/Rpower.v b/stdlib/theories/Reals/Rpower.v index 77cd0cbd7c3f..5ac329b54891 100644 --- a/stdlib/theories/Reals/Rpower.v +++ b/stdlib/theories/Reals/Rpower.v @@ -26,6 +26,7 @@ Require Import Sqrt_reg. Require Import MVT. Require Import Ranalysis4. Require Import Lra. +Require Import Arith.Factorial. Local Open Scope R_scope. Definition P_Rmin_stt (P:R -> Prop) x y := Rmin_case x y P. diff --git a/stdlib/theories/Reals/Rprod.v b/stdlib/theories/Reals/Rprod.v index 2772931d22c7..f9698fdbfb0d 100644 --- a/stdlib/theories/Reals/Rprod.v +++ b/stdlib/theories/Reals/Rprod.v @@ -15,6 +15,8 @@ Require Import Rseries. Require Import PartSum. Require Import Binomial. Require Import Lia. +Require Import Arith.Factorial. +Require Import Peano_dec. Local Open Scope R_scope. (** TT Ak; 0<=k<=N *) diff --git a/stdlib/theories/Reals/Rtrigo.v b/stdlib/theories/Reals/Rtrigo.v index 03132ad470bd..72468b1c1fa4 100644 --- a/stdlib/theories/Reals/Rtrigo.v +++ b/stdlib/theories/Reals/Rtrigo.v @@ -16,7 +16,7 @@ Require Export Rtrigo_def. Require Export Rtrigo_alt. Require Export Cos_rel. Require Export Cos_plus. -Require Import ZArith_base. +Require Import BinInt. Require Import Zcomplements. Require Import Lra. Require Import Ranalysis1. diff --git a/stdlib/theories/Reals/Rtrigo1.v b/stdlib/theories/Reals/Rtrigo1.v index a39d51a8a5d7..7818a57ede14 100644 --- a/stdlib/theories/Reals/Rtrigo1.v +++ b/stdlib/theories/Reals/Rtrigo1.v @@ -16,13 +16,15 @@ Require Export Rtrigo_def. Require Export Rtrigo_alt. Require Export Cos_rel. Require Export Cos_plus. -Require Import ZArith_base. +Require Import BinInt. Require Import Zcomplements. Require Import Lia. Require Import Lra. Require Import Ranalysis1. Require Import Rsqrt_def. Require Import PSeries_reg. +Require Import Arith.Factorial. +Require Import Znat. Local Open Scope nat_scope. Local Open Scope R_scope. diff --git a/stdlib/theories/Reals/Rtrigo_alt.v b/stdlib/theories/Reals/Rtrigo_alt.v index 66b01b1b7359..6646860acb14 100644 --- a/stdlib/theories/Reals/Rtrigo_alt.v +++ b/stdlib/theories/Reals/Rtrigo_alt.v @@ -13,6 +13,7 @@ Require Import Rfunctions. Require Import SeqSeries. Require Import Rtrigo_def. Require Import Lia Lra. +Require Import Arith.Factorial. Local Open Scope R_scope. (***************************************************************) diff --git a/stdlib/theories/Reals/Rtrigo_def.v b/stdlib/theories/Reals/Rtrigo_def.v index acc80c95134b..390d75a5b402 100644 --- a/stdlib/theories/Reals/Rtrigo_def.v +++ b/stdlib/theories/Reals/Rtrigo_def.v @@ -9,6 +9,7 @@ (************************************************************************) Require Import Rbase Rfunctions SeqSeries Rtrigo_fun. +Require Import Arith.Factorial. Require Import Lra Lia. Local Open Scope R_scope. diff --git a/stdlib/theories/Reals/Rtrigo_fun.v b/stdlib/theories/Reals/Rtrigo_fun.v index 82116e1f67b5..917e2a56bf8a 100644 --- a/stdlib/theories/Reals/Rtrigo_fun.v +++ b/stdlib/theories/Reals/Rtrigo_fun.v @@ -11,6 +11,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. +Require Import Arith.Factorial. Local Open Scope R_scope. (*****************************************************************) diff --git a/stdlib/theories/Reals/Rtrigo_reg.v b/stdlib/theories/Reals/Rtrigo_reg.v index 980755135143..a99b3372e0cf 100644 --- a/stdlib/theories/Reals/Rtrigo_reg.v +++ b/stdlib/theories/Reals/Rtrigo_reg.v @@ -15,6 +15,7 @@ Require Import Rtrigo1. Require Import Ranalysis1. Require Import PSeries_reg. Require Import Lra. +Require Import Arith.Factorial. Local Open Scope nat_scope. Local Open Scope R_scope. diff --git a/stdlib/theories/Reals/SeqProp.v b/stdlib/theories/Reals/SeqProp.v index af5e61f0ab32..7a9c88047a73 100644 --- a/stdlib/theories/Reals/SeqProp.v +++ b/stdlib/theories/Reals/SeqProp.v @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +Require Import Arith.Factorial. Require Import Rbase. Require Import Rfunctions. Require Import Rseries. diff --git a/stdlib/theories/Reals/SeqSeries.v b/stdlib/theories/Reals/SeqSeries.v index ecfdbbb8e7e0..6fa0f08d3cce 100644 --- a/stdlib/theories/Reals/SeqSeries.v +++ b/stdlib/theories/Reals/SeqSeries.v @@ -21,6 +21,7 @@ Require Export Rprod. Require Export Cauchy_prod. Require Export Alembert. Require Import Lra. +Require Import Compare_dec. Local Open Scope R_scope. (**********) diff --git a/stdlib/theories/Structures/OrderedTypeEx.v b/stdlib/theories/Structures/OrderedTypeEx.v index 228f62b068c8..7c7143334ac6 100644 --- a/stdlib/theories/Structures/OrderedTypeEx.v +++ b/stdlib/theories/Structures/OrderedTypeEx.v @@ -9,7 +9,7 @@ (************************************************************************) Require Import OrderedType. -Require Import ZArith_base. +Require Import BinInt. Require Import PeanoNat Peano_dec Compare_dec. Require Import Ascii String. Require Import NArith Ndec. diff --git a/stdlib/theories/ZArith/ZArith.v b/stdlib/theories/ZArith/ZArith.v index 77c28b6425c4..175c42fcc0eb 100644 --- a/stdlib/theories/ZArith/ZArith.v +++ b/stdlib/theories/ZArith/ZArith.v @@ -10,7 +10,30 @@ (** Library for manipulating integers based on binary encoding *) -Require Export ZArith_base. +Require Export BinNums. +Require Export BinPos. +Require Export BinNat. +Require Export BinInt. +Require Export Zcompare. +Require Export Zorder. +Require Export Zeven. +Require Export Zminmax. +Require Export Zmin. +Require Export Zmax. +Require Export Zabs. +Require Export Znat. +Require Export auxiliary. +Require Export ZArith_dec. +Require Export Zbool. +Require Export Zmisc. +Require Export Wf_Z. + +#[global] +Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l + Z.add_0_r Z.mul_1_l Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_add_distr_l + Z.mul_add_distr_r: zarith. + +Require Export Zhints. (** Extra definitions *) diff --git a/stdlib/theories/ZArith/ZArith_base.v b/stdlib/theories/ZArith/ZArith_base.v index 84ec867c35e4..c26e455b7cb8 100644 --- a/stdlib/theories/ZArith/ZArith_base.v +++ b/stdlib/theories/ZArith/ZArith_base.v @@ -8,8 +8,10 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +Attributes deprecated(since="9.0", note="use ZArith instead"). + (** Library for manipulating integers based on binary encoding. - These are the basic modules, required by [Omega] and [Ring] for instance. + This is a subset of basic modules. The full library is [ZArith]. *) Require Export BinNums. diff --git a/stdlib/theories/ZArith/Zbool.v b/stdlib/theories/ZArith/Zbool.v index d8adc36f3ae1..069455e658c6 100644 --- a/stdlib/theories/ZArith/Zbool.v +++ b/stdlib/theories/ZArith/Zbool.v @@ -17,44 +17,6 @@ Require Import Sumbool. Local Open Scope Z_scope. -(** * Boolean operations from decidability of order *) -(** The decidability of equality and order relations over - type [Z] gives some boolean functions with the adequate specification. *) - -Definition Z_lt_ge_bool (x y:Z) := bool_of_sumbool (Z_lt_ge_dec x y). -Definition Z_ge_lt_bool (x y:Z) := bool_of_sumbool (Z_ge_lt_dec x y). - -Definition Z_le_gt_bool (x y:Z) := bool_of_sumbool (Z_le_gt_dec x y). -Definition Z_gt_le_bool (x y:Z) := bool_of_sumbool (Z_gt_le_dec x y). - -Definition Z_eq_bool (x y:Z) := bool_of_sumbool (Z.eq_dec x y). -Definition Z_noteq_bool (x y:Z) := bool_of_sumbool (Z_noteq_dec x y). - -Definition Zeven_odd_bool (x:Z) := bool_of_sumbool (Zeven_odd_dec x). - -(**********************************************************************) -(** * Boolean comparisons of binary integers *) - -Notation Zle_bool := Z.leb (only parsing). -Notation Zge_bool := Z.geb (only parsing). -Notation Zlt_bool := Z.ltb (only parsing). -Notation Zgt_bool := Z.gtb (only parsing). - -(** We now provide a direct [Z.eqb] that doesn't refer to [Z.compare]. - The old [Zeq_bool] is kept for compatibility. *) - -Definition Zeq_bool (x y:Z) := - match x ?= y with - | Eq => true - | _ => false - end. - -Definition Zneq_bool (x y:Z) := - match x ?= y with - | Eq => false - | _ => true - end. - (** Properties in term of [if ... then ... else ...] *) Lemma Zle_cases n m : if n <=? m then n <= m else n > m. @@ -161,24 +123,72 @@ Proof. Z.swap_greater. rewrite Z.leb_le. apply Z.lt_le_pred. Qed. +Local Set Warnings "-deprecated". + (** Properties of the deprecated [Zeq_bool] *) +(** * Boolean operations from decidability of order *) +(** The decidability of equality and order relations over + type [Z] gives some boolean functions with the adequate specification. *) + +#[deprecated(use=Z.eqb, since="9.0")] +Definition Z_lt_ge_bool (x y:Z) := bool_of_sumbool (Z_lt_ge_dec x y). +#[deprecated(use=Z.eqb, since="9.0")] +Definition Z_ge_lt_bool (x y:Z) := bool_of_sumbool (Z_ge_lt_dec x y). + +#[deprecated(use=Z.eqb, since="9.0")] +Definition Z_le_gt_bool (x y:Z) := bool_of_sumbool (Z_le_gt_dec x y). +#[deprecated(use=Z.eqb, since="9.0")] +Definition Z_gt_le_bool (x y:Z) := bool_of_sumbool (Z_gt_le_dec x y). + +#[deprecated(use=Z.eqb, since="9.0")] +Definition Z_eq_bool (x y:Z) := bool_of_sumbool (Z.eq_dec x y). +#[deprecated(use=Z.eqb, since="9.0")] +Definition Z_noteq_bool (x y:Z) := bool_of_sumbool (Z_noteq_dec x y). + +#[deprecated(use=Z.eqb, since="9.0")] +Definition Zeven_odd_bool (x:Z) := bool_of_sumbool (Zeven_odd_dec x). + +(**********************************************************************) +(** * Boolean comparisons of binary integers *) + +#[deprecated(use=Z.eqb, since="9.0")] +Notation Zle_bool := Z.leb (only parsing). +#[deprecated(use=Z.eqb, since="9.0")] +Notation Zge_bool := Z.geb (only parsing). +#[deprecated(use=Z.eqb, since="9.0")] +Notation Zlt_bool := Z.ltb (only parsing). +#[deprecated(use=Z.eqb, since="9.0")] +Notation Zgt_bool := Z.gtb (only parsing). + +(** We now provide a direct [Z.eqb] that doesn't refer to [Z.compare]. + The old [Zeq_bool] is kept for compatibility. *) + +#[deprecated(use=Z.eqb, since="9.0")] +Notation Zeq_bool := Z.eqb. + +#[deprecated(use=Z.eqb_eq, since="9.0")] Lemma Zeq_is_eq_bool x y : x = y <-> Zeq_bool x y = true. -Proof. - unfold Zeq_bool. - rewrite <- Z.compare_eq_iff. destruct Z.compare; now split. -Qed. +Proof. symmetry; apply Z.eqb_eq. Qed. +#[deprecated(use=Z.eqb_eq, since="9.0")] Lemma Zeq_bool_eq x y : Zeq_bool x y = true -> x = y. -Proof. - apply Zeq_is_eq_bool. -Qed. +Proof. apply Z.eqb_eq. Qed. + +#[deprecated(use=Z.eqb, since="9.0")] +Definition Zneq_bool (x y:Z) := + match x ?= y with + | Eq => false + | _ => true + end. +#[deprecated(use=Z.eqb_eq, since="9.0")] Lemma Zeq_bool_neq x y : Zeq_bool x y = false -> x <> y. Proof. rewrite Zeq_is_eq_bool; now destruct Zeq_bool. Qed. +#[deprecated(use=Z.eqb_eq, since="9.0")] Lemma Zeq_bool_if x y : if Zeq_bool x y then x=y else x<>y. Proof. generalize (Zeq_bool_eq x y) (Zeq_bool_neq x y). diff --git a/stdlib/theories/ZArith/Zcomplements.v b/stdlib/theories/ZArith/Zcomplements.v index 4c540f72e4da..3107efe01a25 100644 --- a/stdlib/theories/ZArith/Zcomplements.v +++ b/stdlib/theories/ZArith/Zcomplements.v @@ -9,14 +9,18 @@ (************************************************************************) Require Import ZArithRing. -Require Import ZArith_base. +Require Import BinInt. +Require Import Znat. Require Import Wf_nat. Local Open Scope Z_scope. +Require Zabs Wf_Z. +Require Zeven. (**********************************************************************) (** About parity *) -Notation two_or_two_plus_one := Z_modulo_2 (only parsing). +#[deprecated(since="9.0")] +Notation two_or_two_plus_one := Zeven.Z_modulo_2 (only parsing). (**********************************************************************) (** The biggest power of 2 that is stricly less than [a] @@ -41,15 +45,15 @@ Proof. unfold floor. intros p; induction p as [p [IH1p IH2p]|p [IH1p IH2]|]; simpl. - rewrite !Pos2Z.inj_xI, (Pos2Z.inj_xO (xO _)), Pos2Z.inj_xO. split. - + apply Z.le_trans with (2 * Z.pos p); auto with zarith. + + apply Z.le_trans with (2 * Z.pos p); auto using Z.le_succ_diag_r. + apply Z.lt_le_trans with (2 * (Z.pos p + 1)). * rewrite Z.mul_add_distr_l, Z.mul_1_r. - apply Zplus_lt_compat_l; red; auto with zarith. - * apply Z.mul_le_mono_nonneg_l; auto with zarith. - rewrite Z.add_1_r; apply Zlt_le_succ; auto. + apply Z.add_lt_mono_l; reflexivity. + * apply Z.mul_le_mono_nonneg_l; trivial using Z.le_0_2. + rewrite Z.add_1_r. apply Z.le_succ_l. trivial. - rewrite (Pos2Z.inj_xO (xO _)), (Pos2Z.inj_xO p), Pos2Z.inj_xO. split; auto with zarith. - - split; auto with zarith; red; auto. + - split; auto using Z.le_refl, Z.lt_1_2. Qed. (**********************************************************************) @@ -63,16 +67,16 @@ Proof. intros P HP p. set (Q := fun z => 0 <= z -> P z * P (- z)). enough (H:Q (Z.abs p)) by - (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith). - apply (Z_lt_rec Q); auto with zarith. + (destruct (Zabs.Zabs_dec p) as [-> | ->]; elim H; auto using Z.abs_nonneg ). + apply (Wf_Z.Z_lt_rec Q); auto using Z.abs_nonneg. subst Q; intros x H. split; apply HP. - rewrite Z.abs_eq; auto; intros m ?. - destruct (H (Z.abs m)); auto with zarith. - destruct (Zabs_dec m) as [-> | ->]; trivial. + destruct (H (Z.abs m)); auto using Z.abs_nonneg. + destruct (Zabs.Zabs_dec m) as [-> | ->]; trivial. - rewrite Z.abs_neq, Z.opp_involutive; [intros m ?|]. - + destruct (H (Z.abs m)); auto with zarith. - destruct (Zabs_dec m) as [-> | ->]; trivial. + + destruct (H (Z.abs m)); auto using Z.abs_nonneg. + destruct (Zabs.Zabs_dec m) as [-> | ->]; trivial. + apply Z.opp_le_mono; rewrite Z.opp_involutive; auto. Qed. @@ -84,16 +88,16 @@ Proof. intros P HP p. set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *. enough (Q (Z.abs p)) as H by - (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith). - apply (Z_lt_induction Q); auto with zarith. + (destruct (Zabs.Zabs_dec p) as [-> | ->]; elim H; auto using Z.abs_nonneg). + apply (Wf_Z.Z_lt_induction Q); auto using Z.abs_nonneg. subst Q; intros ? H. split; apply HP. - rewrite Z.abs_eq; auto; intros m ?. - elim (H (Z.abs m)); intros; auto with zarith. - elim (Zabs_dec m); intro eq; rewrite eq; trivial. + elim (H (Z.abs m)); intros; auto using Z.abs_nonneg. + elim (Zabs.Zabs_dec m); intro eq; rewrite eq; trivial. - rewrite Z.abs_neq, Z.opp_involutive; [intros m ?|]. - + destruct (H (Z.abs m)); auto with zarith. - destruct (Zabs_dec m) as [-> | ->]; trivial. + + destruct (H (Z.abs m)); auto using Z.abs_nonneg. + destruct (Zabs.Zabs_dec m) as [-> | ->]; trivial. + apply Z.opp_le_mono; rewrite Z.opp_involutive; auto. Qed. @@ -135,9 +139,9 @@ Section Zlength_properties. Proof. assert (H : forall l acc, Zlength_aux acc A l = acc + Z.of_nat (length l)). - clear l. intros l; induction l as [|? ? IHl]. - + auto with zarith. + + auto using Z.add_0_r. + intros. simpl length; simpl Zlength_aux. - rewrite IHl, Nat2Z.inj_succ, Z.add_succ_comm; auto. + rewrite IHl, Znat.Nat2Z.inj_succ, Z.add_succ_comm; auto. - unfold Zlength. now rewrite H. Qed. diff --git a/stdlib/theories/ZArith/Zdiv.v b/stdlib/theories/ZArith/Zdiv.v index db631e8117f5..5a144eaf3244 100644 --- a/stdlib/theories/ZArith/Zdiv.v +++ b/stdlib/theories/ZArith/Zdiv.v @@ -13,8 +13,8 @@ (** Initial Contribution by Claude Marché and Xavier Urbain *) -Require Export ZArith_base. -Require Import Zbool ZArithRing Zcomplements Setoid Morphisms. +Require Export BinInt. +Require Import Wf_Z Zbool ZArithRing Zcomplements Setoid Morphisms. Local Open Scope Z_scope. (** The definition of the division is now in [BinIntDef], the initial @@ -227,7 +227,7 @@ Lemma Z_mod_same_full : forall a, a mod a = 0. Proof. intros a. zero_or_not a. apply Z.mod_same; auto. Qed. Lemma Z_mod_mult : forall a b, (a*b) mod b = 0. -Proof. intros a b. zero_or_not b. now apply Z.mod_mul. Qed. +Proof. intros a b. zero_or_not b. apply Z.mul_0_r. now apply Z.mod_mul. Qed. Lemma Z_div_mult_full : forall a b:Z, b <> 0 -> (a*b)/b = a. Proof Z.div_mul. @@ -340,8 +340,8 @@ Proof. destruct Z.pos_div_eucl as (q,r); destruct r; rewrite ?Z.mul_1_r, <-?Z.opp_eq_mul_m1, ?Z.sgn_opp, ?Z.opp_involutive; match goal with [|- (_ -> _ -> ?P) -> _] => - intros HH; assert (HH1 : P); auto with zarith - end; apply Z.sgn_nonneg; auto with zarith. + intros HH; assert (HH1 : P); auto using Pos2Z.is_pos, Pos2Z.is_nonneg + end; apply Z.sgn_nonneg; auto using Z.add_nonneg_nonneg, Z.le_succ_diag_r. Qed. (** * Relations between usual operations and Z.modulo and Z.div *) @@ -565,7 +565,7 @@ Qed. Theorem Zdiv_mult_le: forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b. Proof. - intros a b c ? ? ?. zero_or_not b. + intros a b c ? ? ?. zero_or_not b; rewrite ?Z.mul_0_r; trivial. apply Z.div_mul_le; auto. apply Z.le_neq; auto. Qed. @@ -576,7 +576,7 @@ Lemma Zmod_divides : forall a b, b<>0 -> (a mod b = 0 <-> exists c, a = b*c). Proof. intros. rewrite Z.mod_divide; trivial. - split; intros (c,Hc); exists c; subst; auto with zarith. + split; intros (c,Hc); exists c; subst; auto using Z.mul_comm. Qed. (** Particular case : dividing by 2 is related with parity *) @@ -591,15 +591,15 @@ Qed. Lemma Zmod_even : forall a, a mod 2 = if Z.even a then 0 else 1. Proof. - intros a. rewrite Zmod_odd, Zodd_even_bool. now destruct Z.even. + intros a. rewrite Zmod_odd, <-Z.negb_even; now destruct Z.even. Qed. -Lemma Zodd_mod : forall a, Z.odd a = Zeq_bool (a mod 2) 1. +Lemma Zodd_mod : forall a, Z.odd a = Z.eqb (a mod 2) 1. Proof. intros a. rewrite Zmod_odd. now destruct Z.odd. Qed. -Lemma Zeven_mod : forall a, Z.even a = Zeq_bool (a mod 2) 0. +Lemma Zeven_mod : forall a, Z.even a = Z.eqb (a mod 2) 0. Proof. intros a. rewrite Zmod_even. now destruct Z.even. Qed. @@ -721,16 +721,16 @@ Theorem Zdiv_eucl_extended : {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b}. Proof. intros b Hb a. - destruct (Z_le_gt_dec 0 b) as [Hb'|Hb']. + destruct (Z.leb 0 b) eqn:Hb'; [ apply Z.leb_le in Hb' | apply Z.leb_gt in Hb']. - assert (Hb'' : b > 0) by (apply Z.lt_gt, Z.le_neq; auto). rewrite Z.abs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ]. - assert (Hb'' : - b > 0). - { now apply Z.lt_gt, Z.opp_lt_mono; rewrite Z.opp_involutive; apply Z.gt_lt. } + { apply Z.lt_gt, Z.opp_lt_mono; rewrite Z.opp_involutive. apply Hb'. } destruct (Zdiv_eucl_exist Hb'' a) as ((q,r),[]). exists (- q, r). split. + rewrite <- Z.mul_opp_comm; assumption. - + rewrite Z.abs_neq; [ assumption | apply Z.lt_le_incl, Z.gt_lt; auto ]. + + rewrite Z.abs_neq; [ assumption | apply Z.lt_le_incl; auto ]. Qed. Arguments Zdiv_eucl_extended : default implicits. @@ -752,7 +752,7 @@ Lemma mod_pow_l a b c : (a mod c)^b mod c = ((a ^ b) mod c). Proof. destruct (Z.ltb_spec b 0) as [|Hb]. { rewrite !Z.pow_neg_r; trivial. } destruct (Z.eqb_spec c 0) as [|Hc]. { subst. rewrite !Zmod_0_r; trivial. } - generalize dependent b; eapply natlike_ind; trivial; intros x Hx IH. + generalize dependent b; eapply Wf_Z.natlike_ind; trivial; intros x Hx IH. rewrite !Z.pow_succ_r, <-Z.mul_mod_idemp_r, IH, Z.mul_mod_idemp_l, Z.mul_mod_idemp_r; trivial. Qed. diff --git a/stdlib/theories/ZArith/Zgcd_alt.v b/stdlib/theories/ZArith/Zgcd_alt.v index 7bac64e23754..649c29590a6b 100644 --- a/stdlib/theories/ZArith/Zgcd_alt.v +++ b/stdlib/theories/ZArith/Zgcd_alt.v @@ -21,7 +21,8 @@ Author: Pierre Letouzey here due to both its intrinsic interest and its use as reference point when proving gcd on Int31 numbers *) -Require Import ZArith_base. +Require Import BinInt. +Require Import Znat. Require Import ZArithRing. Require Import Zdiv. Require Import Znumtheory. diff --git a/stdlib/theories/ZArith/Znumtheory.v b/stdlib/theories/ZArith/Znumtheory.v index 96f607a15b3a..7e8747c7f61f 100644 --- a/stdlib/theories/ZArith/Znumtheory.v +++ b/stdlib/theories/ZArith/Znumtheory.v @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +Local Set Warnings "-deprecated". Require Import ZArith_base. Require Import ZArithRing. Require Import Zcomplements. diff --git a/stdlib/theories/ZArith/Zpow_facts.v b/stdlib/theories/ZArith/Zpow_facts.v index 88b4e6b9bd66..1549a672a86a 100644 --- a/stdlib/theories/ZArith/Zpow_facts.v +++ b/stdlib/theories/ZArith/Zpow_facts.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import ZArith_base ZArithRing Lia Zcomplements Zdiv Znumtheory. +Require Import BinInt Znat ZArithRing Lia Wf_Z Zcomplements Zdiv Znumtheory. Require Export Zpower. Local Open Scope Z_scope. @@ -104,7 +104,7 @@ Theorem Zpower_mod p q n : 0 < n -> (p^q) mod n = ((p mod n)^q) mod n. Proof. intros Hn; destruct (Z.le_gt_cases 0 q) as [H1|H1]. - - pattern q; apply natlike_ind; trivial. + - pattern q; apply Wf_Z.natlike_ind; trivial. clear q H1. intros q Hq Rec. rewrite !Z.pow_succ_r; trivial. rewrite Z.mul_mod_idemp_l by lia. rewrite Z.mul_mod, Rec, <- Z.mul_mod by lia. reflexivity. diff --git a/stdlib/theories/ZArith/Zpower.v b/stdlib/theories/ZArith/Zpower.v index c14177818061..e2557e952210 100644 --- a/stdlib/theories/ZArith/Zpower.v +++ b/stdlib/theories/ZArith/Zpower.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Wf_nat ZArith_base Zcomplements. +Require Import Wf_nat BinInt Zcomplements Znat. Require Export Zpow_def. Local Open Scope Z_scope. @@ -276,11 +276,11 @@ Section power_div_with_rest. assert (H1 : 0 < d) by now apply Z.le_lt_trans with (1 := H1'). assert (H2 : 0 <= d + r) by now apply Z.add_nonneg_nonneg; auto; apply Z.lt_le_incl. assert (H3 : d + r < 2 * d) - by now rewrite <-Z.add_diag; apply Zplus_lt_compat_l. + by now rewrite <-Z.add_diag; apply Z.add_lt_mono_l. assert (H4 : r < 2 * d) by now apply Z.lt_le_trans with (1 * d); [ rewrite Z.mul_1_l; auto | - apply Zmult_le_compat_r; try discriminate; + apply Z.mul_le_mono_nonneg_r; try discriminate; now apply Z.lt_le_incl]. destruct q as [ |[q|q| ]|[q|q| ]]. - repeat split; auto. diff --git a/stdlib/theories/ZArith/Zquot.v b/stdlib/theories/ZArith/Zquot.v index 3c915ecc7910..ba0502234150 100644 --- a/stdlib/theories/ZArith/Zquot.v +++ b/stdlib/theories/ZArith/Zquot.v @@ -8,7 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Nnat ZArith_base Lia ZArithRing Zdiv Morphisms. +Require Import BinNat BinInt Nnat Znat Lia ZArithRing Zdiv Morphisms. +Require Zeven. Local Open Scope Z_scope. @@ -388,12 +389,12 @@ Proof. intros. symmetry. apply Zrem_unique_full with (Z.quot2 a). - apply Zquot2_odd_remainder. - - apply Zquot2_odd_eqn. + - apply Zeven.Zquot2_odd_eqn. Qed. Lemma Zrem_even : forall a, Z.rem a 2 = if Z.even a then 0 else Z.sgn a. Proof. - intros a. rewrite Zrem_odd, Zodd_even_bool. now destruct Z.even. + intros a. rewrite Zrem_odd, <-Z.negb_even. now destruct Z.even. Qed. Lemma Zeven_rem : forall a, Z.even a = Z.eqb (Z.rem a 2) 0. diff --git a/stdlib/theories/ZArith/Zwf.v b/stdlib/theories/ZArith/Zwf.v index 726cab958afd..7177fb0141fb 100644 --- a/stdlib/theories/ZArith/Zwf.v +++ b/stdlib/theories/ZArith/Zwf.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import ZArith_base. +Require Import PeanoNat BinInt. Require Export Wf_nat. Require Import Lia. Local Open Scope Z_scope. diff --git a/stdlib/theories/micromega/RMicromega.v b/stdlib/theories/micromega/RMicromega.v index 58c6dcd36d56..d989b6355d1f 100644 --- a/stdlib/theories/micromega/RMicromega.v +++ b/stdlib/theories/micromega/RMicromega.v @@ -18,10 +18,12 @@ Require Import OrderedRing. Require Import QMicromega RingMicromega. Require Import Refl. Require Import Sumbool Raxioms Rfunctions RIneq Rpow_def. +Require Import BinNat. Require Import QArith. Require Import Qfield. Require Import Qreals. Require Import DeclConstant. +Require Import Znat. Require Setoid. @@ -111,14 +113,12 @@ Proof. now apply Q2R_inv, Qeq_bool_neq. Qed. -Notation to_nat := N.to_nat. - Lemma QSORaddon : @SORaddon R R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle (* ring elements *) Q 0%Q 1%Q Qplus Qmult Qminus Qopp (* coefficients *) Qeq_bool Qle_bool - Q2R nat to_nat pow. + Q2R nat N.to_nat pow. Proof. constructor. - constructor ; intros ; try reflexivity. @@ -201,7 +201,7 @@ Proof. - destruct z ; try congruence. + compute. congruence. + compute. congruence. - - generalize (Zle_0_nat n). auto using Z.le_ge. + - generalize (Znat.Nat2Z.is_nonneg n). auto using Z.le_ge. Qed. Definition CInvR0 (r : Rcst) := Qeq_bool (Q_of_Rcst r) (0 # 1). @@ -459,7 +459,7 @@ Proof. apply Reval_pop2_eval_op2. Qed. -Definition QReval_expr := eval_pexpr Rplus Rmult Rminus Ropp Q2R to_nat pow. +Definition QReval_expr := eval_pexpr Rplus Rmult Rminus Ropp Q2R N.to_nat pow. Definition QReval_formula (e: PolEnv R) (k: Tauto.kind) (ff : Formula Q) := let (lhs,o,rhs) := ff in Reval_op2 k o (QReval_expr e lhs) (QReval_expr e rhs). @@ -566,3 +566,6 @@ Qed. (* Local Variables: *) (* coding: utf-8 *) (* End: *) + +#[deprecated(since="9.0")] +Notation to_nat := N.to_nat. diff --git a/stdlib/theories/micromega/VarMap.v b/stdlib/theories/micromega/VarMap.v index cf00bfb100a4..cb525b8a2b1e 100644 --- a/stdlib/theories/micromega/VarMap.v +++ b/stdlib/theories/micromega/VarMap.v @@ -15,7 +15,7 @@ (* *) (************************************************************************) -Require Import ZArith_base. +Require Import BinInt. Require Import List. Set Implicit Arguments. diff --git a/stdlib/theories/micromega/ZArith_hints.v b/stdlib/theories/micromega/ZArith_hints.v index 782ed26fd7cc..878b433bd6bb 100644 --- a/stdlib/theories/micromega/ZArith_hints.v +++ b/stdlib/theories/micromega/ZArith_hints.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Lia. -Import ZArith_base. +Import BinInt. #[global] Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l diff --git a/stdlib/theories/micromega/ZCoeff.v b/stdlib/theories/micromega/ZCoeff.v index d1f4a2e04c5a..c0ef8af73ca3 100644 --- a/stdlib/theories/micromega/ZCoeff.v +++ b/stdlib/theories/micromega/ZCoeff.v @@ -12,7 +12,7 @@ Require Import OrderedRing. Require Import RingMicromega. -Require Import ZArith_base. +Require Import BinInt. Require Import InitialRing. Require Import Setoid. Require Import ZArithRing. @@ -164,13 +164,11 @@ case_eq (x ?= y)%Z; intro H1; rewrite H1 in H. - discriminate. Qed. -Lemma Zcneqb_morph : forall x y : Z, Zeq_bool x y = false -> [x] ~= [y]. +Lemma Zcneqb_morph : forall x y : Z, Z.eqb x y = false -> [x] ~= [y]. Proof. -intros x y H. unfold Zeq_bool in H. -case_eq (Z.compare x y); intro H1; rewrite H1 in *; (discriminate || clear H). +intros x y []%Z.eqb_neq%Z.lt_gt_cases. - apply (Rlt_neq sor). now apply clt_morph. -- fold (x > y)%Z in H1. rewrite Z.gt_lt_iff in H1. - apply (Rneq_symm sor). apply (Rlt_neq sor). now apply clt_morph. +- apply (Rneq_symm sor). apply (Rlt_neq sor). now apply clt_morph. Qed. End InitialMorphism. diff --git a/stdlib/theories/micromega/ZMicromega.v b/stdlib/theories/micromega/ZMicromega.v index c863394e43fd..e16b64ad910d 100644 --- a/stdlib/theories/micromega/ZMicromega.v +++ b/stdlib/theories/micromega/ZMicromega.v @@ -751,22 +751,22 @@ Proof. case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros z z0 H z1 z2 H0 H1. inv H1. unfold ZgcdM at 1. - destruct (Zmax_spec (Z.gcd (ZgcdM z1 z2) z) 1) as [HH1 | HH1]; + destruct (Z.max_spec (Z.gcd (ZgcdM z1 z2) z) 1) as [HH1 | HH1]; cycle 1; destruct HH1 as [HH1 HH1'] ; rewrite HH1'. + constructor. * apply (Zdivide_pol_Zdivide _ (ZgcdM z1 z2)). -- unfold ZgcdM. - destruct (Zmax_spec (Z.gcd z1 z2) 1) as [HH2 | HH2]. + destruct (Z.max_spec (Z.gcd z1 z2) 1) as [HH2 | HH2]; cycle 1. ++ destruct HH2 as [H1 H2]. rewrite H2. apply Zdivide_pol_sub ; auto. apply Z.lt_le_trans with 1. ** reflexivity. - ** now apply Z.ge_le. + ** trivial. ++ destruct HH2 as [H1 H2]. rewrite H2. apply Zdivide_pol_one. -- unfold ZgcdM in HH1. unfold ZgcdM. - destruct (Zmax_spec (Z.gcd z1 z2) 1) as [HH2 | HH2]. + destruct (Z.max_spec (Z.gcd z1 z2) 1) as [HH2 | HH2]; cycle 1. ++ destruct HH2 as [H1 H2]. rewrite H2 in *. destruct (Zgcd_is_gcd (Z.gcd z1 z2) z); auto. ++ destruct HH2 as [H1 H2]. rewrite H2. @@ -1082,7 +1082,7 @@ Fixpoint bdepth (pf : ZArithProof) : nat := | ExProof _ p => S (bdepth p) end. -Require Import Wf_nat. +Require Import PeanoNat Wf_nat. Lemma in_bdepth : forall l a b y, In y l -> ltof ZArithProof bdepth y (EnumProof a b l). Proof. @@ -1159,13 +1159,13 @@ Proof. unfold makeCuttingPlane in H0. revert H0. case_eq (Zgcd_pol e) ; intros g c0. - generalize (Zgt_cases g 0) ; destruct (Z.gtb g 0). + case Z.gtb_spec. - intros H0 H1 H2. inv H2. change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in *. apply (Zgcd_pol_correct_lt _ env) in H1. 2: auto using Z.gt_lt. apply Z.le_add_le_sub_l, Z.ge_le; rewrite Z.add_0_r. - apply (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Z.sub e c0) g)) H0). + apply (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Z.sub e c0) g))); auto using Z.lt_gt. apply Z.le_ge. rewrite <- Z.sub_0_l. apply Z.le_sub_le_add_r. @@ -1196,7 +1196,7 @@ Proof. change (eval_pol env e = 0) in H2. case_eq (Z.gtb g 0). + intros H H3. - rewrite <- Zgt_is_gt_bool in H. + rewrite Z.gtb_lt in H. rewrite Zgcd_pol_correct_lt with (1:= H1) in H2. 2: auto using Z.gt_lt. unfold nformula_of_cutting_plane. change (eval_pol env (padd e' (Pc z)) = 0). @@ -1206,7 +1206,7 @@ Proof. simpl. rewrite andb_false_iff in H0. destruct H0 as [H0|H0]. - * rewrite Zgt_is_gt_bool in H ; congruence. + * rewrite <-Z.gtb_lt in H ; congruence. * rewrite andb_false_iff in H0. destruct H0 as [H0|H0]. -- rewrite negb_false_iff in H0. @@ -1272,7 +1272,7 @@ Proof. match goal with [ H' : negb (Z.eqb (Z.gcd g c) g) = true |- ?G ] => rename H' into H5 end. rewrite negb_true_iff in H5. apply Z.eqb_neq in H5. - rewrite <- Zgt_is_gt_bool in H3. + rewrite Z.gtb_lt in H3. rewrite negb_true_iff in H. apply Z.eqb_neq in H. change (eval_pol env p = 0) in H2. @@ -1280,7 +1280,7 @@ Proof. set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub p c) g)) in *; clearbody x. contradict H5. apply Zis_gcd_gcd. - * apply Z.lt_le_incl, Z.gt_lt; assumption. + * apply Z.lt_le_incl; assumption. * constructor; auto with zarith. exists (-x). rewrite Z.mul_opp_l, Z.mul_comm. @@ -1611,11 +1611,11 @@ Proof. revert z1 z2. induction pf as [|a pf IHpf];simpl ;intros z1 z2 Hfix x **. - revert Hfix. - now case (Z.gtb_spec); [ | easy ]; intros LT; elim (Zlt_not_le _ _ LT); transitivity x. + now case (Z.gtb_spec); [ | easy ]; intros LT; elim (Zorder.Zlt_not_le _ _ LT); transitivity x. - flatten_bool. match goal with [ H' : _ <= x <= _ |- _ ] => rename H' into H0 end. match goal with [ H' : FF pf (z1 + 1) z2 = true |- _ ] => rename H' into H2 end. - destruct (Z_le_lt_eq_dec _ _ (proj1 H0)) as [ LT | -> ]. + destruct (ZArith_dec.Z_le_lt_eq_dec _ _ (proj1 H0)) as [ LT | -> ]. 2: exists a; auto. rewrite <- Z.le_succ_l in LT. assert (LE: (Z.succ z1 <= x <= z2)%Z) by intuition. diff --git a/stdlib/theories/setoid_ring/Cring.v b/stdlib/theories/setoid_ring/Cring.v index 71391b526ee0..15a79bcdcda0 100644 --- a/stdlib/theories/setoid_ring/Cring.v +++ b/stdlib/theories/setoid_ring/Cring.v @@ -14,7 +14,7 @@ Require Import BinPos. Require Import BinList. Require Import Znumtheory. Require Export Morphisms Setoid Bool. -Require Import ZArith_base. +Require Import BinInt. Require Export Algebra_syntax. Require Export Ncring. Require Export Ncring_initial. @@ -67,8 +67,8 @@ intros. apply mk_art ;intros. Defined. Lemma cring_morph: - ring_morph zero one _+_ _*_ _-_ -_ _==_ - 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool + ring_morph zero one _+_ _*_ _-_ -_ _==_ + 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb Ncring_initial.gen_phiZ. intros. apply mkmorph ; intros; simpl; try reflexivity. - rewrite Ncring_initial.gen_phiZ_add; reflexivity. @@ -76,7 +76,7 @@ intros. apply mkmorph ; intros; simpl; try reflexivity. rewrite Ncring_initial.gen_phiZ_opp; reflexivity. - rewrite Ncring_initial.gen_phiZ_mul; reflexivity. - rewrite Ncring_initial.gen_phiZ_opp; reflexivity. -- rewrite (Zeqb_ok x y H). reflexivity. +- apply Z.eqb_eq in H. rewrite H. reflexivity. Defined. Lemma cring_power_theory : @@ -109,7 +109,7 @@ Ltac cring_gen := ring_setoid cring_eq_ext cring_almost_ring_theory - Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool + Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb Ncring_initial.gen_phiZ cring_morph N @@ -144,12 +144,11 @@ Ltac cring_simplify_aux lterm fv lexpr hyp := match lexpr with | ?e::?le => let t := constr:(@Ring_polynom.norm_subst - Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool Z.quotrem O nil e) in + Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb Z.quotrem O nil e) in let te := constr:(@Ring_polynom.Pphi_dev _ 0 1 _+_ _*_ _-_ -_ - - Z 0%Z 1%Z Zeq_bool + Z 0%Z 1%Z Z.eqb Ncring_initial.gen_phiZ get_signZ fv t) in let eq1 := fresh "ring" in @@ -167,7 +166,7 @@ Ltac cring_simplify_aux lterm fv lexpr hyp := ring_setoid cring_eq_ext cring_almost_ring_theory - Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool + Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb Ncring_initial.gen_phiZ cring_morph N @@ -190,7 +189,7 @@ Ltac cring_simplify_aux lterm fv lexpr hyp := pattern (@Ring_polynom.Pphi_dev _ 0 1 _+_ _*_ _-_ -_ - Z 0%Z 1%Z Zeq_bool + Z 0%Z 1%Z Z.eqb Ncring_initial.gen_phiZ get_signZ fv t'); match goal with @@ -205,8 +204,7 @@ Ltac cring_simplify_aux lterm fv lexpr hyp := rewrite eq1 in H; pattern (@Ring_polynom.Pphi_dev _ 0 1 _+_ _*_ _-_ -_ - - Z 0%Z 1%Z Zeq_bool + Z 0%Z 1%Z Z.eqb Ncring_initial.gen_phiZ get_signZ fv t') in H; match type of H with diff --git a/stdlib/theories/setoid_ring/Integral_domain.v b/stdlib/theories/setoid_ring/Integral_domain.v index bcaa0d8b509e..cec8f4385c45 100644 --- a/stdlib/theories/setoid_ring/Integral_domain.v +++ b/stdlib/theories/setoid_ring/Integral_domain.v @@ -9,7 +9,7 @@ (************************************************************************) Require Export Cring. - +Import BinNat. (* Definition of integral domains: commutative ring without zero divisor *) diff --git a/stdlib/theories/setoid_ring/Ncring.v b/stdlib/theories/setoid_ring/Ncring.v index 39819121290a..9199fd6d8301 100644 --- a/stdlib/theories/setoid_ring/Ncring.v +++ b/stdlib/theories/setoid_ring/Ncring.v @@ -14,7 +14,7 @@ Require Import Setoid. Require Import BinPos. Require Import BinNat. Require Export Morphisms Setoid Bool. -Require Export ZArith_base. +Require Export BinInt. Require Export Algebra_syntax. Set Implicit Arguments. diff --git a/stdlib/theories/setoid_ring/Ncring_initial.v b/stdlib/theories/setoid_ring/Ncring_initial.v index f09fda59fd7f..e662b63f3214 100644 --- a/stdlib/theories/setoid_ring/Ncring_initial.v +++ b/stdlib/theories/setoid_ring/Ncring_initial.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import ZArith_base. +Require Import BinInt. Require Import Zpow_def. Require Import BinInt. Require Import BinNat. @@ -21,6 +21,8 @@ Require Import Setoid. Require Export Ncring. Require Export Ncring_polynom. +Require Zbool. + Set Implicit Arguments. (* An object to return when an expression is not recognized as a constant *) @@ -153,14 +155,6 @@ Ltac rsimpl := simpl. destruct x;rsimpl; try rewrite same_gen; reflexivity. Qed. - Lemma gen_Zeqb_ok : forall x y, - Zeq_bool x y = true -> [x] == [y]. - Proof. - intros x y H7. - assert (H10 := Zeq_bool_eq x y H7);unfold IDphi in H10. - rewrite H10;reflexivity. - Qed. - Lemma gen_phiZ1_add_pos_neg : forall x y, gen_phiZ1 (Z.pos_sub x y) == gen_phiPOS1 x + -gen_phiPOS1 y. @@ -228,6 +222,11 @@ Global Instance gen_phiZ_morph : - apply gen_phiZ_ext. Defined. +#[deprecated(since="9.0")] +Lemma gen_Zeqb_ok : forall x y, + Z.eqb x y = true -> [x] == [y]. +Proof. intros x y ->%Z.eqb_eq; reflexivity. Qed. + End ZMORPHISM. #[global] diff --git a/stdlib/theories/setoid_ring/Ncring_tac.v b/stdlib/theories/setoid_ring/Ncring_tac.v index c0d3beaa71d5..37f8bba31d5a 100644 --- a/stdlib/theories/setoid_ring/Ncring_tac.v +++ b/stdlib/theories/setoid_ring/Ncring_tac.v @@ -165,8 +165,11 @@ Ltac lterm_goal g := | (_ ?t1 ?t2) => constr:(t1::t2::nil) end. -Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y. - intros x y H. rewrite (Zeq_bool_eq x y H). reflexivity. Qed. +Lemma Private_Zeqb_ok: forall x y : Z, Z.eqb x y = true -> x == y. +Proof. intros x y ->%Z.eqb_eq. reflexivity. Qed. + +#[deprecated(use=Z.eqb_eq, since="9.0")] +Notation Zeqb_ok := Private_Zeqb_ok (only parsing). Ltac reify_goal lvar lexpr lterm:= @@ -220,7 +223,7 @@ Ltac ring_gen := |- ?g => apply (@ring_correct Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (@gen_phiZ _ _ _ _ _ _ _ _ _) _ - (@comm _ _ _ _ _ _ _ _ _ _) Zeq_bool Zeqb_ok N (fun n:N => n) + (@comm _ _ _ _ _ _ _ _ _ _) Z.eqb Private_Zeqb_ok N (fun n:N => n) (@pow_N _ _ _ _ _ _ _ _ _)); [apply mkpow_th; reflexivity |vm_compute; reflexivity] @@ -240,7 +243,7 @@ Ltac ring_simplify_aux lterm fv lexpr hyp := match lexpr with | ?e::?le => (* e:PExpr Z est la réification de t0:R *) let t := constr:(@Ncring_polynom.norm_subst - Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z) Zops Zeq_bool e) in + Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z) Zops Z.eqb e) in (* t:Pol Z *) let te := constr:(@Ncring_polynom.Pphi Z @@ -258,7 +261,7 @@ Ltac ring_simplify_aux lterm fv lexpr hyp := [apply (@Ncring_polynom.norm_subst_ok Z _ 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z) _ _ 0 1 _+_ _*_ _-_ -_ _==_ _ _ Ncring_initial.gen_phiZ _ - (@comm _ 0 1 _+_ _*_ _-_ -_ _==_ _ _) _ Zeqb_ok); + (@comm _ 0 1 _+_ _*_ _-_ -_ _==_ _ _) _ Private_Zeqb_ok); apply mkpow_th; reflexivity | match hyp with | 1%nat => rewrite eq2 diff --git a/stdlib/theories/setoid_ring/RealField.v b/stdlib/theories/setoid_ring/RealField.v index 492db8c87bd7..d340075aa4d7 100644 --- a/stdlib/theories/setoid_ring/RealField.v +++ b/stdlib/theories/setoid_ring/RealField.v @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +Require Import PeanoNat. +Require Import BinNat. Require Import Nnat. Require Import ArithRing. Require Export Ring Field. diff --git a/stdlib/theories/setoid_ring/Ring_base.v b/stdlib/theories/setoid_ring/Ring_base.v index 9b0a6059b2f7..1dcfdbd6c2bd 100644 --- a/stdlib/theories/setoid_ring/Ring_base.v +++ b/stdlib/theories/setoid_ring/Ring_base.v @@ -10,7 +10,7 @@ (* This module gathers the necessary base to build an instance of the ring tactic. Abstract rings need more theory, depending on - ZArith_base. *) + BinInt. *) Declare ML Module "rocq-runtime.plugins.ring". Require Export Ring_theory. From 795809c16ddb392b3c7a612904e6d401009379a6 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 3 Jan 2025 21:41:16 +0000 Subject: [PATCH 4/5] changelog --- .../19792-zmicromega-without-zarith.rst | 4 ---- .../11-standard-library/19801-less-ZArith_base.rst | 10 ++++++++++ 2 files changed, 10 insertions(+), 4 deletions(-) delete mode 100644 doc/changelog/11-standard-library/19792-zmicromega-without-zarith.rst create mode 100644 doc/changelog/11-standard-library/19801-less-ZArith_base.rst diff --git a/doc/changelog/11-standard-library/19792-zmicromega-without-zarith.rst b/doc/changelog/11-standard-library/19792-zmicromega-without-zarith.rst deleted file mode 100644 index aa975eb38bc4..000000000000 --- a/doc/changelog/11-standard-library/19792-zmicromega-without-zarith.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Deprecated:** internal-to-be-internal module :g:`Ztac`; use `Lia` instead. - **Changed:** :g:`ZMicromega` to use :g:`Z.eqb` instead of :g:`Zeq_bool` - (`#19792 `_, - by Andres Erbsen). diff --git a/doc/changelog/11-standard-library/19801-less-ZArith_base.rst b/doc/changelog/11-standard-library/19801-less-ZArith_base.rst new file mode 100644 index 000000000000..40a5eb609a62 --- /dev/null +++ b/doc/changelog/11-standard-library/19801-less-ZArith_base.rst @@ -0,0 +1,10 @@ +- **Deprecated:** module :g:`ZArith_Base`, module :g:`Ztac`, and :g:`Zeq_bool`. + Use :g:`ZArith` (or :g:`BinInt`), :g:`Lia`, and :g:`Z.eqb` instead. + Reducing use of the deprecated modules in stdlib **changed** the transitive + dependencies of several stdlib files; you may now need to ``Require`` or + ``Import`` :g:`ZArith` or :g:`Lia`. + The definition of :g:`Zeq_bool` was also **changed** to be an alias for + :g:`Z.eqb`; this is expected to simplify simultaneous compatibility with 8.20 + and 9.0 + (`#19801 `_, + by Andres Erbsen). From 9af8e675c23deac98abf739bdf7485ccbe75fae0 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 6 Jan 2025 14:29:58 +0100 Subject: [PATCH 5/5] Add overlays --- dev/ci/user-overlays/19801-andres-erbsen-Zeq_bool.sh | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 dev/ci/user-overlays/19801-andres-erbsen-Zeq_bool.sh diff --git a/dev/ci/user-overlays/19801-andres-erbsen-Zeq_bool.sh b/dev/ci/user-overlays/19801-andres-erbsen-Zeq_bool.sh new file mode 100644 index 000000000000..40e4d817846f --- /dev/null +++ b/dev/ci/user-overlays/19801-andres-erbsen-Zeq_bool.sh @@ -0,0 +1,4 @@ +overlay flocq https://github.com/proux01/flocq coq_19801 19801 +overlay vst https://github.com/andres-erbsen/VST less-ZArith_base 19801 +overlay compcert https://github.com/andres-erbsen/CompCert less-ZArith_base 19801 +overlay coquelicot https://github.com/proux01/coquelicot coq_19801 19801