From ebb3fe944b6bd1cd363e3348465d7ea2fd85c62c Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 3 Jun 2008 00:04:16 +0000 Subject: In abstract parts of theories/Numbers, plus/times becomes add/mul, for increased consistency with bignums parts (commit part II: names of files + additional translation minus --> sub) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11040 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Natural/Abstract/NAdd.v | 156 ++++++++++++++++++++ theories/Numbers/Natural/Abstract/NAddOrder.v | 114 +++++++++++++++ theories/Numbers/Natural/Abstract/NAxioms.v | 4 +- theories/Numbers/Natural/Abstract/NBase.v | 8 +- theories/Numbers/Natural/Abstract/NMinus.v | 180 ------------------------ theories/Numbers/Natural/Abstract/NMul.v | 87 ++++++++++++ theories/Numbers/Natural/Abstract/NMulOrder.v | 131 +++++++++++++++++ theories/Numbers/Natural/Abstract/NOrder.v | 4 +- theories/Numbers/Natural/Abstract/NPlus.v | 156 -------------------- theories/Numbers/Natural/Abstract/NPlusOrder.v | 114 --------------- theories/Numbers/Natural/Abstract/NStrongRec.v | 4 +- theories/Numbers/Natural/Abstract/NSub.v | 180 ++++++++++++++++++++++++ theories/Numbers/Natural/Abstract/NTimes.v | 87 ------------ theories/Numbers/Natural/Abstract/NTimesOrder.v | 131 ----------------- theories/Numbers/Natural/BigN/BigN.v | 4 +- theories/Numbers/Natural/Binary/NBinDefs.v | 12 +- theories/Numbers/Natural/Peano/NPeano.v | 14 +- theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 8 +- 18 files changed, 697 insertions(+), 697 deletions(-) create mode 100644 theories/Numbers/Natural/Abstract/NAdd.v create mode 100644 theories/Numbers/Natural/Abstract/NAddOrder.v delete mode 100644 theories/Numbers/Natural/Abstract/NMinus.v create mode 100644 theories/Numbers/Natural/Abstract/NMul.v create mode 100644 theories/Numbers/Natural/Abstract/NMulOrder.v delete mode 100644 theories/Numbers/Natural/Abstract/NPlus.v delete mode 100644 theories/Numbers/Natural/Abstract/NPlusOrder.v create mode 100644 theories/Numbers/Natural/Abstract/NSub.v delete mode 100644 theories/Numbers/Natural/Abstract/NTimes.v delete mode 100644 theories/Numbers/Natural/Abstract/NTimesOrder.v (limited to 'theories/Numbers/Natural') diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v new file mode 100644 index 0000000000..37244159ff --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -0,0 +1,156 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* forall m1 m2 : N, m1 == m2 -> n1 + m1 == n2 + m2. +Proof NZadd_wd. + +Theorem add_0_l : forall n : N, 0 + n == n. +Proof NZadd_0_l. + +Theorem add_succ_l : forall n m : N, (S n) + m == S (n + m). +Proof NZadd_succ_l. + +(** Theorems that are valid for both natural numbers and integers *) + +Theorem add_0_r : forall n : N, n + 0 == n. +Proof NZadd_0_r. + +Theorem add_succ_r : forall n m : N, n + S m == S (n + m). +Proof NZadd_succ_r. + +Theorem add_comm : forall n m : N, n + m == m + n. +Proof NZadd_comm. + +Theorem add_assoc : forall n m p : N, n + (m + p) == (n + m) + p. +Proof NZadd_assoc. + +Theorem add_shuffle1 : forall n m p q : N, (n + m) + (p + q) == (n + p) + (m + q). +Proof NZadd_shuffle1. + +Theorem add_shuffle2 : forall n m p q : N, (n + m) + (p + q) == (n + q) + (m + p). +Proof NZadd_shuffle2. + +Theorem add_1_l : forall n : N, 1 + n == S n. +Proof NZadd_1_l. + +Theorem add_1_r : forall n : N, n + 1 == S n. +Proof NZadd_1_r. + +Theorem add_cancel_l : forall n m p : N, p + n == p + m <-> n == m. +Proof NZadd_cancel_l. + +Theorem add_cancel_r : forall n m p : N, n + p == m + p <-> n == m. +Proof NZadd_cancel_r. + +(* Theorems that are valid for natural numbers but cannot be proved for Z *) + +Theorem eq_add_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0. +Proof. +intros n m; induct n. +(* The next command does not work with the axiom add_0_l from NAddSig *) +rewrite add_0_l. intuition reflexivity. +intros n IH. rewrite add_succ_l. +setoid_replace (S (n + m) == 0) with False using relation iff by + (apply -> neg_false; apply neq_succ_0). +setoid_replace (S n == 0) with False using relation iff by + (apply -> neg_false; apply neq_succ_0). tauto. +Qed. + +Theorem eq_add_succ : + forall n m : N, (exists p : N, n + m == S p) <-> + (exists n' : N, n == S n') \/ (exists m' : N, m == S m'). +Proof. +intros n m; cases n. +split; intro H. +destruct H as [p H]. rewrite add_0_l in H; right; now exists p. +destruct H as [[n' H] | [m' H]]. +symmetry in H; false_hyp H neq_succ_0. +exists m'; now rewrite add_0_l. +intro n; split; intro H. +left; now exists n. +exists (n + m); now rewrite add_succ_l. +Qed. + +Theorem eq_add_1 : forall n m : N, + n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1. +Proof. +intros n m H. +assert (H1 : exists p : N, n + m == S p) by now exists 0. +apply -> eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]]. +left. rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H. +apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split. +right. rewrite H1 in H; rewrite add_succ_r in H; apply succ_inj in H. +apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split. +Qed. + +Theorem succ_add_discr : forall n m : N, m ~= S (n + m). +Proof. +intro n; induct m. +apply neq_symm. apply neq_succ_0. +intros m IH H. apply succ_inj in H. rewrite add_succ_r in H. +unfold not in IH; now apply IH. +Qed. + +Theorem add_pred_l : forall n m : N, n ~= 0 -> P n + m == P (n + m). +Proof. +intros n m; cases n. +intro H; now elim H. +intros n IH; rewrite add_succ_l; now do 2 rewrite pred_succ. +Qed. + +Theorem add_pred_r : forall n m : N, m ~= 0 -> n + P m == P (n + m). +Proof. +intros n m H; rewrite (add_comm n (P m)); +rewrite (add_comm n m); now apply add_pred_l. +Qed. + +(* One could define n <= m as exists p : N, p + n == m. Then we have +dichotomy: + +forall n m : N, n <= m \/ m <= n, + +i.e., + +forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n) (1) + +We will need (1) in the proof of induction principle for integers +constructed as pairs of natural numbers. The formula (1) can be proved +using properties of order and truncated subtraction. Thus, p would be +m - n or n - m and (1) would hold by theorem sub_add from Sub.v +depending on whether n <= m or m <= n. However, in proving induction +for integers constructed from natural numbers we do not need to +require implementations of order and sub; it is enough to prove (1) +here. *) + +Theorem add_dichotomy : + forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n). +Proof. +intros n m; induct n. +left; exists m; apply add_0_r. +intros n IH. +destruct IH as [[p H] | [p H]]. +destruct (zero_or_succ p) as [H1 | [p' H1]]; rewrite H1 in H. +rewrite add_0_l in H. right; exists (S 0); rewrite H; rewrite add_succ_l; now rewrite add_0_l. +left; exists p'; rewrite add_succ_r; now rewrite add_succ_l in H. +right; exists (S p). rewrite add_succ_l; now rewrite H. +Qed. + +End NAddPropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v new file mode 100644 index 0000000000..59f1c93475 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NAddOrder.v @@ -0,0 +1,114 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* p + n < p + m. +Proof NZadd_lt_mono_l. + +Theorem add_lt_mono_r : forall n m p : N, n < m <-> n + p < m + p. +Proof NZadd_lt_mono_r. + +Theorem add_lt_mono : forall n m p q : N, n < m -> p < q -> n + p < m + q. +Proof NZadd_lt_mono. + +Theorem add_le_mono_l : forall n m p : N, n <= m <-> p + n <= p + m. +Proof NZadd_le_mono_l. + +Theorem add_le_mono_r : forall n m p : N, n <= m <-> n + p <= m + p. +Proof NZadd_le_mono_r. + +Theorem add_le_mono : forall n m p q : N, n <= m -> p <= q -> n + p <= m + q. +Proof NZadd_le_mono. + +Theorem add_lt_le_mono : forall n m p q : N, n < m -> p <= q -> n + p < m + q. +Proof NZadd_lt_le_mono. + +Theorem add_le_lt_mono : forall n m p q : N, n <= m -> p < q -> n + p < m + q. +Proof NZadd_le_lt_mono. + +Theorem add_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n + m. +Proof NZadd_pos_pos. + +Theorem lt_add_pos_l : forall n m : N, 0 < n -> m < n + m. +Proof NZlt_add_pos_l. + +Theorem lt_add_pos_r : forall n m : N, 0 < n -> m < m + n. +Proof NZlt_add_pos_r. + +Theorem le_lt_add_lt : forall n m p q : N, n <= m -> p + m < q + n -> p < q. +Proof NZle_lt_add_lt. + +Theorem lt_le_add_lt : forall n m p q : N, n < m -> p + m <= q + n -> p < q. +Proof NZlt_le_add_lt. + +Theorem le_le_add_le : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q. +Proof NZle_le_add_le. + +Theorem add_lt_cases : forall n m p q : N, n + m < p + q -> n < p \/ m < q. +Proof NZadd_lt_cases. + +Theorem add_le_cases : forall n m p q : N, n + m <= p + q -> n <= p \/ m <= q. +Proof NZadd_le_cases. + +Theorem add_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m. +Proof NZadd_pos_cases. + +(* Theorems true for natural numbers *) + +Theorem le_add_r : forall n m : N, n <= n + m. +Proof. +intro n; induct m. +rewrite add_0_r; now apply eq_le_incl. +intros m IH. rewrite add_succ_r; now apply le_le_succ_r. +Qed. + +Theorem lt_lt_add_r : forall n m p : N, n < m -> n < m + p. +Proof. +intros n m p H; rewrite <- (add_0_r n). +apply add_lt_le_mono; [assumption | apply le_0_l]. +Qed. + +Theorem lt_lt_add_l : forall n m p : N, n < m -> n < p + m. +Proof. +intros n m p; rewrite add_comm; apply lt_lt_add_r. +Qed. + +Theorem add_pos_l : forall n m : N, 0 < n -> 0 < n + m. +Proof. +intros; apply NZadd_pos_nonneg. assumption. apply le_0_l. +Qed. + +Theorem add_pos_r : forall n m : N, 0 < m -> 0 < n + m. +Proof. +intros; apply NZadd_nonneg_pos. apply le_0_l. assumption. +Qed. + +(* The following property is used to prove the correctness of the +definition of order on integers constructed from pairs of natural numbers *) + +Theorem add_lt_repl_pair : forall n m n' m' u v : N, + n + u < m + v -> n + m' == n' + m -> n' + u < m' + v. +Proof. +intros n m n' m' u v H1 H2. +symmetry in H2. assert (H3 : n' + m <= n + m') by now apply eq_le_incl. +pose proof (add_lt_le_mono _ _ _ _ H1 H3) as H4. +rewrite (add_shuffle2 n u), (add_shuffle1 m v), (add_comm m n) in H4. +do 2 rewrite <- add_assoc in H4. do 2 apply <- add_lt_mono_l in H4. +now rewrite (add_comm n' u), (add_comm m' v). +Qed. + +End NAddOrderPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index c31f216a30..60f2aae7d5 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -26,7 +26,7 @@ Notation S := NZsucc. Notation P := NZpred. Notation add := NZadd. Notation mul := NZmul. -Notation minus := NZminus. +Notation sub := NZsub. Notation lt := NZlt. Notation le := NZle. Notation min := NZmin. @@ -36,7 +36,7 @@ Notation "x ~= y" := (~ Neq x y) (at level 70) : NatScope. Notation "0" := NZ0 : NatScope. Notation "1" := (NZsucc NZ0) : NatScope. Notation "x + y" := (NZadd x y) : NatScope. -Notation "x - y" := (NZminus x y) : NatScope. +Notation "x - y" := (NZsub x y) : NatScope. Notation "x * y" := (NZmul x y) : NatScope. Notation "x < y" := (NZlt x y) : NatScope. Notation "x <= y" := (NZle x y) : NatScope. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index eb46e69de0..0d7bc63eb6 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -12,7 +12,7 @@ Require Export Decidable. Require Export NAxioms. -Require Import NZTimesOrder. (* The last property functor on NZ, which subsumes all others *) +Require Import NZMulOrder. (* The last property functor on NZ, which subsumes all others *) Module NBasePropFunct (Import NAxiomsMod : NAxiomsSig). @@ -22,16 +22,16 @@ Open Local Scope NatScope. ones, to get all properties of NZ at once. This way we will include them only one time. *) -Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod. +Module Export NZMulOrderMod := NZMulOrderPropFunct NZOrdAxiomsMod. (* Here we probably need to re-prove all axioms declared in NAxioms.v to make sure that the definitions like N, S and add are unfolded in them, since unfolding is done only inside a functor. In fact, we'll do it in the files that prove the corresponding properties. In those files, we will also rename properties proved in NZ files by removing NZ from their names. In -this way, one only has to consult, for example, NPlus.v to see all +this way, one only has to consult, for example, NAdd.v to see all available properties for add, i.e., one does not have to go to NAxioms.v -for axioms and NZPlus.v for theorems. *) +for axioms and NZAdd.v for theorems. *) Theorem succ_wd : forall n1 n2 : N, n1 == n2 -> S n1 == S n2. Proof NZsucc_wd. diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v deleted file mode 100644 index 81b41dc03b..0000000000 --- a/theories/Numbers/Natural/Abstract/NMinus.v +++ /dev/null @@ -1,180 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* forall m1 m2 : N, m1 == m2 -> n1 - m1 == n2 - m2. -Proof NZminus_wd. - -Theorem minus_0_r : forall n : N, n - 0 == n. -Proof NZminus_0_r. - -Theorem minus_succ_r : forall n m : N, n - (S m) == P (n - m). -Proof NZminus_succ_r. - -Theorem minus_1_r : forall n : N, n - 1 == P n. -Proof. -intro n; rewrite minus_succ_r; now rewrite minus_0_r. -Qed. - -Theorem minus_0_l : forall n : N, 0 - n == 0. -Proof. -induct n. -apply minus_0_r. -intros n IH; rewrite minus_succ_r; rewrite IH. now apply pred_0. -Qed. - -Theorem minus_succ : forall n m : N, S n - S m == n - m. -Proof. -intro n; induct m. -rewrite minus_succ_r. do 2 rewrite minus_0_r. now rewrite pred_succ. -intros m IH. rewrite minus_succ_r. rewrite IH. now rewrite minus_succ_r. -Qed. - -Theorem minus_diag : forall n : N, n - n == 0. -Proof. -induct n. apply minus_0_r. intros n IH; rewrite minus_succ; now rewrite IH. -Qed. - -Theorem minus_gt : forall n m : N, n > m -> n - m ~= 0. -Proof. -intros n m H; elim H using lt_ind_rel; clear n m H. -solve_relation_wd. -intro; rewrite minus_0_r; apply neq_succ_0. -intros; now rewrite minus_succ. -Qed. - -Theorem add_minus_assoc : forall n m p : N, p <= m -> n + (m - p) == (n + m) - p. -Proof. -intros n m p; induct p. -intro; now do 2 rewrite minus_0_r. -intros p IH H. do 2 rewrite minus_succ_r. -rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l). -rewrite add_pred_r by (apply minus_gt; now apply -> le_succ_l). -reflexivity. -Qed. - -Theorem minus_succ_l : forall n m : N, n <= m -> S m - n == S (m - n). -Proof. -intros n m H. rewrite <- (add_1_l m). rewrite <- (add_1_l (m - n)). -symmetry; now apply add_minus_assoc. -Qed. - -Theorem add_minus : forall n m : N, (n + m) - m == n. -Proof. -intros n m. rewrite <- add_minus_assoc by (apply le_refl). -rewrite minus_diag; now rewrite add_0_r. -Qed. - -Theorem minus_add : forall n m : N, n <= m -> (m - n) + n == m. -Proof. -intros n m H. rewrite add_comm. rewrite add_minus_assoc by assumption. -rewrite add_comm. apply add_minus. -Qed. - -Theorem add_minus_eq_l : forall n m p : N, 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_minus in H1. -Qed. - -Theorem add_minus_eq_r : forall n m p : N, m + p == n -> n - p == m. -Proof. -intros n m p H; rewrite add_comm in H; now apply add_minus_eq_l. -Qed. - -(* This could be proved by adding m to both sides. Then the proof would -use add_minus_assoc and minus_0_le, which is proven below. *) - -Theorem add_minus_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n. -Proof. -intros n m p H; double_induct n m. -intros m H1; rewrite minus_0_l in H1. symmetry in H1; false_hyp H1 H. -intro n; rewrite minus_0_r; now rewrite add_0_l. -intros n m IH H1. rewrite minus_succ in H1. apply IH in H1. -rewrite add_succ_l; now rewrite H1. -Qed. - -Theorem minus_add_distr : forall n m p : N, n - (m + p) == (n - m) - p. -Proof. -intros n m; induct p. -rewrite add_0_r; now rewrite minus_0_r. -intros p IH. rewrite add_succ_r; do 2 rewrite minus_succ_r. now rewrite IH. -Qed. - -Theorem add_minus_swap : forall n m p : N, p <= n -> n + m - p == n - p + m. -Proof. -intros n m p H. -rewrite (add_comm n m). -rewrite <- add_minus_assoc by assumption. -now rewrite (add_comm m (n - p)). -Qed. - -(** Minus and order *) - -Theorem le_minus_l : forall n m : N, n - m <= n. -Proof. -intro n; induct m. -rewrite minus_0_r; now apply eq_le_incl. -intros m IH. rewrite minus_succ_r. -apply le_trans with (n - m); [apply le_pred_l | assumption]. -Qed. - -Theorem minus_0_le : forall n m : N, n - m == 0 <-> n <= m. -Proof. -double_induct n m. -intro m; split; intro; [apply le_0_l | apply minus_0_l]. -intro m; rewrite minus_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 minus_succ. -Qed. - -(** Minus and mul *) - -Theorem mul_pred_r : forall n m : N, n * (P m) == n * m - n. -Proof. -intros n m; cases m. -now rewrite pred_0, mul_0_r, minus_0_l. -intro m; rewrite pred_succ, mul_succ_r, <- add_minus_assoc. -now rewrite minus_diag, add_0_r. -now apply eq_le_incl. -Qed. - -Theorem mul_minus_distr_r : forall n m p : N, (n - m) * p == n * p - m * p. -Proof. -intros n m p; induct n. -now rewrite minus_0_l, mul_0_l, minus_0_l. -intros n IH. destruct (le_gt_cases m n) as [H | H]. -rewrite minus_succ_l by assumption. do 2 rewrite mul_succ_l. -rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p). -rewrite <- (add_minus_assoc p (n * p) (m * p)) by now apply mul_le_mono_r. -now apply <- add_cancel_l. -assert (H1 : S n <= m); [now apply <- le_succ_l |]. -setoid_replace (S n - m) with 0 by now apply <- minus_0_le. -setoid_replace ((S n * p) - m * p) with 0 by (apply <- minus_0_le; now apply mul_le_mono_r). -apply mul_0_l. -Qed. - -Theorem mul_minus_distr_l : forall n m p : N, 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_minus_distr_r. -Qed. - -End NMinusPropFunct. - diff --git a/theories/Numbers/Natural/Abstract/NMul.v b/theories/Numbers/Natural/Abstract/NMul.v new file mode 100644 index 0000000000..69b284fdcf --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NMul.v @@ -0,0 +1,87 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* forall m1 m2 : N, m1 == m2 -> n1 * m1 == n2 * m2. +Proof NZmul_wd. + +Theorem mul_0_l : forall n : N, 0 * n == 0. +Proof NZmul_0_l. + +Theorem mul_succ_l : forall n m : N, (S n) * m == n * m + m. +Proof NZmul_succ_l. + +(** Theorems that are valid for both natural numbers and integers *) + +Theorem mul_0_r : forall n, n * 0 == 0. +Proof NZmul_0_r. + +Theorem mul_succ_r : forall n m, n * (S m) == n * m + n. +Proof NZmul_succ_r. + +Theorem mul_comm : forall n m : N, n * m == m * n. +Proof NZmul_comm. + +Theorem mul_add_distr_r : forall n m p : N, (n + m) * p == n * p + m * p. +Proof NZmul_add_distr_r. + +Theorem mul_add_distr_l : forall n m p : N, n * (m + p) == n * m + n * p. +Proof NZmul_add_distr_l. + +Theorem mul_assoc : forall n m p : N, n * (m * p) == (n * m) * p. +Proof NZmul_assoc. + +Theorem mul_1_l : forall n : N, 1 * n == n. +Proof NZmul_1_l. + +Theorem mul_1_r : forall n : N, n * 1 == n. +Proof NZmul_1_r. + +(* Theorems that cannot be proved in NZMul *) + +(* In proving the correctness of the definition of multiplication on +integers constructed from pairs of natural numbers, we'll need the +following fact about natural numbers: + +a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u = a * m' + v + +Here n + m' == n' + m expresses equality of integers (n, m) and (n', m'), +since a pair (a, b) of natural numbers represents the integer a - b. On +integers, the formula above could be proved by moving a * m to the left, +factoring out a and replacing n - m by n' - m'. However, the formula is +required in the process of constructing integers, so it has to be proved +for natural numbers, where terms cannot be moved from one side of an +equation to the other. The proof uses the cancellation laws add_cancel_l +and add_cancel_r. *) + +Theorem add_mul_repl_pair : forall a n m n' m' u v : N, + a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u == a * m' + v. +Proof. +intros a n m n' m' u v H1 H2. +apply (@NZmul_wd a a) in H2; [| reflexivity]. +do 2 rewrite mul_add_distr_l in H2. symmetry in H2. +pose proof (NZadd_wd _ _ H1 _ _ H2) as H3. +rewrite (add_shuffle1 (a * m)), (add_comm (a * m) (a * n)) in H3. +do 2 rewrite <- add_assoc in H3. apply -> add_cancel_l in H3. +rewrite (add_assoc u), (add_comm (a * m)) in H3. +apply -> add_cancel_r in H3. +now rewrite (add_comm (a * n') u), (add_comm (a * m') v). +Qed. + +End NMulPropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v new file mode 100644 index 0000000000..ac4cc5e9ed --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NMulOrder.v @@ -0,0 +1,131 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (p * n < p * m <-> q * n + m < q * m + n). +Proof NZmul_lt_pred. + +Theorem mul_lt_mono_pos_l : forall p n m : N, 0 < p -> (n < m <-> p * n < p * m). +Proof NZmul_lt_mono_pos_l. + +Theorem mul_lt_mono_pos_r : forall p n m : N, 0 < p -> (n < m <-> n * p < m * p). +Proof NZmul_lt_mono_pos_r. + +Theorem mul_cancel_l : forall n m p : N, p ~= 0 -> (p * n == p * m <-> n == m). +Proof NZmul_cancel_l. + +Theorem mul_cancel_r : forall n m p : N, p ~= 0 -> (n * p == m * p <-> n == m). +Proof NZmul_cancel_r. + +Theorem mul_id_l : forall n m : N, m ~= 0 -> (n * m == m <-> n == 1). +Proof NZmul_id_l. + +Theorem mul_id_r : forall n m : N, n ~= 0 -> (n * m == n <-> m == 1). +Proof NZmul_id_r. + +Theorem mul_le_mono_pos_l : forall n m p : N, 0 < p -> (n <= m <-> p * n <= p * m). +Proof NZmul_le_mono_pos_l. + +Theorem mul_le_mono_pos_r : forall n m p : N, 0 < p -> (n <= m <-> n * p <= m * p). +Proof NZmul_le_mono_pos_r. + +Theorem mul_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m. +Proof NZmul_pos_pos. + +Theorem lt_1_mul_pos : forall n m : N, 1 < n -> 0 < m -> 1 < n * m. +Proof NZlt_1_mul_pos. + +Theorem eq_mul_0 : forall n m : N, n * m == 0 <-> n == 0 \/ m == 0. +Proof NZeq_mul_0. + +Theorem neq_mul_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Proof NZneq_mul_0. + +Theorem eq_square_0 : forall n : N, n * n == 0 <-> n == 0. +Proof NZeq_square_0. + +Theorem eq_mul_0_l : forall n m : N, n * m == 0 -> m ~= 0 -> n == 0. +Proof NZeq_mul_0_l. + +Theorem eq_mul_0_r : forall n m : N, n * m == 0 -> n ~= 0 -> m == 0. +Proof NZeq_mul_0_r. + +Theorem square_lt_mono : forall n m : N, n < m <-> n * n < m * m. +Proof. +intros n m; split; intro; +[apply NZsquare_lt_mono_nonneg | apply NZsquare_lt_simpl_nonneg]; +try assumption; apply le_0_l. +Qed. + +Theorem square_le_mono : forall n m : N, n <= m <-> n * n <= m * m. +Proof. +intros n m; split; intro; +[apply NZsquare_le_mono_nonneg | apply NZsquare_le_simpl_nonneg]; +try assumption; apply le_0_l. +Qed. + +Theorem mul_2_mono_l : forall n m : N, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Proof NZmul_2_mono_l. + +(* Theorems that are either not valid on Z or have different proofs on N and Z *) + +Theorem mul_le_mono_l : forall n m p : N, n <= m -> p * n <= p * m. +Proof. +intros; apply NZmul_le_mono_nonneg_l. apply le_0_l. assumption. +Qed. + +Theorem mul_le_mono_r : forall n m p : N, n <= m -> n * p <= m * p. +Proof. +intros; apply NZmul_le_mono_nonneg_r. apply le_0_l. assumption. +Qed. + +Theorem mul_lt_mono : forall n m p q : N, n < m -> p < q -> n * p < m * q. +Proof. +intros; apply NZmul_lt_mono_nonneg; try assumption; apply le_0_l. +Qed. + +Theorem mul_le_mono : forall n m p q : N, n <= m -> p <= q -> n * p <= m * q. +Proof. +intros; apply NZmul_le_mono_nonneg; try assumption; apply le_0_l. +Qed. + +Theorem lt_0_mul : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0. +Proof. +intros n m; split; [intro H | intros [H1 H2]]. +apply -> NZlt_0_mul in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r. +now apply NZmul_pos_pos. +Qed. + +Notation mul_pos := lt_0_mul (only parsing). + +Theorem eq_mul_1 : forall n m : N, n * m == 1 <-> n == 1 /\ m == 1. +Proof. +intros n m. +split; [| intros [H1 H2]; now rewrite H1, H2, mul_1_l]. +intro H; destruct (NZlt_trichotomy n 1) as [H1 | [H1 | H1]]. +apply -> lt_1_r in H1. rewrite H1, mul_0_l in H. false_hyp H neq_0_succ. +rewrite H1, mul_1_l in H; now split. +destruct (eq_0_gt_0_cases m) as [H2 | H2]. +rewrite H2, mul_0_r in H; false_hyp H neq_0_succ. +apply -> (mul_lt_mono_pos_r m) in H1; [| assumption]. rewrite mul_1_l in H1. +assert (H3 : 1 < n * m) by now apply (lt_1_l 0 m). +rewrite H in H3; false_hyp H3 lt_irrefl. +Qed. + +End NMulOrderPropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index bc5753d167..bcd4b92d6c 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -10,10 +10,10 @@ (*i $Id$ i*) -Require Export NTimes. +Require Export NMul. Module NOrderPropFunct (Import NAxiomsMod : NAxiomsSig). -Module Export NTimesPropMod := NTimesPropFunct NAxiomsMod. +Module Export NMulPropMod := NMulPropFunct NAxiomsMod. Open Local Scope NatScope. (* The tactics le_less, le_equal and le_elim are inherited from NZOrder.v *) diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v deleted file mode 100644 index 67443acff2..0000000000 --- a/theories/Numbers/Natural/Abstract/NPlus.v +++ /dev/null @@ -1,156 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* forall m1 m2 : N, m1 == m2 -> n1 + m1 == n2 + m2. -Proof NZadd_wd. - -Theorem add_0_l : forall n : N, 0 + n == n. -Proof NZadd_0_l. - -Theorem add_succ_l : forall n m : N, (S n) + m == S (n + m). -Proof NZadd_succ_l. - -(** Theorems that are valid for both natural numbers and integers *) - -Theorem add_0_r : forall n : N, n + 0 == n. -Proof NZadd_0_r. - -Theorem add_succ_r : forall n m : N, n + S m == S (n + m). -Proof NZadd_succ_r. - -Theorem add_comm : forall n m : N, n + m == m + n. -Proof NZadd_comm. - -Theorem add_assoc : forall n m p : N, n + (m + p) == (n + m) + p. -Proof NZadd_assoc. - -Theorem add_shuffle1 : forall n m p q : N, (n + m) + (p + q) == (n + p) + (m + q). -Proof NZadd_shuffle1. - -Theorem add_shuffle2 : forall n m p q : N, (n + m) + (p + q) == (n + q) + (m + p). -Proof NZadd_shuffle2. - -Theorem add_1_l : forall n : N, 1 + n == S n. -Proof NZadd_1_l. - -Theorem add_1_r : forall n : N, n + 1 == S n. -Proof NZadd_1_r. - -Theorem add_cancel_l : forall n m p : N, p + n == p + m <-> n == m. -Proof NZadd_cancel_l. - -Theorem add_cancel_r : forall n m p : N, n + p == m + p <-> n == m. -Proof NZadd_cancel_r. - -(* Theorems that are valid for natural numbers but cannot be proved for Z *) - -Theorem eq_add_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0. -Proof. -intros n m; induct n. -(* The next command does not work with the axiom add_0_l from NPlusSig *) -rewrite add_0_l. intuition reflexivity. -intros n IH. rewrite add_succ_l. -setoid_replace (S (n + m) == 0) with False using relation iff by - (apply -> neg_false; apply neq_succ_0). -setoid_replace (S n == 0) with False using relation iff by - (apply -> neg_false; apply neq_succ_0). tauto. -Qed. - -Theorem eq_add_succ : - forall n m : N, (exists p : N, n + m == S p) <-> - (exists n' : N, n == S n') \/ (exists m' : N, m == S m'). -Proof. -intros n m; cases n. -split; intro H. -destruct H as [p H]. rewrite add_0_l in H; right; now exists p. -destruct H as [[n' H] | [m' H]]. -symmetry in H; false_hyp H neq_succ_0. -exists m'; now rewrite add_0_l. -intro n; split; intro H. -left; now exists n. -exists (n + m); now rewrite add_succ_l. -Qed. - -Theorem eq_add_1 : forall n m : N, - n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1. -Proof. -intros n m H. -assert (H1 : exists p : N, n + m == S p) by now exists 0. -apply -> eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]]. -left. rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H. -apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split. -right. rewrite H1 in H; rewrite add_succ_r in H; apply succ_inj in H. -apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split. -Qed. - -Theorem succ_add_discr : forall n m : N, m ~= S (n + m). -Proof. -intro n; induct m. -apply neq_symm. apply neq_succ_0. -intros m IH H. apply succ_inj in H. rewrite add_succ_r in H. -unfold not in IH; now apply IH. -Qed. - -Theorem add_pred_l : forall n m : N, n ~= 0 -> P n + m == P (n + m). -Proof. -intros n m; cases n. -intro H; now elim H. -intros n IH; rewrite add_succ_l; now do 2 rewrite pred_succ. -Qed. - -Theorem add_pred_r : forall n m : N, m ~= 0 -> n + P m == P (n + m). -Proof. -intros n m H; rewrite (add_comm n (P m)); -rewrite (add_comm n m); now apply add_pred_l. -Qed. - -(* One could define n <= m as exists p : N, p + n == m. Then we have -dichotomy: - -forall n m : N, n <= m \/ m <= n, - -i.e., - -forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n) (1) - -We will need (1) in the proof of induction principle for integers -constructed as pairs of natural numbers. The formula (1) can be proved -using properties of order and truncated subtraction. Thus, p would be -m - n or n - m and (1) would hold by theorem minus_add from Minus.v -depending on whether n <= m or m <= n. However, in proving induction -for integers constructed from natural numbers we do not need to -require implementations of order and minus; it is enough to prove (1) -here. *) - -Theorem add_dichotomy : - forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n). -Proof. -intros n m; induct n. -left; exists m; apply add_0_r. -intros n IH. -destruct IH as [[p H] | [p H]]. -destruct (zero_or_succ p) as [H1 | [p' H1]]; rewrite H1 in H. -rewrite add_0_l in H. right; exists (S 0); rewrite H; rewrite add_succ_l; now rewrite add_0_l. -left; exists p'; rewrite add_succ_r; now rewrite add_succ_l in H. -right; exists (S p). rewrite add_succ_l; now rewrite H. -Qed. - -End NPlusPropFunct. - diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NPlusOrder.v deleted file mode 100644 index 07eeffdfd8..0000000000 --- a/theories/Numbers/Natural/Abstract/NPlusOrder.v +++ /dev/null @@ -1,114 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* p + n < p + m. -Proof NZadd_lt_mono_l. - -Theorem add_lt_mono_r : forall n m p : N, n < m <-> n + p < m + p. -Proof NZadd_lt_mono_r. - -Theorem add_lt_mono : forall n m p q : N, n < m -> p < q -> n + p < m + q. -Proof NZadd_lt_mono. - -Theorem add_le_mono_l : forall n m p : N, n <= m <-> p + n <= p + m. -Proof NZadd_le_mono_l. - -Theorem add_le_mono_r : forall n m p : N, n <= m <-> n + p <= m + p. -Proof NZadd_le_mono_r. - -Theorem add_le_mono : forall n m p q : N, n <= m -> p <= q -> n + p <= m + q. -Proof NZadd_le_mono. - -Theorem add_lt_le_mono : forall n m p q : N, n < m -> p <= q -> n + p < m + q. -Proof NZadd_lt_le_mono. - -Theorem add_le_lt_mono : forall n m p q : N, n <= m -> p < q -> n + p < m + q. -Proof NZadd_le_lt_mono. - -Theorem add_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n + m. -Proof NZadd_pos_pos. - -Theorem lt_add_pos_l : forall n m : N, 0 < n -> m < n + m. -Proof NZlt_add_pos_l. - -Theorem lt_add_pos_r : forall n m : N, 0 < n -> m < m + n. -Proof NZlt_add_pos_r. - -Theorem le_lt_add_lt : forall n m p q : N, n <= m -> p + m < q + n -> p < q. -Proof NZle_lt_add_lt. - -Theorem lt_le_add_lt : forall n m p q : N, n < m -> p + m <= q + n -> p < q. -Proof NZlt_le_add_lt. - -Theorem le_le_add_le : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q. -Proof NZle_le_add_le. - -Theorem add_lt_cases : forall n m p q : N, n + m < p + q -> n < p \/ m < q. -Proof NZadd_lt_cases. - -Theorem add_le_cases : forall n m p q : N, n + m <= p + q -> n <= p \/ m <= q. -Proof NZadd_le_cases. - -Theorem add_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m. -Proof NZadd_pos_cases. - -(* Theorems true for natural numbers *) - -Theorem le_add_r : forall n m : N, n <= n + m. -Proof. -intro n; induct m. -rewrite add_0_r; now apply eq_le_incl. -intros m IH. rewrite add_succ_r; now apply le_le_succ_r. -Qed. - -Theorem lt_lt_add_r : forall n m p : N, n < m -> n < m + p. -Proof. -intros n m p H; rewrite <- (add_0_r n). -apply add_lt_le_mono; [assumption | apply le_0_l]. -Qed. - -Theorem lt_lt_add_l : forall n m p : N, n < m -> n < p + m. -Proof. -intros n m p; rewrite add_comm; apply lt_lt_add_r. -Qed. - -Theorem add_pos_l : forall n m : N, 0 < n -> 0 < n + m. -Proof. -intros; apply NZadd_pos_nonneg. assumption. apply le_0_l. -Qed. - -Theorem add_pos_r : forall n m : N, 0 < m -> 0 < n + m. -Proof. -intros; apply NZadd_nonneg_pos. apply le_0_l. assumption. -Qed. - -(* The following property is used to prove the correctness of the -definition of order on integers constructed from pairs of natural numbers *) - -Theorem add_lt_repl_pair : forall n m n' m' u v : N, - n + u < m + v -> n + m' == n' + m -> n' + u < m' + v. -Proof. -intros n m n' m' u v H1 H2. -symmetry in H2. assert (H3 : n' + m <= n + m') by now apply eq_le_incl. -pose proof (add_lt_le_mono _ _ _ _ H1 H3) as H4. -rewrite (add_shuffle2 n u), (add_shuffle1 m v), (add_comm m n) in H4. -do 2 rewrite <- add_assoc in H4. do 2 apply <- add_lt_mono_l in H4. -now rewrite (add_comm n' u), (add_comm m' v). -Qed. - -End NPlusOrderPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index 78b647d995..5303bf8e57 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -13,10 +13,10 @@ (** This file defined the strong (course-of-value, well-founded) recursion and proves its properties *) -Require Export NMinus. +Require Export NSub. Module NStrongRecPropFunct (Import NAxiomsMod : NAxiomsSig). -Module Export NMinusPropMod := NMinusPropFunct NAxiomsMod. +Module Export NSubPropMod := NSubPropFunct NAxiomsMod. Open Local Scope NatScope. Section StrongRecursion. diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v new file mode 100644 index 0000000000..cfeb6709b2 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -0,0 +1,180 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* forall m1 m2 : N, m1 == m2 -> n1 - m1 == n2 - m2. +Proof NZsub_wd. + +Theorem sub_0_r : forall n : N, n - 0 == n. +Proof NZsub_0_r. + +Theorem sub_succ_r : forall n m : N, n - (S m) == P (n - m). +Proof NZsub_succ_r. + +Theorem sub_1_r : forall n : N, n - 1 == P n. +Proof. +intro n; rewrite sub_succ_r; now rewrite sub_0_r. +Qed. + +Theorem sub_0_l : forall n : N, 0 - n == 0. +Proof. +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 : N, S n - S m == n - m. +Proof. +intro n; 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 - n == 0. +Proof. +induct n. apply sub_0_r. intros n IH; rewrite sub_succ; now rewrite IH. +Qed. + +Theorem sub_gt : forall n m : N, n > m -> n - m ~= 0. +Proof. +intros n m H; elim H using lt_ind_rel; clear n m H. +solve_relation_wd. +intro; rewrite sub_0_r; apply neq_succ_0. +intros; now rewrite sub_succ. +Qed. + +Theorem add_sub_assoc : forall n m p : N, 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. +Qed. + +Theorem sub_succ_l : forall n m : N, n <= m -> S m - n == S (m - n). +Proof. +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, (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, 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 : N, 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 : N, m + p == n -> n - p == m. +Proof. +intros n m p H; rewrite add_comm in H; now apply add_sub_eq_l. +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. *) + +Theorem add_sub_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n. +Proof. +intros n m p H; double_induct n m. +intros m H1; rewrite sub_0_l in H1. symmetry in H1; false_hyp H1 H. +intro n; rewrite sub_0_r; now rewrite add_0_l. +intros n m IH H1. rewrite sub_succ in H1. apply IH in H1. +rewrite add_succ_l; now rewrite H1. +Qed. + +Theorem sub_add_distr : forall n m p : N, n - (m + p) == (n - m) - p. +Proof. +intros n m; 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 : N, p <= n -> n + m - p == n - p + m. +Proof. +intros n m p H. +rewrite (add_comm n m). +rewrite <- add_sub_assoc by assumption. +now rewrite (add_comm m (n - p)). +Qed. + +(** Sub and order *) + +Theorem le_sub_l : forall n m : N, n - m <= n. +Proof. +intro n; induct m. +rewrite sub_0_r; now apply eq_le_incl. +intros m IH. rewrite sub_succ_r. +apply le_trans with (n - m); [apply le_pred_l | assumption]. +Qed. + +Theorem sub_0_le : forall n m : N, n - m == 0 <-> n <= m. +Proof. +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. + +(** Sub and mul *) + +Theorem mul_pred_r : forall n m : N, 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, (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); [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 : N, 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. + +End NSubPropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v deleted file mode 100644 index 3b1ffa79e8..0000000000 --- a/theories/Numbers/Natural/Abstract/NTimes.v +++ /dev/null @@ -1,87 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* forall m1 m2 : N, m1 == m2 -> n1 * m1 == n2 * m2. -Proof NZmul_wd. - -Theorem mul_0_l : forall n : N, 0 * n == 0. -Proof NZmul_0_l. - -Theorem mul_succ_l : forall n m : N, (S n) * m == n * m + m. -Proof NZmul_succ_l. - -(** Theorems that are valid for both natural numbers and integers *) - -Theorem mul_0_r : forall n, n * 0 == 0. -Proof NZmul_0_r. - -Theorem mul_succ_r : forall n m, n * (S m) == n * m + n. -Proof NZmul_succ_r. - -Theorem mul_comm : forall n m : N, n * m == m * n. -Proof NZmul_comm. - -Theorem mul_add_distr_r : forall n m p : N, (n + m) * p == n * p + m * p. -Proof NZmul_add_distr_r. - -Theorem mul_add_distr_l : forall n m p : N, n * (m + p) == n * m + n * p. -Proof NZmul_add_distr_l. - -Theorem mul_assoc : forall n m p : N, n * (m * p) == (n * m) * p. -Proof NZmul_assoc. - -Theorem mul_1_l : forall n : N, 1 * n == n. -Proof NZmul_1_l. - -Theorem mul_1_r : forall n : N, n * 1 == n. -Proof NZmul_1_r. - -(* Theorems that cannot be proved in NZTimes *) - -(* In proving the correctness of the definition of multiplication on -integers constructed from pairs of natural numbers, we'll need the -following fact about natural numbers: - -a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u = a * m' + v - -Here n + m' == n' + m expresses equality of integers (n, m) and (n', m'), -since a pair (a, b) of natural numbers represents the integer a - b. On -integers, the formula above could be proved by moving a * m to the left, -factoring out a and replacing n - m by n' - m'. However, the formula is -required in the process of constructing integers, so it has to be proved -for natural numbers, where terms cannot be moved from one side of an -equation to the other. The proof uses the cancellation laws add_cancel_l -and add_cancel_r. *) - -Theorem add_mul_repl_pair : forall a n m n' m' u v : N, - a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u == a * m' + v. -Proof. -intros a n m n' m' u v H1 H2. -apply (@NZmul_wd a a) in H2; [| reflexivity]. -do 2 rewrite mul_add_distr_l in H2. symmetry in H2. -pose proof (NZadd_wd _ _ H1 _ _ H2) as H3. -rewrite (add_shuffle1 (a * m)), (add_comm (a * m) (a * n)) in H3. -do 2 rewrite <- add_assoc in H3. apply -> add_cancel_l in H3. -rewrite (add_assoc u), (add_comm (a * m)) in H3. -apply -> add_cancel_r in H3. -now rewrite (add_comm (a * n') u), (add_comm (a * m') v). -Qed. - -End NTimesPropFunct. - diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v deleted file mode 100644 index 31f4177335..0000000000 --- a/theories/Numbers/Natural/Abstract/NTimesOrder.v +++ /dev/null @@ -1,131 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (p * n < p * m <-> q * n + m < q * m + n). -Proof NZmul_lt_pred. - -Theorem mul_lt_mono_pos_l : forall p n m : N, 0 < p -> (n < m <-> p * n < p * m). -Proof NZmul_lt_mono_pos_l. - -Theorem mul_lt_mono_pos_r : forall p n m : N, 0 < p -> (n < m <-> n * p < m * p). -Proof NZmul_lt_mono_pos_r. - -Theorem mul_cancel_l : forall n m p : N, p ~= 0 -> (p * n == p * m <-> n == m). -Proof NZmul_cancel_l. - -Theorem mul_cancel_r : forall n m p : N, p ~= 0 -> (n * p == m * p <-> n == m). -Proof NZmul_cancel_r. - -Theorem mul_id_l : forall n m : N, m ~= 0 -> (n * m == m <-> n == 1). -Proof NZmul_id_l. - -Theorem mul_id_r : forall n m : N, n ~= 0 -> (n * m == n <-> m == 1). -Proof NZmul_id_r. - -Theorem mul_le_mono_pos_l : forall n m p : N, 0 < p -> (n <= m <-> p * n <= p * m). -Proof NZmul_le_mono_pos_l. - -Theorem mul_le_mono_pos_r : forall n m p : N, 0 < p -> (n <= m <-> n * p <= m * p). -Proof NZmul_le_mono_pos_r. - -Theorem mul_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m. -Proof NZmul_pos_pos. - -Theorem lt_1_mul_pos : forall n m : N, 1 < n -> 0 < m -> 1 < n * m. -Proof NZlt_1_mul_pos. - -Theorem eq_mul_0 : forall n m : N, n * m == 0 <-> n == 0 \/ m == 0. -Proof NZeq_mul_0. - -Theorem neq_mul_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. -Proof NZneq_mul_0. - -Theorem eq_square_0 : forall n : N, n * n == 0 <-> n == 0. -Proof NZeq_square_0. - -Theorem eq_mul_0_l : forall n m : N, n * m == 0 -> m ~= 0 -> n == 0. -Proof NZeq_mul_0_l. - -Theorem eq_mul_0_r : forall n m : N, n * m == 0 -> n ~= 0 -> m == 0. -Proof NZeq_mul_0_r. - -Theorem square_lt_mono : forall n m : N, n < m <-> n * n < m * m. -Proof. -intros n m; split; intro; -[apply NZsquare_lt_mono_nonneg | apply NZsquare_lt_simpl_nonneg]; -try assumption; apply le_0_l. -Qed. - -Theorem square_le_mono : forall n m : N, n <= m <-> n * n <= m * m. -Proof. -intros n m; split; intro; -[apply NZsquare_le_mono_nonneg | apply NZsquare_le_simpl_nonneg]; -try assumption; apply le_0_l. -Qed. - -Theorem mul_2_mono_l : forall n m : N, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. -Proof NZmul_2_mono_l. - -(* Theorems that are either not valid on Z or have different proofs on N and Z *) - -Theorem mul_le_mono_l : forall n m p : N, n <= m -> p * n <= p * m. -Proof. -intros; apply NZmul_le_mono_nonneg_l. apply le_0_l. assumption. -Qed. - -Theorem mul_le_mono_r : forall n m p : N, n <= m -> n * p <= m * p. -Proof. -intros; apply NZmul_le_mono_nonneg_r. apply le_0_l. assumption. -Qed. - -Theorem mul_lt_mono : forall n m p q : N, n < m -> p < q -> n * p < m * q. -Proof. -intros; apply NZmul_lt_mono_nonneg; try assumption; apply le_0_l. -Qed. - -Theorem mul_le_mono : forall n m p q : N, n <= m -> p <= q -> n * p <= m * q. -Proof. -intros; apply NZmul_le_mono_nonneg; try assumption; apply le_0_l. -Qed. - -Theorem lt_0_mul : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0. -Proof. -intros n m; split; [intro H | intros [H1 H2]]. -apply -> NZlt_0_mul in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r. -now apply NZmul_pos_pos. -Qed. - -Notation mul_pos := lt_0_mul (only parsing). - -Theorem eq_mul_1 : forall n m : N, n * m == 1 <-> n == 1 /\ m == 1. -Proof. -intros n m. -split; [| intros [H1 H2]; now rewrite H1, H2, mul_1_l]. -intro H; destruct (NZlt_trichotomy n 1) as [H1 | [H1 | H1]]. -apply -> lt_1_r in H1. rewrite H1, mul_0_l in H. false_hyp H neq_0_succ. -rewrite H1, mul_1_l in H; now split. -destruct (eq_0_gt_0_cases m) as [H2 | H2]. -rewrite H2, mul_0_r in H; false_hyp H neq_0_succ. -apply -> (mul_lt_mono_pos_r m) in H1; [| assumption]. rewrite mul_1_l in H1. -assert (H3 : 1 < n * m) by now apply (lt_1_l 0 m). -rewrite H in H3; false_hyp H3 lt_irrefl. -Qed. - -End NTimesOrderPropFunct. - diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 330a97ab52..485480fa04 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -20,14 +20,14 @@ Require Import Cyclic31. Require Import NSig. Require Import NSigNAxioms. Require Import NMake. -Require Import NMinus. +Require Import NSub. Module BigN <: NType := NMake.Make Int31Cyclic. (** Module [BigN] implements [NAxiomsSig] *) Module Export BigNAxiomsMod := NSig_NAxioms BigN. -Module Export BigNMinusPropMod := NMinusPropFunct BigNAxiomsMod. +Module Export BigNSubPropMod := NSubPropFunct BigNAxiomsMod. (** Notations about [BigN] *) diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v index 268879aa4d..e0f3fdf4bb 100644 --- a/theories/Numbers/Natural/Binary/NBinDefs.v +++ b/theories/Numbers/Natural/Binary/NBinDefs.v @@ -12,7 +12,7 @@ Require Import BinPos. Require Export BinNat. -Require Import NMinus. +Require Import NSub. Open Local Scope N_scope. @@ -28,7 +28,7 @@ Definition NZ0 := N0. Definition NZsucc := Nsucc. Definition NZpred := Npred. Definition NZadd := Nplus. -Definition NZminus := Nminus. +Definition NZsub := Nminus. Definition NZmul := Nmult. Theorem NZeq_equiv : equiv N NZeq. @@ -55,7 +55,7 @@ Proof. congruence. Qed. -Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. Proof. congruence. Qed. @@ -93,12 +93,12 @@ simpl in |- *; reflexivity. simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity. Qed. -Theorem NZminus_0_r : forall n : NZ, n - N0 = n. +Theorem NZsub_0_r : forall n : NZ, n - N0 = n. Proof. now destruct n. Qed. -Theorem NZminus_succ_r : forall n m : NZ, n - (NZsucc m) = NZpred (n - m). +Theorem NZsub_succ_r : forall n m : NZ, n - (NZsucc m) = NZpred (n - m). Proof. destruct n as [| p]; destruct m as [| q]; try reflexivity. now destruct p. @@ -242,7 +242,7 @@ Qed. End NBinaryAxiomsMod. -Module Export NBinaryMinusPropMod := NMinusPropFunct NBinaryAxiomsMod. +Module Export NBinarySubPropMod := NSubPropFunct NBinaryAxiomsMod. (* Some fun comparing the efficiency of the generic log defined by strong (course-of-value) recursion and the log defined by recursion diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 0b35868884..8d9e17fb09 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -13,7 +13,7 @@ Require Import Arith. Require Import Min. Require Import Max. -Require Import NMinus. +Require Import NSub. Module NPeanoAxiomsMod <: NAxiomsSig. Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. @@ -25,7 +25,7 @@ Definition NZ0 := 0. Definition NZsucc := S. Definition NZpred := pred. Definition NZadd := plus. -Definition NZminus := minus. +Definition NZsub := minus. Definition NZmul := mult. Theorem NZeq_equiv : equiv nat NZeq. @@ -56,7 +56,7 @@ Proof. congruence. Qed. -Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. Proof. congruence. Qed. @@ -88,14 +88,14 @@ Proof. reflexivity. Qed. -Theorem NZminus_0_r : forall n : nat, n - 0 = n. +Theorem NZsub_0_r : forall n : nat, n - 0 = n. Proof. intro n; now destruct n. Qed. -Theorem NZminus_succ_r : forall n m : nat, n - (S m) = pred (n - m). +Theorem NZsub_succ_r : forall n m : nat, n - (S m) = pred (n - m). Proof. -intros n m; induction n m using nat_double_ind; simpl; auto. apply NZminus_0_r. +intros n m; induction n m using nat_double_ind; simpl; auto. apply NZsub_0_r. Qed. Theorem NZmul_0_l : forall n : nat, 0 * n = 0. @@ -216,5 +216,5 @@ End NPeanoAxiomsMod. (* Now we apply the largest property functor *) -Module Export NPeanoMinusPropMod := NMinusPropFunct NPeanoAxiomsMod. +Module Export NPeanoSubPropMod := NSubPropFunct NPeanoAxiomsMod. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 54d7aec524..4f558e80ad 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -36,7 +36,7 @@ Definition NZ0 := N.zero. Definition NZsucc := N.succ. Definition NZpred := N.pred. Definition NZadd := N.add. -Definition NZminus := N.sub. +Definition NZsub := N.sub. Definition NZmul := N.mul. Theorem NZeq_equiv : equiv N.t N.eq. @@ -69,7 +69,7 @@ Proof. unfold N.eq; intros; rewrite 2 N.spec_add; f_equal; auto. Qed. -Add Morphism NZminus with signature N.eq ==> N.eq ==> N.eq as NZminus_wd. +Add Morphism NZsub with signature N.eq ==> N.eq ==> N.eq as NZsub_wd. Proof. unfold N.eq; intros x x' Hx y y' Hy. destruct (Z_lt_le_dec [x] [y]). @@ -147,13 +147,13 @@ Proof. intros; red; rewrite N.spec_add, 2 N.spec_succ, N.spec_add; auto with zarith. Qed. -Theorem NZminus_0_r : forall n, n - 0 == n. +Theorem NZsub_0_r : forall n, n - 0 == n. Proof. intros; red; rewrite N.spec_sub; rewrite N.spec_0; auto with zarith. apply N.spec_pos. Qed. -Theorem NZminus_succ_r : forall n m, n - (N.succ m) == N.pred (n - m). +Theorem NZsub_succ_r : forall n m, n - (N.succ m) == N.pred (n - m). Proof. intros; red. destruct (Z_lt_le_dec [n] [N.succ m]) as [H|H]. -- cgit v1.2.3