From 58a05369b22deca69007b314ff2e3eddb04587a1 Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Sun, 18 Feb 2024 16:54:53 +0100 Subject: [PATCH] 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 | 2 +- theories/Numbers/Integer/Abstract/ZAddOrder.v | 1 + theories/Numbers/Integer/Abstract/ZAxioms.v | 6 +- theories/Numbers/NatInt/NZAddOrder.v | 228 +++++++++++++++++- theories/Numbers/NatInt/NZAxioms.v | 27 ++- theories/Numbers/NatInt/NZDomain.v | 2 +- theories/Numbers/NatInt/NZOrder.v | 53 ++++ theories/Numbers/NatInt/NZParity.v | 2 +- 8 files changed, 303 insertions(+), 18 deletions(-) diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index f277588940f9c..d1a4dc2167242 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/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. diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index caba5925e8e17..29d493a645bf1 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/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)); diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index de01a78dab7ca..631d377f90623 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/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. diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v index 4182740c058e7..e6a750c9eeabf 100644 --- a/theories/Numbers/NatInt/NZAddOrder.v +++ b/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 exists p, m == p+n /\ 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. diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 840254cba5224..471822472d421 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/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? *) diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index 300ffcc2b0098..9e2aa378432b1 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/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. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 634c1574fff9a..aa855b95e4e11 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -669,6 +669,59 @@ End MeasureInduction. End NZOrderProp. +Module Type NatIntOrderProp + (Import NI : NatIntSig') + (Import NZBase : NZBaseProp NI). + +Include NZOrderProp NI NZBase. +Module PrivateNatIntOrderProp. +Theorem nat_le_0_l_aux : S (P 0) ~= 0 -> forall n, 0 <= n. +Proof. + intros H0 n. destruct (le_gt_cases 0 n) as [I | I]; [exact I |]. + exfalso; apply H0; apply lt_succ_pred in I; exact I. +Qed. + +Theorem int_or_nat : + (forall n, S (P n) == n) \/ (P 0 == 0). +Proof. + pose proof Private_succ_pred as HSP. + destruct (eq_decidable (S (P 0)) 0) as [E | NE]; [left | right]. + - intros n; destruct (eq_decidable n 0) as [-> | H%HSP]; [exact E | exact H]. + - pose proof le_pred_l as HP. + apply le_antisymm; [exact (HP 0) | apply nat_le_0_l_aux; exact NE]. +Qed. + +Theorem nat_le_0_l : P 0 == 0 -> forall n, 0 <= n. +Proof. + intros H; apply nat_le_0_l_aux; rewrite H; exact (neq_succ_diag_l _). +Qed. + +Lemma int_pred_inj : + (forall n, S (P n) == n) -> forall n m, pred n == pred m -> n == m. +Proof. + intros isInt n m H; rewrite <-(isInt n), <-(isInt m), H; reflexivity. +Qed. + +Lemma nat_zero_or_succ : + P 0 == 0 -> forall n, n == 0 \/ exists m, n == S m. +Proof. + intros H n. + pose proof (nat_le_0_l H n) as [E | I]%le_lteq; [| now left]. + right; apply lt_succ_pred in E; exists (P n); symmetry; exact E. +Qed. + +Theorem nat_induction : + P 0 == 0 -> forall Q : t -> Prop, Proper (eq ==> iff) Q -> Q 0 -> + (forall n, Q n -> Q (S n)) -> forall n, Q n. +Proof. + intros isNat Q Qprop H0 IH n. + apply right_induction with 0; + [exact Qprop | exact H0 | intros m _; exact (IH _) |]. + apply nat_le_0_l; exact isNat. +Qed. +End PrivateNatIntOrderProp. +End NatIntOrderProp. + (* If we have moreover a [compare] function, we can build an [OrderedType] structure. *) diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v index 45df36a4f63cb..3b3e70db94b09 100644 --- a/theories/Numbers/NatInt/NZParity.v +++ b/theories/Numbers/NatInt/NZParity.v @@ -12,7 +12,7 @@ Require Import Bool NZAxioms NZMulOrder. (** Parity functions *) -Module Type NZParity (Import A : NZAxiomsSig'). +Module Type NZParity (Import A : NZBasicFunsSig'). Parameter Inline even odd : t -> bool. Definition Even n := exists m, n == 2*m. Definition Odd n := exists m, n == 2*m+1.