-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathexamples_other.hl
61 lines (45 loc) · 2.45 KB
/
examples_other.hl
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
(* ========================================================================== *)
(* Formal verification of nonlinear inequalities in HOL Light *)
(* *)
(* Copyright (c) 2014 Alexey Solovyev *)
(* *)
(* This file is distributed under the terms of the MIT licence *)
(* ========================================================================== *)
(* -------------------------------------------------------------------------- *)
(* Additional test inequalities *)
(* -------------------------------------------------------------------------- *)
needs "arith_options.hl";;
(* Arith_options.base := 100;; *)
needs "verifier/m_verifier_main.hl";;
needs "verifier_options.hl";;
Verifier_options.info_print_level := 2;;
open M_verifier_main;;
verify_ineq default_params 5
`&0 <= x /\ x <= &1 ==> exp (x pow 3) < &3`;;
verify_ineq default_params 5
`&1 <= x /\ x <= &3 /\ &1 <= y /\ y <= &10
==> log (x pow 2 + y) < &3`;;
(* MetiTarski home page *)
verify_ineq default_params 5
`&0 <= x /\ x <= #1.46 / &10 pow 6 ==>
(#64.42 * sin(#1.71 * &10 pow 6 * x) - #21.08 * cos(#1.71 * &10 pow 6 * x)) * exp(#9.05 * &10 pow 5 * x)
+ #24.24 * exp(-- #1.86 * &10 pow 6 * x) > &0`;;
verify_ineq default_params 5
`&0 <= x /\ x <= &289 /\ -- &1 <= s /\ s <= &1 /\ -- &1 <= c /\ c <= &1 ==>
(s pow 2 + c pow 2 < &1 \/ s pow 2 + c pow 2 > &1 \/
#1.51 - #0.023 * exp(-- #0.019 * x) - (#2.35 * c + #0.42 * s) * exp(#0.00024 * x) > -- &2)`;;
verify_ineq default_params 5
`#0.35 <= t /\ t <= &10 /\ &0 <= v /\ v <= &10 ==>
((#1.565 + #0.313 * v) * cos(#1.16 * v) +
(#0.01340 + #0.00268 * v) * sin(#1.16 * t)) * exp(-- #1.34 * t)
- (#6.55 + #1.31 * v) * exp(-- #0.318 * t) + v + &10 > &0`;;
(* Approximations of abs(x) from
"A certificate-based approach to formally verified approximations" *)
verify_ineq default_params 5
`&0 <= x /\ x <= &1 ==> abs(sqrt(#0.01 + x * x) - abs(x)) < #0.1001`;;
verify_ineq default_params 5
`&0 <= x /\ x <= &1 ==> abs(sqrt(#0.001 * #0.001 + x * x) - abs(x)) < #0.0011`;;
verify_ineq default_params 5
`&0 <= x /\ x <= &1 ==> sqrt(#0.001 * #0.001 + x * x) - abs(x) < #0.0011`;;
verify_ineq default_params 5
`&0 <= x /\ x <= &1 ==> sqrt(#0.001 * #0.001 + x * x) - abs(x) > -- #0.0011`;;