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.

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/ZAddOrder.v

@@ -163,6 +163,7 @@ 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));

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/NatInt/NZAddOrder.v

@@ -159,9 +159,6 @@ Qed.
 
 (** Subtraction *)
 
-(** We can prove the existence of a subtraction of any number by
-    a smaller one *)
-
 Lemma le_exists_sub : forall n m, n<=m -> exists p, m == p+n /\ 0<=p.
 Proof.
   intros n m H. apply le_ind with (4:=H). - solve_proper.
@@ -170,9 +167,228 @@ Proof.
     split. + nzsimpl. now f_equiv. + now apply le_le_succ_r.
 Qed.
 
-(** For the moment, it doesn't seem possible to relate
-    this existing subtraction with [sub].
-*)
+Lemma lt_exists_sub : forall n m, n<m -> exists p, m == p+n /\ 0<p.
+Proof.
+  intros n m I; pose proof (lt_le_incl _ _ I) as [p [E Ip]]%le_exists_sub.
+  exists p; split; [exact E |].
+  apply le_lteq in Ip as [Ip | Ep]; [exact Ip | exfalso].
+  apply (lt_irrefl m); rewrite E at 1; rewrite <-Ep, add_0_l; exact I.
+Qed.
 
 End NZAddOrderProp.
 
+Module Type NZSubNatInt
+  (Import NI : NatIntAxiomsSig')
+  (Import NIA : NZAddOrderProp NI)
+  (Import PNI : Private_NatIntOrderProp NI NIA NIA).
+
+Lemma Private_nat_sub_0_l : P 0 == 0 -> forall n, 0 - n == 0.
+Proof.
+  intros isNat; apply (nat_induction isNat); [now intros x y -> | |].
+  - rewrite sub_0_r; reflexivity.
+  - intros n IH; rewrite sub_succ_r, IH; exact isNat.
+Qed.
+
+Lemma Private_int_sub_succ_l :
+  (forall n, S (P n) == n) -> forall n m, S n - m == S (n - m).
+Proof.
+  intros isInt n. nzinduct m.
+  - rewrite 2!sub_0_r; reflexivity.
+  - intros m; split; intros IH.
+    + rewrite 2!sub_succ_r, IH, pred_succ, isInt; reflexivity.
+    + rewrite 2!sub_succ_r, isInt in IH.
+      rewrite <-(isInt (S n - m)), IH; reflexivity.
+Qed.
+
+Lemma sub_succ : forall n m, S n - S m == n - m.
+Proof.
+  destruct (int_or_nat) as [isInt | isNat].
+  - intros n m; rewrite Private_int_sub_succ_l, sub_succ_r, isInt
+      by (exact isInt); reflexivity.
+  - intros n; apply (nat_induction isNat); [now intros x y -> | |].
+    + rewrite sub_succ_r, 2!sub_0_r, pred_succ; reflexivity.
+    + intros m IH; rewrite sub_succ_r, IH, sub_succ_r; reflexivity.
+Qed.
+
+Lemma sub_diag : forall n, n - n == 0.
+Proof.
+  nzinduct n.
+  - rewrite sub_0_r; reflexivity.
+  - intros n; rewrite sub_succ; reflexivity.
+Qed.
+
+Lemma add_simpl_r : forall n m, n + m - m == n.
+Proof.
+  intros n; nzinduct m.
+  - rewrite add_0_r, sub_0_r; reflexivity.
+  - intros m; rewrite add_succ_r, sub_succ; reflexivity.
+Qed.
+
+(* add_sub was in Natural, add_simpl_r in Integer *)
+Notation add_sub := add_simpl_r.
+
+Theorem add_simpl_l n m : n + m - n == m.
+Proof. rewrite add_comm; exact (add_simpl_r _ _). Qed.
+
+Theorem sub_add_distr n m p : n - (m + p) == (n - m) - p.
+Proof.
+  destruct int_or_nat as [isInt | isNat].
+  - nzinduct p.
+    + rewrite sub_0_r, add_0_r; reflexivity.
+    + intros p; rewrite add_succ_r, 2!sub_succ_r; split.
+      * intros ->; reflexivity.
+      * intros ->%int_pred_inj; [reflexivity | exact isInt].
+  - revert p; apply (nat_induction isNat); [now intros x y -> | |].
+    + rewrite add_0_r, sub_0_r; reflexivity.
+    + intros p; rewrite add_succ_r, 2!sub_succ_r; intros ->; reflexivity.
+Qed.
+
+Theorem add_add_simpl_l_l n m p : (n + m) - (n + p) == m - p.
+Proof. rewrite sub_add_distr, add_simpl_l; reflexivity. Qed.
+
+Theorem add_add_simpl_l_r n m p : (n + m) - (p + n) == m - p.
+Proof. rewrite (add_comm p n), add_add_simpl_l_l; reflexivity. Qed.
+
+Theorem add_add_simpl_r_l n m p : (n + m) - (m + p) == n - p.
+Proof. rewrite (add_comm n m), add_add_simpl_l_l; reflexivity. Qed.
+
+Theorem add_add_simpl_r_r n m p : (n + m) - (p + m) == n - p.
+Proof. rewrite (add_comm p m), add_add_simpl_r_l; reflexivity. Qed.
+
+Theorem add_sub_eq_l : forall n m p, m + p == n -> n - m == p.
+Proof. intros n m p <-; exact (add_simpl_l _ _). Qed.
+
+Theorem add_sub_eq_r : forall n m p, m + p == n -> n - p == m.
+Proof. intros n m p; rewrite add_comm; exact (add_sub_eq_l _ _ _). Qed.
+
+Theorem lt_0_sub : forall n m, 0 < m - n <-> n < m.
+Proof.
+  intros n m; split; cycle 1. {
+    intros [p [-> Ip]]%lt_exists_sub; rewrite add_simpl_r; exact Ip.
+  }
+  destruct int_or_nat as [isInt | isNat].
+  - revert m; nzinduct n; [intros m; rewrite sub_0_r; intros H; exact H |].
+    intros n; split; intros IH.
+    + intros m; rewrite <-(isInt m), sub_succ; intros I%IH.
+      apply ->succ_lt_mono; exact I.
+    + intros m; rewrite <-sub_succ; intros I%IH; apply succ_lt_mono; exact I.
+  - revert n m.
+    apply (nat_induction isNat (fun n => (forall m, _ -> _))).
+    + intros x y E; split; intros H m; [rewrite <-E | rewrite E]; now apply H.
+    + intros m; rewrite sub_0_r; intros H; exact H.
+    + intros n IH m.
+      destruct (nat_zero_or_succ isNat m) as [-> | [m' ->]]. {
+        rewrite (Private_nat_sub_0_l isNat); intros []%lt_irrefl.
+      }
+      rewrite sub_succ; intros I%IH%succ_lt_mono; exact I.
+Qed.
+
+Lemma Private_nat_sub_0_le : P 0 == 0 -> forall n m, n - m == 0 <-> n <= m.
+Proof.
+  intros isNat n m; split; intros H.
+  - apply nlt_ge; intros [p [Ep Ip]]%lt_exists_sub.
+    rewrite Ep, add_simpl_r in H; rewrite H in Ip; apply lt_irrefl in Ip as [].
+  - apply le_antisymm; [| exact (nat_le_0_l isNat _)].
+    now apply nlt_ge; intros J; apply ->lt_0_sub in J; apply nlt_ge in H.
+Qed.
+
+Lemma Private_int_add_pred_l : (forall n, S (P n) == n) ->
+  forall n m, P n + m == P (n + m).
+Proof.
+  intros isInt n m; rewrite <-(isInt n) at 2; now rewrite add_succ_l, pred_succ.
+Qed.
+
+Lemma Private_int_sub_add :
+  (forall n, S (P n) == n) -> forall m n, m - n + n == m.
+Proof.
+  intros isInt m n; nzinduct n.
+  - rewrite sub_0_r, add_0_r; reflexivity.
+  - now intros n; rewrite add_succ_r, sub_succ_r, Private_int_add_pred_l, isInt.
+Qed.
+
+Lemma Private_sub_add_le : forall n m, n <= n - m + m.
+Proof.
+  destruct int_or_nat as [isInt | isNat]. {
+    intros n m; rewrite (Private_int_sub_add isInt); reflexivity.
+  }
+  intros n m; destruct (lt_ge_cases m n) as [I | I].
+  - apply lt_exists_sub in I as [p [-> I]]; rewrite add_simpl_r.
+    exact (le_refl _).
+  - apply (Private_nat_sub_0_le isNat) in I as E; rewrite E, add_0_l; exact I.
+Qed.
+
+Lemma Private_nat_nle_succ_0 : P 0 == 0 -> forall n, ~ (S n <= 0).
+Proof.
+  intros isNat; apply (nat_induction isNat).
+  - intros x y ->; reflexivity.
+  - intros H; apply nlt_ge in H; apply H; exact (lt_succ_diag_r _).
+  - intros n H; apply nle_gt; apply nle_gt in H; apply lt_trans with (1 := H).
+    exact (lt_succ_diag_r _).
+Qed.
+
+Lemma Private_sub_add : forall n m, n <= m -> (m - n) + n == m.
+Proof.
+  destruct int_or_nat as [isInt | isNat]. {
+    intros n m _; rewrite (Private_int_sub_add isInt); reflexivity.
+  }
+  apply (nat_induction isNat (fun n => forall m, _ -> _)).
+  - now intros x y E; split; intros H m; [rewrite <-E | rewrite E]; apply H.
+  - intros m _; rewrite add_0_r, sub_0_r; reflexivity.
+  - intros n IH m H; destruct (nat_zero_or_succ isNat m) as [E | [k E]].
+    + rewrite E in H; exfalso; exact (Private_nat_nle_succ_0 isNat n H).
+    + rewrite E, sub_succ, add_succ_r, IH; [reflexivity |].
+      apply succ_le_mono; rewrite E in H; exact H.
+Qed.
+
+Theorem le_sub_le_add_r : forall n m p, n - p <= m <-> n <= m + p.
+Proof.
+  intros n m p; split; intros H.
+  - apply (add_le_mono_r _ _ p) in H; apply le_trans with (2 := H).
+    exact (Private_sub_add_le _ _).
+  - destruct int_or_nat as [isInt | isNat]. {
+      now apply (add_le_mono_r _ _ p); rewrite (Private_int_sub_add isInt).
+    }
+    destruct (le_ge_cases n p) as [I | I].
+    + apply (Private_nat_sub_0_le isNat) in I as ->;
+        exact (nat_le_0_l isNat _).
+    + apply le_exists_sub in I as [k [Ek Ik]]; rewrite Ek, add_simpl_r.
+      apply (add_le_mono_r _ _ p); rewrite <-Ek; exact H.
+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; exact (le_sub_le_add_r _ _ _). Qed.
+
+Theorem lt_add_lt_sub_r : forall n m p, n + p < m <-> n < m - p.
+Proof.
+  intros n m p; split; intros H.
+  - apply (add_lt_mono_r _ _ p), lt_le_trans with (1 := H).
+    exact (Private_sub_add_le _ _).
+  - destruct int_or_nat as [isInt | isNat].
+    + apply (add_lt_mono_r _ _ p) in H.
+      rewrite (Private_int_sub_add isInt) in H; exact H.
+    + assert (p <= m) as I. {
+        apply lt_le_incl, lt_0_sub, le_lt_trans with (2 := H).
+        exact (nat_le_0_l isNat _).
+      }
+      apply (add_lt_mono_r _ _ p) in H.
+      rewrite Private_sub_add in H by (exact I); exact H.
+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; exact (lt_add_lt_sub_r _ _ _). 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 I H; apply add_le_lt_mono with (1 := I) in H as H'.
+  rewrite (add_comm n), (add_comm m) in H'.
+  assert (q - m + m == q) as Eq. {
+    destruct int_or_nat as [isInt | isNat];
+      [exact (Private_int_sub_add isInt _ _) |].
+    apply Private_sub_add, lt_le_incl, lt_0_sub, le_lt_trans with (2 := H).
+    exact (nat_le_0_l isNat _).
+  }
+  rewrite Eq in H'; apply le_lt_trans with (2 := H').
+  exact (Private_sub_add_le _ _).
+Qed.
+
+End NZSubNatInt.

theories/Numbers/NatInt/NZAxioms.v

@@ -47,6 +47,8 @@ Module Type
      forall A : t -> Prop,
      Proper (eq ==> iff) A ->
      A zero -> (forall n : t, A n <-> A (succ n)) -> forall n : t, A n.
+   Parameter Private_succ_pred :
+    forall n : t, ~ eq n zero -> eq (succ (pred n)) n.
    Parameter one : t.
    Parameter two : t.
    Parameter one_succ : eq one (succ zero).
@@ -204,11 +206,6 @@ End IsAddSubMul.
 Module Type NZBasicFunsSig := NZDomainSig <+ AddSubMul <+ IsAddSubMul.
 Module Type NZBasicFunsSig' := NZDomainSig' <+ AddSubMul' <+IsAddSubMul.
 
-(** Old name for the same interface: *)
-
-Module Type NZAxiomsSig := NZBasicFunsSig.
-Module Type NZAxiomsSig' := NZBasicFunsSig'.
-
 (** ** Axiomatization of order *)
 
 (** The module type [HasLt] (resp. [HasLe]) is just a type equipped with
@@ -228,8 +225,19 @@ End IsNZOrd.
 (** NB: the compatibility of [le] can be proved later from [lt_wd]
     and [lt_eq_cases] *)
 
+Module Type IsNatInt (Import NZ : NZOrd').
+ (** The following axiom (together with the axioms about orders) ensures that
+     the only models are indeed integers and natural numbers.
+     We keep it private in order to redefine it for integers. *)
+ Axiom Private_succ_pred : forall n, n ~= 0 -> S (P n) == n.
+ (** The following axiom will force [P 0 == 0] for natural numbers. *)
+ Axiom le_pred_l : forall n, P n <= n.
+End IsNatInt.
+
 Module Type NZOrdSig := NZOrd <+ IsNZOrd.
 Module Type NZOrdSig' := NZOrd' <+ IsNZOrd.
+Module Type NatIntSig := NZOrdSig <+ IsNatInt.
+Module Type NatIntSig' := NZOrdSig' <+ IsNatInt.
 
 (** Everything together : *)
 
@@ -241,6 +249,10 @@ Module Type NZOrdAxiomsSig <: NZBasicFunsSig <: NZOrdSig
 Module Type NZOrdAxiomsSig' <: NZOrdAxiomsSig
  := NZOrdSig' <+ AddSubMul' <+ IsAddSubMul <+ HasMinMax.
 
+Module Type NatIntAxiomsSig <: NZBasicFunsSig <: NZOrdSig <: NatIntSig
+ := NatIntSig <+ AddSubMul <+ IsAddSubMul <+ HasMinMax.
+Module Type NatIntAxiomsSig' <: NatIntAxiomsSig
+ := NatIntSig' <+ AddSubMul' <+ IsAddSubMul <+ HasMinMax.
 
 (** Same, plus a comparison function. *)
 
@@ -251,10 +263,13 @@ Module Type NZOrdAxiomsSig' <: NZOrdAxiomsSig
 
 Module Type NZDecOrdSig := NZOrdSig <+ HasCompare.
 Module Type NZDecOrdSig' := NZOrdSig' <+ HasCompare.
+Module Type NatIntDecSig := NatIntSig <+ HasCompare.
+Module Type NatIntDecSig' := NatIntSig' <+ HasCompare.
 
 Module Type NZDecOrdAxiomsSig := NZOrdAxiomsSig <+ HasCompare.
 Module Type NZDecOrdAxiomsSig' := NZOrdAxiomsSig' <+ HasCompare.
-
+Module Type NatIntDecAxiomsSig := NZOrdAxiomsSig <+ HasCompare.
+Module Type NatIntDecAxiomsSig' := NZOrdAxiomsSig' <+ HasCompare.
 (** A square function *)
 
 (* TODO: why is this here? *)

theories/Numbers/NatInt/NZDomain.v

@@ -329,7 +329,7 @@ End NZOfNatOrd.
 (** For basic operations, we can prove correspondence with
     their counterpart in [nat]. *)
 
-Module NZOfNatOps (Import NZ:NZAxiomsSig').
+Module NZOfNatOps (Import NZ:NZBasicFunsSig').
 Include NZOfNat NZ.
 Local Open Scope ofnat.