polypaver.why 563 Bytes
Newer Older
1

MARCHE Claude's avatar
MARCHE Claude committed
2
theory TestReal
3 4 5 6 7 8 9 10

  (*

  Examples from http://michalkonecny.github.io/polypaver/_site/index.html

*)

  use import real.Real
MARCHE Claude's avatar
MARCHE Claude committed
11 12 13 14 15 16

  goal add1 : 1.0 + 2.0 = 3.0

  goal add2 : 1.2 + 3.4 = 5.6

  use import real.Square
17 18
  use import real.ExpLog

MARCHE Claude's avatar
MARCHE Claude committed
19 20 21 22 23
  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)

24 25 26
  goal g1:
    forall a b:real.
      -10.0 <= a <= 10.0 /\ -10.0 <= b <= 10.0 /\ b > a + 0.1 ->
MARCHE Claude's avatar
MARCHE Claude committed
27
      exp b - exp a > (b-a) * exp ((a + b) / 2.0)
28 29

end