From 493dc64d50f920291a86c11fde19b71fdfbed36c Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Mon, 10 Mar 2025 16:57:29 +0100 Subject: [PATCH] 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 --- theories/Numbers/Cyclic/Abstract/NZCyclic.v | 2 +- theories/Numbers/Integer/Abstract/ZAdd.v | 45 +--- theories/Numbers/Integer/Abstract/ZAddOrder.v | 34 +-- theories/Numbers/Integer/Abstract/ZAxioms.v | 6 +- theories/Numbers/Integer/Abstract/ZBase.v | 9 + theories/Numbers/Integer/Abstract/ZLt.v | 6 +- theories/Numbers/Integer/Abstract/ZMul.v | 24 +- theories/Numbers/NatInt/NZAddOrder.v | 248 +++++++++++++++++- theories/Numbers/NatInt/NZAxioms.v | 235 +++++++---------- theories/Numbers/NatInt/NZDomain.v | 2 +- theories/Numbers/NatInt/NZOrder.v | 103 +++++++- theories/Numbers/NatInt/NZParity.v | 2 +- theories/Numbers/Natural/Abstract/NBase.v | 96 +++---- theories/Numbers/Natural/Abstract/NOrder.v | 9 +- theories/Numbers/Natural/Abstract/NSub.v | 153 +---------- 15 files changed, 500 insertions(+), 474 deletions(-) diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 7d2525917e..bfbb92850d 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -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. diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index 339953d81c..324307d9b1 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/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, @@ -293,3 +249,4 @@ Qed. (** Of course, there are many other variants *) End ZAddProp. + diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index 1263305ced..5e4257c130 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/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. @@ -283,3 +253,5 @@ End PosNeg. Ltac zero_pos_neg n := induction_maker n ltac:(apply zero_pos_neg). End ZAddOrderProp. + + diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index 732d0ed455..811d856d31 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -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. diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 581f278315..e2fd78efbe 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -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. + diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index 407be64874..48e9988f9d 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/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. @@ -132,3 +127,4 @@ setoid_replace (P 0) with (-1) in H2. Qed. End ZOrderProp. + diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v index 1694e538a4..8941c155b0 100644 --- a/theories/Numbers/Integer/Abstract/ZMul.v +++ b/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,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. diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v index 7546755a49..5b8a2ccdcc 100644 --- a/theories/Numbers/NatInt/NZAddOrder.v +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -14,9 +14,12 @@ * Properties of orders and addition for modules implementing [NZOrdAxiomsSig'] This file defines the [NZAddOrderProp] functor type, meant to be [Include]d -in a module implementing [NZOrdAxiomsSig'] (see [Stdlib.Numbers.NatInt.NZAxioms]). +in a module implementing [NZOrdAxiomsSig'] (see [Coq.Numbers.NatInt.NZAxioms]). This gives important basic compatibility lemmas between [add] and [lt], [le]. + +In the second part of this file, we further assume [IsNatInt] and prove +results about subtraction which are shared between integers and natural numbers. *) From Stdlib.Numbers.NatInt Require Import NZAxioms NZBase NZMul NZOrder. @@ -159,9 +162,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,8 +170,242 @@ 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 (Private_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; rewrite 2!sub_succ_r, isInt; split; intros IH; + [rewrite IH, pred_succ | rewrite <-IH, isInt]; reflexivity. +Qed. + +Lemma sub_succ : forall n m, S n - S m == n - m. +Proof. + destruct (Private_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 (Private_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 | 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 *) +(* TODO: should we keep both? *) +Lemma add_sub : forall n m, n + m - m == n. +Proof. exact add_simpl_r. Qed. + +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 Private_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. + symmetry; exact (Private_int_pred_inj isInt _ _). + - revert p; apply (Private_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. + +Lemma Private_nat_sub_0_le : P 0 == 0 -> forall n m, n - m == 0 <-> n <= m. +Proof. + intros isNat; apply (Private_nat_induction isNat (fun n => forall m, _)). + - intros x y H; split; intros H' n; [rewrite <-H | rewrite H]; exact (H' _). + - intros m; rewrite (Private_nat_sub_0_l isNat); split; intros _; + [exact (Private_nat_le_0_l isNat _) | reflexivity]. + - intros n IH m; destruct (Private_nat_zero_or_succ isNat m) as [-> | [m' ->]]. + + rewrite sub_0_r; split; intros H; exfalso. + * apply (Private_nat_neq_succ_0 isNat n); exact H. + * apply (Private_nat_nle_succ_0 isNat n); exact H. + + rewrite sub_succ, <-succ_le_mono; exact (IH _). +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. + +Theorem lt_0_sub : forall n m, 0 < m - n <-> n < m. +Proof. + destruct Private_int_or_nat as [isInt | isNat]. + - intros n m; rewrite (add_lt_mono_r 0 (m - n) n), add_0_l. + rewrite (Private_int_sub_add isInt); reflexivity. + - intros n m; rewrite <-(Private_nat_neq_0_lt_0 isNat), lt_nge; split; + intros H1 H2%(Private_nat_sub_0_le isNat); apply H1; exact H2. +Qed. + +Lemma Private_sub_add : forall n m, n <= m -> (m - n) + n == m. +Proof. + destruct Private_int_or_nat as [isInt | isNat]. { + intros n m _; rewrite (Private_int_sub_add isInt); reflexivity. + } + apply (Private_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 (Private_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. + +Lemma Private_sub_add_le : forall n m, n <= n - m + m. +Proof. + destruct Private_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. + +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 Private_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 (Private_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 Private_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 (Private_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 Private_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 (Private_nat_le_0_l isNat _). + } + rewrite Eq in H'; apply le_lt_trans with (2 := H'). + exact (Private_sub_add_le _ _). +Qed. + +Theorem mul_pred_r : forall n m, n * (P m) == n * m - n. +Proof. + intros n m; destruct (eq_decidable m 0) as [-> | H%Private_succ_pred]. + - destruct Private_int_or_nat as [isInt | isNat]. + + rewrite <-(isInt 0) at 2; rewrite mul_succ_r, add_sub; reflexivity. + + rewrite isNat, mul_0_r, Private_nat_sub_0_l by (exact isNat); reflexivity. + - rewrite <-H at 2; rewrite mul_succ_r, add_sub; reflexivity. +Qed. + +Theorem mul_pred_l : forall n m, P n * m == n * m - m. +Proof. intros n m; rewrite mul_comm, mul_pred_r, mul_comm; reflexivity. Qed. + +Theorem mul_sub_distr_r : forall n m p, (n - m) * p == n * p - m * p. +Proof. + intros n m p; destruct Private_int_or_nat as [isInt | isNat]. + - nzinduct m; [| intros m'; split]. + + rewrite mul_0_l, 2!sub_0_r; reflexivity. + + now intros H; rewrite sub_succ_r, mul_pred_l, H, mul_succ_l, sub_add_distr. + + intros H; rewrite <-(Private_int_sub_add isInt ((n - m') * p) p). + rewrite sub_succ_r, mul_pred_l, mul_succ_l, sub_add_distr in H. + rewrite H, Private_int_sub_add by (exact isInt); reflexivity. + - revert m; apply (Private_nat_induction isNat). + + intros x y ->; reflexivity. + + rewrite mul_0_l, 2!sub_0_r; reflexivity. + + intros m H; rewrite sub_succ_r, mul_pred_l, mul_succ_l, sub_add_distr, H. + reflexivity. +Qed. + +Theorem mul_sub_distr_l : forall n m p, n * (m - p) == n * m - n * p. +Proof. + intros n m p; rewrite (mul_comm n (m - p)), (mul_comm n m), (mul_comm n p). + exact (mul_sub_distr_r _ _ _). +Qed. + +End NatIntAddOrderProp. diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index a024c34009..6f01f4cbaf 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -10,103 +10,81 @@ (** Initial Author : Evgeny Makarov, INRIA, 2007 *) -(** * Axioms for a domain with [zero], [succ], [pred]. *) +(** * Axioms for a domain with [zero], [succ], [pred], [le] and [lt] *) + +(** This file is the starting point of a modular and axiomatic development of +natural numbers and integers. The files and modules in [Coq.Numbers.NatInt] +contain specifications and proofs which are common to natural numbers and +integers. The files and modules in [Coq.Numbers.Natural.Abstract] give specific +results about natural numbers, with the extra axiom that the predecessor of 0 +is 0, while the sublibrary [Coq.Numbers.Integer.Abstract] give specific +results about integers, with the extra axiom that successor and predecessor +are one-to-one correspondences. + +The module type [NZDomainSig'] specifies a type [t] with: +- a general equality [eq], denoted by [==] and its negation [neq] denoted by [~=], +- a constant [zero] denoted by [0] and unary operators [succ] and [pred], + denoted by [S] and [P] satisfying + - [pred_succ : forall n, P (S n) == n] + - [bi_induction], a bidirectional induction principle centered at [0] +- the constants [1 = S 0] and [2 = S 1] + +The module type [NZOrdSig'] further assumes the existence of the predicates +[le] (denoted by [<=]) and [lt] (denoted by [<]) satisfying +- [lt_eq_cases : forall n m : t, n <= m <-> n < m \/ n == m] +- [lt_irrefl : forall n : t, ~ n < n] +- [lt_succ_r : forall n m : t, n < S m <-> n <= m] +The combined specification, imposes that the models of this theory are +infinite. There are two cases: +- either [S] is surjective, in which case we have integers +- or there exists a unique initial point [i <= 0] such that [S (P i) ~= i], + in which case we have natural numbers, possibly shifted on the left; the + predecessor of the initial point being arbitrary. + +The interested reader can refer to [Coq.Numbers.NatInt.NZOrder], in particular +[lt_exists_pred], [lt_succ_pred] and the module type [NatIntOrderProp]. + +This underspecification in the natural case prevented to state common results +about subtraction, therefore we complete it with the module type [IsNatInt] +which further imposes: +- [Private_succ_pred : forall n, n ~= 0 -> S (P n) == n] +- [le_pred_l : forall n, P n <= n] +In the natural case, this forces the initial point to be [0] and [P 0 == 0]. +So this restricts the models to only natural numbers or integers. +The module type [IsNatInt] is currently kept separate from all the other module +types for technical and historical reasons. + +The module type [NZBasicFunsSig'] adds to [NZDomainSig'] the operations [add], +[sub] and [mul] denoted by [+], [-] and [*] respectively, satisfying +- [add_0_l : forall n, 0 + n == n] +- [add_succ_l : forall n m, (S n) + m == S (n + m)] +- [sub_0_r : forall n, n - 0 == n] +- [sub_succ_r : forall n m, n - (S m) == P (n - m)] +- [mul_0_l : forall n, 0 * n == 0] +- [mul_succ_l : forall n m, S n * m == n * m + m] + +We build the module type [NZOrdAxiomsSig'] by adding the orders as well as +[min] and [max] functions consistent with [le]. + +Finally, [NZDecOrdAxiomsSig'] is obtained by adding a three-valued [compare] +function, therefore imposing that equality and orders are decidable. +*) From Stdlib.Structures Require Export Equalities Orders. (** We use the [Equalities] module in order to work with a general decidable - equality [eq]. *) - -(** The [Orders] module contains module types about orders [lt] and [le] in - [Prop]. -*) +equality [eq]. The [Orders] module contains module types about orders [lt] and +[le] in [Prop]. *) From Stdlib.Numbers Require Export NumPrelude. From Stdlib.Structures Require Export GenericMinMax. -(** The [GenericMinMax] module adds specifications and basic lemmas for [min] - and [max] operators on ordered types. *) - - -(** At the end of the day, this file defines the module types - [NZDecOrdAxiomsSig] and [NZDecOrdAxiomsSig'] (with notations) : -[[ -Module Type - NZDecOrdAxiomsSig' = - Sig - Parameter t : Type. - Parameter eq : t -> t -> Prop. - Parameter eq_equiv : Equivalence eq. - Parameter zero : t. - Parameter succ : t -> t. - Parameter pred : t -> t. - Parameter succ_wd : Proper (eq ==> eq) succ. - Parameter pred_wd : Proper (eq ==> eq) pred. - Parameter pred_succ : forall n : t, eq (pred (succ n)) n. - Parameter bi_induction : - forall A : t -> Prop, - Proper (eq ==> iff) A -> - A zero -> (forall n : t, A n <-> A (succ n)) -> forall n : t, A n. - Parameter one : t. - Parameter two : t. - Parameter one_succ : eq one (succ zero). - Parameter two_succ : eq two (succ one). - Parameter lt : t -> t -> Prop. - Parameter le : t -> t -> Prop. - Parameter lt_wd : Proper (eq ==> eq ==> iff) lt. - Parameter lt_eq_cases : forall n m : t, le n m <-> lt n m \/ eq n m. - Parameter lt_irrefl : forall n : t, ~ lt n n. - Parameter lt_succ_r : forall n m : t, lt n (succ m) <-> le n m. - Parameter add : t -> t -> t. - Parameter sub : t -> t -> t. - Parameter mul : t -> t -> t. - Parameter add_wd : Proper (eq ==> eq ==> eq) add. - Parameter sub_wd : Proper (eq ==> eq ==> eq) sub. - Parameter mul_wd : Proper (eq ==> eq ==> eq) mul. - Parameter add_0_l : forall n : t, eq (add zero n) n. - Parameter add_succ_l : - forall n m : t, eq (add (succ n) m) (succ (add n m)). - Parameter sub_0_r : forall n : t, eq (sub n zero) n. - Parameter sub_succ_r : - forall n m : t, eq (sub n (succ m)) (pred (sub n m)). - Parameter mul_0_l : forall n : t, eq (mul zero n) zero. - Parameter mul_succ_l : - forall n m : t, eq (mul (succ n) m) (add (mul n m) m). - Parameter max : t -> t -> t. - Parameter max_l : forall x y : t, le y x -> eq (max x y) x. - Parameter max_r : forall x y : t, le x y -> eq (max x y) y. - Parameter min : t -> t -> t. - Parameter min_l : forall x y : t, le x y -> eq (min x y) x. - Parameter min_r : forall x y : t, le y x -> eq (min x y) y. - Parameter compare : t -> t -> comparison. - Parameter compare_spec : - forall x y : t, CompareSpec (eq x y) (lt x y) (lt y x) (compare x y). - End -]] - *) - -(** ** Axiomatization of a domain with [zero], [succ], [pred] and a bi-directional induction principle. *) - -(* NB: This was Pierre Letouzey's conclusion in the (now deprecated) NZDomain - file. *) -(** We require [P (S n) = n] but not the other way around, since this domain - is meant to be either N or Z. In fact it can be a few other things, - - S is always injective, P is always surjective (thanks to [pred_succ]). - - I) If S is not surjective, we have an initial point, which is unique. - This bottom is below zero: we have N shifted (or not) to the left. - P cannot be injective: P init = P (S (P init)). - (P init) can be arbitrary. - - II) If S is surjective, we have [forall n, S (P n) = n], S and P are - bijective and reciprocal. - - IIa) if [exists k<>O, 0 == S^k 0], then we have a cyclic structure Z/nZ - IIb) otherwise, we have Z -*) +(** The [GenericMinMax] module gives specifications and basic lemmas for [min] + and [max] operators on ordered types. *) -(** The [Typ] module type in [Equalities] only has a parameter [t : Type]. *) +(** ** Axiomatization of a domain with [zero], [succ], [pred] and a bi-directional induction principle *) + +(** The [Typ] module type in [Equalities] has a unique parameter [t : Type]. *) Module Type ZeroSuccPred (Import T:Typ). Parameter Inline(20) zero : t. @@ -124,7 +102,7 @@ Module Type ZeroSuccPred' (T:Typ) := ZeroSuccPred T <+ ZeroSuccPredNotation T. (** The [Eq'] module type in [Equalities] is a [Type] [t] with a binary predicate - [eq] denoted [==]. The negation of [==] is denoted [~=]. *) + [eq] denoted by [==]. The negation of [==] is denoted by [~=]. *) Module Type IsNZDomain (Import E:Eq')(Import NZ:ZeroSuccPred' E). #[global] @@ -137,11 +115,8 @@ Module Type IsNZDomain (Import E:Eq')(Import NZ:ZeroSuccPred' E). A 0 -> (forall n, A n <-> A (S n)) -> forall n, A n. End IsNZDomain. -(** ** Axiomatization of some more constants *) - -(** Simply denoting "1" for (S 0) and so on works ok when implementing - by [nat], but leaves some ([N.succ N0]) when implementing by [N]. -*) +(* Simply denoting "1" for (S 0) and so on works ok when implementing +by [nat], but leaves some ([N.succ N0]) when implementing by [N]. *) Module Type OneTwo (Import T:Typ). Parameter Inline(20) one two : t. @@ -165,12 +140,33 @@ Module Type NZDomainSig := Module Type NZDomainSig' := EqualityType' <+ ZeroSuccPred' <+ IsNZDomain <+ OneTwo' <+ IsOneTwo. -(** At this point, a module implementing [NZDomainSig] has : -- two unary operators [pred] and [succ] such that - [forall n, pred (succ n) = n]. -- a bidirectional induction principle -- three constants [0], [1 = S 0], [2 = S 1] -*) +(** ** Axiomatization of order *) + +(** The module type [HasLt] (resp. [HasLe]) is just a type equipped with +a relation [lt] (resp. [le]) in [Prop]. *) + +Module Type NZOrd := NZDomainSig <+ HasLt <+ HasLe. +Module Type NZOrd' := NZDomainSig' <+ HasLt <+ HasLe <+ + LtNotation <+ LeNotation <+ LtLeNotation. + +Module Type IsNZOrd (Import NZ : NZOrd'). +#[global] + Declare Instance lt_wd : Proper (eq ==> eq ==> iff) lt. + Axiom lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. + Axiom lt_irrefl : forall n, ~ (n < n). + Axiom lt_succ_r : forall n m, n < S m <-> n <= m. +End IsNZOrd. + +(* NB: the compatibility of [le] can be proved later from [lt_wd] and +[lt_eq_cases]. *) + +Module Type NZOrdSig := NZOrd <+ IsNZOrd. +Module Type NZOrdSig' := NZOrd' <+ IsNZOrd. + +Module Type IsNatInt (Import NZ : NZOrdSig'). + Axiom Private_succ_pred : forall n, n ~= 0 -> S (P n) == n. + Axiom le_pred_l : forall n, P n <= n. +End IsNatInt. (** ** Axiomatization of basic operations : [+] [-] [*] *) @@ -204,50 +200,19 @@ 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 - a relation [lt] (resp. [le]) in [Prop]. *) -Module Type NZOrd := NZDomainSig <+ HasLt <+ HasLe. -Module Type NZOrd' := NZDomainSig' <+ HasLt <+ HasLe <+ - LtNotation <+ LeNotation <+ LtLeNotation. - -Module Type IsNZOrd (Import NZ : NZOrd'). -#[global] - Declare Instance lt_wd : Proper (eq ==> eq ==> iff) lt. - Axiom lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. - Axiom lt_irrefl : forall n, ~ (n < n). - Axiom lt_succ_r : forall n m, n < S m <-> n <= m. -End IsNZOrd. - -(** NB: the compatibility of [le] can be proved later from [lt_wd] - and [lt_eq_cases] *) - -Module Type NZOrdSig := NZOrd <+ IsNZOrd. -Module Type NZOrdSig' := NZOrd' <+ IsNZOrd. - -(** Everything together : *) +(** ** Everything together with [min], [max] and [compare] functions *) (** The [HasMinMax] module type is a type with [min] and [max] operators - consistent with [le]. *) +consistent with [le]. *) Module Type NZOrdAxiomsSig <: NZBasicFunsSig <: NZOrdSig := NZOrdSig <+ AddSubMul <+ IsAddSubMul <+ HasMinMax. Module Type NZOrdAxiomsSig' <: NZOrdAxiomsSig := NZOrdSig' <+ AddSubMul' <+ IsAddSubMul <+ HasMinMax. - -(** Same, plus a comparison function. *) - (** The [HasCompare] module type requires a comparison function in type - [comparison] consistent with [eq] and [lt]. In particular, this imposes - that the order is decidable. -*) +[comparison] consistent with [eq] and [lt]. In particular, this imposes +that the order is decidable. *) Module Type NZDecOrdSig := NZOrdSig <+ HasCompare. Module Type NZDecOrdSig' := NZOrdSig' <+ HasCompare. diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index bfd3bf9d1d..ff23fc46ca 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 722e607a01..bf3944c652 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -11,10 +11,12 @@ (************************************************************************) (** -* Lemmas about orders for modules implementing [NZOrdSig'] +* Lemmas about orders for natural numbers or integers This file defines the [NZOrderProp] functor type, meant to be [Include]d in -a module implementing the [NZOrdSig'] module type. +a module implementing the [NZOrdSig'] module type and the [NatIntOrderProp] +functor type (with only private lemmas) about modules further implementing +the [IsNatInt] module type. It contains lemmas and tactics about [le], [lt] and [eq]. @@ -24,11 +26,15 @@ The firt part contains important basic lemmas about [le] and [lt], for instance - decidability lemmas like [le_gt_cases], [eq_decidable], ... It also adds the following tactics: - [le_elim H] to reason by cases on an hypothesis [(H) : n <= m] -- the domain-agnostic [order] (see [Stdlib.Structures.OrdersTac]) and [order'] +- the domain-agnostic [order] (see [Coq.Structures.OrdersTac]) and [order'] which knows that [0 < 1 < 2] The second part proves many induction principles involving the orders and defines the tactic notation [nzord_induct]. + +The third part contains private results stating in particular that the models +satisfying [IsNatInt] as exactly natural numbers or integers. These private +lemma are useful later to prove lemmas about subtraction (see [NZAddOrder]). *) From Stdlib.Numbers.NatInt Require Import NZAxioms NZBase. From Stdlib.Logic Require Import Decidable. @@ -117,7 +123,7 @@ Qed. Notation lt_eq_gt_cases := lt_trichotomy (only parsing). -(** *** Asymmetry and transitivity. *) +(** *** Asymmetry and transitivity *) Theorem lt_asymm : forall n m, n < m -> ~ m < n. Proof. @@ -669,11 +675,86 @@ End MeasureInduction. End NZOrderProp. -(* If we have moreover a [compare] function, we can build - an [OrderedType] structure. *) +(** ** Private basic lemmas for modules satisfying [IsNatInt] -(* Temporary workaround for bug #2949: remove this problematic + unused functor -Module NZOrderedType (NZ : NZDecOrdSig') - <: DecidableTypeFull <: OrderedTypeFull - := NZ <+ NZBaseProp <+ NZOrderProp <+ Compare2EqBool <+ HasEqBool2Dec. -*) +Unfortunately, we need a little part of the specific theories of natural numbers +and integers in order to prove common lemmas afterwards. Since these lemmas +have an additional condition, they must be kept private before being + specialized in [Natural] and/or [Integer]. *) + +Module Type NatIntOrderProp + (Import NZ : NZOrdSig') + (Import NI : IsNatInt NZ) + (Import NZBase : NZBaseProp NZ) + (Import NZOP : NZOrderProp NZ NZBase). + +Lemma Private_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. + +Lemma Private_int_or_nat : (forall n, S (P n) == n) \/ (P 0 == 0). +Proof. + destruct (eq_decidable (S (P 0)) 0) as [E | NE]; [left; intros n | right]. + - now destruct (eq_decidable n 0) as [-> | ->%Private_succ_pred]. + - now apply le_antisymm; [exact (le_pred_l 0) | apply Private_nat_le_0_l_aux]. +Qed. + +Lemma Private_nat_le_0_l : P 0 == 0 -> forall n, 0 <= n. +Proof. + intros H; apply Private_nat_le_0_l_aux; rewrite H; exact (neq_succ_diag_l _). +Qed. + +Lemma Private_nat_neq_succ_0 : P 0 == 0 -> forall n, S n ~= 0. +Proof. + intros H n E; rewrite <-E in H at 1; rewrite pred_succ in H; rewrite H in E. + now apply (neq_succ_diag_l 0). +Qed. + +Lemma Private_nat_zero_or_succ : + P 0 == 0 -> forall n, n == 0 \/ exists m, n == S m. +Proof. + intros H n; destruct (eq_decidable n 0) as [-> | NE]; [now left | right]. + exists (P n); symmetry; exact (Private_succ_pred n NE). +Qed. + +Theorem Private_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 Private_nat_le_0_l; exact isNat. +Qed. + +Lemma Private_nat_nle_succ_0 : P 0 == 0 -> forall n, ~ (S n <= 0). +Proof. + intros isNat n; apply nle_gt, le_neq; split. + - exact (Private_nat_le_0_l isNat _). + - apply neq_sym; exact (Private_nat_neq_succ_0 isNat _). +Qed. + +Lemma Private_nat_nlt_0_r : P 0 == 0 -> forall n, ~ n < 0. +Proof. + intros isNat n I; apply (lt_irrefl 0), le_lt_trans with (2 := I). + exact (Private_nat_le_0_l isNat n). +Qed. + +Lemma Private_nat_neq_0_lt_0 : P 0 == 0 -> forall n, n ~= 0 <-> 0 < n. +Proof. + intros isNat n; destruct (Private_nat_zero_or_succ isNat n) as [-> | [m ->]]. + - split; intros H; exfalso; + [apply H; reflexivity | apply (lt_irrefl 0); exact H]. + - split; intros _. + + apply nle_gt; exact (Private_nat_nle_succ_0 isNat _). + + exact (Private_nat_neq_succ_0 isNat _). +Qed. + +Lemma Private_int_pred_inj : + (forall n, S (P n) == n) -> forall n m, pred n == pred m <-> n == m. +Proof. + intros isInt n m; split; [| intros ->; reflexivity]. + intros H; rewrite <-(isInt n), <-(isInt m), H; reflexivity. +Qed. +End NatIntOrderProp. diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v index 3f6385e628..2cf6e560b0 100644 --- a/theories/Numbers/NatInt/NZParity.v +++ b/theories/Numbers/NatInt/NZParity.v @@ -12,7 +12,7 @@ From Stdlib 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. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index d00633cc4e..1d1c329c04 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -15,47 +15,46 @@ From Stdlib Require Export NAxioms. From Stdlib Require Import NZMulOrder. Module NBaseProp (Import N : NAxiomsMiniSig'). -(** First, we import all known facts about both natural numbers and integers. *) + (** First, we import all known facts about modules implementing [NZAxiomsSig]. *) Include NZMulOrderProp N. -(** From [pred_0] and order facts, we can prove that 0 isn't a successor. *) +(** Now we prove that [NAxiomsMiniSig'] specializes [NZAxioms.IsNatInt]. *) -Theorem neq_succ_0 : forall n, S n ~= 0. +Lemma Private_succ_pred n : n ~= 0 -> S (P n) == n. Proof. - intros n EQ. - assert (EQ' := pred_succ n). - rewrite EQ, pred_0 in EQ'. - rewrite <- EQ' in EQ. - now apply (neq_succ_diag_l 0). + intros Hn; apply (lt_succ_pred 0), le_neq; split; [| exact (neq_sym _ _ Hn)]. + destruct (le_gt_cases 0 n) as [I | I%lt_succ_pred]; [exact I | exfalso]. + rewrite pred_0 in I; apply (neq_succ_diag_l 0); exact I. Qed. -Theorem neq_0_succ : forall n, 0 ~= S n. +Lemma le_pred_l n : P n <= n. Proof. -intro n; apply neq_sym; apply neq_succ_0. + destruct (eq_decidable n 0) as [-> | H]. + - rewrite pred_0; exact (le_refl 0). + - apply Private_succ_pred in H; rewrite <-H at 2; exact (le_succ_diag_r _). Qed. -(** Next, we show that all numbers are nonnegative and recover regular - induction from the bidirectional induction on NZ *) +Include NZAddOrder.NatIntAddOrderProp N. + +Theorem succ_pred n : n ~= 0 -> S (P n) == n. +Proof. exact (Private_succ_pred n). Qed. Theorem le_0_l : forall n, 0 <= n. -Proof. -intro n; nzinduct n. -- now apply eq_le_incl. -- intro n; split. - + apply le_le_succ_r. - + intro H; apply le_succ_r in H; destruct H as [H | H]. - * assumption. - * symmetry in H; false_hyp H neq_succ_0. -Qed. +Proof. exact (Private_nat_le_0_l pred_0). Qed. + +Theorem neq_succ_0 : forall n, S n ~= 0. +Proof. exact (Private_nat_neq_succ_0 pred_0). Qed. + +Theorem neq_0_succ : forall n, 0 ~= S n. +Proof. intros n; apply neq_sym; exact (neq_succ_0 _). Qed. + +Theorem zero_or_succ n : n == 0 \/ exists m, n == S m. +Proof. exact (Private_nat_zero_or_succ pred_0 n). Qed. Theorem induction : forall A : N.t -> Prop, Proper (N.eq==>iff) A -> A 0 -> (forall n, A n -> A (S n)) -> forall n, A n. -Proof. -intros A A_wd A0 AS n; apply right_induction with 0; try assumption. -- intros; auto; apply le_0_l. -- apply le_0_l. -Qed. +Proof. exact (Private_nat_induction pred_0). Qed. (** The theorems [bi_induction], [central_induction] and the tactic [nzinduct] refer to bidirectional induction, which is not useful on natural @@ -76,52 +75,24 @@ Qed. Ltac cases n := induction_maker n ltac:(apply case_analysis). Theorem neq_0 : ~ forall n, n == 0. -Proof. -intro H; apply (neq_succ_0 0). apply H. -Qed. +Proof. intros H; exact (neq_succ_0 0 (H (S 0))). Qed. Theorem neq_0_r n : n ~= 0 <-> exists m, n == S m. Proof. - cases n. - - split; intro H;[now elim H | destruct H as [m H]; - symmetry in H; false_hyp H neq_succ_0]. - - intro n; split; intro H; [now exists n | apply neq_succ_0]. -Qed. - -Theorem zero_or_succ n : n == 0 \/ exists m, n == S m. -Proof. -cases n. -- now left. -- intro n; right; now exists n. + split; [intros H%succ_pred | intros [m ->]; exact (neq_succ_0 _)]. + exists (P n); symmetry; exact H. Qed. Theorem eq_pred_0 n : P n == 0 <-> n == 0 \/ n == 1. Proof. -cases n. -- rewrite pred_0. now split; [left|]. -- intro n. rewrite pred_succ. - split. - + intros H; right. now rewrite H, one_succ. - + intros [H|H]. - * elim (neq_succ_0 _ H). - * apply succ_inj_wd. now rewrite <- one_succ. -Qed. - -Theorem succ_pred n : n ~= 0 -> S (P n) == n. -Proof. -cases n. -- intro H; exfalso; now apply H. -- intros; now rewrite pred_succ. + rewrite one_succ; split. + - destruct (zero_or_succ n) as [-> | [m ->]]; [intros _; left; reflexivity |]. + rewrite pred_succ; intros ->; right; reflexivity. + - intros [-> | ->]; [exact pred_0 | exact (pred_succ 0)]. Qed. Theorem pred_inj n m : n ~= 0 -> m ~= 0 -> P n == P m -> n == m. -Proof. -cases n. -- intros H; exfalso; now apply H. -- intros n _; cases m. - + intros H; exfalso; now apply H. - + intros m H2 H3. do 2 rewrite pred_succ in H3. now rewrite H3. -Qed. +Proof. intros H%succ_pred K%succ_pred L; rewrite <-H, <-K, L; reflexivity. Qed. (** The following induction principle is useful for reasoning about, e.g., Fibonacci numbers *) @@ -190,3 +161,4 @@ Ltac double_induct n m := [solve_proper | | | ]. End NBaseProp. + diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 4554c4b116..aac3abaa1c 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -26,7 +26,7 @@ setoid_replace lt with (fun n m => 0 <= n < m). + now intros [_ H]. Defined. -(* "le_0_l : forall n : N, 0 <= n" was proved in NBase.v *) +(** Note that [le_0_l : forall n, 0 <= n] is already proved in [NBase]. *) Theorem nlt_0_r : forall n, ~ n < 0. Proof. @@ -162,12 +162,7 @@ intros n H; apply succ_pred; intro H1; rewrite H1 in H. false_hyp H lt_irrefl. Qed. -Theorem le_pred_l : forall n, P n <= n. -Proof. -intro n; cases n. -- rewrite pred_0; now apply eq_le_incl. -- intros; rewrite pred_succ; apply le_succ_diag_r. -Qed. +(** The lemma [le_pred_l] is proved in NBase. *) Theorem lt_pred_l : forall n, n ~= 0 -> P n < n. Proof. diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index a0e3c3c9db..3bb665d67c 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -16,42 +16,16 @@ Module Type NSubProp (Import N : NAxiomsMiniSig'). Include NMulOrderProp N. Theorem sub_0_l : forall n, 0 - n == 0. -Proof. -intro n; induct n. -- apply sub_0_r. -- intros n IH; rewrite sub_succ_r; rewrite IH. now apply pred_0. -Qed. - -Theorem sub_succ : forall n m, S n - S m == n - m. -Proof. -intros n m; induct m. -- rewrite sub_succ_r. do 2 rewrite sub_0_r. now rewrite pred_succ. -- intros m IH. rewrite sub_succ_r. rewrite IH. now rewrite sub_succ_r. -Qed. - -Theorem sub_diag : forall n, n - n == 0. -Proof. - intro n; induct n. - - apply sub_0_r. - - intros n IH; rewrite sub_succ; now rewrite IH. -Qed. +Proof. exact (Private_nat_sub_0_l pred_0). Qed. Theorem sub_gt : forall n m, n > m -> n - m ~= 0. -Proof. -intros n m H; elim H using lt_ind_rel; clear n m H. -- solve_proper. -- intro; rewrite sub_0_r; apply neq_succ_0. -- intros; now rewrite sub_succ. -Qed. +Proof. intros n m H%lt_0_sub%lt_neq; apply neq_sym; exact H. Qed. Theorem add_sub_assoc : forall n m p, p <= m -> n + (m - p) == (n + m) - p. Proof. -intros n m p; induct p. -- intro; now do 2 rewrite sub_0_r. -- intros p IH H. do 2 rewrite sub_succ_r. - rewrite <- IH by (apply lt_le_incl; now apply le_succ_l). - rewrite add_pred_r by (apply sub_gt; now apply le_succ_l). - reflexivity. + intros n m p I; apply (add_cancel_r _ _ p); rewrite <-add_assoc. + rewrite 2!Private_sub_add; [reflexivity | | exact I]. + rewrite <-(add_0_l p); apply add_le_mono; [exact (le_0_l _) | exact I]. Qed. Theorem sub_succ_l : forall n m, n <= m -> S m - n == S (m - n). @@ -60,29 +34,8 @@ intros n m H. rewrite <- (add_1_l m). rewrite <- (add_1_l (m - n)). symmetry; now apply add_sub_assoc. Qed. -Theorem add_sub : forall n m, (n + m) - m == n. -Proof. -intros n m. rewrite <- add_sub_assoc by (apply le_refl). -rewrite sub_diag; now rewrite add_0_r. -Qed. - Theorem sub_add : forall n m, n <= m -> (m - n) + n == m. -Proof. -intros n m H. rewrite add_comm. rewrite add_sub_assoc by assumption. -rewrite add_comm. apply add_sub. -Qed. - -Theorem add_sub_eq_l : forall n m p, m + p == n -> n - m == p. -Proof. -intros n m p H. symmetry. -assert (H1 : m + p - m == n - m) by now rewrite H. -rewrite add_comm in H1. now rewrite add_sub in H1. -Qed. - -Theorem add_sub_eq_r : forall n m p, m + p == n -> n - p == m. -Proof. -intros n m p H; rewrite add_comm in H; now apply add_sub_eq_l. -Qed. +Proof. exact Private_sub_add. Qed. (* This could be proved by adding m to both sides. Then the proof would use add_sub_assoc and sub_0_le, which is proven below. *) @@ -96,13 +49,6 @@ intros n m p H; double_induct n m. rewrite add_succ_l; now rewrite H1. Qed. -Theorem sub_add_distr : forall n m p, n - (m + p) == (n - m) - p. -Proof. -intros n m p; induct p. -- rewrite add_0_r; now rewrite sub_0_r. -- intros p IH. rewrite add_succ_r; do 2 rewrite sub_succ_r. now rewrite IH. -Qed. - Theorem add_sub_swap : forall n m p, p <= n -> n + m - p == n - p + m. Proof. intros n m p H. @@ -122,13 +68,7 @@ intros n m; induct m. Qed. Theorem sub_0_le : forall n m, n - m == 0 <-> n <= m. -Proof. -intros n m; double_induct n m. -- intro m; split; intro; [apply le_0_l | apply sub_0_l]. -- intro m; rewrite sub_0_r; split; intro H; - [false_hyp H neq_succ_0 | false_hyp H nle_succ_0]. -- intros n m H. rewrite <- succ_le_mono. now rewrite sub_succ. -Qed. +Proof. exact (Private_nat_sub_0_le pred_0). Qed. Theorem sub_pred_l : forall n m, P n - m == P (n - m). Proof. @@ -148,30 +88,7 @@ apply sub_gt, le_succ_l; exact H'. Qed. Theorem sub_add_le : forall n m, n <= n - m + m. -Proof. -intros n m. -destruct (le_ge_cases n m) as [LE|GE]. -- rewrite <- sub_0_le in LE. rewrite LE; nzsimpl. - now rewrite <- sub_0_le. -- rewrite sub_add by assumption. apply le_refl. -Qed. - -Theorem le_sub_le_add_r : forall n m p, - n - p <= m <-> n <= m + p. -Proof. -intros n m p. -split; intros LE. -- rewrite (add_le_mono_r _ _ p) in LE. - apply le_trans with (n-p+p); auto using sub_add_le. -- destruct (le_ge_cases n p) as [LE'|GE]. - + rewrite <- sub_0_le in LE'. rewrite LE'. apply le_0_l. - + rewrite (add_le_mono_r _ _ p). now rewrite sub_add. -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. +Proof. exact Private_sub_add_le. Qed. Theorem lt_sub_lt_add_r : forall n m p, n - p < m -> n < m + p. @@ -207,26 +124,6 @@ Proof. intros n m p. rewrite add_comm; apply le_add_le_sub_r. Qed. -Theorem lt_add_lt_sub_r : forall n m p, n + p < m <-> n < m - p. -Proof. -intros n m p. -destruct (le_ge_cases p m) as [LE|GE]. -- rewrite <- (sub_add p m) at 1 by assumption. - now rewrite <- add_lt_mono_r. -- assert (GE' := GE). rewrite <- sub_0_le in GE'; rewrite GE'. - split; intros LT. - + elim (lt_irrefl m). apply le_lt_trans with (n+p); trivial. - rewrite <- (add_0_l m). apply add_le_mono. - * apply le_0_l. - * assumption. - + now elim (nlt_0_r n). -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 sub_lt : forall n m, m <= n -> 0 < m -> n - m < n. Proof. intros n m LE LT. @@ -267,38 +164,7 @@ Proof. exact (le_succ_diag_r _). Qed. -(** Sub and mul *) - -Theorem mul_pred_r : forall n m, n * (P m) == n * m - n. -Proof. -intros n m; cases m. -- now rewrite pred_0, mul_0_r, sub_0_l. -- intro m; rewrite pred_succ, mul_succ_r, <- add_sub_assoc. - + now rewrite sub_diag, add_0_r. - + now apply eq_le_incl. -Qed. - -Theorem mul_sub_distr_r : forall n m p, (n - m) * p == n * p - m * p. -Proof. -intros n m p; induct n. -- now rewrite sub_0_l, mul_0_l, sub_0_l. -- intros n IH. destruct (le_gt_cases m n) as [H | H]. - + rewrite sub_succ_l by assumption. do 2 rewrite mul_succ_l. - rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p). - rewrite <- (add_sub_assoc p (n * p) (m * p)) by now apply mul_le_mono_r. - now apply add_cancel_l. - + assert (H1 : S n <= m) by now apply le_succ_l. - setoid_replace (S n - m) with 0 by now apply sub_0_le. - setoid_replace ((S n * p) - m * p) with 0 by (apply sub_0_le; now apply mul_le_mono_r). - apply mul_0_l. -Qed. - -Theorem mul_sub_distr_l : forall n m p, p * (n - m) == p * n - p * m. -Proof. -intros n m p; rewrite (mul_comm p (n - m)), (mul_comm p n), (mul_comm p m). -apply mul_sub_distr_r. -Qed. - +(* TODO: deprecate this part in 8.20 and remove it in 8.22 *) (** Alternative definitions of [<=] and [<] based on [+] *) Definition le_alt n m := exists p, p + n == m. @@ -363,3 +229,4 @@ Theorem add_dichotomy : Proof. exact le_alt_dichotomy. Qed. End NSubProp. +