mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
19 lines
313 B
Plaintext
19 lines
313 B
Plaintext
theory CosineSingle
|
|
|
|
use real.Real
|
|
use real.Abs
|
|
use real.Trigonometry
|
|
|
|
(* approximation of cosine function by 1 - x^2 / 2 on interval [-1/32; 1/32] *)
|
|
|
|
|
|
|
|
lemma MethodError: forall x:real. abs x <= 0x1p-5 ->
|
|
abs (1.0 - 0.5 * (x * x) - cos x) <= 0x1p-24
|
|
(* this one is proved in Coq + interval tactics *)
|
|
|
|
|
|
end
|
|
|
|
|