metitarski.why 847 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12
theory P

  use import real.Real

  goal x_mul_x_pos :
    forall x:real. x * x >= 0.0

  function sqr (x:real) : real = x * x

  goal sqr_pos :
    forall x:real. sqr x >= 0.0

MARCHE Claude's avatar
MARCHE Claude committed
13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
end

theory P2

  use import real.Real
  use import real.Square

  goal sqr_pos :
    forall x:real. sqr x >= 0.0

end

theory P3

  use import real.Real
  use import real.Trigonometry

30
  (* unprovable without cos-constant.ax, which causes failures for more interesting goals *)
MARCHE Claude's avatar
MARCHE Claude committed
31 32 33 34
  goal cos_bound :
    forall x:real. -1.0 <= cos x <= 1.0

  goal cos_bound_harder :
35
    forall x:real. -0.7 <= x <= 0.7 -> 0.7 <= cos x <= 1.0
MARCHE Claude's avatar
MARCHE Claude committed
36

MARCHE Claude's avatar
MARCHE Claude committed
37 38 39 40 41 42 43 44 45

  use import real.Abs

  goal MethodErrorOK: forall x:real. abs x <= 0x1p-5 ->
    abs (1.0 - 0.5 * (x * x) - cos x) <= 0x1p-24

  goal MethodErrorWrong: forall x:real. abs x <= 0x1p-5 ->
    abs (1.0 - 0.5 * (x * x) - cos x) <= 0x1p-25

MARCHE Claude's avatar
MARCHE Claude committed
46 47
end