From 50d8da95f7bfd943ca7617b12c5cc057282be850 Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Mon, 18 Sep 2023 17:13:50 +0200 Subject: [PATCH 1/6] Remove deprecate files in Arith * Removed in Arith: - Div2.v - Even.v - Gt.v - Le.v - Lt.v - Max.v - Minus.v - Min.v - Mult.v - Plus.v * Removed Numbers/Natural/Peano/NPeano.v * Many "Require" statements involving these files removed in other parts of the library * Several deprecated lemmas removed in Arith/EqNat * Register commands moved from Arith_prebase to PeanoNat * Some test files had to change: - bugs/bug_13307.v - bugs/bug_1779.v - bugs/bug_4187.v - bugs/bug_4456.v - modules/Nat.v - success/Funind.v - success/RecTutorial.v - success/Require.v (Not sure about this one) - success/extraction.v - success/import_lib.v --- .../addendum/miscellaneous-extensions.rst | 2 +- test-suite/bugs/bug_13307.v | 2 +- test-suite/bugs/bug_1779.v | 18 +- test-suite/bugs/bug_4187.v | 3 +- test-suite/bugs/bug_4456.v | 4 +- test-suite/modules/Nat.v | 2 +- test-suite/success/Funind.v | 7 +- test-suite/success/RecTutorial.v | 2 - test-suite/success/Require.v | 5 +- test-suite/success/extraction.v | 7 +- test-suite/success/import_lib.v | 6 +- theories/Arith/Arith_base.v | 7 - theories/Arith/Arith_prebase.v | 16 -- theories/Arith/Between.v | 3 - theories/Arith/Compare.v | 2 - theories/Arith/Compare_dec.v | 3 - theories/Arith/Div2.v | 189 ------------ theories/Arith/EqNat.v | 39 --- theories/Arith/Euclid.v | 3 - theories/Arith/Even.v | 270 ------------------ theories/Arith/Factorial.v | 3 - theories/Arith/Gt.v | 99 ------- theories/Arith/Le.v | 82 ------ theories/Arith/Lt.v | 122 -------- theories/Arith/Max.v | 72 ----- theories/Arith/Min.v | 67 ----- theories/Arith/Minus.v | 81 ------ theories/Arith/Mult.v | 136 --------- theories/Arith/PeanoNat.v | 14 + theories/Arith/Peano_dec.v | 3 - theories/Arith/Plus.v | 150 ---------- theories/Arith/Wf_nat.v | 3 - theories/Bool/Bvector.v | 3 - theories/Logic/WKL.v | 3 - theories/NArith/Ndist.v | 3 - theories/Numbers/NatInt/NZDomain.v | 3 - theories/Numbers/Natural/Peano/NPeano.v | 154 ---------- theories/PArith/BinPos.v | 3 - theories/Reals/Alembert.v | 3 - theories/Reals/AltSeries.v | 3 - theories/Reals/ArithProp.v | 3 - theories/Reals/Cos_plus.v | 3 - theories/Reals/Exp_prop.v | 3 - theories/Reals/PSeries_reg.v | 3 - theories/Reals/PartSum.v | 3 - theories/Reals/Ranalysis5.v | 3 - theories/Reals/Rcomplete.v | 3 - theories/Reals/RiemannInt.v | 3 - theories/Reals/Rtrigo_def.v | 3 - theories/Reals/SeqProp.v | 3 - theories/Reals/SeqSeries.v | 3 - theories/Sets/Finite_sets_facts.v | 3 - theories/Sets/Image.v | 3 - theories/Sets/Infinite_sets.v | 3 - theories/Sets/Integers.v | 3 - theories/Sets/Multiset.v | 3 - theories/ZArith/Zcompare.v | 3 - theories/extraction/ExtrOcamlNatBigInt.v | 2 +- theories/extraction/ExtrOcamlNatInt.v | 2 +- theories/micromega/VarMap.v | 1 - theories/micromega/ZifyInst.v | 1 - theories/omega/PreOmega.v | 1 - theories/setoid_ring/ArithRing.v | 4 - 63 files changed, 42 insertions(+), 1617 deletions(-) delete mode 100644 theories/Arith/Div2.v delete mode 100644 theories/Arith/Even.v delete mode 100644 theories/Arith/Gt.v delete mode 100644 theories/Arith/Le.v delete mode 100644 theories/Arith/Lt.v delete mode 100644 theories/Arith/Max.v delete mode 100644 theories/Arith/Min.v delete mode 100644 theories/Arith/Minus.v delete mode 100644 theories/Arith/Mult.v delete mode 100644 theories/Arith/Plus.v delete mode 100644 theories/Numbers/Natural/Peano/NPeano.v diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index 8d70ffec0117..ad41022bda61 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -29,7 +29,7 @@ it provides the following command: .. coqtop:: all Require Coq.derive.Derive. - Require Import Coq.Numbers.Natural.Peano.NPeano. + Require Import PeanoNat. Section P. diff --git a/test-suite/bugs/bug_13307.v b/test-suite/bugs/bug_13307.v index 11252ebd8c49..2e8181fe6061 100644 --- a/test-suite/bugs/bug_13307.v +++ b/test-suite/bugs/bug_13307.v @@ -1,5 +1,5 @@ Module numbers. - From Coq Require Export EqdepFacts PArith NArith ZArith NPeano. + From Coq Require Export EqdepFacts PArith NArith ZArith. End numbers. Import numbers. diff --git a/test-suite/bugs/bug_1779.v b/test-suite/bugs/bug_1779.v index 95bb66b962e6..2e1d73cb4fe1 100644 --- a/test-suite/bugs/bug_1779.v +++ b/test-suite/bugs/bug_1779.v @@ -1,24 +1,24 @@ -Require Import Div2. +Require Import PeanoNat. -Lemma double_div2: forall n, div2 (double n) = n. +Lemma double_div2: forall n, Nat.div2 (Nat.double n) = n. exact (fun n => let _subcase := let _cofact := fun _ : 0 = 0 => refl_equal 0 in _cofact (let _fact := refl_equal 0 in _fact) in let _subcase0 := - fun (m : nat) (Hrec : div2 (double m) = m) => - let _fact := f_equal div2 (double_S m) in - let _eq := trans_eq _fact (refl_equal (S (div2 (double m)))) in + fun (m : nat) (Hrec : Nat.div2 (Nat.double m) = m) => + let _fact := f_equal Nat.div2 (Nat.double_S m) in + let _eq := trans_eq _fact (refl_equal (S (Nat.div2 (Nat.double m)))) in let _eq0 := trans_eq _eq (trans_eq - (f_equal (fun f : nat -> nat => f (div2 (double m))) + (f_equal (fun f : nat -> nat => f (Nat.div2 (Nat.double m))) (refl_equal S)) (f_equal S Hrec)) in _eq0 in - (fix _fix (__ : nat) : div2 (double __) = __ := - match __ as n return (div2 (double n) = n) with + (fix _fix (__ : nat) : Nat.div2 (Nat.double __) = __ := + match __ as n return (Nat.div2 (Nat.double n) = n) with | 0 => _subcase | S __0 => - (fun _hrec : div2 (double __0) = __0 => _subcase0 __0 _hrec) + (fun _hrec : Nat.div2 (Nat.double __0) = __0 => _subcase0 __0 _hrec) (_fix __0) end) n). Guarded. diff --git a/test-suite/bugs/bug_4187.v b/test-suite/bugs/bug_4187.v index d729d1a287f7..ca96a03ddb63 100644 --- a/test-suite/bugs/bug_4187.v +++ b/test-suite/bugs/bug_4187.v @@ -7,7 +7,6 @@ Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. Require Import Coq.Lists.List. Require Import Coq.Setoids.Setoid. -Require Import Coq.Numbers.Natural.Peano.NPeano. Global Set Implicit Arguments. Global Generalizable All Variables. Coercion is_true : bool >-> Sortclass. @@ -378,7 +377,7 @@ Section general. End general. Module Export BooleanRecognizer. -Import Coq.Numbers.Natural.Peano.NPeano. +Import Coq.Arith.PeanoNat. Import Coq.Arith.Compare_dec. Import Coq.Arith.Wf_nat. diff --git a/test-suite/bugs/bug_4456.v b/test-suite/bugs/bug_4456.v index 27e836dfdcec..f5e042ef379a 100644 --- a/test-suite/bugs/bug_4456.v +++ b/test-suite/bugs/bug_4456.v @@ -576,7 +576,7 @@ admit. Defined. Local Ltac t_parse_production_for := repeat match goal with - | [ H : (beq_nat _ _) = true |- _ ] => apply EqNat.beq_nat_true in H + | [ H : (Nat.eqb _ _) = true |- _ ] => apply ->Nat.eqb_eq in H | _ => progress subst | _ => solve [ constructor; assumption ] | [ H : minimal_parse_of_production _ _ _ nil |- _ ] => (inversion H; clear H) @@ -619,7 +619,7 @@ Defined. dec (minimal_parse_of_production (G := G) len0 valid str prod)) ( fun Hreachable str len Hlen pf - => match Utils.dec (beq_nat len 0) with + => match Utils.dec (Nat.eqb len 0) with | left H => inl _ | right H => inr (fun p => _) end) diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v index 8d6863da3e90..b7b89e9e577f 100644 --- a/test-suite/modules/Nat.v +++ b/test-suite/modules/Nat.v @@ -8,7 +8,7 @@ Lemma le_refl : forall n : nat, le n n. auto. Qed. -Require Import Le. +Require Import Arith. Lemma le_trans : forall n m k : nat, le n m -> le m k -> le n k. eauto with arith. diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v index c3615e8eccd0..9d06b256dc58 100644 --- a/test-suite/success/Funind.v +++ b/test-suite/success/Funind.v @@ -152,12 +152,11 @@ Function nat_equal_bool (n m : nat) {struct n} : bool := end. -Require Export Div2. Require Import Nat. -Functional Scheme div2_ind := Induction for div2 Sort Prop. -Lemma div2_inf : forall n : nat, div2 n <= n. +Functional Scheme div2_ind := Induction for Nat.div2 Sort Prop. +Lemma div2_inf : forall n : nat, Nat.div2 n <= n. intros n. - functional induction div2 n. + functional induction Nat.div2 n. auto. auto. diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 809f1c44d0a2..c79c2c313dd1 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -859,8 +859,6 @@ Defined. Print Acc. -Require Import Minus. - Fail Fixpoint div (x y:nat){struct x}: nat := if eq_nat_dec x 0 then 0 diff --git a/test-suite/success/Require.v b/test-suite/success/Require.v index de5987c4f773..79ade7f59dba 100644 --- a/test-suite/success/Require.v +++ b/test-suite/success/Require.v @@ -1,8 +1,7 @@ (* -*- coq-prog-args: ("-noinit"); -*- *) -Require Import Coq.Arith.Plus. -Require Coq.Arith.Minus. -Locate Library Coq.Arith.Minus. +Require Import Coq.Arith.PeanoNat. +Locate Library Coq.Arith.PeanoNat. (* Check that Init didn't get exported by the import above *) Fail Check nat. diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index a882ee81be03..8ef7d8bf34c1 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -322,10 +322,9 @@ Extraction test24. (** Coq term non strongly-normalizable after extraction *) -Require Import Gt. Definition loop (Ax:Acc gt 0) := (fix F (a:nat) (b:Acc gt a) {struct b} : nat := - F (S a) (Acc_inv b (S a) (gt_Sn_n a))) 0 Ax. + F (S a) (Acc_inv b (S a) (Nat.lt_succ_diag_r a))) 0 Ax. Extraction loop. (* let loop _ = let rec f a = @@ -684,5 +683,5 @@ Require Import Euclid ExtrOcamlNatBigInt. Definition test n m (H:m>0) := let (q,r,_,_) := eucl_dev m H n in Nat.compare n (q*m+r). -Recursive Extraction test fact pred minus max min Div2.div2. -Extraction TestCompile test fact pred minus max min Div2.div2. +Recursive Extraction test fact pred minus max min Nat.div2. +Extraction TestCompile test fact pred minus max min Nat.div2. diff --git a/test-suite/success/import_lib.v b/test-suite/success/import_lib.v index 5c587a2dfeb4..8a57fa70e455 100644 --- a/test-suite/success/import_lib.v +++ b/test-suite/success/import_lib.v @@ -3,16 +3,16 @@ Definition le_trans := 0. Module Test_Read. Module M. - Require Le. (* Reading without importing *) + Require PeanoNat. (* Reading without importing *) - Check Le.le_trans. + Check PeanoNat.Nat.le_trans. Lemma th0 : le_trans = 0. reflexivity. Qed. End M. - Check Le.le_trans. + Check PeanoNat.Nat.le_trans. Lemma th0 : le_trans = 0. reflexivity. diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v index c2630343c721..b5b62412f7a6 100644 --- a/theories/Arith/Arith_base.v +++ b/theories/Arith/Arith_base.v @@ -10,13 +10,6 @@ Require Export Arith_prebase. -Require Export Le. -Require Export Lt. -Require Export Plus. -Require Export Gt. -Require Export Minus. -Require Export Mult. - Require Export Factorial. Require Export Between. Require Export Peano_dec. diff --git a/theories/Arith/Arith_prebase.v b/theories/Arith/Arith_prebase.v index db411944ad95..612903a17d33 100644 --- a/theories/Arith/Arith_prebase.v +++ b/theories/Arith/Arith_prebase.v @@ -313,19 +313,3 @@ Hint Resolve Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r: arith. Hint Constructors Nat.Even_alt: arith. #[global] Hint Constructors Nat.Odd_alt: arith. - - -(* Register *) -#[local] -Definition lt_n_Sm_le := (fun n m => (proj1 (Nat.lt_succ_r n m))). -Register lt_n_Sm_le as num.nat.lt_n_Sm_le. -#[local] -Definition le_lt_n_Sm := (fun n m => (proj2 (Nat.lt_succ_r n m))). -Register le_lt_n_Sm as num.nat.le_lt_n_Sm. -#[local] -Definition lt_S_n := (fun n m => (proj2 (Nat.succ_lt_mono n m))). -Register lt_S_n as num.nat.lt_S_n. -Register Nat.le_lt_trans as num.nat.le_lt_trans. -#[local] -Definition pred_of_minus := (fun n => eq_sym (Nat.sub_1_r n)). -Register pred_of_minus as num.nat.pred_of_minus. diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index ae38a4a2507d..6fb5efb54a0e 100644 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -210,6 +210,3 @@ Section Between. Qed. End Between. - -(* TODO #14736 for compatibility only, should be removed after deprecation *) -Require Import Le Lt. diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index 1cb1274b3550..7ac3b81cf056 100644 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -56,5 +56,3 @@ Proof. Qed. Require Export Wf_nat. - -Require Export Min Max. diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 625f0cfe63d8..c35be9900ebd 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -250,6 +250,3 @@ Lemma leb_compare n m : (n <=? m) = true <-> (n ?= m) <> Gt. Proof. rewrite Nat.compare_le_iff. apply Nat.leb_le. Qed. - -(* TODO #14736 for compatibility only, should be removed after deprecation *) -Require Import Le Lt Gt. diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v deleted file mode 100644 index 14a1e228fbed..000000000000 --- a/theories/Arith/Div2.v +++ /dev/null @@ -1,189 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* Prop, - P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n. -Proof. - intros P H0 H1 H2. - fix ind_0_1_SS 1. - intros n; destruct n as [|[|n]]. - - exact H0. - - exact H1. - - apply H2, ind_0_1_SS. -Qed. -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete.")] -Notation ind_0_1_SS := ind_0_1_SS_stt. - -(** [0 n/2 < n] *) - -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.lt_div2 instead.")] -Notation lt_div2 := Nat.lt_div2 (only parsing). - -#[global] -Hint Resolve Nat.lt_div2: arith. - -(** Properties related to the parity *) - -#[local] -Definition even_div2_stt n : Nat.Even_alt n -> Nat.div2 n = Nat.div2 (S n). -Proof. - rewrite Nat.Even_alt_Even. intros (p,->). - rewrite Nat.div2_succ_double. apply Nat.div2_double. -Qed. -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.Even_div2 (together with Nat.Even_alt_Even) instead.")] -Notation even_div2 := even_div2_stt. - -#[local] -Definition odd_div2_stt n : Nat.Odd_alt n -> S (Nat.div2 n) = Nat.div2 (S n). -Proof. - rewrite Nat.Odd_alt_Odd. intros (p,->). - rewrite Nat.add_1_r, Nat.div2_succ_double. - simpl. f_equal. symmetry. apply Nat.div2_double. -Qed. -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.Odd_div2 (together with Nat.Odd_alt_Odd) instead.")] -Notation odd_div2 := odd_div2_stt. - -#[local] -Definition div2_even_stt n : Nat.div2 n = Nat.div2 (S n) -> Nat.Even_alt n. -Proof. - rewrite Nat.Even_alt_Even; apply Nat.div2_Even. -Qed. -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.div2_Even (together with Nat.Even_alt_Even) instead.")] -Notation div2_even := div2_even_stt. - -#[local] -Definition div2_odd_stt n : S (Nat.div2 n) = Nat.div2 (S n) -> Nat.Odd_alt n. -Proof. - rewrite Nat.Odd_alt_Odd; apply Nat.div2_Odd. -Qed. -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.div2_Odd (together with Nat.Odd_alt_Odd) instead.")] -Notation div2_odd := div2_odd_stt. - -#[global] -Hint Resolve even_div2_stt div2_even_stt odd_div2_stt div2_odd_stt: arith. - -#[local] -Definition even_odd_div2_stt n : - (Nat.Even_alt n <-> Nat.div2 n = Nat.div2 (S n)) /\ - (Nat.Odd_alt n <-> S (Nat.div2 n) = Nat.div2 (S n)). -Proof. - split; split; auto using div2_odd_stt, div2_even_stt, odd_div2_stt, even_div2_stt. -Qed. -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.Even_Odd_div2 (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation even_odd_div2 := even_odd_div2_stt. - - - -(** Properties related to the double ([2n]) *) - -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.double instead.")] -Notation double := Nat.double (only parsing). - -#[global] -Hint Unfold Nat.double: arith. - -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.double_S instead.")] -Notation double_S := Nat.double_S. - -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.double_add instead.")] -Notation double_plus := Nat.double_add. - -#[global] -Hint Resolve Nat.double_S: arith. - -#[local] -Definition even_odd_double_stt n : - (Nat.Even_alt n <-> n = Nat.double (Nat.div2 n)) /\ (Nat.Odd_alt n <-> n = S (Nat.double (Nat.div2 n))). -Proof. - rewrite Nat.Even_alt_Even, Nat.Odd_alt_Odd; apply Nat.Even_Odd_double. -Qed. -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.Even_Odd_double (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation even_odd_double := even_odd_double_stt. - -(** Specializations *) - -#[local] -Definition even_double_stt n : Nat.Even_alt n -> n = Nat.double (Nat.div2 n). -Proof proj1 (proj1 (even_odd_double_stt n)). -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.")] -Notation even_double := even_double_stt. - -#[local] -Definition double_even_stt n : n = Nat.double (Nat.div2 n) -> Nat.Even_alt n. -Proof proj2 (proj1 (even_odd_double_stt n)). -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.double_Even (together with Nat.Even_alt_Even) instead.")] -Notation double_even := double_even_stt. - -#[local] -Definition odd_double_stt n : Nat.Odd_alt n -> n = S (Nat.double (Nat.div2 n)). -Proof proj1 (proj2 (even_odd_double_stt n)). -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.")] -Notation odd_double := odd_double_stt. - -#[local] -Definition double_odd_stt n : n = S (Nat.double (Nat.div2 n)) -> Nat.Odd_alt n. -Proof proj2 (proj2 (even_odd_double_stt n)). -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.double_Odd (together with Nat.Odd_alt_Odd) instead.")] -Notation double_odd := double_odd_stt. - -#[global] -Hint Resolve even_double_stt double_even_stt odd_double_stt double_odd_stt: arith. - -(** Application: - - if [n] is even then there is a [p] such that [n = 2p] - - if [n] is odd then there is a [p] such that [n = 2p+1] - - (Immediate: it is [n/2]) *) - -#[local] -Definition even_2n_stt : forall n, Nat.Even_alt n -> {p : nat | n = Nat.double p}. -Proof. - intros n H. exists (Nat.div2 n). auto with arith. -Defined. -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.Even_alt_Even instead.")] -Notation even_2n := even_2n_stt. - -#[local] -Definition odd_S2n_stt : forall n, Nat.Odd_alt n -> {p : nat | n = S (Nat.double p)}. -Proof. - intros n H. exists (Nat.div2 n). auto with arith. -Defined. -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.Odd_alt_Odd instead.")] -Notation odd_S2n := odd_S2n_stt. - -(** Doubling before dividing by two brings back to the initial number. *) - -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.div2_double instead.")] -Notation div2_double := Nat.div2_double. -#[deprecated(since="8.16",note="The Arith.Div2 file is obsolete. Use Nat.div2_succ_double instead.")] -Notation div2_double_plus_one := Nat.div2_succ_double. - -(* TODO #15411 for compatibility only, should be removed after deprecation *) -Require Import Even. diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index 1f9ae75c1533..1689bbb40c6c 100644 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -61,42 +61,3 @@ Proof. - right; intro; trivial. - apply IHn. Defined. - - -(** * Boolean equality on [nat]. - - We reuse the one already defined in module [Nat]. - In scope [nat_scope], the notation "=?" can be used. *) - -#[deprecated(since="8.16",note="Use Nat.eqb instead.")] -Notation beq_nat := Nat.eqb (only parsing). - -#[deprecated(since="8.16",note="Use Nat.eqb_eq instead.")] -Notation beq_nat_true_iff := Nat.eqb_eq (only parsing). -#[deprecated(since="8.16",note="Use Nat.eqb_neq instead.")] -Notation beq_nat_false_iff := Nat.eqb_neq (only parsing). - -#[local] -Definition beq_nat_refl_stt := fun n => eq_sym (Nat.eqb_refl n). -Opaque beq_nat_refl_stt. -#[deprecated(since="8.16",note="Use Nat.eqb_refl (with symmetry of equality) instead.")] -Notation beq_nat_refl := beq_nat_refl_stt. - -#[local] -Definition beq_nat_true_stt := fun n m => proj1 (Nat.eqb_eq n m). -Opaque beq_nat_true_stt. -#[deprecated(since="8.16",note="Use the bidirectional version Nat.eqb_eq instead.")] -Notation beq_nat_true := beq_nat_true_stt. - -#[local] -Definition beq_nat_false_stt := fun n m => proj1 (Nat.eqb_neq n m). -Opaque beq_nat_false_stt. -#[deprecated(since="8.16",note="Use the bidirectional version Nat.eqb_neq instead.")] -Notation beq_nat_false := beq_nat_false_stt. - -(* previously was given as transparent *) -#[local] -Definition beq_nat_eq_stt := fun n m Heq => proj1 (Nat.eqb_eq n m) (eq_sym Heq). -Opaque beq_nat_eq_stt. -#[deprecated(since="8.16",note="Use the bidirectional version Nat.eqb_eq (with symmetry of equality) instead.")] -Notation beq_nat_eq := beq_nat_eq_stt. diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v index 8e4d27b7b42e..1c6c1de82f43 100644 --- a/theories/Arith/Euclid.v +++ b/theories/Arith/Euclid.v @@ -54,6 +54,3 @@ Proof. simpl; rewrite <- Nat.add_assoc, <- Heq, Nat.add_comm, Nat.sub_add; trivial. - exists m; exists 0; simpl; auto. Defined. - -(* TODO #14736 for compatibility only, should be removed after deprecation *) -Require Import Mult. diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v deleted file mode 100644 index 27599e584b71..000000000000 --- a/theories/Arith/Even.v +++ /dev/null @@ -1,270 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* Nat.Odd_alt n -> False. -Proof. - induction n. - - intros Ev Od. inversion Od. - - intros Ev Od. inversion Ev. inversion Od. auto with arith. -Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Even_Odd_False (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation not_even_and_odd := not_even_and_odd_stt (only parsing). - - -(** * Facts about [even] & [odd] wrt. [plus] *) - -#[deprecated(since="8.16",note="The Arith.Even file is obsolete.")] -Ltac parity2bool := - rewrite ?Nat.Even_alt_Even, ?Nat.Odd_alt_Odd, <- ?Nat.even_spec, <- ?Nat.odd_spec. - -#[local] -Ltac parity2bool_dep := - rewrite ?Nat.Even_alt_Even, ?Nat.Odd_alt_Odd, <- ?Nat.even_spec, <- ?Nat.odd_spec. - -#[deprecated(since="8.16",note="The Arith.Even file is obsolete.")] -Ltac parity_binop_spec := - rewrite ?Nat.even_add, ?Nat.odd_add, ?Nat.even_mul, ?Nat.odd_mul. - -#[local] -Ltac parity_binop_spec_dep := - rewrite ?Nat.even_add, ?Nat.odd_add, ?Nat.even_mul, ?Nat.odd_mul. - -#[deprecated(since="8.16",note="The Arith.Even file is obsolete.")] -Ltac parity_binop := - parity2bool_dep; parity_binop_spec_dep; unfold Nat.odd; - do 2 destruct Nat.even; simpl; tauto. - -#[local] -Ltac parity_binop_dep := - parity2bool_dep; parity_binop_spec_dep; unfold Nat.odd; - do 2 destruct Nat.even; simpl; tauto. - -#[local] -Definition even_plus_split_stt n m : - Nat.Even_alt (n + m) -> Nat.Even_alt n /\ Nat.Even_alt m \/ Nat.Odd_alt n /\ Nat.Odd_alt m. -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Even_add_split (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation even_plus_split := even_plus_split_stt. - -#[local] -Definition odd_plus_split_stt n m : - Nat.Odd_alt (n + m) -> Nat.Odd_alt n /\ Nat.Even_alt m \/ Nat.Even_alt n /\ Nat.Odd_alt m. -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Odd_add_split (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation odd_plus_split := odd_plus_split_stt. - -#[local] -Definition even_even_plus_stt n m: Nat.Even_alt n -> Nat.Even_alt m -> Nat.Even_alt (n + m). -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Even_Even_add (together with Nat.Even_alt_Even) instead.")] -Notation even_even_plus := even_even_plus_stt. - -#[local] -Definition odd_plus_l_stt n m : Nat.Odd_alt n -> Nat.Even_alt m -> Nat.Odd_alt (n + m). -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Odd_add_l (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation odd_plus_l := odd_plus_l_stt. - -#[local] -Definition odd_plus_r_stt n m : Nat.Even_alt n -> Nat.Odd_alt m -> Nat.Odd_alt (n + m). -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Odd_add_r (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation odd_plus_r := odd_plus_r_stt. - -#[local] -Definition odd_even_plus_stt n m : Nat.Odd_alt n -> Nat.Odd_alt m -> Nat.Even_alt (n + m). -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Odd_Odd_add instead.")] -Notation odd_even_plus := odd_even_plus_stt. - -#[local] -Definition even_plus_aux_stt n m : - (Nat.Odd_alt (n + m) <-> Nat.Odd_alt n /\ Nat.Even_alt m \/ Nat.Even_alt n /\ Nat.Odd_alt m) /\ - (Nat.Even_alt (n + m) <-> Nat.Even_alt n /\ Nat.Even_alt m \/ Nat.Odd_alt n /\ Nat.Odd_alt m). -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Even_add_aux (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation even_plus_aux := even_plus_aux_stt. - -#[local] -Definition even_plus_even_inv_r_stt n m : Nat.Even_alt (n + m) -> Nat.Even_alt n -> Nat.Even_alt m. -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Even_add_Even_inv_r (together with Nat.Even_alt_Even) instead.")] -Notation even_plus_even_inv_r := even_plus_even_inv_r_stt. - -#[local] -Definition even_plus_even_inv_l_stt n m : Nat.Even_alt (n + m) -> Nat.Even_alt m -> Nat.Even_alt n. -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Even_add_Even_inv_l (together with Nat.Even_alt_Even) instead.")] -Notation even_plus_even_inv_l := even_plus_even_inv_l_stt. - -#[local] -Definition even_plus_odd_inv_r_stt n m : Nat.Even_alt (n + m) -> Nat.Odd_alt n -> Nat.Odd_alt m. -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Even_add_Odd_inv_r (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation even_plus_odd_inv_r := even_plus_odd_inv_r_stt. - -#[local] -Definition even_plus_odd_inv_l_stt n m : Nat.Even_alt (n + m) -> Nat.Odd_alt m -> Nat.Odd_alt n. -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Even_add_Even_inv_l (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation even_plus_odd_inv_l := even_plus_odd_inv_l_stt. - -#[local] -Definition odd_plus_even_inv_l_stt n m : Nat.Odd_alt (n + m) -> Nat.Odd_alt m -> Nat.Even_alt n. -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Odd_add_Even_inv_l (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation odd_plus_even_inv_l := odd_plus_even_inv_l_stt. - -#[local] -Definition odd_plus_even_inv_r_stt n m : Nat.Odd_alt (n + m) -> Nat.Odd_alt n -> Nat.Even_alt m. -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Odd_add_Even_inv_r (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation odd_plus_even_inv_r := odd_plus_even_inv_r_stt. - -#[local] -Definition odd_plus_odd_inv_l_stt n m : Nat.Odd_alt (n + m) -> Nat.Even_alt m -> Nat.Odd_alt n. -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Odd_add_Odd_inv_l (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation odd_plus_odd_inv_l := odd_plus_odd_inv_l_stt. - -#[local] -Definition odd_plus_odd_inv_r_stt n m : Nat.Odd_alt (n + m) -> Nat.Even_alt n -> Nat.Odd_alt m. -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Odd_add_Odd_inv_r (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation odd_plus_odd_inv_r := odd_plus_odd_inv_r_stt. - - -(** * Facts about [even] and [odd] wrt. [mult] *) - -#[local] -Definition even_mult_aux_stt n m : - (Nat.Odd_alt (n * m) <-> Nat.Odd_alt n /\ Nat.Odd_alt m) /\ (Nat.Even_alt (n * m) <-> Nat.Even_alt n \/ Nat.Even_alt m). -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Even_mul_aux (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation even_mult_aux := even_mult_aux_stt. - -#[local] -Definition even_mult_l_stt n m : Nat.Even_alt n -> Nat.Even_alt (n * m). -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Even_mul_l (together with Nat.Even_alt_Even) instead.")] -Notation even_mult_l := even_mult_l_stt. - -#[local] -Definition even_mult_r_stt n m : Nat.Even_alt m -> Nat.Even_alt (n * m). -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Even_mul_r (together with Nat.Even_alt_Even) instead.")] -Notation even_mult_r := even_mult_r_stt. - -#[local] -Definition even_mult_inv_r_stt n m : Nat.Even_alt (n * m) -> Nat.Odd_alt n -> Nat.Even_alt m. -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Even_mul_inv_r (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation even_mult_inv_r := even_mult_inv_r_stt. - -#[local] -Definition even_mult_inv_l_stt n m : Nat.Even_alt (n * m) -> Nat.Odd_alt m -> Nat.Even_alt n. -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Even_mul_inv_l (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.")] -Notation even_mult_inv_l := even_mult_inv_l_stt. - -#[local] -Definition odd_mult_stt n m : Nat.Odd_alt n -> Nat.Odd_alt m -> Nat.Odd_alt (n * m). -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Odd_mul (together with Nat.Odd_alt_Odd) instead.")] -Notation odd_mult := odd_mult_stt. - -#[local] -Definition odd_mult_inv_l_stt n m : Nat.Odd_alt (n * m) -> Nat.Odd_alt n. -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Odd_mul_inv_l (together with Nat.Odd_alt_Odd) instead.")] -Notation odd_mult_inv_l := odd_mult_inv_l_stt. - -#[local] -Definition odd_mult_inv_r_stt n m : Nat.Odd_alt (n * m) -> Nat.Odd_alt m. -Proof. parity_binop_dep. Qed. -#[deprecated(since="8.16",note="The Arith.Even file is obsolete. Use Nat.Odd_mul_inv_r (together with Nat.Odd_alt_Odd) instead.")] -Notation odd_mult_inv_r := odd_mult_inv_r_stt. - -#[global] -Hint Resolve - even_even_plus_stt odd_even_plus_stt odd_plus_l_stt odd_plus_r_stt - even_mult_l_stt even_mult_r_stt even_mult_l_stt even_mult_r_stt odd_mult_stt : arith. diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 447ec175a073..795a55db3012 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -40,6 +40,3 @@ Proof. + trivial. + apply Nat.le_add_r. Qed. - -(* TODO #14736 for compatibility only, should be removed after deprecation *) -Require Import Plus Mult Lt. diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v deleted file mode 100644 index 6e29c2c5a1a9..000000000000 --- a/theories/Arith/Gt.v +++ /dev/null @@ -1,99 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* m -> n > m \/ m = n := fun n m Hgt => proj1 (Nat.lt_eq_cases m n) (proj2 (Nat.succ_le_mono m n) Hgt). -Opaque gt_S_stt. -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use the bidirectional version Nat.lt_eq_cases (together with Nat.succ_le_mono) instead.")] -Notation gt_S := gt_S_stt. -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use the bidirectional version Nat.lt_succ_lt_pred instead.")] -Notation gt_pred := Arith_prebase.gt_pred_stt. - -(** * Irreflexivity *) - -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use Nat.lt_irrefl instead.")] -Notation gt_irrefl := Arith_prebase.gt_irrefl_stt. - -(** * Asymmetry *) - -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use Nat.lt_asymm instead.")] -Notation gt_asym := Arith_prebase.gt_asym_stt. - -(** * Relating strict and large orders *) - -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use the bidirectional version Nat.le_ngt instead.")] -Notation le_not_gt := Arith_prebase.le_not_gt_stt. -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use the bidirectional version Nat.lt_nge instead.")] -Notation gt_not_le := Arith_prebase.gt_not_le_stt. -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use the bidirectional version Nat.le_succ_l instead.")] -Notation le_S_gt := Arith_prebase.le_S_gt_stt. -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use the bidirectional version Nat.succ_le_mono instead.")] -Notation gt_S_le := Arith_prebase.gt_S_le_stt. -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use the bidirectional version Nat.le_succ_l instead.")] -Notation gt_le_S := Arith_prebase.gt_le_S_stt. -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use the bidirectional version Nat.succ_le_mono instead.")] -Notation le_gt_S := Arith_prebase.le_gt_S_stt. - -(** * Transitivity *) - -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use Nat.lt_le_trans instead.")] -Notation le_gt_trans := Arith_prebase.le_gt_trans_stt. -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use Nat.le_lt_trans instead.")] -Notation gt_le_trans := Arith_prebase.gt_le_trans_stt. -#[local] -Definition gt_trans_stt : forall n m p, n > m -> m > p -> n > p := fun n m p Hgt1 Hgt2 => Nat.lt_trans p m n Hgt2 Hgt1. -Opaque gt_trans_stt. -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use Nat.lt_trans instead.")] -Notation gt_trans := gt_trans_stt. -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use Nat.lt_le_trans (together with Nat.succ_le_mono) instead.")] -Notation gt_trans_S := Arith_prebase.gt_trans_S_stt. - -(** * Comparison to 0 *) - -#[local] -Definition gt_0_eq_stt n : n > 0 \/ 0 = n. -Proof. destruct (Nat.eq_0_gt_0_cases n); auto. Qed. -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use Nat.eq_0_gt_0_cases (and commutativity of disjunction) instead.")] -Notation gt_0_eq := gt_0_eq_stt. -(* begin hide *) -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use Nat.eq_0_gt_0_cases (and commutativity of disjunction) instead.")] -Notation gt_O_eq := gt_0_eq_stt (only parsing). -(* end hide *) - -(** * Simplification and compatibility *) - -#[local] -Definition plus_gt_reg_l_stt : forall n m p, p + n > p + m -> n > m := fun n m p Hgt => proj2 (Nat.add_lt_mono_l m n p) Hgt. -Opaque plus_gt_reg_l_stt. -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.")] -Notation plus_gt_reg_l := plus_gt_reg_l_stt. -#[deprecated(since="8.16",note="The Arith.Gt file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.")] -Notation plus_gt_compat_l := Arith_prebase.plus_gt_compat_l_stt. - -Require Import Le Lt Plus. diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v deleted file mode 100644 index 80fd9e82c0cd..000000000000 --- a/theories/Arith/Le.v +++ /dev/null @@ -1,82 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* n <= m := Nat.lt_le_incl. -Opaque le_Sn_le_stt. -#[deprecated(since="8.16",note="The Arith.Le file is obsolete. Use Nat.lt_le_incl instead.")] -Notation le_Sn_le := le_Sn_le_stt. - -(** * Properties of [le] w.r.t predecessor *) - -#[deprecated(since="8.16",note="The Arith.Le file is obsolete. Use Nat.le_pred_l instead.")] -Notation le_pred_n := Nat.le_pred_l (only parsing). (* pred n <= n *) -#[deprecated(since="8.16",note="The Arith.Le file is obsolete. Use Nat.pred_le_mono instead.")] -Notation le_pred := Nat.pred_le_mono (only parsing). (* n<=m -> pred n <= pred m *) - -(** * A different elimination principle for the order on natural numbers *) - -#[local] -Definition le_elim_rel_stt : - forall P:nat -> nat -> Prop, - (forall p, P 0 p) -> - (forall p (q:nat), p <= q -> P p q -> P (S p) (S q)) -> - forall n m, n <= m -> P n m. -Proof. - intros P H0 HS n. - induction n; trivial. - intros m Le. elim Le; intuition auto with arith. -Qed. -#[deprecated(since="8.16",note="The Arith.Le file is obsolete.")] -Notation le_elim_rel := le_elim_rel_stt. - -(* begin hide *) -#[deprecated(since="8.16",note="The Arith.Le file is obsolete. Use Nat.le_0_l instead.")] -Notation le_O_n := Nat.le_0_l (only parsing). -#[deprecated(since="8.16",note="The Arith.Le file is obsolete. Use Nat.nle_succ_0 instead.")] -Notation le_Sn_O := Nat.nle_succ_0 (only parsing). -#[deprecated(since="8.16",note="The Arith.Le file is obsolete. Use the bidirectional version Nat.le_0_r (with symmetry of equality) instead.")] -Notation le_n_O_eq := Arith_prebase.le_n_0_eq_stt. -(* end hide *) diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v deleted file mode 100644 index f96c9fb1901b..000000000000 --- a/theories/Arith/Lt.v +++ /dev/null @@ -1,122 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* ~m n < S m *) -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.")] -Notation lt_n_S := Arith_prebase.lt_n_S_stt. -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.")] -Notation lt_S_n := Arith_prebase.lt_S_n_stt. - -(** * Predecessor *) - -#[local] -Definition S_pred_stt := fun n m Hlt => eq_sym (Nat.lt_succ_pred m n Hlt). -Opaque S_pred_stt. -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.")] -Notation S_pred := S_pred_stt. -#[local] -Definition S_pred_pos_stt := fun n Hlt => eq_sym (Nat.lt_succ_pred 0 n Hlt). -Opaque S_pred_pos_stt. -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.")] -Notation S_pred_pos := S_pred_pos_stt (only parsing). -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_lt_pred instead.")] -Notation lt_pred := Arith_prebase.lt_pred_stt. -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use Nat.lt_pred_l (together with Nat.neq_0_lt_0) instead.")] -Notation lt_pred_n_n := Arith_prebase.lt_pred_n_n_stt. - -(** * Transitivity properties *) - -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use Nat.lt_trans instead.")] -Notation lt_trans := Nat.lt_trans (only parsing). -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use Nat.lt_le_trans instead.")] -Notation lt_le_trans := Nat.lt_le_trans (only parsing). -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use Nat.le_lt_trans instead.")] -Notation le_lt_trans := Nat.le_lt_trans (only parsing). - -(** * Large = strict or equal *) - -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use Nat.lt_eq_cases instead.")] -Notation le_lt_or_eq_iff := Nat.lt_eq_cases (only parsing). -#[local] -Definition le_lt_or_eq_stt := fun n m => proj1 (Nat.lt_eq_cases n m). -Opaque le_lt_or_eq_stt. -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.")] -Notation le_lt_or_eq := le_lt_or_eq_stt. -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.")] -Notation lt_le_weak := Nat.lt_le_incl (only parsing). - -(** * Dichotomy *) - -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.")] -Notation le_or_lt := Nat.le_gt_cases (only parsing). (* n <= m \/ m < n *) -#[local] -Definition nat_total_order_stt := fun n m => proj1 (Nat.lt_gt_cases n m). -Opaque nat_total_order_stt. -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_gt_cases instead.")] -Notation nat_total_order := nat_total_order_stt. - -(* begin hide *) -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use Nat.lt_0_succ instead.")] -Notation lt_O_Sn := Nat.lt_0_succ (only parsing). -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use the bidirectional version Nat.neq_0_lt_0 (together with Nat.neq_sym) instead.")] -Notation neq_O_lt := Arith_prebase.neq_0_lt_stt. -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use the bidirectional version Nat.neq_0_lt_0 (together with Nat.neq_sym) instead.")] -Notation lt_O_neq := Arith_prebase.lt_0_neq_stt. -#[deprecated(since="8.16",note="The Arith.Lt file is obsolete. Use Nat.nlt_0_r instead.")] -Notation lt_n_O := Nat.nlt_0_r (only parsing). -(* end hide *) - -Require Import Le. diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v deleted file mode 100644 index 20220340caf6..000000000000 --- a/theories/Arith/Max.v +++ /dev/null @@ -1,72 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* eq_sym (Nat.sub_1_r n). -Opaque pred_of_minus_stt. -#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.sub_1_r (and symmetry of equality) instead.")] -Notation pred_of_minus:= pred_of_minus_stt. - -(** * Diagonal *) - -#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.sub_diag instead.")] -Notation minus_diag := Nat.sub_diag (only parsing). (* n - n = 0 *) -#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.sub_diag (and symmetry of equality) instead.")] -Notation minus_diag_reverse := Arith_prebase.minus_diag_reverse_stt. -#[local] -Definition minus_n_n_stt := fun n => eq_sym (Nat.sub_diag n). -Opaque minus_n_n_stt. -#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.sub_diag (and symmetry of equality) instead.")] -Notation minus_n_n := minus_n_n_stt. - -(** * Simplification *) - -#[deprecated(since="8.16",note="The Arith.Minus file is obsolete.")] -Notation minus_plus_simpl_l_reverse := Arith_prebase.minus_plus_simpl_l_reverse_stt. - -(** * Relation with plus *) - -#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.add_sub_eq_l (and symmetry of equality) instead.")] -Notation plus_minus := Arith_prebase.plus_minus_stt. -#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.add_sub (together with Nat.add_comm) instead.")] -Notation minus_plus := Arith_prebase.minus_plus_stt. -#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.")] -Notation le_plus_minus_r := Arith_prebase.le_plus_minus_r_stt. -#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.")] -Notation le_plus_minus := Arith_prebase.le_plus_minus_stt. - -(** * Relation with order *) - -#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.sub_le_mono_r instead.")] -Notation minus_le_compat_r := Nat.sub_le_mono_r (only parsing). (* n <= m -> n - p <= m - p. *) -#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.sub_le_mono_l instead.")] -Notation minus_le_compat_l := Nat.sub_le_mono_l (only parsing). (* n <= m -> p - m <= p - n. *) -#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.le_sub_l instead.")] -Notation le_minus := Nat.le_sub_l (only parsing). (* n - m <= n *) -#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.sub_lt instead.")] -Notation lt_minus := Nat.sub_lt (only parsing). (* m <= n -> 0 < m -> n-m < n *) -#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use the bidirectional version (Nat.lt_add_lt_sub_r 0) instead.")] -Notation lt_O_minus_lt := Arith_prebase.lt_O_minus_lt_stt. -#[local] -Definition not_le_minus_0_stt := fun n m Hn => proj2 (Nat.sub_0_le n m) (Nat.lt_le_incl _ _ (proj2 (Nat.lt_nge _ _) Hn)). -Opaque not_le_minus_0_stt. -#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.sub_0_le (together with Nat.lt_nge and Nat.lt_le_incl) instead.")] -Notation not_le_minus_0 := not_le_minus_0_stt. - -Require Import Lt Le. diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v deleted file mode 100644 index 7a7d3cf2d5ee..000000000000 --- a/theories/Arith/Mult.v +++ /dev/null @@ -1,136 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* proj1 (Nat.eq_mul_0 n m) Heq. -Opaque mult_is_O_stt. -#[deprecated(since="8.16",note="The Arith.Mult file is obsolete. Use the bidirectional version Nat.eq_mul_0 instead.")] -Notation mult_is_O := mult_is_O_stt. -#[local] -Definition mult_is_one_stt := fun n m Heq => proj1 (Nat.eq_mul_1 n m) Heq. -Opaque mult_is_one_stt. -#[deprecated(since="8.16",note="The Arith.Mult file is obsolete. Use the bidirectional version Nat.eq_mul_1 instead.")] -Notation mult_is_one := mult_is_one_stt. - -(** ** Multiplication and successor *) - -#[deprecated(since="8.16",note="The Arith.Mult file is obsolete. Use Nat.mul_succ_l instead.")] -Notation mult_succ_l := Nat.mul_succ_l (only parsing). (* S n * m = n * m + m *) -#[deprecated(since="8.16",note="The Arith.Mult file is obsolete. Use Nat.mul_succ_r instead.")] -Notation mult_succ_r := Nat.mul_succ_r (only parsing). (* n * S m = n * m + n *) - -(** * Compatibility with orders *) - -#[deprecated(since="8.16",note="The Arith.Mult file is obsolete.")] -Notation mult_O_le := Arith_prebase.mult_O_le_stt. -#[deprecated(since="8.16",note="The Arith.Mult file is obsolete. Use Nat.mul_le_mono_l instead.")] -Notation mult_le_compat_l := Nat.mul_le_mono_l (only parsing). -#[deprecated(since="8.16",note="The Arith.Mult file is obsolete. Use Nat.mul_le_mono_r instead.")] -Notation mult_le_compat_r := Nat.mul_le_mono_r (only parsing). -#[deprecated(since="8.16",note="The Arith.Mult file is obsolete. Use Nat.mul_le_mono instead.")] -Notation mult_le_compat := Nat.mul_le_mono (only parsing). -#[deprecated(since="8.16",note="The Arith.Mult file is obsolete. Use the bidirectional version (Nat.mul_lt_mono_pos_l (S _)) (together with Nat.lt_0_succ) instead.")] -Notation mult_S_lt_compat_l := Arith_prebase.mult_S_lt_compat_l_stt. -#[local] -Definition mult_lt_compat_l_stt := fun n m p Hlt Hp => proj1 (Nat.mul_lt_mono_pos_l p n m Hp) Hlt. -Opaque mult_lt_compat_l_stt. -#[deprecated(since="8.16",note="The Arith.Mult file is obsolete. Use the bidirectional version Nat.mul_lt_mono_pos_l instead.")] -Notation mult_lt_compat_l := mult_lt_compat_l_stt. -#[local] -Definition mult_lt_compat_r_stt := fun n m p Hlt Hp => proj1 (Nat.mul_lt_mono_pos_r p n m Hp) Hlt. -Opaque mult_lt_compat_r_stt. -#[deprecated(since="8.16",note="The Arith.Mult file is obsolete. Use the bidirectional version Nat.mul_lt_mono_pos_r instead.")] -Notation mult_lt_compat_r := mult_lt_compat_r_stt. -#[local] -Definition mult_S_le_reg_l_stt := fun n m p Hle => proj2 (Nat.mul_le_mono_pos_l m p (S n) (Nat.lt_0_succ n)) Hle. -Opaque mult_S_le_reg_l_stt. -#[deprecated(since="8.16",note="The Arith.Mult file is obsolete. Use the bidirectional version (Nat.mul_le_mono_pos_l _ _ (S _)) (together with Nat.lt_0_succ) instead.")] -Notation mult_S_le_reg_l := mult_S_le_reg_l_stt. - -(** * n|->2*n and n|->2n+1 have disjoint image *) - -#[local] -Definition odd_even_lem_stt p q : 2 * p + 1 <> 2 * q. -Proof. - intro. apply (Nat.Even_Odd_False (2*q)). - - now exists q. - - now exists p. -Qed. -#[deprecated(since="8.16",note="The Arith.Mult file is obsolete. Use Nat.Even_Odd_False instead.")] -Notation odd_even_lem := odd_even_lem_stt. - -(** * Tail-recursive [mult] *) - -#[deprecated(since="8.16",note="The Arith.Mult file is obsolete. Use Nat.tail_mul instead.")] -Notation tail_mult := Nat.tail_mul (only parsing). -#[local] -Definition mult_tail_mult_stt := fun n m => eq_sym (Nat.tail_mul_spec n m). -Opaque mult_tail_mult_stt. -#[deprecated(since="8.16",note="The Arith.Mult file is obsolete. Use Nat.tail_mul_spec (with symmetry of equality) instead.")] -Notation mult_tail_mult := mult_tail_mult_stt. -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete.")] -Ltac tail_simpl := - repeat rewrite Nat.tail_add_spec; repeat rewrite Nat.tail_mul_spec; simpl. - -Require Export Plus Minus Le Lt. diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v index 2ba19f3d1477..1d7db9434b11 100644 --- a/theories/Arith/PeanoNat.v +++ b/theories/Arith/PeanoNat.v @@ -1257,6 +1257,20 @@ Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope. #[global] Hint Unfold Nat.le : core. #[global] Hint Unfold Nat.lt : core. +(* Register *) +#[local] +Definition lt_n_Sm_le := (fun n m => (proj1 (Nat.lt_succ_r n m))). +Register lt_n_Sm_le as num.nat.lt_n_Sm_le. +#[local] +Definition le_lt_n_Sm := (fun n m => (proj2 (Nat.lt_succ_r n m))). +Register le_lt_n_Sm as num.nat.le_lt_n_Sm. +#[local] +Definition lt_S_n := (fun n m => (proj2 (Nat.succ_lt_mono n m))). +Register lt_S_n as num.nat.lt_S_n. +Register Nat.le_lt_trans as num.nat.le_lt_trans. +#[local] +Definition pred_of_minus := (fun n => eq_sym (Nat.sub_1_r n)). +Register pred_of_minus as num.nat.pred_of_minus. Register Nat.le_trans as num.nat.le_trans. Register Nat.nlt_0_r as num.nat.nlt_0_r. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 6e7a7e9c8821..3bee041e8fda 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -60,6 +60,3 @@ destruct le_mn1 as [|? le_mn1]; intros le_mn2; destruct le_mn2 as [|? le_mn2]. * now apply IHn0. * now rewrite H. Qed. - -(* TODO #14736 for compatibility only, should be removed after deprecation *) -Require Import Le Lt. diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v deleted file mode 100644 index 58de55204ad0..000000000000 --- a/theories/Arith/Plus.v +++ /dev/null @@ -1,150 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* proj1 (Nat.add_cancel_l n m p). -Opaque plus_reg_l_stt. -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_cancel_l instead.")] -Notation plus_reg_l := plus_reg_l_stt. -#[local] -Definition plus_le_reg_l_stt := fun n m p => proj2 (Nat.add_le_mono_l n m p). -Opaque plus_le_reg_l_stt. -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_le_mono_l instead.")] -Notation plus_le_reg_l := plus_le_reg_l_stt. -#[local] -Definition plus_lt_reg_l_stt := fun n m p => proj2 (Nat.add_lt_mono_l n m p). -Opaque plus_lt_reg_l_stt. -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.")] -Notation plus_lt_reg_l := plus_lt_reg_l_stt. - -(** * Compatibility with order *) - -#[local] -Definition plus_le_compat_l_stt := fun n m p => proj1 (Nat.add_le_mono_l n m p). -Opaque plus_le_compat_l_stt. -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_le_mono_l instead.")] -Notation plus_le_compat_l := plus_le_compat_l_stt. -#[local] -Definition plus_le_compat_r_stt := fun n m p => proj1 (Nat.add_le_mono_r n m p). -Opaque plus_le_compat_r_stt. -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_le_mono_r instead.")] -Notation plus_le_compat_r := plus_le_compat_r_stt. -#[local] -Definition plus_lt_compat_l_stt := fun n m p => proj1 (Nat.add_lt_mono_l n m p). -Opaque plus_lt_compat_l_stt. -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.")] -Notation plus_lt_compat_l := plus_lt_compat_l_stt. -#[local] -Definition plus_lt_compat_r_stt := fun n m p => proj1 (Nat.add_lt_mono_r n m p). -Opaque plus_lt_compat_r_stt. -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_r instead.")] -Notation plus_lt_compat_r := plus_lt_compat_r_stt. - -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use Nat.add_le_mono instead.")] -Notation plus_le_compat := Nat.add_le_mono (only parsing). -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use Nat.add_le_lt_mono instead.")] -Notation plus_le_lt_compat := Nat.add_le_lt_mono (only parsing). -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use Nat.add_lt_le_mono instead.")] -Notation plus_lt_le_compat := Nat.add_lt_le_mono (only parsing). -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use Nat.add_lt_mono instead.")] -Notation plus_lt_compat := Nat.add_lt_mono (only parsing). -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use Nat.le_add_r instead.")] -Notation le_plus_l := Nat.le_add_r (only parsing). -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use Nat.le_add_l (with arguments reversed) instead.")] -Notation le_plus_r := Arith_prebase.le_plus_r_stt. -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use Nat.le_add_r (together with Nat.le_trans) instead.")] -Notation le_plus_trans := Arith_prebase.le_plus_trans_stt. -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use Nat.le_add_r (together with Nat.lt_le_trans) instead.")] -Notation lt_plus_trans := Arith_prebase.lt_plus_trans_stt. - -(** * Inversion lemmas *) - -#[local] -Definition plus_is_O_stt := fun n m => proj1 (Nat.eq_add_0 n m). -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use the bidirectional version Nat.eq_add_0 instead.")] -Notation plus_is_O := plus_is_O_stt. - -#[local] -Definition plus_is_one_stt m n : - m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}. -Proof. - destruct m as [| m]; auto. - destruct m; auto. - discriminate. -Defined. -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use the Prop version Nat.eq_add_1 instead.")] -Notation plus_is_one := plus_is_one_stt. - -(** * Derived properties *) - -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use Nat.add_shuffle1 instead.")] -Notation plus_permute_2_in_4 := Nat.add_shuffle1 (only parsing). - -(** * Discrimination *) - -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use Nat.succ_add_discr instead.")] -Notation succ_plus_discr := Nat.succ_add_discr (only parsing). -#[local] -Definition n_SSn_stt : forall n, n <> S (S n) := fun n => Nat.succ_add_discr 1 n. -Opaque n_SSn_stt. -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use (Nat.succ_add_discr 1) instead.")] -Notation n_SSn := n_SSn_stt. -#[local] -Definition n_SSSn_stt : forall n, n <> S (S (S n)) := fun n => Nat.succ_add_discr 2 n. -Opaque n_SSSn_stt. -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use (Nat.succ_add_discr 2) instead.")] -Notation n_SSSn := n_SSSn_stt. -#[local] -Definition n_SSSSn_stt : forall n, n <> S (S (S (S n))) := fun n => Nat.succ_add_discr 3 n. -Opaque n_SSSSn_stt. -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use (Nat.succ_add_discr 3) instead.")] -Notation n_SSSSn := n_SSSSn_stt. - -(** * Tail-recursive [plus] *) -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use Nat.tail_add instead.")] -Notation tail_plus := Nat.tail_add (only parsing). -#[local] -Definition plus_tail_plus_stt := fun n m => eq_sym (Nat.tail_add_spec n m). -Opaque plus_tail_plus_stt. -#[deprecated(since="8.16",note="The Arith.Plus file is obsolete. Use Nat.tail_add_spec (with symmetry of equality) instead.")] -Notation plus_tail_plus := plus_tail_plus_stt. - -Require Import Le Lt. diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index a5b57cd747c1..a13bca830d80 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -271,6 +271,3 @@ Qed. Unset Implicit Arguments. Notation iter_nat n A f x := (nat_rect (fun _ => A) x (fun _ => f) n) (only parsing). - -(* TODO #14736 for compatibility only, should be removed after deprecation *) -Require Import Le Lt. diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 742e6a24ad92..d8a8276cb773 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -110,6 +110,3 @@ Infix "^|" := (BVor _) (at level 50, left associativity) : Bvector_scope Infix "=?" := (BVeq _ _) (at level 70, no associativity) : Bvector_scope. Open Scope Bvector_scope. End BvectorNotations. - -(* TODO #14736 for compatibility only, should be removed after deprecation *) -Require Import Minus. diff --git a/theories/Logic/WKL.v b/theories/Logic/WKL.v index aa12d3b13a39..5c95f49641da 100644 --- a/theories/Logic/WKL.v +++ b/theories/Logic/WKL.v @@ -270,6 +270,3 @@ intros P Hdec Hinf. apply inductively_barred_at_is_path_from_decidable in Hdec. apply PreWeakKonigsLemma; assumption. Qed. - -(* TODO #14736 for compatibility only, should be removed after deprecation *) -Require Import Le Lt. diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v index deeabff18835..3a92395ac236 100644 --- a/theories/NArith/Ndist.v +++ b/theories/NArith/Ndist.v @@ -394,6 +394,3 @@ Proof. - rewrite N.lxor_assoc. rewrite <- (N.lxor_assoc a'' a'' a'). rewrite N.lxor_nilpotent. rewrite N.lxor_0_l. reflexivity. Qed. - -(* TODO #14736 for compatibility only, should be removed after deprecation *) -Require Import Min. diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index 71a0effdff0b..c09c702044ac 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -379,6 +379,3 @@ Proof. Qed. End NZOfNatOps. - -(* TODO #14736 for compatibility only, should be removed after deprecation *) -Require Import Plus Minus. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v deleted file mode 100644 index d18b5d224a82..000000000000 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ /dev/null @@ -1,154 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* Date: Sun, 15 Oct 2023 09:34:54 +0200 Subject: [PATCH 2/6] Remove Arith_prebase The Hint database arith goes in Arith_base --- theories/Arith/Arith_base.v | 301 ++++++++++++++++++++++++++++++- theories/Arith/Arith_prebase.v | 315 --------------------------------- 2 files changed, 299 insertions(+), 317 deletions(-) delete mode 100644 theories/Arith/Arith_prebase.v diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v index b5b62412f7a6..1b58c3b8163b 100644 --- a/theories/Arith/Arith_base.v +++ b/theories/Arith/Arith_base.v @@ -8,8 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Export Arith_prebase. - +Require Export PeanoNat. Require Export Factorial. Require Export Between. Require Export Peano_dec. @@ -17,6 +16,8 @@ Require Export Compare_dec. Require Export EqNat. Require Export Wf_nat. +(** * [arith] hint database *) + (* ** [eq_nat] *) #[global] Hint Resolve eq_nat_refl: arith. @@ -29,3 +30,299 @@ Hint Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le in_int_S in_int_intro: arith. #[global] Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith. + +(** ** [lt] and [le] *) +#[global] +Hint Resolve Nat.le_trans: arith. (* Le.le_trans *) +#[global] +Hint Immediate Nat.le_antisymm: arith. (* Le.le_antisym *) +#[global] +Hint Resolve Nat.le_0_l Nat.nle_succ_0: arith. (* Le.le_0_n Le.le_Sn_0*) +#[global] +Hint Resolve Peano.le_n_S Nat.le_succ_diag_r Nat.nle_succ_diag_l : arith. (* Le.le_n_S Le.le_n_Sn Le.le_Sn_n *) +#[local] +Definition le_n_0_eq_stt := fun n Hle => eq_sym (proj1 (Nat.le_0_r n) Hle). +Opaque le_n_0_eq_stt. +#[global] +Hint Immediate le_n_0_eq_stt Nat.lt_le_incl Peano.le_S_n : arith. (* Le.le_n_0_eq Le.le_Sn_le Le.le_S_n *) +#[global] +Hint Resolve Nat.le_pred_l: arith. (* Le.le_pred_n *) +#[global] +Hint Resolve Nat.lt_irrefl: arith. (* Lt.lt_irrefl *) +#[local] +Definition lt_le_S_stt := fun n m => (proj2 (Nat.le_succ_l n m)). +Opaque lt_le_S_stt. +#[global] +Hint Immediate lt_le_S_stt: arith. (* Lt.lt_le_S *) +#[local] +Definition lt_n_Sm_le_stt := fun n m => (proj1 (Nat.lt_succ_r n m)). +Opaque lt_n_Sm_le_stt. +#[global] +Hint Immediate lt_n_Sm_le_stt: arith. (* Lt.lt_n_Sm_le *) +#[local] +Definition le_lt_n_Sm_stt := fun n m => (proj2 (Nat.lt_succ_r n m)). +Opaque le_lt_n_Sm_stt. +#[global] +Hint Immediate le_lt_n_Sm_stt: arith. (* Lt.le_lt_n_Sm *) +#[local] +Definition le_not_lt_stt := fun n m => (proj1 (Nat.le_ngt n m)). +Opaque le_not_lt_stt. +#[global] +Hint Immediate le_not_lt_stt: arith. (* Lt.le_not_lt *) +#[local] +Definition lt_not_le_stt := fun n m => (proj1 (Nat.lt_nge n m)). +Opaque lt_not_le_stt. +#[global] +Hint Immediate lt_not_le_stt: arith. (* Lt.lt_not_le *) +#[global] +Hint Resolve Nat.lt_0_succ Nat.nlt_0_r: arith. (* Lt.lt_0_Sn Lt.lt_n_0 *) +#[local] +Definition neq_0_lt_stt := fun n Hn => proj1 (Nat.neq_0_lt_0 n) (Nat.neq_sym 0 n Hn). +Opaque neq_0_lt_stt. +#[local] +Definition lt_0_neq_stt := fun n Hlt => Nat.neq_sym n 0 (proj2 (Nat.neq_0_lt_0 n) Hlt). +Opaque lt_0_neq_stt. +#[global] +Hint Immediate neq_0_lt_stt lt_0_neq_stt: arith. (* Lt.neq_0_lt Lt.lt_0_neq *) +#[global] +Hint Resolve Nat.lt_succ_diag_r Nat.lt_lt_succ_r: arith. (* Lt.lt_n_Sn Lt.lt_S *) +#[local] +Definition lt_n_S_stt := fun n m => (proj1 (Nat.succ_lt_mono n m)). +Opaque lt_n_S_stt. +#[global] +Hint Resolve lt_n_S_stt: arith. (* Lt.lt_n_S *) +#[local] +Definition lt_S_n_stt := fun n m => (proj2 (Nat.succ_lt_mono n m)). +Opaque lt_S_n_stt. +#[global] +Hint Immediate lt_S_n_stt: arith. (* Lt.lt_S_n *) +#[local] +Definition lt_pred_stt := fun n m => proj1 (Nat.lt_succ_lt_pred n m). +Opaque lt_pred_stt. +#[global] +Hint Immediate lt_pred_stt: arith. (* Lt.lt_pred *) +#[local] +Definition lt_pred_n_n_stt := fun n Hlt => Nat.lt_pred_l n (proj2 (Nat.neq_0_lt_0 n) Hlt). +Opaque lt_pred_n_n_stt. +#[global] +Hint Resolve lt_pred_n_n_stt: arith. (* Lt.lt_pred_n_n *) +#[global] +Hint Resolve Nat.lt_trans Nat.lt_le_trans Nat.le_lt_trans: arith. (* Lt.lt_trans Lt.lt_le_trans Lt.le_lt_trans *) +#[global] +Hint Immediate Nat.lt_le_incl: arith. (* Lt.lt_le_weak *) +#[local] +Definition gt_Sn_O_stt : forall n, S n > 0 := Nat.lt_0_succ. +Opaque gt_Sn_O_stt. +#[global] +Hint Resolve gt_Sn_O_stt: arith. (* Gt.gt_Sn_O *) +#[local] +Definition gt_Sn_n_stt : forall n, S n > n := Nat.lt_succ_diag_r. +Opaque gt_Sn_n_stt. +#[global] +Hint Resolve gt_Sn_n_stt: arith. (* Gt.gt_Sn_n *) +#[local] +Definition gt_n_S_stt : forall n m, n > m -> S n > S m := fun n m Hgt => proj1 (Nat.succ_lt_mono m n) Hgt. +Opaque gt_n_S_stt. +#[global] +Hint Resolve gt_n_S_stt: arith. (* Gt.gt_n_S *) +#[local] +Definition gt_S_n_stt : forall n m, S m > S n -> m > n := fun n m Hgt => proj2 (Nat.succ_lt_mono n m) Hgt. +Opaque gt_S_n_stt. +#[global] +Hint Immediate gt_S_n_stt: arith. (* Gt.gt_S_n *) +#[local] +Definition gt_pred_stt : forall n m, m > S n -> pred m > n := fun n m Hgt => proj1 (Nat.lt_succ_lt_pred n m) Hgt. +Opaque gt_pred_stt. +#[global] +Hint Immediate gt_pred_stt: arith. (* Gt.gt_pred *) +#[local] +Definition gt_irrefl_stt : forall n, ~ n > n := Nat.lt_irrefl. +Opaque gt_irrefl_stt. +#[global] +Hint Resolve gt_irrefl_stt: arith. (* Gt.gt_irrefl *) +#[local] +Definition gt_asym_stt : forall n m, n > m -> ~ m > n := fun n m => Nat.lt_asymm m n. +Opaque gt_asym_stt. +#[global] +Hint Resolve gt_asym_stt: arith. (* Gt.gt_asym *) +#[local] +Definition le_not_gt_stt : forall n m, n <= m -> ~ n > m := fun n m => proj1 (Nat.le_ngt n m). +Opaque le_not_gt_stt. +#[global] +Hint Resolve le_not_gt_stt: arith. (* Gt.le_not_gt *) +#[local] +Definition gt_not_le_stt: forall n m, n > m -> ~ n <= m := fun n m => proj1 (Nat.lt_nge m n). +Opaque gt_not_le_stt. +#[global] +Hint Resolve gt_not_le_stt: arith. (* Gt.gt_not_le *) +#[local] +Definition le_S_gt_stt: forall n m, S n <= m -> m > n := fun n m => proj1 (Nat.le_succ_l n m). +Opaque le_S_gt_stt. +#[global] +Hint Immediate le_S_gt_stt:arith. (* Gt.le_S_gt *) +#[local] +Definition gt_S_le_stt : forall n m, S m > n -> n <= m := fun n m => proj2 (Nat.succ_le_mono n m). +Opaque gt_S_le_stt. +#[global] +Hint Immediate gt_S_le_stt:arith. (* Gt.gt_S_le *) +#[local] +Definition gt_le_S_stt : forall n m, m > n -> S n <= m := fun n m => proj2 (Nat.le_succ_l n m). +Opaque gt_le_S_stt. +#[global] +Hint Resolve gt_le_S_stt:arith. (* Gt.gt_le_S *) +#[local] +Definition le_gt_S_stt : forall n m, n <= m -> S m > n := fun n m => proj1 (Nat.succ_le_mono n m). +Opaque le_gt_S_stt. +#[global] +Hint Resolve le_gt_S_stt:arith. (* Gt.le_gt_S *) +#[local] +Definition gt_trans_S_stt : forall n m p, S n > m -> m > p -> n > p + := fun n m p Hgt1 Hgt2 => Nat.lt_le_trans p m n Hgt2 (proj2 (Nat.succ_le_mono _ _) Hgt1). +Opaque gt_trans_S_stt. +#[global] +Hint Resolve gt_trans_S_stt:arith. (* Gt.gt_trans_S *) +#[local] +Definition le_gt_trans_stt : forall n m p, m <= n -> m > p -> n > p + := fun n m p Hle Hgt => Nat.lt_le_trans p m n Hgt Hle. +Opaque le_gt_trans_stt. +#[global] +Hint Resolve le_gt_trans_stt:arith. (* Gt.le_gt_trans *) +#[local] +Definition gt_le_trans_stt : forall n m p, n > m -> p <= m -> n > p + := fun n m p Hgt Hle => Nat.le_lt_trans p m n Hle Hgt. +Opaque gt_le_trans_stt. +#[global] +Hint Resolve gt_le_trans_stt:arith. (* Gt.gt_le_trans *) +#[local] +Definition plus_gt_compat_l_stt : forall n m p, n > m -> p + n > p + m + := fun n m p Hgt => proj1 (Nat.add_lt_mono_l m n p) Hgt. +Opaque plus_gt_compat_l_stt. +#[global] +Hint Resolve plus_gt_compat_l_stt:arith. (* Gt.plus_gt_compat_l *) + +(* ** [add] *) +#[global] +Hint Immediate Nat.add_comm : arith. (* Plus.plus_comm *) +#[global] +Hint Resolve Nat.add_assoc : arith. (* Plus.plus_assoc *) +#[local] +Definition plus_assoc_reverse_stt := fun n m p => eq_sym (Nat.add_assoc n m p). +Opaque plus_assoc_reverse_stt. +#[global] +Hint Resolve plus_assoc_reverse_stt : arith. (* Plus.plus_assoc_reverse *) +#[global] +Hint Resolve -> Nat.add_le_mono_l : arith. (* Plus.plus_le_compat_l *) +#[global] +Hint Resolve -> Nat.add_le_mono_r : arith. (* Plus.plus_le_compat_r *) +#[local] +Definition le_plus_r_stt := (fun n m => Nat.le_add_l m n). +#[local] +Definition le_plus_trans_stt := (fun n m p Hle => Nat.le_trans n _ _ Hle (Nat.le_add_r m p)). +Opaque le_plus_r_stt le_plus_trans_stt. +#[global] +Hint Resolve Nat.le_add_r le_plus_r_stt le_plus_trans_stt : arith. (* Plus.le_plus_l Plus.le_plus_r_stt Plus.le_plus_trans_stt *) +#[local] +Definition lt_plus_trans_stt := (fun n m p Hlt => Nat.lt_le_trans n _ _ Hlt (Nat.le_add_r m p)). +Opaque lt_plus_trans_stt. +#[global] +Hint Immediate lt_plus_trans_stt : arith. (* Plus.lt_plus_trans_stt *) +#[global] +Hint Resolve -> Nat.add_lt_mono_l : arith. (* Plus_lt_compat_l *) +#[global] +Hint Resolve -> Nat.add_lt_mono_r : arith. (* Plus_lt_compat_r *) + + +(* ** [sub] *) +#[local] +Definition minus_n_O_stt := fun n => eq_sym (Nat.sub_0_r n). +Opaque minus_n_O_stt. +#[global] +Hint Resolve minus_n_O_stt: arith. (* Minus.minus_n_O *) +#[local] +Definition minus_Sn_m_stt := fun n m Hle => eq_sym (Nat.sub_succ_l m n Hle). +Opaque minus_Sn_m_stt. +#[global] +Hint Resolve minus_Sn_m_stt: arith. (* Minus.minus_Sn_m *) +#[local] +Definition minus_diag_reverse_stt := fun n => eq_sym (Nat.sub_diag n). +Opaque minus_diag_reverse_stt. +#[global] +Hint Resolve minus_diag_reverse_stt: arith. (* Minus.minus_diag_reverse *) +#[local] +Definition minus_plus_simpl_l_reverse_stt n m p : n - m = p + n - (p + m). +Proof. + now rewrite Nat.sub_add_distr, Nat.add_comm, Nat.add_sub. +Qed. +#[global] +Hint Resolve minus_plus_simpl_l_reverse_stt: arith. (* Minus.minus_plus_simpl_l_reverse *) +#[local] +Definition plus_minus_stt := fun n m p Heq => eq_sym (Nat.add_sub_eq_l n m p (eq_sym Heq)). +Opaque plus_minus_stt. +#[global] +Hint Immediate plus_minus_stt: arith. (* Minus.plus_minus *) +#[local] +Definition minus_plus_stt := (fun n m => eq_ind _ (fun x => x - n = m) (Nat.add_sub m n) _ (Nat.add_comm _ _)). +Opaque minus_plus_stt. +#[global] +Hint Resolve minus_plus_stt: arith. (* Minus.minus_plus *) +#[local] +Definition le_plus_minus_stt := fun n m Hle => eq_sym (eq_trans (Nat.add_comm _ _) (Nat.sub_add n m Hle)). +Opaque le_plus_minus_stt. +#[global] +Hint Resolve le_plus_minus_stt: arith. (* Minus.le_plus_minus *) +#[local] +Definition le_plus_minus_r_stt := fun n m Hle => eq_trans (Nat.add_comm _ _) (Nat.sub_add n m Hle). +Opaque le_plus_minus_r_stt. +#[global] +Hint Resolve le_plus_minus_r_stt: arith. (* Minus.le_plus_minus_r *) +#[global] +Hint Resolve Nat.sub_lt: arith. (* Minus.lt_minus *) +#[local] +Definition lt_O_minus_lt_stt : forall n m, 0 < n - m -> m < n + := fun n m => proj2 (Nat.lt_add_lt_sub_r 0 n m). +Opaque lt_O_minus_lt_stt. +#[global] +Hint Immediate lt_O_minus_lt_stt: arith. (* Minus.lt_O_minus_lt *) + +(* ** [mul] *) +#[global] +Hint Resolve Nat.mul_1_l Nat.mul_1_r: arith. (* Mult.mult_1_l Mult.mult_1_r *) +#[global] +Hint Resolve Nat.mul_comm: arith. (* Mult.mult_comm *) +#[global] +Hint Resolve Nat.mul_add_distr_r: arith. (* Mult.mult_plus_distr_r *) +#[global] +Hint Resolve Nat.mul_sub_distr_r: arith. (* Mult.mult_minus_distr_r *) +#[global] +Hint Resolve Nat.mul_sub_distr_l: arith. (* Mult.mult_minus_distr_l *) +#[local] +Definition mult_assoc_reverse_stt := fun n m p => eq_sym (Nat.mul_assoc n m p). +Opaque mult_assoc_reverse_stt. +#[global] +Hint Resolve mult_assoc_reverse_stt Nat.mul_assoc: arith. (* Mult.mult_assoc_reverse Mult.mult_assoc *) +#[local] +Definition mult_O_le_stt n m : m = 0 \/ n <= m * n. +Proof. + destruct m; [left|right]; simpl; trivial using Nat.le_add_r. +Qed. +#[global] +Hint Resolve mult_O_le_stt: arith. (* Mult.mult_O_le *) +#[global] +Hint Resolve Nat.mul_le_mono_l: arith. (* Mult.mult_le_compat_l *) +#[local] +Definition mult_S_lt_compat_l_stt := (fun n m p Hlt => proj1 (Nat.mul_lt_mono_pos_l (S n) m p (Nat.lt_0_succ n)) Hlt). +Opaque mult_S_lt_compat_l_stt. +#[global] +Hint Resolve mult_S_lt_compat_l_stt: arith. (* Mult.mult_S_lt_compat_l *) + +(* ** [min] and [max] *) +#[global] +Hint Resolve Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r: arith. +#[global] +Hint Resolve Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r: arith. + +(* ** [Even_alt] and [Odd_alt] *) +#[global] +Hint Constructors Nat.Even_alt: arith. +#[global] +Hint Constructors Nat.Odd_alt: arith. diff --git a/theories/Arith/Arith_prebase.v b/theories/Arith/Arith_prebase.v deleted file mode 100644 index 612903a17d33..000000000000 --- a/theories/Arith/Arith_prebase.v +++ /dev/null @@ -1,315 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* eq_sym (proj1 (Nat.le_0_r n) Hle). -Opaque le_n_0_eq_stt. -#[global] -Hint Immediate le_n_0_eq_stt Nat.lt_le_incl Peano.le_S_n : arith. (* Le.le_n_0_eq Le.le_Sn_le Le.le_S_n *) -#[global] -Hint Resolve Nat.le_pred_l: arith. (* Le.le_pred_n *) -#[global] -Hint Resolve Nat.lt_irrefl: arith. (* Lt.lt_irrefl *) -#[local] -Definition lt_le_S_stt := fun n m => (proj2 (Nat.le_succ_l n m)). -Opaque lt_le_S_stt. -#[global] -Hint Immediate lt_le_S_stt: arith. (* Lt.lt_le_S *) -#[local] -Definition lt_n_Sm_le_stt := fun n m => (proj1 (Nat.lt_succ_r n m)). -Opaque lt_n_Sm_le_stt. -#[global] -Hint Immediate lt_n_Sm_le_stt: arith. (* Lt.lt_n_Sm_le *) -#[local] -Definition le_lt_n_Sm_stt := fun n m => (proj2 (Nat.lt_succ_r n m)). -Opaque le_lt_n_Sm_stt. -#[global] -Hint Immediate le_lt_n_Sm_stt: arith. (* Lt.le_lt_n_Sm *) -#[local] -Definition le_not_lt_stt := fun n m => (proj1 (Nat.le_ngt n m)). -Opaque le_not_lt_stt. -#[global] -Hint Immediate le_not_lt_stt: arith. (* Lt.le_not_lt *) -#[local] -Definition lt_not_le_stt := fun n m => (proj1 (Nat.lt_nge n m)). -Opaque lt_not_le_stt. -#[global] -Hint Immediate lt_not_le_stt: arith. (* Lt.lt_not_le *) -#[global] -Hint Resolve Nat.lt_0_succ Nat.nlt_0_r: arith. (* Lt.lt_0_Sn Lt.lt_n_0 *) -#[local] -Definition neq_0_lt_stt := fun n Hn => proj1 (Nat.neq_0_lt_0 n) (Nat.neq_sym 0 n Hn). -Opaque neq_0_lt_stt. -#[local] -Definition lt_0_neq_stt := fun n Hlt => Nat.neq_sym n 0 (proj2 (Nat.neq_0_lt_0 n) Hlt). -Opaque lt_0_neq_stt. -#[global] -Hint Immediate neq_0_lt_stt lt_0_neq_stt: arith. (* Lt.neq_0_lt Lt.lt_0_neq *) -#[global] -Hint Resolve Nat.lt_succ_diag_r Nat.lt_lt_succ_r: arith. (* Lt.lt_n_Sn Lt.lt_S *) -#[local] -Definition lt_n_S_stt := fun n m => (proj1 (Nat.succ_lt_mono n m)). -Opaque lt_n_S_stt. -#[global] -Hint Resolve lt_n_S_stt: arith. (* Lt.lt_n_S *) -#[local] -Definition lt_S_n_stt := fun n m => (proj2 (Nat.succ_lt_mono n m)). -Opaque lt_S_n_stt. -#[global] -Hint Immediate lt_S_n_stt: arith. (* Lt.lt_S_n *) -#[local] -Definition lt_pred_stt := fun n m => proj1 (Nat.lt_succ_lt_pred n m). -Opaque lt_pred_stt. -#[global] -Hint Immediate lt_pred_stt: arith. (* Lt.lt_pred *) -#[local] -Definition lt_pred_n_n_stt := fun n Hlt => Nat.lt_pred_l n (proj2 (Nat.neq_0_lt_0 n) Hlt). -Opaque lt_pred_n_n_stt. -#[global] -Hint Resolve lt_pred_n_n_stt: arith. (* Lt.lt_pred_n_n *) -#[global] -Hint Resolve Nat.lt_trans Nat.lt_le_trans Nat.le_lt_trans: arith. (* Lt.lt_trans Lt.lt_le_trans Lt.le_lt_trans *) -#[global] -Hint Immediate Nat.lt_le_incl: arith. (* Lt.lt_le_weak *) -#[local] -Definition gt_Sn_O_stt : forall n, S n > 0 := Nat.lt_0_succ. -Opaque gt_Sn_O_stt. -#[global] -Hint Resolve gt_Sn_O_stt: arith. (* Gt.gt_Sn_O *) -#[local] -Definition gt_Sn_n_stt : forall n, S n > n := Nat.lt_succ_diag_r. -Opaque gt_Sn_n_stt. -#[global] -Hint Resolve gt_Sn_n_stt: arith. (* Gt.gt_Sn_n *) -#[local] -Definition gt_n_S_stt : forall n m, n > m -> S n > S m := fun n m Hgt => proj1 (Nat.succ_lt_mono m n) Hgt. -Opaque gt_n_S_stt. -#[global] -Hint Resolve gt_n_S_stt: arith. (* Gt.gt_n_S *) -#[local] -Definition gt_S_n_stt : forall n m, S m > S n -> m > n := fun n m Hgt => proj2 (Nat.succ_lt_mono n m) Hgt. -Opaque gt_S_n_stt. -#[global] -Hint Immediate gt_S_n_stt: arith. (* Gt.gt_S_n *) -#[local] -Definition gt_pred_stt : forall n m, m > S n -> pred m > n := fun n m Hgt => proj1 (Nat.lt_succ_lt_pred n m) Hgt. -Opaque gt_pred_stt. -#[global] -Hint Immediate gt_pred_stt: arith. (* Gt.gt_pred *) -#[local] -Definition gt_irrefl_stt : forall n, ~ n > n := Nat.lt_irrefl. -Opaque gt_irrefl_stt. -#[global] -Hint Resolve gt_irrefl_stt: arith. (* Gt.gt_irrefl *) -#[local] -Definition gt_asym_stt : forall n m, n > m -> ~ m > n := fun n m => Nat.lt_asymm m n. -Opaque gt_asym_stt. -#[global] -Hint Resolve gt_asym_stt: arith. (* Gt.gt_asym *) -#[local] -Definition le_not_gt_stt : forall n m, n <= m -> ~ n > m := fun n m => proj1 (Nat.le_ngt n m). -Opaque le_not_gt_stt. -#[global] -Hint Resolve le_not_gt_stt: arith. (* Gt.le_not_gt *) -#[local] -Definition gt_not_le_stt: forall n m, n > m -> ~ n <= m := fun n m => proj1 (Nat.lt_nge m n). -Opaque gt_not_le_stt. -#[global] -Hint Resolve gt_not_le_stt: arith. (* Gt.gt_not_le *) -#[local] -Definition le_S_gt_stt: forall n m, S n <= m -> m > n := fun n m => proj1 (Nat.le_succ_l n m). -Opaque le_S_gt_stt. -#[global] -Hint Immediate le_S_gt_stt:arith. (* Gt.le_S_gt *) -#[local] -Definition gt_S_le_stt : forall n m, S m > n -> n <= m := fun n m => proj2 (Nat.succ_le_mono n m). -Opaque gt_S_le_stt. -#[global] -Hint Immediate gt_S_le_stt:arith. (* Gt.gt_S_le *) -#[local] -Definition gt_le_S_stt : forall n m, m > n -> S n <= m := fun n m => proj2 (Nat.le_succ_l n m). -Opaque gt_le_S_stt. -#[global] -Hint Resolve gt_le_S_stt:arith. (* Gt.gt_le_S *) -#[local] -Definition le_gt_S_stt : forall n m, n <= m -> S m > n := fun n m => proj1 (Nat.succ_le_mono n m). -Opaque le_gt_S_stt. -#[global] -Hint Resolve le_gt_S_stt:arith. (* Gt.le_gt_S *) -#[local] -Definition gt_trans_S_stt : forall n m p, S n > m -> m > p -> n > p - := fun n m p Hgt1 Hgt2 => Nat.lt_le_trans p m n Hgt2 (proj2 (Nat.succ_le_mono _ _) Hgt1). -Opaque gt_trans_S_stt. -#[global] -Hint Resolve gt_trans_S_stt:arith. (* Gt.gt_trans_S *) -#[local] -Definition le_gt_trans_stt : forall n m p, m <= n -> m > p -> n > p - := fun n m p Hle Hgt => Nat.lt_le_trans p m n Hgt Hle. -Opaque le_gt_trans_stt. -#[global] -Hint Resolve le_gt_trans_stt:arith. (* Gt.le_gt_trans *) -#[local] -Definition gt_le_trans_stt : forall n m p, n > m -> p <= m -> n > p - := fun n m p Hgt Hle => Nat.le_lt_trans p m n Hle Hgt. -Opaque gt_le_trans_stt. -#[global] -Hint Resolve gt_le_trans_stt:arith. (* Gt.gt_le_trans *) -#[local] -Definition plus_gt_compat_l_stt : forall n m p, n > m -> p + n > p + m - := fun n m p Hgt => proj1 (Nat.add_lt_mono_l m n p) Hgt. -Opaque plus_gt_compat_l_stt. -#[global] -Hint Resolve plus_gt_compat_l_stt:arith. (* Gt.plus_gt_compat_l *) - -(* ** [add] *) -#[global] -Hint Immediate Nat.add_comm : arith. (* Plus.plus_comm *) -#[global] -Hint Resolve Nat.add_assoc : arith. (* Plus.plus_assoc *) -#[local] -Definition plus_assoc_reverse_stt := fun n m p => eq_sym (Nat.add_assoc n m p). -Opaque plus_assoc_reverse_stt. -#[global] -Hint Resolve plus_assoc_reverse_stt : arith. (* Plus.plus_assoc_reverse *) -#[global] -Hint Resolve -> Nat.add_le_mono_l : arith. (* Plus.plus_le_compat_l *) -#[global] -Hint Resolve -> Nat.add_le_mono_r : arith. (* Plus.plus_le_compat_r *) -#[local] -Definition le_plus_r_stt := (fun n m => Nat.le_add_l m n). -#[local] -Definition le_plus_trans_stt := (fun n m p Hle => Nat.le_trans n _ _ Hle (Nat.le_add_r m p)). -Opaque le_plus_r_stt le_plus_trans_stt. -#[global] -Hint Resolve Nat.le_add_r le_plus_r_stt le_plus_trans_stt : arith. (* Plus.le_plus_l Plus.le_plus_r_stt Plus.le_plus_trans_stt *) -#[local] -Definition lt_plus_trans_stt := (fun n m p Hlt => Nat.lt_le_trans n _ _ Hlt (Nat.le_add_r m p)). -Opaque lt_plus_trans_stt. -#[global] -Hint Immediate lt_plus_trans_stt : arith. (* Plus.lt_plus_trans_stt *) -#[global] -Hint Resolve -> Nat.add_lt_mono_l : arith. (* Plus_lt_compat_l *) -#[global] -Hint Resolve -> Nat.add_lt_mono_r : arith. (* Plus_lt_compat_r *) - - -(* ** [sub] *) -#[local] -Definition minus_n_O_stt := fun n => eq_sym (Nat.sub_0_r n). -Opaque minus_n_O_stt. -#[global] -Hint Resolve minus_n_O_stt: arith. (* Minus.minus_n_O *) -#[local] -Definition minus_Sn_m_stt := fun n m Hle => eq_sym (Nat.sub_succ_l m n Hle). -Opaque minus_Sn_m_stt. -#[global] -Hint Resolve minus_Sn_m_stt: arith. (* Minus.minus_Sn_m *) -#[local] -Definition minus_diag_reverse_stt := fun n => eq_sym (Nat.sub_diag n). -Opaque minus_diag_reverse_stt. -#[global] -Hint Resolve minus_diag_reverse_stt: arith. (* Minus.minus_diag_reverse *) -#[local] -Definition minus_plus_simpl_l_reverse_stt n m p : n - m = p + n - (p + m). -Proof. - now rewrite Nat.sub_add_distr, Nat.add_comm, Nat.add_sub. -Qed. -#[global] -Hint Resolve minus_plus_simpl_l_reverse_stt: arith. (* Minus.minus_plus_simpl_l_reverse *) -#[local] -Definition plus_minus_stt := fun n m p Heq => eq_sym (Nat.add_sub_eq_l n m p (eq_sym Heq)). -Opaque plus_minus_stt. -#[global] -Hint Immediate plus_minus_stt: arith. (* Minus.plus_minus *) -#[local] -Definition minus_plus_stt := (fun n m => eq_ind _ (fun x => x - n = m) (Nat.add_sub m n) _ (Nat.add_comm _ _)). -Opaque minus_plus_stt. -#[global] -Hint Resolve minus_plus_stt: arith. (* Minus.minus_plus *) -#[local] -Definition le_plus_minus_stt := fun n m Hle => eq_sym (eq_trans (Nat.add_comm _ _) (Nat.sub_add n m Hle)). -Opaque le_plus_minus_stt. -#[global] -Hint Resolve le_plus_minus_stt: arith. (* Minus.le_plus_minus *) -#[local] -Definition le_plus_minus_r_stt := fun n m Hle => eq_trans (Nat.add_comm _ _) (Nat.sub_add n m Hle). -Opaque le_plus_minus_r_stt. -#[global] -Hint Resolve le_plus_minus_r_stt: arith. (* Minus.le_plus_minus_r *) -#[global] -Hint Resolve Nat.sub_lt: arith. (* Minus.lt_minus *) -#[local] -Definition lt_O_minus_lt_stt : forall n m, 0 < n - m -> m < n - := fun n m => proj2 (Nat.lt_add_lt_sub_r 0 n m). -Opaque lt_O_minus_lt_stt. -#[global] -Hint Immediate lt_O_minus_lt_stt: arith. (* Minus.lt_O_minus_lt *) - -(* ** [mul] *) -#[global] -Hint Resolve Nat.mul_1_l Nat.mul_1_r: arith. (* Mult.mult_1_l Mult.mult_1_r *) -#[global] -Hint Resolve Nat.mul_comm: arith. (* Mult.mult_comm *) -#[global] -Hint Resolve Nat.mul_add_distr_r: arith. (* Mult.mult_plus_distr_r *) -#[global] -Hint Resolve Nat.mul_sub_distr_r: arith. (* Mult.mult_minus_distr_r *) -#[global] -Hint Resolve Nat.mul_sub_distr_l: arith. (* Mult.mult_minus_distr_l *) -#[local] -Definition mult_assoc_reverse_stt := fun n m p => eq_sym (Nat.mul_assoc n m p). -Opaque mult_assoc_reverse_stt. -#[global] -Hint Resolve mult_assoc_reverse_stt Nat.mul_assoc: arith. (* Mult.mult_assoc_reverse Mult.mult_assoc *) -#[local] -Definition mult_O_le_stt n m : m = 0 \/ n <= m * n. -Proof. - destruct m; [left|right]; simpl; trivial using Nat.le_add_r. -Qed. -#[global] -Hint Resolve mult_O_le_stt: arith. (* Mult.mult_O_le *) -#[global] -Hint Resolve Nat.mul_le_mono_l: arith. (* Mult.mult_le_compat_l *) -#[local] -Definition mult_S_lt_compat_l_stt := (fun n m p Hlt => proj1 (Nat.mul_lt_mono_pos_l (S n) m p (Nat.lt_0_succ n)) Hlt). -Opaque mult_S_lt_compat_l_stt. -#[global] -Hint Resolve mult_S_lt_compat_l_stt: arith. (* Mult.mult_S_lt_compat_l *) - -(* ** [min] and [max] *) -#[global] -Hint Resolve Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r: arith. -#[global] -Hint Resolve Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r: arith. - -(* ** [Even_alt] and [Odd_alt] *) -#[global] -Hint Constructors Nat.Even_alt: arith. -#[global] -Hint Constructors Nat.Odd_alt: arith. From a6cfb17da725b6d871580afe8ade2425962e26a6 Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Sun, 15 Oct 2023 10:03:28 +0200 Subject: [PATCH 3/6] Search Blacklist lemmas in Arith_base --- theories/Arith/Arith_base.v | 45 +++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v index 1b58c3b8163b..ab40e3d07097 100644 --- a/theories/Arith/Arith_base.v +++ b/theories/Arith/Arith_base.v @@ -43,6 +43,7 @@ Hint Resolve Peano.le_n_S Nat.le_succ_diag_r Nat.nle_succ_diag_l : arith. (* Le. #[local] Definition le_n_0_eq_stt := fun n Hle => eq_sym (proj1 (Nat.le_0_r n) Hle). Opaque le_n_0_eq_stt. +Add Search Blacklist "Coq.Arith.Arith_base.le_n_0_eq_stt". #[global] Hint Immediate le_n_0_eq_stt Nat.lt_le_incl Peano.le_S_n : arith. (* Le.le_n_0_eq Le.le_Sn_le Le.le_S_n *) #[global] @@ -52,26 +53,31 @@ Hint Resolve Nat.lt_irrefl: arith. (* Lt.lt_irrefl *) #[local] Definition lt_le_S_stt := fun n m => (proj2 (Nat.le_succ_l n m)). Opaque lt_le_S_stt. +Add Search Blacklist "Coq.Arith.Arith_base.lt_le_S_stt". #[global] Hint Immediate lt_le_S_stt: arith. (* Lt.lt_le_S *) #[local] Definition lt_n_Sm_le_stt := fun n m => (proj1 (Nat.lt_succ_r n m)). Opaque lt_n_Sm_le_stt. +Add Search Blacklist "Coq.Arith.Arith_base.lt_n_Sm_le_stt". #[global] Hint Immediate lt_n_Sm_le_stt: arith. (* Lt.lt_n_Sm_le *) #[local] Definition le_lt_n_Sm_stt := fun n m => (proj2 (Nat.lt_succ_r n m)). Opaque le_lt_n_Sm_stt. +Add Search Blacklist "Coq.Arith.Arith_base.le_lt_n_Sm_stt". #[global] Hint Immediate le_lt_n_Sm_stt: arith. (* Lt.le_lt_n_Sm *) #[local] Definition le_not_lt_stt := fun n m => (proj1 (Nat.le_ngt n m)). Opaque le_not_lt_stt. +Add Search Blacklist "Coq.Arith.Arith_base.le_not_lt_stt". #[global] Hint Immediate le_not_lt_stt: arith. (* Lt.le_not_lt *) #[local] Definition lt_not_le_stt := fun n m => (proj1 (Nat.lt_nge n m)). Opaque lt_not_le_stt. +Add Search Blacklist "Coq.Arith.Arith_base.lt_not_le_stt". #[global] Hint Immediate lt_not_le_stt: arith. (* Lt.lt_not_le *) #[global] @@ -79,9 +85,11 @@ Hint Resolve Nat.lt_0_succ Nat.nlt_0_r: arith. (* Lt.lt_0_Sn Lt.lt_n_0 *) #[local] Definition neq_0_lt_stt := fun n Hn => proj1 (Nat.neq_0_lt_0 n) (Nat.neq_sym 0 n Hn). Opaque neq_0_lt_stt. +Add Search Blacklist "Coq.Arith.Arith_base.neq_0_lt_stt". #[local] Definition lt_0_neq_stt := fun n Hlt => Nat.neq_sym n 0 (proj2 (Nat.neq_0_lt_0 n) Hlt). Opaque lt_0_neq_stt. +Add Search Blacklist "Coq.Arith.Arith_base.lt_0_neq_stt". #[global] Hint Immediate neq_0_lt_stt lt_0_neq_stt: arith. (* Lt.neq_0_lt Lt.lt_0_neq *) #[global] @@ -89,21 +97,25 @@ Hint Resolve Nat.lt_succ_diag_r Nat.lt_lt_succ_r: arith. (* Lt.lt_n_Sn Lt.lt_S * #[local] Definition lt_n_S_stt := fun n m => (proj1 (Nat.succ_lt_mono n m)). Opaque lt_n_S_stt. +Add Search Blacklist "Coq.Arith.Arith_base.lt_n_S_stt". #[global] Hint Resolve lt_n_S_stt: arith. (* Lt.lt_n_S *) #[local] Definition lt_S_n_stt := fun n m => (proj2 (Nat.succ_lt_mono n m)). Opaque lt_S_n_stt. +Add Search Blacklist "Coq.Arith.Arith_base.lt_S_n_stt". #[global] Hint Immediate lt_S_n_stt: arith. (* Lt.lt_S_n *) #[local] Definition lt_pred_stt := fun n m => proj1 (Nat.lt_succ_lt_pred n m). Opaque lt_pred_stt. +Add Search Blacklist "Coq.Arith.Arith_base.lt_pred_stt". #[global] Hint Immediate lt_pred_stt: arith. (* Lt.lt_pred *) #[local] Definition lt_pred_n_n_stt := fun n Hlt => Nat.lt_pred_l n (proj2 (Nat.neq_0_lt_0 n) Hlt). Opaque lt_pred_n_n_stt. +Add Search Blacklist "Coq.Arith.Arith_base.lt_pred_n_n_stt". #[global] Hint Resolve lt_pred_n_n_stt: arith. (* Lt.lt_pred_n_n *) #[global] @@ -113,90 +125,107 @@ Hint Immediate Nat.lt_le_incl: arith. (* Lt.lt_le_weak *) #[local] Definition gt_Sn_O_stt : forall n, S n > 0 := Nat.lt_0_succ. Opaque gt_Sn_O_stt. +Add Search Blacklist "Coq.Arith.Arith_base.gt_Sn_O_stt". #[global] Hint Resolve gt_Sn_O_stt: arith. (* Gt.gt_Sn_O *) #[local] Definition gt_Sn_n_stt : forall n, S n > n := Nat.lt_succ_diag_r. Opaque gt_Sn_n_stt. +Add Search Blacklist "Coq.Arith.Arith_base.gt_Sn_n_stt". #[global] Hint Resolve gt_Sn_n_stt: arith. (* Gt.gt_Sn_n *) #[local] Definition gt_n_S_stt : forall n m, n > m -> S n > S m := fun n m Hgt => proj1 (Nat.succ_lt_mono m n) Hgt. Opaque gt_n_S_stt. +Add Search Blacklist "Coq.Arith.Arith_base.gt_n_S_stt". #[global] Hint Resolve gt_n_S_stt: arith. (* Gt.gt_n_S *) #[local] Definition gt_S_n_stt : forall n m, S m > S n -> m > n := fun n m Hgt => proj2 (Nat.succ_lt_mono n m) Hgt. Opaque gt_S_n_stt. +Add Search Blacklist "Coq.Arith.Arith_base.gt_S_n_stt". #[global] Hint Immediate gt_S_n_stt: arith. (* Gt.gt_S_n *) #[local] Definition gt_pred_stt : forall n m, m > S n -> pred m > n := fun n m Hgt => proj1 (Nat.lt_succ_lt_pred n m) Hgt. Opaque gt_pred_stt. +Add Search Blacklist "Coq.Arith.Arith_base.gt_pred_stt". #[global] Hint Immediate gt_pred_stt: arith. (* Gt.gt_pred *) #[local] Definition gt_irrefl_stt : forall n, ~ n > n := Nat.lt_irrefl. Opaque gt_irrefl_stt. +Add Search Blacklist "Coq.Arith.Arith_base.gt_irrefl_stt". #[global] Hint Resolve gt_irrefl_stt: arith. (* Gt.gt_irrefl *) #[local] Definition gt_asym_stt : forall n m, n > m -> ~ m > n := fun n m => Nat.lt_asymm m n. Opaque gt_asym_stt. +Add Search Blacklist "Coq.Arith.Arith_base.gt_asym_stt". #[global] Hint Resolve gt_asym_stt: arith. (* Gt.gt_asym *) #[local] Definition le_not_gt_stt : forall n m, n <= m -> ~ n > m := fun n m => proj1 (Nat.le_ngt n m). Opaque le_not_gt_stt. +Add Search Blacklist "Coq.Arith.Arith_base.le_not_gt_stt". #[global] Hint Resolve le_not_gt_stt: arith. (* Gt.le_not_gt *) #[local] Definition gt_not_le_stt: forall n m, n > m -> ~ n <= m := fun n m => proj1 (Nat.lt_nge m n). Opaque gt_not_le_stt. +Add Search Blacklist "Coq.Arith.Arith_base.gt_not_le_stt". #[global] Hint Resolve gt_not_le_stt: arith. (* Gt.gt_not_le *) #[local] Definition le_S_gt_stt: forall n m, S n <= m -> m > n := fun n m => proj1 (Nat.le_succ_l n m). Opaque le_S_gt_stt. +Add Search Blacklist "Coq.Arith.Arith_base.le_S_gt_stt". #[global] Hint Immediate le_S_gt_stt:arith. (* Gt.le_S_gt *) #[local] Definition gt_S_le_stt : forall n m, S m > n -> n <= m := fun n m => proj2 (Nat.succ_le_mono n m). Opaque gt_S_le_stt. +Add Search Blacklist "Coq.Arith.Arith_base.gt_S_le_stt". #[global] Hint Immediate gt_S_le_stt:arith. (* Gt.gt_S_le *) #[local] Definition gt_le_S_stt : forall n m, m > n -> S n <= m := fun n m => proj2 (Nat.le_succ_l n m). Opaque gt_le_S_stt. +Add Search Blacklist "Coq.Arith.Arith_base.gt_le_S_stt". #[global] Hint Resolve gt_le_S_stt:arith. (* Gt.gt_le_S *) #[local] Definition le_gt_S_stt : forall n m, n <= m -> S m > n := fun n m => proj1 (Nat.succ_le_mono n m). Opaque le_gt_S_stt. +Add Search Blacklist "Coq.Arith.Arith_base.le_gt_S_stt". #[global] Hint Resolve le_gt_S_stt:arith. (* Gt.le_gt_S *) #[local] Definition gt_trans_S_stt : forall n m p, S n > m -> m > p -> n > p := fun n m p Hgt1 Hgt2 => Nat.lt_le_trans p m n Hgt2 (proj2 (Nat.succ_le_mono _ _) Hgt1). Opaque gt_trans_S_stt. +Add Search Blacklist "Coq.Arith.Arith_base.gt_trans_S_stt". #[global] Hint Resolve gt_trans_S_stt:arith. (* Gt.gt_trans_S *) #[local] Definition le_gt_trans_stt : forall n m p, m <= n -> m > p -> n > p := fun n m p Hle Hgt => Nat.lt_le_trans p m n Hgt Hle. Opaque le_gt_trans_stt. +Add Search Blacklist "Coq.Arith.Arith_base.le_gt_trans_stt". #[global] Hint Resolve le_gt_trans_stt:arith. (* Gt.le_gt_trans *) #[local] Definition gt_le_trans_stt : forall n m p, n > m -> p <= m -> n > p := fun n m p Hgt Hle => Nat.le_lt_trans p m n Hle Hgt. Opaque gt_le_trans_stt. +Add Search Blacklist "Coq.Arith.Arith_base.gt_le_trans_stt". #[global] Hint Resolve gt_le_trans_stt:arith. (* Gt.gt_le_trans *) #[local] Definition plus_gt_compat_l_stt : forall n m p, n > m -> p + n > p + m := fun n m p Hgt => proj1 (Nat.add_lt_mono_l m n p) Hgt. Opaque plus_gt_compat_l_stt. +Add Search Blacklist "Coq.Arith.Arith_base.plus_gt_compat_l_stt". #[global] Hint Resolve plus_gt_compat_l_stt:arith. (* Gt.plus_gt_compat_l *) @@ -208,6 +237,7 @@ Hint Resolve Nat.add_assoc : arith. (* Plus.plus_assoc *) #[local] Definition plus_assoc_reverse_stt := fun n m p => eq_sym (Nat.add_assoc n m p). Opaque plus_assoc_reverse_stt. +Add Search Blacklist "Coq.Arith.Arith_base.plus_assoc_reverse_stt". #[global] Hint Resolve plus_assoc_reverse_stt : arith. (* Plus.plus_assoc_reverse *) #[global] @@ -219,11 +249,14 @@ Definition le_plus_r_stt := (fun n m => Nat.le_add_l m n). #[local] Definition le_plus_trans_stt := (fun n m p Hle => Nat.le_trans n _ _ Hle (Nat.le_add_r m p)). Opaque le_plus_r_stt le_plus_trans_stt. +Add Search Blacklist "Coq.Arith.Arith_base.le_plus_r_stt". +Add Search Blacklist "Coq.Arith.Arith_base.le_plus_trans_stt". #[global] Hint Resolve Nat.le_add_r le_plus_r_stt le_plus_trans_stt : arith. (* Plus.le_plus_l Plus.le_plus_r_stt Plus.le_plus_trans_stt *) #[local] Definition lt_plus_trans_stt := (fun n m p Hlt => Nat.lt_le_trans n _ _ Hlt (Nat.le_add_r m p)). Opaque lt_plus_trans_stt. +Add Search Blacklist "Coq.Arith.Arith_base.lt_plus_trans_stt". #[global] Hint Immediate lt_plus_trans_stt : arith. (* Plus.lt_plus_trans_stt *) #[global] @@ -236,16 +269,19 @@ Hint Resolve -> Nat.add_lt_mono_r : arith. (* Plus_lt_compat_r *) #[local] Definition minus_n_O_stt := fun n => eq_sym (Nat.sub_0_r n). Opaque minus_n_O_stt. +Add Search Blacklist "Coq.Arith.Arith_base.minus_n_O_stt". #[global] Hint Resolve minus_n_O_stt: arith. (* Minus.minus_n_O *) #[local] Definition minus_Sn_m_stt := fun n m Hle => eq_sym (Nat.sub_succ_l m n Hle). Opaque minus_Sn_m_stt. +Add Search Blacklist "Coq.Arith.Arith_base.minus_Sn_m_stt". #[global] Hint Resolve minus_Sn_m_stt: arith. (* Minus.minus_Sn_m *) #[local] Definition minus_diag_reverse_stt := fun n => eq_sym (Nat.sub_diag n). Opaque minus_diag_reverse_stt. +Add Search Blacklist "Coq.Arith.Arith_base.minus_diag_reverse_stt". #[global] Hint Resolve minus_diag_reverse_stt: arith. (* Minus.minus_diag_reverse *) #[local] @@ -253,26 +289,31 @@ Definition minus_plus_simpl_l_reverse_stt n m p : n - m = p + n - (p + m). Proof. now rewrite Nat.sub_add_distr, Nat.add_comm, Nat.add_sub. Qed. +Add Search Blacklist "Coq.Arith.Arith_base.minus_plus_simpl_l_reverse_stt". #[global] Hint Resolve minus_plus_simpl_l_reverse_stt: arith. (* Minus.minus_plus_simpl_l_reverse *) #[local] Definition plus_minus_stt := fun n m p Heq => eq_sym (Nat.add_sub_eq_l n m p (eq_sym Heq)). Opaque plus_minus_stt. +Add Search Blacklist "Coq.Arith.Arith_base.plus_minus_stt". #[global] Hint Immediate plus_minus_stt: arith. (* Minus.plus_minus *) #[local] Definition minus_plus_stt := (fun n m => eq_ind _ (fun x => x - n = m) (Nat.add_sub m n) _ (Nat.add_comm _ _)). Opaque minus_plus_stt. +Add Search Blacklist "Coq.Arith.Arith_base.minus_plus_stt". #[global] Hint Resolve minus_plus_stt: arith. (* Minus.minus_plus *) #[local] Definition le_plus_minus_stt := fun n m Hle => eq_sym (eq_trans (Nat.add_comm _ _) (Nat.sub_add n m Hle)). Opaque le_plus_minus_stt. +Add Search Blacklist "Coq.Arith.Arith_base.le_plus_minus_stt". #[global] Hint Resolve le_plus_minus_stt: arith. (* Minus.le_plus_minus *) #[local] Definition le_plus_minus_r_stt := fun n m Hle => eq_trans (Nat.add_comm _ _) (Nat.sub_add n m Hle). Opaque le_plus_minus_r_stt. +Add Search Blacklist "Coq.Arith.Arith_base.le_plus_minus_r_stt". #[global] Hint Resolve le_plus_minus_r_stt: arith. (* Minus.le_plus_minus_r *) #[global] @@ -281,6 +322,7 @@ Hint Resolve Nat.sub_lt: arith. (* Minus.lt_minus *) Definition lt_O_minus_lt_stt : forall n m, 0 < n - m -> m < n := fun n m => proj2 (Nat.lt_add_lt_sub_r 0 n m). Opaque lt_O_minus_lt_stt. +Add Search Blacklist "Coq.Arith.Arith_base.lt_O_minus_lt_stt". #[global] Hint Immediate lt_O_minus_lt_stt: arith. (* Minus.lt_O_minus_lt *) @@ -298,6 +340,7 @@ Hint Resolve Nat.mul_sub_distr_l: arith. (* Mult.mult_minus_distr_l *) #[local] Definition mult_assoc_reverse_stt := fun n m p => eq_sym (Nat.mul_assoc n m p). Opaque mult_assoc_reverse_stt. +Add Search Blacklist "Coq.Arith.Arith_base.mult_assoc_reverse_stt". #[global] Hint Resolve mult_assoc_reverse_stt Nat.mul_assoc: arith. (* Mult.mult_assoc_reverse Mult.mult_assoc *) #[local] @@ -305,6 +348,7 @@ Definition mult_O_le_stt n m : m = 0 \/ n <= m * n. Proof. destruct m; [left|right]; simpl; trivial using Nat.le_add_r. Qed. +Add Search Blacklist "Coq.Arith.Arith_base.mult_O_le_stt". #[global] Hint Resolve mult_O_le_stt: arith. (* Mult.mult_O_le *) #[global] @@ -312,6 +356,7 @@ Hint Resolve Nat.mul_le_mono_l: arith. (* Mult.mult_le_compat_l *) #[local] Definition mult_S_lt_compat_l_stt := (fun n m p Hlt => proj1 (Nat.mul_lt_mono_pos_l (S n) m p (Nat.lt_0_succ n)) Hlt). Opaque mult_S_lt_compat_l_stt. +Add Search Blacklist "Coq.Arith.Arith_base.mult_S_lt_compat_l_stt". #[global] Hint Resolve mult_S_lt_compat_l_stt: arith. (* Mult.mult_S_lt_compat_l *) From 60c5a2bb45e12f7380799ce988d5bec5502ae4f7 Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Sun, 15 Oct 2023 10:06:29 +0200 Subject: [PATCH 4/6] Remove some entries in doc/stdlib/hidden-files --- doc/stdlib/hidden-files | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 75dfa2b24f0e..3dd4c140e810 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -1,14 +1,3 @@ -theories/Arith/Arith_prebase.v -theories/Arith/Le.v -theories/Arith/Lt.v -theories/Arith/Plus.v -theories/Arith/Minus.v -theories/Arith/Mult.v -theories/Arith/Gt.v -theories/Arith/Min.v -theories/Arith/Max.v -theories/Arith/Div2.v -theories/Arith/Even.v theories/btauto/Algebra.v theories/btauto/Btauto.v theories/btauto/Reflect.v @@ -71,7 +60,6 @@ theories/micromega/ZifyPow.v theories/micromega/Zify.v theories/nsatz/NsatzTactic.v theories/nsatz/Nsatz.v -theories/Numbers/Natural/Peano/NPeano.v theories/omega/OmegaLemmas.v theories/omega/PreOmega.v theories/quote/Quote.v From 6e5aefb118be141f3f4f3251867dd5e42c3fbf64 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 23 Nov 2023 18:43:36 +0100 Subject: [PATCH 5/6] Declare last failing jobs of #18164 allow_failure So that they can be updated by their devs at their own pace in the coming weeks. --- .gitlab-ci.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b4e32942eb05..79781d43a61b 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -636,6 +636,7 @@ library:ci-coquelicot: library:ci-cross_crypto: extends: .ci-template + allow_failure: true # See https://github.com/coq/coq/pull/18164/ library:ci-engine_bench: extends: .ci-template @@ -657,6 +658,7 @@ library:ci-fiat_crypto: - plugin:ci-bignums - plugin:ci-rewriter timeout: 3h + allow_failure: true # See https://github.com/coq/coq/pull/18164/ library:ci-fiat_crypto_legacy: extends: .ci-template-flambda @@ -676,6 +678,7 @@ library:ci-fiat_crypto_ocaml: - library:ci-fiat_crypto artifacts: paths: [] # These artifacts would go over the size limit + allow_failure: true # See https://github.com/coq/coq/pull/18164/ library:ci-flocq: extends: .ci-template-flambda @@ -887,6 +890,7 @@ plugin:ci-equations_test: plugin:ci-fiat_parsers: extends: .ci-template + allow_failure: true # See https://github.com/coq/coq/pull/18164/ plugin:ci-lean_importer: extends: .ci-template From 0521c8f03ec6be46f25c7d8249838019369d85b4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 23 Nov 2023 18:47:47 +0100 Subject: [PATCH 6/6] Add changelog --- doc/changelog/11-standard-library/18164-rm_arith_files.rst | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 doc/changelog/11-standard-library/18164-rm_arith_files.rst diff --git a/doc/changelog/11-standard-library/18164-rm_arith_files.rst b/doc/changelog/11-standard-library/18164-rm_arith_files.rst new file mode 100644 index 000000000000..0066e004a82c --- /dev/null +++ b/doc/changelog/11-standard-library/18164-rm_arith_files.rst @@ -0,0 +1,6 @@ +- **Removed:** + long deprecated files in `Arith`: `Div2.v`, `Even.v`, `Gt.v`, + `Le.v`, `Lt.v`, `Max.v`, `Minus.v`, `Min.v`, `Mult.v`, `Plus.v`, + `Arith_prebase.v` + (`#18164 `_, + by Pierre Rousselin).