pvslib/exact_real_arith/examples/era_examples.pvs at master · nasa/pvslib · GitHub

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
era_examples : THEORY
  BEGIN

  IMPORTING exact_real_arith@strategies

  %%% Examples of the era-numerical strategy.

  %% In simple cases era-numerical will compute the value of the given
  %% expression to a desired precision (which defaults to three decimal places).
  %% Calling (era-numerical <expr>) introduces two new antecedents:
  %% <expr> < b and a < <expr> where a and b are given to the precision
  %% specified by the :precision keyword argument.

  %|- *_num_p* : PROOF
  %|- (then (era-numerical (! 1 1 2) :precision $2) (assert))
  %|- QED

  sqrt23_num_p11 : LEMMA
    0.0046717163 < sqrt(2) + sqrt(3) - pi AND
    sqrt(2) + sqrt(3) - pi < 0.0046717164

  sin6sqrt2_num_p11 : LEMMA
    1.5187420256 < sin(6 * pi / 180) + sqrt(2) AND
    sin(6 * pi / 180) + sqrt(2) < 1.5187420257

  exp_pi_num_p9 : LEMMA
    19.99909997 < exp(pi) - pi AND exp(pi) - pi < 19.99909998

  %% For numbers which are near the edge of the domain of the expression,
  %% zero-prec is used to tell the strategy how much precision is needed to
  %% check that domain rules are satisfied. For example, without specifying
  %% zero-prec in the proof of div_small_z8_p24, the strategy will fail because
  %% 0.0000001 is indistinguishable from zero at the default precision

  %|- *_num_z*_p* : PROOF
  %|- (then (era-numerical (! 1 1 2) :precision $3 :zero-prec $2) (assert))
  %|- QED

  div_small_num_z8_p24 : LEMMA
    3.14159265358979323846264 < 0.0000001 * pi / 0.0000001 AND
    0.0000001 * pi / 0.0000001 < 3.14159265358979323846265

  ln_small_num_z7_p9 : LEMMA
    -16.11809566 < ln(0.0000001) AND ln(0.0000001) < -16.11809565

  %% If there is an equality in the antecedents, era-numerical can replaces the
  %% variable with it's value in the expression.

  trivial_binding : LEMMA
    FORALL (q: rat): q = 1.5 IMPLIES q < q * q

  %|- trivial_binding : PROOF
  %|- (then (skeep) (era-numerical "q * q") (assert))
  %|- QED

  sq_sin_cos_1 : LEMMA
    LET one = sq(sin(1))+sq(cos(1)) IN
    0.999 <= one AND one <= 1.001

%|- sq_sin_cos_1 : PROOF
%|- (then (era-numerical "sq(sin(1)) + sq(cos(1))") (assert))
%|- QED

  %|- *_num_b* : PROOF
  %|- (then (beta) (era-numerical (! 1 1 2) :precision $2 :bin-prec? t) (assert))
  %|- QED

  pi_num_b210:    LEMMA % 60 dp
         3.141592653589793238462643383279502884197169399375105820974944 < pi AND
    pi < 3.141592653589793238462643383279502884197169399375105820974945

  ln2_num_b210:   LEMMA % 60 dp
    LET l :real = ln(2) IN
        0.693147180559945309417232121458176568075500134360255254120680 < l  AND
    l < 0.693147180559945309417232121458176568075500134360255254120681

  e_num_b210:     LEMMA % 60 dp
        2.718281828459045235360287471352662497757247093699959574966967 < e  AND
    e < 2.718281828459045235360287471352662497757247093699959574966968

  sqrt2_num_b210: LEMMA % 60 dp
    LET s :real = sqrt(2) IN
        1.414213562373095048801688724209698078569671875376948073176679 < s  AND
    s < 1.414213562373095048801688724209698078569671875376948073176680


%%% THE COMMENTED LEMMAS CAN BE PROVED AS THE PREVIOUS LEMMAS, BUT THEY
%%% TAKE SEVERAL MINUTES (CAM)

% sin1_num_p60: LEMMA % 60 dp
%    LET s = sin(1) IN
%        0.841470984807896506652502321630298999622563060798371065672751 < s  AND
%    s < 0.841470984807896506652502321630298999622563060798371065672752

%  cos1_num_p60: LEMMA % 60 dp
%    LET c = cos(1) IN
%        0.540302305868139717400936607442976603732310420617922227670097 < c  AND
%    c < 0.540302305868139717400936607442976603732310420617922227670098

END era_examples