Subtraction in NatInt

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.

theories/Numbers/Cyclic/Abstract/NZCyclic.v

@@ -25,7 +25,7 @@ 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

@@ -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,

theories/Numbers/Integer/Abstract/ZAddOrder.v

@@ -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.

theories/Numbers/Integer/Abstract/ZAxioms.v

@@ -16,7 +16,7 @@ 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

@@ -17,6 +17,14 @@ 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.

theories/Numbers/Integer/Abstract/ZLt.v

@@ -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.

theories/Numbers/Integer/Abstract/ZMul.v

@@ -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,18 +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.
-
-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.