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 --- Makefile.common | 12 +- theories/Numbers/Cyclic/Abstract/NZCyclic.v | 14 +- theories/Numbers/Integer/Abstract/ZAdd.v | 345 ++++++++++++++++++++++ theories/Numbers/Integer/Abstract/ZAddOrder.v | 373 ++++++++++++++++++++++++ theories/Numbers/Integer/Abstract/ZAxioms.v | 4 +- theories/Numbers/Integer/Abstract/ZBase.v | 4 +- theories/Numbers/Integer/Abstract/ZLt.v | 4 +- theories/Numbers/Integer/Abstract/ZMul.v | 115 ++++++++ theories/Numbers/Integer/Abstract/ZMulOrder.v | 343 ++++++++++++++++++++++ theories/Numbers/Integer/Abstract/ZPlus.v | 345 ---------------------- theories/Numbers/Integer/Abstract/ZPlusOrder.v | 373 ------------------------ theories/Numbers/Integer/Abstract/ZTimes.v | 115 -------- theories/Numbers/Integer/Abstract/ZTimesOrder.v | 343 ---------------------- theories/Numbers/Integer/BigZ/BigZ.v | 4 +- theories/Numbers/Integer/Binary/ZBinary.v | 14 +- theories/Numbers/Integer/NatPairs/ZNatPairs.v | 28 +- theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 8 +- theories/Numbers/NatInt/NZAdd.v | 91 ++++++ theories/Numbers/NatInt/NZAddOrder.v | 166 +++++++++++ theories/Numbers/NatInt/NZAxioms.v | 14 +- theories/Numbers/NatInt/NZMul.v | 80 +++++ theories/Numbers/NatInt/NZMulOrder.v | 310 ++++++++++++++++++++ theories/Numbers/NatInt/NZOrder.v | 4 +- theories/Numbers/NatInt/NZPlus.v | 91 ------ theories/Numbers/NatInt/NZPlusOrder.v | 166 ----------- theories/Numbers/NatInt/NZTimes.v | 80 ----- theories/Numbers/NatInt/NZTimesOrder.v | 310 -------------------- 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 +- 45 files changed, 2575 insertions(+), 2575 deletions(-) create mode 100644 theories/Numbers/Integer/Abstract/ZAdd.v create mode 100644 theories/Numbers/Integer/Abstract/ZAddOrder.v create mode 100644 theories/Numbers/Integer/Abstract/ZMul.v create mode 100644 theories/Numbers/Integer/Abstract/ZMulOrder.v delete mode 100644 theories/Numbers/Integer/Abstract/ZPlus.v delete mode 100644 theories/Numbers/Integer/Abstract/ZPlusOrder.v delete mode 100644 theories/Numbers/Integer/Abstract/ZTimes.v delete mode 100644 theories/Numbers/Integer/Abstract/ZTimesOrder.v create mode 100644 theories/Numbers/NatInt/NZAdd.v create mode 100644 theories/Numbers/NatInt/NZAddOrder.v create mode 100644 theories/Numbers/NatInt/NZMul.v create mode 100644 theories/Numbers/NatInt/NZMulOrder.v delete mode 100644 theories/Numbers/NatInt/NZPlus.v delete mode 100644 theories/Numbers/NatInt/NZPlusOrder.v delete mode 100644 theories/Numbers/NatInt/NZTimes.v delete mode 100644 theories/Numbers/NatInt/NZTimesOrder.v 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 diff --git a/Makefile.common b/Makefile.common index cba65055a1..b90cdbc0f0 100644 --- a/Makefile.common +++ b/Makefile.common @@ -671,12 +671,12 @@ CYCLICVO:=$(CYCLICABSTRACTVO) $(CYCLICINT31VO) $(CYCLICDOUBLECYCLICVO) \ $(CYCLICZMODULOVO) NATINTVO:=$(addprefix theories/Numbers/NatInt/, \ - NZAxioms.vo NZBase.vo NZPlus.vo NZTimes.vo \ - NZOrder.vo NZPlusOrder.vo NZTimesOrder.vo ) + NZAxioms.vo NZBase.vo NZAdd.vo NZMul.vo \ + NZOrder.vo NZAddOrder.vo NZMulOrder.vo ) NATURALABSTRACTVO:=$(addprefix theories/Numbers/Natural/Abstract/, \ - NAxioms.vo NBase.vo NPlus.vo NTimes.vo \ - NOrder.vo NPlusOrder.vo NTimesOrder.vo NMinus.vo \ + NAxioms.vo NBase.vo NAdd.vo NMul.vo \ + NOrder.vo NAddOrder.vo NMulOrder.vo NSub.vo \ NIso.vo ) NATURALPEANOVO:=$(addprefix theories/Numbers/Natural/Peano/, \ @@ -695,8 +695,8 @@ NATURALVO:=$(NATURALABSTRACTVO) $(NATURALPEANOVO) $(NATURALBINARYVO) \ $(NATURALSPECVIAZVO) $(NATURALBIGNVO) INTEGERABSTRACTVO:=$(addprefix theories/Numbers/Integer/Abstract/, \ - ZAxioms.vo ZBase.vo ZPlus.vo ZTimes.vo \ - ZLt.vo ZPlusOrder.vo ZTimesOrder.vo ) + ZAxioms.vo ZBase.vo ZAdd.vo ZMul.vo \ + ZLt.vo ZAddOrder.vo ZMulOrder.vo ) INTEGERBINARYVO:=$(addprefix theories/Numbers/Integer/Binary/, \ ZBinary.vo ) diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 113945e0de..92ada3d748 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -40,7 +40,7 @@ Definition NZ0 := w_op.(znz_0). Definition NZsucc := w_op.(znz_succ). Definition NZpred := w_op.(znz_pred). Definition NZadd := w_op.(znz_add). -Definition NZminus := w_op.(znz_sub). +Definition NZsub := w_op.(znz_sub). Definition NZmul := w_op.(znz_mul). Theorem NZeq_equiv : equiv NZ NZeq. @@ -71,7 +71,7 @@ unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add). now rewrite H1, H2. Qed. -Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. Proof. unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub). now rewrite H1, H2. @@ -93,7 +93,7 @@ Notation "'S'" := NZsucc : IntScope. Notation "'P'" := NZpred : IntScope. (*Notation "1" := (S 0) : IntScope.*) Notation "x + y" := (NZadd x y) : IntScope. -Notation "x - y" := (NZminus x y) : IntScope. +Notation "x - y" := (NZsub x y) : IntScope. Notation "x * y" := (NZmul x y) : IntScope. Theorem gt_wB_1 : 1 < wB. @@ -204,15 +204,15 @@ rewrite <- (Zplus_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l. rewrite (Zplus_comm 1 [| m |]); now rewrite Zplus_assoc. Qed. -Theorem NZminus_0_r : forall n : NZ, n - 0 == n. +Theorem NZsub_0_r : forall n : NZ, n - 0 == n. Proof. -intro n; unfold NZminus, NZ0, NZeq. rewrite w_spec.(spec_sub). +intro n; unfold NZsub, NZ0, NZeq. rewrite w_spec.(spec_sub). rewrite w_spec.(spec_0). rewrite Zminus_0_r. apply NZ_to_Z_mod. Qed. -Theorem NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m). +Theorem NZsub_succ_r : forall n m : NZ, n - (S m) == P (n - m). Proof. -intros n m; unfold NZminus, NZsucc, NZpred, NZeq. +intros n m; unfold NZsub, NZsucc, NZpred, NZeq. rewrite w_spec.(spec_pred). do 2 rewrite w_spec.(spec_sub). rewrite w_spec.(spec_succ). rewrite Zminus_mod_idemp_r. rewrite Zminus_mod_idemp_l. diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v new file mode 100644 index 0000000000..daa7c530b9 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -0,0 +1,345 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* forall m1 m2 : Z, m1 == m2 -> n1 + m1 == n2 + m2. +Proof NZadd_wd. + +Theorem Zadd_0_l : forall n : Z, 0 + n == n. +Proof NZadd_0_l. + +Theorem Zadd_succ_l : forall n m : Z, (S n) + m == S (n + m). +Proof NZadd_succ_l. + +Theorem Zsub_0_r : forall n : Z, n - 0 == n. +Proof NZsub_0_r. + +Theorem Zsub_succ_r : forall n m : Z, n - (S m) == P (n - m). +Proof NZsub_succ_r. + +Theorem Zopp_0 : - 0 == 0. +Proof Zopp_0. + +Theorem Zopp_succ : forall n : Z, - (S n) == P (- n). +Proof Zopp_succ. + +(* Theorems that are valid for both natural numbers and integers *) + +Theorem Zadd_0_r : forall n : Z, n + 0 == n. +Proof NZadd_0_r. + +Theorem Zadd_succ_r : forall n m : Z, n + S m == S (n + m). +Proof NZadd_succ_r. + +Theorem Zadd_comm : forall n m : Z, n + m == m + n. +Proof NZadd_comm. + +Theorem Zadd_assoc : forall n m p : Z, n + (m + p) == (n + m) + p. +Proof NZadd_assoc. + +Theorem Zadd_shuffle1 : forall n m p q : Z, (n + m) + (p + q) == (n + p) + (m + q). +Proof NZadd_shuffle1. + +Theorem Zadd_shuffle2 : forall n m p q : Z, (n + m) + (p + q) == (n + q) + (m + p). +Proof NZadd_shuffle2. + +Theorem Zadd_1_l : forall n : Z, 1 + n == S n. +Proof NZadd_1_l. + +Theorem Zadd_1_r : forall n : Z, n + 1 == S n. +Proof NZadd_1_r. + +Theorem Zadd_cancel_l : forall n m p : Z, p + n == p + m <-> n == m. +Proof NZadd_cancel_l. + +Theorem Zadd_cancel_r : forall n m p : Z, n + p == m + p <-> n == m. +Proof NZadd_cancel_r. + +(* Theorems that are either not valid on N or have different proofs on N and Z *) + +Theorem Zadd_pred_l : forall n m : Z, P n + m == P (n + m). +Proof. +intros n m. +rewrite <- (Zsucc_pred n) at 2. +rewrite Zadd_succ_l. now rewrite Zpred_succ. +Qed. + +Theorem Zadd_pred_r : forall n m : Z, n + P m == P (n + m). +Proof. +intros n m; rewrite (Zadd_comm n (P m)), (Zadd_comm n m); +apply Zadd_pred_l. +Qed. + +Theorem Zadd_opp_r : forall n m : Z, n + (- m) == n - m. +Proof. +NZinduct m. +rewrite Zopp_0; rewrite Zsub_0_r; now rewrite Zadd_0_r. +intro m. rewrite Zopp_succ, Zsub_succ_r, Zadd_pred_r; now rewrite Zpred_inj_wd. +Qed. + +Theorem Zsub_0_l : forall n : Z, 0 - n == - n. +Proof. +intro n; rewrite <- Zadd_opp_r; now rewrite Zadd_0_l. +Qed. + +Theorem Zsub_succ_l : forall n m : Z, S n - m == S (n - m). +Proof. +intros n m; do 2 rewrite <- Zadd_opp_r; now rewrite Zadd_succ_l. +Qed. + +Theorem Zsub_pred_l : forall n m : Z, P n - m == P (n - m). +Proof. +intros n m. rewrite <- (Zsucc_pred n) at 2. +rewrite Zsub_succ_l; now rewrite Zpred_succ. +Qed. + +Theorem Zsub_pred_r : forall n m : Z, n - (P m) == S (n - m). +Proof. +intros n m. rewrite <- (Zsucc_pred m) at 2. +rewrite Zsub_succ_r; now rewrite Zsucc_pred. +Qed. + +Theorem Zopp_pred : forall n : Z, - (P n) == S (- n). +Proof. +intro n. rewrite <- (Zsucc_pred n) at 2. +rewrite Zopp_succ. now rewrite Zsucc_pred. +Qed. + +Theorem Zsub_diag : forall n : Z, n - n == 0. +Proof. +NZinduct n. +now rewrite Zsub_0_r. +intro n. rewrite Zsub_succ_r, Zsub_succ_l; now rewrite Zpred_succ. +Qed. + +Theorem Zadd_opp_diag_l : forall n : Z, - n + n == 0. +Proof. +intro n; now rewrite Zadd_comm, Zadd_opp_r, Zsub_diag. +Qed. + +Theorem Zadd_opp_diag_r : forall n : Z, n + (- n) == 0. +Proof. +intro n; rewrite Zadd_comm; apply Zadd_opp_diag_l. +Qed. + +Theorem Zadd_opp_l : forall n m : Z, - m + n == n - m. +Proof. +intros n m; rewrite <- Zadd_opp_r; now rewrite Zadd_comm. +Qed. + +Theorem Zadd_sub_assoc : forall n m p : Z, n + (m - p) == (n + m) - p. +Proof. +intros n m p; do 2 rewrite <- Zadd_opp_r; now rewrite Zadd_assoc. +Qed. + +Theorem Zopp_involutive : forall n : Z, - (- n) == n. +Proof. +NZinduct n. +now do 2 rewrite Zopp_0. +intro n. rewrite Zopp_succ, Zopp_pred; now rewrite Zsucc_inj_wd. +Qed. + +Theorem Zopp_add_distr : forall n m : Z, - (n + m) == - n + (- m). +Proof. +intros n m; NZinduct n. +rewrite Zopp_0; now do 2 rewrite Zadd_0_l. +intro n. rewrite Zadd_succ_l; do 2 rewrite Zopp_succ; rewrite Zadd_pred_l. +now rewrite Zpred_inj_wd. +Qed. + +Theorem Zopp_sub_distr : forall n m : Z, - (n - m) == - n + m. +Proof. +intros n m; rewrite <- Zadd_opp_r, Zopp_add_distr. +now rewrite Zopp_involutive. +Qed. + +Theorem Zopp_inj : forall n m : Z, - n == - m -> n == m. +Proof. +intros n m H. apply Zopp_wd in H. now do 2 rewrite Zopp_involutive in H. +Qed. + +Theorem Zopp_inj_wd : forall n m : Z, - n == - m <-> n == m. +Proof. +intros n m; split; [apply Zopp_inj | apply Zopp_wd]. +Qed. + +Theorem Zeq_opp_l : forall n m : Z, - n == m <-> n == - m. +Proof. +intros n m. now rewrite <- (Zopp_inj_wd (- n) m), Zopp_involutive. +Qed. + +Theorem Zeq_opp_r : forall n m : Z, n == - m <-> - n == m. +Proof. +symmetry; apply Zeq_opp_l. +Qed. + +Theorem Zsub_add_distr : forall n m p : Z, n - (m + p) == (n - m) - p. +Proof. +intros n m p; rewrite <- Zadd_opp_r, Zopp_add_distr, Zadd_assoc. +now do 2 rewrite Zadd_opp_r. +Qed. + +Theorem Zsub_sub_distr : forall n m p : Z, n - (m - p) == (n - m) + p. +Proof. +intros n m p; rewrite <- Zadd_opp_r, Zopp_sub_distr, Zadd_assoc. +now rewrite Zadd_opp_r. +Qed. + +Theorem sub_opp_l : forall n m : Z, - n - m == - m - n. +Proof. +intros n m. do 2 rewrite <- Zadd_opp_r. now rewrite Zadd_comm. +Qed. + +Theorem Zsub_opp_r : forall n m : Z, n - (- m) == n + m. +Proof. +intros n m; rewrite <- Zadd_opp_r; now rewrite Zopp_involutive. +Qed. + +Theorem Zadd_sub_swap : forall n m p : Z, n + m - p == n - p + m. +Proof. +intros n m p. rewrite <- Zadd_sub_assoc, <- (Zadd_opp_r n p), <- Zadd_assoc. +now rewrite Zadd_opp_l. +Qed. + +Theorem Zsub_cancel_l : forall n m p : Z, n - m == n - p <-> m == p. +Proof. +intros n m p. rewrite <- (Zadd_cancel_l (n - m) (n - p) (- n)). +do 2 rewrite Zadd_sub_assoc. rewrite Zadd_opp_diag_l; do 2 rewrite Zsub_0_l. +apply Zopp_inj_wd. +Qed. + +Theorem Zsub_cancel_r : forall n m p : Z, n - p == m - p <-> n == m. +Proof. +intros n m p. +stepl (n - p + p == m - p + p) by apply Zadd_cancel_r. +now do 2 rewrite <- Zsub_sub_distr, Zsub_diag, Zsub_0_r. +Qed. + +(* The next several theorems are devoted to moving terms from one side of +an equation to the other. The name contains the operation in the original +equation (add or sub) and the indication whether the left or right term +is moved. *) + +Theorem Zadd_move_l : forall n m p : Z, n + m == p <-> m == p - n. +Proof. +intros n m p. +stepl (n + m - n == p - n) by apply Zsub_cancel_r. +now rewrite Zadd_comm, <- Zadd_sub_assoc, Zsub_diag, Zadd_0_r. +Qed. + +Theorem Zadd_move_r : forall n m p : Z, n + m == p <-> n == p - m. +Proof. +intros n m p; rewrite Zadd_comm; now apply Zadd_move_l. +Qed. + +(* The two theorems above do not allow rewriting subformulas of the form +n - m == p to n == p + m since subtraction is in the right-hand side of +the equation. Hence the following two theorems. *) + +Theorem Zsub_move_l : forall n m p : Z, n - m == p <-> - m == p - n. +Proof. +intros n m p; rewrite <- (Zadd_opp_r n m); apply Zadd_move_l. +Qed. + +Theorem Zsub_move_r : forall n m p : Z, n - m == p <-> n == p + m. +Proof. +intros n m p; rewrite <- (Zadd_opp_r n m). now rewrite Zadd_move_r, Zsub_opp_r. +Qed. + +Theorem Zadd_move_0_l : forall n m : Z, n + m == 0 <-> m == - n. +Proof. +intros n m; now rewrite Zadd_move_l, Zsub_0_l. +Qed. + +Theorem Zadd_move_0_r : forall n m : Z, n + m == 0 <-> n == - m. +Proof. +intros n m; now rewrite Zadd_move_r, Zsub_0_l. +Qed. + +Theorem Zsub_move_0_l : forall n m : Z, n - m == 0 <-> - m == - n. +Proof. +intros n m. now rewrite Zsub_move_l, Zsub_0_l. +Qed. + +Theorem Zsub_move_0_r : forall n m : Z, n - m == 0 <-> n == m. +Proof. +intros n m. now rewrite Zsub_move_r, Zadd_0_l. +Qed. + +(* The following section is devoted to cancellation of like terms. The name +includes the first operator and the position of the term being canceled. *) + +Theorem Zadd_simpl_l : forall n m : Z, n + m - n == m. +Proof. +intros; now rewrite Zadd_sub_swap, Zsub_diag, Zadd_0_l. +Qed. + +Theorem Zadd_simpl_r : forall n m : Z, n + m - m == n. +Proof. +intros; now rewrite <- Zadd_sub_assoc, Zsub_diag, Zadd_0_r. +Qed. + +Theorem Zsub_simpl_l : forall n m : Z, - n - m + n == - m. +Proof. +intros; now rewrite <- Zadd_sub_swap, Zadd_opp_diag_l, Zsub_0_l. +Qed. + +Theorem Zsub_simpl_r : forall n m : Z, n - m + m == n. +Proof. +intros; now rewrite <- Zsub_sub_distr, Zsub_diag, Zsub_0_r. +Qed. + +(* Now we have two sums or differences; the name includes the two operators +and the position of the terms being canceled *) + +Theorem Zadd_add_simpl_l_l : forall n m p : Z, (n + m) - (n + p) == m - p. +Proof. +intros n m p. now rewrite (Zadd_comm n m), <- Zadd_sub_assoc, +Zsub_add_distr, Zsub_diag, Zsub_0_l, Zadd_opp_r. +Qed. + +Theorem Zadd_add_simpl_l_r : forall n m p : Z, (n + m) - (p + n) == m - p. +Proof. +intros n m p. rewrite (Zadd_comm p n); apply Zadd_add_simpl_l_l. +Qed. + +Theorem Zadd_add_simpl_r_l : forall n m p : Z, (n + m) - (m + p) == n - p. +Proof. +intros n m p. rewrite (Zadd_comm n m); apply Zadd_add_simpl_l_l. +Qed. + +Theorem Zadd_add_simpl_r_r : forall n m p : Z, (n + m) - (p + m) == n - p. +Proof. +intros n m p. rewrite (Zadd_comm p m); apply Zadd_add_simpl_r_l. +Qed. + +Theorem Zsub_add_simpl_r_l : forall n m p : Z, (n - m) + (m + p) == n + p. +Proof. +intros n m p. now rewrite <- Zsub_sub_distr, Zsub_add_distr, Zsub_diag, +Zsub_0_l, Zsub_opp_r. +Qed. + +Theorem Zsub_add_simpl_r_r : forall n m p : Z, (n - m) + (p + m) == n + p. +Proof. +intros n m p. rewrite (Zadd_comm p m); apply Zsub_add_simpl_r_l. +Qed. + +(* Of course, there are many other variants *) + +End ZAddPropFunct. + diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v new file mode 100644 index 0000000000..917e3fc123 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -0,0 +1,373 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* p + n < p + m. +Proof NZadd_lt_mono_l. + +Theorem Zadd_lt_mono_r : forall n m p : Z, n < m <-> n + p < m + p. +Proof NZadd_lt_mono_r. + +Theorem Zadd_lt_mono : forall n m p q : Z, n < m -> p < q -> n + p < m + q. +Proof NZadd_lt_mono. + +Theorem Zadd_le_mono_l : forall n m p : Z, n <= m <-> p + n <= p + m. +Proof NZadd_le_mono_l. + +Theorem Zadd_le_mono_r : forall n m p : Z, n <= m <-> n + p <= m + p. +Proof NZadd_le_mono_r. + +Theorem Zadd_le_mono : forall n m p q : Z, n <= m -> p <= q -> n + p <= m + q. +Proof NZadd_le_mono. + +Theorem Zadd_lt_le_mono : forall n m p q : Z, n < m -> p <= q -> n + p < m + q. +Proof NZadd_lt_le_mono. + +Theorem Zadd_le_lt_mono : forall n m p q : Z, n <= m -> p < q -> n + p < m + q. +Proof NZadd_le_lt_mono. + +Theorem Zadd_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n + m. +Proof NZadd_pos_pos. + +Theorem Zadd_pos_nonneg : forall n m : Z, 0 < n -> 0 <= m -> 0 < n + m. +Proof NZadd_pos_nonneg. + +Theorem Zadd_nonneg_pos : forall n m : Z, 0 <= n -> 0 < m -> 0 < n + m. +Proof NZadd_nonneg_pos. + +Theorem Zadd_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n + m. +Proof NZadd_nonneg_nonneg. + +Theorem Zlt_add_pos_l : forall n m : Z, 0 < n -> m < n + m. +Proof NZlt_add_pos_l. + +Theorem Zlt_add_pos_r : forall n m : Z, 0 < n -> m < m + n. +Proof NZlt_add_pos_r. + +Theorem Zle_lt_add_lt : forall n m p q : Z, n <= m -> p + m < q + n -> p < q. +Proof NZle_lt_add_lt. + +Theorem Zlt_le_add_lt : forall n m p q : Z, n < m -> p + m <= q + n -> p < q. +Proof NZlt_le_add_lt. + +Theorem Zle_le_add_le : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q. +Proof NZle_le_add_le. + +Theorem Zadd_lt_cases : forall n m p q : Z, n + m < p + q -> n < p \/ m < q. +Proof NZadd_lt_cases. + +Theorem Zadd_le_cases : forall n m p q : Z, n + m <= p + q -> n <= p \/ m <= q. +Proof NZadd_le_cases. + +Theorem Zadd_neg_cases : forall n m : Z, n + m < 0 -> n < 0 \/ m < 0. +Proof NZadd_neg_cases. + +Theorem Zadd_pos_cases : forall n m : Z, 0 < n + m -> 0 < n \/ 0 < m. +Proof NZadd_pos_cases. + +Theorem Zadd_nonpos_cases : forall n m : Z, n + m <= 0 -> n <= 0 \/ m <= 0. +Proof NZadd_nonpos_cases. + +Theorem Zadd_nonneg_cases : forall n m : Z, 0 <= n + m -> 0 <= n \/ 0 <= m. +Proof NZadd_nonneg_cases. + +(* Theorems that are either not valid on N or have different proofs on N and Z *) + +Theorem Zadd_neg_neg : forall n m : Z, n < 0 -> m < 0 -> n + m < 0. +Proof. +intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_lt_mono. +Qed. + +Theorem Zadd_neg_nonpos : forall n m : Z, n < 0 -> m <= 0 -> n + m < 0. +Proof. +intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_lt_le_mono. +Qed. + +Theorem Zadd_nonpos_neg : forall n m : Z, n <= 0 -> m < 0 -> n + m < 0. +Proof. +intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_le_lt_mono. +Qed. + +Theorem Zadd_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> n + m <= 0. +Proof. +intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_le_mono. +Qed. + +(** Sub and order *) + +Theorem Zlt_0_sub : forall n m : Z, 0 < m - n <-> n < m. +Proof. +intros n m. stepl (0 + n < m - n + n) by symmetry; apply Zadd_lt_mono_r. +rewrite Zadd_0_l; now rewrite Zsub_simpl_r. +Qed. + +Notation Zsub_pos := Zlt_0_sub (only parsing). + +Theorem Zle_0_sub : forall n m : Z, 0 <= m - n <-> n <= m. +Proof. +intros n m; stepl (0 + n <= m - n + n) by symmetry; apply Zadd_le_mono_r. +rewrite Zadd_0_l; now rewrite Zsub_simpl_r. +Qed. + +Notation Zsub_nonneg := Zle_0_sub (only parsing). + +Theorem Zlt_sub_0 : forall n m : Z, n - m < 0 <-> n < m. +Proof. +intros n m. stepl (n - m + m < 0 + m) by symmetry; apply Zadd_lt_mono_r. +rewrite Zadd_0_l; now rewrite Zsub_simpl_r. +Qed. + +Notation Zsub_neg := Zlt_sub_0 (only parsing). + +Theorem Zle_sub_0 : forall n m : Z, n - m <= 0 <-> n <= m. +Proof. +intros n m. stepl (n - m + m <= 0 + m) by symmetry; apply Zadd_le_mono_r. +rewrite Zadd_0_l; now rewrite Zsub_simpl_r. +Qed. + +Notation Zsub_nonpos := Zle_sub_0 (only parsing). + +Theorem Zopp_lt_mono : forall n m : Z, n < m <-> - m < - n. +Proof. +intros n m. stepr (m + - m < m + - n) by symmetry; apply Zadd_lt_mono_l. +do 2 rewrite Zadd_opp_r. rewrite Zsub_diag. symmetry; apply Zlt_0_sub. +Qed. + +Theorem Zopp_le_mono : forall n m : Z, n <= m <-> - m <= - n. +Proof. +intros n m. stepr (m + - m <= m + - n) by symmetry; apply Zadd_le_mono_l. +do 2 rewrite Zadd_opp_r. rewrite Zsub_diag. symmetry; apply Zle_0_sub. +Qed. + +Theorem Zopp_pos_neg : forall n : Z, 0 < - n <-> n < 0. +Proof. +intro n; rewrite (Zopp_lt_mono n 0); now rewrite Zopp_0. +Qed. + +Theorem Zopp_neg_pos : forall n : Z, - n < 0 <-> 0 < n. +Proof. +intro n. rewrite (Zopp_lt_mono 0 n). now rewrite Zopp_0. +Qed. + +Theorem Zopp_nonneg_nonpos : forall n : Z, 0 <= - n <-> n <= 0. +Proof. +intro n; rewrite (Zopp_le_mono n 0); now rewrite Zopp_0. +Qed. + +Theorem Zopp_nonpos_nonneg : forall n : Z, - n <= 0 <-> 0 <= n. +Proof. +intro n. rewrite (Zopp_le_mono 0 n). now rewrite Zopp_0. +Qed. + +Theorem Zsub_lt_mono_l : forall n m p : Z, n < m <-> p - m < p - n. +Proof. +intros n m p. do 2 rewrite <- Zadd_opp_r. rewrite <- Zadd_lt_mono_l. +apply Zopp_lt_mono. +Qed. + +Theorem Zsub_lt_mono_r : forall n m p : Z, n < m <-> n - p < m - p. +Proof. +intros n m p; do 2 rewrite <- Zadd_opp_r; apply Zadd_lt_mono_r. +Qed. + +Theorem Zsub_lt_mono : forall n m p q : Z, n < m -> q < p -> n - p < m - q. +Proof. +intros n m p q H1 H2. +apply NZlt_trans with (m - p); +[now apply -> Zsub_lt_mono_r | now apply -> Zsub_lt_mono_l]. +Qed. + +Theorem Zsub_le_mono_l : forall n m p : Z, n <= m <-> p - m <= p - n. +Proof. +intros n m p; do 2 rewrite <- Zadd_opp_r; rewrite <- Zadd_le_mono_l; +apply Zopp_le_mono. +Qed. + +Theorem Zsub_le_mono_r : forall n m p : Z, n <= m <-> n - p <= m - p. +Proof. +intros n m p; do 2 rewrite <- Zadd_opp_r; apply Zadd_le_mono_r. +Qed. + +Theorem Zsub_le_mono : forall n m p q : Z, n <= m -> q <= p -> n - p <= m - q. +Proof. +intros n m p q H1 H2. +apply NZle_trans with (m - p); +[now apply -> Zsub_le_mono_r | now apply -> Zsub_le_mono_l]. +Qed. + +Theorem Zsub_lt_le_mono : forall n m p q : Z, n < m -> q <= p -> n - p < m - q. +Proof. +intros n m p q H1 H2. +apply NZlt_le_trans with (m - p); +[now apply -> Zsub_lt_mono_r | now apply -> Zsub_le_mono_l]. +Qed. + +Theorem Zsub_le_lt_mono : forall n m p q : Z, n <= m -> q < p -> n - p < m - q. +Proof. +intros n m p q H1 H2. +apply NZle_lt_trans with (m - p); +[now apply -> Zsub_le_mono_r | now apply -> Zsub_lt_mono_l]. +Qed. + +Theorem Zle_lt_sub_lt : forall n m p q : Z, n <= m -> p - n < q - m -> p < q. +Proof. +intros n m p q H1 H2. apply (Zle_lt_add_lt (- m) (- n)); +[now apply -> Zopp_le_mono | now do 2 rewrite Zadd_opp_r]. +Qed. + +Theorem Zlt_le_sub_lt : forall n m p q : Z, n < m -> p - n <= q - m -> p < q. +Proof. +intros n m p q H1 H2. apply (Zlt_le_add_lt (- m) (- n)); +[now apply -> Zopp_lt_mono | now do 2 rewrite Zadd_opp_r]. +Qed. + +Theorem Zle_le_sub_lt : forall n m p q : Z, n <= m -> p - n <= q - m -> p <= q. +Proof. +intros n m p q H1 H2. apply (Zle_le_add_le (- m) (- n)); +[now apply -> Zopp_le_mono | now do 2 rewrite Zadd_opp_r]. +Qed. + +Theorem Zlt_add_lt_sub_r : forall n m p : Z, n + p < m <-> n < m - p. +Proof. +intros n m p. stepl (n + p - p < m - p) by symmetry; apply Zsub_lt_mono_r. +now rewrite Zadd_simpl_r. +Qed. + +Theorem Zle_add_le_sub_r : forall n m p : Z, n + p <= m <-> n <= m - p. +Proof. +intros n m p. stepl (n + p - p <= m - p) by symmetry; apply Zsub_le_mono_r. +now rewrite Zadd_simpl_r. +Qed. + +Theorem Zlt_add_lt_sub_l : forall n m p : Z, n + p < m <-> p < m - n. +Proof. +intros n m p. rewrite Zadd_comm; apply Zlt_add_lt_sub_r. +Qed. + +Theorem Zle_add_le_sub_l : forall n m p : Z, n + p <= m <-> p <= m - n. +Proof. +intros n m p. rewrite Zadd_comm; apply Zle_add_le_sub_r. +Qed. + +Theorem Zlt_sub_lt_add_r : forall n m p : Z, n - p < m <-> n < m + p. +Proof. +intros n m p. stepl (n - p + p < m + p) by symmetry; apply Zadd_lt_mono_r. +now rewrite Zsub_simpl_r. +Qed. + +Theorem Zle_sub_le_add_r : forall n m p : Z, n - p <= m <-> n <= m + p. +Proof. +intros n m p. stepl (n - p + p <= m + p) by symmetry; apply Zadd_le_mono_r. +now rewrite Zsub_simpl_r. +Qed. + +Theorem Zlt_sub_lt_add_l : forall n m p : Z, n - m < p <-> n < m + p. +Proof. +intros n m p. rewrite Zadd_comm; apply Zlt_sub_lt_add_r. +Qed. + +Theorem Zle_sub_le_add_l : forall n m p : Z, n - m <= p <-> n <= m + p. +Proof. +intros n m p. rewrite Zadd_comm; apply Zle_sub_le_add_r. +Qed. + +Theorem Zlt_sub_lt_add : forall n m p q : Z, n - m < p - q <-> n + q < m + p. +Proof. +intros n m p q. rewrite Zlt_sub_lt_add_l. rewrite Zadd_sub_assoc. +now rewrite <- Zlt_add_lt_sub_r. +Qed. + +Theorem Zle_sub_le_add : forall n m p q : Z, n - m <= p - q <-> n + q <= m + p. +Proof. +intros n m p q. rewrite Zle_sub_le_add_l. rewrite Zadd_sub_assoc. +now rewrite <- Zle_add_le_sub_r. +Qed. + +Theorem Zlt_sub_pos : forall n m : Z, 0 < m <-> n - m < n. +Proof. +intros n m. stepr (n - m < n - 0) by now rewrite Zsub_0_r. apply Zsub_lt_mono_l. +Qed. + +Theorem Zle_sub_nonneg : forall n m : Z, 0 <= m <-> n - m <= n. +Proof. +intros n m. stepr (n - m <= n - 0) by now rewrite Zsub_0_r. apply Zsub_le_mono_l. +Qed. + +Theorem Zsub_lt_cases : forall n m p q : Z, n - m < p - q -> n < m \/ q < p. +Proof. +intros n m p q H. rewrite Zlt_sub_lt_add in H. now apply Zadd_lt_cases. +Qed. + +Theorem Zsub_le_cases : forall n m p q : Z, n - m <= p - q -> n <= m \/ q <= p. +Proof. +intros n m p q H. rewrite Zle_sub_le_add in H. now apply Zadd_le_cases. +Qed. + +Theorem Zsub_neg_cases : forall n m : Z, n - m < 0 -> n < 0 \/ 0 < m. +Proof. +intros n m H; rewrite <- Zadd_opp_r in H. +setoid_replace (0 < m) with (- m < 0) using relation iff by (symmetry; apply Zopp_neg_pos). +now apply Zadd_neg_cases. +Qed. + +Theorem Zsub_pos_cases : forall n m : Z, 0 < n - m -> 0 < n \/ m < 0. +Proof. +intros n m H; rewrite <- Zadd_opp_r in H. +setoid_replace (m < 0) with (0 < - m) using relation iff by (symmetry; apply Zopp_pos_neg). +now apply Zadd_pos_cases. +Qed. + +Theorem Zsub_nonpos_cases : forall n m : Z, n - m <= 0 -> n <= 0 \/ 0 <= m. +Proof. +intros n m H; rewrite <- Zadd_opp_r in H. +setoid_replace (0 <= m) with (- m <= 0) using relation iff by (symmetry; apply Zopp_nonpos_nonneg). +now apply Zadd_nonpos_cases. +Qed. + +Theorem Zsub_nonneg_cases : forall n m : Z, 0 <= n - m -> 0 <= n \/ m <= 0. +Proof. +intros n m H; rewrite <- Zadd_opp_r in H. +setoid_replace (m <= 0) with (0 <= - m) using relation iff by (symmetry; apply Zopp_nonneg_nonpos). +now apply Zadd_nonneg_cases. +Qed. + +Section PosNeg. + +Variable P : Z -> Prop. +Hypothesis P_wd : predicate_wd Zeq P. + +Add Morphism P with signature Zeq ==> iff as P_morph. Proof. exact P_wd. Qed. + +Theorem Z0_pos_neg : + P 0 -> (forall n : Z, 0 < n -> P n /\ P (- n)) -> forall n : Z, P n. +Proof. +intros H1 H2 n. destruct (Zlt_trichotomy n 0) as [H3 | [H3 | H3]]. +apply <- Zopp_pos_neg in H3. apply H2 in H3. destruct H3 as [_ H3]. +now rewrite Zopp_involutive in H3. +now rewrite H3. +apply H2 in H3; now destruct H3. +Qed. + +End PosNeg. + +Ltac Z0_pos_neg n := induction_maker n ltac:(apply Z0_pos_neg). + +End ZAddOrderPropFunct. + + diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index 19fb40dfee..dfffe9a7fe 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -26,7 +26,7 @@ Notation S := NZsucc. Notation P := NZpred. Notation Zadd := NZadd. Notation Zmul := NZmul. -Notation Zminus := NZminus. +Notation Zsub := NZsub. Notation Zlt := NZlt. Notation Zle := NZle. Notation Zmin := NZmin. @@ -36,7 +36,7 @@ Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope. Notation "0" := NZ0 : IntScope. Notation "1" := (NZsucc NZ0) : IntScope. Notation "x + y" := (NZadd x y) : IntScope. -Notation "x - y" := (NZminus x y) : IntScope. +Notation "x - y" := (NZsub x y) : IntScope. Notation "x * y" := (NZmul x y) : IntScope. Notation "x < y" := (NZlt x y) : IntScope. Notation "x <= y" := (NZle x y) : IntScope. diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 0b8538873e..d175c358cd 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -12,7 +12,7 @@ Require Export Decidable. Require Export ZAxioms. -Require Import NZTimesOrder. +Require Import NZMulOrder. Module ZBasePropFunct (Import ZAxiomsMod : ZAxiomsSig). @@ -22,7 +22,7 @@ notations in Zadd and later *) Open Local Scope IntScope. -Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod. +Module Export NZMulOrderMod := NZMulOrderPropFunct NZOrdAxiomsMod. Theorem Zsucc_wd : forall n1 n2 : Z, n1 == n2 -> S n1 == S n2. Proof NZsucc_wd. diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index 8ceecdbf2e..1b8bdda408 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -10,10 +10,10 @@ (*i $Id$ i*) -Require Export ZTimes. +Require Export ZMul. Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig). -Module Export ZTimesPropMod := ZTimesPropFunct ZAxiomsMod. +Module Export ZMulPropMod := ZMulPropFunct ZAxiomsMod. Open Local Scope IntScope. (* Axioms *) diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v new file mode 100644 index 0000000000..785c0f41bd --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZMul.v @@ -0,0 +1,115 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* forall m1 m2 : Z, m1 == m2 -> n1 * m1 == n2 * m2. +Proof NZmul_wd. + +Theorem Zmul_0_l : forall n : Z, 0 * n == 0. +Proof NZmul_0_l. + +Theorem Zmul_succ_l : forall n m : Z, (S n) * m == n * m + m. +Proof NZmul_succ_l. + +(* Theorems that are valid for both natural numbers and integers *) + +Theorem Zmul_0_r : forall n : Z, n * 0 == 0. +Proof NZmul_0_r. + +Theorem Zmul_succ_r : forall n m : Z, n * (S m) == n * m + n. +Proof NZmul_succ_r. + +Theorem Zmul_comm : forall n m : Z, n * m == m * n. +Proof NZmul_comm. + +Theorem Zmul_add_distr_r : forall n m p : Z, (n + m) * p == n * p + m * p. +Proof NZmul_add_distr_r. + +Theorem Zmul_add_distr_l : forall n m p : Z, n * (m + p) == n * m + n * p. +Proof NZmul_add_distr_l. + +(* A note on naming: right (correspondingly, left) distributivity happens +when the sum is multiplied by a number on the right (left), not when the +sum itself is the right (left) factor in the product (see planetmath.org +and mathworld.wolfram.com). In the old library BinInt, distributivity over +subtraction was named correctly, but distributivity over addition was named +incorrectly. The names in Isabelle/HOL library are also incorrect. *) + +Theorem Zmul_assoc : forall n m p : Z, n * (m * p) == (n * m) * p. +Proof NZmul_assoc. + +Theorem Zmul_1_l : forall n : Z, 1 * n == n. +Proof NZmul_1_l. + +Theorem Zmul_1_r : forall n : Z, n * 1 == n. +Proof NZmul_1_r. + +(* The following two theorems are true in an ordered ring, +but since they don't mention order, we'll put them here *) + +Theorem Zeq_mul_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0. +Proof NZeq_mul_0. + +Theorem Zneq_mul_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Proof NZneq_mul_0. + +(* Theorems that are either not valid on N or have different proofs on N and Z *) + +Theorem Zmul_pred_r : forall n m : Z, n * (P m) == n * m - n. +Proof. +intros n m. +rewrite <- (Zsucc_pred m) at 2. +now rewrite Zmul_succ_r, <- Zadd_sub_assoc, Zsub_diag, Zadd_0_r. +Qed. + +Theorem Zmul_pred_l : forall n m : Z, (P n) * m == n * m - m. +Proof. +intros n m; rewrite (Zmul_comm (P n) m), (Zmul_comm n m). apply Zmul_pred_r. +Qed. + +Theorem Zmul_opp_l : forall n m : Z, (- n) * m == - (n * m). +Proof. +intros n m. apply -> Zadd_move_0_r. +now rewrite <- Zmul_add_distr_r, Zadd_opp_diag_l, Zmul_0_l. +Qed. + +Theorem Zmul_opp_r : forall n m : Z, n * (- m) == - (n * m). +Proof. +intros n m; rewrite (Zmul_comm n (- m)), (Zmul_comm n m); apply Zmul_opp_l. +Qed. + +Theorem Zmul_opp_opp : forall n m : Z, (- n) * (- m) == n * m. +Proof. +intros n m; now rewrite Zmul_opp_l, Zmul_opp_r, Zopp_involutive. +Qed. + +Theorem Zmul_sub_distr_l : forall n m p : Z, n * (m - p) == n * m - n * p. +Proof. +intros n m p. do 2 rewrite <- Zadd_opp_r. rewrite Zmul_add_distr_l. +now rewrite Zmul_opp_r. +Qed. + +Theorem Zmul_sub_distr_r : forall n m p : Z, (n - m) * p == n * p - m * p. +Proof. +intros n m p; rewrite (Zmul_comm (n - m) p), (Zmul_comm n p), (Zmul_comm m p); +now apply Zmul_sub_distr_l. +Qed. + +End ZMulPropFunct. + + diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v new file mode 100644 index 0000000000..46a8a38aff --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -0,0 +1,343 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (p * n < p * m <-> q * n + m < q * m + n). +Proof NZmul_lt_pred. + +Theorem Zmul_lt_mono_pos_l : forall p n m : Z, 0 < p -> (n < m <-> p * n < p * m). +Proof NZmul_lt_mono_pos_l. + +Theorem Zmul_lt_mono_pos_r : forall p n m : Z, 0 < p -> (n < m <-> n * p < m * p). +Proof NZmul_lt_mono_pos_r. + +Theorem Zmul_lt_mono_neg_l : forall p n m : Z, p < 0 -> (n < m <-> p * m < p * n). +Proof NZmul_lt_mono_neg_l. + +Theorem Zmul_lt_mono_neg_r : forall p n m : Z, p < 0 -> (n < m <-> m * p < n * p). +Proof NZmul_lt_mono_neg_r. + +Theorem Zmul_le_mono_nonneg_l : forall n m p : Z, 0 <= p -> n <= m -> p * n <= p * m. +Proof NZmul_le_mono_nonneg_l. + +Theorem Zmul_le_mono_nonpos_l : forall n m p : Z, p <= 0 -> n <= m -> p * m <= p * n. +Proof NZmul_le_mono_nonpos_l. + +Theorem Zmul_le_mono_nonneg_r : forall n m p : Z, 0 <= p -> n <= m -> n * p <= m * p. +Proof NZmul_le_mono_nonneg_r. + +Theorem Zmul_le_mono_nonpos_r : forall n m p : Z, p <= 0 -> n <= m -> m * p <= n * p. +Proof NZmul_le_mono_nonpos_r. + +Theorem Zmul_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m). +Proof NZmul_cancel_l. + +Theorem Zmul_cancel_r : forall n m p : Z, p ~= 0 -> (n * p == m * p <-> n == m). +Proof NZmul_cancel_r. + +Theorem Zmul_id_l : forall n m : Z, m ~= 0 -> (n * m == m <-> n == 1). +Proof NZmul_id_l. + +Theorem Zmul_id_r : forall n m : Z, n ~= 0 -> (n * m == n <-> m == 1). +Proof NZmul_id_r. + +Theorem Zmul_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m). +Proof NZmul_le_mono_pos_l. + +Theorem Zmul_le_mono_pos_r : forall n m p : Z, 0 < p -> (n <= m <-> n * p <= m * p). +Proof NZmul_le_mono_pos_r. + +Theorem Zmul_le_mono_neg_l : forall n m p : Z, p < 0 -> (n <= m <-> p * m <= p * n). +Proof NZmul_le_mono_neg_l. + +Theorem Zmul_le_mono_neg_r : forall n m p : Z, p < 0 -> (n <= m <-> m * p <= n * p). +Proof NZmul_le_mono_neg_r. + +Theorem Zmul_lt_mono_nonneg : + forall n m p q : Z, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q. +Proof NZmul_lt_mono_nonneg. + +Theorem Zmul_lt_mono_nonpos : + forall n m p q : Z, m <= 0 -> n < m -> q <= 0 -> p < q -> m * q < n * p. +Proof. +intros n m p q H1 H2 H3 H4. +apply Zle_lt_trans with (m * p). +apply Zmul_le_mono_nonpos_l; [assumption | now apply Zlt_le_incl]. +apply -> Zmul_lt_mono_neg_r; [assumption | now apply Zlt_le_trans with q]. +Qed. + +Theorem Zmul_le_mono_nonneg : + forall n m p q : Z, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q. +Proof NZmul_le_mono_nonneg. + +Theorem Zmul_le_mono_nonpos : + forall n m p q : Z, m <= 0 -> n <= m -> q <= 0 -> p <= q -> m * q <= n * p. +Proof. +intros n m p q H1 H2 H3 H4. +apply Zle_trans with (m * p). +now apply Zmul_le_mono_nonpos_l. +apply Zmul_le_mono_nonpos_r; [now apply Zle_trans with q | assumption]. +Qed. + +Theorem Zmul_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n * m. +Proof NZmul_pos_pos. + +Theorem Zmul_neg_neg : forall n m : Z, n < 0 -> m < 0 -> 0 < n * m. +Proof NZmul_neg_neg. + +Theorem Zmul_pos_neg : forall n m : Z, 0 < n -> m < 0 -> n * m < 0. +Proof NZmul_pos_neg. + +Theorem Zmul_neg_pos : forall n m : Z, n < 0 -> 0 < m -> n * m < 0. +Proof NZmul_neg_pos. + +Theorem Zmul_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m. +Proof. +intros n m H1 H2. +rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonneg_r. +Qed. + +Theorem Zmul_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m. +Proof. +intros n m H1 H2. +rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonpos_r. +Qed. + +Theorem Zmul_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0. +Proof. +intros n m H1 H2. +rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonpos_r. +Qed. + +Theorem Zmul_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0. +Proof. +intros; rewrite Zmul_comm; now apply Zmul_nonneg_nonpos. +Qed. + +Theorem Zlt_1_mul_pos : forall n m : Z, 1 < n -> 0 < m -> 1 < n * m. +Proof NZlt_1_mul_pos. + +Theorem Zeq_mul_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0. +Proof NZeq_mul_0. + +Theorem Zneq_mul_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Proof NZneq_mul_0. + +Theorem Zeq_square_0 : forall n : Z, n * n == 0 <-> n == 0. +Proof NZeq_square_0. + +Theorem Zeq_mul_0_l : forall n m : Z, n * m == 0 -> m ~= 0 -> n == 0. +Proof NZeq_mul_0_l. + +Theorem Zeq_mul_0_r : forall n m : Z, n * m == 0 -> n ~= 0 -> m == 0. +Proof NZeq_mul_0_r. + +Theorem Zlt_0_mul : forall n m : Z, 0 < n * m <-> 0 < n /\ 0 < m \/ m < 0 /\ n < 0. +Proof NZlt_0_mul. + +Notation Zmul_pos := Zlt_0_mul (only parsing). + +Theorem Zlt_mul_0 : + forall n m : Z, n * m < 0 <-> n < 0 /\ m > 0 \/ n > 0 /\ m < 0. +Proof. +intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]]. +destruct (Zlt_trichotomy n 0) as [H1 | [H1 | H1]]; +[| rewrite H1 in H; rewrite Zmul_0_l in H; false_hyp H Zlt_irrefl |]; +(destruct (Zlt_trichotomy m 0) as [H2 | [H2 | H2]]; +[| rewrite H2 in H; rewrite Zmul_0_r in H; false_hyp H Zlt_irrefl |]); +try (left; now split); try (right; now split). +assert (H3 : n * m > 0) by now apply Zmul_neg_neg. +elimtype False; now apply (Zlt_asymm (n * m) 0). +assert (H3 : n * m > 0) by now apply Zmul_pos_pos. +elimtype False; now apply (Zlt_asymm (n * m) 0). +now apply Zmul_neg_pos. now apply Zmul_pos_neg. +Qed. + +Notation Zmul_neg := Zlt_mul_0 (only parsing). + +Theorem Zle_0_mul : + forall n m : Z, 0 <= n * m -> 0 <= n /\ 0 <= m \/ n <= 0 /\ m <= 0. +Proof. +assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_symm). +intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R. +rewrite Zlt_0_mul, Zeq_mul_0. +pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto. +Qed. + +Notation Zmul_nonneg := Zle_0_mul (only parsing). + +Theorem Zle_mul_0 : + forall n m : Z, n * m <= 0 -> 0 <= n /\ m <= 0 \/ n <= 0 /\ 0 <= m. +Proof. +assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_symm). +intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R. +rewrite Zlt_mul_0, Zeq_mul_0. +pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto. +Qed. + +Notation Zmul_nonpos := Zle_mul_0 (only parsing). + +Theorem Zle_0_square : forall n : Z, 0 <= n * n. +Proof. +intro n; destruct (Zneg_nonneg_cases n). +apply Zlt_le_incl; now apply Zmul_neg_neg. +now apply Zmul_nonneg_nonneg. +Qed. + +Notation Zsquare_nonneg := Zle_0_square (only parsing). + +Theorem Znlt_square_0 : forall n : Z, ~ n * n < 0. +Proof. +intros n H. apply -> Zlt_nge in H. apply H. apply Zsquare_nonneg. +Qed. + +Theorem Zsquare_lt_mono_nonneg : forall n m : Z, 0 <= n -> n < m -> n * n < m * m. +Proof NZsquare_lt_mono_nonneg. + +Theorem Zsquare_lt_mono_nonpos : forall n m : Z, n <= 0 -> m < n -> n * n < m * m. +Proof. +intros n m H1 H2. now apply Zmul_lt_mono_nonpos. +Qed. + +Theorem Zsquare_le_mono_nonneg : forall n m : Z, 0 <= n -> n <= m -> n * n <= m * m. +Proof NZsquare_le_mono_nonneg. + +Theorem Zsquare_le_mono_nonpos : forall n m : Z, n <= 0 -> m <= n -> n * n <= m * m. +Proof. +intros n m H1 H2. now apply Zmul_le_mono_nonpos. +Qed. + +Theorem Zsquare_lt_simpl_nonneg : forall n m : Z, 0 <= m -> n * n < m * m -> n < m. +Proof NZsquare_lt_simpl_nonneg. + +Theorem Zsquare_le_simpl_nonneg : forall n m : Z, 0 <= m -> n * n <= m * m -> n <= m. +Proof NZsquare_le_simpl_nonneg. + +Theorem Zsquare_lt_simpl_nonpos : forall n m : Z, m <= 0 -> n * n < m * m -> m < n. +Proof. +intros n m H1 H2. destruct (Zle_gt_cases n 0). +destruct (NZlt_ge_cases m n). +assumption. assert (F : m * m <= n * n) by now apply Zsquare_le_mono_nonpos. +apply -> NZle_ngt in F. false_hyp H2 F. +now apply Zle_lt_trans with 0. +Qed. + +Theorem Zsquare_le_simpl_nonpos : forall n m : NZ, m <= 0 -> n * n <= m * m -> m <= n. +Proof. +intros n m H1 H2. destruct (NZle_gt_cases n 0). +destruct (NZle_gt_cases m n). +assumption. assert (F : m * m < n * n) by now apply Zsquare_lt_mono_nonpos. +apply -> NZlt_nge in F. false_hyp H2 F. +apply Zlt_le_incl; now apply NZle_lt_trans with 0. +Qed. + +Theorem Zmul_2_mono_l : forall n m : Z, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Proof NZmul_2_mono_l. + +Theorem Zlt_1_mul_neg : forall n m : Z, n < -1 -> m < 0 -> 1 < n * m. +Proof. +intros n m H1 H2. apply -> (NZmul_lt_mono_neg_r m) in H1. +apply <- Zopp_pos_neg in H2. rewrite Zmul_opp_l, Zmul_1_l in H1. +now apply Zlt_1_l with (- m). +assumption. +Qed. + +Theorem Zlt_mul_n1_neg : forall n m : Z, 1 < n -> m < 0 -> n * m < -1. +Proof. +intros n m H1 H2. apply -> (NZmul_lt_mono_neg_r m) in H1. +rewrite Zmul_1_l in H1. now apply Zlt_n1_r with m. +assumption. +Qed. + +Theorem Zlt_mul_n1_pos : forall n m : Z, n < -1 -> 0 < m -> n * m < -1. +Proof. +intros n m H1 H2. apply -> (NZmul_lt_mono_pos_r m) in H1. +rewrite Zmul_opp_l, Zmul_1_l in H1. +apply <- Zopp_neg_pos in H2. now apply Zlt_n1_r with (- m). +assumption. +Qed. + +Theorem Zlt_1_mul_l : forall n m : Z, 1 < n -> n * m < -1 \/ n * m == 0 \/ 1 < n * m. +Proof. +intros n m H; destruct (Zlt_trichotomy m 0) as [H1 | [H1 | H1]]. +left. now apply Zlt_mul_n1_neg. +right; left; now rewrite H1, Zmul_0_r. +right; right; now apply Zlt_1_mul_pos. +Qed. + +Theorem Zlt_n1_mul_r : forall n m : Z, n < -1 -> n * m < -1 \/ n * m == 0 \/ 1 < n * m. +Proof. +intros n m H; destruct (Zlt_trichotomy m 0) as [H1 | [H1 | H1]]. +right; right. now apply Zlt_1_mul_neg. +right; left; now rewrite H1, Zmul_0_r. +left. now apply Zlt_mul_n1_pos. +Qed. + +Theorem Zeq_mul_1 : forall n m : Z, n * m == 1 -> n == 1 \/ n == -1. +Proof. +assert (F : ~ 1 < -1). +intro H. +assert (H1 : -1 < 0). apply <- Zopp_neg_pos. apply Zlt_succ_diag_r. +assert (H2 : 1 < 0) by now apply Zlt_trans with (-1). false_hyp H2 Znlt_succ_diag_l. +Z0_pos_neg n. +intros m H; rewrite Zmul_0_l in H; false_hyp H Zneq_succ_diag_r. +intros n H; split; apply <- Zle_succ_l in H; le_elim H. +intros m H1; apply (Zlt_1_mul_l n m) in H. +rewrite H1 in H; destruct H as [H | [H | H]]. +false_hyp H F. false_hyp H Zneq_succ_diag_l. false_hyp H Zlt_irrefl. +intros; now left. +intros m H1; apply (Zlt_1_mul_l n m) in H. rewrite Zmul_opp_l in H1; +apply -> Zeq_opp_l in H1. rewrite H1 in H; destruct H as [H | [H | H]]. +false_hyp H Zlt_irrefl. apply -> Zeq_opp_l in H. rewrite Zopp_0 in H. +false_hyp H Zneq_succ_diag_l. false_hyp H F. +intros; right; symmetry; now apply Zopp_wd. +Qed. + +Theorem Zlt_mul_diag_l : forall n m : Z, n < 0 -> (1 < m <-> n * m < n). +Proof. +intros n m H. stepr (n * m < n * 1) by now rewrite Zmul_1_r. +now apply Zmul_lt_mono_neg_l. +Qed. + +Theorem Zlt_mul_diag_r : forall n m : Z, 0 < n -> (1 < m <-> n < n * m). +Proof. +intros n m H. stepr (n * 1 < n * m) by now rewrite Zmul_1_r. +now apply Zmul_lt_mono_pos_l. +Qed. + +Theorem Zle_mul_diag_l : forall n m : Z, n < 0 -> (1 <= m <-> n * m <= n). +Proof. +intros n m H. stepr (n * m <= n * 1) by now rewrite Zmul_1_r. +now apply Zmul_le_mono_neg_l. +Qed. + +Theorem Zle_mul_diag_r : forall n m : Z, 0 < n -> (1 <= m <-> n <= n * m). +Proof. +intros n m H. stepr (n * 1 <= n * m) by now rewrite Zmul_1_r. +now apply Zmul_le_mono_pos_l. +Qed. + +Theorem Zlt_mul_r : forall n m p : Z, 0 < n -> 1 < p -> n < m -> n < m * p. +Proof. +intros. stepl (n * 1) by now rewrite Zmul_1_r. +apply Zmul_lt_mono_nonneg. +now apply Zlt_le_incl. assumption. apply Zle_0_1. assumption. +Qed. + +End ZMulOrderPropFunct. + diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v deleted file mode 100644 index d72d00379c..0000000000 --- a/theories/Numbers/Integer/Abstract/ZPlus.v +++ /dev/null @@ -1,345 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* forall m1 m2 : Z, m1 == m2 -> n1 + m1 == n2 + m2. -Proof NZadd_wd. - -Theorem Zadd_0_l : forall n : Z, 0 + n == n. -Proof NZadd_0_l. - -Theorem Zadd_succ_l : forall n m : Z, (S n) + m == S (n + m). -Proof NZadd_succ_l. - -Theorem Zminus_0_r : forall n : Z, n - 0 == n. -Proof NZminus_0_r. - -Theorem Zminus_succ_r : forall n m : Z, n - (S m) == P (n - m). -Proof NZminus_succ_r. - -Theorem Zopp_0 : - 0 == 0. -Proof Zopp_0. - -Theorem Zopp_succ : forall n : Z, - (S n) == P (- n). -Proof Zopp_succ. - -(* Theorems that are valid for both natural numbers and integers *) - -Theorem Zadd_0_r : forall n : Z, n + 0 == n. -Proof NZadd_0_r. - -Theorem Zadd_succ_r : forall n m : Z, n + S m == S (n + m). -Proof NZadd_succ_r. - -Theorem Zadd_comm : forall n m : Z, n + m == m + n. -Proof NZadd_comm. - -Theorem Zadd_assoc : forall n m p : Z, n + (m + p) == (n + m) + p. -Proof NZadd_assoc. - -Theorem Zadd_shuffle1 : forall n m p q : Z, (n + m) + (p + q) == (n + p) + (m + q). -Proof NZadd_shuffle1. - -Theorem Zadd_shuffle2 : forall n m p q : Z, (n + m) + (p + q) == (n + q) + (m + p). -Proof NZadd_shuffle2. - -Theorem Zadd_1_l : forall n : Z, 1 + n == S n. -Proof NZadd_1_l. - -Theorem Zadd_1_r : forall n : Z, n + 1 == S n. -Proof NZadd_1_r. - -Theorem Zadd_cancel_l : forall n m p : Z, p + n == p + m <-> n == m. -Proof NZadd_cancel_l. - -Theorem Zadd_cancel_r : forall n m p : Z, n + p == m + p <-> n == m. -Proof NZadd_cancel_r. - -(* Theorems that are either not valid on N or have different proofs on N and Z *) - -Theorem Zadd_pred_l : forall n m : Z, P n + m == P (n + m). -Proof. -intros n m. -rewrite <- (Zsucc_pred n) at 2. -rewrite Zadd_succ_l. now rewrite Zpred_succ. -Qed. - -Theorem Zadd_pred_r : forall n m : Z, n + P m == P (n + m). -Proof. -intros n m; rewrite (Zadd_comm n (P m)), (Zadd_comm n m); -apply Zadd_pred_l. -Qed. - -Theorem Zadd_opp_r : forall n m : Z, n + (- m) == n - m. -Proof. -NZinduct m. -rewrite Zopp_0; rewrite Zminus_0_r; now rewrite Zadd_0_r. -intro m. rewrite Zopp_succ, Zminus_succ_r, Zadd_pred_r; now rewrite Zpred_inj_wd. -Qed. - -Theorem Zminus_0_l : forall n : Z, 0 - n == - n. -Proof. -intro n; rewrite <- Zadd_opp_r; now rewrite Zadd_0_l. -Qed. - -Theorem Zminus_succ_l : forall n m : Z, S n - m == S (n - m). -Proof. -intros n m; do 2 rewrite <- Zadd_opp_r; now rewrite Zadd_succ_l. -Qed. - -Theorem Zminus_pred_l : forall n m : Z, P n - m == P (n - m). -Proof. -intros n m. rewrite <- (Zsucc_pred n) at 2. -rewrite Zminus_succ_l; now rewrite Zpred_succ. -Qed. - -Theorem Zminus_pred_r : forall n m : Z, n - (P m) == S (n - m). -Proof. -intros n m. rewrite <- (Zsucc_pred m) at 2. -rewrite Zminus_succ_r; now rewrite Zsucc_pred. -Qed. - -Theorem Zopp_pred : forall n : Z, - (P n) == S (- n). -Proof. -intro n. rewrite <- (Zsucc_pred n) at 2. -rewrite Zopp_succ. now rewrite Zsucc_pred. -Qed. - -Theorem Zminus_diag : forall n : Z, n - n == 0. -Proof. -NZinduct n. -now rewrite Zminus_0_r. -intro n. rewrite Zminus_succ_r, Zminus_succ_l; now rewrite Zpred_succ. -Qed. - -Theorem Zadd_opp_diag_l : forall n : Z, - n + n == 0. -Proof. -intro n; now rewrite Zadd_comm, Zadd_opp_r, Zminus_diag. -Qed. - -Theorem Zadd_opp_diag_r : forall n : Z, n + (- n) == 0. -Proof. -intro n; rewrite Zadd_comm; apply Zadd_opp_diag_l. -Qed. - -Theorem Zadd_opp_l : forall n m : Z, - m + n == n - m. -Proof. -intros n m; rewrite <- Zadd_opp_r; now rewrite Zadd_comm. -Qed. - -Theorem Zadd_minus_assoc : forall n m p : Z, n + (m - p) == (n + m) - p. -Proof. -intros n m p; do 2 rewrite <- Zadd_opp_r; now rewrite Zadd_assoc. -Qed. - -Theorem Zopp_involutive : forall n : Z, - (- n) == n. -Proof. -NZinduct n. -now do 2 rewrite Zopp_0. -intro n. rewrite Zopp_succ, Zopp_pred; now rewrite Zsucc_inj_wd. -Qed. - -Theorem Zopp_add_distr : forall n m : Z, - (n + m) == - n + (- m). -Proof. -intros n m; NZinduct n. -rewrite Zopp_0; now do 2 rewrite Zadd_0_l. -intro n. rewrite Zadd_succ_l; do 2 rewrite Zopp_succ; rewrite Zadd_pred_l. -now rewrite Zpred_inj_wd. -Qed. - -Theorem Zopp_minus_distr : forall n m : Z, - (n - m) == - n + m. -Proof. -intros n m; rewrite <- Zadd_opp_r, Zopp_add_distr. -now rewrite Zopp_involutive. -Qed. - -Theorem Zopp_inj : forall n m : Z, - n == - m -> n == m. -Proof. -intros n m H. apply Zopp_wd in H. now do 2 rewrite Zopp_involutive in H. -Qed. - -Theorem Zopp_inj_wd : forall n m : Z, - n == - m <-> n == m. -Proof. -intros n m; split; [apply Zopp_inj | apply Zopp_wd]. -Qed. - -Theorem Zeq_opp_l : forall n m : Z, - n == m <-> n == - m. -Proof. -intros n m. now rewrite <- (Zopp_inj_wd (- n) m), Zopp_involutive. -Qed. - -Theorem Zeq_opp_r : forall n m : Z, n == - m <-> - n == m. -Proof. -symmetry; apply Zeq_opp_l. -Qed. - -Theorem Zminus_add_distr : forall n m p : Z, n - (m + p) == (n - m) - p. -Proof. -intros n m p; rewrite <- Zadd_opp_r, Zopp_add_distr, Zadd_assoc. -now do 2 rewrite Zadd_opp_r. -Qed. - -Theorem Zminus_minus_distr : forall n m p : Z, n - (m - p) == (n - m) + p. -Proof. -intros n m p; rewrite <- Zadd_opp_r, Zopp_minus_distr, Zadd_assoc. -now rewrite Zadd_opp_r. -Qed. - -Theorem minus_opp_l : forall n m : Z, - n - m == - m - n. -Proof. -intros n m. do 2 rewrite <- Zadd_opp_r. now rewrite Zadd_comm. -Qed. - -Theorem Zminus_opp_r : forall n m : Z, n - (- m) == n + m. -Proof. -intros n m; rewrite <- Zadd_opp_r; now rewrite Zopp_involutive. -Qed. - -Theorem Zadd_minus_swap : forall n m p : Z, n + m - p == n - p + m. -Proof. -intros n m p. rewrite <- Zadd_minus_assoc, <- (Zadd_opp_r n p), <- Zadd_assoc. -now rewrite Zadd_opp_l. -Qed. - -Theorem Zminus_cancel_l : forall n m p : Z, n - m == n - p <-> m == p. -Proof. -intros n m p. rewrite <- (Zadd_cancel_l (n - m) (n - p) (- n)). -do 2 rewrite Zadd_minus_assoc. rewrite Zadd_opp_diag_l; do 2 rewrite Zminus_0_l. -apply Zopp_inj_wd. -Qed. - -Theorem Zminus_cancel_r : forall n m p : Z, n - p == m - p <-> n == m. -Proof. -intros n m p. -stepl (n - p + p == m - p + p) by apply Zadd_cancel_r. -now do 2 rewrite <- Zminus_minus_distr, Zminus_diag, Zminus_0_r. -Qed. - -(* The next several theorems are devoted to moving terms from one side of -an equation to the other. The name contains the operation in the original -equation (add or minus) and the indication whether the left or right term -is moved. *) - -Theorem Zadd_move_l : forall n m p : Z, n + m == p <-> m == p - n. -Proof. -intros n m p. -stepl (n + m - n == p - n) by apply Zminus_cancel_r. -now rewrite Zadd_comm, <- Zadd_minus_assoc, Zminus_diag, Zadd_0_r. -Qed. - -Theorem Zadd_move_r : forall n m p : Z, n + m == p <-> n == p - m. -Proof. -intros n m p; rewrite Zadd_comm; now apply Zadd_move_l. -Qed. - -(* The two theorems above do not allow rewriting subformulas of the form -n - m == p to n == p + m since subtraction is in the right-hand side of -the equation. Hence the following two theorems. *) - -Theorem Zminus_move_l : forall n m p : Z, n - m == p <-> - m == p - n. -Proof. -intros n m p; rewrite <- (Zadd_opp_r n m); apply Zadd_move_l. -Qed. - -Theorem Zminus_move_r : forall n m p : Z, n - m == p <-> n == p + m. -Proof. -intros n m p; rewrite <- (Zadd_opp_r n m). now rewrite Zadd_move_r, Zminus_opp_r. -Qed. - -Theorem Zadd_move_0_l : forall n m : Z, n + m == 0 <-> m == - n. -Proof. -intros n m; now rewrite Zadd_move_l, Zminus_0_l. -Qed. - -Theorem Zadd_move_0_r : forall n m : Z, n + m == 0 <-> n == - m. -Proof. -intros n m; now rewrite Zadd_move_r, Zminus_0_l. -Qed. - -Theorem Zminus_move_0_l : forall n m : Z, n - m == 0 <-> - m == - n. -Proof. -intros n m. now rewrite Zminus_move_l, Zminus_0_l. -Qed. - -Theorem Zminus_move_0_r : forall n m : Z, n - m == 0 <-> n == m. -Proof. -intros n m. now rewrite Zminus_move_r, Zadd_0_l. -Qed. - -(* The following section is devoted to cancellation of like terms. The name -includes the first operator and the position of the term being canceled. *) - -Theorem Zadd_simpl_l : forall n m : Z, n + m - n == m. -Proof. -intros; now rewrite Zadd_minus_swap, Zminus_diag, Zadd_0_l. -Qed. - -Theorem Zadd_simpl_r : forall n m : Z, n + m - m == n. -Proof. -intros; now rewrite <- Zadd_minus_assoc, Zminus_diag, Zadd_0_r. -Qed. - -Theorem Zminus_simpl_l : forall n m : Z, - n - m + n == - m. -Proof. -intros; now rewrite <- Zadd_minus_swap, Zadd_opp_diag_l, Zminus_0_l. -Qed. - -Theorem Zminus_simpl_r : forall n m : Z, n - m + m == n. -Proof. -intros; now rewrite <- Zminus_minus_distr, Zminus_diag, Zminus_0_r. -Qed. - -(* Now we have two sums or differences; the name includes the two operators -and the position of the terms being canceled *) - -Theorem Zadd_add_simpl_l_l : forall n m p : Z, (n + m) - (n + p) == m - p. -Proof. -intros n m p. now rewrite (Zadd_comm n m), <- Zadd_minus_assoc, -Zminus_add_distr, Zminus_diag, Zminus_0_l, Zadd_opp_r. -Qed. - -Theorem Zadd_add_simpl_l_r : forall n m p : Z, (n + m) - (p + n) == m - p. -Proof. -intros n m p. rewrite (Zadd_comm p n); apply Zadd_add_simpl_l_l. -Qed. - -Theorem Zadd_add_simpl_r_l : forall n m p : Z, (n + m) - (m + p) == n - p. -Proof. -intros n m p. rewrite (Zadd_comm n m); apply Zadd_add_simpl_l_l. -Qed. - -Theorem Zadd_add_simpl_r_r : forall n m p : Z, (n + m) - (p + m) == n - p. -Proof. -intros n m p. rewrite (Zadd_comm p m); apply Zadd_add_simpl_r_l. -Qed. - -Theorem Zminus_add_simpl_r_l : forall n m p : Z, (n - m) + (m + p) == n + p. -Proof. -intros n m p. now rewrite <- Zminus_minus_distr, Zminus_add_distr, Zminus_diag, -Zminus_0_l, Zminus_opp_r. -Qed. - -Theorem Zminus_add_simpl_r_r : forall n m p : Z, (n - m) + (p + m) == n + p. -Proof. -intros n m p. rewrite (Zadd_comm p m); apply Zminus_add_simpl_r_l. -Qed. - -(* Of course, there are many other variants *) - -End ZPlusPropFunct. - diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v deleted file mode 100644 index 85f6714987..0000000000 --- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v +++ /dev/null @@ -1,373 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* p + n < p + m. -Proof NZadd_lt_mono_l. - -Theorem Zadd_lt_mono_r : forall n m p : Z, n < m <-> n + p < m + p. -Proof NZadd_lt_mono_r. - -Theorem Zadd_lt_mono : forall n m p q : Z, n < m -> p < q -> n + p < m + q. -Proof NZadd_lt_mono. - -Theorem Zadd_le_mono_l : forall n m p : Z, n <= m <-> p + n <= p + m. -Proof NZadd_le_mono_l. - -Theorem Zadd_le_mono_r : forall n m p : Z, n <= m <-> n + p <= m + p. -Proof NZadd_le_mono_r. - -Theorem Zadd_le_mono : forall n m p q : Z, n <= m -> p <= q -> n + p <= m + q. -Proof NZadd_le_mono. - -Theorem Zadd_lt_le_mono : forall n m p q : Z, n < m -> p <= q -> n + p < m + q. -Proof NZadd_lt_le_mono. - -Theorem Zadd_le_lt_mono : forall n m p q : Z, n <= m -> p < q -> n + p < m + q. -Proof NZadd_le_lt_mono. - -Theorem Zadd_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n + m. -Proof NZadd_pos_pos. - -Theorem Zadd_pos_nonneg : forall n m : Z, 0 < n -> 0 <= m -> 0 < n + m. -Proof NZadd_pos_nonneg. - -Theorem Zadd_nonneg_pos : forall n m : Z, 0 <= n -> 0 < m -> 0 < n + m. -Proof NZadd_nonneg_pos. - -Theorem Zadd_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n + m. -Proof NZadd_nonneg_nonneg. - -Theorem Zlt_add_pos_l : forall n m : Z, 0 < n -> m < n + m. -Proof NZlt_add_pos_l. - -Theorem Zlt_add_pos_r : forall n m : Z, 0 < n -> m < m + n. -Proof NZlt_add_pos_r. - -Theorem Zle_lt_add_lt : forall n m p q : Z, n <= m -> p + m < q + n -> p < q. -Proof NZle_lt_add_lt. - -Theorem Zlt_le_add_lt : forall n m p q : Z, n < m -> p + m <= q + n -> p < q. -Proof NZlt_le_add_lt. - -Theorem Zle_le_add_le : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q. -Proof NZle_le_add_le. - -Theorem Zadd_lt_cases : forall n m p q : Z, n + m < p + q -> n < p \/ m < q. -Proof NZadd_lt_cases. - -Theorem Zadd_le_cases : forall n m p q : Z, n + m <= p + q -> n <= p \/ m <= q. -Proof NZadd_le_cases. - -Theorem Zadd_neg_cases : forall n m : Z, n + m < 0 -> n < 0 \/ m < 0. -Proof NZadd_neg_cases. - -Theorem Zadd_pos_cases : forall n m : Z, 0 < n + m -> 0 < n \/ 0 < m. -Proof NZadd_pos_cases. - -Theorem Zadd_nonpos_cases : forall n m : Z, n + m <= 0 -> n <= 0 \/ m <= 0. -Proof NZadd_nonpos_cases. - -Theorem Zadd_nonneg_cases : forall n m : Z, 0 <= n + m -> 0 <= n \/ 0 <= m. -Proof NZadd_nonneg_cases. - -(* Theorems that are either not valid on N or have different proofs on N and Z *) - -Theorem Zadd_neg_neg : forall n m : Z, n < 0 -> m < 0 -> n + m < 0. -Proof. -intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_lt_mono. -Qed. - -Theorem Zadd_neg_nonpos : forall n m : Z, n < 0 -> m <= 0 -> n + m < 0. -Proof. -intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_lt_le_mono. -Qed. - -Theorem Zadd_nonpos_neg : forall n m : Z, n <= 0 -> m < 0 -> n + m < 0. -Proof. -intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_le_lt_mono. -Qed. - -Theorem Zadd_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> n + m <= 0. -Proof. -intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_le_mono. -Qed. - -(** Minus and order *) - -Theorem Zlt_0_minus : forall n m : Z, 0 < m - n <-> n < m. -Proof. -intros n m. stepl (0 + n < m - n + n) by symmetry; apply Zadd_lt_mono_r. -rewrite Zadd_0_l; now rewrite Zminus_simpl_r. -Qed. - -Notation Zminus_pos := Zlt_0_minus (only parsing). - -Theorem Zle_0_minus : forall n m : Z, 0 <= m - n <-> n <= m. -Proof. -intros n m; stepl (0 + n <= m - n + n) by symmetry; apply Zadd_le_mono_r. -rewrite Zadd_0_l; now rewrite Zminus_simpl_r. -Qed. - -Notation Zminus_nonneg := Zle_0_minus (only parsing). - -Theorem Zlt_minus_0 : forall n m : Z, n - m < 0 <-> n < m. -Proof. -intros n m. stepl (n - m + m < 0 + m) by symmetry; apply Zadd_lt_mono_r. -rewrite Zadd_0_l; now rewrite Zminus_simpl_r. -Qed. - -Notation Zminus_neg := Zlt_minus_0 (only parsing). - -Theorem Zle_minus_0 : forall n m : Z, n - m <= 0 <-> n <= m. -Proof. -intros n m. stepl (n - m + m <= 0 + m) by symmetry; apply Zadd_le_mono_r. -rewrite Zadd_0_l; now rewrite Zminus_simpl_r. -Qed. - -Notation Zminus_nonpos := Zle_minus_0 (only parsing). - -Theorem Zopp_lt_mono : forall n m : Z, n < m <-> - m < - n. -Proof. -intros n m. stepr (m + - m < m + - n) by symmetry; apply Zadd_lt_mono_l. -do 2 rewrite Zadd_opp_r. rewrite Zminus_diag. symmetry; apply Zlt_0_minus. -Qed. - -Theorem Zopp_le_mono : forall n m : Z, n <= m <-> - m <= - n. -Proof. -intros n m. stepr (m + - m <= m + - n) by symmetry; apply Zadd_le_mono_l. -do 2 rewrite Zadd_opp_r. rewrite Zminus_diag. symmetry; apply Zle_0_minus. -Qed. - -Theorem Zopp_pos_neg : forall n : Z, 0 < - n <-> n < 0. -Proof. -intro n; rewrite (Zopp_lt_mono n 0); now rewrite Zopp_0. -Qed. - -Theorem Zopp_neg_pos : forall n : Z, - n < 0 <-> 0 < n. -Proof. -intro n. rewrite (Zopp_lt_mono 0 n). now rewrite Zopp_0. -Qed. - -Theorem Zopp_nonneg_nonpos : forall n : Z, 0 <= - n <-> n <= 0. -Proof. -intro n; rewrite (Zopp_le_mono n 0); now rewrite Zopp_0. -Qed. - -Theorem Zopp_nonpos_nonneg : forall n : Z, - n <= 0 <-> 0 <= n. -Proof. -intro n. rewrite (Zopp_le_mono 0 n). now rewrite Zopp_0. -Qed. - -Theorem Zminus_lt_mono_l : forall n m p : Z, n < m <-> p - m < p - n. -Proof. -intros n m p. do 2 rewrite <- Zadd_opp_r. rewrite <- Zadd_lt_mono_l. -apply Zopp_lt_mono. -Qed. - -Theorem Zminus_lt_mono_r : forall n m p : Z, n < m <-> n - p < m - p. -Proof. -intros n m p; do 2 rewrite <- Zadd_opp_r; apply Zadd_lt_mono_r. -Qed. - -Theorem Zminus_lt_mono : forall n m p q : Z, n < m -> q < p -> n - p < m - q. -Proof. -intros n m p q H1 H2. -apply NZlt_trans with (m - p); -[now apply -> Zminus_lt_mono_r | now apply -> Zminus_lt_mono_l]. -Qed. - -Theorem Zminus_le_mono_l : forall n m p : Z, n <= m <-> p - m <= p - n. -Proof. -intros n m p; do 2 rewrite <- Zadd_opp_r; rewrite <- Zadd_le_mono_l; -apply Zopp_le_mono. -Qed. - -Theorem Zminus_le_mono_r : forall n m p : Z, n <= m <-> n - p <= m - p. -Proof. -intros n m p; do 2 rewrite <- Zadd_opp_r; apply Zadd_le_mono_r. -Qed. - -Theorem Zminus_le_mono : forall n m p q : Z, n <= m -> q <= p -> n - p <= m - q. -Proof. -intros n m p q H1 H2. -apply NZle_trans with (m - p); -[now apply -> Zminus_le_mono_r | now apply -> Zminus_le_mono_l]. -Qed. - -Theorem Zminus_lt_le_mono : forall n m p q : Z, n < m -> q <= p -> n - p < m - q. -Proof. -intros n m p q H1 H2. -apply NZlt_le_trans with (m - p); -[now apply -> Zminus_lt_mono_r | now apply -> Zminus_le_mono_l]. -Qed. - -Theorem Zminus_le_lt_mono : forall n m p q : Z, n <= m -> q < p -> n - p < m - q. -Proof. -intros n m p q H1 H2. -apply NZle_lt_trans with (m - p); -[now apply -> Zminus_le_mono_r | now apply -> Zminus_lt_mono_l]. -Qed. - -Theorem Zle_lt_minus_lt : forall n m p q : Z, n <= m -> p - n < q - m -> p < q. -Proof. -intros n m p q H1 H2. apply (Zle_lt_add_lt (- m) (- n)); -[now apply -> Zopp_le_mono | now do 2 rewrite Zadd_opp_r]. -Qed. - -Theorem Zlt_le_minus_lt : forall n m p q : Z, n < m -> p - n <= q - m -> p < q. -Proof. -intros n m p q H1 H2. apply (Zlt_le_add_lt (- m) (- n)); -[now apply -> Zopp_lt_mono | now do 2 rewrite Zadd_opp_r]. -Qed. - -Theorem Zle_le_minus_lt : forall n m p q : Z, n <= m -> p - n <= q - m -> p <= q. -Proof. -intros n m p q H1 H2. apply (Zle_le_add_le (- m) (- n)); -[now apply -> Zopp_le_mono | now do 2 rewrite Zadd_opp_r]. -Qed. - -Theorem Zlt_add_lt_minus_r : forall n m p : Z, n + p < m <-> n < m - p. -Proof. -intros n m p. stepl (n + p - p < m - p) by symmetry; apply Zminus_lt_mono_r. -now rewrite Zadd_simpl_r. -Qed. - -Theorem Zle_add_le_minus_r : forall n m p : Z, n + p <= m <-> n <= m - p. -Proof. -intros n m p. stepl (n + p - p <= m - p) by symmetry; apply Zminus_le_mono_r. -now rewrite Zadd_simpl_r. -Qed. - -Theorem Zlt_add_lt_minus_l : forall n m p : Z, n + p < m <-> p < m - n. -Proof. -intros n m p. rewrite Zadd_comm; apply Zlt_add_lt_minus_r. -Qed. - -Theorem Zle_add_le_minus_l : forall n m p : Z, n + p <= m <-> p <= m - n. -Proof. -intros n m p. rewrite Zadd_comm; apply Zle_add_le_minus_r. -Qed. - -Theorem Zlt_minus_lt_add_r : forall n m p : Z, n - p < m <-> n < m + p. -Proof. -intros n m p. stepl (n - p + p < m + p) by symmetry; apply Zadd_lt_mono_r. -now rewrite Zminus_simpl_r. -Qed. - -Theorem Zle_minus_le_add_r : forall n m p : Z, n - p <= m <-> n <= m + p. -Proof. -intros n m p. stepl (n - p + p <= m + p) by symmetry; apply Zadd_le_mono_r. -now rewrite Zminus_simpl_r. -Qed. - -Theorem Zlt_minus_lt_add_l : forall n m p : Z, n - m < p <-> n < m + p. -Proof. -intros n m p. rewrite Zadd_comm; apply Zlt_minus_lt_add_r. -Qed. - -Theorem Zle_minus_le_add_l : forall n m p : Z, n - m <= p <-> n <= m + p. -Proof. -intros n m p. rewrite Zadd_comm; apply Zle_minus_le_add_r. -Qed. - -Theorem Zlt_minus_lt_add : forall n m p q : Z, n - m < p - q <-> n + q < m + p. -Proof. -intros n m p q. rewrite Zlt_minus_lt_add_l. rewrite Zadd_minus_assoc. -now rewrite <- Zlt_add_lt_minus_r. -Qed. - -Theorem Zle_minus_le_add : forall n m p q : Z, n - m <= p - q <-> n + q <= m + p. -Proof. -intros n m p q. rewrite Zle_minus_le_add_l. rewrite Zadd_minus_assoc. -now rewrite <- Zle_add_le_minus_r. -Qed. - -Theorem Zlt_minus_pos : forall n m : Z, 0 < m <-> n - m < n. -Proof. -intros n m. stepr (n - m < n - 0) by now rewrite Zminus_0_r. apply Zminus_lt_mono_l. -Qed. - -Theorem Zle_minus_nonneg : forall n m : Z, 0 <= m <-> n - m <= n. -Proof. -intros n m. stepr (n - m <= n - 0) by now rewrite Zminus_0_r. apply Zminus_le_mono_l. -Qed. - -Theorem Zminus_lt_cases : forall n m p q : Z, n - m < p - q -> n < m \/ q < p. -Proof. -intros n m p q H. rewrite Zlt_minus_lt_add in H. now apply Zadd_lt_cases. -Qed. - -Theorem Zminus_le_cases : forall n m p q : Z, n - m <= p - q -> n <= m \/ q <= p. -Proof. -intros n m p q H. rewrite Zle_minus_le_add in H. now apply Zadd_le_cases. -Qed. - -Theorem Zminus_neg_cases : forall n m : Z, n - m < 0 -> n < 0 \/ 0 < m. -Proof. -intros n m H; rewrite <- Zadd_opp_r in H. -setoid_replace (0 < m) with (- m < 0) using relation iff by (symmetry; apply Zopp_neg_pos). -now apply Zadd_neg_cases. -Qed. - -Theorem Zminus_pos_cases : forall n m : Z, 0 < n - m -> 0 < n \/ m < 0. -Proof. -intros n m H; rewrite <- Zadd_opp_r in H. -setoid_replace (m < 0) with (0 < - m) using relation iff by (symmetry; apply Zopp_pos_neg). -now apply Zadd_pos_cases. -Qed. - -Theorem Zminus_nonpos_cases : forall n m : Z, n - m <= 0 -> n <= 0 \/ 0 <= m. -Proof. -intros n m H; rewrite <- Zadd_opp_r in H. -setoid_replace (0 <= m) with (- m <= 0) using relation iff by (symmetry; apply Zopp_nonpos_nonneg). -now apply Zadd_nonpos_cases. -Qed. - -Theorem Zminus_nonneg_cases : forall n m : Z, 0 <= n - m -> 0 <= n \/ m <= 0. -Proof. -intros n m H; rewrite <- Zadd_opp_r in H. -setoid_replace (m <= 0) with (0 <= - m) using relation iff by (symmetry; apply Zopp_nonneg_nonpos). -now apply Zadd_nonneg_cases. -Qed. - -Section PosNeg. - -Variable P : Z -> Prop. -Hypothesis P_wd : predicate_wd Zeq P. - -Add Morphism P with signature Zeq ==> iff as P_morph. Proof. exact P_wd. Qed. - -Theorem Z0_pos_neg : - P 0 -> (forall n : Z, 0 < n -> P n /\ P (- n)) -> forall n : Z, P n. -Proof. -intros H1 H2 n. destruct (Zlt_trichotomy n 0) as [H3 | [H3 | H3]]. -apply <- Zopp_pos_neg in H3. apply H2 in H3. destruct H3 as [_ H3]. -now rewrite Zopp_involutive in H3. -now rewrite H3. -apply H2 in H3; now destruct H3. -Qed. - -End PosNeg. - -Ltac Z0_pos_neg n := induction_maker n ltac:(apply Z0_pos_neg). - -End ZPlusOrderPropFunct. - - diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v deleted file mode 100644 index ccf324a062..0000000000 --- a/theories/Numbers/Integer/Abstract/ZTimes.v +++ /dev/null @@ -1,115 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* forall m1 m2 : Z, m1 == m2 -> n1 * m1 == n2 * m2. -Proof NZmul_wd. - -Theorem Zmul_0_l : forall n : Z, 0 * n == 0. -Proof NZmul_0_l. - -Theorem Zmul_succ_l : forall n m : Z, (S n) * m == n * m + m. -Proof NZmul_succ_l. - -(* Theorems that are valid for both natural numbers and integers *) - -Theorem Zmul_0_r : forall n : Z, n * 0 == 0. -Proof NZmul_0_r. - -Theorem Zmul_succ_r : forall n m : Z, n * (S m) == n * m + n. -Proof NZmul_succ_r. - -Theorem Zmul_comm : forall n m : Z, n * m == m * n. -Proof NZmul_comm. - -Theorem Zmul_add_distr_r : forall n m p : Z, (n + m) * p == n * p + m * p. -Proof NZmul_add_distr_r. - -Theorem Zmul_add_distr_l : forall n m p : Z, n * (m + p) == n * m + n * p. -Proof NZmul_add_distr_l. - -(* A note on naming: right (correspondingly, left) distributivity happens -when the sum is multiplied by a number on the right (left), not when the -sum itself is the right (left) factor in the product (see planetmath.org -and mathworld.wolfram.com). In the old library BinInt, distributivity over -subtraction was named correctly, but distributivity over addition was named -incorrectly. The names in Isabelle/HOL library are also incorrect. *) - -Theorem Zmul_assoc : forall n m p : Z, n * (m * p) == (n * m) * p. -Proof NZmul_assoc. - -Theorem Zmul_1_l : forall n : Z, 1 * n == n. -Proof NZmul_1_l. - -Theorem Zmul_1_r : forall n : Z, n * 1 == n. -Proof NZmul_1_r. - -(* The following two theorems are true in an ordered ring, -but since they don't mention order, we'll put them here *) - -Theorem Zeq_mul_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0. -Proof NZeq_mul_0. - -Theorem Zneq_mul_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. -Proof NZneq_mul_0. - -(* Theorems that are either not valid on N or have different proofs on N and Z *) - -Theorem Zmul_pred_r : forall n m : Z, n * (P m) == n * m - n. -Proof. -intros n m. -rewrite <- (Zsucc_pred m) at 2. -now rewrite Zmul_succ_r, <- Zadd_minus_assoc, Zminus_diag, Zadd_0_r. -Qed. - -Theorem Zmul_pred_l : forall n m : Z, (P n) * m == n * m - m. -Proof. -intros n m; rewrite (Zmul_comm (P n) m), (Zmul_comm n m). apply Zmul_pred_r. -Qed. - -Theorem Zmul_opp_l : forall n m : Z, (- n) * m == - (n * m). -Proof. -intros n m. apply -> Zadd_move_0_r. -now rewrite <- Zmul_add_distr_r, Zadd_opp_diag_l, Zmul_0_l. -Qed. - -Theorem Zmul_opp_r : forall n m : Z, n * (- m) == - (n * m). -Proof. -intros n m; rewrite (Zmul_comm n (- m)), (Zmul_comm n m); apply Zmul_opp_l. -Qed. - -Theorem Zmul_opp_opp : forall n m : Z, (- n) * (- m) == n * m. -Proof. -intros n m; now rewrite Zmul_opp_l, Zmul_opp_r, Zopp_involutive. -Qed. - -Theorem Zmul_minus_distr_l : forall n m p : Z, n * (m - p) == n * m - n * p. -Proof. -intros n m p. do 2 rewrite <- Zadd_opp_r. rewrite Zmul_add_distr_l. -now rewrite Zmul_opp_r. -Qed. - -Theorem Zmul_minus_distr_r : forall n m p : Z, (n - m) * p == n * p - m * p. -Proof. -intros n m p; rewrite (Zmul_comm (n - m) p), (Zmul_comm n p), (Zmul_comm m p); -now apply Zmul_minus_distr_l. -Qed. - -End ZTimesPropFunct. - - diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v deleted file mode 100644 index d3f5a03963..0000000000 --- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v +++ /dev/null @@ -1,343 +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 Zmul_lt_mono_pos_l : forall p n m : Z, 0 < p -> (n < m <-> p * n < p * m). -Proof NZmul_lt_mono_pos_l. - -Theorem Zmul_lt_mono_pos_r : forall p n m : Z, 0 < p -> (n < m <-> n * p < m * p). -Proof NZmul_lt_mono_pos_r. - -Theorem Zmul_lt_mono_neg_l : forall p n m : Z, p < 0 -> (n < m <-> p * m < p * n). -Proof NZmul_lt_mono_neg_l. - -Theorem Zmul_lt_mono_neg_r : forall p n m : Z, p < 0 -> (n < m <-> m * p < n * p). -Proof NZmul_lt_mono_neg_r. - -Theorem Zmul_le_mono_nonneg_l : forall n m p : Z, 0 <= p -> n <= m -> p * n <= p * m. -Proof NZmul_le_mono_nonneg_l. - -Theorem Zmul_le_mono_nonpos_l : forall n m p : Z, p <= 0 -> n <= m -> p * m <= p * n. -Proof NZmul_le_mono_nonpos_l. - -Theorem Zmul_le_mono_nonneg_r : forall n m p : Z, 0 <= p -> n <= m -> n * p <= m * p. -Proof NZmul_le_mono_nonneg_r. - -Theorem Zmul_le_mono_nonpos_r : forall n m p : Z, p <= 0 -> n <= m -> m * p <= n * p. -Proof NZmul_le_mono_nonpos_r. - -Theorem Zmul_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m). -Proof NZmul_cancel_l. - -Theorem Zmul_cancel_r : forall n m p : Z, p ~= 0 -> (n * p == m * p <-> n == m). -Proof NZmul_cancel_r. - -Theorem Zmul_id_l : forall n m : Z, m ~= 0 -> (n * m == m <-> n == 1). -Proof NZmul_id_l. - -Theorem Zmul_id_r : forall n m : Z, n ~= 0 -> (n * m == n <-> m == 1). -Proof NZmul_id_r. - -Theorem Zmul_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m). -Proof NZmul_le_mono_pos_l. - -Theorem Zmul_le_mono_pos_r : forall n m p : Z, 0 < p -> (n <= m <-> n * p <= m * p). -Proof NZmul_le_mono_pos_r. - -Theorem Zmul_le_mono_neg_l : forall n m p : Z, p < 0 -> (n <= m <-> p * m <= p * n). -Proof NZmul_le_mono_neg_l. - -Theorem Zmul_le_mono_neg_r : forall n m p : Z, p < 0 -> (n <= m <-> m * p <= n * p). -Proof NZmul_le_mono_neg_r. - -Theorem Zmul_lt_mono_nonneg : - forall n m p q : Z, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q. -Proof NZmul_lt_mono_nonneg. - -Theorem Zmul_lt_mono_nonpos : - forall n m p q : Z, m <= 0 -> n < m -> q <= 0 -> p < q -> m * q < n * p. -Proof. -intros n m p q H1 H2 H3 H4. -apply Zle_lt_trans with (m * p). -apply Zmul_le_mono_nonpos_l; [assumption | now apply Zlt_le_incl]. -apply -> Zmul_lt_mono_neg_r; [assumption | now apply Zlt_le_trans with q]. -Qed. - -Theorem Zmul_le_mono_nonneg : - forall n m p q : Z, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q. -Proof NZmul_le_mono_nonneg. - -Theorem Zmul_le_mono_nonpos : - forall n m p q : Z, m <= 0 -> n <= m -> q <= 0 -> p <= q -> m * q <= n * p. -Proof. -intros n m p q H1 H2 H3 H4. -apply Zle_trans with (m * p). -now apply Zmul_le_mono_nonpos_l. -apply Zmul_le_mono_nonpos_r; [now apply Zle_trans with q | assumption]. -Qed. - -Theorem Zmul_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n * m. -Proof NZmul_pos_pos. - -Theorem Zmul_neg_neg : forall n m : Z, n < 0 -> m < 0 -> 0 < n * m. -Proof NZmul_neg_neg. - -Theorem Zmul_pos_neg : forall n m : Z, 0 < n -> m < 0 -> n * m < 0. -Proof NZmul_pos_neg. - -Theorem Zmul_neg_pos : forall n m : Z, n < 0 -> 0 < m -> n * m < 0. -Proof NZmul_neg_pos. - -Theorem Zmul_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m. -Proof. -intros n m H1 H2. -rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonneg_r. -Qed. - -Theorem Zmul_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m. -Proof. -intros n m H1 H2. -rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonpos_r. -Qed. - -Theorem Zmul_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0. -Proof. -intros n m H1 H2. -rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonpos_r. -Qed. - -Theorem Zmul_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0. -Proof. -intros; rewrite Zmul_comm; now apply Zmul_nonneg_nonpos. -Qed. - -Theorem Zlt_1_mul_pos : forall n m : Z, 1 < n -> 0 < m -> 1 < n * m. -Proof NZlt_1_mul_pos. - -Theorem Zeq_mul_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0. -Proof NZeq_mul_0. - -Theorem Zneq_mul_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. -Proof NZneq_mul_0. - -Theorem Zeq_square_0 : forall n : Z, n * n == 0 <-> n == 0. -Proof NZeq_square_0. - -Theorem Zeq_mul_0_l : forall n m : Z, n * m == 0 -> m ~= 0 -> n == 0. -Proof NZeq_mul_0_l. - -Theorem Zeq_mul_0_r : forall n m : Z, n * m == 0 -> n ~= 0 -> m == 0. -Proof NZeq_mul_0_r. - -Theorem Zlt_0_mul : forall n m : Z, 0 < n * m <-> 0 < n /\ 0 < m \/ m < 0 /\ n < 0. -Proof NZlt_0_mul. - -Notation Zmul_pos := Zlt_0_mul (only parsing). - -Theorem Zlt_mul_0 : - forall n m : Z, n * m < 0 <-> n < 0 /\ m > 0 \/ n > 0 /\ m < 0. -Proof. -intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]]. -destruct (Zlt_trichotomy n 0) as [H1 | [H1 | H1]]; -[| rewrite H1 in H; rewrite Zmul_0_l in H; false_hyp H Zlt_irrefl |]; -(destruct (Zlt_trichotomy m 0) as [H2 | [H2 | H2]]; -[| rewrite H2 in H; rewrite Zmul_0_r in H; false_hyp H Zlt_irrefl |]); -try (left; now split); try (right; now split). -assert (H3 : n * m > 0) by now apply Zmul_neg_neg. -elimtype False; now apply (Zlt_asymm (n * m) 0). -assert (H3 : n * m > 0) by now apply Zmul_pos_pos. -elimtype False; now apply (Zlt_asymm (n * m) 0). -now apply Zmul_neg_pos. now apply Zmul_pos_neg. -Qed. - -Notation Zmul_neg := Zlt_mul_0 (only parsing). - -Theorem Zle_0_mul : - forall n m : Z, 0 <= n * m -> 0 <= n /\ 0 <= m \/ n <= 0 /\ m <= 0. -Proof. -assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_symm). -intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R. -rewrite Zlt_0_mul, Zeq_mul_0. -pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto. -Qed. - -Notation Zmul_nonneg := Zle_0_mul (only parsing). - -Theorem Zle_mul_0 : - forall n m : Z, n * m <= 0 -> 0 <= n /\ m <= 0 \/ n <= 0 /\ 0 <= m. -Proof. -assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_symm). -intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R. -rewrite Zlt_mul_0, Zeq_mul_0. -pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto. -Qed. - -Notation Zmul_nonpos := Zle_mul_0 (only parsing). - -Theorem Zle_0_square : forall n : Z, 0 <= n * n. -Proof. -intro n; destruct (Zneg_nonneg_cases n). -apply Zlt_le_incl; now apply Zmul_neg_neg. -now apply Zmul_nonneg_nonneg. -Qed. - -Notation Zsquare_nonneg := Zle_0_square (only parsing). - -Theorem Znlt_square_0 : forall n : Z, ~ n * n < 0. -Proof. -intros n H. apply -> Zlt_nge in H. apply H. apply Zsquare_nonneg. -Qed. - -Theorem Zsquare_lt_mono_nonneg : forall n m : Z, 0 <= n -> n < m -> n * n < m * m. -Proof NZsquare_lt_mono_nonneg. - -Theorem Zsquare_lt_mono_nonpos : forall n m : Z, n <= 0 -> m < n -> n * n < m * m. -Proof. -intros n m H1 H2. now apply Zmul_lt_mono_nonpos. -Qed. - -Theorem Zsquare_le_mono_nonneg : forall n m : Z, 0 <= n -> n <= m -> n * n <= m * m. -Proof NZsquare_le_mono_nonneg. - -Theorem Zsquare_le_mono_nonpos : forall n m : Z, n <= 0 -> m <= n -> n * n <= m * m. -Proof. -intros n m H1 H2. now apply Zmul_le_mono_nonpos. -Qed. - -Theorem Zsquare_lt_simpl_nonneg : forall n m : Z, 0 <= m -> n * n < m * m -> n < m. -Proof NZsquare_lt_simpl_nonneg. - -Theorem Zsquare_le_simpl_nonneg : forall n m : Z, 0 <= m -> n * n <= m * m -> n <= m. -Proof NZsquare_le_simpl_nonneg. - -Theorem Zsquare_lt_simpl_nonpos : forall n m : Z, m <= 0 -> n * n < m * m -> m < n. -Proof. -intros n m H1 H2. destruct (Zle_gt_cases n 0). -destruct (NZlt_ge_cases m n). -assumption. assert (F : m * m <= n * n) by now apply Zsquare_le_mono_nonpos. -apply -> NZle_ngt in F. false_hyp H2 F. -now apply Zle_lt_trans with 0. -Qed. - -Theorem Zsquare_le_simpl_nonpos : forall n m : NZ, m <= 0 -> n * n <= m * m -> m <= n. -Proof. -intros n m H1 H2. destruct (NZle_gt_cases n 0). -destruct (NZle_gt_cases m n). -assumption. assert (F : m * m < n * n) by now apply Zsquare_lt_mono_nonpos. -apply -> NZlt_nge in F. false_hyp H2 F. -apply Zlt_le_incl; now apply NZle_lt_trans with 0. -Qed. - -Theorem Zmul_2_mono_l : forall n m : Z, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. -Proof NZmul_2_mono_l. - -Theorem Zlt_1_mul_neg : forall n m : Z, n < -1 -> m < 0 -> 1 < n * m. -Proof. -intros n m H1 H2. apply -> (NZmul_lt_mono_neg_r m) in H1. -apply <- Zopp_pos_neg in H2. rewrite Zmul_opp_l, Zmul_1_l in H1. -now apply Zlt_1_l with (- m). -assumption. -Qed. - -Theorem Zlt_mul_n1_neg : forall n m : Z, 1 < n -> m < 0 -> n * m < -1. -Proof. -intros n m H1 H2. apply -> (NZmul_lt_mono_neg_r m) in H1. -rewrite Zmul_1_l in H1. now apply Zlt_n1_r with m. -assumption. -Qed. - -Theorem Zlt_mul_n1_pos : forall n m : Z, n < -1 -> 0 < m -> n * m < -1. -Proof. -intros n m H1 H2. apply -> (NZmul_lt_mono_pos_r m) in H1. -rewrite Zmul_opp_l, Zmul_1_l in H1. -apply <- Zopp_neg_pos in H2. now apply Zlt_n1_r with (- m). -assumption. -Qed. - -Theorem Zlt_1_mul_l : forall n m : Z, 1 < n -> n * m < -1 \/ n * m == 0 \/ 1 < n * m. -Proof. -intros n m H; destruct (Zlt_trichotomy m 0) as [H1 | [H1 | H1]]. -left. now apply Zlt_mul_n1_neg. -right; left; now rewrite H1, Zmul_0_r. -right; right; now apply Zlt_1_mul_pos. -Qed. - -Theorem Zlt_n1_mul_r : forall n m : Z, n < -1 -> n * m < -1 \/ n * m == 0 \/ 1 < n * m. -Proof. -intros n m H; destruct (Zlt_trichotomy m 0) as [H1 | [H1 | H1]]. -right; right. now apply Zlt_1_mul_neg. -right; left; now rewrite H1, Zmul_0_r. -left. now apply Zlt_mul_n1_pos. -Qed. - -Theorem Zeq_mul_1 : forall n m : Z, n * m == 1 -> n == 1 \/ n == -1. -Proof. -assert (F : ~ 1 < -1). -intro H. -assert (H1 : -1 < 0). apply <- Zopp_neg_pos. apply Zlt_succ_diag_r. -assert (H2 : 1 < 0) by now apply Zlt_trans with (-1). false_hyp H2 Znlt_succ_diag_l. -Z0_pos_neg n. -intros m H; rewrite Zmul_0_l in H; false_hyp H Zneq_succ_diag_r. -intros n H; split; apply <- Zle_succ_l in H; le_elim H. -intros m H1; apply (Zlt_1_mul_l n m) in H. -rewrite H1 in H; destruct H as [H | [H | H]]. -false_hyp H F. false_hyp H Zneq_succ_diag_l. false_hyp H Zlt_irrefl. -intros; now left. -intros m H1; apply (Zlt_1_mul_l n m) in H. rewrite Zmul_opp_l in H1; -apply -> Zeq_opp_l in H1. rewrite H1 in H; destruct H as [H | [H | H]]. -false_hyp H Zlt_irrefl. apply -> Zeq_opp_l in H. rewrite Zopp_0 in H. -false_hyp H Zneq_succ_diag_l. false_hyp H F. -intros; right; symmetry; now apply Zopp_wd. -Qed. - -Theorem Zlt_mul_diag_l : forall n m : Z, n < 0 -> (1 < m <-> n * m < n). -Proof. -intros n m H. stepr (n * m < n * 1) by now rewrite Zmul_1_r. -now apply Zmul_lt_mono_neg_l. -Qed. - -Theorem Zlt_mul_diag_r : forall n m : Z, 0 < n -> (1 < m <-> n < n * m). -Proof. -intros n m H. stepr (n * 1 < n * m) by now rewrite Zmul_1_r. -now apply Zmul_lt_mono_pos_l. -Qed. - -Theorem Zle_mul_diag_l : forall n m : Z, n < 0 -> (1 <= m <-> n * m <= n). -Proof. -intros n m H. stepr (n * m <= n * 1) by now rewrite Zmul_1_r. -now apply Zmul_le_mono_neg_l. -Qed. - -Theorem Zle_mul_diag_r : forall n m : Z, 0 < n -> (1 <= m <-> n <= n * m). -Proof. -intros n m H. stepr (n * 1 <= n * m) by now rewrite Zmul_1_r. -now apply Zmul_le_mono_pos_l. -Qed. - -Theorem Zlt_mul_r : forall n m p : Z, 0 < n -> 1 < p -> n < m -> n < m * p. -Proof. -intros. stepl (n * 1) by now rewrite Zmul_1_r. -apply Zmul_lt_mono_nonneg. -now apply Zlt_le_incl. assumption. apply Zle_0_1. assumption. -Qed. - -End ZTimesOrderPropFunct. - diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index f547370369..947dc818e1 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -11,7 +11,7 @@ (*i $Id$ i*) Require Export BigN. -Require Import ZTimesOrder. +Require Import ZMulOrder. Require Import ZSig. Require Import ZSigZAxioms. Require Import ZMake. @@ -21,7 +21,7 @@ Module BigZ <: ZType := ZMake.Make BigN. (** Module [BigZ] implements [ZAxiomsSig] *) Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ. -Module Export BigZTimesOrderPropMod := ZTimesOrderPropFunct BigZAxiomsMod. +Module Export BigZMulOrderPropMod := ZMulOrderPropFunct BigZAxiomsMod. (** Notations about [BigZ] *) diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index acc77b3e78..0ff896367e 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -10,7 +10,7 @@ (*i $Id$ i*) -Require Import ZTimesOrder. +Require Import ZMulOrder. Require Import ZArith. Open Local Scope Z_scope. @@ -25,7 +25,7 @@ Definition NZ0 := 0. Definition NZsucc := Zsucc'. Definition NZpred := Zpred'. Definition NZadd := Zplus. -Definition NZminus := Zminus. +Definition NZsub := Zminus. Definition NZmul := Zmult. Theorem NZeq_equiv : equiv Z NZeq. @@ -54,7 +54,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. @@ -89,12 +89,12 @@ Proof. intros; do 2 rewrite <- Zsucc_succ'; apply Zplus_succ_l. Qed. -Theorem NZminus_0_r : forall n : Z, n - 0 = n. +Theorem NZsub_0_r : forall n : Z, n - 0 = n. Proof. exact Zminus_0_r. Qed. -Theorem NZminus_succ_r : forall n m : Z, n - (NZsucc m) = NZpred (n - m). +Theorem NZsub_succ_r : forall n m : Z, n - (NZsucc m) = NZpred (n - m). Proof. intros; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred'; apply Zminus_succ_r. @@ -213,11 +213,11 @@ Qed. End ZBinAxiomsMod. -Module Export ZBinTimesOrderPropMod := ZTimesOrderPropFunct ZBinAxiomsMod. +Module Export ZBinMulOrderPropMod := ZMulOrderPropFunct ZBinAxiomsMod. (** Z forms a ring *) -(*Lemma Zring : ring_theory 0 1 NZadd NZmul NZminus Zopp NZeq. +(*Lemma Zring : ring_theory 0 1 NZadd NZmul NZsub Zopp NZeq. Proof. constructor. exact Zadd_0_l. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 97a72e0875..aa027103fb 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -10,15 +10,15 @@ (*i $Id$ i*) -Require Import NMinus. (* The most complete file for natural numbers *) -Require Export ZTimesOrder. (* The most complete file for integers *) +Require Import NSub. (* The most complete file for natural numbers *) +Require Export ZMulOrder. (* The most complete file for integers *) Require Export Ring. Module ZPairsAxiomsMod (Import NAxiomsMod : NAxiomsSig) <: ZAxiomsSig. -Module Import NPropMod := NMinusPropFunct NAxiomsMod. (* Get all properties of natural numbers *) +Module Import NPropMod := NSubPropFunct NAxiomsMod. (* Get all properties of natural numbers *) (* We do not declare ring in Natural/Abstract for two reasons. First, some -of the properties proved in NPlus and NTimes are used in the new BinNat, +of the properties proved in NAdd and NMul are used in the new BinNat, and it is in turn used in Ring. Using ring in Natural/Abstract would be circular. It is possible, however, not to make BinNat dependent on Numbers/Natural and prove the properties necessary for ring from scratch @@ -62,7 +62,7 @@ canonical values. In that case, we could get rid of setoids and arrive at integers as signed natural numbers. *) Definition Zadd (n m : Z) : Z := ((fst n) + (fst m), (snd n) + (snd m)). -Definition Zminus (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst m)). +Definition Zsub (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst m)). (* Unfortunately, the elements of the pair keep increasing, even during subtraction *) @@ -81,7 +81,7 @@ Notation "x ~= y" := (~ Zeq x y) (at level 70) : IntScope. Notation "0" := Z0 : IntScope. Notation "1" := (Zsucc Z0) : IntScope. Notation "x + y" := (Zadd x y) : IntScope. -Notation "x - y" := (Zminus x y) : IntScope. +Notation "x - y" := (Zsub x y) : IntScope. Notation "x * y" := (Zmul x y) : IntScope. Notation "x < y" := (Zlt x y) : IntScope. Notation "x <= y" := (Zle x y) : IntScope. @@ -102,7 +102,7 @@ Definition NZ0 := Z0. Definition NZsucc := Zsucc. Definition NZpred := Zpred. Definition NZadd := Zadd. -Definition NZminus := Zminus. +Definition NZsub := Zsub. Definition NZmul := Zmul. Theorem ZE_refl : reflexive Z Zeq. @@ -162,9 +162,9 @@ stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring. now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring. Qed. -Add Morphism NZminus with signature Zeq ==> Zeq ==> Zeq as NZminus_wd. +Add Morphism NZsub with signature Zeq ==> Zeq ==> Zeq as NZsub_wd. Proof. -unfold Zeq, NZminus; intros n1 m1 H1 n2 m2 H2; simpl. +unfold Zeq, NZsub; intros n1 m1 H1 n2 m2 H2; simpl. symmetry in H2. assert (H3 : (fst n1 + snd m1) + (fst m2 + snd n2) == (fst m1 + snd n1) + (fst n2 + snd m2)) by now apply add_wd. @@ -243,14 +243,14 @@ Proof. intros n m; unfold NZadd, Zeq; simpl. now do 2 rewrite add_succ_l. Qed. -Theorem NZminus_0_r : forall n : Z, n - 0 == n. +Theorem NZsub_0_r : forall n : Z, n - 0 == n. Proof. -intro n; unfold NZminus, Zeq; simpl. now do 2 rewrite add_0_r. +intro n; unfold NZsub, Zeq; simpl. now do 2 rewrite add_0_r. Qed. -Theorem NZminus_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m). +Theorem NZsub_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m). Proof. -intros n m; unfold NZminus, Zeq; simpl. symmetry; now rewrite add_succ_r. +intros n m; unfold NZsub, Zeq; simpl. symmetry; now rewrite add_succ_r. Qed. Theorem NZmul_0_l : forall n : Z, 0 * n == 0. @@ -413,7 +413,7 @@ and get their properties *) Require Import NPeano. Module Export ZPairsPeanoAxiomsMod := ZPairsAxiomsMod NPeanoAxiomsMod. -Module Export ZPairsTimesOrderPropMod := ZTimesOrderPropFunct ZPairsPeanoAxiomsMod. +Module Export ZPairsMulOrderPropMod := ZMulOrderPropFunct ZPairsPeanoAxiomsMod. Open Local Scope IntScope. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index bb56e6997c..e1f04e45ad 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -42,7 +42,7 @@ Definition NZ0 := Z.zero. Definition NZsucc := Z.succ. Definition NZpred := Z.pred. Definition NZadd := Z.add. -Definition NZminus := Z.sub. +Definition NZsub := Z.sub. Definition NZmul := Z.mul. Theorem NZeq_equiv : equiv Z.t Z.eq. @@ -71,7 +71,7 @@ Proof. intros; zsimpl; f_equal; assumption. Qed. -Add Morphism NZminus with signature Z.eq ==> Z.eq ==> Z.eq as NZminus_wd. +Add Morphism NZsub with signature Z.eq ==> Z.eq ==> Z.eq as NZsub_wd. Proof. intros; zsimpl; f_equal; assumption. Qed. @@ -154,12 +154,12 @@ Proof. intros; zsimpl; auto with zarith. Qed. -Theorem NZminus_0_r : forall n, n - 0 == n. +Theorem NZsub_0_r : forall n, n - 0 == n. Proof. intros; zsimpl; auto with zarith. Qed. -Theorem NZminus_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m). +Theorem NZsub_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m). Proof. intros; zsimpl; auto with zarith. Qed. diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v new file mode 100644 index 0000000000..9c852bf908 --- /dev/null +++ b/theories/Numbers/NatInt/NZAdd.v @@ -0,0 +1,91 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* n == m. +Proof. +intros n m p; NZinduct p. +now do 2 rewrite NZadd_0_l. +intro p. do 2 rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd. +Qed. + +Theorem NZadd_cancel_r : forall n m p : NZ, n + p == m + p <-> n == m. +Proof. +intros n m p. rewrite (NZadd_comm n p); rewrite (NZadd_comm m p). +apply NZadd_cancel_l. +Qed. + +Theorem NZsub_1_r : forall n : NZ, n - 1 == P n. +Proof. +intro n; rewrite NZsub_succ_r; now rewrite NZsub_0_r. +Qed. + +End NZAddPropFunct. + diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v new file mode 100644 index 0000000000..d1caa83eeb --- /dev/null +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -0,0 +1,166 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* p + n < p + m. +Proof. +intros n m p; NZinduct p. +now do 2 rewrite NZadd_0_l. +intro p. do 2 rewrite NZadd_succ_l. now rewrite <- NZsucc_lt_mono. +Qed. + +Theorem NZadd_lt_mono_r : forall n m p : NZ, n < m <-> n + p < m + p. +Proof. +intros n m p. +rewrite (NZadd_comm n p); rewrite (NZadd_comm m p); apply NZadd_lt_mono_l. +Qed. + +Theorem NZadd_lt_mono : forall n m p q : NZ, n < m -> p < q -> n + p < m + q. +Proof. +intros n m p q H1 H2. +apply NZlt_trans with (m + p); +[now apply -> NZadd_lt_mono_r | now apply -> NZadd_lt_mono_l]. +Qed. + +Theorem NZadd_le_mono_l : forall n m p : NZ, n <= m <-> p + n <= p + m. +Proof. +intros n m p; NZinduct p. +now do 2 rewrite NZadd_0_l. +intro p. do 2 rewrite NZadd_succ_l. now rewrite <- NZsucc_le_mono. +Qed. + +Theorem NZadd_le_mono_r : forall n m p : NZ, n <= m <-> n + p <= m + p. +Proof. +intros n m p. +rewrite (NZadd_comm n p); rewrite (NZadd_comm m p); apply NZadd_le_mono_l. +Qed. + +Theorem NZadd_le_mono : forall n m p q : NZ, n <= m -> p <= q -> n + p <= m + q. +Proof. +intros n m p q H1 H2. +apply NZle_trans with (m + p); +[now apply -> NZadd_le_mono_r | now apply -> NZadd_le_mono_l]. +Qed. + +Theorem NZadd_lt_le_mono : forall n m p q : NZ, n < m -> p <= q -> n + p < m + q. +Proof. +intros n m p q H1 H2. +apply NZlt_le_trans with (m + p); +[now apply -> NZadd_lt_mono_r | now apply -> NZadd_le_mono_l]. +Qed. + +Theorem NZadd_le_lt_mono : forall n m p q : NZ, n <= m -> p < q -> n + p < m + q. +Proof. +intros n m p q H1 H2. +apply NZle_lt_trans with (m + p); +[now apply -> NZadd_le_mono_r | now apply -> NZadd_lt_mono_l]. +Qed. + +Theorem NZadd_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n + m. +Proof. +intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_lt_mono. +Qed. + +Theorem NZadd_pos_nonneg : forall n m : NZ, 0 < n -> 0 <= m -> 0 < n + m. +Proof. +intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_lt_le_mono. +Qed. + +Theorem NZadd_nonneg_pos : forall n m : NZ, 0 <= n -> 0 < m -> 0 < n + m. +Proof. +intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_le_lt_mono. +Qed. + +Theorem NZadd_nonneg_nonneg : forall n m : NZ, 0 <= n -> 0 <= m -> 0 <= n + m. +Proof. +intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_le_mono. +Qed. + +Theorem NZlt_add_pos_l : forall n m : NZ, 0 < n -> m < n + m. +Proof. +intros n m H. apply -> (NZadd_lt_mono_r 0 n m) in H. +now rewrite NZadd_0_l in H. +Qed. + +Theorem NZlt_add_pos_r : forall n m : NZ, 0 < n -> m < m + n. +Proof. +intros; rewrite NZadd_comm; now apply NZlt_add_pos_l. +Qed. + +Theorem NZle_lt_add_lt : forall n m p q : NZ, n <= m -> p + m < q + n -> p < q. +Proof. +intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption]. +pose proof (NZadd_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H2. +false_hyp H3 H2. +Qed. + +Theorem NZlt_le_add_lt : forall n m p q : NZ, n < m -> p + m <= q + n -> p < q. +Proof. +intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption]. +pose proof (NZadd_le_lt_mono q p n m H H1) as H3. apply <- NZnle_gt in H3. +false_hyp H2 H3. +Qed. + +Theorem NZle_le_add_le : forall n m p q : NZ, n <= m -> p + m <= q + n -> p <= q. +Proof. +intros n m p q H1 H2. destruct (NZle_gt_cases p q); [assumption |]. +pose proof (NZadd_lt_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H3. +false_hyp H2 H3. +Qed. + +Theorem NZadd_lt_cases : forall n m p q : NZ, n + m < p + q -> n < p \/ m < q. +Proof. +intros n m p q H; +destruct (NZle_gt_cases p n) as [H1 | H1]. +destruct (NZle_gt_cases q m) as [H2 | H2]. +pose proof (NZadd_le_mono p n q m H1 H2) as H3. apply -> NZle_ngt in H3. +false_hyp H H3. +now right. now left. +Qed. + +Theorem NZadd_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q. +Proof. +intros n m p q H. +destruct (NZle_gt_cases n p) as [H1 | H1]. now left. +destruct (NZle_gt_cases m q) as [H2 | H2]. now right. +assert (H3 : p + q < n + m) by now apply NZadd_lt_mono. +apply -> NZle_ngt in H. false_hyp H3 H. +Qed. + +Theorem NZadd_neg_cases : forall n m : NZ, n + m < 0 -> n < 0 \/ m < 0. +Proof. +intros n m H; apply NZadd_lt_cases; now rewrite NZadd_0_l. +Qed. + +Theorem NZadd_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m. +Proof. +intros n m H; apply NZadd_lt_cases; now rewrite NZadd_0_l. +Qed. + +Theorem NZadd_nonpos_cases : forall n m : NZ, n + m <= 0 -> n <= 0 \/ m <= 0. +Proof. +intros n m H; apply NZadd_le_cases; now rewrite NZadd_0_l. +Qed. + +Theorem NZadd_nonneg_cases : forall n m : NZ, 0 <= n + m -> 0 <= n \/ 0 <= m. +Proof. +intros n m H; apply NZadd_le_cases; now rewrite NZadd_0_l. +Qed. + +End NZAddOrderPropFunct. + diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 516cf5b42b..1ef7809866 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -20,11 +20,11 @@ Parameter Inline NZ0 : NZ. Parameter Inline NZsucc : NZ -> NZ. Parameter Inline NZpred : NZ -> NZ. Parameter Inline NZadd : NZ -> NZ -> NZ. -Parameter Inline NZminus : NZ -> NZ -> NZ. +Parameter Inline NZsub : NZ -> NZ -> NZ. Parameter Inline NZmul : NZ -> NZ -> NZ. -(* Unary minus (opp) is not defined on natural numbers, so we have it for -integers only *) +(* Unary subtraction (opp) is not defined on natural numbers, so we have + it for integers only *) Axiom NZeq_equiv : equiv NZ NZeq. Add Relation NZ NZeq @@ -36,7 +36,7 @@ as NZeq_rel. Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd. -Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd. Delimit Scope NatIntScope with NatInt. @@ -48,7 +48,7 @@ Notation S := NZsucc. Notation P := NZpred. Notation "1" := (S 0) : NatIntScope. Notation "x + y" := (NZadd x y) : NatIntScope. -Notation "x - y" := (NZminus x y) : NatIntScope. +Notation "x - y" := (NZsub x y) : NatIntScope. Notation "x * y" := (NZmul x y) : NatIntScope. Axiom NZpred_succ : forall n : NZ, P (S n) == n. @@ -60,8 +60,8 @@ Axiom NZinduction : Axiom NZadd_0_l : forall n : NZ, 0 + n == n. Axiom NZadd_succ_l : forall n m : NZ, (S n) + m == S (n + m). -Axiom NZminus_0_r : forall n : NZ, n - 0 == n. -Axiom NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m). +Axiom NZsub_0_r : forall n : NZ, n - 0 == n. +Axiom NZsub_succ_r : forall n m : NZ, n - (S m) == P (n - m). Axiom NZmul_0_l : forall n : NZ, 0 * n == 0. Axiom NZmul_succ_l : forall n m : NZ, S n * m == n * m + m. diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v new file mode 100644 index 0000000000..7d9b1aabd3 --- /dev/null +++ b/theories/Numbers/NatInt/NZMul.v @@ -0,0 +1,80 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (p * n < p * m <-> q * n + m < q * m + n). +Proof. +intros p q n m H. rewrite <- H. do 2 rewrite NZmul_succ_l. +rewrite <- (NZadd_assoc (p * n) n m). +rewrite <- (NZadd_assoc (p * m) m n). +rewrite (NZadd_comm n m). now rewrite <- NZadd_lt_mono_r. +Qed. + +Theorem NZmul_lt_mono_pos_l : forall p n m : NZ, 0 < p -> (n < m <-> p * n < p * m). +Proof. +NZord_induct p. +intros n m H; false_hyp H NZlt_irrefl. +intros p H IH n m H1. do 2 rewrite NZmul_succ_l. +le_elim H. assert (LR : forall n m : NZ, n < m -> p * n + n < p * m + m). +intros n1 m1 H2. apply NZadd_lt_mono; [now apply -> IH | assumption]. +split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3. +apply <- NZle_ngt in H3. le_elim H3. +apply NZlt_asymm in H2. apply H2. now apply LR. +rewrite H3 in H2; false_hyp H2 NZlt_irrefl. +rewrite <- H; do 2 rewrite NZmul_0_l; now do 2 rewrite NZadd_0_l. +intros p H1 _ n m H2. apply NZlt_asymm in H1. false_hyp H2 H1. +Qed. + +Theorem NZmul_lt_mono_pos_r : forall p n m : NZ, 0 < p -> (n < m <-> n * p < m * p). +Proof. +intros p n m. +rewrite (NZmul_comm n p); rewrite (NZmul_comm m p). now apply NZmul_lt_mono_pos_l. +Qed. + +Theorem NZmul_lt_mono_neg_l : forall p n m : NZ, p < 0 -> (n < m <-> p * m < p * n). +Proof. +NZord_induct p. +intros n m H; false_hyp H NZlt_irrefl. +intros p H1 _ n m H2. apply NZlt_succ_l in H2. apply <- NZnle_gt in H2. false_hyp H1 H2. +intros p H IH n m H1. apply <- NZle_succ_l in H. +le_elim H. assert (LR : forall n m : NZ, n < m -> p * m < p * n). +intros n1 m1 H2. apply (NZle_lt_add_lt n1 m1). +now apply NZlt_le_incl. do 2 rewrite <- NZmul_succ_l. now apply -> IH. +split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3. +apply <- NZle_ngt in H3. le_elim H3. +apply NZlt_asymm in H2. apply H2. now apply LR. +rewrite H3 in H2; false_hyp H2 NZlt_irrefl. +rewrite (NZmul_lt_pred p (S p)) by reflexivity. +rewrite H; do 2 rewrite NZmul_0_l; now do 2 rewrite NZadd_0_l. +Qed. + +Theorem NZmul_lt_mono_neg_r : forall p n m : NZ, p < 0 -> (n < m <-> m * p < n * p). +Proof. +intros p n m. +rewrite (NZmul_comm n p); rewrite (NZmul_comm m p). now apply NZmul_lt_mono_neg_l. +Qed. + +Theorem NZmul_le_mono_nonneg_l : forall n m p : NZ, 0 <= p -> n <= m -> p * n <= p * m. +Proof. +intros n m p H1 H2. le_elim H1. +le_elim H2. apply NZlt_le_incl. now apply -> NZmul_lt_mono_pos_l. +apply NZeq_le_incl; now rewrite H2. +apply NZeq_le_incl; rewrite <- H1; now do 2 rewrite NZmul_0_l. +Qed. + +Theorem NZmul_le_mono_nonpos_l : forall n m p : NZ, p <= 0 -> n <= m -> p * m <= p * n. +Proof. +intros n m p H1 H2. le_elim H1. +le_elim H2. apply NZlt_le_incl. now apply -> NZmul_lt_mono_neg_l. +apply NZeq_le_incl; now rewrite H2. +apply NZeq_le_incl; rewrite H1; now do 2 rewrite NZmul_0_l. +Qed. + +Theorem NZmul_le_mono_nonneg_r : forall n m p : NZ, 0 <= p -> n <= m -> n * p <= m * p. +Proof. +intros n m p H1 H2; rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); +now apply NZmul_le_mono_nonneg_l. +Qed. + +Theorem NZmul_le_mono_nonpos_r : forall n m p : NZ, p <= 0 -> n <= m -> m * p <= n * p. +Proof. +intros n m p H1 H2; rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); +now apply NZmul_le_mono_nonpos_l. +Qed. + +Theorem NZmul_cancel_l : forall n m p : NZ, p ~= 0 -> (p * n == p * m <-> n == m). +Proof. +intros n m p H; split; intro H1. +destruct (NZlt_trichotomy p 0) as [H2 | [H2 | H2]]. +apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3]. +assert (H4 : p * m < p * n); [now apply -> NZmul_lt_mono_neg_l |]. +rewrite H1 in H4; false_hyp H4 NZlt_irrefl. +assert (H4 : p * n < p * m); [now apply -> NZmul_lt_mono_neg_l |]. +rewrite H1 in H4; false_hyp H4 NZlt_irrefl. +false_hyp H2 H. +apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3]. +assert (H4 : p * n < p * m) by (now apply -> NZmul_lt_mono_pos_l). +rewrite H1 in H4; false_hyp H4 NZlt_irrefl. +assert (H4 : p * m < p * n) by (now apply -> NZmul_lt_mono_pos_l). +rewrite H1 in H4; false_hyp H4 NZlt_irrefl. +now rewrite H1. +Qed. + +Theorem NZmul_cancel_r : forall n m p : NZ, p ~= 0 -> (n * p == m * p <-> n == m). +Proof. +intros n m p. rewrite (NZmul_comm n p), (NZmul_comm m p); apply NZmul_cancel_l. +Qed. + +Theorem NZmul_id_l : forall n m : NZ, m ~= 0 -> (n * m == m <-> n == 1). +Proof. +intros n m H. +stepl (n * m == 1 * m) by now rewrite NZmul_1_l. now apply NZmul_cancel_r. +Qed. + +Theorem NZmul_id_r : forall n m : NZ, n ~= 0 -> (n * m == n <-> m == 1). +Proof. +intros n m; rewrite NZmul_comm; apply NZmul_id_l. +Qed. + +Theorem NZmul_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m). +Proof. +intros n m p H; do 2 rewrite NZlt_eq_cases. +rewrite (NZmul_lt_mono_pos_l p n m) by assumption. +now rewrite -> (NZmul_cancel_l n m p) by +(intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl). +Qed. + +Theorem NZmul_le_mono_pos_r : forall n m p : NZ, 0 < p -> (n <= m <-> n * p <= m * p). +Proof. +intros n m p. rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); +apply NZmul_le_mono_pos_l. +Qed. + +Theorem NZmul_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n). +Proof. +intros n m p H; do 2 rewrite NZlt_eq_cases. +rewrite (NZmul_lt_mono_neg_l p n m); [| assumption]. +rewrite -> (NZmul_cancel_l m n p) by (intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl). +now setoid_replace (n == m) with (m == n) using relation iff by (split; now intro). +Qed. + +Theorem NZmul_le_mono_neg_r : forall n m p : NZ, p < 0 -> (n <= m <-> m * p <= n * p). +Proof. +intros n m p. rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); +apply NZmul_le_mono_neg_l. +Qed. + +Theorem NZmul_lt_mono_nonneg : + forall n m p q : NZ, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q. +Proof. +intros n m p q H1 H2 H3 H4. +apply NZle_lt_trans with (m * p). +apply NZmul_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl]. +apply -> NZmul_lt_mono_pos_l; [assumption | now apply NZle_lt_trans with n]. +Qed. + +(* There are still many variants of the theorem above. One can assume 0 < n +or 0 < p or n <= m or p <= q. *) + +Theorem NZmul_le_mono_nonneg : + forall n m p q : NZ, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q. +Proof. +intros n m p q H1 H2 H3 H4. +le_elim H2; le_elim H4. +apply NZlt_le_incl; now apply NZmul_lt_mono_nonneg. +rewrite <- H4; apply NZmul_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl]. +rewrite <- H2; apply NZmul_le_mono_nonneg_l; [assumption | now apply NZlt_le_incl]. +rewrite H2; rewrite H4; now apply NZeq_le_incl. +Qed. + +Theorem NZmul_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n * m. +Proof. +intros n m H1 H2. +rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_pos_r. +Qed. + +Theorem NZmul_neg_neg : forall n m : NZ, n < 0 -> m < 0 -> 0 < n * m. +Proof. +intros n m H1 H2. +rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_neg_r. +Qed. + +Theorem NZmul_pos_neg : forall n m : NZ, 0 < n -> m < 0 -> n * m < 0. +Proof. +intros n m H1 H2. +rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_neg_r. +Qed. + +Theorem NZmul_neg_pos : forall n m : NZ, n < 0 -> 0 < m -> n * m < 0. +Proof. +intros; rewrite NZmul_comm; now apply NZmul_pos_neg. +Qed. + +Theorem NZlt_1_mul_pos : forall n m : NZ, 1 < n -> 0 < m -> 1 < n * m. +Proof. +intros n m H1 H2. apply -> (NZmul_lt_mono_pos_r m) in H1. +rewrite NZmul_1_l in H1. now apply NZlt_1_l with m. +assumption. +Qed. + +Theorem NZeq_mul_0 : forall n m : NZ, n * m == 0 <-> n == 0 \/ m == 0. +Proof. +intros n m; split. +intro H; destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; +destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]]; +try (now right); try (now left). +elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZmul_neg_neg |]. +elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZmul_neg_pos |]. +elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZmul_pos_neg |]. +elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZmul_pos_pos |]. +intros [H | H]. now rewrite H, NZmul_0_l. now rewrite H, NZmul_0_r. +Qed. + +Theorem NZneq_mul_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Proof. +intros n m; split; intro H. +intro H1; apply -> NZeq_mul_0 in H1. tauto. +split; intro H1; rewrite H1 in H; +(rewrite NZmul_0_l in H || rewrite NZmul_0_r in H); now apply H. +Qed. + +Theorem NZeq_square_0 : forall n : NZ, n * n == 0 <-> n == 0. +Proof. +intro n; rewrite NZeq_mul_0; tauto. +Qed. + +Theorem NZeq_mul_0_l : forall n m : NZ, n * m == 0 -> m ~= 0 -> n == 0. +Proof. +intros n m H1 H2. apply -> NZeq_mul_0 in H1. destruct H1 as [H1 | H1]. +assumption. false_hyp H1 H2. +Qed. + +Theorem NZeq_mul_0_r : forall n m : NZ, n * m == 0 -> n ~= 0 -> m == 0. +Proof. +intros n m H1 H2; apply -> NZeq_mul_0 in H1. destruct H1 as [H1 | H1]. +false_hyp H1 H2. assumption. +Qed. + +Theorem NZlt_0_mul : forall n m : NZ, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0). +Proof. +intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]]. +destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; +[| rewrite H1 in H; rewrite NZmul_0_l in H; false_hyp H NZlt_irrefl |]; +(destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]]; +[| rewrite H2 in H; rewrite NZmul_0_r in H; false_hyp H NZlt_irrefl |]); +try (left; now split); try (right; now split). +assert (H3 : n * m < 0) by now apply NZmul_neg_pos. +elimtype False; now apply (NZlt_asymm (n * m) 0). +assert (H3 : n * m < 0) by now apply NZmul_pos_neg. +elimtype False; now apply (NZlt_asymm (n * m) 0). +now apply NZmul_pos_pos. now apply NZmul_neg_neg. +Qed. + +Theorem NZsquare_lt_mono_nonneg : forall n m : NZ, 0 <= n -> n < m -> n * n < m * m. +Proof. +intros n m H1 H2. now apply NZmul_lt_mono_nonneg. +Qed. + +Theorem NZsquare_le_mono_nonneg : forall n m : NZ, 0 <= n -> n <= m -> n * n <= m * m. +Proof. +intros n m H1 H2. now apply NZmul_le_mono_nonneg. +Qed. + +(* The converse theorems require nonnegativity (or nonpositivity) of the +other variable *) + +Theorem NZsquare_lt_simpl_nonneg : forall n m : NZ, 0 <= m -> n * n < m * m -> n < m. +Proof. +intros n m H1 H2. destruct (NZlt_ge_cases n 0). +now apply NZlt_le_trans with 0. +destruct (NZlt_ge_cases n m). +assumption. assert (F : m * m <= n * n) by now apply NZsquare_le_mono_nonneg. +apply -> NZle_ngt in F. false_hyp H2 F. +Qed. + +Theorem NZsquare_le_simpl_nonneg : forall n m : NZ, 0 <= m -> n * n <= m * m -> n <= m. +Proof. +intros n m H1 H2. destruct (NZlt_ge_cases n 0). +apply NZlt_le_incl; now apply NZlt_le_trans with 0. +destruct (NZle_gt_cases n m). +assumption. assert (F : m * m < n * n) by now apply NZsquare_lt_mono_nonneg. +apply -> NZlt_nge in F. false_hyp H2 F. +Qed. + +Theorem NZmul_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Proof. +intros n m H. apply <- NZle_succ_l in H. +apply -> (NZmul_le_mono_pos_l (S n) m (1 + 1)) in H. +repeat rewrite NZmul_add_distr_r in *; repeat rewrite NZmul_1_l in *. +repeat rewrite NZadd_succ_r in *. repeat rewrite NZadd_succ_l in *. rewrite NZadd_0_l. +now apply -> NZle_succ_l. +apply NZadd_pos_pos; now apply NZlt_succ_diag_r. +Qed. + +End NZMulOrderPropFunct. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index f76fa94808..d8eaeb99c2 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -11,11 +11,11 @@ (*i $Id$ i*) Require Import NZAxioms. -Require Import NZTimes. +Require Import NZMul. Require Import Decidable. Module NZOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig). -Module Export NZTimesPropMod := NZTimesPropFunct NZAxiomsMod. +Module Export NZMulPropMod := NZMulPropFunct NZAxiomsMod. Open Local Scope NatIntScope. Ltac le_elim H := rewrite NZlt_eq_cases in H; destruct H as [H | H]. diff --git a/theories/Numbers/NatInt/NZPlus.v b/theories/Numbers/NatInt/NZPlus.v deleted file mode 100644 index 6fb72ed4a9..0000000000 --- a/theories/Numbers/NatInt/NZPlus.v +++ /dev/null @@ -1,91 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* n == m. -Proof. -intros n m p; NZinduct p. -now do 2 rewrite NZadd_0_l. -intro p. do 2 rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd. -Qed. - -Theorem NZadd_cancel_r : forall n m p : NZ, n + p == m + p <-> n == m. -Proof. -intros n m p. rewrite (NZadd_comm n p); rewrite (NZadd_comm m p). -apply NZadd_cancel_l. -Qed. - -Theorem NZminus_1_r : forall n : NZ, n - 1 == P n. -Proof. -intro n; rewrite NZminus_succ_r; now rewrite NZminus_0_r. -Qed. - -End NZPlusPropFunct. - diff --git a/theories/Numbers/NatInt/NZPlusOrder.v b/theories/Numbers/NatInt/NZPlusOrder.v deleted file mode 100644 index 00d178c0d9..0000000000 --- a/theories/Numbers/NatInt/NZPlusOrder.v +++ /dev/null @@ -1,166 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* p + n < p + m. -Proof. -intros n m p; NZinduct p. -now do 2 rewrite NZadd_0_l. -intro p. do 2 rewrite NZadd_succ_l. now rewrite <- NZsucc_lt_mono. -Qed. - -Theorem NZadd_lt_mono_r : forall n m p : NZ, n < m <-> n + p < m + p. -Proof. -intros n m p. -rewrite (NZadd_comm n p); rewrite (NZadd_comm m p); apply NZadd_lt_mono_l. -Qed. - -Theorem NZadd_lt_mono : forall n m p q : NZ, n < m -> p < q -> n + p < m + q. -Proof. -intros n m p q H1 H2. -apply NZlt_trans with (m + p); -[now apply -> NZadd_lt_mono_r | now apply -> NZadd_lt_mono_l]. -Qed. - -Theorem NZadd_le_mono_l : forall n m p : NZ, n <= m <-> p + n <= p + m. -Proof. -intros n m p; NZinduct p. -now do 2 rewrite NZadd_0_l. -intro p. do 2 rewrite NZadd_succ_l. now rewrite <- NZsucc_le_mono. -Qed. - -Theorem NZadd_le_mono_r : forall n m p : NZ, n <= m <-> n + p <= m + p. -Proof. -intros n m p. -rewrite (NZadd_comm n p); rewrite (NZadd_comm m p); apply NZadd_le_mono_l. -Qed. - -Theorem NZadd_le_mono : forall n m p q : NZ, n <= m -> p <= q -> n + p <= m + q. -Proof. -intros n m p q H1 H2. -apply NZle_trans with (m + p); -[now apply -> NZadd_le_mono_r | now apply -> NZadd_le_mono_l]. -Qed. - -Theorem NZadd_lt_le_mono : forall n m p q : NZ, n < m -> p <= q -> n + p < m + q. -Proof. -intros n m p q H1 H2. -apply NZlt_le_trans with (m + p); -[now apply -> NZadd_lt_mono_r | now apply -> NZadd_le_mono_l]. -Qed. - -Theorem NZadd_le_lt_mono : forall n m p q : NZ, n <= m -> p < q -> n + p < m + q. -Proof. -intros n m p q H1 H2. -apply NZle_lt_trans with (m + p); -[now apply -> NZadd_le_mono_r | now apply -> NZadd_lt_mono_l]. -Qed. - -Theorem NZadd_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n + m. -Proof. -intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_lt_mono. -Qed. - -Theorem NZadd_pos_nonneg : forall n m : NZ, 0 < n -> 0 <= m -> 0 < n + m. -Proof. -intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_lt_le_mono. -Qed. - -Theorem NZadd_nonneg_pos : forall n m : NZ, 0 <= n -> 0 < m -> 0 < n + m. -Proof. -intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_le_lt_mono. -Qed. - -Theorem NZadd_nonneg_nonneg : forall n m : NZ, 0 <= n -> 0 <= m -> 0 <= n + m. -Proof. -intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_le_mono. -Qed. - -Theorem NZlt_add_pos_l : forall n m : NZ, 0 < n -> m < n + m. -Proof. -intros n m H. apply -> (NZadd_lt_mono_r 0 n m) in H. -now rewrite NZadd_0_l in H. -Qed. - -Theorem NZlt_add_pos_r : forall n m : NZ, 0 < n -> m < m + n. -Proof. -intros; rewrite NZadd_comm; now apply NZlt_add_pos_l. -Qed. - -Theorem NZle_lt_add_lt : forall n m p q : NZ, n <= m -> p + m < q + n -> p < q. -Proof. -intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption]. -pose proof (NZadd_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H2. -false_hyp H3 H2. -Qed. - -Theorem NZlt_le_add_lt : forall n m p q : NZ, n < m -> p + m <= q + n -> p < q. -Proof. -intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption]. -pose proof (NZadd_le_lt_mono q p n m H H1) as H3. apply <- NZnle_gt in H3. -false_hyp H2 H3. -Qed. - -Theorem NZle_le_add_le : forall n m p q : NZ, n <= m -> p + m <= q + n -> p <= q. -Proof. -intros n m p q H1 H2. destruct (NZle_gt_cases p q); [assumption |]. -pose proof (NZadd_lt_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H3. -false_hyp H2 H3. -Qed. - -Theorem NZadd_lt_cases : forall n m p q : NZ, n + m < p + q -> n < p \/ m < q. -Proof. -intros n m p q H; -destruct (NZle_gt_cases p n) as [H1 | H1]. -destruct (NZle_gt_cases q m) as [H2 | H2]. -pose proof (NZadd_le_mono p n q m H1 H2) as H3. apply -> NZle_ngt in H3. -false_hyp H H3. -now right. now left. -Qed. - -Theorem NZadd_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q. -Proof. -intros n m p q H. -destruct (NZle_gt_cases n p) as [H1 | H1]. now left. -destruct (NZle_gt_cases m q) as [H2 | H2]. now right. -assert (H3 : p + q < n + m) by now apply NZadd_lt_mono. -apply -> NZle_ngt in H. false_hyp H3 H. -Qed. - -Theorem NZadd_neg_cases : forall n m : NZ, n + m < 0 -> n < 0 \/ m < 0. -Proof. -intros n m H; apply NZadd_lt_cases; now rewrite NZadd_0_l. -Qed. - -Theorem NZadd_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m. -Proof. -intros n m H; apply NZadd_lt_cases; now rewrite NZadd_0_l. -Qed. - -Theorem NZadd_nonpos_cases : forall n m : NZ, n + m <= 0 -> n <= 0 \/ m <= 0. -Proof. -intros n m H; apply NZadd_le_cases; now rewrite NZadd_0_l. -Qed. - -Theorem NZadd_nonneg_cases : forall n m : NZ, 0 <= n + m -> 0 <= n \/ 0 <= m. -Proof. -intros n m H; apply NZadd_le_cases; now rewrite NZadd_0_l. -Qed. - -End NZPlusOrderPropFunct. - diff --git a/theories/Numbers/NatInt/NZTimes.v b/theories/Numbers/NatInt/NZTimes.v deleted file mode 100644 index 9f93e0a1bf..0000000000 --- a/theories/Numbers/NatInt/NZTimes.v +++ /dev/null @@ -1,80 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (p * n < p * m <-> q * n + m < q * m + n). -Proof. -intros p q n m H. rewrite <- H. do 2 rewrite NZmul_succ_l. -rewrite <- (NZadd_assoc (p * n) n m). -rewrite <- (NZadd_assoc (p * m) m n). -rewrite (NZadd_comm n m). now rewrite <- NZadd_lt_mono_r. -Qed. - -Theorem NZmul_lt_mono_pos_l : forall p n m : NZ, 0 < p -> (n < m <-> p * n < p * m). -Proof. -NZord_induct p. -intros n m H; false_hyp H NZlt_irrefl. -intros p H IH n m H1. do 2 rewrite NZmul_succ_l. -le_elim H. assert (LR : forall n m : NZ, n < m -> p * n + n < p * m + m). -intros n1 m1 H2. apply NZadd_lt_mono; [now apply -> IH | assumption]. -split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3. -apply <- NZle_ngt in H3. le_elim H3. -apply NZlt_asymm in H2. apply H2. now apply LR. -rewrite H3 in H2; false_hyp H2 NZlt_irrefl. -rewrite <- H; do 2 rewrite NZmul_0_l; now do 2 rewrite NZadd_0_l. -intros p H1 _ n m H2. apply NZlt_asymm in H1. false_hyp H2 H1. -Qed. - -Theorem NZmul_lt_mono_pos_r : forall p n m : NZ, 0 < p -> (n < m <-> n * p < m * p). -Proof. -intros p n m. -rewrite (NZmul_comm n p); rewrite (NZmul_comm m p). now apply NZmul_lt_mono_pos_l. -Qed. - -Theorem NZmul_lt_mono_neg_l : forall p n m : NZ, p < 0 -> (n < m <-> p * m < p * n). -Proof. -NZord_induct p. -intros n m H; false_hyp H NZlt_irrefl. -intros p H1 _ n m H2. apply NZlt_succ_l in H2. apply <- NZnle_gt in H2. false_hyp H1 H2. -intros p H IH n m H1. apply <- NZle_succ_l in H. -le_elim H. assert (LR : forall n m : NZ, n < m -> p * m < p * n). -intros n1 m1 H2. apply (NZle_lt_add_lt n1 m1). -now apply NZlt_le_incl. do 2 rewrite <- NZmul_succ_l. now apply -> IH. -split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3. -apply <- NZle_ngt in H3. le_elim H3. -apply NZlt_asymm in H2. apply H2. now apply LR. -rewrite H3 in H2; false_hyp H2 NZlt_irrefl. -rewrite (NZmul_lt_pred p (S p)) by reflexivity. -rewrite H; do 2 rewrite NZmul_0_l; now do 2 rewrite NZadd_0_l. -Qed. - -Theorem NZmul_lt_mono_neg_r : forall p n m : NZ, p < 0 -> (n < m <-> m * p < n * p). -Proof. -intros p n m. -rewrite (NZmul_comm n p); rewrite (NZmul_comm m p). now apply NZmul_lt_mono_neg_l. -Qed. - -Theorem NZmul_le_mono_nonneg_l : forall n m p : NZ, 0 <= p -> n <= m -> p * n <= p * m. -Proof. -intros n m p H1 H2. le_elim H1. -le_elim H2. apply NZlt_le_incl. now apply -> NZmul_lt_mono_pos_l. -apply NZeq_le_incl; now rewrite H2. -apply NZeq_le_incl; rewrite <- H1; now do 2 rewrite NZmul_0_l. -Qed. - -Theorem NZmul_le_mono_nonpos_l : forall n m p : NZ, p <= 0 -> n <= m -> p * m <= p * n. -Proof. -intros n m p H1 H2. le_elim H1. -le_elim H2. apply NZlt_le_incl. now apply -> NZmul_lt_mono_neg_l. -apply NZeq_le_incl; now rewrite H2. -apply NZeq_le_incl; rewrite H1; now do 2 rewrite NZmul_0_l. -Qed. - -Theorem NZmul_le_mono_nonneg_r : forall n m p : NZ, 0 <= p -> n <= m -> n * p <= m * p. -Proof. -intros n m p H1 H2; rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); -now apply NZmul_le_mono_nonneg_l. -Qed. - -Theorem NZmul_le_mono_nonpos_r : forall n m p : NZ, p <= 0 -> n <= m -> m * p <= n * p. -Proof. -intros n m p H1 H2; rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); -now apply NZmul_le_mono_nonpos_l. -Qed. - -Theorem NZmul_cancel_l : forall n m p : NZ, p ~= 0 -> (p * n == p * m <-> n == m). -Proof. -intros n m p H; split; intro H1. -destruct (NZlt_trichotomy p 0) as [H2 | [H2 | H2]]. -apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3]. -assert (H4 : p * m < p * n); [now apply -> NZmul_lt_mono_neg_l |]. -rewrite H1 in H4; false_hyp H4 NZlt_irrefl. -assert (H4 : p * n < p * m); [now apply -> NZmul_lt_mono_neg_l |]. -rewrite H1 in H4; false_hyp H4 NZlt_irrefl. -false_hyp H2 H. -apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3]. -assert (H4 : p * n < p * m) by (now apply -> NZmul_lt_mono_pos_l). -rewrite H1 in H4; false_hyp H4 NZlt_irrefl. -assert (H4 : p * m < p * n) by (now apply -> NZmul_lt_mono_pos_l). -rewrite H1 in H4; false_hyp H4 NZlt_irrefl. -now rewrite H1. -Qed. - -Theorem NZmul_cancel_r : forall n m p : NZ, p ~= 0 -> (n * p == m * p <-> n == m). -Proof. -intros n m p. rewrite (NZmul_comm n p), (NZmul_comm m p); apply NZmul_cancel_l. -Qed. - -Theorem NZmul_id_l : forall n m : NZ, m ~= 0 -> (n * m == m <-> n == 1). -Proof. -intros n m H. -stepl (n * m == 1 * m) by now rewrite NZmul_1_l. now apply NZmul_cancel_r. -Qed. - -Theorem NZmul_id_r : forall n m : NZ, n ~= 0 -> (n * m == n <-> m == 1). -Proof. -intros n m; rewrite NZmul_comm; apply NZmul_id_l. -Qed. - -Theorem NZmul_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m). -Proof. -intros n m p H; do 2 rewrite NZlt_eq_cases. -rewrite (NZmul_lt_mono_pos_l p n m) by assumption. -now rewrite -> (NZmul_cancel_l n m p) by -(intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl). -Qed. - -Theorem NZmul_le_mono_pos_r : forall n m p : NZ, 0 < p -> (n <= m <-> n * p <= m * p). -Proof. -intros n m p. rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); -apply NZmul_le_mono_pos_l. -Qed. - -Theorem NZmul_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n). -Proof. -intros n m p H; do 2 rewrite NZlt_eq_cases. -rewrite (NZmul_lt_mono_neg_l p n m); [| assumption]. -rewrite -> (NZmul_cancel_l m n p) by (intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl). -now setoid_replace (n == m) with (m == n) using relation iff by (split; now intro). -Qed. - -Theorem NZmul_le_mono_neg_r : forall n m p : NZ, p < 0 -> (n <= m <-> m * p <= n * p). -Proof. -intros n m p. rewrite (NZmul_comm n p); rewrite (NZmul_comm m p); -apply NZmul_le_mono_neg_l. -Qed. - -Theorem NZmul_lt_mono_nonneg : - forall n m p q : NZ, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q. -Proof. -intros n m p q H1 H2 H3 H4. -apply NZle_lt_trans with (m * p). -apply NZmul_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl]. -apply -> NZmul_lt_mono_pos_l; [assumption | now apply NZle_lt_trans with n]. -Qed. - -(* There are still many variants of the theorem above. One can assume 0 < n -or 0 < p or n <= m or p <= q. *) - -Theorem NZmul_le_mono_nonneg : - forall n m p q : NZ, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q. -Proof. -intros n m p q H1 H2 H3 H4. -le_elim H2; le_elim H4. -apply NZlt_le_incl; now apply NZmul_lt_mono_nonneg. -rewrite <- H4; apply NZmul_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl]. -rewrite <- H2; apply NZmul_le_mono_nonneg_l; [assumption | now apply NZlt_le_incl]. -rewrite H2; rewrite H4; now apply NZeq_le_incl. -Qed. - -Theorem NZmul_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n * m. -Proof. -intros n m H1 H2. -rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_pos_r. -Qed. - -Theorem NZmul_neg_neg : forall n m : NZ, n < 0 -> m < 0 -> 0 < n * m. -Proof. -intros n m H1 H2. -rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_neg_r. -Qed. - -Theorem NZmul_pos_neg : forall n m : NZ, 0 < n -> m < 0 -> n * m < 0. -Proof. -intros n m H1 H2. -rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_neg_r. -Qed. - -Theorem NZmul_neg_pos : forall n m : NZ, n < 0 -> 0 < m -> n * m < 0. -Proof. -intros; rewrite NZmul_comm; now apply NZmul_pos_neg. -Qed. - -Theorem NZlt_1_mul_pos : forall n m : NZ, 1 < n -> 0 < m -> 1 < n * m. -Proof. -intros n m H1 H2. apply -> (NZmul_lt_mono_pos_r m) in H1. -rewrite NZmul_1_l in H1. now apply NZlt_1_l with m. -assumption. -Qed. - -Theorem NZeq_mul_0 : forall n m : NZ, n * m == 0 <-> n == 0 \/ m == 0. -Proof. -intros n m; split. -intro H; destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; -destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]]; -try (now right); try (now left). -elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZmul_neg_neg |]. -elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZmul_neg_pos |]. -elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZmul_pos_neg |]. -elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZmul_pos_pos |]. -intros [H | H]. now rewrite H, NZmul_0_l. now rewrite H, NZmul_0_r. -Qed. - -Theorem NZneq_mul_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. -Proof. -intros n m; split; intro H. -intro H1; apply -> NZeq_mul_0 in H1. tauto. -split; intro H1; rewrite H1 in H; -(rewrite NZmul_0_l in H || rewrite NZmul_0_r in H); now apply H. -Qed. - -Theorem NZeq_square_0 : forall n : NZ, n * n == 0 <-> n == 0. -Proof. -intro n; rewrite NZeq_mul_0; tauto. -Qed. - -Theorem NZeq_mul_0_l : forall n m : NZ, n * m == 0 -> m ~= 0 -> n == 0. -Proof. -intros n m H1 H2. apply -> NZeq_mul_0 in H1. destruct H1 as [H1 | H1]. -assumption. false_hyp H1 H2. -Qed. - -Theorem NZeq_mul_0_r : forall n m : NZ, n * m == 0 -> n ~= 0 -> m == 0. -Proof. -intros n m H1 H2; apply -> NZeq_mul_0 in H1. destruct H1 as [H1 | H1]. -false_hyp H1 H2. assumption. -Qed. - -Theorem NZlt_0_mul : forall n m : NZ, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0). -Proof. -intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]]. -destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; -[| rewrite H1 in H; rewrite NZmul_0_l in H; false_hyp H NZlt_irrefl |]; -(destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]]; -[| rewrite H2 in H; rewrite NZmul_0_r in H; false_hyp H NZlt_irrefl |]); -try (left; now split); try (right; now split). -assert (H3 : n * m < 0) by now apply NZmul_neg_pos. -elimtype False; now apply (NZlt_asymm (n * m) 0). -assert (H3 : n * m < 0) by now apply NZmul_pos_neg. -elimtype False; now apply (NZlt_asymm (n * m) 0). -now apply NZmul_pos_pos. now apply NZmul_neg_neg. -Qed. - -Theorem NZsquare_lt_mono_nonneg : forall n m : NZ, 0 <= n -> n < m -> n * n < m * m. -Proof. -intros n m H1 H2. now apply NZmul_lt_mono_nonneg. -Qed. - -Theorem NZsquare_le_mono_nonneg : forall n m : NZ, 0 <= n -> n <= m -> n * n <= m * m. -Proof. -intros n m H1 H2. now apply NZmul_le_mono_nonneg. -Qed. - -(* The converse theorems require nonnegativity (or nonpositivity) of the -other variable *) - -Theorem NZsquare_lt_simpl_nonneg : forall n m : NZ, 0 <= m -> n * n < m * m -> n < m. -Proof. -intros n m H1 H2. destruct (NZlt_ge_cases n 0). -now apply NZlt_le_trans with 0. -destruct (NZlt_ge_cases n m). -assumption. assert (F : m * m <= n * n) by now apply NZsquare_le_mono_nonneg. -apply -> NZle_ngt in F. false_hyp H2 F. -Qed. - -Theorem NZsquare_le_simpl_nonneg : forall n m : NZ, 0 <= m -> n * n <= m * m -> n <= m. -Proof. -intros n m H1 H2. destruct (NZlt_ge_cases n 0). -apply NZlt_le_incl; now apply NZlt_le_trans with 0. -destruct (NZle_gt_cases n m). -assumption. assert (F : m * m < n * n) by now apply NZsquare_lt_mono_nonneg. -apply -> NZlt_nge in F. false_hyp H2 F. -Qed. - -Theorem NZmul_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. -Proof. -intros n m H. apply <- NZle_succ_l in H. -apply -> (NZmul_le_mono_pos_l (S n) m (1 + 1)) in H. -repeat rewrite NZmul_add_distr_r in *; repeat rewrite NZmul_1_l in *. -repeat rewrite NZadd_succ_r in *. repeat rewrite NZadd_succ_l in *. rewrite NZadd_0_l. -now apply -> NZle_succ_l. -apply NZadd_pos_pos; now apply NZlt_succ_diag_r. -Qed. - -End NZTimesOrderPropFunct. 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