Adapt wrt coq/coq#18164 (#1738)

These changes should be mostly backwards compatible (at least down to
8.16).

src/Algebra/Hierarchy.v

@@ -5,7 +5,6 @@ Require Export Crypto.Util.Decidable.
 Require Coq.PArith.BinPos.
 Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 
-Require Coq.Numbers.Natural.Peano.NPeano.
 Require Coq.Lists.List.
 
 Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope.

src/Arithmetic/ModularArithmeticTheorems.v

@@ -176,7 +176,7 @@ Module F.
     Qed.
   End FandZ.
   Section FandNat.
-    Import NPeano Nat.
+    Import Nat.
     Local Infix "mod" := modulo : nat_scope.
     Local Open Scope nat_scope.
 

src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v

@@ -89,7 +89,7 @@ Section WordByWordMontgomery.
        numlimbs_drop_high
        using (repeat autounfold with word_by_word_montgomery; t_small)
     : push_numlimbs.
-  Hint Rewrite <- Max.succ_max_distr pred_Sn Min.succ_min_distr : push_numlimbs.
+  Hint Rewrite <- Nat.succ_max_distr pred_Sn Nat.succ_min_distr : push_numlimbs.
 
 
   (* Recurse for a as many iterations as A has limbs, varying A := A, S := 0, r, bounds *)
@@ -167,7 +167,7 @@ Section WordByWordMontgomery.
       repeat autounfold with word_by_word_montgomery; rewrite Z.mul_split_mod.
       repeat autorewrite with push_numlimbs.
       change Init.Nat.max with Nat.max.
-      rewrite <- ?(Max.max_assoc (numlimbs S)).
+      rewrite <- ?(Nat.max_assoc (numlimbs S)).
       reflexivity.
     Qed.
 
@@ -326,11 +326,11 @@ Section WordByWordMontgomery.
   Local Ltac t_min_max_step _ :=
     match goal with
     | [ |- context[Init.Nat.max ?x ?y] ]
-      => first [ rewrite (Max.max_l x y) by lia
-               | rewrite (Max.max_r x y) by lia ]
+      => first [ rewrite (Nat.max_l x y) by lia
+               | rewrite (Nat.max_r x y) by lia ]
     | [ |- context[Init.Nat.min ?x ?y] ]
-      => first [ rewrite (Min.min_l x y) by lia
-               | rewrite (Min.min_r x y) by lia ]
+      => first [ rewrite (Nat.min_l x y) by lia
+               | rewrite (Nat.min_r x y) by lia ]
     | _ => progress change Init.Nat.max with Nat.max
     | _ => progress change Init.Nat.min with Nat.min
     end.
@@ -364,7 +364,7 @@ Section WordByWordMontgomery.
                      | rewrite Nat.min_comm, Nat.min_max_distr ]. }
     rewrite Hgen; clear Hgen.
     destruct count; [ reflexivity | ].
-    repeat apply Max.max_case_strong; apply Min.min_case_strong; lia.
+    repeat apply Nat.max_case_strong; apply Nat.min_case_strong; lia.
   Qed.
 
 

src/Compilers/Named/NameUtilProperties.v

@@ -71,7 +71,7 @@ Section language.
       unfold mname_list_unique; intro H; split; intros k N;
         rewrite <- ?firstn_map, <- ?skipn_map, ?skipn_skipn, ?firstn_firstn_min, ?firstn_skipn_add;
         intros; eapply H; try eassumption.
-      { apply Min.min_case_strong.
+      { apply Nat.min_case_strong.
         { match goal with H : _ |- _ => rewrite skipn_firstn in H end;
             eauto using In_firstn. }
         { intro; match goal with H : _ |- _ => rewrite skipn_all in H by (rewrite firstn_length; lia * ) end.

src/Compilers/WfReflectiveGen.v

@@ -240,14 +240,14 @@ Section language.
     : fst (natize_interp_flat_type base v1) = length (flatten_binding_list v1 v2) + base.
   Proof using Type.
     revert base; induction t; simpl; [ reflexivity | reflexivity | ].
-    intros; rewrite List.app_length, <- plus_assoc.
+    intros; rewrite List.app_length, <- Nat.add_assoc.
     rewrite_hyp <- ?*; reflexivity.
   Qed.
   Lemma length_natize_interp_flat_type2 {t} (base : nat) (v1 : interp_flat_type var1 t) (v2 : interp_flat_type var2 t)
     : fst (natize_interp_flat_type base v2) = length (flatten_binding_list v1 v2) + base.
   Proof using Type.
     revert base; induction t; simpl; [ reflexivity | reflexivity | ].
-    intros; rewrite List.app_length, <- plus_assoc.
+    intros; rewrite List.app_length, <- Nat.add_assoc.
     rewrite_hyp <- ?*; reflexivity.
   Qed.
 
@@ -285,7 +285,7 @@ Section language.
        | TT, TT => rTrue
        | TT, _ => rFalse
        | Var t0 x, Var t1 y
-         => match beq_nat (fst x) (fst y), List.nth_error G (List.length G - S (fst x)) with
+         => match Nat.eqb (fst x) (fst y), List.nth_error G (List.length G - S (fst x)) with
            | true, Some v => eq_type_and_var v (existT _ (t0, t1) (snd x, snd y))
            | _, _ => rFalse
            end

src/Compilers/Z/Bounds/RoundUpLemmas.v

@@ -1,4 +1,5 @@
 Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
+Require Import Coq.Arith.PeanoNat.
 Require Import Crypto.Compilers.Z.Bounds.Interpretation.
 Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.Tactics.BreakMatch.
@@ -27,8 +28,8 @@ Proof.
            | _ => progress simpl in *
            | _ => progress break_innermost_match_step
            | _ => progress break_innermost_match_hyps_step
-           | [ H : ?leb _ _ = true |- _ ] => apply NPeano.Nat.leb_le in H
-           | [ H : ?leb _ _ = false |- _ ] => apply NPeano.Nat.leb_gt in H
+           | [ H : ?leb _ _ = true |- _ ] => apply Nat.leb_le in H
+           | [ H : ?leb _ _ = false |- _ ] => apply Nat.leb_gt in H
            | _ => lia *
            end. }
 Qed.

src/Experiments/SimplyTypedArithmetic.v

@@ -7385,7 +7385,7 @@ Section rcarry_mul.
       rewrite negb_false_iff in *.
       Z.ltb_to_lt.
       rewrite Qle_bool_iff in *.
-      rewrite NPeano.Nat.eqb_neq in *.
+      rewrite Nat.eqb_neq in *.
       intros.
       cbv [Qnum Qden limbwidth Qceiling Qfloor Qopp Qdiv Qplus inject_Z Qmult Qinv] in *.
       rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *.

src/LegacyArithmetic/BaseSystem.v

@@ -1,6 +1,6 @@
 Require Import Coq.Lists.List.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv.
-Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
+Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Arith.Arith.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.Notations.
 Require Export Crypto.Util.FixCoqMistakes.

src/LegacyArithmetic/BaseSystemProofs.v

@@ -1,7 +1,7 @@
 Require Import Coq.Lists.List Coq.micromega.Psatz Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Crypto.Util.ListUtil.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv.
-Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
+Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Arith.Arith.
 Require Import Crypto.LegacyArithmetic.BaseSystem.
 Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.Notations.
@@ -101,7 +101,7 @@ Section BaseSystemProofs.
   Qed.
   Hint Rewrite peel_decode.
 
-  Hint Rewrite plus_0_r.
+  Hint Rewrite Nat.add_0_r.
 
   Lemma set_higher : forall bs vs x,
     decode' bs (vs++x::nil) = decode' bs vs + nth_default 0 bs (length vs) * x.
@@ -128,7 +128,7 @@ Section BaseSystemProofs.
       assert (HH: nth_error (z0 :: l) 0 = Some z) by
           (
             pose proof @nth_error_skipn _ (length vs) bs 0;
-            rewrite plus_0_r in *;
+            rewrite Nat.add_0_r in *;
             congruence); simpl in HH; congruence. }
   Qed.
 End BaseSystemProofs.

src/LegacyArithmetic/Pow2BaseProofs.v

@@ -1,6 +1,5 @@
 Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.micromega.Psatz Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.Lists.List.
 Require Import Coq.funind.Recdef.
 Require Import Crypto.Util.ListUtil Crypto.Util.NatUtil.
@@ -116,7 +115,7 @@ Section Pow2BaseProofs.
       erewrite base_from_limb_widths_step; eauto.
       f_equal.
       simpl.
-      destruct (NPeano.Nat.eq_dec i 0).
+      destruct (Nat.eq_dec i 0).
       - subst; unfold sum_firstn; simpl.
         apply nth_error_exists_first in nth_err_w.
         destruct nth_err_w as [l' lw_destruct]; subst.
@@ -162,7 +161,7 @@ Section Pow2BaseProofs.
     autorewrite with simpl_firstn simpl_skipn in *.
     rewrite H, skipn_app, skipn_all by auto with arith distr_length; clear H.
     simpl; distr_length.
-    apply Min.min_case_strong; intro;
+    apply Nat.min_case_strong; intro;
       unfold sum_firstn; autorewrite with natsimplify simpl_skipn simpl_firstn;
         reflexivity.
   Qed.

src/Primitives/EdDSARepChange.v

@@ -12,7 +12,6 @@ Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Pro
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Option Crypto.Util.Logic Crypto.Util.Relations Crypto.Util.WordUtil Util.LetIn Util.NatUtil.
 Require Import Crypto.Spec.ModularArithmetic Crypto.Arithmetic.PrimeFieldTheorems.
-Import NPeano.
 
 Import Notations.
 

src/Spec/EdDSA.v

@@ -2,7 +2,6 @@ Require bbv.WordScope Crypto.Util.WordUtil.
 Require Import Coq.ZArith.BinIntDef.
 Require Crypto.Algebra.Hierarchy Algebra.ScalarMult.
 Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
-Require Coq.Numbers.Natural.Peano.NPeano.
 
 Require Import Crypto.Spec.ModularArithmetic.
 

src/Util/Decidable/Decidable2Bool.v

@@ -37,7 +37,7 @@ Lemma dec_nat_eq_to_bool a b
   : (if dec (a = b) then true else false) = Nat.eqb a b.
 Proof.
   destruct (Nat.eqb a b) eqn:H; break_match; try reflexivity.
-  { apply beq_nat_true in H; congruence. }
+  { apply Nat.eqb_eq in H; congruence. }
   { rewrite Nat.eqb_refl in H; congruence. }
 Qed.
 #[global]

src/Util/FixedWordSizesEquality.v

@@ -31,7 +31,7 @@ Proof.
   destruct (NatUtil.nat_eq_dec x y) as [pf|pf]; [ intros; assumption | ].
   intro H; exfalso.
   let pf := pf in
-  abstract (apply pf; eapply NPeano.Nat.pow_inj_r; [ | eassumption ]; lia).
+  abstract (apply pf; eapply Nat.pow_inj_r; [ | eassumption ]; lia).
 Defined.
 Lemma pow2_inj_helper_refl x p : pow2_inj_helper x x p = eq_refl.
 Proof.

src/Util/ListUtil.v

@@ -4,7 +4,6 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Coq.Arith.Peano_dec.
 Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Pointed.
 Require Import Crypto.Util.Prod.
@@ -172,10 +171,10 @@ Module Export List.
   Proof.
    revert start. induction len as [|len IHlen]; simpl; intros.
    - rewrite <- plus_n_O. split;[easy|].
-     intros (H,H'). apply (Lt.lt_irrefl _ (Lt.le_lt_trans _ _ _ H H')).
+     intros (H,H'). apply (Nat.lt_irrefl _ (Nat.le_lt_trans _ _ _ H H')).
    - rewrite IHlen, <- plus_n_Sm; simpl; split.
      * intros [H|H]; subst; intuition auto with arith.
-     * intros (H,H'). destruct (Lt.le_lt_or_eq _ _ H); intuition.
+     * intros (H,H'). destruct (proj1 (Nat.lt_eq_cases _ _) H); intuition.
   Qed.
 
   Section Facts.
@@ -226,7 +225,7 @@ Module Export List.
     Lemma firstn_length_le: forall l:list A, forall n:nat,
           n <= length l -> length (firstn n l) = n.
     Proof using Type. induction l as [|x xs Hrec].
-           - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now simpl.
+           - simpl. intros n H. apply Nat.le_0_r in H. rewrite H. now simpl.
            - destruct n as [|n].
              * now simpl.
              * simpl. intro H. apply le_S_n in H. now rewrite (Hrec n H).
@@ -238,7 +237,7 @@ Module Export List.
     Proof using Type. induction n as [|k iHk]; intros l1 l2.
            - now simpl.
            - destruct l1 as [|x xs].
-             * unfold List.firstn at 2, length. now rewrite 2!app_nil_l, <- minus_n_O.
+             * unfold List.firstn at 2, length. now rewrite 2!app_nil_l, Nat.sub_0_r.
              * rewrite <- app_comm_cons. simpl. f_equal. apply iHk.
     Qed.
 
@@ -247,7 +246,7 @@ Module Export List.
         firstn ((length l1) + n) (l1 ++ l2) = l1 ++ firstn n l2.
     Proof using Type. induction n as [| k iHk];intros l1 l2.
            - unfold List.firstn at 2. rewrite <- plus_n_O, app_nil_r.
-             rewrite firstn_app. rewrite <- minus_diag_reverse.
+             rewrite firstn_app. rewrite Nat.sub_diag.
              unfold List.firstn at 2. rewrite app_nil_r. apply firstn_all.
            - destruct l2 as [|x xs].
              * simpl. rewrite app_nil_r. apply firstn_all2. auto with arith.
@@ -1360,7 +1359,7 @@ Lemma firstn_firstn : forall {A} m n (l : list A), (n <= m)%nat ->
   firstn n (firstn m l) = firstn n l.
 Proof.
   intros A m n l H; rewrite firstn_firstn_min.
-  apply Min.min_case_strong; intro; [ reflexivity | ].
+  apply Nat.min_case_strong; intro; [ reflexivity | ].
   assert (n = m) by lia; subst; reflexivity.
 Qed.
 
@@ -1874,7 +1873,7 @@ Proof.
   intros A d l i; induction n as [|n IHn]; break_match; autorewrite with push_nth_default; auto; try lia.
   + rewrite (firstn_succ d) by lia.
     autorewrite with push_nth_default; repeat (break_match_hyps; break_match; distr_length);
-      rewrite Min.min_l in * by lia; try lia.
+      rewrite Nat.min_l in * by lia; try lia.
     - apply IHn; lia.
     - replace i with n in * by lia.
       rewrite Nat.sub_diag.

src/Util/NUtil.v

@@ -1,6 +1,5 @@
 Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Coq.NArith.NArith.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.Util.NatUtil Crypto.Util.Decidable.
 Require Export Crypto.Util.NUtil.WithoutReferenceToZ.
 Require bbv.WordScope.

src/Util/NUtil/WithoutReferenceToZ.v

@@ -1,8 +1,7 @@
 (** NUtil that doesn't depend on ZUtil stuff *)
 (** Should probably come up with a better organization of this stuff *)
 Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Classes.RelationClasses.
-Require Import Coq.NArith.NArith.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
+Require Import Coq.NArith.NArith Coq.Arith.PeanoNat.
 Require Import Crypto.Util.NatUtil Crypto.Util.Decidable.
 
 Module N.