real.why 9.11 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

MARCHE Claude's avatar
MARCHE Claude committed
11
theory 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

Andrei Paskevich's avatar
Andrei Paskevich committed
16
17
18
  predicate (< ) real real
  predicate (> ) (x y : real) = y < x
  predicate (<=) (x y : real) = x < y \/ x = y
MARCHE Claude's avatar
MARCHE Claude committed
19

Andrei Paskevich's avatar
Andrei Paskevich committed
20
  clone export algebra.OrderedField with type t = real,
21
    constant zero = zero, constant one = one, predicate (<=) = (<=)
22

MARCHE Claude's avatar
MARCHE Claude committed
23
(***
24
  lemma sub_zero: forall x y:real. x - y = 0.0 -> x = y
25
*)
26

MARCHE Claude's avatar
MARCHE Claude committed
27
28
end

29
(** {2 Alternative Infix Operators}
MARCHE Claude's avatar
MARCHE Claude committed
30

31
32
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
33
34
35

*)

MARCHE Claude's avatar
MARCHE Claude committed
36
37
38
39
theory RealInfix

  use import Real

Andrei Paskevich's avatar
Andrei Paskevich committed
40
41
42
43
44
  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
45
  function inv (x:real) : real = Real.inv x
MARCHE Claude's avatar
MARCHE Claude committed
46

Andrei Paskevich's avatar
Andrei Paskevich committed
47
48
49
50
  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
MARCHE Claude's avatar
MARCHE Claude committed
51
52

end
53

MARCHE Claude's avatar
MARCHE Claude committed
54
55
(** {2 Absolute Value} *)

56
57
58
59
theory Abs

  use import Real

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
66
(***
67
  lemma Abs_zero: forall x:real. abs x = 0.0 -> x = 0.0
68
*)
69

MARCHE Claude's avatar
MARCHE Claude committed
70
71
72
73
74
75
76
  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)

77
78
end

MARCHE Claude's avatar
MARCHE Claude committed
79
80
(** {2 Minimum and Maximum} *)

81
82
83
theory MinMax

  use import Real
84
  clone export relations.MinMax with type t = real, predicate le = (<=),
85
86
87
88
    goal TotalOrder.Refl,
    goal TotalOrder.Trans,
    goal TotalOrder.Antisymm,
    goal TotalOrder.Total
89
90
91

end

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

94
95
96
97
98
theory FromInt

  use int.Int
  use import Real

Andrei Paskevich's avatar
Andrei Paskevich committed
99
  function from_int int : real
100

101
102
  axiom Zero: from_int 0 = 0.0
  axiom One: from_int 1 = 1.0
103

MARCHE Claude's avatar
MARCHE Claude committed
104
  axiom Add:
105
    forall x y:int. from_int (Int.(+) x y) = from_int x + from_int y
MARCHE Claude's avatar
MARCHE Claude committed
106
  axiom Sub:
107
    forall x y:int. from_int (Int.(-) x y) = from_int x - from_int y
MARCHE Claude's avatar
MARCHE Claude committed
108
  axiom Mul:
109
    forall x y:int. from_int (Int.(*) x y) = from_int x * from_int y
MARCHE Claude's avatar
MARCHE Claude committed
110
  axiom Neg:
111
    forall x:int. from_int (Int.(-_) (x)) = - from_int x
112

MARCHE Claude's avatar
MARCHE Claude committed
113
114
end

MARCHE Claude's avatar
MARCHE Claude committed
115
116
(** {2 Various truncation functions} *)

117
118
theory Truncate

MARCHE Claude's avatar
MARCHE Claude committed
119
120
121
  use import Real
  use import FromInt

MARCHE Claude's avatar
MARCHE Claude committed
122
  (** truncate: rounds towards zero *)
MARCHE Claude's avatar
MARCHE Claude committed
123

Andrei Paskevich's avatar
Andrei Paskevich committed
124
  function truncate real : int
MARCHE Claude's avatar
MARCHE Claude committed
125
126

  axiom Truncate_int :
127
    forall i:int. truncate (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
128
129

  axiom Truncate_down_pos:
MARCHE Claude's avatar
MARCHE Claude committed
130
    forall x:real. x >= 0.0 ->
131
      from_int (truncate x) <= x < from_int (Int.(+) (truncate x) 1)
MARCHE Claude's avatar
MARCHE Claude committed
132
133

  axiom Truncate_up_neg:
MARCHE Claude's avatar
MARCHE Claude committed
134
    forall x:real. x <= 0.0 ->
135
      from_int (Int.(-) (truncate x) 1) < x <= from_int (truncate x)
MARCHE Claude's avatar
MARCHE Claude committed
136
137

  axiom Real_of_truncate:
138
    forall x:real. x - 1.0 <= from_int (truncate x) <= x + 1.0
MARCHE Claude's avatar
MARCHE Claude committed
139
140

  axiom Truncate_monotonic:
141
    forall x y:real. x <= y -> Int.(<=) (truncate x) (truncate y)
MARCHE Claude's avatar
MARCHE Claude committed
142
143

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

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

MARCHE Claude's avatar
MARCHE Claude committed
149
  (** roundings up and down *)
MARCHE Claude's avatar
MARCHE Claude committed
150

Andrei Paskevich's avatar
Andrei Paskevich committed
151
152
  function floor real : int
  function ceil real : int
MARCHE Claude's avatar
MARCHE Claude committed
153
154

  axiom Floor_int :
155
    forall i:int. floor (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
156
157

  axiom Ceil_int :
158
    forall i:int. ceil (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
159
160

  axiom Floor_down:
161
    forall x:real. from_int (floor x) <= x < from_int (Int.(+) (floor x) 1)
MARCHE Claude's avatar
MARCHE Claude committed
162
163

  axiom Ceil_up:
164
    forall x:real. from_int (Int.(-) (ceil x) 1) < x <= from_int (ceil x)
MARCHE Claude's avatar
MARCHE Claude committed
165
166

  axiom Floor_monotonic:
167
    forall x y:real. x <= y -> Int.(<=) (floor x) (floor y)
MARCHE Claude's avatar
MARCHE Claude committed
168
169

  axiom Ceil_monotonic:
170
    forall x y:real. x <= y -> Int.(<=) (ceil x) (ceil y)
171
172
173

end

MARCHE Claude's avatar
MARCHE Claude committed
174
(** {2 Square and Square Root} *)
MARCHE Claude's avatar
MARCHE Claude committed
175

MARCHE Claude's avatar
MARCHE Claude committed
176
177
178
179
theory Square

  use import Real

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

Andrei Paskevich's avatar
Andrei Paskevich committed
182
  function sqrt real : real
MARCHE Claude's avatar
MARCHE Claude committed
183

MARCHE Claude's avatar
MARCHE Claude committed
184
  axiom Sqrt_positive:
185
    forall x:real. x >= 0.0 -> sqrt x >= 0.0
MARCHE Claude's avatar
MARCHE Claude committed
186

MARCHE Claude's avatar
MARCHE Claude committed
187
  axiom Sqrt_square:
188
    forall x:real. x >= 0.0 -> sqr (sqrt x) = x
MARCHE Claude's avatar
MARCHE Claude committed
189

MARCHE Claude's avatar
MARCHE Claude committed
190
  axiom Square_sqrt:
191
    forall x:real. x >= 0.0 -> sqrt (x*x) = x
192

193
194
195
196
197
198
199
  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

200
201
end

MARCHE Claude's avatar
MARCHE Claude committed
202
203
(** {2 Exponential and Logarithm} *)

204
205
theory ExpLog

MARCHE Claude's avatar
MARCHE Claude committed
206
207
  use import Real

Andrei Paskevich's avatar
Andrei Paskevich committed
208
  function exp real : real
MARCHE Claude's avatar
MARCHE Claude committed
209
  axiom Exp_zero : exp(0.0) = 1.0
210
  axiom Exp_sum : forall x y:real. exp (x+y) = exp x * exp y
MARCHE Claude's avatar
MARCHE Claude committed
211

212
  constant e : real = exp 1.0
MARCHE Claude's avatar
MARCHE Claude committed
213

Andrei Paskevich's avatar
Andrei Paskevich committed
214
  function log real : real
215
  axiom Log_one : log 1.0 = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
216
  axiom Log_mul :
Andrei Paskevich's avatar
Andrei Paskevich committed
217
    forall x y:real. x > 0.0 /\ y > 0.0 -> log (x*y) = log x + log y
MARCHE Claude's avatar
MARCHE Claude committed
218

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
223
224
  function log2 (x : real) : real = log x / log 2.0
  function log10 (x : real) : real = log x / log 10.0
225
226
227

end

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

230
231
theory PowerInt

232
233
  use import int.Int
  use import RealInfix
234
235

  clone export int.Exponentiation with
236
237
238
    type t = real, constant one = Real.one, function (*) = Real.(*),
    goal CommutativeMonoid.Assoc, goal CommutativeMonoid.Unit_def_l,
    goal CommutativeMonoid.Unit_def_r, goal CommutativeMonoid.Comm.Comm
239

240
  lemma Pow_ge_one:
Andrei Paskevich's avatar
Andrei Paskevich committed
241
    forall x:real, n:int. 0 <= n /\ 1.0 <=. x -> 1.0 <=. power x n
242

243
244
end

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

247
theory PowerReal
248

MARCHE Claude's avatar
MARCHE Claude committed
249
250
251
  use import Real
  use import ExpLog

Andrei Paskevich's avatar
Andrei Paskevich committed
252
  function pow real real : real
MARCHE Claude's avatar
MARCHE Claude committed
253

254
255
256
257
258
259
260
261
  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
262

263
264
  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
265

266
267
  lemma Pow_x_zero:
    forall x:real. x > 0.0 -> pow x 0.0 = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
268

269
270
271
272
  lemma Pow_x_one:
    forall x:real. x > 0.0 -> pow x 1.0 = x

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

275
  use import Square
MARCHE Claude's avatar
MARCHE Claude committed
276

277
278
  lemma Pow_x_two:
    forall x:real. x > 0.0 -> pow x 2.0 = sqr x
MARCHE Claude's avatar
MARCHE Claude committed
279

280
281
  lemma Pow_half:
    forall x:real. x > 0.0 -> pow x 0.5 = sqrt x
MARCHE Claude's avatar
MARCHE Claude committed
282

283
284
end

MARCHE Claude's avatar
MARCHE Claude committed
285
(** {2 Trigonometric Functions}
MARCHE Claude's avatar
MARCHE Claude committed
286

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

MARCHE Claude's avatar
MARCHE Claude committed
289
*)
290

MARCHE Claude's avatar
MARCHE Claude committed
291
theory Trigonometry
MARCHE Claude's avatar
MARCHE Claude committed
292
293
294
295
296

  use import Real
  use import Square
  use import Abs

Andrei Paskevich's avatar
Andrei Paskevich committed
297
298
  function cos real : real
  function sin real : real
MARCHE Claude's avatar
MARCHE Claude committed
299
300

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

303
304
  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
305

306
307
  axiom Cos_0: cos 0.0 = 1.0
  axiom Sin_0: sin 0.0 = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
308

309
  constant pi : real
MARCHE Claude's avatar
MARCHE Claude committed
310

311
312
313
  axiom Pi_double_precision_bounds:
    0x1.921fb54442d18p+1 < pi < 0x1.921fb54442d19p+1
(*
MARCHE Claude's avatar
more db    
MARCHE Claude committed
314
315
316
317
  axiom Pi_interval:
   3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196
   < pi <
   3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197
318
*)
MARCHE Claude's avatar
more db    
MARCHE Claude committed
319

320
321
  axiom Cos_pi: cos pi = -1.0
  axiom Sin_pi: sin pi = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
322

323
324
  axiom Cos_pi2: cos (0.5 * pi) = 0.0
  axiom Sin_pi2: sin (0.5 * pi) = 1.0
325

326
327
  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
328

329
330
  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
331
332

  axiom Cos_neg:
333
    forall x:real. cos (-x) = cos x
MARCHE Claude's avatar
MARCHE Claude committed
334
  axiom Sin_neg:
335
    forall x:real. sin (-x) = - sin x
MARCHE Claude's avatar
MARCHE Claude committed
336

MARCHE Claude's avatar
MARCHE Claude committed
337
  axiom Cos_sum:
338
    forall x y:real. cos (x+y) = cos x * cos y - sin x * sin y
MARCHE Claude's avatar
MARCHE Claude committed
339
  axiom Sin_sum:
340
    forall x y:real. sin (x+y) = sin x * cos y + cos x * sin y
MARCHE Claude's avatar
MARCHE Claude committed
341

Andrei Paskevich's avatar
Andrei Paskevich committed
342
343
  function tan (x : real) : real = sin x / cos x
  function atan real : real
MARCHE Claude's avatar
MARCHE Claude committed
344
  axiom Tan_atan:
345
    forall x:real. tan (atan x) = x
346
347
348

end

MARCHE Claude's avatar
MARCHE Claude committed
349
(** {2 Hyperbolic Functions}
350
351
352

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

MARCHE Claude's avatar
MARCHE Claude committed
353
*)
354

355
356
theory Hyperbolic

MARCHE Claude's avatar
MARCHE Claude committed
357
358
359
360
  use import Real
  use import Square
  use import ExpLog

Andrei Paskevich's avatar
Andrei Paskevich committed
361
362
363
  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
364

Andrei Paskevich's avatar
Andrei Paskevich committed
365
366
  function asinh (x : real) : real = log (x + sqrt (sqr x + 1.0))
  function acosh (x : real) : real
MARCHE Claude's avatar
MARCHE Claude committed
367
368
  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
369
  function atanh (x : real) : real
MARCHE Claude's avatar
MARCHE Claude committed
370
371
  axiom Atanh_def:
    forall x:real. -1.0 < x < 1.0 -> atanh x = 0.5 * log ((1.0+x)/(1.0-x))
372
373
374

end

MARCHE Claude's avatar
MARCHE Claude committed
375
(** {2 Polar Coordinates}
376
377
378

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

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

381
382
theory Polar

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

Andrei Paskevich's avatar
Andrei Paskevich committed
387
388
  function hypot (x y : real) : real = sqrt (sqr x + sqr y)
  function atan2 real real : real
MARCHE Claude's avatar
MARCHE Claude committed
389

MARCHE Claude's avatar
MARCHE Claude committed
390
  axiom X_from_polar:
391
    forall x y:real. x = hypot x y * cos (atan2 y x)
MARCHE Claude's avatar
MARCHE Claude committed
392
393

  axiom Y_from_polar:
394
    forall x y:real. y = hypot x y * sin (atan2 y x)
395

396
end