← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Arith/Mult.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Arith/Mult.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: Mult.v 11015 2008-05-28 20:06:42Z herbelin $ i*)
 
10
 
 
11
Require Export Plus.
 
12
Require Export Minus.
 
13
Require Export Lt.
 
14
Require Export Le.
 
15
 
 
16
Open Local Scope nat_scope.
 
17
 
 
18
Implicit Types m n p : nat.
 
19
 
 
20
(** Theorems about multiplication in [nat]. [mult] is defined in module [Init/Peano.v]. *)
 
21
 
 
22
(** * [nat] is a semi-ring *)
 
23
 
 
24
(** ** Zero property *)
 
25
 
 
26
Lemma mult_0_r : forall n, n * 0 = 0.
 
27
Proof.
 
28
  intro; symmetry  in |- *; apply mult_n_O.
 
29
Qed.
 
30
 
 
31
Lemma mult_0_l : forall n, 0 * n = 0.
 
32
Proof.
 
33
  reflexivity.
 
34
Qed.
 
35
 
 
36
(** ** 1 is neutral *)
 
37
 
 
38
Lemma mult_1_l : forall n, 1 * n = n.
 
39
Proof.
 
40
  simpl in |- *; auto with arith.
 
41
Qed.
 
42
Hint Resolve mult_1_l: arith v62.
 
43
 
 
44
Lemma mult_1_r : forall n, n * 1 = n.
 
45
Proof.
 
46
  induction n; [ trivial | 
 
47
    simpl; rewrite IHn; reflexivity].
 
48
Qed.
 
49
Hint Resolve mult_1_r: arith v62.
 
50
 
 
51
(** ** Commutativity *)
 
52
 
 
53
Lemma mult_comm : forall n m, n * m = m * n.
 
54
Proof.
 
55
intros; elim n; intros; simpl in |- *; auto with arith.
 
56
elim mult_n_Sm.
 
57
elim H; apply plus_comm.
 
58
Qed.
 
59
Hint Resolve mult_comm: arith v62.
 
60
 
 
61
(** ** Distributivity *)
 
62
 
 
63
Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p.
 
64
Proof.
 
65
  intros; elim n; simpl in |- *; intros; auto with arith.
 
66
  elim plus_assoc; elim H; auto with arith.
 
67
Qed.
 
68
Hint Resolve mult_plus_distr_r: arith v62.
 
69
 
 
70
Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p.
 
71
Proof.
 
72
  induction n. trivial.
 
73
  intros. simpl in |- *. rewrite (IHn m p). apply sym_eq. apply plus_permute_2_in_4.
 
74
Qed.
 
75
 
 
76
Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p.
 
77
Proof.
 
78
  intros; pattern n, m in |- *; apply nat_double_ind; simpl in |- *; intros;
 
79
    auto with arith.
 
80
  elim minus_plus_simpl_l_reverse; auto with arith.
 
81
Qed.
 
82
Hint Resolve mult_minus_distr_r: arith v62.
 
83
 
 
84
Lemma mult_minus_distr_l : forall n m p, n * (m - p) = n * m - n * p.
 
85
Proof.
 
86
  intros n m p. rewrite mult_comm. rewrite mult_minus_distr_r. 
 
87
  rewrite (mult_comm m n); rewrite (mult_comm p n); reflexivity.
 
88
Qed.
 
89
Hint Resolve mult_minus_distr_l: arith v62.
 
90
 
 
91
(** ** Associativity *)
 
92
 
 
93
Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p).
 
94
Proof.
 
95
  intros; elim n; intros; simpl in |- *; auto with arith.
 
96
  rewrite mult_plus_distr_r.
 
97
  elim H; auto with arith.
 
98
Qed.
 
99
Hint Resolve mult_assoc_reverse: arith v62.
 
100
 
 
101
Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p.
 
102
Proof.
 
103
  auto with arith.
 
104
Qed.
 
105
Hint Resolve mult_assoc: arith v62.
 
106
 
 
107
(** ** Inversion lemmas *)
 
108
 
 
109
Lemma mult_is_O : forall n m, n * m = 0 -> n = 0 \/ m = 0.
 
110
Proof.
 
111
  destruct n as [| n]. 
 
112
    intros; left; trivial.
 
113
 
 
114
    simpl; intros m H; right. 
 
115
    assert (H':m = 0 /\ n * m = 0) by apply (plus_is_O _ _ H).
 
116
    destruct H'; trivial.
 
117
Qed.
 
118
 
 
119
Lemma mult_is_one : forall n m, n * m = 1 -> n = 1 /\ m = 1.
 
120
Proof.
 
121
  destruct n as [|n].
 
122
    simpl; intros m H; elim (O_S _ H).
 
123
 
 
124
    simpl; intros m H.
 
125
    destruct (plus_is_one _ _ H) as [[Hm Hnm] | [Hm Hnm]].
 
126
      rewrite Hm in H; simpl in H; rewrite mult_0_r in H; elim (O_S _ H).
 
127
      rewrite Hm in Hnm; rewrite mult_1_r in Hnm; auto. 
 
128
Qed.
 
129
 
 
130
(** ** Multiplication and successor *)
 
131
 
 
132
Lemma mult_succ_l : forall n m:nat, S n * m = n * m + m.
 
133
Proof.
 
134
  intros; simpl. rewrite plus_comm. reflexivity.
 
135
Qed.
 
136
 
 
137
Lemma mult_succ_r : forall n m:nat, n * S m = n * m + n.
 
138
Proof.
 
139
  induction n as [| p H]; intro m; simpl.
 
140
  reflexivity.
 
141
  rewrite H, <- plus_n_Sm; apply f_equal; rewrite plus_assoc; reflexivity.
 
142
Qed.
 
143
 
 
144
(** * Compatibility with orders *)
 
145
 
 
146
Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n.
 
147
Proof.
 
148
  induction m; simpl in |- *; auto with arith.
 
149
Qed.
 
150
Hint Resolve mult_O_le: arith v62.
 
151
 
 
152
Lemma mult_le_compat_l : forall n m p, n <= m -> p * n <= p * m.
 
153
Proof.
 
154
  induction p as [| p IHp]. intros. simpl in |- *. apply le_n.
 
155
  intros. simpl in |- *. apply plus_le_compat. assumption.
 
156
  apply IHp. assumption.
 
157
Qed.
 
158
Hint Resolve mult_le_compat_l: arith.
 
159
 
 
160
 
 
161
Lemma mult_le_compat_r : forall n m p, n <= m -> n * p <= m * p.
 
162
Proof.
 
163
  intros m n p H.
 
164
  rewrite mult_comm. rewrite (mult_comm n).
 
165
  auto with arith.
 
166
Qed.
 
167
 
 
168
Lemma mult_le_compat :
 
169
  forall n m p (q:nat), n <= m -> p <= q -> n * p <= m * q.
 
170
Proof.
 
171
  intros m n p q Hmn Hpq; induction Hmn.
 
172
  induction Hpq.
 
173
  (* m*p<=m*p *)
 
174
  apply le_n.
 
175
  (* m*p<=m*m0 -> m*p<=m*(S m0) *)
 
176
  rewrite <- mult_n_Sm; apply le_trans with (m * m0).
 
177
  assumption.
 
178
  apply le_plus_l.
 
179
  (* m*p<=m0*q -> m*p<=(S m0)*q *)
 
180
  simpl in |- *; apply le_trans with (m0 * q).
 
181
  assumption.
 
182
  apply le_plus_r.
 
183
Qed.
 
184
 
 
185
Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.
 
186
Proof.
 
187
  intro m; induction m. intros. simpl in |- *. rewrite <- plus_n_O. rewrite <- plus_n_O. assumption.
 
188
  intros. exact (plus_lt_compat _ _ _ _ H (IHm _ _ H)).
 
189
Qed.
 
190
 
 
191
Hint Resolve mult_S_lt_compat_l: arith.
 
192
 
 
193
Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p.
 
194
Proof.
 
195
  intros m n p H H0.
 
196
  induction p.
 
197
  elim (lt_irrefl _ H0).
 
198
  rewrite mult_comm.
 
199
  replace (n * S p) with (S p * n); auto with arith.
 
200
Qed.
 
201
 
 
202
Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p.
 
203
Proof.
 
204
  intros m n p H. elim (le_or_lt n p). trivial.
 
205
  intro H0. cut (S m * n < S m * n). intro. elim (lt_irrefl _ H1).
 
206
  apply le_lt_trans with (m := S m * p). assumption.
 
207
  apply mult_S_lt_compat_l. assumption.
 
208
Qed.
 
209
 
 
210
(** * n|->2*n and n|->2n+1 have disjoint image *)
 
211
 
 
212
Theorem odd_even_lem : forall p q, 2 * p + 1 <> 2 * q.
 
213
Proof.
 
214
  intros p; elim p; auto.
 
215
  intros q; case q; simpl in |- *.
 
216
  red in |- *; intros; discriminate.
 
217
  intros q'; rewrite (fun x y => plus_comm x (S y)); simpl in |- *; red in |- *;
 
218
    intros; discriminate.
 
219
  intros p' H q; case q.
 
220
  simpl in |- *; red in |- *; intros; discriminate.
 
221
  intros q'; red in |- *; intros H0; case (H q').
 
222
  replace (2 * q') with (2 * S q' - 2).
 
223
  rewrite <- H0; simpl in |- *; auto.
 
224
  repeat rewrite (fun x y => plus_comm x (S y)); simpl in |- *; auto.
 
225
  simpl in |- *; repeat rewrite (fun x y => plus_comm x (S y)); simpl in |- *;
 
226
    auto.
 
227
  case q'; simpl in |- *; auto.
 
228
Qed.
 
229
 
 
230
 
 
231
(** * Tail-recursive mult *)
 
232
 
 
233
(** [tail_mult] is an alternative definition for [mult] which is 
 
234
    tail-recursive, whereas [mult] is not. This can be useful 
 
235
    when extracting programs. *)
 
236
 
 
237
Fixpoint mult_acc (s:nat) m n {struct n} : nat :=
 
238
  match n with
 
239
    | O => s
 
240
    | S p => mult_acc (tail_plus m s) m p
 
241
  end.
 
242
 
 
243
Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n.
 
244
Proof.
 
245
  induction n as [| p IHp]; simpl in |- *; auto.
 
246
  intros s m; rewrite <- plus_tail_plus; rewrite <- IHp.
 
247
  rewrite <- plus_assoc_reverse; apply (f_equal2 (A1:=nat) (A2:=nat)); auto.
 
248
  rewrite plus_comm; auto.
 
249
Qed.
 
250
 
 
251
Definition tail_mult n m := mult_acc 0 m n.
 
252
 
 
253
Lemma mult_tail_mult : forall n m, n * m = tail_mult n m.
 
254
Proof.
 
255
  intros; unfold tail_mult in |- *; rewrite <- mult_acc_aux; auto.
 
256
Qed.
 
257
 
 
258
(** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus] 
 
259
    and [mult] and simplify *)
 
260
 
 
261
Ltac tail_simpl :=
 
262
  repeat rewrite <- plus_tail_plus; repeat rewrite <- mult_tail_mult;
 
263
    simpl in |- *.