aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith/Mult.v
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-17 12:53:34 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-17 12:53:34 +0000
commit28dc7a05cc1d3e03ed1435b3db4340db954a59e2 (patch)
tree63cdf18cd47260eb90550f62f7b22e2e2e208f6c /theories/Arith/Mult.v
parent744e7f6a319f4d459a3cc2309f575d43041d75aa (diff)
Mise en forme des theories
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Mult.v')
-rw-r--r--theories/Arith/Mult.v162
1 files changed, 85 insertions, 77 deletions
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 85977244e..ab3e65856 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -17,19 +17,38 @@ 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.
+
+(** ** 1 is neutral *)
+
+Lemma mult_1_l : forall n, 1 * n = n.
+Proof.
+ simpl in |- *; auto with arith.
Qed.
+Hint Resolve mult_1_l: arith v62.
-(** Commutativity *)
+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.
+
+(** ** Commutativity *)
Lemma mult_comm : forall n m, n * m = m * n.
Proof.
@@ -39,12 +58,12 @@ elim H; apply plus_comm.
Qed.
Hint Resolve mult_comm: arith v62.
-(** Distributivity *)
+(** ** Distributivity *)
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; elim n; simpl in |- *; intros; auto with arith.
+ elim plus_assoc; elim H; auto with arith.
Qed.
Hint Resolve mult_plus_distr_r: arith v62.
@@ -56,9 +75,9 @@ 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; 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.
@@ -69,41 +88,27 @@ Proof.
Qed.
Hint Resolve mult_minus_distr_l: arith v62.
-(** Associativity *)
+(** ** Associativity *)
Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (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; intros; simpl in |- *; auto with arith.
+ rewrite mult_plus_distr_r.
+ elim H; auto with arith.
Qed.
Hint Resolve mult_assoc_reverse: arith v62.
Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p.
Proof.
-auto with arith.
+ auto with arith.
Qed.
Hint Resolve mult_assoc: arith v62.
-(** 1 is neutral *)
-
-Lemma mult_1_l : forall n, 1 * n = n.
-Proof.
-simpl in |- *; auto with arith.
-Qed.
-Hint Resolve mult_1_l: arith v62.
-
-Lemma mult_1_r : forall n, n * 1 = n.
-Proof.
-intro; elim mult_comm; auto with arith.
-Qed.
-Hint Resolve mult_1_r: 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.
@@ -117,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.
@@ -148,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.
@@ -163,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
@@ -191,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]
@@ -215,4 +223,4 @@ Qed.
Ltac tail_simpl :=
repeat rewrite <- plus_tail_plus; repeat rewrite <- mult_tail_mult;
- simpl in |- *.
+ simpl in |- *. \ No newline at end of file