summaryrefslogtreecommitdiff
path: root/theories/Arith/Mult.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Arith/Mult.v')
-rw-r--r--theories/Arith/Mult.v201
1 files changed, 62 insertions, 139 deletions
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 588afde3..2d82920b 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -1,220 +1,144 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-Require Export Plus.
-Require Export Minus.
-Require Export Lt.
-Require Export Le.
+(** * Properties of multiplication.
-Local Open Scope nat_scope.
+ This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead.
+
+ [Nat.mul] is defined in [Init/Nat.v].
+*)
-Implicit Types m n p : nat.
+Require Import PeanoNat.
+(** For Compatibility: *)
+Require Export Plus Minus Le Lt.
-(** Theorems about multiplication in [nat]. [mult] is defined in module [Init/Peano.v]. *)
+Local Open Scope nat_scope.
(** * [nat] is a semi-ring *)
(** ** Zero property *)
-Lemma mult_0_r : forall n, n * 0 = 0.
-Proof.
- intro; symmetry ; apply mult_n_O.
-Qed.
-
-Lemma mult_0_l : forall n, 0 * n = 0.
-Proof.
- reflexivity.
-Qed.
+Notation mult_0_l := Nat.mul_0_l (compat "8.4"). (* 0 * n = 0 *)
+Notation mult_0_r := Nat.mul_0_r (compat "8.4"). (* n * 0 = 0 *)
(** ** 1 is neutral *)
-Lemma mult_1_l : forall n, 1 * n = n.
-Proof.
- simpl; auto with arith.
-Qed.
-Hint Resolve mult_1_l: arith v62.
+Notation mult_1_l := Nat.mul_1_l (compat "8.4"). (* 1 * n = n *)
+Notation mult_1_r := Nat.mul_1_r (compat "8.4"). (* n * 1 = n *)
-Lemma mult_1_r : forall n, n * 1 = n.
-Proof.
- induction n; [ trivial |
- simpl; rewrite IHn; reflexivity].
-Qed.
-Hint Resolve mult_1_r: arith v62.
+Hint Resolve mult_1_l mult_1_r: arith v62.
(** ** Commutativity *)
-Lemma mult_comm : forall n m, n * m = m * n.
-Proof.
-intros; induction n; simpl; auto with arith.
-rewrite <- mult_n_Sm.
-rewrite IHn; apply plus_comm.
-Qed.
+Notation mult_comm := Nat.mul_comm (compat "8.4"). (* n * m = m * n *)
+
Hint Resolve mult_comm: arith v62.
(** ** Distributivity *)
-Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p.
-Proof.
- intros; induction n; simpl; auto with arith.
- rewrite <- plus_assoc, IHn; auto with arith.
-Qed.
-Hint Resolve mult_plus_distr_r: arith v62.
+Notation mult_plus_distr_r :=
+ Nat.mul_add_distr_r (compat "8.4"). (* (n+m)*p = n*p + m*p *)
-Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p.
-Proof.
- induction n. trivial.
- intros. simpl. rewrite IHn. symmetry. apply plus_permute_2_in_4.
-Qed.
+Notation mult_plus_distr_l :=
+ Nat.mul_add_distr_l (compat "8.4"). (* n*(m+p) = n*m + n*p *)
-Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p.
-Proof.
- intros; induction n, m using nat_double_ind; simpl; auto with arith.
- rewrite <- minus_plus_simpl_l_reverse; auto with arith.
-Qed.
-Hint Resolve mult_minus_distr_r: arith v62.
+Notation mult_minus_distr_r :=
+ Nat.mul_sub_distr_r (compat "8.4"). (* (n-m)*p = n*p - m*p *)
-Lemma mult_minus_distr_l : forall n m p, n * (m - p) = n * m - n * p.
-Proof.
- intros n m p.
- rewrite mult_comm, mult_minus_distr_r, (mult_comm m n), (mult_comm p n); reflexivity.
-Qed.
+Notation mult_minus_distr_l :=
+ Nat.mul_sub_distr_l (compat "8.4"). (* n*(m-p) = n*m - n*p *)
+
+Hint Resolve mult_plus_distr_r: arith v62.
+Hint Resolve mult_minus_distr_r: arith v62.
Hint Resolve mult_minus_distr_l: arith v62.
(** ** Associativity *)
-Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p).
-Proof.
- intros; induction n; simpl; auto with arith.
- rewrite mult_plus_distr_r.
- induction IHn; auto with arith.
-Qed.
-Hint Resolve mult_assoc_reverse: arith v62.
+Notation mult_assoc := Nat.mul_assoc (compat "8.4"). (* n*(m*p)=n*m*p *)
-Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p.
+Lemma mult_assoc_reverse n m p : n * m * p = n * (m * p).
Proof.
- auto with arith.
+ symmetry. apply Nat.mul_assoc.
Qed.
+
+Hint Resolve mult_assoc_reverse: arith v62.
Hint Resolve mult_assoc: arith v62.
(** ** Inversion lemmas *)
-Lemma mult_is_O : forall n m, n * m = 0 -> n = 0 \/ m = 0.
+Lemma mult_is_O n m : n * m = 0 -> n = 0 \/ m = 0.
Proof.
- destruct n as [| n]; simpl; intros m H.
- left; trivial.
- right; apply plus_is_O in H; destruct H; trivial.
+ apply Nat.eq_mul_0.
Qed.
-Lemma mult_is_one : forall n m, n * m = 1 -> n = 1 /\ m = 1.
+Lemma mult_is_one n m : n * m = 1 -> n = 1 /\ m = 1.
Proof.
- destruct n as [|n]; simpl; intros m H.
- edestruct O_S; eauto.
- destruct plus_is_one with (1:=H) as [[-> Hnm] | [-> Hnm]].
- simpl in H; rewrite mult_0_r in H; elim (O_S _ H).
- rewrite mult_1_r in Hnm; auto.
+ apply Nat.eq_mul_1.
Qed.
(** ** Multiplication and successor *)
-Lemma mult_succ_l : forall n m:nat, S n * m = n * m + m.
-Proof.
- intros; simpl. rewrite plus_comm. reflexivity.
-Qed.
-
-Lemma mult_succ_r : forall n m:nat, n * S m = n * m + n.
-Proof.
- induction n as [| p H]; intro m; simpl.
- reflexivity.
- rewrite H, <- plus_n_Sm; apply f_equal; rewrite plus_assoc; reflexivity.
-Qed.
+Notation mult_succ_l := Nat.mul_succ_l (compat "8.4"). (* S n * m = n * m + m *)
+Notation mult_succ_r := Nat.mul_succ_r (compat "8.4"). (* n * S m = n * m + n *)
(** * Compatibility with orders *)
-Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n.
+Lemma mult_O_le n m : m = 0 \/ n <= m * n.
Proof.
- induction m; simpl; auto with arith.
+ destruct m; [left|right]; simpl; trivial using Nat.le_add_r.
Qed.
Hint Resolve mult_O_le: arith v62.
-Lemma mult_le_compat_l : forall n m p, n <= m -> p * n <= p * m.
+Lemma mult_le_compat_l n m p : n <= m -> p * n <= p * m.
Proof.
- induction p as [| p IHp]; intros; simpl.
- apply le_n.
- auto using plus_le_compat.
+ apply Nat.mul_le_mono_nonneg_l, Nat.le_0_l. (* TODO : get rid of 0<=n hyp *)
Qed.
Hint Resolve mult_le_compat_l: arith.
-
-Lemma mult_le_compat_r : forall n m p, n <= m -> n * p <= m * p.
+Lemma mult_le_compat_r n m p : n <= m -> n * p <= m * p.
Proof.
- intros m n p H; rewrite mult_comm, (mult_comm n); auto with arith.
+ apply Nat.mul_le_mono_nonneg_r, Nat.le_0_l.
Qed.
-Lemma mult_le_compat :
- forall n m p (q:nat), n <= m -> p <= q -> n * p <= m * q.
+Lemma mult_le_compat n m p q : n <= m -> p <= q -> n * p <= m * q.
Proof.
- intros m n p q Hmn Hpq; induction Hmn.
- induction Hpq.
- (* m*p<=m*p *)
- apply le_n.
- (* m*p<=m*m0 -> m*p<=m*(S m0) *)
- rewrite <- mult_n_Sm; apply le_trans with (m * m0).
- assumption.
- apply le_plus_l.
- (* m*p<=m0*q -> m*p<=(S m0)*q *)
- simpl; apply le_trans with (m0 * q).
- assumption.
- apply le_plus_r.
+ intros. apply Nat.mul_le_mono_nonneg; trivial; apply Nat.le_0_l.
Qed.
-Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.
+Lemma mult_S_lt_compat_l n m p : m < p -> S n * m < S n * p.
Proof.
- induction n; intros; simpl in *.
- rewrite <- 2 plus_n_O; assumption.
- auto using plus_lt_compat.
+ apply Nat.mul_lt_mono_pos_l, Nat.lt_0_succ.
Qed.
Hint Resolve mult_S_lt_compat_l: arith.
-Lemma mult_lt_compat_l : forall n m p, n < m -> 0 < p -> p * n < p * m.
+Lemma mult_lt_compat_l n m p : n < m -> 0 < p -> p * n < p * m.
Proof.
- intros m n p H Hp. destruct p. elim (lt_irrefl _ Hp).
- now apply mult_S_lt_compat_l.
+ intros. now apply Nat.mul_lt_mono_pos_l.
Qed.
-Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p.
+Lemma mult_lt_compat_r n m p : n < m -> 0 < p -> n * p < m * p.
Proof.
- intros m n p H Hp. destruct p. elim (lt_irrefl _ Hp).
- rewrite (mult_comm m), (mult_comm n). now apply mult_S_lt_compat_l.
+ intros. now apply Nat.mul_lt_mono_pos_r.
Qed.
-Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p.
+Lemma mult_S_le_reg_l n m p : S n * m <= S n * p -> m <= p.
Proof.
- intros m n p H; destruct (le_or_lt n p). trivial.
- assert (H1:S m * n < S m * n).
- apply le_lt_trans with (m := S m * p). assumption.
- apply mult_S_lt_compat_l. assumption.
- elim (lt_irrefl _ H1).
+ apply Nat.mul_le_mono_pos_l, Nat.lt_0_succ.
Qed.
(** * n|->2*n and n|->2n+1 have disjoint image *)
-Theorem odd_even_lem : forall p q, 2 * p + 1 <> 2 * q.
+Theorem odd_even_lem p q : 2 * p + 1 <> 2 * q.
Proof.
- induction p; destruct q.
- discriminate.
- simpl; rewrite plus_comm. discriminate.
- discriminate.
- intro H0; destruct (IHp q).
- replace (2 * q) with (2 * S q - 2).
- rewrite <- H0; simpl.
- repeat rewrite (fun x y => plus_comm x (S y)); simpl; auto.
- simpl; rewrite (fun y => plus_comm q (S y)); destruct q; simpl; auto.
+ intro. apply (Nat.Even_Odd_False (2*q)).
+ - now exists q.
+ - now exists p.
Qed.
@@ -232,10 +156,9 @@ Fixpoint mult_acc (s:nat) m n : nat :=
Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n.
Proof.
- induction n as [| p IHp]; simpl; auto.
- intros s m; rewrite <- plus_tail_plus; rewrite <- IHp.
- rewrite <- plus_assoc_reverse; apply f_equal2; auto.
- rewrite plus_comm; auto.
+ induction n as [| n IHn]; simpl; auto.
+ intros. rewrite Nat.add_assoc, IHn. f_equal.
+ rewrite Nat.add_comm. apply plus_tail_plus.
Qed.
Definition tail_mult n m := mult_acc 0 m n.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 05:16:19 +0000