-
Notifications
You must be signed in to change notification settings - Fork 50
/
quad_minmax.pvs
169 lines (131 loc) · 5.8 KB
/
quad_minmax.pvs
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
quad_minmax: THEORY
%----------------------------------------------------------------------------
%
% Minimums and Maximums of quadratic functions:
%
% quadratic(a,b,c)(x): real = a*sq(x) + b*x + c
%
%----------------------------------------------------------------------------
BEGIN
IMPORTING quadratic
a : VAR nonzero_real
b,c: VAR real
x,y : VAR real
xl,xu,t: VAR real
f: VAR [real -> real]
epsil: VAR posreal
D,ap: VAR posreal
% ---------- Following apply to both min and max cases -----------
quad_minmaxpt_delta: LEMMA LET f = quadratic(a,b,c), m = -b/(2*a) IN
f(m + t) = f(m - t)
quad_minmaxpt_midpt: LEMMA LET f = quadratic(a,b,c), m = -b/(2*a) IN
x /= y AND f(x) = f(y) IMPLIES m = (x + y)/2
% ---- is_minimum? is also defined in real_fun_preds in analysis library
is_minimum?(x, f): bool = FORALL y : f(x) <= f(y)
quad_min : LEMMA LET f = quadratic(a,b,c),
minpt = -b/(2*a) IN
a > 0 IMPLIES
is_minimum?(minpt,f)
quad_min_val : LEMMA LET f = quadratic(a,b,c),
minpt = -b/(2*a) IN
a > 0
IMPLIES f(x) >= (4*a*c-sq(b))/(4*a)
quad_min_mono_inc : LEMMA LET f = quadratic(a,b,c),
minpt = -b/(2*a) IN
a > 0 IMPLIES
x > y AND y >= minpt
IMPLIES
f(x) > f(y)
quad_min_mono_dec : LEMMA LET f = quadratic(a,b,c),
minpt = -b/(2*a) IN
a > 0 AND
x < y AND y <= minpt
IMPLIES
f(x) > f(y)
quad_min_eq_intv: LEMMA a > 0 AND
quadratic(a,b,c)(xl) = quadratic(a,b,c)(xu) AND
xl < t AND t < xu
IMPLIES
quadratic(a,b,c)(t) < quadratic(a,b,c)(xu)
quad_min_eq_is_in: LEMMA a > 0 AND
quadratic(a,b,c)(xl) = quadratic(a,b,c)(xu) AND
quadratic(a,b,c)(t) < quadratic(a,b,c)(xu) AND
xl < xu
IMPLIES
(xl < t AND t < xu)
quad_loc_min_is_glob_min: LEMMA a > 0 AND (FORALL (y): (x-epsil < y AND
y < x+epsil) IMPLIES
quadratic(a,b,c)(y) >= quadratic(a,b,c)(x))
IMPLIES
x = -b/(2*a)
is_maximum?(x, f): bool = FORALL y : f(x) >= f(y)
quad_max : LEMMA LET f = quadratic(a,b,c),
maxpt = -b/(2*a) IN
a < 0
IMPLIES is_maximum?(maxpt,f)
quad_max_val : LEMMA LET f = quadratic(a,b,c),
maxpt = -b/(2*a) IN
a < 0
IMPLIES f(x) <= (4*a*c-sq(b))/(4*a)
quad_max_mono_inc : LEMMA LET f = quadratic(a,b,c),
maxpt = -b/(2*a) IN
a < 0 AND
x < y AND y <= maxpt
IMPLIES
f(x) < f(y)
quad_max_mono_dec : LEMMA LET f = quadratic(a,b,c),
maxpt = -b/(2*a) IN
a < 0 AND
x > y AND y >= maxpt
IMPLIES
f(x) < f(y)
quad_max_eq_intv: LEMMA a < 0 AND
quadratic(a,b,c)(xl) = quadratic(a,b,c)(xu) AND
xl < t AND t < xu
IMPLIES
quadratic(a,b,c)(t) > quadratic(a,b,c)(xu)
quad_max_eq_is_in: LEMMA a < 0 AND
quadratic(a,b,c)(xl) = quadratic(a,b,c)(xu) AND
quadratic(a,b,c)(t) > quadratic(a,b,c)(xu) AND
xl < xu
IMPLIES
(xl < t AND t < xu)
quad_loc_max_is_glob_max: LEMMA a < 0 AND (FORALL (y): (x-epsil < y AND
y < x+epsil) IMPLIES
quadratic(a,b,c)(y) <= quadratic(a,b,c)(x))
IMPLIES
x = -b/(2*a)
quad_intv_max_at_endpoint: LEMMA a>0 AND xl<=xu IMPLIES
(FORALL (t): xl<=t AND t<=xu IMPLIES quadratic(a,b,c)(t)<=quadratic(a,b,c)(xl))
OR
(FORALL (t): xl<=t AND t<=xu IMPLIES quadratic(a,b,c)(t)<=quadratic(a,b,c)(xu))
quad_intv_increasing_from_min: LEMMA a > 0 AND abs(x-(-b/(2*a))) <= abs(y-(-b/(2*a)))
IMPLIES quadratic(a,b,c)(x) <= quadratic(a,b,c)(y)
% the minimum of a quadratic in an interval
quad_min_int(a,b,c,xl,xu): real =
LET F = quadratic(a,b,c) IN
IF a<0 AND F(xl)>=F(xu) THEN xu
ELSIF a<0 THEN xl
ELSIF 2*a*xl<=-b AND -b<=2*a*xu THEN -b/(2*a)
ELSIF -b<2*a*xl THEN xl
ELSE xu ENDIF
quad_min_interval_def: LEMMA xl<=xu IMPLIES
(xl<=quad_min_int(a,b,c,xl,xu) AND quad_min_int(a,b,c,xl,xu)<=xu)
AND
(FORALL (t): xl<=t AND t<=xu IMPLIES
quadratic(a,b,c)(t)>=quadratic(a,b,c)(quad_min_int(a,b,c,xl,xu)))
% is the quadratic ever <D in the interval [xl,xu]
quad_min_le_D_int(ap,b,c,xl,xu,D): bool =
IF xl>xu THEN FALSE
ELSIF 2*ap*xl<=-b AND -b<=2*ap*xu THEN b^2-4*ap*(c-D)>0
ELSE quadratic(ap,b,c-D)(xl)<0 OR
quadratic(ap,b,c-D)(xu)<0
ENDIF
quad_min_le_D_int_def: LEMMA xl<=xu IMPLIES
(quad_min_le_D_int(ap,b,c,xl,xu,D) IFF
quadratic(ap,b,c)(quad_min_int(ap,b,c,xl,xu))<D)
quad_min_le_D_int_def2: LEMMA xl<=xu IMPLIES
(quad_min_le_D_int(ap,b,c,xl,xu,D) IFF
EXISTS (x:real): xl<=x AND x<=xu AND
quadratic(ap,b,c)(x)<D)
END quad_minmax