Merge PR coq#18164: Remove deprecated files in Arith and Numbers/Natural

Reviewed-by: proux01
Co-authored-by: proux01 <[email protected]>

.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

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 <https://github.com/coq/coq/pull/18164>`_,
+  by Pierre Rousselin).

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.
 

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

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.

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.

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.
 

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)

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.

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.
 

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

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.

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.

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.