real.mlw 9.69 KB
Newer Older
1

Guillaume Melquiond's avatar
Guillaume Melquiond committed
2
(** {1 Theory of reals}
MARCHE Claude's avatar
MARCHE Claude committed
3

4 5
This file provides the basic theory of real numbers, and several
additional theories for classical real functions.
MARCHE Claude's avatar
MARCHE Claude committed
6 7 8 9

*)

(** {2 Real numbers and the basic unary and binary operators} *)
10

11
module Real
MARCHE Claude's avatar
MARCHE Claude committed
12

13 14
  constant zero : real = 0.0
  constant one  : real = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
15

16 17 18 19 20 21 22 23 24 25 26
  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 (-)  (x y : real) = x + -y
  let predicate (>)  (x y : real) = y < x
  let predicate (<=) (x y : real) = x < y || x = y
  let predicate (>=) (x y : real) = y <= x
MARCHE Claude's avatar
MARCHE Claude committed
27

Andrei Paskevich's avatar
Andrei Paskevich committed
28
  clone export algebra.OrderedField with type t = real,
29 30
    constant zero = zero, constant one = one,
    function (-_) = (-_), function (+) = (+),
31
    function (*) = (*), predicate (<=) = (<=)
32

33 34 35 36
  val (/) (x y:real) : real
    requires { y <> 0.0 }
    ensures  { result = x / y }

MARCHE Claude's avatar
MARCHE Claude committed
37
(***
38
  lemma sub_zero: forall x y:real. x - y = 0.0 -> x = y
39
*)
40

MARCHE Claude's avatar
MARCHE Claude committed
41 42
end

43
(** {2 Alternative Infix Operators}
MARCHE Claude's avatar
MARCHE Claude committed
44

45 46
This theory should be used instead of Real when one wants to use both
integer and real binary operators.
MARCHE Claude's avatar
MARCHE Claude committed
47 48 49

*)

50
module RealInfix
MARCHE Claude's avatar
MARCHE Claude committed
51

52
  use Real
MARCHE Claude's avatar
MARCHE Claude committed
53

54 55 56
  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
Andrei Paskevich's avatar
Andrei Paskevich committed
57
  function (/.) (x:real) (y:real) : real = x / y
58
  let function (-._) (x:real) : real = - x
59
  function inv (x:real) : real = Real.inv x
MARCHE Claude's avatar
MARCHE Claude committed
60

61
  let (=.) (x:real) (y:real) = x = y
62 63 64 65
  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
MARCHE Claude's avatar
MARCHE Claude committed
66

67 68 69
  val (/.) (x y:real) : real
    requires { y <> 0.0 }
    ensures  { result = x /. y }
MARCHE Claude's avatar
MARCHE Claude committed
70 71

end
72

MARCHE Claude's avatar
MARCHE Claude committed
73 74
(** {2 Absolute Value} *)

75
module Abs
76

77
  use Real
78

Andrei Paskevich's avatar
Andrei Paskevich committed
79
  function abs(x : real) : real = if x >= 0.0 then x else -x
80

81
  lemma Abs_le: forall x y:real. abs x <= y <-> -y <= x <= y
MARCHE Claude's avatar
MARCHE Claude committed
82

83
  lemma Abs_pos: forall x:real. abs x >= 0.0
MARCHE Claude's avatar
MARCHE Claude committed
84

MARCHE Claude's avatar
MARCHE Claude committed
85
(***
86
  lemma Abs_zero: forall x:real. abs x = 0.0 -> x = 0.0
87
*)
88

MARCHE Claude's avatar
MARCHE Claude committed
89 90 91 92 93 94 95
  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)

96 97
end

MARCHE Claude's avatar
MARCHE Claude committed
98 99
(** {2 Minimum and Maximum} *)

100
module MinMax
101

102
  use Real
103
  clone export relations.MinMax with type t = real, predicate le = (<=), goal .
104 105 106

end

MARCHE Claude's avatar
MARCHE Claude committed
107 108
(** {2 Injection of integers into reals} *)

109
module FromInt
110

111
  use int.Int as Int
112
  use Real
113

Andrei Paskevich's avatar
Andrei Paskevich committed
114
  function from_int int : real
115

116 117
  axiom Zero: from_int 0 = 0.0
  axiom One: from_int 1 = 1.0
118

MARCHE Claude's avatar
MARCHE Claude committed
119
  axiom Add:
120
    forall x y:int. from_int (Int.(+) x y) = from_int x + from_int y
MARCHE Claude's avatar
MARCHE Claude committed
121
  axiom Sub:
122
    forall x y:int. from_int (Int.(-) x y) = from_int x - from_int y
MARCHE Claude's avatar
MARCHE Claude committed
123
  axiom Mul:
124
    forall x y:int. from_int (Int.(*) x y) = from_int x * from_int y
MARCHE Claude's avatar
MARCHE Claude committed
125
  axiom Neg:
126
    forall x:int. from_int (Int.(-_) (x)) = - from_int x
127

128
  lemma Injective:
129
    forall x y: int. from_int x = from_int y -> x = y
130 131 132
  axiom Monotonic:
    forall x y:int. Int.(<=) x y -> from_int x <= from_int y

MARCHE Claude's avatar
MARCHE Claude committed
133 134
end

MARCHE Claude's avatar
MARCHE Claude committed
135 136
(** {2 Various truncation functions} *)

137
module Truncate
138

139 140
  use Real
  use FromInt
MARCHE Claude's avatar
MARCHE Claude committed
141

MARCHE Claude's avatar
MARCHE Claude committed
142
  (** truncate: rounds towards zero *)
MARCHE Claude's avatar
MARCHE Claude committed
143

Andrei Paskevich's avatar
Andrei Paskevich committed
144
  function truncate real : int
MARCHE Claude's avatar
MARCHE Claude committed
145 146

  axiom Truncate_int :
147
    forall i:int. truncate (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
148 149

  axiom Truncate_down_pos:
MARCHE Claude's avatar
MARCHE Claude committed
150
    forall x:real. x >= 0.0 ->
151
      from_int (truncate x) <= x < from_int (Int.(+) (truncate x) 1)
MARCHE Claude's avatar
MARCHE Claude committed
152 153

  axiom Truncate_up_neg:
MARCHE Claude's avatar
MARCHE Claude committed
154
    forall x:real. x <= 0.0 ->
155
      from_int (Int.(-) (truncate x) 1) < x <= from_int (truncate x)
MARCHE Claude's avatar
MARCHE Claude committed
156 157

  axiom Real_of_truncate:
158
    forall x:real. x - 1.0 <= from_int (truncate x) <= x + 1.0
MARCHE Claude's avatar
MARCHE Claude committed
159 160

  axiom Truncate_monotonic:
161
    forall x y:real. x <= y -> Int.(<=) (truncate x) (truncate y)
MARCHE Claude's avatar
MARCHE Claude committed
162 163

  axiom Truncate_monotonic_int1:
164
    forall x:real, i:int. x <= from_int i -> Int.(<=) (truncate x) i
MARCHE Claude's avatar
MARCHE Claude committed
165 166

  axiom Truncate_monotonic_int2:
167
    forall x:real, i:int. from_int i <= x -> Int.(<=) i (truncate x)
MARCHE Claude's avatar
MARCHE Claude committed
168

MARCHE Claude's avatar
MARCHE Claude committed
169
  (** roundings up and down *)
MARCHE Claude's avatar
MARCHE Claude committed
170

Andrei Paskevich's avatar
Andrei Paskevich committed
171 172
  function floor real : int
  function ceil real : int
MARCHE Claude's avatar
MARCHE Claude committed
173 174

  axiom Floor_int :
175
    forall i:int. floor (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
176 177

  axiom Ceil_int :
178
    forall i:int. ceil (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
179 180

  axiom Floor_down:
181
    forall x:real. from_int (floor x) <= x < from_int (Int.(+) (floor x) 1)
MARCHE Claude's avatar
MARCHE Claude committed
182 183

  axiom Ceil_up:
184
    forall x:real. from_int (Int.(-) (ceil x) 1) < x <= from_int (ceil x)
MARCHE Claude's avatar
MARCHE Claude committed
185 186

  axiom Floor_monotonic:
187
    forall x y:real. x <= y -> Int.(<=) (floor x) (floor y)
MARCHE Claude's avatar
MARCHE Claude committed
188 189

  axiom Ceil_monotonic:
190
    forall x y:real. x <= y -> Int.(<=) (ceil x) (ceil y)
191 192 193

end

MARCHE Claude's avatar
MARCHE Claude committed
194
(** {2 Square and Square Root} *)
MARCHE Claude's avatar
MARCHE Claude committed
195

196
module Square
MARCHE Claude's avatar
MARCHE Claude committed
197

198
  use Real
MARCHE Claude's avatar
MARCHE Claude committed
199

Andrei Paskevich's avatar
Andrei Paskevich committed
200
  function sqr (x : real) : real = x * x
MARCHE Claude's avatar
MARCHE Claude committed
201

Andrei Paskevich's avatar
Andrei Paskevich committed
202
  function sqrt real : real
MARCHE Claude's avatar
MARCHE Claude committed
203

MARCHE Claude's avatar
MARCHE Claude committed
204
  axiom Sqrt_positive:
205
    forall x:real. x >= 0.0 -> sqrt x >= 0.0
MARCHE Claude's avatar
MARCHE Claude committed
206

MARCHE Claude's avatar
MARCHE Claude committed
207
  axiom Sqrt_square:
208
    forall x:real. x >= 0.0 -> sqr (sqrt x) = x
MARCHE Claude's avatar
MARCHE Claude committed
209

MARCHE Claude's avatar
MARCHE Claude committed
210
  axiom Square_sqrt:
211
    forall x:real. x >= 0.0 -> sqrt (x*x) = x
212

213 214 215 216 217 218 219
  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

220 221
end

MARCHE Claude's avatar
MARCHE Claude committed
222 223
(** {2 Exponential and Logarithm} *)

224
module ExpLog
225

226
  use Real
MARCHE Claude's avatar
MARCHE Claude committed
227

Andrei Paskevich's avatar
Andrei Paskevich committed
228
  function exp real : real
MARCHE Claude's avatar
MARCHE Claude committed
229
  axiom Exp_zero : exp(0.0) = 1.0
230
  axiom Exp_sum : forall x y:real. exp (x+y) = exp x * exp y
MARCHE Claude's avatar
MARCHE Claude committed
231

232
  constant e : real = exp 1.0
MARCHE Claude's avatar
MARCHE Claude committed
233

Andrei Paskevich's avatar
Andrei Paskevich committed
234
  function log real : real
235
  axiom Log_one : log 1.0 = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
236
  axiom Log_mul :
Andrei Paskevich's avatar
Andrei Paskevich committed
237
    forall x y:real. x > 0.0 /\ y > 0.0 -> log (x*y) = log x + log y
MARCHE Claude's avatar
MARCHE Claude committed
238

239
  axiom Log_exp: forall x:real. log (exp x) = x
MARCHE Claude's avatar
MARCHE Claude committed
240

241
  axiom Exp_log: forall x:real. x > 0.0 -> exp (log x) = x
MARCHE Claude's avatar
MARCHE Claude committed
242

Andrei Paskevich's avatar
Andrei Paskevich committed
243 244
  function log2 (x : real) : real = log x / log 2.0
  function log10 (x : real) : real = log x / log 10.0
245 246 247

end

MARCHE Claude's avatar
MARCHE Claude committed
248
(** {2 Power of a real to an integer} *)
249

250
module PowerInt
251

252 253
  use int.Int
  use RealInfix
254 255

  clone export int.Exponentiation with
256
    type t = real, constant one = Real.one, function (*) = Real.(*),
257
    goal Assoc, goal Unit_def_l, goal Unit_def_r, axiom Power_0, axiom Power_s
258

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

262 263
end

MARCHE Claude's avatar
MARCHE Claude committed
264
(** {2 Power of a real to a real exponent} *)
265

266
module PowerReal
267

268 269
  use Real
  use ExpLog
MARCHE Claude's avatar
MARCHE Claude committed
270

Andrei Paskevich's avatar
Andrei Paskevich committed
271
  function pow real real : real
MARCHE Claude's avatar
MARCHE Claude committed
272

273 274 275 276 277 278 279 280
  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
MARCHE Claude's avatar
MARCHE Claude committed
281

282 283
  lemma Pow_mult :
    forall x y z. x > 0.0 -> pow (pow x y) z = pow x (y * z)
MARCHE Claude's avatar
MARCHE Claude committed
284

285 286
  lemma Pow_x_zero:
    forall x:real. x > 0.0 -> pow x 0.0 = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
287

288 289 290 291
  lemma Pow_x_one:
    forall x:real. x > 0.0 -> pow x 1.0 = x

  lemma Pow_one_y:
292
    forall y:real. pow 1.0 y = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
293

294
  use Square
MARCHE Claude's avatar
MARCHE Claude committed
295

296 297
  lemma Pow_x_two:
    forall x:real. x > 0.0 -> pow x 2.0 = sqr x
MARCHE Claude's avatar
MARCHE Claude committed
298

299 300
  lemma Pow_half:
    forall x:real. x > 0.0 -> pow x 0.5 = sqrt x
MARCHE Claude's avatar
MARCHE Claude committed
301

302 303
  use FromInt
  use int.Power
304

305
  lemma pow_from_int: forall x y: int. Int.(<) 0 x -> Int.(<=) 0 y ->
306 307 308
                      pow (from_int x) (from_int y) = from_int (power x y)


309 310
end

MARCHE Claude's avatar
MARCHE Claude committed
311
(** {2 Trigonometric Functions}
MARCHE Claude's avatar
MARCHE Claude committed
312

313 314
See the {h <a href="http://en.wikipedia.org/wiki/Trigonometric_function">wikipedia page</a>}.

MARCHE Claude's avatar
MARCHE Claude committed
315
*)
316

317
module Trigonometry
MARCHE Claude's avatar
MARCHE Claude committed
318

319 320 321
  use Real
  use Square
  use Abs
MARCHE Claude's avatar
MARCHE Claude committed
322

Andrei Paskevich's avatar
Andrei Paskevich committed
323 324
  function cos real : real
  function sin real : real
MARCHE Claude's avatar
MARCHE Claude committed
325 326

  axiom Pythagorean_identity:
327
    forall x:real. sqr (cos x) + sqr (sin x) = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
328

329 330
  lemma Cos_le_one: forall x:real. abs (cos x) <= 1.0
  lemma Sin_le_one: forall x:real. abs (sin x) <= 1.0
MARCHE Claude's avatar
MARCHE Claude committed
331

332 333
  axiom Cos_0: cos 0.0 = 1.0
  axiom Sin_0: sin 0.0 = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
334

335
  constant pi : real
MARCHE Claude's avatar
MARCHE Claude committed
336

337 338 339
  axiom Pi_double_precision_bounds:
    0x1.921fb54442d18p+1 < pi < 0x1.921fb54442d19p+1
(*
MARCHE Claude's avatar
MARCHE Claude committed
340 341 342 343
  axiom Pi_interval:
   3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196
   < pi <
   3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197
344
*)
MARCHE Claude's avatar
MARCHE Claude committed
345

346 347
  axiom Cos_pi: cos pi = -1.0
  axiom Sin_pi: sin pi = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
348

349 350
  axiom Cos_pi2: cos (0.5 * pi) = 0.0
  axiom Sin_pi2: sin (0.5 * pi) = 1.0
351

352 353
  axiom Cos_plus_pi: forall x:real. cos (x + pi) = - cos x
  axiom Sin_plus_pi: forall x:real. sin (x + pi) = - sin x
MARCHE Claude's avatar
MARCHE Claude committed
354

355 356
  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
MARCHE Claude's avatar
MARCHE Claude committed
357 358

  axiom Cos_neg:
359
    forall x:real. cos (-x) = cos x
MARCHE Claude's avatar
MARCHE Claude committed
360
  axiom Sin_neg:
361
    forall x:real. sin (-x) = - sin x
MARCHE Claude's avatar
MARCHE Claude committed
362

MARCHE Claude's avatar
MARCHE Claude committed
363
  axiom Cos_sum:
364
    forall x y:real. cos (x+y) = cos x * cos y - sin x * sin y
MARCHE Claude's avatar
MARCHE Claude committed
365
  axiom Sin_sum:
366
    forall x y:real. sin (x+y) = sin x * cos y + cos x * sin y
MARCHE Claude's avatar
MARCHE Claude committed
367

Andrei Paskevich's avatar
Andrei Paskevich committed
368 369
  function tan (x : real) : real = sin x / cos x
  function atan real : real
MARCHE Claude's avatar
MARCHE Claude committed
370
  axiom Tan_atan:
371
    forall x:real. tan (atan x) = x
372 373 374

end

MARCHE Claude's avatar
MARCHE Claude committed
375
(** {2 Hyperbolic Functions}
376 377 378

See the {h <a href="http://en.wikipedia.org/wiki/Hyperbolic_function">wikipedia page</a>}.

MARCHE Claude's avatar
MARCHE Claude committed
379
*)
380

381
module Hyperbolic
382

383 384 385
  use Real
  use Square
  use ExpLog
MARCHE Claude's avatar
MARCHE Claude committed
386

Andrei Paskevich's avatar
Andrei Paskevich committed
387 388 389
  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
MARCHE Claude's avatar
MARCHE Claude committed
390

Andrei Paskevich's avatar
Andrei Paskevich committed
391 392
  function asinh (x : real) : real = log (x + sqrt (sqr x + 1.0))
  function acosh (x : real) : real
MARCHE Claude's avatar
MARCHE Claude committed
393 394
  axiom Acosh_def:
    forall x:real. x >= 1.0 -> acosh x = log (x + sqrt (sqr x - 1.0))
Andrei Paskevich's avatar
Andrei Paskevich committed
395
  function atanh (x : real) : real
MARCHE Claude's avatar
MARCHE Claude committed
396 397
  axiom Atanh_def:
    forall x:real. -1.0 < x < 1.0 -> atanh x = 0.5 * log ((1.0+x)/(1.0-x))
398 399 400

end

MARCHE Claude's avatar
MARCHE Claude committed
401
(** {2 Polar Coordinates}
402 403 404

See the {h <a href="http://en.wikipedia.org/wiki/Atan2">wikipedia page</a>}.

MARCHE Claude's avatar
MARCHE Claude committed
405
*)
406

407
module Polar
408

409 410 411
  use Real
  use Square
  use Trigonometry
MARCHE Claude's avatar
MARCHE Claude committed
412

Andrei Paskevich's avatar
Andrei Paskevich committed
413 414
  function hypot (x y : real) : real = sqrt (sqr x + sqr y)
  function atan2 real real : real
MARCHE Claude's avatar
MARCHE Claude committed
415

MARCHE Claude's avatar
MARCHE Claude committed
416
  axiom X_from_polar:
417
    forall x y:real. x = hypot x y * cos (atan2 y x)
MARCHE Claude's avatar
MARCHE Claude committed
418 419

  axiom Y_from_polar:
420
    forall x y:real. y = hypot x y * sin (atan2 y x)
421

422
end