← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/ZArith/Zcompare.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/Zcompare.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 $$ i*)
 
10
 
 
11
(**********************************************************************)
 
12
(** Binary Integers (Pierre Cr�gut, CNET, Lannion, France)            *)
 
13
(**********************************************************************)
 
14
 
 
15
Require Export BinPos.
 
16
Require Export BinInt.
 
17
Require Import Lt.
 
18
Require Import Gt.
 
19
Require Import Plus.
 
20
Require Import Mult.
 
21
 
 
22
Open Local Scope Z_scope.
 
23
 
 
24
(***************************)
 
25
(** * Comparison on integers *)
 
26
 
 
27
Lemma Zcompare_refl : forall n:Z, (n ?= n) = Eq.
 
28
Proof.
 
29
  intro x; destruct x as [| p| p]; simpl in |- *;
 
30
    [ reflexivity | apply Pcompare_refl | rewrite Pcompare_refl; reflexivity ].
 
31
Qed.
 
32
 
 
33
Lemma Zcompare_Eq_eq : forall n m:Z, (n ?= m) = Eq -> n = m.
 
34
Proof.
 
35
  intros x y; destruct x as [| x'| x']; destruct y as [| y'| y']; simpl in |- *;
 
36
    intro H; reflexivity || (try discriminate H);
 
37
      [ rewrite (Pcompare_Eq_eq x' y' H); reflexivity
 
38
        | rewrite (Pcompare_Eq_eq x' y');
 
39
          [ reflexivity
 
40
            | destruct ((x' ?= y')%positive Eq); reflexivity || discriminate ] ].
 
41
Qed.
 
42
 
 
43
Ltac destr_zcompare := 
 
44
 match goal with |- context [Zcompare ?x ?y] => 
 
45
  let H := fresh "H" in 
 
46
  case_eq (Zcompare x y); intro H;
 
47
   [generalize (Zcompare_Eq_eq _ _ H); clear H; intro H |
 
48
    change (x<y)%Z in H | 
 
49
    change (x>y)%Z in H ]
 
50
 end.
 
51
 
 
52
Lemma Zcompare_Eq_iff_eq : forall n m:Z, (n ?= m) = Eq <-> n = m.
 
53
Proof.
 
54
  intros x y; split; intro E;
 
55
    [ apply Zcompare_Eq_eq; assumption | rewrite E; apply Zcompare_refl ].
 
56
Qed.
 
57
 
 
58
Lemma Zcompare_antisym : forall n m:Z, CompOpp (n ?= m) = (m ?= n).
 
59
Proof.
 
60
  intros x y; destruct x; destruct y; simpl in |- *;
 
61
    reflexivity || discriminate H || rewrite Pcompare_antisym; 
 
62
      reflexivity.
 
63
Qed.
 
64
 
 
65
Lemma Zcompare_Gt_Lt_antisym : forall n m:Z, (n ?= m) = Gt <-> (m ?= n) = Lt.
 
66
Proof.
 
67
  intros x y; split; intro H;
 
68
    [ change Lt with (CompOpp Gt) in |- *; rewrite <- Zcompare_antisym;
 
69
      rewrite H; reflexivity
 
70
      | change Gt with (CompOpp Lt) in |- *; rewrite <- Zcompare_antisym;
 
71
        rewrite H; reflexivity ].
 
72
Qed.
 
73
 
 
74
(** * Transitivity of comparison *)
 
75
 
 
76
Lemma Zcompare_Gt_trans :
 
77
  forall n m p:Z, (n ?= m) = Gt -> (m ?= p) = Gt -> (n ?= p) = Gt.
 
78
Proof.
 
79
  intros x y z; case x; case y; case z; simpl in |- *;
 
80
    try (intros; discriminate H || discriminate H0); auto with arith;
 
81
      [ intros p q r H H0; apply nat_of_P_gt_Gt_compare_complement_morphism;
 
82
        unfold gt in |- *; apply lt_trans with (m := nat_of_P q);
 
83
          apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; 
 
84
            assumption
 
85
        | intros p q r; do 3 rewrite <- ZC4; intros H H0;
 
86
          apply nat_of_P_gt_Gt_compare_complement_morphism; 
 
87
            unfold gt in |- *; apply lt_trans with (m := nat_of_P q);
 
88
              apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; 
 
89
                assumption ].
 
90
Qed.
 
91
 
 
92
(** * Comparison and opposite *)
 
93
 
 
94
Lemma Zcompare_opp : forall n m:Z, (n ?= m) = (- m ?= - n).
 
95
Proof.
 
96
  intros x y; case x; case y; simpl in |- *; auto with arith; intros;
 
97
    rewrite <- ZC4; trivial with arith.
 
98
Qed.
 
99
 
 
100
Hint Local Resolve Pcompare_refl.
 
101
 
 
102
(** * Comparison first-order specification *)
 
103
 
 
104
Lemma Zcompare_Gt_spec :
 
105
  forall n m:Z, (n ?= m) = Gt ->  exists h : positive, n + - m = Zpos h.
 
106
Proof.
 
107
  intros x y; case x; case y;
 
108
    [ simpl in |- *; intros H; discriminate H
 
109
      | simpl in |- *; intros p H; discriminate H
 
110
      | intros p H; exists p; simpl in |- *; auto with arith
 
111
      | intros p H; exists p; simpl in |- *; auto with arith
 
112
      | intros q p H; exists (p - q)%positive; unfold Zplus, Zopp in |- *;
 
113
        unfold Zcompare in H; rewrite H; trivial with arith
 
114
      | intros q p H; exists (p + q)%positive; simpl in |- *; trivial with arith
 
115
      | simpl in |- *; intros p H; discriminate H
 
116
      | simpl in |- *; intros q p H; discriminate H
 
117
      | unfold Zcompare in |- *; intros q p; rewrite <- ZC4; intros H;
 
118
        exists (q - p)%positive; simpl in |- *; rewrite (ZC1 q p H);
 
119
          trivial with arith ].
 
120
Qed.
 
121
 
 
122
(** * Comparison and addition *)
 
123
 
 
124
Lemma weaken_Zcompare_Zplus_compatible :
 
125
  (forall (n m:Z) (p:positive), (Zpos p + n ?= Zpos p + m) = (n ?= m)) ->
 
126
  forall n m p:Z, (p + n ?= p + m) = (n ?= m).
 
127
Proof.
 
128
  intros H x y z; destruct z;
 
129
    [ reflexivity
 
130
      | apply H
 
131
      | rewrite (Zcompare_opp x y); rewrite Zcompare_opp;
 
132
        do 2 rewrite Zopp_plus_distr; rewrite Zopp_neg; 
 
133
          apply H ].
 
134
Qed.
 
135
 
 
136
Hint Local Resolve ZC4.
 
137
 
 
138
Lemma weak_Zcompare_Zplus_compatible :
 
139
  forall (n m:Z) (p:positive), (Zpos p + n ?= Zpos p + m) = (n ?= m).
 
140
Proof.
 
141
  intros x y z; case x; case y; simpl in |- *; auto with arith;
 
142
    [ intros p; apply nat_of_P_lt_Lt_compare_complement_morphism; apply ZL17
 
143
      | intros p; ElimPcompare z p; intros E; rewrite E; auto with arith;
 
144
        apply nat_of_P_gt_Gt_compare_complement_morphism;
 
145
          rewrite nat_of_P_minus_morphism;
 
146
            [ unfold gt in |- *; apply ZL16 | assumption ]
 
147
      | intros p; ElimPcompare z p; intros E; auto with arith;
 
148
        apply nat_of_P_gt_Gt_compare_complement_morphism; 
 
149
          unfold gt in |- *; apply ZL17
 
150
      | intros p q; ElimPcompare q p; intros E; rewrite E;
 
151
        [ rewrite (Pcompare_Eq_eq q p E); apply Pcompare_refl
 
152
          | apply nat_of_P_lt_Lt_compare_complement_morphism;
 
153
            do 2 rewrite nat_of_P_plus_morphism; apply plus_lt_compat_l;
 
154
              apply nat_of_P_lt_Lt_compare_morphism with (1 := E)
 
155
          | apply nat_of_P_gt_Gt_compare_complement_morphism; unfold gt in |- *;
 
156
            do 2 rewrite nat_of_P_plus_morphism; apply plus_lt_compat_l;
 
157
              exact (nat_of_P_gt_Gt_compare_morphism q p E) ]
 
158
      | intros p q; ElimPcompare z p; intros E; rewrite E; auto with arith;
 
159
        apply nat_of_P_gt_Gt_compare_complement_morphism;
 
160
          rewrite nat_of_P_minus_morphism;
 
161
            [ unfold gt in |- *; apply lt_trans with (m := nat_of_P z);
 
162
              [ apply ZL16 | apply ZL17 ]
 
163
              | assumption ]
 
164
      | intros p; ElimPcompare z p; intros E; rewrite E; auto with arith;
 
165
        simpl in |- *; apply nat_of_P_lt_Lt_compare_complement_morphism;
 
166
          rewrite nat_of_P_minus_morphism; [ apply ZL16 | assumption ]
 
167
      | intros p q; ElimPcompare z q; intros E; rewrite E; auto with arith;
 
168
        simpl in |- *; apply nat_of_P_lt_Lt_compare_complement_morphism;
 
169
          rewrite nat_of_P_minus_morphism;
 
170
            [ apply lt_trans with (m := nat_of_P z); [ apply ZL16 | apply ZL17 ]
 
171
              | assumption ]
 
172
      | intros p q; ElimPcompare z q; intros E0; rewrite E0; ElimPcompare z p;
 
173
        intros E1; rewrite E1; ElimPcompare q p; intros E2; 
 
174
          rewrite E2; auto with arith;
 
175
            [ absurd ((q ?= p)%positive Eq = Lt);
 
176
              [ rewrite <- (Pcompare_Eq_eq z q E0);
 
177
                rewrite <- (Pcompare_Eq_eq z p E1); rewrite (Pcompare_refl z);
 
178
                  discriminate
 
179
                | assumption ]
 
180
              | absurd ((q ?= p)%positive Eq = Gt);
 
181
                [ rewrite <- (Pcompare_Eq_eq z q E0);
 
182
                  rewrite <- (Pcompare_Eq_eq z p E1); rewrite (Pcompare_refl z);
 
183
                    discriminate
 
184
                  | assumption ]
 
185
              | absurd ((z ?= p)%positive Eq = Lt);
 
186
                [ rewrite (Pcompare_Eq_eq z q E0); rewrite <- (Pcompare_Eq_eq q p E2);
 
187
                  rewrite (Pcompare_refl q); discriminate
 
188
                  | assumption ]
 
189
              | absurd ((z ?= p)%positive Eq = Lt);
 
190
                [ rewrite (Pcompare_Eq_eq z q E0); rewrite E2; discriminate
 
191
                  | assumption ]
 
192
              | absurd ((z ?= p)%positive Eq = Gt);
 
193
                [ rewrite (Pcompare_Eq_eq z q E0); rewrite <- (Pcompare_Eq_eq q p E2);
 
194
                  rewrite (Pcompare_refl q); discriminate
 
195
                  | assumption ]
 
196
              | absurd ((z ?= p)%positive Eq = Gt);
 
197
                [ rewrite (Pcompare_Eq_eq z q E0); rewrite E2; discriminate
 
198
                  | assumption ]
 
199
              | absurd ((z ?= q)%positive Eq = Lt);
 
200
                [ rewrite (Pcompare_Eq_eq z p E1); rewrite (Pcompare_Eq_eq q p E2);
 
201
                  rewrite (Pcompare_refl p); discriminate
 
202
                  | assumption ]
 
203
              | absurd ((p ?= q)%positive Eq = Gt);
 
204
                [ rewrite <- (Pcompare_Eq_eq z p E1); rewrite E0; discriminate
 
205
                  | apply ZC2; assumption ]
 
206
              | simpl in |- *; rewrite (Pcompare_Eq_eq q p E2);
 
207
                rewrite (Pcompare_refl (p - z)); auto with arith
 
208
              | simpl in |- *; rewrite <- ZC4;
 
209
                apply nat_of_P_gt_Gt_compare_complement_morphism;
 
210
                  rewrite nat_of_P_minus_morphism;
 
211
                    [ rewrite nat_of_P_minus_morphism;
 
212
                      [ unfold gt in |- *; apply plus_lt_reg_l with (p := nat_of_P z);
 
213
                        rewrite le_plus_minus_r;
 
214
                          [ rewrite le_plus_minus_r;
 
215
                            [ apply nat_of_P_lt_Lt_compare_morphism; assumption
 
216
                              | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
 
217
                                assumption ]
 
218
                            | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
 
219
                              assumption ]
 
220
                        | apply ZC2; assumption ]
 
221
                      | apply ZC2; assumption ]
 
222
              | simpl in |- *; rewrite <- ZC4;
 
223
                apply nat_of_P_lt_Lt_compare_complement_morphism;
 
224
                  rewrite nat_of_P_minus_morphism;
 
225
                    [ rewrite nat_of_P_minus_morphism;
 
226
                      [ apply plus_lt_reg_l with (p := nat_of_P z);
 
227
                        rewrite le_plus_minus_r;
 
228
                          [ rewrite le_plus_minus_r;
 
229
                            [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1;
 
230
                              assumption
 
231
                              | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
 
232
                                assumption ]
 
233
                            | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
 
234
                              assumption ]
 
235
                        | apply ZC2; assumption ]
 
236
                      | apply ZC2; assumption ]
 
237
              | absurd ((z ?= q)%positive Eq = Lt);
 
238
                [ rewrite (Pcompare_Eq_eq q p E2); rewrite E1; discriminate
 
239
                  | assumption ]
 
240
              | absurd ((q ?= p)%positive Eq = Lt);
 
241
                [ cut ((q ?= p)%positive Eq = Gt);
 
242
                  [ intros E; rewrite E; discriminate
 
243
                    | apply nat_of_P_gt_Gt_compare_complement_morphism;
 
244
                      unfold gt in |- *; apply lt_trans with (m := nat_of_P z);
 
245
                        [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption
 
246
                          | apply nat_of_P_lt_Lt_compare_morphism; assumption ] ]
 
247
                  | assumption ]
 
248
              | absurd ((z ?= q)%positive Eq = Gt);
 
249
                [ rewrite (Pcompare_Eq_eq z p E1); rewrite (Pcompare_Eq_eq q p E2);
 
250
                  rewrite (Pcompare_refl p); discriminate
 
251
                  | assumption ]
 
252
              | absurd ((z ?= q)%positive Eq = Gt);
 
253
                [ rewrite (Pcompare_Eq_eq z p E1); rewrite ZC1;
 
254
                  [ discriminate | assumption ]
 
255
                  | assumption ]
 
256
              | absurd ((z ?= q)%positive Eq = Gt);
 
257
                [ rewrite (Pcompare_Eq_eq q p E2); rewrite E1; discriminate
 
258
                  | assumption ]
 
259
              | absurd ((q ?= p)%positive Eq = Gt);
 
260
                [ rewrite ZC1;
 
261
                  [ discriminate
 
262
                    | apply nat_of_P_gt_Gt_compare_complement_morphism;
 
263
                      unfold gt in |- *; apply lt_trans with (m := nat_of_P z);
 
264
                        [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption
 
265
                          | apply nat_of_P_lt_Lt_compare_morphism; assumption ] ]
 
266
                  | assumption ]
 
267
              | simpl in |- *; rewrite (Pcompare_Eq_eq q p E2); apply Pcompare_refl
 
268
              | simpl in |- *; apply nat_of_P_gt_Gt_compare_complement_morphism;
 
269
                unfold gt in |- *; rewrite nat_of_P_minus_morphism;
 
270
                  [ rewrite nat_of_P_minus_morphism;
 
271
                    [ apply plus_lt_reg_l with (p := nat_of_P p);
 
272
                      rewrite le_plus_minus_r;
 
273
                        [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P q);
 
274
                          rewrite plus_assoc; rewrite le_plus_minus_r;
 
275
                            [ rewrite (plus_comm (nat_of_P q)); apply plus_lt_compat_l;
 
276
                              apply nat_of_P_lt_Lt_compare_morphism; 
 
277
                                assumption
 
278
                              | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
 
279
                                apply ZC1; assumption ]
 
280
                          | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
 
281
                            apply ZC1; assumption ]
 
282
                      | assumption ]
 
283
                    | assumption ]
 
284
              | simpl in |- *; apply nat_of_P_lt_Lt_compare_complement_morphism;
 
285
                rewrite nat_of_P_minus_morphism;
 
286
                  [ rewrite nat_of_P_minus_morphism;
 
287
                    [ apply plus_lt_reg_l with (p := nat_of_P q);
 
288
                      rewrite le_plus_minus_r;
 
289
                        [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P p);
 
290
                          rewrite plus_assoc; rewrite le_plus_minus_r;
 
291
                            [ rewrite (plus_comm (nat_of_P p)); apply plus_lt_compat_l;
 
292
                              apply nat_of_P_lt_Lt_compare_morphism; 
 
293
                                apply ZC1; assumption
 
294
                              | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
 
295
                                apply ZC1; assumption ]
 
296
                          | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
 
297
                            apply ZC1; assumption ]
 
298
                      | assumption ]
 
299
                    | assumption ] ] ].
 
300
Qed.
 
301
 
 
302
Lemma Zcompare_plus_compat : forall n m p:Z, (p + n ?= p + m) = (n ?= m).
 
303
Proof.
 
304
  exact (weaken_Zcompare_Zplus_compatible weak_Zcompare_Zplus_compatible).
 
305
Qed.
 
306
 
 
307
Lemma Zplus_compare_compat :
 
308
  forall (r:comparison) (n m p q:Z),
 
309
    (n ?= m) = r -> (p ?= q) = r -> (n + p ?= m + q) = r.
 
310
Proof.
 
311
  intros r x y z t; case r;
 
312
    [ intros H1 H2; elim (Zcompare_Eq_iff_eq x y); elim (Zcompare_Eq_iff_eq z t);
 
313
      intros H3 H4 H5 H6; rewrite H3;
 
314
        [ rewrite H5;
 
315
          [ elim (Zcompare_Eq_iff_eq (y + t) (y + t)); auto with arith
 
316
            | auto with arith ]
 
317
          | auto with arith ]
 
318
      | intros H1 H2; elim (Zcompare_Gt_Lt_antisym (y + t) (x + z)); intros H3 H4;
 
319
        apply H3; apply Zcompare_Gt_trans with (m := y + z);
 
320
          [ rewrite Zcompare_plus_compat; elim (Zcompare_Gt_Lt_antisym t z);
 
321
            auto with arith
 
322
            | do 2 rewrite <- (Zplus_comm z); rewrite Zcompare_plus_compat;
 
323
              elim (Zcompare_Gt_Lt_antisym y x); auto with arith ]
 
324
      | intros H1 H2; apply Zcompare_Gt_trans with (m := x + t);
 
325
        [ rewrite Zcompare_plus_compat; assumption
 
326
          | do 2 rewrite <- (Zplus_comm t); rewrite Zcompare_plus_compat;
 
327
            assumption ] ].
 
328
Qed.
 
329
 
 
330
Lemma Zcompare_succ_Gt : forall n:Z, (Zsucc n ?= n) = Gt.
 
331
Proof.
 
332
  intro x; unfold Zsucc in |- *; pattern x at 2 in |- *;
 
333
    rewrite <- (Zplus_0_r x); rewrite Zcompare_plus_compat; 
 
334
      reflexivity.
 
335
Qed.
 
336
 
 
337
Lemma Zcompare_Gt_not_Lt : forall n m:Z, (n ?= m) = Gt <-> (n ?= m + 1) <> Lt.
 
338
Proof.
 
339
  intros x y; split;
 
340
    [ intro H; elim_compare x (y + 1);
 
341
      [ intro H1; rewrite H1; discriminate
 
342
        | intros H1; elim Zcompare_Gt_spec with (1 := H); intros h H2;
 
343
          absurd ((nat_of_P h > 0)%nat /\ (nat_of_P h < 1)%nat);
 
344
            [ unfold not in |- *; intros H3; elim H3; intros H4 H5;
 
345
              absurd (nat_of_P h > 0)%nat;
 
346
                [ unfold gt in |- *; apply le_not_lt; apply le_S_n; exact H5
 
347
                  | assumption ]
 
348
              | split;
 
349
                [ elim (ZL4 h); intros i H3; rewrite H3; apply gt_Sn_O
 
350
                  | change (nat_of_P h < nat_of_P 1)%nat in |- *;
 
351
                    apply nat_of_P_lt_Lt_compare_morphism;
 
352
                      change ((Zpos h ?= 1) = Lt) in |- *; rewrite <- H2;
 
353
                        rewrite <- (fun m n:Z => Zcompare_plus_compat m n y);
 
354
                          rewrite (Zplus_comm x); rewrite Zplus_assoc; 
 
355
                            rewrite Zplus_opp_r; simpl in |- *; exact H1 ] ]
 
356
        | intros H1; rewrite H1; discriminate ]
 
357
      | intros H; elim_compare x (y + 1);
 
358
        [ intros H1; elim (Zcompare_Eq_iff_eq x (y + 1)); intros H2 H3;
 
359
          rewrite (H2 H1); exact (Zcompare_succ_Gt y)
 
360
          | intros H1; absurd ((x ?= y + 1) = Lt); assumption
 
361
          | intros H1; apply Zcompare_Gt_trans with (m := Zsucc y);
 
362
            [ exact H1 | exact (Zcompare_succ_Gt y) ] ] ].
 
363
Qed.
 
364
 
 
365
(** * Successor and comparison *)
 
366
 
 
367
Lemma Zcompare_succ_compat : forall n m:Z, (Zsucc n ?= Zsucc m) = (n ?= m).
 
368
Proof.
 
369
  intros n m; unfold Zsucc in |- *; do 2 rewrite (fun t:Z => Zplus_comm t 1);
 
370
    rewrite Zcompare_plus_compat; auto with arith.
 
371
Qed.
 
372
 
 
373
(** * Multiplication and comparison *)
 
374
 
 
375
Lemma Zcompare_mult_compat :
 
376
  forall (p:positive) (n m:Z), (Zpos p * n ?= Zpos p * m) = (n ?= m).
 
377
Proof.
 
378
  intros x; induction x as [p H| p H| ];
 
379
    [ intros y z; cut (Zpos (xI p) = Zpos p + Zpos p + 1);
 
380
      [ intros E; rewrite E; do 4 rewrite Zmult_plus_distr_l;
 
381
        do 2 rewrite Zmult_1_l; apply Zplus_compare_compat;
 
382
          [ apply Zplus_compare_compat; apply H | trivial with arith ]
 
383
        | simpl in |- *; rewrite (Pplus_diag p); trivial with arith ]
 
384
      | intros y z; cut (Zpos (xO p) = Zpos p + Zpos p);
 
385
        [ intros E; rewrite E; do 2 rewrite Zmult_plus_distr_l;
 
386
          apply Zplus_compare_compat; apply H
 
387
          | simpl in |- *; rewrite (Pplus_diag p); trivial with arith ]
 
388
      | intros y z; do 2 rewrite Zmult_1_l; trivial with arith ].
 
389
Qed.
 
390
 
 
391
 
 
392
(** * Reverting [x ?= y] to trichotomy *)
 
393
 
 
394
Lemma rename :
 
395
  forall (A:Type) (P:A -> Prop) (x:A), (forall y:A, x = y -> P y) -> P x.
 
396
Proof.
 
397
  auto with arith. 
 
398
Qed.
 
399
 
 
400
Lemma Zcompare_elim :
 
401
  forall (c1 c2 c3:Prop) (n m:Z),
 
402
    (n = m -> c1) ->
 
403
    (n < m -> c2) ->
 
404
    (n > m -> c3) -> match n ?= m with
 
405
                       | Eq => c1
 
406
                       | Lt => c2
 
407
                       | Gt => c3
 
408
                     end.
 
409
Proof.
 
410
  intros c1 c2 c3 x y; intros.
 
411
  apply rename with (x := x ?= y); intro r; elim r;
 
412
    [ intro; apply H; apply (Zcompare_Eq_eq x y); assumption
 
413
      | unfold Zlt in H0; assumption
 
414
      | unfold Zgt in H1; assumption ].
 
415
Qed.
 
416
 
 
417
Lemma Zcompare_eq_case :
 
418
  forall (c1 c2 c3:Prop) (n m:Z),
 
419
    c1 -> n = m -> match n ?= m with
 
420
                     | Eq => c1
 
421
                     | Lt => c2
 
422
                     | Gt => c3
 
423
                   end.
 
424
Proof.
 
425
  intros c1 c2 c3 x y; intros.
 
426
  rewrite H0; rewrite Zcompare_refl.
 
427
  assumption.
 
428
Qed.
 
429
 
 
430
(** * Decompose an egality between two [?=] relations into 3 implications *)
 
431
 
 
432
Lemma Zcompare_egal_dec :
 
433
  forall n m p q:Z,
 
434
    (n < m -> p < q) ->
 
435
    ((n ?= m) = Eq -> (p ?= q) = Eq) ->
 
436
    (n > m -> p > q) -> (n ?= m) = (p ?= q).
 
437
Proof.
 
438
  intros x1 y1 x2 y2.
 
439
  unfold Zgt in |- *; unfold Zlt in |- *; case (x1 ?= y1); case (x2 ?= y2);
 
440
    auto with arith; symmetry  in |- *; auto with arith.
 
441
Qed.
 
442
 
 
443
(** * Relating [x ?= y] to [Zle], [Zlt], [Zge] or [Zgt] *)
 
444
 
 
445
Lemma Zle_compare :
 
446
  forall n m:Z,
 
447
    n <= m -> match n ?= m with
 
448
                | Eq => True
 
449
                | Lt => True
 
450
                | Gt => False
 
451
              end.
 
452
Proof.
 
453
  intros x y; unfold Zle in |- *; elim (x ?= y); auto with arith.
 
454
Qed.
 
455
 
 
456
Lemma Zlt_compare :
 
457
  forall n m:Z,
 
458
   n < m -> match n ?= m with
 
459
              | Eq => False
 
460
              | Lt => True
 
461
              | Gt => False
 
462
            end.
 
463
Proof.
 
464
  intros x y; unfold Zlt in |- *; elim (x ?= y); intros;
 
465
    discriminate || trivial with arith.
 
466
Qed.
 
467
 
 
468
Lemma Zge_compare :
 
469
  forall n m:Z,
 
470
    n >= m -> match n ?= m with
 
471
                | Eq => True
 
472
                | Lt => False
 
473
                | Gt => True
 
474
              end.
 
475
Proof.
 
476
  intros x y; unfold Zge in |- *; elim (x ?= y); auto with arith. 
 
477
Qed.
 
478
 
 
479
Lemma Zgt_compare :
 
480
  forall n m:Z,
 
481
    n > m -> match n ?= m with
 
482
               | Eq => False
 
483
               | Lt => False
 
484
               | Gt => True
 
485
             end.
 
486
Proof.
 
487
  intros x y; unfold Zgt in |- *; elim (x ?= y); intros;
 
488
    discriminate || trivial with arith.
 
489
Qed.
 
490
 
 
491
(*********************)
 
492
(** * Other properties *)
 
493
 
 
494
Lemma Zmult_compare_compat_l :
 
495
  forall n m p:Z, p > 0 -> (n ?= m) = (p * n ?= p * m).
 
496
Proof.
 
497
  intros x y z H; destruct z.
 
498
  discriminate H.
 
499
  rewrite Zcompare_mult_compat; reflexivity.
 
500
  discriminate H.
 
501
Qed.
 
502
 
 
503
Lemma Zmult_compare_compat_r :
 
504
  forall n m p:Z, p > 0 -> (n ?= m) = (n * p ?= m * p).
 
505
Proof.
 
506
  intros x y z H; rewrite (Zmult_comm x z); rewrite (Zmult_comm y z);
 
507
    apply Zmult_compare_compat_l; assumption.
 
508
Qed.
 
509