mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
30 lines
542 B
Plaintext
30 lines
542 B
Plaintext
|
|
theory TestReal
|
|
|
|
(*
|
|
|
|
Examples from http://michalkonecny.github.io/polypaver/_site/index.html
|
|
|
|
*)
|
|
|
|
use real.Real
|
|
|
|
goal add1 : 1.0 + 2.0 = 3.0
|
|
|
|
goal add2 : 1.2 + 3.4 = 5.6
|
|
|
|
use real.Square
|
|
use real.ExpLog
|
|
|
|
goal exp_hyp:
|
|
forall x:real. 0.01 < x < 5.1785 ->
|
|
(3.0 + sqr x / 11.0) * ((exp x - exp (-x))/2.0) <
|
|
x * (2.0 + (exp x + exp (-x))/2.0 + sqr x / 11.0)
|
|
|
|
goal g1:
|
|
forall a b:real.
|
|
-10.0 <= a <= 10.0 /\ -10.0 <= b <= 10.0 /\ b > a + 0.1 ->
|
|
exp b - exp a > (b-a) * exp ((a + b) / 2.0)
|
|
|
|
end
|