Why3 Standard Library index



Theory of reals

This file provides the basic theory of real numbers, and several additional theories for classical real functions.


Real numbers and the basic unary and binary operators

theory Real

  constant zero : real = 0.0
  constant one  : real = 1.0

  predicate (< ) real real
  predicate (> ) (x y : real) = y < x
  predicate (<=) (x y : real) = x < y \/ x = y

  clone export algebra.OrderedField with type t = real,
    constant zero = zero, constant one = one, predicate (<=) = (<=)

end

Alternative Infix Operators

This theory should be used instead of Real when one wants to use both integer and real binary operators.

theory RealInfix

  use import Real

  function (+.) (x:real) (y:real) : real = x + y
  function (-.) (x:real) (y:real) : real = x - y
  function ( *.) (x:real) (y:real) : real = x * y
  function (/.) (x:real) (y:real) : real = x / y
  function (-._) (x:real) : real = - x
  function inv (x:real) : real = Real.inv x

  predicate (<=.) (x:real) (y:real) = x <= y
  predicate (>=.) (x:real) (y:real) = x >= y
  predicate ( <.) (x:real) (y:real) = x < y
  predicate ( >.) (x:real) (y:real) = x > y

end

Absolute Value

theory Abs

  use import Real

  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

Minimum and Maximum

theory MinMax

  use import Real
  clone export relations.MinMax with type t = real, predicate le = (<=),
    goal TotalOrder.Refl,
    goal TotalOrder.Trans,
    goal TotalOrder.Antisymm,
    goal TotalOrder.Total

end

Injection of integers into reals

theory FromInt

  use int.Int
  use import 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

  axiom Monotonic:
    forall x y:int. Int.(<=) x y -> from_int x <= from_int y

end

Various truncation functions

theory Truncate

  use import Real
  use import FromInt

truncate: rounds towards zero

  function truncate real : int

  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)

roundings up and down

  function floor real : int
  function ceil real : int

  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

Square and Square Root

theory Square

  use import Real

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

  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

Exponential and Logarithm

theory ExpLog

  use import Real

  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

  constant e : real = exp 1.0

  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_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

end

Power of a real to an integer

theory PowerInt

  use import int.Int
  use import RealInfix

  clone export int.Exponentiation with
    type t = real, constant one = Real.one, function (*) = Real.(*),
    goal Monoid.Assoc, goal Monoid.Unit_def_l, goal Monoid.Unit_def_r

  lemma Pow_ge_one:
    forall x:real, n:int. 0 <= n /\ 1.0 <=. x -> 1.0 <=. power x n

end

Power of a real to a real exponent

theory PowerReal

  use import Real
  use import 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 import 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

end

Trigonometric Functions

See the wikipedia page.

theory Trigonometry

  use import Real
  use import Square
  use import 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

  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

Hyperbolic Functions

See the wikipedia page.

theory Hyperbolic

  use import Real
  use import Square
  use import 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

Polar Coordinates

See the wikipedia page.

theory Polar

  use import Real
  use import Square
  use import 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

Generated by why3doc 0.88.0