Subtraction in NatInt

This is the revival of an old PR in former repository.

We add two axioms in NatInt to restrict the models to exactly the
integers and the natural numbers (with `pred 0 = 0`). This allows
us to prove lemmas such as `sub_succ` and then prove many properties of
`sub` which are shared between the natural numbers and the integers.

The Natural and Integer parts of Numbers are modified in consequence.
The result should be completely compatible except for `mul_sub_distr_l`
which had different variable names in Integers and Natural (we chose to
keep it as it was in Integers).

We also remove references to old NZAxiomsSig modules.

This needs more polishing, so still a draft:
- the case of `mul_sub_distr_l` should be decided
- removing some `Private_` lemmas is possible (e.g. with `Let`), this
  would result in a cleaner PR
- check exactly the before/after for a user importing PeanoNat, etc

Author: Villetaneuse

theories/Numbers/Cyclic/Abstract/NZCyclic.v

@@ -1,5 +1,5 @@
 (************************************************************************)
-(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
 (*  v      *         Copyright INRIA, CNRS and contributors             *)
 (* <O___,, * (see version control and CREDITS file for authors & dates) *)
 (*   \VV/  **************************************************************)
@@ -25,7 +25,7 @@ From Stdlib Require Import Lia.
     a power of 2.
 *)
 
-Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZAxiomsSig.
+Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZBasicFunsSig.
 
 Local Open Scope Z_scope.
 

theories/Numbers/Integer/Abstract/ZAdd.v

@@ -1,5 +1,5 @@
 (************************************************************************)
-(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
 (*  v      *         Copyright INRIA, CNRS and contributors             *)
 (* <O___,, * (see version control and CREDITS file for authors & dates) *)
 (*   \VV/  **************************************************************)
@@ -66,13 +66,6 @@ rewrite <- (succ_pred n) at 2.
 rewrite opp_succ. now rewrite succ_pred.
 Qed.
 
-Theorem sub_diag n : n - n == 0.
-Proof.
-nzinduct n.
-- now nzsimpl.
-- intro n. rewrite sub_succ_r, sub_succ_l; now rewrite pred_succ.
-Qed.
-
 Theorem add_opp_diag_l n : - n + n == 0.
 Proof.
 now rewrite add_comm, add_opp_r, sub_diag.
@@ -134,12 +127,6 @@ Proof.
 symmetry; apply eq_opp_l.
 Qed.
 
-Theorem sub_add_distr n m p : n - (m + p) == (n - m) - p.
-Proof.
-rewrite <- add_opp_r, opp_add_distr, add_assoc.
-now rewrite 2 add_opp_r.
-Qed.
-
 Theorem sub_sub_distr n m p : n - (m - p) == (n - m) + p.
 Proof.
 rewrite <- add_opp_r, opp_sub_distr, add_assoc.
@@ -230,16 +217,6 @@ Qed.
     terms. The name includes the first operator and the position of
     the term being canceled. *)
 
-Theorem add_simpl_l n m : n + m - n == m.
-Proof.
-now rewrite add_sub_swap, sub_diag, add_0_l.
-Qed.
-
-Theorem add_simpl_r n m : n + m - m == n.
-Proof.
-now rewrite <- add_sub_assoc, sub_diag, add_0_r.
-Qed.
-
 Theorem sub_simpl_l n m : - n - m + n == - m.
 Proof.
 now rewrite <- add_sub_swap, add_opp_diag_l, sub_0_l.
@@ -258,27 +235,6 @@ Qed.
 (** Now we have two sums or differences; the name includes the two
     operators and the position of the terms being canceled *)
 
-Theorem add_add_simpl_l_l n m p : (n + m) - (n + p) == m - p.
-Proof.
-now rewrite (add_comm n m), <- add_sub_assoc,
-sub_add_distr, sub_diag, sub_0_l, add_opp_r.
-Qed.
-
-Theorem add_add_simpl_l_r n m p : (n + m) - (p + n) == m - p.
-Proof.
-rewrite (add_comm p n); apply add_add_simpl_l_l.
-Qed.
-
-Theorem add_add_simpl_r_l n m p : (n + m) - (m + p) == n - p.
-Proof.
-rewrite (add_comm n m); apply add_add_simpl_l_l.
-Qed.
-
-Theorem add_add_simpl_r_r n m p : (n + m) - (p + m) == n - p.
-Proof.
-rewrite (add_comm p m); apply add_add_simpl_r_l.
-Qed.
-
 Theorem sub_add_simpl_r_l n m p : (n - m) + (m + p) == n + p.
 Proof.
 now rewrite <- sub_sub_distr, sub_add_distr, sub_diag,
@@ -293,3 +249,4 @@ Qed.
 (** Of course, there are many other variants *)
 
 End ZAddProp.
+

theories/Numbers/Integer/Abstract/ZAddOrder.v

@@ -1,5 +1,5 @@
 (************************************************************************)
-(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
 (*  v      *         Copyright INRIA, CNRS and contributors             *)
 (* <O___,, * (see version control and CREDITS file for authors & dates) *)
 (*   \VV/  **************************************************************)
@@ -40,11 +40,6 @@ Qed.
 
 (** Sub and order *)
 
-Theorem lt_0_sub : forall n m, 0 < m - n <-> n < m.
-Proof.
-intros n m. now rewrite (add_lt_mono_r _ _ n), add_0_l, sub_simpl_r.
-Qed.
-
 Notation sub_pos := lt_0_sub (only parsing).
 
 Theorem le_0_sub : forall n m, 0 <= m - n <-> n <= m.
@@ -151,39 +146,24 @@ apply le_lt_trans with (m - p);
 [now apply sub_le_mono_r | now apply sub_lt_mono_l].
 Qed.
 
-Theorem le_lt_sub_lt : forall n m p q, n <= m -> p - n < q - m -> p < q.
-Proof.
-intros n m p q H1 H2. apply (le_lt_add_lt (- m) (- n));
-[now apply -> opp_le_mono | now rewrite 2 add_opp_r].
-Qed.
-
 Theorem lt_le_sub_lt : forall n m p q, n < m -> p - n <= q - m -> p < q.
 Proof.
 intros n m p q H1 H2. apply (lt_le_add_lt (- m) (- n));
 [now apply -> opp_lt_mono | now rewrite 2 add_opp_r].
 Qed.
 
+(* TODO: fix name *)
 Theorem le_le_sub_lt : forall n m p q, n <= m -> p - n <= q - m -> p <= q.
 Proof.
 intros n m p q H1 H2. apply (le_le_add_le (- m) (- n));
 [now apply -> opp_le_mono | now rewrite 2 add_opp_r].
 Qed.
 
-Theorem lt_add_lt_sub_r : forall n m p, n + p < m <-> n < m - p.
-Proof.
-intros n m p. now rewrite (sub_lt_mono_r _ _ p), add_simpl_r.
-Qed.
-
 Theorem le_add_le_sub_r : forall n m p, n + p <= m <-> n <= m - p.
 Proof.
 intros n m p. now rewrite (sub_le_mono_r _ _ p), add_simpl_r.
 Qed.
 
-Theorem lt_add_lt_sub_l : forall n m p, n + p < m <-> p < m - n.
-Proof.
-intros n m p. rewrite add_comm; apply lt_add_lt_sub_r.
-Qed.
-
 Theorem le_add_le_sub_l : forall n m p, n + p <= m <-> p <= m - n.
 Proof.
 intros n m p. rewrite add_comm; apply le_add_le_sub_r.
@@ -194,21 +174,11 @@ Proof.
 intros n m p. now rewrite (add_lt_mono_r _ _ p), sub_simpl_r.
 Qed.
 
-Theorem le_sub_le_add_r : forall n m p, n - p <= m <-> n <= m + p.
-Proof.
-intros n m p. now rewrite (add_le_mono_r _ _ p), sub_simpl_r.
-Qed.
-
 Theorem lt_sub_lt_add_l : forall n m p, n - m < p <-> n < m + p.
 Proof.
 intros n m p. rewrite add_comm; apply lt_sub_lt_add_r.
 Qed.
 
-Theorem le_sub_le_add_l : forall n m p, n - m <= p <-> n <= m + p.
-Proof.
-intros n m p. rewrite add_comm; apply le_sub_le_add_r.
-Qed.
-
 Theorem lt_sub_lt_add : forall n m p q, n - m < p - q <-> n + q < m + p.
 Proof.
 intros n m p q. now rewrite lt_sub_lt_add_l, add_sub_assoc, <- lt_add_lt_sub_r.
@@ -283,3 +253,5 @@ End PosNeg.
 Ltac zero_pos_neg n := induction_maker n ltac:(apply zero_pos_neg).
 
 End ZAddOrderProp.
+
+

theories/Numbers/Integer/Abstract/ZAxioms.v

@@ -1,5 +1,5 @@
 (************************************************************************)
-(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
 (*  v      *         Copyright INRIA, CNRS and contributors             *)
 (* <O___,, * (see version control and CREDITS file for authors & dates) *)
 (*   \VV/  **************************************************************)
@@ -16,7 +16,7 @@ From Stdlib Require Import Bool NZParity NZPow NZSqrt NZLog NZGcd NZDiv NZBits.
 (** We obtain integers by postulating that successor of predecessor
     is identity. *)
 
-Module Type ZAxiom (Import Z : NZAxiomsSig').
+Module Type ZAxiom (Import Z : NZBasicFunsSig').
  Axiom succ_pred : forall n, S (P n) == n.
 End ZAxiom.
 
@@ -34,14 +34,14 @@ End OppNotation.
 
 Module Type Opp' (T:Typ) := Opp T <+ OppNotation T.
 
-Module Type IsOpp (Import Z : NZAxiomsSig')(Import O : Opp' Z).
+Module Type IsOpp (Import Z : NZBasicFunsSig')(Import O : Opp' Z).
 #[global]
  Declare Instance opp_wd : Proper (eq==>eq) opp.
  Axiom opp_0 : - 0 == 0.
  Axiom opp_succ : forall n, - (S n) == P (- n).
 End IsOpp.
 
-Module Type OppCstNotation (Import A : NZAxiomsSig)(Import B : Opp A).
+Module Type OppCstNotation (Import A : NZBasicFunsSig)(Import B : Opp A).
  Notation "- 1" := (opp one).
  Notation "- 2" := (opp two).
 End OppCstNotation.

theories/Numbers/Integer/Abstract/ZBase.v

@@ -1,5 +1,5 @@
 (************************************************************************)
-(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
 (*  v      *         Copyright INRIA, CNRS and contributors             *)
 (* <O___,, * (see version control and CREDITS file for authors & dates) *)
 (*   \VV/  **************************************************************)
@@ -17,6 +17,14 @@ From Stdlib Require Import NZMulOrder.
 Module ZBaseProp (Import Z : ZAxiomsMiniSig').
 Include NZMulOrderProp Z.
 
+Lemma Private_succ_pred n : n ~= 0 -> S (P n) == n.
+Proof. intros _; exact (succ_pred _). Qed.
+
+Lemma le_pred_l n : P n <= n.
+Proof. rewrite <-(succ_pred n), pred_succ; exact (le_succ_diag_r _). Qed.
+
+Include NZAddOrder.NatIntAddOrderProp Z.
+
 (* Theorems that are true for integers but not for natural numbers *)
 
 Theorem pred_inj : forall n m, P n == P m -> n == m.
@@ -35,3 +43,4 @@ Proof.
 Qed.
 
 End ZBaseProp.
+

theories/Numbers/Integer/Abstract/ZLt.v

@@ -1,5 +1,5 @@
 (************************************************************************)
-(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
 (*  v      *         Copyright INRIA, CNRS and contributors             *)
 (* <O___,, * (see version control and CREDITS file for authors & dates) *)
 (*   \VV/  **************************************************************)
@@ -47,11 +47,6 @@ Proof.
 intro n; rewrite <- (succ_pred n) at 2; apply lt_succ_diag_r.
 Qed.
 
-Theorem le_pred_l : forall n, P n <= n.
-Proof.
-intro; apply lt_le_incl; apply lt_pred_l.
-Qed.
-
 Theorem lt_le_pred : forall n m, n < m <-> n <= P m.
 Proof.
 intros n m; rewrite <- (succ_pred m); rewrite pred_succ. apply lt_succ_r.
@@ -132,3 +127,4 @@ setoid_replace (P 0) with (-1) in H2.
 Qed.
 
 End ZOrderProp.
+

theories/Numbers/Integer/Abstract/ZMul.v

@@ -1,5 +1,5 @@
 (************************************************************************)
-(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
 (*  v      *         Copyright INRIA, CNRS and contributors             *)
 (* <O___,, * (see version control and CREDITS file for authors & dates) *)
 (*   \VV/  **************************************************************)
@@ -27,18 +27,6 @@ Include ZAddProp Z.
 (** Theorems that are either not valid on N or have different proofs
     on N and Z *)
 
-Theorem mul_pred_r : forall n m, n * (P m) == n * m - n.
-Proof.
-intros n m.
-rewrite <- (succ_pred m) at 2.
-now rewrite mul_succ_r, <- add_sub_assoc, sub_diag, add_0_r.
-Qed.
-
-Theorem mul_pred_l : forall n m, (P n) * m == n * m - m.
-Proof.
-intros n m; rewrite (mul_comm (P n) m), (mul_comm n m). apply mul_pred_r.
-Qed.
-
 Theorem mul_opp_l : forall n m, (- n) * m == - (n * m).
 Proof.
 intros n m. apply add_move_0_r.
@@ -60,16 +48,6 @@ Proof.
 intros n m. now rewrite mul_opp_l, <- mul_opp_r.
 Qed.
 
-Theorem mul_sub_distr_l : forall n m p, n * (m - p) == n * m - n * p.
-Proof.
-intros n m p. do 2 rewrite <- add_opp_r. rewrite mul_add_distr_l.
-now rewrite mul_opp_r.
-Qed.
+End ZMulProp.
 
-Theorem mul_sub_distr_r : forall n m p, (n - m) * p == n * p - m * p.
-Proof.
-intros n m p; rewrite (mul_comm (n - m) p), (mul_comm n p), (mul_comm m p);
-now apply mul_sub_distr_l.
-Qed.
 
-End ZMulProp.