← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/ZArith/Zmax.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/Zmax.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
(*i $Id: Zmax.v 10291 2007-11-06 02:18:53Z letouzey $ i*)
 
9
 
 
10
Require Import Arith_base.
 
11
Require Import BinInt.
 
12
Require Import Zcompare.
 
13
Require Import Zorder.
 
14
 
 
15
Open Local Scope Z_scope.
 
16
 
 
17
(******************************************)
 
18
(** Maximum of two binary integer numbers *)
 
19
 
 
20
Definition Zmax m n :=
 
21
  match m ?= n with
 
22
    | Eq | Gt => m
 
23
    | Lt => n
 
24
  end.
 
25
 
 
26
(** * Characterization of maximum on binary integer numbers *)
 
27
 
 
28
Lemma Zmax_case : forall (n m:Z) (P:Z -> Type), P n -> P m -> P (Zmax n m).
 
29
Proof.
 
30
  intros n m P H1 H2; unfold Zmax in |- *; case (n ?= m); auto with arith.
 
31
Qed.
 
32
 
 
33
Lemma Zmax_case_strong : forall (n m:Z) (P:Z -> Type), 
 
34
  (m<=n -> P n) -> (n<=m -> P m) -> P (Zmax n m).
 
35
Proof.
 
36
  intros n m P H1 H2; unfold Zmax, Zle, Zge in *.
 
37
  rewrite <- (Zcompare_antisym n m) in H1.
 
38
  destruct (n ?= m); (apply H1|| apply H2); discriminate. 
 
39
Qed.
 
40
 
 
41
Lemma Zmax_spec : forall x y:Z, 
 
42
  x >= y /\ Zmax x y = x  \/
 
43
  x < y /\ Zmax x y = y.
 
44
Proof.
 
45
 intros; unfold Zmax, Zlt, Zge.
 
46
 destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate.
 
47
Qed.
 
48
 
 
49
Lemma Zmax_left : forall n m:Z, n>=m -> Zmax n m = n.
 
50
Proof.
 
51
  intros n m; unfold Zmax, Zge; destruct (n ?= m); auto.
 
52
  intro H; elim H; auto.
 
53
Qed.
 
54
 
 
55
Lemma Zmax_right : forall n m:Z, n<=m -> Zmax n m = m.
 
56
Proof.
 
57
  intros n m; unfold Zmax, Zle.
 
58
  generalize (Zcompare_Eq_eq n m).
 
59
  destruct (n ?= m); auto.
 
60
  intros _ H; elim H; auto.
 
61
Qed.
 
62
 
 
63
(** * Least upper bound properties of max *)
 
64
 
 
65
Lemma Zle_max_l : forall n m:Z, n <= Zmax n m.
 
66
Proof.
 
67
  intros; apply Zmax_case_strong; auto with zarith.
 
68
Qed.
 
69
 
 
70
Notation Zmax1 := Zle_max_l (only parsing).
 
71
 
 
72
Lemma Zle_max_r : forall n m:Z, m <= Zmax n m.
 
73
Proof.
 
74
  intros; apply Zmax_case_strong; auto with zarith.
 
75
Qed.
 
76
 
 
77
Notation Zmax2 := Zle_max_r (only parsing).
 
78
 
 
79
Lemma Zmax_lub : forall n m p:Z, n <= p -> m <= p -> Zmax n m <= p.
 
80
Proof.
 
81
  intros; apply Zmax_case; assumption.
 
82
Qed.
 
83
 
 
84
(** * Semi-lattice properties of max *)
 
85
 
 
86
Lemma Zmax_idempotent : forall n:Z, Zmax n n = n.
 
87
Proof.
 
88
  intros; apply Zmax_case; auto.
 
89
Qed.
 
90
 
 
91
Lemma Zmax_comm : forall n m:Z, Zmax n m = Zmax m n.
 
92
Proof.
 
93
  intros; do 2 apply Zmax_case_strong; intros; 
 
94
    apply Zle_antisym; auto with zarith.
 
95
Qed.
 
96
 
 
97
Lemma Zmax_assoc : forall n m p:Z, Zmax n (Zmax m p) = Zmax (Zmax n m) p.
 
98
Proof.
 
99
  intros n m p; repeat apply Zmax_case_strong; intros; 
 
100
    reflexivity || (try apply Zle_antisym); eauto with zarith.
 
101
Qed.
 
102
 
 
103
(** * Additional properties of max *)
 
104
 
 
105
Lemma Zmax_irreducible_inf : forall n m:Z, Zmax n m = n \/ Zmax n m = m.
 
106
Proof.
 
107
  intros; apply Zmax_case; auto.
 
108
Qed.
 
109
 
 
110
Lemma Zmax_le_prime_inf : forall n m p:Z, p <= Zmax n m -> p <= n \/ p <= m.
 
111
Proof.
 
112
  intros n m p; apply Zmax_case; auto.
 
113
Qed.
 
114
 
 
115
(** * Operations preserving max *)
 
116
 
 
117
Lemma Zsucc_max_distr : 
 
118
  forall n m:Z, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m).
 
119
Proof.
 
120
  intros n m; unfold Zmax in |- *; rewrite (Zcompare_succ_compat n m);
 
121
    elim_compare n m; intros E; rewrite E; auto with arith.
 
122
Qed.
 
123
 
 
124
Lemma Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m + p.
 
125
Proof.
 
126
  intros x y n; unfold Zmax in |- *.
 
127
  rewrite (Zplus_comm x n); rewrite (Zplus_comm y n);
 
128
    rewrite (Zcompare_plus_compat x y n).
 
129
  case (x ?= y); apply Zplus_comm.
 
130
Qed.
 
131
 
 
132
(** * Maximum and Zpos *)
 
133
 
 
134
Lemma Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q).
 
135
Proof.
 
136
  intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q).
 
137
  destruct Pcompare; auto.
 
138
  intro H; rewrite H; auto.
 
139
Qed.
 
140
 
 
141
Lemma Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p.
 
142
Proof.
 
143
  intros; unfold Zmax; simpl; destruct p; simpl; auto.
 
144
Qed.
 
145
 
 
146
(** * Characterization of Pminus in term of Zminus and Zmax *)
 
147
 
 
148
Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).
 
149
Proof.
 
150
  intros.
 
151
  case_eq (Pcompare p q Eq).
 
152
  intros H; rewrite (Pcompare_Eq_eq _ _ H).
 
153
  rewrite Zminus_diag.
 
154
  unfold Zmax; simpl.
 
155
  unfold Pminus; rewrite Pminus_mask_diag; auto.
 
156
  intros; rewrite Pminus_Lt; auto.
 
157
  destruct (Zmax_spec 1 (Zpos p - Zpos q)) as [(H1,H2)|(H1,H2)]; auto.
 
158
  elimtype False; clear H2.
 
159
  assert (H1':=Zlt_trans 0 1 _ Zlt_0_1 H1).
 
160
  generalize (Zlt_0_minus_lt _ _ H1').
 
161
  unfold Zlt; simpl.
 
162
  rewrite (ZC2 _ _ H); intro; discriminate.
 
163
  intros; simpl; rewrite H.
 
164
  symmetry; apply Zpos_max_1.
 
165
Qed.
 
166