From 4a470866f59617cebadd51384ee62a50917e73ca Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Mon, 18 Sep 2023 17:13:50 +0200 Subject: [PATCH] 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 * 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 `bugs/bug_4725` still does not pass. --- 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/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/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/Cyclic/Int31/Cyclic31.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 - 61 files changed, 27 insertions(+), 1603 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/test-suite/bugs/bug_13307.v b/test-suite/bugs/bug_13307.v index 11252ebd8c494..2e8181fe6061a 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 95bb66b962e60..2e1d73cb4fe14 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 d729d1a287f7b..ca96a03ddb63e 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 27e836dfdcec8..f5e042ef379a1 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 8d6863da3e90f..b7b89e9e577fe 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 c3615e8eccd0e..9d06b256dc588 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 809f1c44d0a24..c79c2c313dd1c 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 de5987c4f773f..79ade7f59dbad 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 a882ee81be03b..8ef7d8bf34c11 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 5c587a2dfeb45..8a57fa70e4553 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 c2630343c7211..b5b62412f7a65 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/Between.v b/theories/Arith/Between.v index ae38a4a2507d9..6fb5efb54a0ec 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 1cb1274b3550d..7ac3b81cf056d 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 625f0cfe63d8e..c35be9900ebd6 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 14a1e228fbed3..0000000000000 --- 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 1f9ae75c15331..1689bbb40c6c2 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 8e4d27b7b42ec..1c6c1de82f435 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 27599e584b714..0000000000000 --- 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 fce7f5281a4a6..92ea6f8fb8784 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 6e29c2c5a1a96..0000000000000 --- 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 80fd9e82c0cd8..0000000000000 --- 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 f96c9fb1901b8..0000000000000 --- 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 20220340caf66..0000000000000 --- 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 7a7d3cf2d5ee9..0000000000000 --- 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/Peano_dec.v b/theories/Arith/Peano_dec.v index 6e7a7e9c8821c..3bee041e8fda7 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 58de55204ad0c..0000000000000 --- 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 a5b57cd747c13..a13bca830d806 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 742e6a24ad929..d8a8276cb773a 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 aa12d3b13a39f..5c95f49641da6 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 deeabff188359..3a92395ac2360 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/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index 33ab6096552bc..a7d5b2a87dcf3 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -2722,6 +2722,3 @@ Module Int31Cyclic <: CyclicType. #[deprecated(note="Consider Numbers.Cyclic.Int63.Cyclic63 instead", since="8.10")] Definition specs := int31_specs. End Int31Cyclic. - -(* 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 71a0effdff0b3..c09c702044acd 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 d18b5d224a826..0000000000000 --- 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 *) -(*