← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/ZArith/BinInt.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/BinInt.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: BinInt.v 11015 2008-05-28 20:06:42Z herbelin $ i*)
 
10
 
 
11
(***********************************************************)
 
12
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 
13
(***********************************************************)
 
14
 
 
15
Require Export BinPos.
 
16
Require Export Pnat.
 
17
Require Import BinNat.
 
18
Require Import Plus.
 
19
Require Import Mult.
 
20
 
 
21
Unset Boxed Definitions.
 
22
 
 
23
(*****************************)
 
24
(** * Binary integer numbers *)
 
25
 
 
26
Inductive Z : Set :=
 
27
  | Z0 : Z
 
28
  | Zpos : positive -> Z
 
29
  | Zneg : positive -> Z.
 
30
 
 
31
 
 
32
(** Automatically open scope positive_scope for the constructors of Z *)
 
33
Delimit Scope Z_scope with Z.
 
34
Bind Scope Z_scope with Z.
 
35
Arguments Scope Zpos [positive_scope].
 
36
Arguments Scope Zneg [positive_scope].
 
37
 
 
38
(** ** Subtraction of positive into Z *)
 
39
 
 
40
Definition Zdouble_plus_one (x:Z) :=
 
41
  match x with
 
42
    | Z0 => Zpos 1
 
43
    | Zpos p => Zpos p~1
 
44
    | Zneg p => Zneg (Pdouble_minus_one p)
 
45
  end.
 
46
 
 
47
Definition Zdouble_minus_one (x:Z) :=
 
48
  match x with
 
49
    | Z0 => Zneg 1
 
50
    | Zneg p => Zneg p~1
 
51
    | Zpos p => Zpos (Pdouble_minus_one p)
 
52
  end.
 
53
 
 
54
Definition Zdouble (x:Z) :=
 
55
  match x with
 
56
    | Z0 => Z0
 
57
    | Zpos p => Zpos p~0
 
58
    | Zneg p => Zneg p~0
 
59
  end.
 
60
 
 
61
Open Local Scope positive_scope.
 
62
 
 
63
Fixpoint ZPminus (x y:positive) {struct y} : Z :=
 
64
  match x, y with
 
65
    | p~1, q~1 => Zdouble (ZPminus p q)
 
66
    | p~1, q~0 => Zdouble_plus_one (ZPminus p q)
 
67
    | p~1, 1 => Zpos p~0
 
68
    | p~0, q~1 => Zdouble_minus_one (ZPminus p q)
 
69
    | p~0, q~0 => Zdouble (ZPminus p q)
 
70
    | p~0, 1 => Zpos (Pdouble_minus_one p)
 
71
    | 1, q~1 => Zneg q~0
 
72
    | 1, q~0 => Zneg (Pdouble_minus_one q)
 
73
    | 1, 1 => Z0
 
74
  end.
 
75
 
 
76
Close Local Scope positive_scope.
 
77
 
 
78
(** ** Addition on integers *)
 
79
 
 
80
Definition Zplus (x y:Z) :=
 
81
  match x, y with
 
82
    | Z0, y => y
 
83
    | Zpos x', Z0 => Zpos x'
 
84
    | Zneg x', Z0 => Zneg x'
 
85
    | Zpos x', Zpos y' => Zpos (x' + y')
 
86
    | Zpos x', Zneg y' =>
 
87
      match (x' ?= y')%positive Eq with
 
88
        | Eq => Z0
 
89
        | Lt => Zneg (y' - x')
 
90
        | Gt => Zpos (x' - y')
 
91
      end
 
92
    | Zneg x', Zpos y' =>
 
93
      match (x' ?= y')%positive Eq with
 
94
        | Eq => Z0
 
95
        | Lt => Zpos (y' - x')
 
96
        | Gt => Zneg (x' - y')
 
97
      end
 
98
    | Zneg x', Zneg y' => Zneg (x' + y')
 
99
  end.
 
100
 
 
101
Infix "+" := Zplus : Z_scope.
 
102
 
 
103
(** ** Opposite *)
 
104
 
 
105
Definition Zopp (x:Z) :=
 
106
  match x with
 
107
    | Z0 => Z0
 
108
    | Zpos x => Zneg x
 
109
    | Zneg x => Zpos x
 
110
  end.
 
111
 
 
112
Notation "- x" := (Zopp x) : Z_scope.
 
113
 
 
114
(** ** Successor on integers *)
 
115
 
 
116
Definition Zsucc (x:Z) := (x + Zpos 1)%Z.
 
117
 
 
118
(** ** Predecessor on integers *)
 
119
 
 
120
Definition Zpred (x:Z) := (x + Zneg 1)%Z.
 
121
 
 
122
(** ** Subtraction on integers *)
 
123
 
 
124
Definition Zminus (m n:Z) := (m + - n)%Z.
 
125
 
 
126
Infix "-" := Zminus : Z_scope.
 
127
 
 
128
(** ** Multiplication on integers *)
 
129
 
 
130
Definition Zmult (x y:Z) :=
 
131
  match x, y with
 
132
    | Z0, _ => Z0
 
133
    | _, Z0 => Z0
 
134
    | Zpos x', Zpos y' => Zpos (x' * y')
 
135
    | Zpos x', Zneg y' => Zneg (x' * y')
 
136
    | Zneg x', Zpos y' => Zneg (x' * y')
 
137
    | Zneg x', Zneg y' => Zpos (x' * y')
 
138
  end.
 
139
 
 
140
Infix "*" := Zmult : Z_scope.
 
141
 
 
142
(** ** Comparison of integers *)
 
143
 
 
144
Definition Zcompare (x y:Z) :=
 
145
  match x, y with
 
146
    | Z0, Z0 => Eq
 
147
    | Z0, Zpos y' => Lt
 
148
    | Z0, Zneg y' => Gt
 
149
    | Zpos x', Z0 => Gt
 
150
    | Zpos x', Zpos y' => (x' ?= y')%positive Eq
 
151
    | Zpos x', Zneg y' => Gt
 
152
    | Zneg x', Z0 => Lt
 
153
    | Zneg x', Zpos y' => Lt
 
154
    | Zneg x', Zneg y' => CompOpp ((x' ?= y')%positive Eq)
 
155
  end.
 
156
 
 
157
Infix "?=" := Zcompare (at level 70, no associativity) : Z_scope.
 
158
 
 
159
Ltac elim_compare com1 com2 :=
 
160
  case (Dcompare (com1 ?= com2)%Z);
 
161
    [ idtac | let x := fresh "H" in
 
162
      (intro x; case x; clear x) ].
 
163
 
 
164
(** ** Sign function *)
 
165
 
 
166
Definition Zsgn (z:Z) : Z :=
 
167
  match z with
 
168
    | Z0 => Z0
 
169
    | Zpos p => Zpos 1
 
170
    | Zneg p => Zneg 1
 
171
  end.
 
172
 
 
173
(** ** Direct, easier to handle variants of successor and addition *)
 
174
 
 
175
Definition Zsucc' (x:Z) :=
 
176
  match x with
 
177
    | Z0 => Zpos 1
 
178
    | Zpos x' => Zpos (Psucc x')
 
179
    | Zneg x' => ZPminus 1 x'
 
180
  end.
 
181
 
 
182
Definition Zpred' (x:Z) :=
 
183
  match x with
 
184
    | Z0 => Zneg 1
 
185
    | Zpos x' => ZPminus x' 1
 
186
    | Zneg x' => Zneg (Psucc x')
 
187
  end.
 
188
 
 
189
Definition Zplus' (x y:Z) :=
 
190
  match x, y with
 
191
    | Z0, y => y
 
192
    | x, Z0 => x
 
193
    | Zpos x', Zpos y' => Zpos (x' + y')
 
194
    | Zpos x', Zneg y' => ZPminus x' y'
 
195
    | Zneg x', Zpos y' => ZPminus y' x'
 
196
    | Zneg x', Zneg y' => Zneg (x' + y')
 
197
  end.
 
198
 
 
199
Open Local Scope Z_scope.
 
200
 
 
201
(**********************************************************************)
 
202
(** ** Inductive specification of Z *)
 
203
 
 
204
Theorem Zind :
 
205
  forall P:Z -> Prop,
 
206
    P Z0 ->
 
207
    (forall x:Z, P x -> P (Zsucc' x)) ->
 
208
    (forall x:Z, P x -> P (Zpred' x)) -> forall n:Z, P n.
 
209
Proof.
 
210
  intros P H0 Hs Hp z; destruct z.
 
211
  assumption.
 
212
  apply Pind with (P := fun p => P (Zpos p)).
 
213
    change (P (Zsucc' Z0)) in |- *; apply Hs; apply H0.
 
214
    intro n; exact (Hs (Zpos n)).
 
215
  apply Pind with (P := fun p => P (Zneg p)).
 
216
    change (P (Zpred' Z0)) in |- *; apply Hp; apply H0.
 
217
    intro n; exact (Hp (Zneg n)).
 
218
Qed.
 
219
 
 
220
(**********************************************************************)
 
221
(** * Misc properties about binary integer operations *)
 
222
 
 
223
 
 
224
(**********************************************************************)
 
225
 
 
226
(** ** Properties of opposite on binary integer numbers *)
 
227
 
 
228
Theorem Zopp_neg : forall p:positive, - Zneg p = Zpos p.
 
229
Proof.
 
230
  reflexivity.
 
231
Qed.
 
232
 
 
233
(** [opp] is involutive *)
 
234
 
 
235
Theorem Zopp_involutive : forall n:Z, - - n = n.
 
236
Proof.
 
237
  intro x; destruct x; reflexivity.
 
238
Qed.
 
239
 
 
240
(** Injectivity of the opposite *)
 
241
 
 
242
Theorem Zopp_inj : forall n m:Z, - n = - m -> n = m.
 
243
Proof.
 
244
  intros x y; case x; case y; simpl in |- *; intros;
 
245
    [ trivial
 
246
      | discriminate H
 
247
      | discriminate H
 
248
      | discriminate H
 
249
      | simplify_eq H; intro E; rewrite E; trivial
 
250
      | discriminate H
 
251
      | discriminate H
 
252
      | discriminate H
 
253
      | simplify_eq H; intro E; rewrite E; trivial ].
 
254
Qed.
 
255
 
 
256
(**********************************************************************)
 
257
(** ** Other properties of binary integer numbers *)
 
258
 
 
259
Lemma ZL0 : 2%nat = (1 + 1)%nat.
 
260
Proof.
 
261
  reflexivity.
 
262
Qed.
 
263
 
 
264
(**********************************************************************)
 
265
(** * Properties of the addition on integers *)
 
266
 
 
267
(** ** zero is left neutral for addition *)
 
268
 
 
269
Theorem Zplus_0_l : forall n:Z, Z0 + n = n.
 
270
Proof.
 
271
  intro x; destruct x; reflexivity.
 
272
Qed.
 
273
 
 
274
(** *** zero is right neutral for addition *)
 
275
 
 
276
Theorem Zplus_0_r : forall n:Z, n + Z0 = n.
 
277
Proof.
 
278
  intro x; destruct x; reflexivity.
 
279
Qed.
 
280
 
 
281
(** ** addition is commutative *)
 
282
 
 
283
Theorem Zplus_comm : forall n m:Z, n + m = m + n.
 
284
Proof.
 
285
  intro x; induction x as [| p| p]; intro y; destruct y as [| q| q];
 
286
    simpl in |- *; try reflexivity.
 
287
  rewrite Pplus_comm; reflexivity.
 
288
  rewrite ZC4; destruct ((q ?= p)%positive Eq); reflexivity.
 
289
  rewrite ZC4; destruct ((q ?= p)%positive Eq); reflexivity.
 
290
  rewrite Pplus_comm; reflexivity.
 
291
Qed.
 
292
 
 
293
(** ** opposite distributes over addition *)
 
294
 
 
295
Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m.
 
296
Proof.
 
297
  intro x; destruct x as [| p| p]; intro y; destruct y as [| q| q];
 
298
    simpl in |- *; reflexivity || destruct ((p ?= q)%positive Eq);
 
299
      reflexivity.
 
300
Qed.
 
301
 
 
302
Theorem Zopp_succ : forall n:Z, Zopp (Zsucc n) = Zpred (Zopp n).
 
303
Proof.
 
304
intro; unfold Zsucc; now rewrite Zopp_plus_distr.
 
305
Qed.
 
306
 
 
307
(** ** opposite is inverse for addition *)
 
308
 
 
309
Theorem Zplus_opp_r : forall n:Z, n + - n = Z0.
 
310
Proof.
 
311
  intro x; destruct x as [| p| p]; simpl in |- *;
 
312
    [ reflexivity
 
313
      | rewrite (Pcompare_refl p); reflexivity
 
314
      | rewrite (Pcompare_refl p); reflexivity ].
 
315
Qed.
 
316
 
 
317
Theorem Zplus_opp_l : forall n:Z, - n + n = Z0.
 
318
Proof.
 
319
  intro; rewrite Zplus_comm; apply Zplus_opp_r.
 
320
Qed.
 
321
 
 
322
Hint Local Resolve Zplus_0_l Zplus_0_r.
 
323
 
 
324
(** ** addition is associative *)
 
325
 
 
326
Lemma weak_assoc :
 
327
  forall (p q:positive) (n:Z), Zpos p + (Zpos q + n) = Zpos p + Zpos q + n.
 
328
Proof.
 
329
  intros x y z'; case z';
 
330
    [ auto with arith
 
331
      | intros z; simpl in |- *; rewrite Pplus_assoc; auto with arith
 
332
      | intros z; simpl in |- *; ElimPcompare y z; intros E0; rewrite E0;
 
333
        ElimPcompare (x + y)%positive z; intros E1; rewrite E1;
 
334
          [ absurd ((x + y ?= z)%positive Eq = Eq);
 
335
            [  (* Case 1 *)
 
336
              rewrite nat_of_P_gt_Gt_compare_complement_morphism;
 
337
                [ discriminate
 
338
                  | rewrite nat_of_P_plus_morphism; rewrite (Pcompare_Eq_eq y z E0);
 
339
                    elim (ZL4 x); intros k E2; rewrite E2; 
 
340
                      simpl in |- *; unfold gt, lt in |- *; 
 
341
                        apply le_n_S; apply le_plus_r ]
 
342
              | assumption ]
 
343
            | absurd ((x + y ?= z)%positive Eq = Lt);
 
344
              [  (* Case 2 *)
 
345
                rewrite nat_of_P_gt_Gt_compare_complement_morphism;
 
346
                  [ discriminate
 
347
                    | rewrite nat_of_P_plus_morphism; rewrite (Pcompare_Eq_eq y z E0);
 
348
                      elim (ZL4 x); intros k E2; rewrite E2; 
 
349
                        simpl in |- *; unfold gt, lt in |- *; 
 
350
                          apply le_n_S; apply le_plus_r ]
 
351
                | assumption ]
 
352
            | rewrite (Pcompare_Eq_eq y z E0);
 
353
          (* Case 3 *)
 
354
              elim (Pminus_mask_Gt (x + z) z);
 
355
                [ intros t H; elim H; intros H1 H2; elim H2; intros H3 H4;
 
356
                  unfold Pminus in |- *; rewrite H1; cut (x = t);
 
357
                    [ intros E; rewrite E; auto with arith
 
358
                      | apply Pplus_reg_r with (r := z); rewrite <- H3;
 
359
                        rewrite Pplus_comm; trivial with arith ]
 
360
                  | pattern z at 1 in |- *; rewrite <- (Pcompare_Eq_eq y z E0);
 
361
                    assumption ]
 
362
            | elim (Pminus_mask_Gt z y);
 
363
              [  (* Case 4 *)
 
364
                intros k H; elim H; intros H1 H2; elim H2; intros H3 H4;
 
365
                  unfold Pminus at 1 in |- *; rewrite H1; cut (x = k);
 
366
                    [ intros E; rewrite E; rewrite (Pcompare_refl k);
 
367
                      trivial with arith
 
368
                      | apply Pplus_reg_r with (r := y); rewrite (Pplus_comm k y);
 
369
                        rewrite H3; apply Pcompare_Eq_eq; assumption ]
 
370
                | apply ZC2; assumption ]
 
371
            | elim (Pminus_mask_Gt z y);
 
372
              [  (* Case 5 *)
 
373
                intros k H; elim H; intros H1 H2; elim H2; intros H3 H4;
 
374
                  unfold Pminus at 1 3 5 in |- *; rewrite H1;
 
375
                    cut ((x ?= k)%positive Eq = Lt);
 
376
                      [ intros E2; rewrite E2; elim (Pminus_mask_Gt k x);
 
377
                        [ intros i H5; elim H5; intros H6 H7; elim H7; intros H8 H9;
 
378
                          elim (Pminus_mask_Gt z (x + y));
 
379
                            [ intros j H10; elim H10; intros H11 H12; elim H12;
 
380
                              intros H13 H14; unfold Pminus in |- *; 
 
381
                                rewrite H6; rewrite H11; cut (i = j);
 
382
                                  [ intros E; rewrite E; auto with arith
 
383
                                    | apply (Pplus_reg_l (x + y)); rewrite H13;
 
384
                                      rewrite (Pplus_comm x y); rewrite <- Pplus_assoc;
 
385
                                        rewrite H8; assumption ]
 
386
                              | apply ZC2; assumption ]
 
387
                          | apply ZC2; assumption ]
 
388
                        | apply nat_of_P_lt_Lt_compare_complement_morphism;
 
389
                          apply plus_lt_reg_l with (p := nat_of_P y);
 
390
                            do 2 rewrite <- nat_of_P_plus_morphism;
 
391
                              apply nat_of_P_lt_Lt_compare_morphism; 
 
392
                                rewrite H3; rewrite Pplus_comm; assumption ]
 
393
                | apply ZC2; assumption ]
 
394
            | elim (Pminus_mask_Gt z y);
 
395
              [  (* Case 6 *)
 
396
                intros k H; elim H; intros H1 H2; elim H2; intros H3 H4;
 
397
                  elim (Pminus_mask_Gt (x + y) z);
 
398
                    [ intros i H5; elim H5; intros H6 H7; elim H7; intros H8 H9;
 
399
                      unfold Pminus in |- *; rewrite H1; rewrite H6;
 
400
                        cut ((x ?= k)%positive Eq = Gt);
 
401
                          [ intros H10; elim (Pminus_mask_Gt x k H10); intros j H11;
 
402
                            elim H11; intros H12 H13; elim H13; 
 
403
                              intros H14 H15; rewrite H10; rewrite H12; 
 
404
                                cut (i = j);
 
405
                                  [ intros H16; rewrite H16; auto with arith
 
406
                                    | apply (Pplus_reg_l (z + k)); rewrite <- (Pplus_assoc z k j);
 
407
                                      rewrite H14; rewrite (Pplus_comm z k);
 
408
                                        rewrite <- Pplus_assoc; rewrite H8;
 
409
                                          rewrite (Pplus_comm x y); rewrite Pplus_assoc;
 
410
                                            rewrite (Pplus_comm k y); rewrite H3; 
 
411
                                              trivial with arith ]
 
412
                            | apply nat_of_P_gt_Gt_compare_complement_morphism;
 
413
                              unfold lt, gt in |- *;
 
414
                                apply plus_lt_reg_l with (p := nat_of_P y);
 
415
                                  do 2 rewrite <- nat_of_P_plus_morphism;
 
416
                                    apply nat_of_P_lt_Lt_compare_morphism; 
 
417
                                      rewrite H3; rewrite Pplus_comm; apply ZC1; 
 
418
                                        assumption ]
 
419
                      | assumption ]
 
420
                | apply ZC2; assumption ]
 
421
            | absurd ((x + y ?= z)%positive Eq = Eq);
 
422
              [  (* Case 7 *)
 
423
                rewrite nat_of_P_gt_Gt_compare_complement_morphism;
 
424
                  [ discriminate
 
425
                    | rewrite nat_of_P_plus_morphism; unfold gt in |- *;
 
426
                      apply lt_le_trans with (m := nat_of_P y);
 
427
                        [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption
 
428
                          | apply le_plus_r ] ]
 
429
                | assumption ]
 
430
            | absurd ((x + y ?= z)%positive Eq = Lt);
 
431
              [  (* Case 8 *)
 
432
                rewrite nat_of_P_gt_Gt_compare_complement_morphism;
 
433
                  [ discriminate
 
434
                    | unfold gt in |- *; apply lt_le_trans with (m := nat_of_P y);
 
435
                      [ exact (nat_of_P_gt_Gt_compare_morphism y z E0)
 
436
                        | rewrite nat_of_P_plus_morphism; apply le_plus_r ] ]
 
437
                | assumption ]
 
438
            | elim Pminus_mask_Gt with (1 := E0); intros k H1;
 
439
          (* Case 9 *)
 
440
              elim Pminus_mask_Gt with (1 := E1); intros i H2; 
 
441
                elim H1; intros H3 H4; elim H4; intros H5 H6; 
 
442
                  elim H2; intros H7 H8; elim H8; intros H9 H10; 
 
443
                    unfold Pminus in |- *; rewrite H3; rewrite H7;
 
444
                      cut ((x + k)%positive = i);
 
445
                        [ intros E; rewrite E; auto with arith
 
446
                          | apply (Pplus_reg_l z); rewrite (Pplus_comm x k); rewrite Pplus_assoc;
 
447
                            rewrite H5; rewrite H9; rewrite Pplus_comm; 
 
448
                              trivial with arith ] ] ].
 
449
Qed.
 
450
 
 
451
Hint Local Resolve weak_assoc.
 
452
 
 
453
Theorem Zplus_assoc : forall n m p:Z, n + (m + p) = n + m + p.
 
454
Proof.
 
455
  intros x y z; case x; case y; case z; auto with arith; intros;
 
456
    [ rewrite (Zplus_comm (Zneg p0)); rewrite weak_assoc;
 
457
      rewrite (Zplus_comm (Zpos p1 + Zneg p0)); rewrite weak_assoc;
 
458
        rewrite (Zplus_comm (Zpos p1)); trivial with arith
 
459
      | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg;
 
460
        rewrite Zplus_comm; rewrite <- weak_assoc;
 
461
          rewrite (Zplus_comm (- Zpos p1));
 
462
            rewrite (Zplus_comm (Zpos p0 + - Zpos p1)); rewrite (weak_assoc p);
 
463
              rewrite weak_assoc; rewrite (Zplus_comm (Zpos p0)); 
 
464
                trivial with arith
 
465
      | rewrite Zplus_comm; rewrite (Zplus_comm (Zpos p0) (Zpos p));
 
466
        rewrite <- weak_assoc; rewrite Zplus_comm; rewrite (Zplus_comm (Zpos p0));
 
467
          trivial with arith
 
468
      | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg;
 
469
        rewrite (Zplus_comm (- Zpos p0)); rewrite weak_assoc;
 
470
          rewrite (Zplus_comm (Zpos p1 + - Zpos p0)); rewrite weak_assoc;
 
471
            rewrite (Zplus_comm (Zpos p)); trivial with arith
 
472
      | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg;
 
473
        apply weak_assoc
 
474
      | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg;
 
475
        apply weak_assoc ].
 
476
Qed.
 
477
 
 
478
 
 
479
Lemma Zplus_assoc_reverse : forall n m p:Z, n + m + p = n + (m + p).
 
480
Proof.
 
481
  intros; symmetry  in |- *; apply Zplus_assoc.
 
482
Qed.
 
483
 
 
484
(** ** Associativity mixed with commutativity *)
 
485
 
 
486
Theorem Zplus_permute : forall n m p:Z, n + (m + p) = m + (n + p).
 
487
Proof.
 
488
  intros n m p; rewrite Zplus_comm; rewrite <- Zplus_assoc;
 
489
    rewrite (Zplus_comm p n); trivial with arith.
 
490
Qed.
 
491
 
 
492
(** ** addition simplifies *)
 
493
 
 
494
Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p.
 
495
  intros n m p H; cut (- n + (n + m) = - n + (n + p));
 
496
    [ do 2 rewrite Zplus_assoc; rewrite (Zplus_comm (- n) n);
 
497
      rewrite Zplus_opp_r; simpl in |- *; trivial with arith
 
498
      | rewrite H; trivial with arith ].
 
499
Qed.
 
500
 
 
501
(** ** addition and successor permutes *)
 
502
 
 
503
Lemma Zplus_succ_l : forall n m:Z, Zsucc n + m = Zsucc (n + m).
 
504
Proof.
 
505
  intros x y; unfold Zsucc in |- *; rewrite (Zplus_comm (x + y));
 
506
    rewrite Zplus_assoc; rewrite (Zplus_comm (Zpos 1)); 
 
507
      trivial with arith.
 
508
Qed.
 
509
 
 
510
Lemma Zplus_succ_r_reverse : forall n m:Z, Zsucc (n + m) = n + Zsucc m.
 
511
Proof.
 
512
  intros n m; unfold Zsucc in |- *; rewrite Zplus_assoc; trivial with arith.
 
513
Qed.
 
514
 
 
515
Notation Zplus_succ_r := Zplus_succ_r_reverse (only parsing).
 
516
 
 
517
Lemma Zplus_succ_comm : forall n m:Z, Zsucc n + m = n + Zsucc m.
 
518
Proof.
 
519
  unfold Zsucc in |- *; intros n m; rewrite <- Zplus_assoc;
 
520
    rewrite (Zplus_comm (Zpos 1)); trivial with arith.
 
521
Qed.
 
522
 
 
523
(** ** Misc properties, usually redundant or non natural *)
 
524
 
 
525
Lemma Zplus_0_r_reverse : forall n:Z, n = n + Z0.
 
526
Proof.
 
527
  symmetry  in |- *; apply Zplus_0_r.
 
528
Qed.
 
529
 
 
530
Lemma Zplus_0_simpl_l : forall n m:Z, n + Z0 = m -> n = m.
 
531
Proof.
 
532
  intros n m; rewrite Zplus_0_r; intro; assumption.
 
533
Qed.
 
534
 
 
535
Lemma Zplus_0_simpl_l_reverse : forall n m:Z, n = m + Z0 -> n = m.
 
536
Proof.
 
537
  intros n m; rewrite Zplus_0_r; intro; assumption.
 
538
Qed.
 
539
 
 
540
Lemma Zplus_eq_compat : forall n m p q:Z, n = m -> p = q -> n + p = m + q.
 
541
Proof.
 
542
  intros; rewrite H; rewrite H0; reflexivity.
 
543
Qed.
 
544
 
 
545
Lemma Zplus_opp_expand : forall n m p:Z, n + - m = n + - p + (p + - m).
 
546
Proof.
 
547
  intros x y z.
 
548
  rewrite <- (Zplus_assoc x).
 
549
  rewrite (Zplus_assoc (- z)).
 
550
  rewrite Zplus_opp_l.
 
551
  reflexivity.
 
552
Qed.
 
553
 
 
554
(************************************************************************)
 
555
(** * Properties of successor and predecessor on binary integer numbers *)
 
556
 
 
557
Theorem Zsucc_discr : forall n:Z, n <> Zsucc n.
 
558
Proof.
 
559
  intros n; cut (Z0 <> Zpos 1);
 
560
    [ unfold not in |- *; intros H1 H2; apply H1; apply (Zplus_reg_l n);
 
561
      rewrite Zplus_0_r; exact H2
 
562
      | discriminate ].
 
563
Qed.
 
564
 
 
565
Theorem Zpos_succ_morphism :
 
566
  forall p:positive, Zpos (Psucc p) = Zsucc (Zpos p).
 
567
Proof.
 
568
  intro; rewrite Pplus_one_succ_r; unfold Zsucc in |- *; simpl in |- *;
 
569
    trivial with arith.
 
570
Qed.
 
571
 
 
572
(** successor and predecessor are inverse functions *)
 
573
 
 
574
Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n).
 
575
Proof.
 
576
  intros n; unfold Zsucc, Zpred in |- *; rewrite <- Zplus_assoc; simpl in |- *;
 
577
    rewrite Zplus_0_r; trivial with arith.
 
578
Qed.
 
579
 
 
580
Hint Immediate Zsucc_pred: zarith.
 
581
 
 
582
Theorem Zpred_succ : forall n:Z, n = Zpred (Zsucc n).
 
583
Proof.
 
584
  intros m; unfold Zpred, Zsucc in |- *; rewrite <- Zplus_assoc; simpl in |- *;
 
585
    rewrite Zplus_comm; auto with arith.
 
586
Qed.
 
587
 
 
588
Theorem Zsucc_inj : forall n m:Z, Zsucc n = Zsucc m -> n = m.
 
589
Proof.
 
590
  intros n m H.
 
591
  change (Zneg 1 + Zpos 1 + n = Zneg 1 + Zpos 1 + m) in |- *;
 
592
    do 2 rewrite <- Zplus_assoc; do 2 rewrite (Zplus_comm (Zpos 1));
 
593
      unfold Zsucc in H; rewrite H; trivial with arith.
 
594
Qed.
 
595
 
 
596
(*************************************************************************)
 
597
(** **  Properties of the direct definition of successor and predecessor *)
 
598
 
 
599
Theorem Zsucc_succ' : forall n:Z, Zsucc n = Zsucc' n.
 
600
Proof.
 
601
destruct n as [| p | p]; simpl.
 
602
reflexivity.
 
603
now rewrite Pplus_one_succ_r.
 
604
now destruct p as [q | q |].
 
605
Qed.
 
606
 
 
607
Theorem Zpred_pred' : forall n:Z, Zpred n = Zpred' n.
 
608
Proof.
 
609
destruct n as [| p | p]; simpl.
 
610
reflexivity.
 
611
now destruct p as [q | q |].
 
612
now rewrite Pplus_one_succ_r.
 
613
Qed.
 
614
 
 
615
Theorem Zsucc'_inj : forall n m:Z, Zsucc' n = Zsucc' m -> n = m.
 
616
Proof.
 
617
intros n m; do 2 rewrite <- Zsucc_succ'; now apply Zsucc_inj.
 
618
Qed.
 
619
 
 
620
Theorem Zsucc'_pred' : forall n:Z, Zsucc' (Zpred' n) = n.
 
621
Proof.
 
622
intro; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred';
 
623
symmetry; apply Zsucc_pred.
 
624
Qed.
 
625
 
 
626
Theorem Zpred'_succ' : forall n:Z, Zpred' (Zsucc' n) = n.
 
627
Proof.
 
628
intro; apply Zsucc'_inj; now rewrite Zsucc'_pred'.
 
629
Qed.
 
630
 
 
631
Theorem Zpred'_inj : forall n m:Z, Zpred' n = Zpred' m -> n = m.
 
632
Proof.
 
633
intros n m H.
 
634
rewrite <- (Zsucc'_pred' n); rewrite <- (Zsucc'_pred' m); now rewrite H.
 
635
Qed.
 
636
 
 
637
Theorem Zsucc'_discr : forall n:Z, n <> Zsucc' n.
 
638
Proof.
 
639
  intro x; destruct x; simpl in |- *.
 
640
  discriminate.
 
641
  injection; apply Psucc_discr.
 
642
  destruct p; simpl in |- *.
 
643
    discriminate.
 
644
    intro H; symmetry  in H; injection H; apply double_moins_un_xO_discr.
 
645
    discriminate.
 
646
Qed.
 
647
 
 
648
(** Misc properties, usually redundant or non natural *)
 
649
 
 
650
Lemma Zsucc_eq_compat : forall n m:Z, n = m -> Zsucc n = Zsucc m.
 
651
Proof.
 
652
  intros n m H; rewrite H; reflexivity.
 
653
Qed.
 
654
 
 
655
Lemma Zsucc_inj_contrapositive : forall n m:Z, n <> m -> Zsucc n <> Zsucc m.
 
656
Proof.
 
657
  unfold not in |- *; intros n m H1 H2; apply H1; apply Zsucc_inj; assumption.
 
658
Qed.
 
659
 
 
660
(**********************************************************************)
 
661
(** * Properties of subtraction on binary integer numbers *)
 
662
 
 
663
(** ** [minus] and [Z0] *)
 
664
 
 
665
Lemma Zminus_0_r : forall n:Z, n - Z0 = n.
 
666
Proof.
 
667
  intro; unfold Zminus in |- *; simpl in |- *; rewrite Zplus_0_r;
 
668
    trivial with arith.
 
669
Qed.
 
670
 
 
671
Lemma Zminus_0_l_reverse : forall n:Z, n = n - Z0.
 
672
Proof.
 
673
  intro; symmetry  in |- *; apply Zminus_0_r.
 
674
Qed.
 
675
 
 
676
Lemma Zminus_diag : forall n:Z, n - n = Z0.
 
677
Proof.
 
678
  intro; unfold Zminus in |- *; rewrite Zplus_opp_r; trivial with arith.
 
679
Qed.
 
680
 
 
681
Lemma Zminus_diag_reverse : forall n:Z, Z0 = n - n.
 
682
Proof.
 
683
  intro; symmetry  in |- *; apply Zminus_diag.
 
684
Qed.
 
685
 
 
686
 
 
687
(** ** Relating [minus] with [plus] and [Zsucc] *)
 
688
 
 
689
Lemma Zminus_plus_distr : forall n m p:Z, n - (m + p) = n - m - p.
 
690
Proof.
 
691
intros; unfold Zminus; rewrite Zopp_plus_distr; apply Zplus_assoc.
 
692
Qed.
 
693
 
 
694
Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m.
 
695
Proof.
 
696
  intros n m; unfold Zminus, Zsucc in |- *; rewrite (Zplus_comm n (- m));
 
697
    rewrite <- Zplus_assoc; apply Zplus_comm.
 
698
Qed.
 
699
 
 
700
Lemma Zminus_succ_r : forall n m:Z, n - (Zsucc m) = Zpred (n - m).
 
701
Proof.
 
702
intros; unfold Zsucc; now rewrite Zminus_plus_distr.
 
703
Qed.
 
704
 
 
705
Lemma Zplus_minus_eq : forall n m p:Z, n = m + p -> p = n - m.
 
706
Proof.
 
707
  intros n m p H; unfold Zminus in |- *; apply (Zplus_reg_l m);
 
708
    rewrite (Zplus_comm m (n + - m)); rewrite <- Zplus_assoc;
 
709
      rewrite Zplus_opp_l; rewrite Zplus_0_r; rewrite H; 
 
710
        trivial with arith.
 
711
Qed.
 
712
 
 
713
Lemma Zminus_plus : forall n m:Z, n + m - n = m.
 
714
Proof.
 
715
  intros n m; unfold Zminus in |- *; rewrite (Zplus_comm n m);
 
716
    rewrite <- Zplus_assoc; rewrite Zplus_opp_r; apply Zplus_0_r.
 
717
Qed.
 
718
 
 
719
Lemma Zplus_minus : forall n m:Z, n + (m - n) = m.
 
720
Proof.
 
721
  unfold Zminus in |- *; intros n m; rewrite Zplus_permute; rewrite Zplus_opp_r;
 
722
    apply Zplus_0_r.
 
723
Qed.
 
724
 
 
725
Lemma Zminus_plus_simpl_l : forall n m p:Z, p + n - (p + m) = n - m.
 
726
Proof.
 
727
  intros n m p; unfold Zminus in |- *; rewrite Zopp_plus_distr;
 
728
    rewrite Zplus_assoc; rewrite (Zplus_comm p); rewrite <- (Zplus_assoc n p);
 
729
      rewrite Zplus_opp_r; rewrite Zplus_0_r; trivial with arith.
 
730
Qed.
 
731
 
 
732
Lemma Zminus_plus_simpl_l_reverse : forall n m p:Z, n - m = p + n - (p + m).
 
733
Proof.
 
734
  intros; symmetry  in |- *; apply Zminus_plus_simpl_l.
 
735
Qed.
 
736
 
 
737
Lemma Zminus_plus_simpl_r : forall n m p:Z, n + p - (m + p) = n - m.
 
738
Proof.
 
739
  intros x y n.
 
740
  unfold Zminus in |- *.
 
741
  rewrite Zopp_plus_distr.
 
742
  rewrite (Zplus_comm (- y) (- n)).
 
743
  rewrite Zplus_assoc.
 
744
  rewrite <- (Zplus_assoc x n (- n)).
 
745
  rewrite (Zplus_opp_r n).
 
746
  rewrite <- Zplus_0_r_reverse.
 
747
  reflexivity.
 
748
Qed.
 
749
 
 
750
Lemma Zpos_minus_morphism : forall a b:positive, Pcompare a b Eq = Lt -> 
 
751
  Zpos (b-a) = Zpos b - Zpos a.
 
752
Proof.
 
753
  intros.
 
754
  simpl.
 
755
  change Eq with (CompOpp Eq).
 
756
  rewrite <- Pcompare_antisym.
 
757
  rewrite H; simpl; auto.
 
758
Qed.
 
759
 
 
760
(** ** Misc redundant properties *)
 
761
 
 
762
Lemma Zeq_minus : forall n m:Z, n = m -> n - m = Z0.
 
763
Proof.
 
764
  intros x y H; rewrite H; symmetry  in |- *; apply Zminus_diag_reverse.
 
765
Qed.
 
766
 
 
767
Lemma Zminus_eq : forall n m:Z, n - m = Z0 -> n = m.
 
768
Proof.
 
769
  intros x y H; rewrite <- (Zplus_minus y x); rewrite H; apply Zplus_0_r.
 
770
Qed.
 
771
 
 
772
 
 
773
(**********************************************************************)
 
774
(** * Properties of multiplication on binary integer numbers *)
 
775
 
 
776
Theorem Zpos_mult_morphism : 
 
777
  forall p q:positive, Zpos (p*q) = Zpos p * Zpos q.
 
778
Proof.
 
779
  auto.
 
780
Qed.
 
781
 
 
782
(** ** One is neutral for multiplication *)
 
783
 
 
784
Theorem Zmult_1_l : forall n:Z, Zpos 1 * n = n.
 
785
Proof.
 
786
  intro x; destruct x; reflexivity.
 
787
Qed.
 
788
 
 
789
Theorem Zmult_1_r : forall n:Z, n * Zpos 1 = n.
 
790
Proof.
 
791
  intro x; destruct x; simpl in |- *; try rewrite Pmult_1_r; reflexivity.
 
792
Qed.
 
793
 
 
794
(** ** Zero property of multiplication *)
 
795
 
 
796
Theorem Zmult_0_l : forall n:Z, Z0 * n = Z0.
 
797
Proof.
 
798
  intro x; destruct x; reflexivity.
 
799
Qed.
 
800
 
 
801
Theorem Zmult_0_r : forall n:Z, n * Z0 = Z0.
 
802
Proof.
 
803
  intro x; destruct x; reflexivity.
 
804
Qed.
 
805
 
 
806
Hint Local Resolve Zmult_0_l Zmult_0_r.
 
807
 
 
808
Lemma Zmult_0_r_reverse : forall n:Z, Z0 = n * Z0.
 
809
Proof.
 
810
  intro x; destruct x; reflexivity.
 
811
Qed.
 
812
 
 
813
(** ** Commutativity of multiplication *)
 
814
 
 
815
Theorem Zmult_comm : forall n m:Z, n * m = m * n.
 
816
Proof.
 
817
  intros x y; destruct x as [| p| p]; destruct y as [| q| q]; simpl in |- *;
 
818
    try rewrite (Pmult_comm p q); reflexivity.
 
819
Qed.
 
820
 
 
821
(** ** Associativity of multiplication *)
 
822
 
 
823
Theorem Zmult_assoc : forall n m p:Z, n * (m * p) = n * m * p.
 
824
Proof.
 
825
  intros x y z; destruct x; destruct y; destruct z; simpl in |- *;
 
826
    try rewrite Pmult_assoc; reflexivity.
 
827
Qed.
 
828
 
 
829
Lemma Zmult_assoc_reverse : forall n m p:Z, n * m * p = n * (m * p).
 
830
Proof.
 
831
  intros n m p; rewrite Zmult_assoc; trivial with arith.
 
832
Qed.
 
833
 
 
834
(** ** Associativity mixed with commutativity *)
 
835
 
 
836
Theorem Zmult_permute : forall n m p:Z, n * (m * p) = m * (n * p).
 
837
Proof.
 
838
  intros x y z; rewrite (Zmult_assoc y x z); rewrite (Zmult_comm y x).
 
839
  apply Zmult_assoc.
 
840
Qed.
 
841
 
 
842
(** ** Z is integral *)
 
843
 
 
844
Theorem Zmult_integral_l : forall n m:Z, n <> Z0 -> m * n = Z0 -> m = Z0.
 
845
Proof.
 
846
  intros x y; destruct x as [| p| p].
 
847
  intro H; absurd (Z0 = Z0); trivial.
 
848
  intros _ H; destruct y as [| q| q]; reflexivity || discriminate.
 
849
  intros _ H; destruct y as [| q| q]; reflexivity || discriminate.
 
850
Qed.
 
851
 
 
852
 
 
853
Theorem Zmult_integral : forall n m:Z, n * m = Z0 -> n = Z0 \/ m = Z0.
 
854
Proof.
 
855
  intros x y; destruct x; destruct y; auto; simpl in |- *; intro H;
 
856
    discriminate H.
 
857
Qed.
 
858
 
 
859
 
 
860
Lemma Zmult_1_inversion_l :
 
861
  forall n m:Z, n * m = Zpos 1 -> n = Zpos 1 \/ n = Zneg 1.
 
862
Proof.
 
863
  intros x y; destruct x as [| p| p]; intro; [ discriminate | left | right ];
 
864
    (destruct y as [| q| q]; try discriminate; simpl in H; injection H; clear H;
 
865
      intro H; rewrite Pmult_1_inversion_l with (1 := H); 
 
866
        reflexivity).
 
867
Qed.
 
868
 
 
869
(** ** Multiplication and Doubling *)
 
870
 
 
871
Lemma Zdouble_mult : forall z, Zdouble z = (Zpos 2) * z.
 
872
Proof.
 
873
  reflexivity.
 
874
Qed.
 
875
 
 
876
Lemma Zdouble_plus_one_mult : forall z, 
 
877
  Zdouble_plus_one z = (Zpos 2) * z + (Zpos 1).
 
878
Proof.
 
879
  destruct z; simpl; auto with zarith.
 
880
Qed.
 
881
 
 
882
(** ** Multiplication and Opposite *)
 
883
 
 
884
Theorem Zopp_mult_distr_l : forall n m:Z, - (n * m) = - n * m.
 
885
Proof.
 
886
  intros x y; destruct x; destruct y; reflexivity.
 
887
Qed.
 
888
 
 
889
Theorem Zopp_mult_distr_r : forall n m:Z, - (n * m) = n * - m.
 
890
Proof.
 
891
  intros x y; rewrite (Zmult_comm x y); rewrite Zopp_mult_distr_l;
 
892
    apply Zmult_comm.
 
893
Qed.
 
894
 
 
895
Lemma Zopp_mult_distr_l_reverse : forall n m:Z, - n * m = - (n * m).
 
896
Proof.
 
897
  intros x y; symmetry  in |- *; apply Zopp_mult_distr_l.
 
898
Qed.
 
899
 
 
900
Theorem Zmult_opp_comm : forall n m:Z, - n * m = n * - m.
 
901
Proof.
 
902
  intros x y; rewrite Zopp_mult_distr_l_reverse; rewrite Zopp_mult_distr_r;
 
903
    trivial with arith.
 
904
Qed.
 
905
 
 
906
Theorem Zmult_opp_opp : forall n m:Z, - n * - m = n * m.
 
907
Proof.
 
908
  intros x y; destruct x; destruct y; reflexivity.
 
909
Qed.
 
910
 
 
911
Theorem Zopp_eq_mult_neg_1 : forall n:Z, - n = n * Zneg 1.
 
912
Proof.
 
913
  intro x; induction x; intros; rewrite Zmult_comm; auto with arith.
 
914
Qed.
 
915
 
 
916
(** ** Distributivity of multiplication over addition *)
 
917
 
 
918
Lemma weak_Zmult_plus_distr_r :
 
919
  forall (p:positive) (n m:Z), Zpos p * (n + m) = Zpos p * n + Zpos p * m.
 
920
Proof.
 
921
  intros x y' z'; case y'; case z'; auto with arith; intros y z;
 
922
    (simpl in |- *; rewrite Pmult_plus_distr_l; trivial with arith) ||
 
923
      (simpl in |- *; ElimPcompare z y; intros E0; rewrite E0;
 
924
        [ rewrite (Pcompare_Eq_eq z y E0); rewrite (Pcompare_refl (x * y));
 
925
          trivial with arith
 
926
          | cut ((x * z ?= x * y)%positive Eq = Lt);
 
927
            [ intros E; rewrite E; rewrite Pmult_minus_distr_l;
 
928
              [ trivial with arith | apply ZC2; assumption ]
 
929
              | apply nat_of_P_lt_Lt_compare_complement_morphism;
 
930
                do 2 rewrite nat_of_P_mult_morphism; elim (ZL4 x); 
 
931
                  intros h H1; rewrite H1; apply mult_S_lt_compat_l;
 
932
                    exact (nat_of_P_lt_Lt_compare_morphism z y E0) ]
 
933
          | cut ((x * z ?= x * y)%positive Eq = Gt);
 
934
            [ intros E; rewrite E; rewrite Pmult_minus_distr_l; auto with arith
 
935
              | apply nat_of_P_gt_Gt_compare_complement_morphism; unfold gt in |- *;
 
936
                do 2 rewrite nat_of_P_mult_morphism; elim (ZL4 x); 
 
937
                  intros h H1; rewrite H1; apply mult_S_lt_compat_l;
 
938
                    exact (nat_of_P_gt_Gt_compare_morphism z y E0) ] ]).
 
939
Qed.
 
940
 
 
941
Theorem Zmult_plus_distr_r : forall n m p:Z, n * (m + p) = n * m + n * p.
 
942
Proof.
 
943
  intros x y z; case x;
 
944
    [ auto with arith
 
945
      | intros x'; apply weak_Zmult_plus_distr_r
 
946
      | intros p; apply Zopp_inj; rewrite Zopp_plus_distr;
 
947
        do 3 rewrite <- Zopp_mult_distr_l_reverse; rewrite Zopp_neg;
 
948
          apply weak_Zmult_plus_distr_r ].
 
949
Qed.
 
950
 
 
951
Theorem Zmult_plus_distr_l : forall n m p:Z, (n + m) * p = n * p + m * p.
 
952
Proof.
 
953
  intros n m p; rewrite Zmult_comm; rewrite Zmult_plus_distr_r;
 
954
    do 2 rewrite (Zmult_comm p); trivial with arith.
 
955
Qed.
 
956
 
 
957
(** ** Distributivity of multiplication over subtraction *)
 
958
 
 
959
Lemma Zmult_minus_distr_r : forall n m p:Z, (n - m) * p = n * p - m * p.
 
960
Proof.
 
961
  intros x y z; unfold Zminus in |- *.
 
962
  rewrite <- Zopp_mult_distr_l_reverse.
 
963
  apply Zmult_plus_distr_l.
 
964
Qed.
 
965
 
 
966
 
 
967
Lemma Zmult_minus_distr_l : forall n m p:Z, p * (n - m) = p * n - p * m.
 
968
Proof.
 
969
  intros x y z; rewrite (Zmult_comm z (x - y)).
 
970
  rewrite (Zmult_comm z x).
 
971
  rewrite (Zmult_comm z y).
 
972
  apply Zmult_minus_distr_r.
 
973
Qed.
 
974
 
 
975
(** ** Simplification of multiplication for non-zero integers *)
 
976
 
 
977
Lemma Zmult_reg_l : forall n m p:Z, p <> Z0 -> p * n = p * m -> n = m.
 
978
Proof.
 
979
  intros x y z H H0.
 
980
  generalize (Zeq_minus _ _ H0).
 
981
  intro.
 
982
  apply Zminus_eq.
 
983
  rewrite <- Zmult_minus_distr_l in H1.
 
984
  clear H0; destruct (Zmult_integral _ _ H1).
 
985
  contradiction.
 
986
  trivial.
 
987
Qed.
 
988
 
 
989
Lemma Zmult_reg_r : forall n m p:Z, p <> Z0 -> n * p = m * p -> n = m.
 
990
Proof.
 
991
  intros x y z Hz.
 
992
  rewrite (Zmult_comm x z).
 
993
  rewrite (Zmult_comm y z).
 
994
  intro; apply Zmult_reg_l with z; assumption.
 
995
Qed.
 
996
 
 
997
(** ** Addition and multiplication by 2 *)
 
998
 
 
999
Lemma Zplus_diag_eq_mult_2 : forall n:Z, n + n = n * Zpos 2.
 
1000
Proof.
 
1001
  intros x; pattern x at 1 2 in |- *; rewrite <- (Zmult_1_r x);
 
1002
    rewrite <- Zmult_plus_distr_r; reflexivity.
 
1003
Qed.
 
1004
 
 
1005
(** ** Multiplication and successor *)
 
1006
 
 
1007
Lemma Zmult_succ_r : forall n m:Z, n * Zsucc m = n * m + n.
 
1008
Proof.
 
1009
  intros n m; unfold Zsucc in |- *; rewrite Zmult_plus_distr_r;
 
1010
    rewrite (Zmult_comm n (Zpos 1)); rewrite Zmult_1_l; 
 
1011
      trivial with arith.
 
1012
Qed.
 
1013
 
 
1014
Lemma Zmult_succ_r_reverse : forall n m:Z, n * m + n = n * Zsucc m.
 
1015
Proof.
 
1016
  intros; symmetry  in |- *; apply Zmult_succ_r.
 
1017
Qed.
 
1018
 
 
1019
Lemma Zmult_succ_l : forall n m:Z, Zsucc n * m = n * m + m.
 
1020
Proof.
 
1021
  intros n m; unfold Zsucc in |- *; rewrite Zmult_plus_distr_l;
 
1022
    rewrite Zmult_1_l; trivial with arith.
 
1023
Qed.
 
1024
 
 
1025
Lemma Zmult_succ_l_reverse : forall n m:Z, n * m + m = Zsucc n * m.
 
1026
Proof.
 
1027
  intros; symmetry  in |- *; apply Zmult_succ_l.
 
1028
Qed.
 
1029
 
 
1030
 
 
1031
 
 
1032
(** ** Misc redundant properties *)
 
1033
 
 
1034
Lemma Z_eq_mult : forall n m:Z, m = Z0 -> m * n = Z0.
 
1035
Proof.
 
1036
  intros x y H; rewrite H; auto with arith.
 
1037
Qed.
 
1038
 
 
1039
 
 
1040
 
 
1041
(**********************************************************************)
 
1042
(** * Relating binary positive numbers and binary integers *)
 
1043
 
 
1044
Lemma Zpos_eq : forall p q:positive, p = q -> Zpos p = Zpos q.
 
1045
Proof.
 
1046
  intros; f_equal; auto.
 
1047
Qed.
 
1048
 
 
1049
Lemma Zpos_eq_rev : forall p q:positive, Zpos p = Zpos q -> p = q.
 
1050
Proof.
 
1051
  inversion 1; auto.
 
1052
Qed.
 
1053
 
 
1054
Lemma Zpos_eq_iff : forall p q:positive, p = q <-> Zpos p = Zpos q.
 
1055
Proof.
 
1056
  split; [apply Zpos_eq|apply Zpos_eq_rev].
 
1057
Qed.
 
1058
 
 
1059
Lemma Zpos_xI : forall p:positive, Zpos p~1 = Zpos 2 * Zpos p + Zpos 1.
 
1060
Proof.
 
1061
  intro; apply refl_equal.
 
1062
Qed.
 
1063
 
 
1064
Lemma Zpos_xO : forall p:positive, Zpos p~0 = Zpos 2 * Zpos p.
 
1065
Proof.
 
1066
  intro; apply refl_equal.
 
1067
Qed.
 
1068
 
 
1069
Lemma Zneg_xI : forall p:positive, Zneg p~1 = Zpos 2 * Zneg p - Zpos 1.
 
1070
Proof.
 
1071
  intro; apply refl_equal.
 
1072
Qed.
 
1073
 
 
1074
Lemma Zneg_xO : forall p:positive, Zneg p~0 = Zpos 2 * Zneg p.
 
1075
Proof.
 
1076
  reflexivity.
 
1077
Qed.
 
1078
 
 
1079
Lemma Zpos_plus_distr : forall p q:positive, Zpos (p + q) = Zpos p + Zpos q.
 
1080
Proof.
 
1081
  intros p p'; destruct p;
 
1082
    [ destruct p' as [p0| p0| ]
 
1083
      | destruct p' as [p0| p0| ]
 
1084
      | destruct p' as [p| p| ] ]; reflexivity.
 
1085
Qed.
 
1086
 
 
1087
Lemma Zneg_plus_distr : forall p q:positive, Zneg (p + q) = Zneg p + Zneg q.
 
1088
Proof.
 
1089
  intros p p'; destruct p;
 
1090
    [ destruct p' as [p0| p0| ]
 
1091
      | destruct p' as [p0| p0| ]
 
1092
      | destruct p' as [p| p| ] ]; reflexivity.
 
1093
Qed.
 
1094
 
 
1095
(**********************************************************************)
 
1096
(** * Order relations *)
 
1097
 
 
1098
Definition Zlt (x y:Z) := (x ?= y) = Lt.
 
1099
Definition Zgt (x y:Z) := (x ?= y) = Gt.
 
1100
Definition Zle (x y:Z) := (x ?= y) <> Gt.
 
1101
Definition Zge (x y:Z) := (x ?= y) <> Lt.
 
1102
Definition Zne (x y:Z) := x <> y.
 
1103
 
 
1104
Infix "<=" := Zle : Z_scope.
 
1105
Infix "<" := Zlt : Z_scope.
 
1106
Infix ">=" := Zge : Z_scope.
 
1107
Infix ">" := Zgt : Z_scope.
 
1108
 
 
1109
Notation "x <= y <= z" := (x <= y /\ y <= z) : Z_scope.
 
1110
Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope.
 
1111
Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
 
1112
Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
 
1113
 
 
1114
(**********************************************************************)
 
1115
(** * Absolute value on integers *)
 
1116
 
 
1117
Definition Zabs_nat (x:Z) : nat :=
 
1118
  match x with
 
1119
    | Z0 => 0%nat
 
1120
    | Zpos p => nat_of_P p
 
1121
    | Zneg p => nat_of_P p
 
1122
  end.
 
1123
 
 
1124
Definition Zabs (z:Z) : Z :=
 
1125
  match z with
 
1126
    | Z0 => Z0
 
1127
    | Zpos p => Zpos p
 
1128
    | Zneg p => Zpos p
 
1129
  end.
 
1130
 
 
1131
(**********************************************************************)
 
1132
(** * From [nat] to [Z] *)
 
1133
 
 
1134
Definition Z_of_nat (x:nat) :=
 
1135
  match x with
 
1136
    | O => Z0
 
1137
    | S y => Zpos (P_of_succ_nat y)
 
1138
  end.
 
1139
 
 
1140
Require Import BinNat.
 
1141
 
 
1142
Definition Zabs_N (z:Z) :=
 
1143
  match z with
 
1144
    | Z0 => 0%N
 
1145
    | Zpos p => Npos p
 
1146
    | Zneg p => Npos p
 
1147
  end.
 
1148
 
 
1149
Definition Z_of_N (x:N) := 
 
1150
  match x with
 
1151
    | N0 => Z0
 
1152
    | Npos p => Zpos p
 
1153
  end.