forked from nasa/pvslib
-
Notifications
You must be signed in to change notification settings - Fork 0
/
dl_solution.pvs
379 lines (318 loc) · 12.2 KB
/
dl_solution.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
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
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
dl_solution : THEORY
% Welcome!
%-------------------------------------------------------------------------%
%-------------------------------------------------------------------------%
%| dl_solution: Develops the preliminary information for the dl-solve |%
%| rule. To be moved to dynamic logic and hp_def most likely |%
%-------------------------------------------------------------------------%
% Created Aug 2022
% JTS,MM
% Last Updated Sept 2022
% JTS
%-------------------------------------------------------------------------%
%-------------------------------------------------------------------------%
%----- %
BEGIN
% -----%
IMPORTING analysis@derivatives,
% substitution,
% more_derivative_props,
% structures@for_examples,
% reals@reals_safe_ops,
% chain_rule_re,
% ODEs_equiv,
% ODEs@linear_ode_1D,
% continuity_props,
% fresh_props
dynamic_logic
%%--------------------------------------------
%%--------------------------------------------
%%Define variables
%%--------------------------------------------
l,m: VAR Assigns
j,k: VAR nat
re: VAR RealExpr
r : VAR real
Gamma,Delta : VAR Formulas
P,Q,J,R : VAR BoolExpr
A,B : VAR HP
i : VAR nat
qQ : VAR QBoolExpr
Progress : VAR RealExpr
re1,re2 : VAR RealExpr
Qe : VAR [RealExpr->BoolExpr]
Re : VAR [RealExpr->BoolExpr]
Ae : VAR [RealExpr->HP]
%%--------------------------------------------
%%Define solves, which is solution_odes with
% the initial condition
%%--------------------------------------------
%solves
solves?(R: BoolExpr)(D: (dd?))(ode: ODEs)
(y: [below(length(ode)) -> [real -> [Environment ->real]]]): bool =
FORALL(envi: (R)): solution_odes?(D, ode, envi)
(LAMBDA(i: below(length(ode))): LAMBDA(r: real): y(i)(r)(envi))
%solves u mean y is the unique solution
solves_u?(R: BoolExpr)(D: (dd?))(ode: ODEs)
(y: [below(length(ode)) -> [real -> [Environment ->real]]]): bool =
FORALL(envi: (R)): solution_odes_u?(D, ode, envi)
(LAMBDA(i: below(length(ode))): LAMBDA(r: real): y(i)(r)(envi))
%%--------------------------------------------
%% nnreal as a predicate
%%--------------------------------------------
nnreal?(r: real): bool = (r >= 0)
%%--------------------------------------------
%% zip_sol will take an ode, a 'solution' y
% and zip them together into a MapExprInj
% which will correspond to the Assignments
% made in dl-solve.
%%--------------------------------------------
init_zip_sol(ode:ODEs,
y:[below(length(ode)) -> [real -> [Environment ->real]]],t:real,
%% accumulator with inductive hypothesis in type
acc:{a: MapExprInj | length(a) <= length(ode)
AND FORALL(i:below(length(a))): nth(a,i) =
(nth(ode,i+(length(ode)-length(a)))`1, y(i + (length(ode)-length(a)))(t))}): RECURSIVE
%% output is 'zipped'
{a: MapExprInj | length(a) = length(ode) AND
FORALL(i:below(length(a))): nth(a,i) = (nth(ode,i)`1, y(i)(t))} =
IF length(acc) = length(ode) THEN acc
ELSE
LET ll: MapExprInj = cons( (nth(ode,length(ode)-( length(acc)+1))`1,
y(length(ode)-(length(acc)+1))(t)), acc)
IN
init_zip_sol(ode, y, t, ll)
ENDIF
MEASURE length(ode)-length(acc)
%%--------------------------------------------
%% Test init_zip_sol
% It won't evaluate, but can expand all the way
% with grind
%%--------------------------------------------
v : VAR dLVar
zip_sol_test: LEMMA
(init_zip_sol( (: (v, cnst(5)) :),
(LAMBDA(i:below(1)):
LAMBDA(r:real):
val(v)+cnst(5)+cnst(r)), 5, null) =
(: (v, val(v) + cnst(5) + cnst(5)) :))
%%--------------------------------------------
%% Define zs - zip sol
%%--------------------------------------------
zs(ode:ODEs,y:[below(length(ode)) -> [real -> [Environment ->real]]])(t:real):
MapExprInj =
init_zip_sol(ode,y,t,null)
%%--------------------------------------------
%% map_inj property of zs
%%--------------------------------------------
map_inj_zs: LEMMA
FORALL(ode:ODEs, t:real, i:nat,
y:[below(length(ode)) -> [real -> [Environment ->real]]]):
not_in_map(ode)(i)
IFF
not_in_map(zs(ode,y)(t))(i)
%%--------------------------------------------
%% Solution axiom in not Dl-format
%%--------------------------------------------
solution_domain_ax_ode: LEMMA
FORALL(ode:ODEs,
y:[below(length(ode)) -> [real -> [Environment ->real]]]):
solves_u?(R)(hp(0))(ode)(y)
IMPLIES
( ((: R :) |-
(: ALLRUNS(DIFF( ode , Q ), P) :))
IFF
FORALL(env: (R), t:nnreal):
(FORALL(s:nnreal | s<=t):
Q( assign_sub(zs(ode,y)(s))(env)) )
IMPLIES
P( assign_sub(zs(ode,y)(t))(env) ))
%%--------------------------------------------
%% Solution axiom (rule?) in dl-format
%%--------------------------------------------
dl_solution_domain_iff: LEMMA
FORALL(ode:ODEs, y: (solves_u?(R)(hp(0))(ode))):
LET
ASSIGN_s = LAMBDA(s:real): ASSIGN(zs(ode,y)(s))
IN
(( (: R :) |- (: ALLRUNS(DIFF(ode, Q), P) :))
IFF
((: R :) |-
(: DLFORALL(UPTO(ASSIGN_s,Q)(P)) :)))
%%--------------------------------------------
%% Solution axiom (rule?) in dl-format,
% forward direction
%%--------------------------------------------
dl_solution_domain: LEMMA
FORALL(ode:ODEs, y: (solves_u?(R)(hp(0))(ode))):
LET
ASSIGN_s = LAMBDA(s:real): ASSIGN(zs(ode,y)(s))
IN
((: R :) |-
(: DLFORALL(UPTO(ASSIGN_s,Q)(P)) :))
IMPLIES
((: R :) |- (: ALLRUNS(DIFF(ode, Q), P) :))
%%--------------------------------------------
%% Solution axiom for single variable as in cheat
% sheat
%%--------------------------------------------
solution_domain_ax: LEMMA
FORALL(y:[below(1) -> [real -> [ Environment -> real]]]):
solves_u?(R)(hp(0))((: (v, re1) :))(y)
IMPLIES
(((: R :) |-
(: ALLRUNS(DIFF( (: (v, re1) :), Q ), P) :))
IFF
FORALL(env: (R), t:nnreal):
LET yenv(i:below(1))(r:real): real = y(i)(r)(env)
IN
(FORALL(s:nnreal | s<=t):
Q(env WITH [ (dlvar_index(v)) := yenv(0)(s)]))
IMPLIES
P(env WITH [ (dlvar_index(v)) := yenv(0)(t)]))
%%--------------------------------------------
%% Linear solution (cnst), non dl-version
%%--------------------------------------------
solution_domain_ax_lin: LEMMA
FORALL(m:real):
(((: R :) |-
(: ALLRUNS(DIFF( (: (v, cnst(m)) :), Q ), P) :))
IFF
FORALL(env: (R), t:nnreal):
(FORALL(s:nnreal | s<=t):
Q(env WITH [ (dlvar_index(v)) := val(v)(env) + m*s]))
IMPLIES
P(env WITH [ (dlvar_index(v)) := val(v)(env) + m*t]))
%%--------------------------------------------
%% Linear solution (val not in map),
% non dl-version
%%--------------------------------------------
solution_domain_ax_lin_val: LEMMA
FORALL(w:(different_var?(v))):
(((: R :) |-
(: ALLRUNS(DIFF( (: (v, val(w)) :), Q ), P) :))
IFF
FORALL(env: (R), t:nnreal):
(FORALL(s:nnreal | s<=t):
Q(env WITH [ (dlvar_index(v)) := val(v)(env) + val(w)(env)*s]))
IMPLIES
P(env WITH [ (dlvar_index(v)) := val(v)(env) + val(w)(env)*t]))
%%--------------------------------------------
%% Quadratic solution, non dl-version
%%--------------------------------------------
solution_domain_ax_quad: LEMMA
FORALL(w:(different_var?(v)),m:real):
(((: R :) |-
(: ALLRUNS(DIFF( (: (v, cnst(m)), (w, val(v)) :), Q ), P) :))
IFF
FORALL(env: (R), t:nnreal):
(FORALL(s:nnreal | s<=t):
Q(env WITH [ (dlvar_index(v)) := val(v)(env) + m*s] WITH [ (dlvar_index(w)) := val(w)(env) + val(v)(env)*s + m * s^2 /2] ))
IMPLIES
P(env WITH [ (dlvar_index(v)) := val(v)(env) + m*t] WITH [ (dlvar_index(w)) := val(w)(env) + val(v)(env)*t + m * t^2 /2]))
%%--------------------------------------------
%% Get_index (executable?)
%%--------------------------------------------
get_index(l: MapExprInj)(j: (in_map(l))): RECURSIVE {n:below(length(l)) | dlvar_index(nth(l,n)`1) = j} =
IF dlvar_index(car(l)`1) = j THEN 0
ELSE 1 + get_index(cdr(l))(j)
ENDIF
MEASURE length(l)
%%--------------------------------------------
%%Quad_cnst means j is the quadratic part
% of another variable
%%--------------------------------------------
quad_cnst?(l: MapExprInj)(j: (in_map(l)) ): bool =
(EXISTS(c3:real): nth(l,get_index(l)(j))`2 = cnst(c3))
OR (EXISTS(c4:real,v:dLVar): (nth(l,get_index(l)(j))`2 = cnst(c4) + val(v) AND NOT in_map(l)(dlvar_index(v))))
%%--------------------------------------------
%%Cnst_lins means every derivative is a constant
% or linear (so quadratic solution)
%%--------------------------------------------
cnst_lins?(l: MapExprInj): bool =
FORALL(i: below(length(l))):
(EXISTS(c:real): nth(l,i)`2 = cnst(c))
OR
(EXISTS(c:real,v:dLVar): nth(l,i)`2 = cnst(c) + val(v) AND
((NOT in_map(l)(dlvar_index(v))) OR quad_cnst?(l)(dlvar_index(v))))
cnst_val_0: LEMMA
FORALL(v:dLVar):
cnst(0) + val(v) = val(v)
cnst_val_com: LEMMA
FORALL(c:real,v:dLVar):
val(v) + cnst(c) = cnst(c) + val(v)
val_inj: LEMMA
FORALL(v,w:dLVar):
val(v) = val(w)
IFF
v = w
%%--------------------------------------------
%%Cnst_lins means every derivative is a constant
% or linear (so quadratic solution)
%%--------------------------------------------
in_map_ex(l)(i:nat): RECURSIVE bool =
IF null?(l) THEN FALSE
ELSE dlvar_index(car(l)`1) = i or in_map_ex(cdr(l))(i)
ENDIF
MEASURE length(l)
in_map_ex_eq: LEMMA
FORALL(l):
in_map(l) = in_map_ex(l)
env_nat_shift(k:nat)(i:nat): real = i+k
% change to env_cnst(c:real) (\LAM{}(i:nat) i+k)
env_c(r:real)(i:nat): real = r
env_c_val: LEMMA
FORALL(c:real, w:dLVar): val(v)(env_c(c)) = c
get_val_cnst_id_ex(l:MapExprInj)(i:below(length(l)) |
EXISTS(j: (in_map(l)), c:real): dlvar_index(nth(l,i)`1) /= j AND nth(l,i)`2 = cnst(c) + val(dlvar(j))):
{vc: [below(length(l)), real] | vc`1 /= i
AND nth(l,i)`2 = cnst(vc`2) + val(nth(l,vc`1)`1)
AND (FORALL(c:real,m:below(length(l))): nth(l,i)`2 = cnst(c) + val(nth(l,m)`1) IMPLIES (m=vc`1 AND vc`2 = c))} =
(get_index(l)(nth(l,i)`2(env_nat_shift(0)) - nth(l,i)`2(env_c(0))), nth(l,i)`2(env_c(0)))
is_cnst?(l: (cnst_lins?))(i:below(length(l))): bool =
nth(l,i)`2(env_nat_shift(0)) = nth(l,i)`2(env_nat_shift(1))
is_val_not_in_map?(l: (cnst_lins?))(i:below(length(l))): bool =
(NOT is_cnst?(l)(i)) AND (NOT in_map_ex(l)(nth(l,i)`2(env_nat_shift(0)) - nth(l,i)`2(env_c(0))))
Y_sol_ex(l:(cnst_lins?))(i:below(length(l)))(s:real): [Environment -> real] =
IF is_cnst?(l)(i) OR is_val_not_in_map?(l)(i)
THEN val(nth(l,i)`1) + nth(l,i)`2 * cnst(s)
ELSE val(nth(l,i)`1) + (cnst(nth(l,i)`2(env_c(0))) + val(nth(l,get_val_cnst_id_ex(l)(i)`1)`1))*cnst(s) +
nth(l,get_val_cnst_id_ex(l)(i)`1)`2* cnst(s)^2 / cnst(2)
ENDIF
cnst_lins_def: LEMMA
FORALL(l:(cnst_lins?),k:below(length(l))):
(EXISTS (j: (in_map(l)), c: real):
dlvar_index(nth[MapExpr](l, k)`1) /= j AND
nth[MapExpr](l, k)`2 = (+[Environment])(cnst(c), val(dlvar(j))))
OR is_cnst?(l)(k)
OR is_val_not_in_map?(l)(k)
cnst_lins_sol: LEMMA
FORALL(l:(cnst_lins?),R:BoolExpr,envi:(R)):
solution_odes?(hp(0), l, envi)
(LAMBDA (i: below(length(l))):
LAMBDA (r: real): Y_sol_ex(l)(i)(r)(envi))
cnst_lins_sol_u: LEMMA
FORALL(R:BoolExpr,l:(cnst_lins?)):
solves_u?(R)(hp(0))(l)(Y_sol_ex(l))
solution_domain_ax_cnst_imp_zip: LEMMA
FORALL(ode:(cnst_lins?)):
LET Z = (zs(ode,Y_sol_ex(ode))),
ASSIGN_s = LAMBDA(s:real): ASSIGN(Z(s))
IN
((: R :) |-
(: DLFORALL(UPTO(ASSIGN_s,Q)(P)) :))
IMPLIES
((: R :) |- (: ALLRUNS(DIFF(ode, Q), P) :))
% less restrictive version of the lemma, used in strategies.
solution_domain_ax_cnst_imp_zip_no_hyp: COROLLARY
FORALL(ode:(cnst_lins?)):
LET
Z = (zs(ode,Y_sol_ex(ode))),
ASSIGN_s = LAMBDA(s:real): ASSIGN(Z(s))
IN
((::) |-
(: DLFORALL(UPTO(ASSIGN_s,Q)(P)) :))
IMPLIES
((::) |-
(: ALLRUNS(DIFF(ode, Q), P) :))
END dl_solution