pvslib/Riemann/examples/riemann_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
riemann_examples : THEORY
  BEGIN

  IMPORTING Riemann@strategies

  %% Examples demonstrating the use of riemann

  % More precision can be obtained by increasing the PRECISION argument, but
  % this will slow down the strategy.

  % The default value of BREAKS is 12. Using fewer can speed up the strategy
  % but it will give less precise results

  cos_test:LEMMA integral(0,1,cos) ## [|0.841 , 0.843|]
  %|- cos_test : PROOF
  %|- (riemann)
  %|- QED

  cos_test1:LEMMA integral(0,1,cos) ## [|0.8414 , 0.8417|]
  %|- cos_test1 : PROOF
  %|- (riemann)
  %|- QED

  cos_test5:LEMMA integral(0,1/230,cos) ## [|0.00434781236,0.00434781241|]
  %|- cos_test5 : PROOF
  %|- (riemann)
  %|- QED

  sin_test1:LEMMA integral(0,1.4142135,sin) ## [|0.843 , 0.8449|]
  %|- sin_test1 : PROOF
  %|- (riemann)
  %|- QED

  sin_test:LEMMA integral(0,1/30,sin) ## [|0.000555 , 0.000556|]
  %|- sin_test : PROOF
  %|- (riemann :breaks 13 :precision 4)
  %|- QED

  sin_test2:LEMMA integral(0,2,sin) ## [|1.4158 , 1.4165|]
  %|- sin_test2 : PROOF
  %|- (riemann)
  %|- QED

  sin_test4:LEMMA integral(-1.5,1,sin) ## [|-0.474 , -0.468|]
  %|- sin_test4 : PROOF
  %|- (riemann)
  %|- QED

  exp_test3:LEMMA integral(0,3,exp) ## [|19.0 , 19.1|]
  %|- exp_test3 : PROOF
  %|- (riemann :precision 3)
  %|- QED

  expcos : LEMMA integral(0, 1, exp * cos) ## [| 1.377, 1.379 |]
  %|- expcos : PROOF
  %|- (riemann)
  %|- QED

  sin_half_period : LEMMA integral(0, 3.14159, sin) ## [| 1.99, 2.01 |]
  %|- sin_half_period : PROOF
  %|- (riemann)
  %|- QED

  % idr can be used to refer to the integration variable

  square : LEMMA integral(0, 2, 3 * idr ^ 2) ## [| 7.99, 8.01 |]
  %|- square : PROOF
  %|- (riemann)
  %|- QED

  % The "o" operator can be used for composition. It is best to explicitly import
  % function_props when doing this even though it's in the prelude because it
  % allows you to fully instantiate o

  IMPORTING function_props[real, real, real]

  comp : LEMMA integral(0, 1, exp o cos) ## [| 2.33, 2.35 |]
  %|- comp : PROOF
  %|- (riemann)
  %|- QED

  %|- *_TCC1 : PROOF
  %|- (prove-integrable?)
  %|- QED

END riemann_examples