diff options
Diffstat (limited to 'theories/Arith/Mult.v')
| -rw-r--r-- | theories/Arith/Mult.v | 189 |
1 files changed, 102 insertions, 87 deletions
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index 051f8645..2315e12c 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Mult.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Mult.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Export Plus. Require Export Minus. @@ -17,86 +17,98 @@ Open Local Scope nat_scope. Implicit Types m n p : nat. -(** Zero property *) +(** Theorems about multiplication in [nat]. [mult] is defined in module [Init/Peano.v]. *) + +(** * [nat] is a semi-ring *) + +(** ** Zero property *) Lemma mult_0_r : forall n, n * 0 = 0. Proof. -intro; symmetry in |- *; apply mult_n_O. + intro; symmetry in |- *; apply mult_n_O. Qed. Lemma mult_0_l : forall n, 0 * n = 0. Proof. -reflexivity. + reflexivity. Qed. -(** Distributivity *) +(** ** 1 is neutral *) -Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p. +Lemma mult_1_l : forall n, 1 * n = n. Proof. -intros; elim n; simpl in |- *; intros; auto with arith. -elim plus_assoc; elim H; auto with arith. + simpl in |- *; auto with arith. Qed. -Hint Resolve mult_plus_distr_r: arith v62. +Hint Resolve mult_1_l: arith v62. -Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p. +Lemma mult_1_r : forall n, n * 1 = n. Proof. - induction n. trivial. - intros. simpl in |- *. rewrite (IHn m p). apply sym_eq. apply plus_permute_2_in_4. + induction n; [ trivial | + simpl; rewrite IHn; reflexivity]. Qed. +Hint Resolve mult_1_r: arith v62. -Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p. +(** ** Commutativity *) + +Lemma mult_comm : forall n m, n * m = m * n. Proof. -intros; pattern n, m in |- *; apply nat_double_ind; simpl in |- *; intros; - auto with arith. -elim minus_plus_simpl_l_reverse; auto with arith. +intros; elim n; intros; simpl in |- *; auto with arith. +elim mult_n_Sm. +elim H; apply plus_comm. Qed. -Hint Resolve mult_minus_distr_r: arith v62. +Hint Resolve mult_comm: arith v62. -(** Associativity *) +(** ** Distributivity *) -Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p). +Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p. Proof. -intros; elim n; intros; simpl in |- *; auto with arith. -rewrite mult_plus_distr_r. -elim H; auto with arith. + intros; elim n; simpl in |- *; intros; auto with arith. + elim plus_assoc; elim H; auto with arith. Qed. -Hint Resolve mult_assoc_reverse: arith v62. +Hint Resolve mult_plus_distr_r: arith v62. -Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p. +Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p. Proof. -auto with arith. + induction n. trivial. + intros. simpl in |- *. rewrite (IHn m p). apply sym_eq. apply plus_permute_2_in_4. Qed. -Hint Resolve mult_assoc: arith v62. -(** Commutativity *) +Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p. +Proof. + intros; pattern n, m in |- *; apply nat_double_ind; simpl in |- *; intros; + auto with arith. + elim minus_plus_simpl_l_reverse; auto with arith. +Qed. +Hint Resolve mult_minus_distr_r: arith v62. -Lemma mult_comm : forall n m, n * m = m * n. +Lemma mult_minus_distr_l : forall n m p, n * (m - p) = n * m - n * p. Proof. -intros; elim n; intros; simpl in |- *; auto with arith. -elim mult_n_Sm. -elim H; apply plus_comm. + intros n m p. rewrite mult_comm. rewrite mult_minus_distr_r. + rewrite (mult_comm m n); rewrite (mult_comm p n); reflexivity. Qed. -Hint Resolve mult_comm: arith v62. +Hint Resolve mult_minus_distr_l: arith v62. -(** 1 is neutral *) +(** ** Associativity *) -Lemma mult_1_l : forall n, 1 * n = n. +Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p). Proof. -simpl in |- *; auto with arith. + intros; elim n; intros; simpl in |- *; auto with arith. + rewrite mult_plus_distr_r. + elim H; auto with arith. Qed. -Hint Resolve mult_1_l: arith v62. +Hint Resolve mult_assoc_reverse: arith v62. -Lemma mult_1_r : forall n, n * 1 = n. +Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p. Proof. -intro; elim mult_comm; auto with arith. + auto with arith. Qed. -Hint Resolve mult_1_r: arith v62. +Hint Resolve mult_assoc: arith v62. -(** Compatibility with orders *) +(** * Compatibility with orders *) Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n. Proof. -induction m; simpl in |- *; auto with arith. + induction m; simpl in |- *; auto with arith. Qed. Hint Resolve mult_O_le: arith v62. @@ -110,26 +122,27 @@ Hint Resolve mult_le_compat_l: arith. Lemma mult_le_compat_r : forall n m p, n <= m -> n * p <= m * p. -intros m n p H. -rewrite mult_comm. rewrite (mult_comm n). -auto with arith. +Proof. + intros m n p H. + rewrite mult_comm. rewrite (mult_comm n). + auto with arith. Qed. Lemma mult_le_compat : - forall n m p (q:nat), 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 in |- *; apply le_trans with (m0 * q). -assumption. -apply le_plus_r. + forall n m p (q:nat), 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 in |- *; apply le_trans with (m0 * q). + assumption. + apply le_plus_r. Qed. Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p. @@ -141,11 +154,12 @@ Qed. Hint Resolve mult_S_lt_compat_l: arith. Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p. -intros m n p H H0. -induction p. -elim (lt_irrefl _ H0). -rewrite mult_comm. -replace (n * S p) with (S p * n); auto with arith. +Proof. + intros m n p H H0. + induction p. + elim (lt_irrefl _ H0). + rewrite mult_comm. + replace (n * S p) with (S p * n); auto with arith. Qed. Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p. @@ -156,27 +170,28 @@ Proof. apply mult_S_lt_compat_l. assumption. Qed. -(** n|->2*n and n|->2n+1 have disjoint image *) +(** * n|->2*n and n|->2n+1 have disjoint image *) Theorem odd_even_lem : forall p q, 2 * p + 1 <> 2 * q. -intros p; elim p; auto. -intros q; case q; simpl in |- *. -red in |- *; intros; discriminate. -intros q'; rewrite (fun x y => plus_comm x (S y)); simpl in |- *; red in |- *; - intros; discriminate. -intros p' H q; case q. -simpl in |- *; red in |- *; intros; discriminate. -intros q'; red in |- *; intros H0; case (H q'). -replace (2 * q') with (2 * S q' - 2). -rewrite <- H0; simpl in |- *; auto. -repeat rewrite (fun x y => plus_comm x (S y)); simpl in |- *; auto. -simpl in |- *; repeat rewrite (fun x y => plus_comm x (S y)); simpl in |- *; - auto. -case q'; simpl in |- *; auto. +Proof. + intros p; elim p; auto. + intros q; case q; simpl in |- *. + red in |- *; intros; discriminate. + intros q'; rewrite (fun x y => plus_comm x (S y)); simpl in |- *; red in |- *; + intros; discriminate. + intros p' H q; case q. + simpl in |- *; red in |- *; intros; discriminate. + intros q'; red in |- *; intros H0; case (H q'). + replace (2 * q') with (2 * S q' - 2). + rewrite <- H0; simpl in |- *; auto. + repeat rewrite (fun x y => plus_comm x (S y)); simpl in |- *; auto. + simpl in |- *; repeat rewrite (fun x y => plus_comm x (S y)); simpl in |- *; + auto. + case q'; simpl in |- *; auto. Qed. -(** Tail-recursive mult *) +(** * Tail-recursive mult *) (** [tail_mult] is an alternative definition for [mult] which is tail-recursive, whereas [mult] is not. This can be useful @@ -184,23 +199,23 @@ Qed. Fixpoint mult_acc (s:nat) m n {struct n} : nat := match n with - | O => s - | S p => mult_acc (tail_plus m s) m p + | O => s + | S p => mult_acc (tail_plus m s) m p end. Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n. Proof. -induction n as [| p IHp]; simpl in |- *; auto. -intros s m; rewrite <- plus_tail_plus; rewrite <- IHp. -rewrite <- plus_assoc_reverse; apply (f_equal2 (A1:=nat) (A2:=nat)); auto. -rewrite plus_comm; auto. + induction n as [| p IHp]; simpl in |- *; auto. + intros s m; rewrite <- plus_tail_plus; rewrite <- IHp. + rewrite <- plus_assoc_reverse; apply (f_equal2 (A1:=nat) (A2:=nat)); auto. + rewrite plus_comm; auto. Qed. Definition tail_mult n m := mult_acc 0 m n. Lemma mult_tail_mult : forall n m, n * m = tail_mult n m. Proof. -intros; unfold tail_mult in |- *; rewrite <- mult_acc_aux; auto. + intros; unfold tail_mult in |- *; rewrite <- mult_acc_aux; auto. Qed. (** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus] @@ -208,4 +223,4 @@ Qed. Ltac tail_simpl := repeat rewrite <- plus_tail_plus; repeat rewrite <- mult_tail_mult; - simpl in |- *.
\ No newline at end of file + simpl in |- *.
\ No newline at end of file |