← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/ZArith/Zeven.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/ZArith/Zeven.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: Zeven.v 10291 2007-11-06 02:18:53Z letouzey $ i*)
 
10
 
 
11
Require Import BinInt.
 
12
 
 
13
Open Scope Z_scope.
 
14
 
 
15
(*******************************************************************)
 
16
(** About parity: even and odd predicates on Z, division by 2 on Z *)
 
17
 
 
18
(***************************************************)
 
19
(** * [Zeven], [Zodd] and their related properties *)
 
20
 
 
21
Definition Zeven (z:Z) :=
 
22
  match z with
 
23
    | Z0 => True
 
24
    | Zpos (xO _) => True
 
25
    | Zneg (xO _) => True
 
26
    | _ => False
 
27
  end.
 
28
 
 
29
Definition Zodd (z:Z) :=
 
30
  match z with
 
31
    | Zpos xH => True
 
32
    | Zneg xH => True
 
33
    | Zpos (xI _) => True
 
34
    | Zneg (xI _) => True
 
35
    | _ => False
 
36
  end.
 
37
 
 
38
Definition Zeven_bool (z:Z) :=
 
39
  match z with
 
40
    | Z0 => true
 
41
    | Zpos (xO _) => true
 
42
    | Zneg (xO _) => true
 
43
    | _ => false
 
44
  end.
 
45
 
 
46
Definition Zodd_bool (z:Z) :=
 
47
  match z with
 
48
    | Z0 => false
 
49
    | Zpos (xO _) => false
 
50
    | Zneg (xO _) => false
 
51
    | _ => true
 
52
  end.
 
53
 
 
54
Definition Zeven_odd_dec : forall z:Z, {Zeven z} + {Zodd z}.
 
55
Proof.
 
56
  intro z. case z;
 
57
  [ left; compute in |- *; trivial
 
58
    | intro p; case p; intros;
 
59
      (right; compute in |- *; exact I) || (left; compute in |- *; exact I)
 
60
    | intro p; case p; intros;
 
61
      (right; compute in |- *; exact I) || (left; compute in |- *; exact I) ].
 
62
Defined.
 
63
 
 
64
Definition Zeven_dec : forall z:Z, {Zeven z} + {~ Zeven z}.
 
65
Proof.
 
66
  intro z. case z;
 
67
  [ left; compute in |- *; trivial
 
68
    | intro p; case p; intros;
 
69
      (left; compute in |- *; exact I) || (right; compute in |- *; trivial)
 
70
    | intro p; case p; intros;
 
71
      (left; compute in |- *; exact I) || (right; compute in |- *; trivial) ].
 
72
Defined.
 
73
 
 
74
Definition Zodd_dec : forall z:Z, {Zodd z} + {~ Zodd z}.
 
75
Proof.
 
76
  intro z. case z;
 
77
  [ right; compute in |- *; trivial
 
78
    | intro p; case p; intros;
 
79
      (left; compute in |- *; exact I) || (right; compute in |- *; trivial)
 
80
    | intro p; case p; intros;
 
81
      (left; compute in |- *; exact I) || (right; compute in |- *; trivial) ].
 
82
Defined.
 
83
 
 
84
Lemma Zeven_not_Zodd : forall n:Z, Zeven n -> ~ Zodd n.
 
85
Proof.
 
86
  intro z; destruct z; [ idtac | destruct p | destruct p ]; compute in |- *;
 
87
    trivial.
 
88
Qed.
 
89
 
 
90
Lemma Zodd_not_Zeven : forall n:Z, Zodd n -> ~ Zeven n.
 
91
Proof.
 
92
  intro z; destruct z; [ idtac | destruct p | destruct p ]; compute in |- *;
 
93
    trivial.
 
94
Qed.
 
95
 
 
96
Lemma Zeven_Sn : forall n:Z, Zodd n -> Zeven (Zsucc n).
 
97
Proof.
 
98
  intro z; destruct z; unfold Zsucc in |- *;
 
99
    [ idtac | destruct p | destruct p ]; simpl in |- *; 
 
100
      trivial. 
 
101
  unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto.
 
102
Qed.
 
103
 
 
104
Lemma Zodd_Sn : forall n:Z, Zeven n -> Zodd (Zsucc n).
 
105
Proof.
 
106
  intro z; destruct z; unfold Zsucc in |- *;
 
107
    [ idtac | destruct p | destruct p ]; simpl in |- *; 
 
108
      trivial. 
 
109
  unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto.
 
110
Qed.
 
111
 
 
112
Lemma Zeven_pred : forall n:Z, Zodd n -> Zeven (Zpred n).
 
113
Proof.
 
114
  intro z; destruct z; unfold Zpred in |- *;
 
115
    [ idtac | destruct p | destruct p ]; simpl in |- *; 
 
116
      trivial. 
 
117
  unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto.
 
118
Qed.
 
119
 
 
120
Lemma Zodd_pred : forall n:Z, Zeven n -> Zodd (Zpred n).
 
121
Proof.
 
122
  intro z; destruct z; unfold Zpred in |- *;
 
123
    [ idtac | destruct p | destruct p ]; simpl in |- *; 
 
124
      trivial. 
 
125
  unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto.
 
126
Qed.
 
127
 
 
128
Hint Unfold Zeven Zodd: zarith.
 
129
 
 
130
 
 
131
(******************************************************************)
 
132
(** * Definition of [Zdiv2] and properties wrt [Zeven] and [Zodd] *)
 
133
 
 
134
(** [Zdiv2] is defined on all [Z], but notice that for odd negative
 
135
    integers it is not the euclidean quotient: in that case we have 
 
136
      [n = 2*(n/2)-1] *)
 
137
 
 
138
Definition Zdiv2 (z:Z) :=
 
139
  match z with
 
140
    | Z0 => 0
 
141
    | Zpos xH => 0
 
142
    | Zpos p => Zpos (Pdiv2 p)
 
143
    | Zneg xH => 0
 
144
    | Zneg p => Zneg (Pdiv2 p)
 
145
  end.
 
146
 
 
147
Lemma Zeven_div2 : forall n:Z, Zeven n -> n = 2 * Zdiv2 n.
 
148
Proof.
 
149
  intro x; destruct x.
 
150
  auto with arith.
 
151
  destruct p; auto with arith.
 
152
  intros. absurd (Zeven (Zpos (xI p))); red in |- *; auto with arith.
 
153
  intros. absurd (Zeven 1); red in |- *; auto with arith.
 
154
  destruct p; auto with arith.
 
155
  intros. absurd (Zeven (Zneg (xI p))); red in |- *; auto with arith.
 
156
  intros. absurd (Zeven (-1)); red in |- *; auto with arith.
 
157
Qed.
 
158
 
 
159
Lemma Zodd_div2 : forall n:Z, n >= 0 -> Zodd n -> n = 2 * Zdiv2 n + 1.
 
160
Proof.
 
161
  intro x; destruct x.
 
162
  intros. absurd (Zodd 0); red in |- *; auto with arith.
 
163
  destruct p; auto with arith.
 
164
  intros. absurd (Zodd (Zpos (xO p))); red in |- *; auto with arith.
 
165
  intros. absurd (Zneg p >= 0); red in |- *; auto with arith.
 
166
Qed.
 
167
 
 
168
Lemma Zodd_div2_neg :
 
169
  forall n:Z, n <= 0 -> Zodd n -> n = 2 * Zdiv2 n - 1.
 
170
Proof.
 
171
  intro x; destruct x.
 
172
  intros. absurd (Zodd 0); red in |- *; auto with arith.
 
173
  intros. absurd (Zneg p >= 0); red in |- *; auto with arith.
 
174
  destruct p; auto with arith.
 
175
  intros. absurd (Zodd (Zneg (xO p))); red in |- *; auto with arith.
 
176
Qed.
 
177
 
 
178
Lemma Z_modulo_2 :
 
179
  forall n:Z, {y : Z | n = 2 * y} + {y : Z | n = 2 * y + 1}.
 
180
Proof.
 
181
  intros x.
 
182
  elim (Zeven_odd_dec x); intro.
 
183
  left. split with (Zdiv2 x). exact (Zeven_div2 x a).
 
184
  right. generalize b; clear b; case x.
 
185
  intro b; inversion b.
 
186
  intro p; split with (Zdiv2 (Zpos p)). apply (Zodd_div2 (Zpos p)); trivial.
 
187
  unfold Zge, Zcompare in |- *; simpl in |- *; discriminate.
 
188
  intro p; split with (Zdiv2 (Zpred (Zneg p))).
 
189
  pattern (Zneg p) at 1 in |- *; rewrite (Zsucc_pred (Zneg p)).
 
190
  pattern (Zpred (Zneg p)) at 1 in |- *; rewrite (Zeven_div2 (Zpred (Zneg p))).
 
191
  reflexivity.
 
192
  apply Zeven_pred; assumption.
 
193
Qed.
 
194
 
 
195
Lemma Zsplit2 :
 
196
  forall n:Z,
 
197
    {p : Z * Z |
 
198
      let (x1, x2) := p in n = x1 + x2 /\ (x1 = x2 \/ x2 = x1 + 1)}.
 
199
Proof.
 
200
  intros x.
 
201
  elim (Z_modulo_2 x); intros [y Hy]; rewrite Zmult_comm in Hy;
 
202
    rewrite <- Zplus_diag_eq_mult_2 in Hy.
 
203
  exists (y, y); split. 
 
204
  assumption.
 
205
  left; reflexivity.
 
206
  exists (y, (y + 1)%Z); split.
 
207
  rewrite Zplus_assoc; assumption.
 
208
  right; reflexivity.
 
209
Qed.
 
210
 
 
211
 
 
212
Theorem Zeven_ex: forall n, Zeven n -> exists m, n = 2 * m.
 
213
Proof.
 
214
  intro n; exists (Zdiv2 n); apply Zeven_div2; auto.
 
215
Qed.
 
216
 
 
217
Theorem Zodd_ex: forall n, Zodd n -> exists m, n = 2 * m + 1.
 
218
Proof.
 
219
  destruct n; intros.
 
220
  inversion H.
 
221
  exists (Zdiv2 (Zpos p)).
 
222
  apply Zodd_div2; simpl; auto; compute; inversion 1.
 
223
  exists (Zdiv2 (Zneg p) - 1).
 
224
  unfold Zminus.
 
225
  rewrite Zmult_plus_distr_r.
 
226
  rewrite <- Zplus_assoc.
 
227
  assert (Zneg p <= 0) by (compute; inversion 1).
 
228
  exact (Zodd_div2_neg _ H0 H).
 
229
Qed.
 
230
 
 
231
Theorem Zeven_2p: forall p, Zeven (2 * p).
 
232
Proof.
 
233
  destruct p; simpl; auto.
 
234
Qed.
 
235
 
 
236
Theorem Zodd_2p_plus_1: forall p, Zodd (2 * p + 1).
 
237
Proof.
 
238
  destruct p; simpl; auto.
 
239
  destruct p; simpl; auto.
 
240
Qed.
 
241
 
 
242
Theorem Zeven_plus_Zodd: forall a b, 
 
243
 Zeven a -> Zodd b -> Zodd (a + b).
 
244
Proof.
 
245
  intros a b H1 H2; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto.
 
246
  case Zodd_ex with (1 := H2); intros y H4; try rewrite H4; auto.
 
247
  replace (2 * x + (2 * y + 1)) with (2 * (x + y) + 1); try apply Zodd_2p_plus_1; auto with zarith.
 
248
  rewrite Zmult_plus_distr_r, Zplus_assoc; auto.
 
249
Qed.
 
250
 
 
251
Theorem Zeven_plus_Zeven: forall a b,
 
252
 Zeven a -> Zeven b -> Zeven (a + b).
 
253
Proof.
 
254
  intros a b H1 H2; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto.
 
255
  case Zeven_ex with (1 := H2); intros y H4; try rewrite H4; auto.
 
256
  replace (2 * x + 2 * y) with (2 * (x + y)); try apply Zeven_2p; auto with zarith.
 
257
  apply Zmult_plus_distr_r; auto.
 
258
Qed.
 
259
 
 
260
Theorem Zodd_plus_Zeven: forall a b, 
 
261
 Zodd a -> Zeven b -> Zodd (a + b).
 
262
Proof.
 
263
  intros a b H1 H2; rewrite Zplus_comm; apply Zeven_plus_Zodd; auto.
 
264
Qed.
 
265
 
 
266
Theorem Zodd_plus_Zodd: forall a b, 
 
267
 Zodd a -> Zodd b -> Zeven (a + b).
 
268
Proof.
 
269
  intros a b H1 H2; case Zodd_ex with (1 := H1); intros x H3; try rewrite H3; auto.
 
270
  case Zodd_ex with (1 := H2); intros y H4; try rewrite H4; auto.
 
271
  replace ((2 * x + 1) + (2 * y + 1)) with (2 * (x + y + 1)); try apply Zeven_2p; auto.
 
272
  (* ring part *)
 
273
  do 2 rewrite Zmult_plus_distr_r; auto.
 
274
  repeat rewrite <- Zplus_assoc; f_equal.
 
275
  rewrite (Zplus_comm 1).
 
276
  repeat rewrite <- Zplus_assoc; auto.
 
277
Qed.
 
278
 
 
279
Theorem Zeven_mult_Zeven_l: forall a b, 
 
280
 Zeven a -> Zeven (a * b).
 
281
Proof.
 
282
  intros a b H1; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto.
 
283
  replace (2 * x * b) with (2 * (x * b)); try apply Zeven_2p; auto with zarith.
 
284
  (* ring part *)
 
285
  apply Zmult_assoc.
 
286
Qed.
 
287
 
 
288
Theorem Zeven_mult_Zeven_r: forall a b, 
 
289
 Zeven b -> Zeven (a * b).
 
290
Proof.
 
291
  intros a b H1; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto.
 
292
  replace (a * (2 * x)) with (2 * (x * a)); try apply Zeven_2p; auto.
 
293
  (* ring part *)
 
294
  rewrite (Zmult_comm x a).
 
295
  do 2 rewrite Zmult_assoc.
 
296
  rewrite (Zmult_comm 2 a); auto.
 
297
Qed.
 
298
 
 
299
Hint Rewrite Zmult_plus_distr_r Zmult_plus_distr_l 
 
300
     Zplus_assoc Zmult_1_r Zmult_1_l : Zexpand.
 
301
 
 
302
Theorem Zodd_mult_Zodd: forall a b, 
 
303
 Zodd a -> Zodd b -> Zodd (a * b).
 
304
Proof.
 
305
  intros a b H1 H2; case Zodd_ex with (1 := H1); intros x H3; try rewrite H3; auto.
 
306
  case Zodd_ex with (1 := H2); intros y H4; try rewrite H4; auto.
 
307
  replace ((2 * x + 1) * (2 * y + 1)) with (2 * (2 * x * y + x + y) + 1); try apply Zodd_2p_plus_1; auto.
 
308
  (* ring part *)
 
309
  autorewrite with Zexpand; f_equal.
 
310
  repeat rewrite <- Zplus_assoc; f_equal.
 
311
  repeat rewrite <- Zmult_assoc; f_equal. 
 
312
  repeat rewrite Zmult_assoc; f_equal; apply Zmult_comm.
 
313
Qed.
 
314
 
 
315
(* for compatibility *)
 
316
Close Scope Z_scope.