real.why 8.04 KB
Newer Older
1

MARCHE Claude's avatar
MARCHE Claude committed
2
theory Real
MARCHE Claude's avatar
MARCHE Claude committed
3

Andrei Paskevich's avatar
Andrei Paskevich committed
4
5
  function zero : real = 0.0
  function one  : real = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
6

Andrei Paskevich's avatar
Andrei Paskevich committed
7
8
9
  predicate (< ) real real
  predicate (> ) (x y : real) = y < x
  predicate (<=) (x y : real) = x < y \/ x = y
MARCHE Claude's avatar
MARCHE Claude committed
10

Andrei Paskevich's avatar
Andrei Paskevich committed
11
12
  clone export algebra.OrderedField with type t = real,
    function zero = zero, function one = one, predicate (<=) = (<=)
13

14
(*
15
  lemma sub_zero: forall x y:real. x - y = 0.0 -> x = y
16
*)
17

MARCHE Claude's avatar
MARCHE Claude committed
18
19
20
21
22
23
end

theory RealInfix

  use import Real

Andrei Paskevich's avatar
Andrei Paskevich committed
24
25
26
27
28
  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
MARCHE Claude's avatar
MARCHE Claude committed
29

Andrei Paskevich's avatar
Andrei Paskevich committed
30
31
32
33
  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
34
35

end
36
37
38
39
40

theory Abs

  use import Real

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

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

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

47
(*
48
  lemma Abs_zero: forall x:real. abs x = 0.0 -> x = 0.0
49
*)
50

51
52
53
54
55
56
end

theory MinMax

  use import Real

Andrei Paskevich's avatar
Andrei Paskevich committed
57
58
  function min real real : real
  function max real real : real
59

Andrei Paskevich's avatar
Andrei Paskevich committed
60
61
62
63
  axiom Max_is_ge   : forall x y:real. max x y >= x /\ max x y >= y
  axiom Max_is_some : forall x y:real. max x y = x \/ max x y = y
  axiom Min_is_le   : forall x y:real. min x y <= x /\ min x y <= y
  axiom Min_is_some : forall x y:real. min x y = x \/ min x y = y
64
65
66
67
68
69
70
71

end

theory FromInt

  use int.Int
  use import Real

Andrei Paskevich's avatar
Andrei Paskevich committed
72
  function from_int int : real
73

74
75
  axiom Zero: from_int 0 = 0.0
  axiom One: from_int 1 = 1.0
76

MARCHE Claude's avatar
MARCHE Claude committed
77
  axiom Add:
78
    forall x y:int. from_int (Int.(+) x y) = from_int x + from_int y
MARCHE Claude's avatar
MARCHE Claude committed
79
  axiom Sub:
80
    forall x y:int. from_int (Int.(-) x y) = from_int x - from_int y
MARCHE Claude's avatar
MARCHE Claude committed
81
  axiom Mul:
82
    forall x y:int. from_int (Int.(*) x y) = from_int x * from_int y
MARCHE Claude's avatar
MARCHE Claude committed
83
  axiom Neg:
84
    forall x y:int. from_int (Int.(-_) (x)) = - from_int x
85

MARCHE Claude's avatar
MARCHE Claude committed
86
87
88
89
90
91
end

theory FromIntTest

  use import FromInt

92
  lemma Test1: from_int 2 = 2.0
MARCHE Claude's avatar
MARCHE Claude committed
93

94
95
96
97
end

theory Truncate

MARCHE Claude's avatar
MARCHE Claude committed
98
99
100
101
102
  use import Real
  use import FromInt

  (* truncate: rounds towards zero *)

Andrei Paskevich's avatar
Andrei Paskevich committed
103
  function truncate real : int
MARCHE Claude's avatar
MARCHE Claude committed
104
105

  axiom Truncate_int :
106
    forall i:int. truncate (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
107
108

  axiom Truncate_down_pos:
MARCHE Claude's avatar
MARCHE Claude committed
109
    forall x:real. x >= 0.0 ->
110
      from_int (truncate x) <= x < from_int (Int.(+) (truncate x) 1)
MARCHE Claude's avatar
MARCHE Claude committed
111
112

  axiom Truncate_up_neg:
MARCHE Claude's avatar
MARCHE Claude committed
113
    forall x:real. x <= 0.0 ->
114
      from_int (Int.(-) (truncate x) 1) < x <= from_int (truncate x)
MARCHE Claude's avatar
MARCHE Claude committed
115
116

  axiom Real_of_truncate:
117
    forall x:real. x - 1.0 <= from_int (truncate x) <= x + 1.0
MARCHE Claude's avatar
MARCHE Claude committed
118
119

  axiom Truncate_monotonic:
120
    forall x y:real. x <= y -> Int.(<=) (truncate x) (truncate y)
MARCHE Claude's avatar
MARCHE Claude committed
121
122

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

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

  (* roundings up and down *)

Andrei Paskevich's avatar
Andrei Paskevich committed
130
131
  function floor real : int
  function ceil real : int
MARCHE Claude's avatar
MARCHE Claude committed
132
133

  axiom Floor_int :
134
    forall i:int. floor (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
135
136

  axiom Ceil_int :
137
    forall i:int. floor (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
138
139

  axiom Floor_down:
140
    forall x:real. from_int (floor x) <= x < from_int (Int.(+) (floor x) 1)
MARCHE Claude's avatar
MARCHE Claude committed
141
142

  axiom Ceil_up:
143
    forall x:real. from_int (Int.(-) (ceil x) 1) < x <= from_int (ceil x)
MARCHE Claude's avatar
MARCHE Claude committed
144
145

  axiom Floor_monotonic:
146
    forall x y:real. x <= y -> Int.(<=) (floor x) (floor y)
MARCHE Claude's avatar
MARCHE Claude committed
147
148

  axiom Ceil_monotonic:
149
    forall x y:real. x <= y -> Int.(<=) (ceil x) (ceil y)
150
151
152

end

MARCHE Claude's avatar
MARCHE Claude committed
153

MARCHE Claude's avatar
MARCHE Claude committed
154
155
156
157
theory Square

  use import Real

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

Andrei Paskevich's avatar
Andrei Paskevich committed
160
  function sqrt real : real
MARCHE Claude's avatar
MARCHE Claude committed
161

MARCHE Claude's avatar
MARCHE Claude committed
162
  axiom Sqrt_positive:
163
    forall x:real. x >= 0.0 -> sqrt x >= 0.0
MARCHE Claude's avatar
MARCHE Claude committed
164

MARCHE Claude's avatar
MARCHE Claude committed
165
  axiom Sqrt_square:
166
    forall x:real. x >= 0.0 -> sqr (sqrt x) = x
MARCHE Claude's avatar
MARCHE Claude committed
167

MARCHE Claude's avatar
MARCHE Claude committed
168
  axiom Square_sqrt:
169
    forall x:real. x >= 0.0 -> sqrt (x*x) = x
170
171
172

end

MARCHE Claude's avatar
MARCHE Claude committed
173
174
175
176
theory SquareTest

  use import Square

177
178
179
  lemma Sqrt_zero: sqrt 0.0 = 0.0
  lemma Sqrt_one: sqrt 1.0 = 1.0
  lemma Sqrt_four: sqrt 4.0 = 2.0
MARCHE Claude's avatar
MARCHE Claude committed
180
181
182

end

183
184
theory ExpLog

MARCHE Claude's avatar
MARCHE Claude committed
185
186
  use import Real

Andrei Paskevich's avatar
Andrei Paskevich committed
187
  function exp real : real
MARCHE Claude's avatar
MARCHE Claude committed
188
  axiom Exp_zero : exp(0.0) = 1.0
189
  axiom Exp_sum : forall x y:real. exp (x+y) = exp x * exp y
MARCHE Claude's avatar
MARCHE Claude committed
190

Andrei Paskevich's avatar
Andrei Paskevich committed
191
  function e : real = exp 1.0
MARCHE Claude's avatar
MARCHE Claude committed
192

Andrei Paskevich's avatar
Andrei Paskevich committed
193
  function log real : real
194
  axiom Log_one : log 1.0 = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
195
  axiom Log_mul :
Andrei Paskevich's avatar
Andrei Paskevich committed
196
    forall x y:real. x > 0.0 /\ y > 0.0 -> log (x*y) = log x + log y
MARCHE Claude's avatar
MARCHE Claude committed
197

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
202
203
  function log2 (x : real) : real = log x / log 2.0
  function log10 (x : real) : real = log x / log 10.0
204
205
206

end

MARCHE Claude's avatar
MARCHE Claude committed
207
208
209
210
theory ExpLogTest

  use import ExpLog

211
  lemma Log_e : log e = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
212
213
214
215

end


MARCHE Claude's avatar
MARCHE Claude committed
216
theory Power
217

MARCHE Claude's avatar
MARCHE Claude committed
218
219
220
221
  use import Real
  use import Square
  use import ExpLog

Andrei Paskevich's avatar
Andrei Paskevich committed
222
  function pow real real : real
MARCHE Claude's avatar
MARCHE Claude committed
223
224

  axiom Pow_zero_y:
225
    forall y:real. y <> 0.0 -> pow 0.0 y = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
226
227

  axiom Pow_x_zero:
228
    forall x:real. x <> 0.0 -> pow x 0.0 = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
229
230

  axiom Pow_x_one:
231
    forall x:real. pow x 1.0 = x
MARCHE Claude's avatar
MARCHE Claude committed
232
233

  axiom Pow_one_y:
234
    forall y:real. pow 1.0 y = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
235
236

  axiom Pow_x_two:
237
    forall x:real. pow x 2.0 = sqr x
MARCHE Claude's avatar
MARCHE Claude committed
238
239

  axiom Pow_half:
MARCHE Claude's avatar
MARCHE Claude committed
240
    forall x:real. x >= 0.0 -> pow x 0.5 = sqrt x
MARCHE Claude's avatar
MARCHE Claude committed
241
242

  axiom Pow_exp_log:
243
    forall x y:real. x > 0.0 -> pow x y = exp (y * log x)
MARCHE Claude's avatar
MARCHE Claude committed
244

245
246
end

MARCHE Claude's avatar
MARCHE Claude committed
247
248
249
250
theory PowerTest

  use import Power

251
  lemma Pow_2_2 : pow 2.0 2.0 = 4.0
MARCHE Claude's avatar
MARCHE Claude committed
252
253
254
255
256

end



MARCHE Claude's avatar
MARCHE Claude committed
257
(** Trigonometric functions
MARCHE Claude's avatar
MARCHE Claude committed
258
259
    [http://en.wikipedia.org/wiki/Trigonometric_function]
*)
MARCHE Claude's avatar
MARCHE Claude committed
260
theory Trigonometry
MARCHE Claude's avatar
MARCHE Claude committed
261
262
263
264
265

  use import Real
  use import Square
  use import Abs

Andrei Paskevich's avatar
Andrei Paskevich committed
266
267
  function cos real : real
  function sin real : real
MARCHE Claude's avatar
MARCHE Claude committed
268
269

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

272
273
  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
274

275
276
  axiom Cos_0: cos 0.0 = 1.0
  axiom Sin_0: sin 0.0 = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
277

Andrei Paskevich's avatar
Andrei Paskevich committed
278
  function pi : real
MARCHE Claude's avatar
MARCHE Claude committed
279

MARCHE Claude's avatar
more db    
MARCHE Claude committed
280
281
282
283
284
  axiom Pi_interval:
   3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196
   < pi <
   3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197

285
286
  axiom Cos_pi: cos pi = -1.0
  axiom Sin_pi: sin pi = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
287

288
289
  axiom Cos_pi2: cos (0.5 * pi) = 0.0
  axiom Sin_pi2: sin (0.5 * pi) = 1.0
290

291
292
  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
293

294
295
  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
296
297

  axiom Cos_neg:
298
    forall x:real. cos (-x) = cos x
MARCHE Claude's avatar
MARCHE Claude committed
299
  axiom Sin_neg:
300
    forall x:real. sin (-x) = - sin x
MARCHE Claude's avatar
MARCHE Claude committed
301

MARCHE Claude's avatar
MARCHE Claude committed
302
  axiom Cos_sum:
303
    forall x y:real. cos (x+y) = cos x * cos y - sin x * sin y
MARCHE Claude's avatar
MARCHE Claude committed
304
  axiom Sin_sum:
305
    forall x y:real. sin (x+y) = sin x * cos y + cos x * sin y
MARCHE Claude's avatar
MARCHE Claude committed
306

Andrei Paskevich's avatar
Andrei Paskevich committed
307
308
  function tan (x : real) : real = sin x / cos x
  function atan real : real
MARCHE Claude's avatar
MARCHE Claude committed
309
  axiom Tan_atan:
310
    forall x:real. tan (atan x) = x
311
312
313

end

MARCHE Claude's avatar
MARCHE Claude committed
314
315
316
317
318
319
theory TrigonometryTest

  use import Real
  use import Trigonometry
  use import Square

320
  lemma Cos_2_pi : cos (2.0 * pi) = 1.0
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
321
  lemma Sin_2_pi : sin (2.0 * pi) = 0.
322
323
  lemma Tan_pi_3 : tan (pi / 2.0) = sqrt 3.0
  lemma Atan_1   : atan 1.0 = pi / 4.0
MARCHE Claude's avatar
MARCHE Claude committed
324
325
326

end

MARCHE Claude's avatar
MARCHE Claude committed
327
(** hyperbolic functions
MARCHE Claude's avatar
MARCHE Claude committed
328
329
    [http://en.wikipedia.org/wiki/Hyperbolic_function]
*)
330
331
theory Hyperbolic

MARCHE Claude's avatar
MARCHE Claude committed
332
333
334
335
  use import Real
  use import Square
  use import ExpLog

Andrei Paskevich's avatar
Andrei Paskevich committed
336
337
338
  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
339

Andrei Paskevich's avatar
Andrei Paskevich committed
340
341
  function asinh (x : real) : real = log (x + sqrt (sqr x + 1.0))
  function acosh (x : real) : real
MARCHE Claude's avatar
MARCHE Claude committed
342
343
  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
344
  function atanh (x : real) : real
MARCHE Claude's avatar
MARCHE Claude committed
345
346
  axiom Atanh_def:
    forall x:real. -1.0 < x < 1.0 -> atanh x = 0.5 * log ((1.0+x)/(1.0-x))
347
348
349

end

MARCHE Claude's avatar
MARCHE Claude committed
350
(** polar coordinates: atan2, hypot
MARCHE Claude's avatar
MARCHE Claude committed
351
352
    [http://en.wikipedia.org/wiki/Atan2]
*)
353
354
theory Polar

MARCHE Claude's avatar
MARCHE Claude committed
355
356
  use import Real
  use import Square
MARCHE Claude's avatar
MARCHE Claude committed
357
  use import Trigonometry
MARCHE Claude's avatar
MARCHE Claude committed
358

Andrei Paskevich's avatar
Andrei Paskevich committed
359
360
  function hypot (x y : real) : real = sqrt (sqr x + sqr y)
  function atan2 real real : real
MARCHE Claude's avatar
MARCHE Claude committed
361

MARCHE Claude's avatar
MARCHE Claude committed
362
  axiom X_from_polar:
363
    forall x y:real. x = hypot x y * cos (atan2 y x)
MARCHE Claude's avatar
MARCHE Claude committed
364
365

  axiom Y_from_polar:
366
    forall x y:real. y = hypot x y * sin (atan2 y x)
367
368
end