1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import OrderedType2 BinInt Zcompare Zorder ZOrderedType
GenericMinMax.
(** * Maximum and Minimum of two [Z] numbers *)
Local Open Scope Z_scope.
Unboxed Definition Zmax (n m:Z) :=
match n ?= m with
| Eq | Gt => n
| Lt => m
end.
Unboxed Definition Zmin (n m:Z) :=
match n ?= m with
| Eq | Lt => n
| Gt => m
end.
(** The functions [Zmax] and [Zmin] implement indeed
a maximum and a minimum *)
Lemma Zmax_spec : forall x y,
(x<y /\ Zmax x y = y) \/ (y<=x /\ Zmax x y = x).
Proof.
unfold Zlt, Zle, Zmax. intros.
generalize (Zcompare_Eq_eq x y).
rewrite <- (Zcompare_antisym x y).
destruct (x ?= y); simpl; auto; right; intuition; discriminate.
Qed.
Lemma Zmin_spec : forall x y,
(x<y /\ Zmin x y = x) \/ (y<=x /\ Zmin x y = y).
Proof.
unfold Zlt, Zle, Zmin. intros.
generalize (Zcompare_Eq_eq x y).
rewrite <- (Zcompare_antisym x y).
destruct (x ?= y); simpl; auto; right; intuition; discriminate.
Qed.
Module ZHasMinMax <: HasMinMax Z_as_OT.
Definition max := Zmax.
Definition min := Zmin.
Definition max_spec := Zmax_spec.
Definition min_spec := Zmin_spec.
End ZHasMinMax.
(** We obtain hence all the generic properties of max and min. *)
Module Import ZMinMaxProps := MinMaxProperties Z_as_OT ZHasMinMax.
(** For some generic properties, we can have nicer statements here,
since underlying equality is Leibniz. *)
Lemma Zmax_case_strong : forall n m (P:Z -> Type),
(m<=n -> P n) -> (n<=m -> P m) -> P (Zmax n m).
Proof. intros; apply max_case_strong; auto. congruence. Defined.
Lemma Zmax_case : forall n m (P:Z -> Type),
P n -> P m -> P (Zmax n m).
Proof. intros. apply Zmax_case_strong; auto. Defined.
Lemma Zmax_monotone: forall f,
(Proper (Zle ==> Zle) f) ->
forall x y, Zmax (f x) (f y) = f (Zmax x y).
Proof. intros; apply max_monotone; auto. congruence. Qed.
Lemma Zmin_case_strong : forall n m (P:Z -> Type),
(n<=m -> P n) -> (m<=n -> P m) -> P (Zmin n m).
Proof. intros; apply min_case_strong; auto. congruence. Defined.
Lemma Zmin_case : forall n m (P:Z -> Type),
P n -> P m -> P (Zmin n m).
Proof. intros. apply Zmin_case_strong; auto. Defined.
Lemma Zmin_monotone: forall f,
(Proper (Zle ==> Zle) f) ->
forall x y, Zmin (f x) (f y) = f (Zmin x y).
Proof. intros; apply min_monotone; auto. congruence. Qed.
Lemma Zmax_min_antimonotone : forall f,
Proper (Zle==>Zge) f ->
forall x y, Zmax (f x) (f y) == f (Zmin x y).
Proof.
intros. apply max_min_antimonotone. congruence.
intros z z' Hz; red. apply Zge_le. auto.
Qed.
Lemma Zmin_max_antimonotone : forall f,
Proper (Zle==>Zge) f ->
forall x y, Zmin (f x) (f y) == f (Zmax x y).
Proof.
intros. apply min_max_antimonotone. congruence.
intros z z' Hz; red. apply Zge_le. auto.
Qed.
(** For the other generic properties, we make aliases,
since otherwise SearchAbout misses some of them
(bad interaction with an Include).
See GenericMinMax (or SearchAbout) for the statements. *)
Definition Zmax_spec_le := max_spec_le.
Definition Zmax_dec := max_dec.
Definition Zmax_unicity := max_unicity.
Definition Zmax_unicity_ext := max_unicity_ext.
Definition Zmax_id := max_id.
Notation Zmax_idempotent := Zmax_id (only parsing).
Definition Zmax_assoc := max_assoc.
Definition Zmax_comm := max_comm.
Definition Zmax_l := max_l.
Definition Zmax_r := max_r.
Definition Zle_max_l := le_max_l.
Definition Zle_max_r := le_max_r.
Definition Zmax_le := max_le.
Definition Zmax_le_iff := max_le_iff.
Definition Zmax_lt_iff := max_lt_iff.
Definition Zmax_lub_l := max_lub_l.
Definition Zmax_lub_r := max_lub_r.
Definition Zmax_lub := max_lub.
Definition Zmax_lub_iff := max_lub_iff.
Definition Zmax_lub_lt := max_lub_lt.
Definition Zmax_lub_lt_iff := max_lub_lt_iff.
Definition Zmax_le_compat_l := max_le_compat_l.
Definition Zmax_le_compat_r := max_le_compat_r.
Definition Zmax_le_compat := max_le_compat.
Definition Zmin_spec_le := min_spec_le.
Definition Zmin_dec := min_dec.
Definition Zmin_unicity := min_unicity.
Definition Zmin_unicity_ext := min_unicity_ext.
Definition Zmin_id := min_id.
Notation Zmin_idempotent := Zmin_id (only parsing).
Definition Zmin_assoc := min_assoc.
Definition Zmin_comm := min_comm.
Definition Zmin_l := min_l.
Definition Zmin_r := min_r.
Definition Zle_min_l := le_min_l.
Definition Zle_min_r := le_min_r.
Definition Zmin_le := min_le.
Definition Zmin_le_iff := min_le_iff.
Definition Zmin_lt_iff := min_lt_iff.
Definition Zmin_glb_l := min_glb_l.
Definition Zmin_glb_r := min_glb_r.
Definition Zmin_glb := min_glb.
Definition Zmin_glb_iff := min_glb_iff.
Definition Zmin_glb_lt := min_glb_lt.
Definition Zmin_glb_lt_iff := min_glb_lt_iff.
Definition Zmin_le_compat_l := min_le_compat_l.
Definition Zmin_le_compat_r := min_le_compat_r.
Definition Zmin_le_compat := min_le_compat.
Definition Zmin_max_absorption := min_max_absorption.
Definition Zmax_min_absorption := max_min_absorption.
Definition Zmax_min_distr := max_min_distr.
Definition Zmin_max_distr := min_max_distr.
Definition Zmax_min_modular := max_min_modular.
Definition Zmin_max_modular := min_max_modular.
Definition Zmax_min_disassoc := max_min_disassoc.
(** * Properties specific to the [Z] domain *)
(** Compatibilities (consequences of monotonicity) *)
Lemma Zplus_max_distr_l : forall n m p, Zmax (p + n) (p + m) = p + Zmax n m.
Proof.
intros. apply Zmax_monotone.
intros x y. apply Zplus_le_compat_l.
Qed.
Lemma Zplus_max_distr_r : forall n m p, Zmax (n + p) (m + p) = Zmax n m + p.
Proof.
intros. rewrite (Zplus_comm n p), (Zplus_comm m p), (Zplus_comm _ p).
apply Zplus_max_distr_l.
Qed.
Lemma Zplus_min_distr_l : forall n m p, Zmin (p + n) (p + m) = p + Zmin n m.
Proof.
intros. apply Zmin_monotone.
intros x y. apply Zplus_le_compat_l.
Qed.
Lemma Zplus_min_distr_r : forall n m p, Zmin (n + p) (m + p) = Zmin n m + p.
Proof.
intros. rewrite (Zplus_comm n p), (Zplus_comm m p), (Zplus_comm _ p).
apply Zplus_min_distr_l.
Qed.
Lemma Zsucc_max_distr : forall n m, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m).
Proof.
unfold Zsucc. intros. symmetry. apply Zplus_max_distr_r.
Qed.
Lemma Zsucc_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m).
Proof.
unfold Zsucc. intros. symmetry. apply Zplus_min_distr_r.
Qed.
Lemma Zpred_max_distr : forall n m, Zpred (Zmax n m) = Zmax (Zpred n) (Zpred m).
Proof.
unfold Zpred. intros. symmetry. apply Zplus_max_distr_r.
Qed.
Lemma Zpred_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m).
Proof.
unfold Zpred. intros. symmetry. apply Zplus_min_distr_r.
Qed.
(** Anti-monotonicity swaps the role of [min] and [max] *)
Lemma Zopp_max_distr : forall n m : Z, -(Zmax n m) = Zmin (- n) (- m).
Proof.
intros. symmetry. apply Zmin_max_antimonotone.
intros x x'. rewrite Zge_iff_le; red; rewrite <- Zcompare_opp; auto.
Qed.
Lemma Zopp_min_distr : forall n m : Z, - (Zmin n m) = Zmax (- n) (- m).
Proof.
intros. symmetry. apply Zmax_min_antimonotone.
intros x x'. rewrite Zge_iff_le; red; rewrite <- Zcompare_opp; auto.
Qed.
Lemma Zminus_max_distr_l : forall n m p, Zmax (p - n) (p - m) = p - Zmin n m.
Proof.
unfold Zminus. intros. rewrite Zopp_min_distr. apply Zplus_max_distr_l.
Qed.
Lemma Zminus_max_distr_r : forall n m p, Zmax (n - p) (m - p) = Zmax n m - p.
Proof.
unfold Zminus. intros. apply Zplus_max_distr_r.
Qed.
Lemma Zminus_min_distr_l : forall n m p, Zmin (p - n) (p - m) = p - Zmax n m.
Proof.
unfold Zminus. intros. rewrite Zopp_max_distr. apply Zplus_min_distr_l.
Qed.
Lemma Zminus_min_distr_r : forall n m p, Zmin (n - p) (m - p) = Zmin n m - p.
Proof.
unfold Zminus. intros. apply Zplus_min_distr_r.
Qed.
(** Compatibility with [Zpos] *)
Lemma Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q).
Proof.
intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q).
destruct Pcompare; auto.
intro H; rewrite H; auto.
Qed.
Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q).
Proof.
intros; unfold Zmin, Pmin; simpl; generalize (Pcompare_Eq_eq p q).
destruct Pcompare; auto.
Qed.
Lemma Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p.
Proof.
intros; unfold Zmax; simpl; destruct p; simpl; auto.
Qed.
Lemma Zpos_min_1 : forall p, Zmin 1 (Zpos p) = 1.
Proof.
intros; unfold Zmax; simpl; destruct p; simpl; auto.
Qed.
(** * Characterization of Pminus in term of Zminus and Zmax *)
Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).
Proof.
intros; simpl. destruct (Pcompare p q Eq) as [ ]_eqn:H.
rewrite (Pcompare_Eq_eq _ _ H).
unfold Pminus; rewrite Pminus_mask_diag; reflexivity.
rewrite Pminus_Lt; auto.
symmetry. apply Zpos_max_1.
Qed.
(*begin hide*)
(* Compatibility with names of the old Zminmax file *)
Notation Zmin_max_absorption_r_r := Zmin_max_absorption (only parsing).
Notation Zmax_min_absorption_r_r := Zmax_min_absorption (only parsing).
Notation Zmax_min_distr_r := Zmax_min_distr (only parsing).
Notation Zmin_max_distr_r := Zmin_max_distr (only parsing).
Notation Zmax_min_modular_r := Zmax_min_modular (only parsing).
Notation Zmin_max_modular_r := Zmin_max_modular (only parsing).
Notation max_min_disassoc := Zmax_min_disassoc (only parsing).
(*end hide*)
|
