Why3 Standard Library index
This file provides the basic theory of real numbers, and several additional theories for classical real functions.
module Real constant zero : real = 0.0 constant one : real = 1.0 val (=) (x y : real) : bool ensures { result <-> x = y } val function (-_) real : real val function (+) real real : real val function (*) real real : real val predicate (<) real real : bool let predicate (>) (x y : real) = y < x let predicate (<=) (x y : real) = x < y || x = y let predicate (>=) (x y : real) = y <= x clone export algebra.OrderedField with type t = real, constant zero = zero, constant one = one, function (-_) = (-_), function (+) = (+), function (*) = (*), predicate (<=) = (<=) meta "remove_unused:keep" function (+) meta "remove_unused:keep" function (-) (* do not necessarily keep, to allow for linear arithmetic only meta "remove_unused:keep" function (*) meta "remove_unused:keep" function (/) *) meta "remove_unused:keep" function (-_) meta "remove_unused:keep" predicate (<) meta "remove_unused:keep" predicate (<=) meta "remove_unused:keep" predicate (>) meta "remove_unused:keep" predicate (>=) let (-) (x y : real) ensures { result = x - y } = x + -y val (/) (x y:real) : real requires { y <> 0.0 } ensures { result = x / y } end
This theory should be used instead of Real when one wants to use both integer and real binary operators.
module RealInfix use Real let function (+.) (x:real) (y:real) : real = x + y let function (-.) (x:real) (y:real) : real = x - y let function ( *.) (x:real) (y:real) : real = x * y function (/.) (x:real) (y:real) : real = x / y let function (-._) (x:real) : real = - x function inv (x:real) : real = Real.inv x let (=.) (x:real) (y:real) = x = y let predicate (<=.) (x:real) (y:real) = x <= y let predicate (>=.) (x:real) (y:real) = x >= y let predicate ( <.) (x:real) (y:real) = x < y let predicate ( >.) (x:real) (y:real) = x > y val (/.) (x y:real) : real requires { y <> 0.0 } ensures { result = x /. y } end
module Abs use Real let function abs(x : real) : real = if x >= 0.0 then x else -x lemma Abs_le: forall x y:real. abs x <= y <-> -y <= x <= y lemma Abs_pos: forall x:real. abs x >= 0.0 lemma Abs_sum: forall x y:real. abs(x+y) <= abs x + abs y lemma Abs_prod: forall x y:real. abs(x*y) = abs x * abs y lemma triangular_inequality: forall x y z:real. abs(x-z) <= abs(x-y) + abs(y-z) end
module MinMax use Real clone export relations.MinMax with type t = real, predicate le = (<=), goal . end
module FromInt use int.Int as Int use Real function from_int int : real axiom Zero: from_int 0 = 0.0 axiom One: from_int 1 = 1.0 axiom Add: forall x y:int. from_int (Int.(+) x y) = from_int x + from_int y axiom Sub: forall x y:int. from_int (Int.(-) x y) = from_int x - from_int y axiom Mul: forall x y:int. from_int (Int.(*) x y) = from_int x * from_int y axiom Neg: forall x:int. from_int (Int.(-_) (x)) = - from_int x lemma Injective: forall x y: int. from_int x = from_int y -> x = y axiom Monotonic: forall x y:int. Int.(<=) x y -> from_int x <= from_int y end
module Truncate use Real use FromInt function truncate real : int
rounds towards zero
axiom Truncate_int : forall i:int. truncate (from_int i) = i axiom Truncate_down_pos: forall x:real. x >= 0.0 -> from_int (truncate x) <= x < from_int (Int.(+) (truncate x) 1) axiom Truncate_up_neg: forall x:real. x <= 0.0 -> from_int (Int.(-) (truncate x) 1) < x <= from_int (truncate x) axiom Real_of_truncate: forall x:real. x - 1.0 <= from_int (truncate x) <= x + 1.0 axiom Truncate_monotonic: forall x y:real. x <= y -> Int.(<=) (truncate x) (truncate y) axiom Truncate_monotonic_int1: forall x:real, i:int. x <= from_int i -> Int.(<=) (truncate x) i axiom Truncate_monotonic_int2: forall x:real, i:int. from_int i <= x -> Int.(<=) i (truncate x) function floor real : int function ceil real : int
roundings up and down
axiom Floor_int : forall i:int. floor (from_int i) = i axiom Ceil_int : forall i:int. ceil (from_int i) = i axiom Floor_down: forall x:real. from_int (floor x) <= x < from_int (Int.(+) (floor x) 1) axiom Ceil_up: forall x:real. from_int (Int.(-) (ceil x) 1) < x <= from_int (ceil x) axiom Floor_monotonic: forall x y:real. x <= y -> Int.(<=) (floor x) (floor y) axiom Ceil_monotonic: forall x y:real. x <= y -> Int.(<=) (ceil x) (ceil y) end
module Square use Real function sqr (x : real) : real = x * x val function sqrt real : real axiom Sqrt_positive: forall x:real. x >= 0.0 -> sqrt x >= 0.0 axiom Sqrt_square: forall x:real. x >= 0.0 -> sqr (sqrt x) = x axiom Square_sqrt: forall x:real. x >= 0.0 -> sqrt (x*x) = x axiom Sqrt_mul: forall x y:real. x >= 0.0 /\ y >= 0.0 -> sqrt (x*y) = sqrt x * sqrt y axiom Sqrt_le : forall x y:real. 0.0 <= x <= y -> sqrt x <= sqrt y end
module ExpLog use Real val function exp real : real axiom Exp_zero : exp(0.0) = 1.0 axiom Exp_sum : forall x y:real. exp (x+y) = exp x * exp y axiom exp_increasing : forall x y. x <= y -> exp(x) <= exp(y) axiom exp_positive : forall x. exp(x) > 0.0 axiom exp_inv : forall x. exp (-x) = inv (exp x) lemma exp_sum_opposite: forall x : real. exp(x) + exp(-x) >= 2.0 constant e : real = exp 1.0 val function log real : real axiom Log_one : log 1.0 = 0.0 axiom Log_mul : forall x y:real. x > 0.0 /\ y > 0.0 -> log (x*y) = log x + log y axiom log_increasing : forall x y. 0.0 < x <= y -> log(x) <= log(y) axiom Log_exp: forall x:real. log (exp x) = x axiom Exp_log: forall x:real. x > 0.0 -> exp (log x) = x function log2 (x : real) : real = log x / log 2.0 function log10 (x : real) : real = log x / log 10.0 lemma log2_increasing : forall x y. 0. < x <= y -> log2(x) <= log2(y) lemma log10_increasing : forall x y. 0. < x <= y -> log10(x) <= log10(y) end
module PowerInt use int.Int use RealInfix clone export int.Exponentiation with type t = real, constant one = Real.one, function (*) = Real.(*), goal Assoc, goal Unit_def_l, goal Unit_def_r, axiom Power_0, axiom Power_s lemma Pow_ge_one: forall x:real, n:int. 0 <= n /\ 1.0 <=. x -> 1.0 <=. power x n end
module PowerReal use Real use ExpLog function pow real real : real axiom Pow_def: forall x y:real. x > 0.0 -> pow x y = exp (y * log x) lemma Pow_pos: forall x y. x > 0.0 -> pow x y > 0.0 lemma Pow_plus : forall x y z. z > 0.0 -> pow z (x + y) = pow z x * pow z y lemma Pow_mult : forall x y z. x > 0.0 -> pow (pow x y) z = pow x (y * z) lemma Pow_x_zero: forall x:real. x > 0.0 -> pow x 0.0 = 1.0 lemma Pow_x_one: forall x:real. x > 0.0 -> pow x 1.0 = x lemma Pow_one_y: forall y:real. pow 1.0 y = 1.0 use Square lemma Pow_x_two: forall x:real. x > 0.0 -> pow x 2.0 = sqr x lemma Pow_half: forall x:real. x > 0.0 -> pow x 0.5 = sqrt x use FromInt use int.Power lemma pow_from_int: forall x y: int. Int.(<) 0 x -> Int.(<=) 0 y -> pow (from_int x) (from_int y) = from_int (power x y) end
See the wikipedia page.
module Trigonometry use Real use Square use Abs function cos real : real function sin real : real axiom Pythagorean_identity: forall x:real. sqr (cos x) + sqr (sin x) = 1.0 lemma Cos_le_one: forall x:real. abs (cos x) <= 1.0 lemma Sin_le_one: forall x:real. abs (sin x) <= 1.0 axiom Cos_0: cos 0.0 = 1.0 axiom Sin_0: sin 0.0 = 0.0 val constant pi : real axiom Pi_double_precision_bounds: 0x1.921fb54442d18p+1 < pi < 0x1.921fb54442d19p+1 (* axiom Pi_interval: 3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 < pi < 3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197 *) axiom Cos_pi: cos pi = -1.0 axiom Sin_pi: sin pi = 0.0 axiom Cos_pi2: cos (0.5 * pi) = 0.0 axiom Sin_pi2: sin (0.5 * pi) = 1.0 axiom Cos_plus_pi: forall x:real. cos (x + pi) = - cos x axiom Sin_plus_pi: forall x:real. sin (x + pi) = - sin x axiom Cos_plus_pi2: forall x:real. cos (x + 0.5*pi) = - sin x axiom Sin_plus_pi2: forall x:real. sin (x + 0.5*pi) = cos x axiom Cos_neg: forall x:real. cos (-x) = cos x axiom Sin_neg: forall x:real. sin (-x) = - sin x axiom Cos_sum: forall x y:real. cos (x+y) = cos x * cos y - sin x * sin y axiom Sin_sum: forall x y:real. sin (x+y) = sin x * cos y + cos x * sin y function tan (x : real) : real = sin x / cos x function atan real : real axiom Tan_atan: forall x:real. tan (atan x) = x end
See the wikipedia page.
module Hyperbolic use Real use Square use ExpLog function sinh (x : real) : real = 0.5 * (exp x - exp (-x)) function cosh (x : real) : real = 0.5 * (exp x + exp (-x)) function tanh (x : real) : real = sinh x / cosh x function asinh (x : real) : real = log (x + sqrt (sqr x + 1.0)) function acosh (x : real) : real axiom Acosh_def: forall x:real. x >= 1.0 -> acosh x = log (x + sqrt (sqr x - 1.0)) function atanh (x : real) : real axiom Atanh_def: forall x:real. -1.0 < x < 1.0 -> atanh x = 0.5 * log ((1.0+x)/(1.0-x)) end
See the wikipedia page.
module Polar use Real use Square use Trigonometry function hypot (x y : real) : real = sqrt (sqr x + sqr y) function atan2 real real : real axiom X_from_polar: forall x y:real. x = hypot x y * cos (atan2 y x) axiom Y_from_polar: forall x y:real. y = hypot x y * sin (atan2 y x) end module Sum use int.Int use RealInfix let rec ghost function sum (f: int -> real) (a b: int) : real variant { b - a } = if (b <= a) then 0. else sum f a (b - 1) +. f (b - 1) end
Generated by why3doc 1.8.0