diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZMul.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZMul.v | 105 |
1 files changed, 31 insertions, 74 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v index c48d1b4c..84d840ad 100644 --- a/theories/Numbers/Integer/Abstract/ZMul.v +++ b/theories/Numbers/Integer/Abstract/ZMul.v @@ -8,106 +8,63 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: ZMul.v 11040 2008-06-03 00:04:16Z letouzey $ i*) +(*i $Id$ i*) Require Export ZAdd. -Module ZMulPropFunct (Import ZAxiomsMod : ZAxiomsSig). -Module Export ZAddPropMod := ZAddPropFunct ZAxiomsMod. -Open Local Scope IntScope. +Module ZMulPropFunct (Import Z : ZAxiomsSig'). +Include ZAddPropFunct Z. -Theorem Zmul_wd : - forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 * m1 == n2 * m2. -Proof NZmul_wd. +(** 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_0_l : forall n : Z, 0 * n == 0. -Proof NZmul_0_l. +(** Theorems that are either not valid on N or have different proofs + on N and Z *) -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. +Theorem mul_pred_r : forall n m, 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. +rewrite <- (succ_pred m) at 2. +now rewrite mul_succ_r, <- add_sub_assoc, sub_diag, add_0_r. Qed. -Theorem Zmul_pred_l : forall n m : Z, (P n) * m == n * m - m. +Theorem mul_pred_l : forall n m, (P n) * m == n * m - m. Proof. -intros n m; rewrite (Zmul_comm (P n) m), (Zmul_comm n m). apply Zmul_pred_r. +intros n m; rewrite (mul_comm (P n) m), (mul_comm n m). apply mul_pred_r. Qed. -Theorem Zmul_opp_l : forall n m : Z, (- n) * m == - (n * m). +Theorem mul_opp_l : forall n m, (- 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. +intros n m. apply -> add_move_0_r. +now rewrite <- mul_add_distr_r, add_opp_diag_l, mul_0_l. Qed. -Theorem Zmul_opp_r : forall n m : Z, n * (- m) == - (n * m). +Theorem mul_opp_r : forall n m, n * (- m) == - (n * m). Proof. -intros n m; rewrite (Zmul_comm n (- m)), (Zmul_comm n m); apply Zmul_opp_l. +intros n m; rewrite (mul_comm n (- m)), (mul_comm n m); apply mul_opp_l. Qed. -Theorem Zmul_opp_opp : forall n m : Z, (- n) * (- m) == n * m. +Theorem mul_opp_opp : forall n m, (- n) * (- m) == n * m. Proof. -intros n m; now rewrite Zmul_opp_l, Zmul_opp_r, Zopp_involutive. +intros n m; now rewrite mul_opp_l, mul_opp_r, opp_involutive. Qed. -Theorem Zmul_sub_distr_l : forall n m p : Z, n * (m - p) == n * m - n * p. +Theorem mul_sub_distr_l : forall n m p, 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. +intros n m p. do 2 rewrite <- add_opp_r. rewrite mul_add_distr_l. +now rewrite mul_opp_r. Qed. -Theorem Zmul_sub_distr_r : forall n m p : Z, (n - m) * p == n * p - m * p. +Theorem mul_sub_distr_r : forall n m p, (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. +intros n m p; rewrite (mul_comm (n - m) p), (mul_comm n p), (mul_comm m p); +now apply mul_sub_distr_l. Qed. End ZMulPropFunct. |