Merge pull request #121 from Villetaneuse/rm_arith_files

Remove deprecated files in Coq.Arith
coq-community · Oct 16, 2023 · fbb6ebe · fbb6ebe
2 parents aaaf68f + 4e3e7a6
commit fbb6ebe
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 22 deletions.
diff --git a/implementations/peano_naturals.v b/implementations/peano_naturals.v
@@ -1,7 +1,7 @@
 Require
   MathClasses.theory.ua_homomorphisms.
 Require Import
-  Coq.Classes.Morphisms Coq.setoid_ring.Ring Coq.Arith.Arith_base
+  Coq.Classes.Morphisms Coq.setoid_ring.Ring Coq.Arith.Arith_base Coq.Arith.PeanoNat
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.theory.categories
   MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.semirings.
 
@@ -20,14 +20,14 @@ Instance nat_mult: Mult nat := Peano.mult.
 Instance: SemiRing nat.
 Proof.
   repeat (split; try apply _); repeat intro.
-         now apply plus_assoc.
-        now apply plus_0_r.
-       now apply plus_comm.
-      now apply mult_assoc.
-     now apply mult_1_l.
-    now apply mult_1_r.
-   now apply mult_comm.
-  now apply mult_plus_distr_l.
+         now apply Nat.add_assoc.
+        now apply Nat.add_0_r.
+       now apply Nat.add_comm.
+      now apply Nat.mul_assoc.
+     now apply Nat.mul_1_l.
+    now apply Nat.mul_1_r.
+   now apply Nat.mul_comm.
+  now apply Nat.mul_add_distr_l.
 Qed.
 
 (* misc *)
@@ -115,7 +115,7 @@ Instance: Naturals nat := {}.
 (* Misc *)
 #[global]
 Instance: NoZeroDivisors nat.
-Proof. intros x [Ex [y [Ey1 Ey2]]]. destruct (Mult.mult_is_O x y Ey2); intuition. Qed.
+Proof. now intros x [Ex [y [Ey1 [H | H]%Nat.eq_mul_0]]]. Qed.
 
 #[global]
 Instance: ∀ z : nat, PropHolds (z ≠ 0) → LeftCancellation (.*.) z.
@@ -133,13 +133,14 @@ Proof.
   assert (TotalRelation nat_le).
    intros x y. now destruct (le_ge_dec x y); intuition.
   assert (PartialOrder nat_le).
-   split; try apply _. intros x y E. now apply Le.le_antisym.
+   split; try apply _. intros x y E. now apply Nat.le_antisymm.
   assert (SemiRingOrder nat_le).
    repeat (split; try apply _).
-      intros x y E. exists (y - x)%nat. now apply le_plus_minus.
-     intros. now apply Plus.plus_le_compat_l.
-    intros. now apply plus_le_reg_l with z.
-   intros x y ? ?. change (0 * 0 <= x * y)%nat. now apply Mult.mult_le_compat.
+      intros x y E. exists (y - x)%nat.
+      now rewrite Nat.add_comm, Nat.sub_add by (exact E).
+     intros. now apply Nat.add_le_mono_l.
+    intros. now apply Nat.add_le_mono_l with z.
+   intros x y ? ?. change (0 * 0 <= x * y)%nat. now apply Nat.mul_le_mono.
   apply dec_full_pseudo_srorder.
   now apply Nat.le_neq.
 Qed.
@@ -162,8 +163,8 @@ Instance: CutMinusSpec nat nat_cut_minus.
 Proof.
   split.
    symmetry. rewrite commutativity.
-   now apply le_plus_minus.
+   now rewrite Nat.add_comm, Nat.sub_add by (exact H).
   intros x y E. destruct (orders.le_equiv_lt x y E) as [E2|E2].
-   rewrite E2. now apply minus_diag.
-  apply not_le_minus_0. now apply orders.lt_not_le_flip.
+   rewrite E2. now apply Nat.sub_diag.
+   apply Nat.sub_0_le; exact E.
 Qed.
diff --git a/theory/naturals.v b/theory/naturals.v
@@ -1,5 +1,6 @@
 Require Import
   Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.implementations.peano_naturals MathClasses.theory.rings
+  Coq.Arith.PeanoNat
   MathClasses.categories.varieties MathClasses.theory.ua_transference.
 Require Export
   MathClasses.interfaces.naturals.
@@ -128,7 +129,7 @@ Section borrowed_from_nat.
   Proof.
     intros x y z.
     rapply (from_nat_stmt (x' + y' === x' + z' -=> y' === z') (three_vars x y z)).
-    intro. simpl. apply Plus.plus_reg_l.
+    intro. simpl. apply Nat.add_cancel_l.
   Qed.
 
   Global Instance: ∀ z : N, RightCancellation (+) z.
@@ -156,20 +157,20 @@ Section borrowed_from_nat.
   Lemma zero_sum (x y : N) : x + y = 0 → x = 0 ∧ y = 0.
   Proof.
     rapply (from_nat_stmt (x' + y' === 0 -=> Conj _ (x' === 0) (y' === 0)) (two_vars x y)).
-    intro. simpl. apply Plus.plus_is_O.
+    intro. simpl. apply Nat.eq_add_0.
   Qed.
 
   Lemma one_sum (x y : N) : x + y = 1 → (x = 1 ∧ y = 0) ∨ (x = 0 ∧ y = 1).
   Proof.
    rapply (from_nat_stmt (x' + y' === 1 -=> Disj _ (Conj _ (x' === 1) (y' === 0)) (Conj _ (x' === 0) (y' === 1))) (two_vars x y)).
-   intros. simpl. intros. edestruct Plus.plus_is_one; eauto.
+   intros. simpl. intros. edestruct Nat.eq_add_1; eauto.
   Qed.
 
   Global Instance: ZeroProduct N.
   Proof.
     intros x y.
     rapply (from_nat_stmt (x' * y' === 0 -=>Disj _ (x' === 0) (y' === 0)) (two_vars x y)).
-    intros ? E. destruct (Mult.mult_is_O _ _ E); red; intuition.
+    intros ? E. destruct ((proj1 (Nat.eq_mul_0 _ _)) E); red; intuition.
   Qed.
 End borrowed_from_nat.