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.v107
1 files changed, 48 insertions, 59 deletions
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index a43579f9..8346cae3 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 11015 2008-05-28 20:06:42Z herbelin $ i*)
+(*i $Id$ i*)
Require Export Plus.
Require Export Minus.
@@ -43,7 +43,7 @@ Hint Resolve mult_1_l: arith v62.
Lemma mult_1_r : forall n, n * 1 = n.
Proof.
- induction n; [ trivial |
+ induction n; [ trivial |
simpl; rewrite IHn; reflexivity].
Qed.
Hint Resolve mult_1_r: arith v62.
@@ -52,9 +52,9 @@ Hint Resolve mult_1_r: arith v62.
Lemma mult_comm : forall n m, n * m = m * n.
Proof.
-intros; elim n; intros; simpl in |- *; auto with arith.
-elim mult_n_Sm.
-elim H; apply plus_comm.
+intros; induction n; simpl; auto with arith.
+rewrite <- mult_n_Sm.
+rewrite IHn; apply plus_comm.
Qed.
Hint Resolve mult_comm: arith v62.
@@ -62,29 +62,28 @@ Hint Resolve mult_comm: arith v62.
Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p.
Proof.
- intros; elim n; simpl in |- *; intros; auto with arith.
- elim plus_assoc; elim H; auto with arith.
+ intros; induction n; simpl; auto with arith.
+ rewrite <- plus_assoc, IHn; auto with arith.
Qed.
Hint Resolve mult_plus_distr_r: arith v62.
Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p.
Proof.
induction n. trivial.
- intros. simpl in |- *. rewrite (IHn m p). apply sym_eq. apply plus_permute_2_in_4.
+ intros. simpl in |- *. rewrite IHn. symmetry. apply plus_permute_2_in_4.
Qed.
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.
+ 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.
Lemma mult_minus_distr_l : forall n m p, n * (m - p) = n * m - n * p.
Proof.
- intros n m p. rewrite mult_comm. rewrite mult_minus_distr_r.
- rewrite (mult_comm m n); rewrite (mult_comm p n); reflexivity.
+ intros n m p.
+ rewrite mult_comm, mult_minus_distr_r, (mult_comm m n), (mult_comm p n); reflexivity.
Qed.
Hint Resolve mult_minus_distr_l: arith v62.
@@ -92,9 +91,9 @@ Hint Resolve mult_minus_distr_l: arith v62.
Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p).
Proof.
- intros; elim n; intros; simpl in |- *; auto with arith.
+ intros; induction n; simpl; auto with arith.
rewrite mult_plus_distr_r.
- elim H; auto with arith.
+ induction IHn; auto with arith.
Qed.
Hint Resolve mult_assoc_reverse: arith v62.
@@ -108,23 +107,18 @@ Hint Resolve mult_assoc: arith v62.
Lemma mult_is_O : forall n m, n * m = 0 -> n = 0 \/ m = 0.
Proof.
- destruct n as [| n].
- intros; left; trivial.
-
- simpl; intros m H; right.
- assert (H':m = 0 /\ n * m = 0) by apply (plus_is_O _ _ H).
- destruct H'; trivial.
+ destruct n as [| n]; simpl; intros m H.
+ left; trivial.
+ right; apply plus_is_O in H; destruct H; trivial.
Qed.
Lemma mult_is_one : forall n m, n * m = 1 -> n = 1 /\ m = 1.
Proof.
- destruct n as [|n].
- simpl; intros m H; elim (O_S _ H).
-
- simpl; intros m H.
- destruct (plus_is_one _ _ H) as [[Hm Hnm] | [Hm Hnm]].
- rewrite Hm in H; simpl in H; rewrite mult_0_r in H; elim (O_S _ H).
- rewrite Hm in Hnm; rewrite mult_1_r in Hnm; auto.
+ 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.
Qed.
(** ** Multiplication and successor *)
@@ -151,18 +145,16 @@ Hint Resolve mult_O_le: arith v62.
Lemma mult_le_compat_l : forall n m p, n <= m -> p * n <= p * m.
Proof.
- induction p as [| p IHp]. intros. simpl in |- *. apply le_n.
- intros. simpl in |- *. apply plus_le_compat. assumption.
- apply IHp. assumption.
+ induction p as [| p IHp]; intros; simpl in |- *.
+ apply le_n.
+ auto using plus_le_compat.
Qed.
Hint Resolve mult_le_compat_l: arith.
Lemma mult_le_compat_r : forall n m p, n <= m -> n * p <= m * p.
Proof.
- intros m n p H.
- rewrite mult_comm. rewrite (mult_comm n).
- auto with arith.
+ intros m n p H; rewrite mult_comm, (mult_comm n); auto with arith.
Qed.
Lemma mult_le_compat :
@@ -184,8 +176,9 @@ Qed.
Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.
Proof.
- intro m; induction m. intros. simpl in |- *. rewrite <- plus_n_O. rewrite <- plus_n_O. assumption.
- intros. exact (plus_lt_compat _ _ _ _ H (IHm _ _ H)).
+ induction n; intros; simpl in *.
+ rewrite <- 2! plus_n_O; assumption.
+ auto using plus_lt_compat.
Qed.
Hint Resolve mult_S_lt_compat_l: arith.
@@ -201,40 +194,36 @@ Qed.
Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p.
Proof.
- intros m n p H. elim (le_or_lt n p). trivial.
- intro H0. cut (S m * n < S m * n). intro. elim (lt_irrefl _ H1).
- apply le_lt_trans with (m := S m * p). assumption.
- apply mult_S_lt_compat_l. assumption.
+ 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).
Qed.
(** * n|->2*n and n|->2n+1 have disjoint image *)
Theorem odd_even_lem : forall p q, 2 * p + 1 <> 2 * q.
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.
+ 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.
Qed.
(** * Tail-recursive mult *)
-(** [tail_mult] is an alternative definition for [mult] which is
- tail-recursive, whereas [mult] is not. This can be useful
+(** [tail_mult] is an alternative definition for [mult] which is
+ tail-recursive, whereas [mult] is not. This can be useful
when extracting programs. *)
-Fixpoint mult_acc (s:nat) m n {struct n} : nat :=
+Fixpoint mult_acc (s:nat) m n : nat :=
match n with
| O => s
| S p => mult_acc (tail_plus m s) m p
@@ -244,7 +233,7 @@ 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_assoc_reverse; apply f_equal2; auto.
rewrite plus_comm; auto.
Qed.
@@ -255,7 +244,7 @@ Proof.
intros; unfold tail_mult in |- *; rewrite <- mult_acc_aux; auto.
Qed.
-(** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus]
+(** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus]
and [mult] and simplify *)
Ltac tail_simpl :=
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 05:13:45 +0000