Adapt to rocq-prover/rocq#18164

We remove some Arith files and NPeano from the stdlib after deprecation.

Author: Villetaneuse

examples/ConsiderDemo.v

@@ -1,6 +1,5 @@
 Require Import Coq.Bool.Bool.
-Require NPeano.
-Import NPeano.Nat.
+Require Import Arith.PeanoNat.
 Require Import ExtLib.Tactics.Consider.
 Require Import ExtLib.Data.Nat.
 
@@ -12,19 +11,19 @@ Set Strict Implicit.
 
 (**  Some tests *)
 Section test.
-  Goal forall x y z,  (ltb x y && ltb y z) = true ->
-                 ltb x z = true.
+  Goal forall x y z,  (Nat.ltb x y && Nat.ltb y z) = true ->
+                 Nat.ltb x z = true.
   intros x y z.
-  consider (ltb x y && ltb y z).
-  consider (ltb x z); auto. intros. exfalso. lia.
+  consider (Nat.ltb x y && Nat.ltb y z).
+  consider (Nat.ltb x z); auto. intros. exfalso. lia.
   Qed.
 
   Goal forall x y z,
-    ltb x y = true ->
-    ltb y z = true ->
-    ltb x z = true.
+    Nat.ltb x y = true ->
+    Nat.ltb y z = true ->
+    Nat.ltb x z = true.
   Proof.
-    intros. consider (ltb x y); consider (ltb y z); consider (ltb x z); intros; auto.
+    intros. consider (Nat.ltb x y); consider (Nat.ltb y z); consider (Nat.ltb x z); intros; auto.
     exfalso; lia.
   Qed.
 

theories/Data/HList.v

@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List.
+Require Import Coq.Lists.List Coq.Arith.PeanoNat.
 Require Import Relations RelationClasses.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Data.SigT.
@@ -658,7 +658,7 @@ Section hlist.
       { clear H IHtvs.
         eexists; split; eauto. eexists; split; eauto.
         simpl. intros. rewrite (hlist_eta vs). reflexivity. }
-      { apply Lt.lt_S_n in H.
+      { apply Nat.succ_lt_mono in H.
         { specialize (IHtvs _ H).
           forward_reason.
           rewrite H0. rewrite H1.

theories/Data/ListNth.v

@@ -1,5 +1,5 @@
 Require Import Coq.Lists.List.
-Require Import Coq.Arith.Lt Coq.Arith.Plus.
+Require Import Coq.Arith.PeanoNat.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -14,7 +14,7 @@ Section parametric.
     induction A; destruct n; simpl; intros; auto.
     { inversion H. }
     { inversion H. }
-    { eapply IHA. apply Lt.lt_S_n; assumption. }
+    { eapply IHA. apply Nat.succ_lt_mono; assumption. }
   Qed.
 
   Lemma nth_error_app_R : forall (A B : list T) n,
@@ -23,7 +23,7 @@ Section parametric.
   Proof.
     induction A; destruct n; simpl; intros; auto.
     + inversion H.
-    + apply IHA. apply Le.le_S_n; assumption.
+    + apply IHA. apply Nat.succ_le_mono; assumption.
   Qed.
 
   Lemma nth_error_weaken : forall ls' (ls : list T) n v,
@@ -45,25 +45,25 @@ Section parametric.
   Proof.
     clear. induction ls; destruct n; simpl; intros; auto.
     + inversion H.
-    + apply IHls. apply Le.le_S_n; assumption.
+    + apply IHls. apply Nat.succ_le_mono; assumption.
   Qed.
 
   Lemma nth_error_length : forall (ls ls' : list T) n,
     nth_error (ls ++ ls') (n + length ls) = nth_error ls' n.
   Proof.
     induction ls; simpl; intros.
-    rewrite Plus.plus_0_r. auto.
-    rewrite <- Plus.plus_Snm_nSm.
+    rewrite Nat.add_0_r. auto.
+    rewrite <-Nat.add_succ_comm.
     simpl. eapply IHls.
   Qed.
 
   Theorem nth_error_length_ge : forall T (ls : list T) n,
     nth_error ls n = None -> length ls <= n.
   Proof.
     induction ls; destruct n; simpl in *; auto; simpl in *.
-    + intro. apply Le.le_0_n.
+    + intro. apply Nat.le_0_l.
     + inversion 1.
-    + intros. eapply Le.le_n_S. auto.
+    + intros. apply ->Nat.succ_le_mono. auto.
   Qed.
 
   Lemma nth_error_length_lt : forall {T} (ls : list T) n val,
@@ -72,8 +72,8 @@ Section parametric.
     induction ls; destruct n; simpl; intros; auto.
     + inversion H.
     + inversion H.
-    + apply Lt.lt_0_Sn.
-    + apply Lt.lt_n_S. eauto.
+    + apply Nat.lt_0_succ.
+    + apply ->Nat.succ_lt_mono. apply IHls with (1 := H).
   Qed.
 
 

theories/Data/Nat.v

@@ -9,47 +9,45 @@ Set Strict Implicit.
 
 
 Global Instance RelDec_eq : RelDec (@eq nat) :=
-{ rel_dec := EqNat.beq_nat }.
-
-Require Coq.Numbers.Natural.Peano.NPeano.
+{ rel_dec := Nat.eqb }.
 
 Global Instance RelDec_lt : RelDec lt :=
-{ rel_dec := NPeano.Nat.ltb }.
+{ rel_dec := Nat.ltb }.
 
 Global Instance RelDec_le : RelDec le :=
-{ rel_dec := NPeano.Nat.leb }.
+{ rel_dec := Nat.leb }.
 
 Global Instance RelDec_gt : RelDec gt :=
-{ rel_dec := fun x y => NPeano.Nat.ltb y x }.
+{ rel_dec := fun x y => Nat.ltb y x }.
 
 Global Instance RelDec_ge : RelDec ge :=
-{ rel_dec := fun x y => NPeano.Nat.leb y x }.
+{ rel_dec := fun x y => Nat.leb y x }.
 
 Global Instance RelDecCorrect_eq : RelDec_Correct RelDec_eq.
 Proof.
-  constructor; simpl. apply EqNat.beq_nat_true_iff.
+  constructor; simpl. apply PeanoNat.Nat.eqb_eq.
 Qed.
 
 Global Instance RelDecCorrect_lt : RelDec_Correct RelDec_lt.
 Proof.
-  constructor; simpl. eapply NPeano.Nat.ltb_lt.
+  constructor; simpl. eapply PeanoNat.Nat.ltb_lt.
 Qed.
 
 Global Instance RelDecCorrect_le : RelDec_Correct RelDec_le.
 Proof.
-  constructor; simpl. eapply NPeano.Nat.leb_le.
+  constructor; simpl. eapply PeanoNat.Nat.leb_le.
 Qed.
 
 Global Instance RelDecCorrect_gt : RelDec_Correct RelDec_gt.
 Proof.
   constructor; simpl. unfold rel_dec; simpl.
-  intros. eapply NPeano.Nat.ltb_lt.
+  intros. eapply PeanoNat.Nat.ltb_lt.
 Qed.
 
 Global Instance RelDecCorrect_ge : RelDec_Correct RelDec_ge.
 Proof.
   constructor; simpl. unfold rel_dec; simpl.
-  intros. eapply NPeano.Nat.leb_le.
+  intros. eapply PeanoNat.Nat.leb_le.
 Qed.
 
 Inductive R_nat_S : nat -> nat -> Prop :=

theories/Data/String.v

@@ -1,7 +1,6 @@
 Require Import Coq.Strings.String.
 Require Import Coq.Program.Program. 
-Require Import Coq.Numbers.Natural.Peano.NPeano.
-Require Import Coq.Arith.Arith.
+Require Import Coq.Arith.PeanoNat.
 
 Require Import ExtLib.Tactics.Consider.
 Require Import ExtLib.Core.RelDec.
@@ -99,19 +98,19 @@ Section Program_Scope.
     destruct n; destruct m; intros.
     inversion H. exfalso. apply H0. etransitivity. 2: eassumption. repeat constructor.
     inversion H.
-    eapply neq_0_lt. congruence.
+    now apply Nat.lt_0_succ.
   Qed.
 
   Program Fixpoint nat2string (n:nat) {measure n}: string :=
-    match NPeano.Nat.ltb n modulus as x return NPeano.Nat.ltb n modulus = x -> string with
+    match Nat.ltb n modulus as x return Nat.ltb n modulus = x -> string with
       | true => fun _ => String (digit2ascii n) EmptyString
       | false => fun pf =>
-        let m := NPeano.Nat.div n modulus in
+        let m := Nat.div n modulus in
         append (nat2string m) (String (digit2ascii (n - modulus * m)) EmptyString)
-    end (@Logic.eq_refl _ (NPeano.Nat.ltb n modulus)).
+    end (@Logic.eq_refl _ (Nat.ltb n modulus)).
   Next Obligation.
-    eapply NPeano.Nat.div_lt; auto.
-    consider (NPeano.Nat.ltb n modulus); try congruence. intros.
+    eapply Nat.div_lt; auto.
+    consider (Nat.ltb n modulus); try congruence. intros.
     eapply _xxx; eassumption.
   Defined.
 

theories/Programming/Show.v

@@ -172,12 +172,12 @@ Section hiding_notation.
     if Compare_dec.le_gt_dec n 9 then
       inject (Char.digit2ascii n)
     else
-      let n' := NPeano.Nat.div n 10 in
+      let n' := Nat.div n 10 in
       (@nat_show n' _) << (inject (Char.digit2ascii (n - 10 * n'))).
   Next Obligation.
-    assert (NPeano.Nat.div n 10 < n) ; eauto.
-    eapply NPeano.Nat.div_lt.
-    match goal with [ H : n > _ |- _ ] => inversion H end; apply Lt.lt_O_Sn.
+    assert (Nat.div n 10 < n) ; eauto.
+    eapply Nat.div_lt.
+    match goal with [ H : n > _ |- _ ] => inversion H end; apply Nat.lt_0_succ.
     repeat constructor.
   Defined.
   Global Instance nat_Show : Show nat := { show := nat_show }.