real.mlw 9.66 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 62 63 64
  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
65

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

end
71

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

74
module Abs
75

76
  use Real
77

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

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

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

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

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

95 96
end

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

99
module MinMax
100

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

end

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

108
module FromInt
109

110
  use int.Int as Int
111
  use Real
112

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

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
132 133
end

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

136
module Truncate
137

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

end

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

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

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

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

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

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

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

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

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

219 220
end

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

223
module ExpLog
224

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

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

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

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

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

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

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

end

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

249
module PowerInt
250

251 252
  use int.Int
  use RealInfix
253 254

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

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

261 262
end

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

265
module PowerReal
266

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

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

272 273 274 275 276 277 278 279
  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
280

281 282
  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
283

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

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

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

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

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

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

301 302
  use FromInt
  use int.Power
303

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


308 309
end

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

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

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

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

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

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

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

328 329
  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
330

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

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

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

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

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

351 352
  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
353

354 355
  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
356 357

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

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

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

end

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

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

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

380
module Hyperbolic
381

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

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

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

end

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

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

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

406
module Polar
407

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

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

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

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

421
end