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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import ZAxioms ZMulOrder GenericMinMax.
(** * Properties of minimum and maximum specific to integer numbers *)
Module Type ZMaxMinProp (Import Z : ZAxiomsMiniSig').
Include ZMulOrderProp Z.
(** The following results are concrete instances of [max_monotone]
and similar lemmas. *)
(** Succ *)
Lemma succ_max_distr : forall n m, S (max n m) == max (S n) (S m).
Proof.
intros. destruct (le_ge_cases n m);
[rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?succ_le_mono.
Qed.
Lemma succ_min_distr : forall n m, S (min n m) == min (S n) (S m).
Proof.
intros. destruct (le_ge_cases n m);
[rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?succ_le_mono.
Qed.
(** Pred *)
Lemma pred_max_distr : forall n m, P (max n m) == max (P n) (P m).
Proof.
intros. destruct (le_ge_cases n m);
[rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?pred_le_mono.
Qed.
Lemma pred_min_distr : forall n m, P (min n m) == min (P n) (P m).
Proof.
intros. destruct (le_ge_cases n m);
[rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?pred_le_mono.
Qed.
(** Add *)
Lemma add_max_distr_l : forall n m p, max (p + n) (p + m) == p + max n m.
Proof.
intros. destruct (le_ge_cases n m);
[rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_l.
Qed.
Lemma add_max_distr_r : forall n m p, max (n + p) (m + p) == max n m + p.
Proof.
intros. destruct (le_ge_cases n m);
[rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_r.
Qed.
Lemma add_min_distr_l : forall n m p, min (p + n) (p + m) == p + min n m.
Proof.
intros. destruct (le_ge_cases n m);
[rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_l.
Qed.
Lemma add_min_distr_r : forall n m p, min (n + p) (m + p) == min n m + p.
Proof.
intros. destruct (le_ge_cases n m);
[rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_r.
Qed.
(** Opp *)
Lemma opp_max_distr : forall n m, -(max n m) == min (-n) (-m).
Proof.
intros. destruct (le_ge_cases n m).
rewrite max_r by trivial. symmetry. apply min_r. now rewrite <- opp_le_mono.
rewrite max_l by trivial. symmetry. apply min_l. now rewrite <- opp_le_mono.
Qed.
Lemma opp_min_distr : forall n m, -(min n m) == max (-n) (-m).
Proof.
intros. destruct (le_ge_cases n m).
rewrite min_l by trivial. symmetry. apply max_l. now rewrite <- opp_le_mono.
rewrite min_r by trivial. symmetry. apply max_r. now rewrite <- opp_le_mono.
Qed.
(** Sub *)
Lemma sub_max_distr_l : forall n m p, max (p - n) (p - m) == p - min n m.
Proof.
intros. destruct (le_ge_cases n m).
rewrite min_l by trivial. apply max_l. now rewrite <- sub_le_mono_l.
rewrite min_r by trivial. apply max_r. now rewrite <- sub_le_mono_l.
Qed.
Lemma sub_max_distr_r : forall n m p, max (n - p) (m - p) == max n m - p.
Proof.
intros. destruct (le_ge_cases n m);
[rewrite 2 max_r | rewrite 2 max_l]; try order; now apply sub_le_mono_r.
Qed.
Lemma sub_min_distr_l : forall n m p, min (p - n) (p - m) == p - max n m.
Proof.
intros. destruct (le_ge_cases n m).
rewrite max_r by trivial. apply min_r. now rewrite <- sub_le_mono_l.
rewrite max_l by trivial. apply min_l. now rewrite <- sub_le_mono_l.
Qed.
Lemma sub_min_distr_r : forall n m p, min (n - p) (m - p) == min n m - p.
Proof.
intros. destruct (le_ge_cases n m);
[rewrite 2 min_l | rewrite 2 min_r]; try order; now apply sub_le_mono_r.
Qed.
(** Mul *)
Lemma mul_max_distr_nonneg_l : forall n m p, 0 <= p ->
max (p * n) (p * m) == p * max n m.
Proof.
intros. destruct (le_ge_cases n m);
[rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_nonneg_l.
Qed.
Lemma mul_max_distr_nonneg_r : forall n m p, 0 <= p ->
max (n * p) (m * p) == max n m * p.
Proof.
intros. destruct (le_ge_cases n m);
[rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_nonneg_r.
Qed.
Lemma mul_min_distr_nonneg_l : forall n m p, 0 <= p ->
min (p * n) (p * m) == p * min n m.
Proof.
intros. destruct (le_ge_cases n m);
[rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_nonneg_l.
Qed.
Lemma mul_min_distr_nonneg_r : forall n m p, 0 <= p ->
min (n * p) (m * p) == min n m * p.
Proof.
intros. destruct (le_ge_cases n m);
[rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_nonneg_r.
Qed.
Lemma mul_max_distr_nonpos_l : forall n m p, p <= 0 ->
max (p * n) (p * m) == p * min n m.
Proof.
intros. destruct (le_ge_cases n m).
rewrite min_l by trivial. rewrite max_l. reflexivity. now apply mul_le_mono_nonpos_l.
rewrite min_r by trivial. rewrite max_r. reflexivity. now apply mul_le_mono_nonpos_l.
Qed.
Lemma mul_max_distr_nonpos_r : forall n m p, p <= 0 ->
max (n * p) (m * p) == min n m * p.
Proof.
intros. destruct (le_ge_cases n m).
rewrite min_l by trivial. rewrite max_l. reflexivity. now apply mul_le_mono_nonpos_r.
rewrite min_r by trivial. rewrite max_r. reflexivity. now apply mul_le_mono_nonpos_r.
Qed.
Lemma mul_min_distr_nonpos_l : forall n m p, p <= 0 ->
min (p * n) (p * m) == p * max n m.
Proof.
intros. destruct (le_ge_cases n m).
rewrite max_r by trivial. rewrite min_r. reflexivity. now apply mul_le_mono_nonpos_l.
rewrite max_l by trivial. rewrite min_l. reflexivity. now apply mul_le_mono_nonpos_l.
Qed.
Lemma mul_min_distr_nonpos_r : forall n m p, p <= 0 ->
min (n * p) (m * p) == max n m * p.
Proof.
intros. destruct (le_ge_cases n m).
rewrite max_r by trivial. rewrite min_r. reflexivity. now apply mul_le_mono_nonpos_r.
rewrite max_l by trivial. rewrite min_l. reflexivity. now apply mul_le_mono_nonpos_r.
Qed.
End ZMaxMinProp.
|
