examples/tests-provers/polypaver.why

   1
   2 theory TestReal
   3
   4   (*
   5
   6   Examples from http://michalkonecny.github.io/polypaver/_site/index.html
   7
   8 *)
   9
  10   use real.Real
  11
  12   goal add1 : 1.0 + 2.0 = 3.0
  13
  14   goal add2 : 1.2 + 3.4 = 5.6
  15
  16   use real.Square
  17   use real.ExpLog
  18
  19   goal exp_hyp:
  20     forall x:real. 0.01 < x < 5.1785 ->
  21       (3.0 + sqr x / 11.0) * ((exp x - exp (-x))/2.0) <
  22         x * (2.0 + (exp x + exp (-x))/2.0 + sqr x / 11.0)
  23
  24   goal g1:
  25     forall a b:real.
  26       -10.0 <= a <= 10.0 /\ -10.0 <= b <= 10.0 /\ b > a + 0.1 ->
  27       exp b - exp a > (b-a) * exp ((a + b) / 2.0)
  28
  29 end