metitarski.why 847 Bytes
 MARCHE Claude committed Oct 16, 2013 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 committed Oct 16, 2013 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 committed Oct 16, 2013 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 committed Oct 16, 2013 36 `````` `````` MARCHE Claude committed Oct 22, 2013 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 committed Oct 16, 2013 46 47 ``````end ``````