real.why 7.48 KB
Newer Older
1
2

theory Real 
MARCHE Claude's avatar
MARCHE Claude committed
3

4
5
6
7
8
9
  logic zero : real = 0.0
  logic one  : real = 1.0
  
  clone export algebra.Field with 
     type t = real, logic zero = zero, logic one = one

10
11
12
13
  logic (< ) real real
  logic (<=) (x y : real) = x < y or x = y
  logic (> ) (x y : real) = y < x
  logic (>=) (x y : real) = y <= x
14
  
15
16
  clone export relations.TotalOrder with
    type t = real, logic rel = (<=)
17
18
19
20
21
22
23

end 

theory Abs

  use import Real

24
  logic abs(x : real) : real = if x >= 0.0 then x else -x
25

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

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

30
31
32
33
34
35
end

theory MinMax

  use import Real

36
37
  logic min real real : real
  logic max real real : real
38

39
40
41
42
  axiom Max_is_ge   : forall x y:real. max x y >= x and max x y >= y
  axiom Max_is_some : forall x y:real. max x y = x or max x y = y
  axiom Min_is_le   : forall x y:real. min x y <= x and min x y <= y
  axiom Min_is_some : forall x y:real. min x y = x or min x y = y
43
44
45
46
47
48
49
50

end

theory FromInt

  use int.Int
  use import Real

51
  logic from_int int : real
52

53
54
  axiom Zero: from_int 0 = 0.0
  axiom One: from_int 1 = 1.0
55
56

  axiom Add: 
57
    forall x y:int. from_int (Int.(+) x y) = from_int x + from_int y
58
  axiom Sub: 
59
    forall x y:int. from_int (Int.(-) x y) = from_int x - from_int y
60
  axiom Mul: 
61
    forall x y:int. from_int (Int.(*) x y) = from_int x * from_int y
62
  axiom Neg: 
63
    forall x y:int. from_int (Int.(-_) (x)) = - from_int x
64

MARCHE Claude's avatar
MARCHE Claude committed
65
66
67
68
69
70
end

theory FromIntTest

  use import FromInt

71
  lemma Test1: from_int 2 = 2.0
MARCHE Claude's avatar
MARCHE Claude committed
72

73
74
75
76
end

theory Truncate

MARCHE Claude's avatar
MARCHE Claude committed
77
78
79
80
81
  use import Real
  use import FromInt

  (* truncate: rounds towards zero *)

82
  logic truncate real : int
MARCHE Claude's avatar
MARCHE Claude committed
83
84

  axiom Truncate_int :
85
    forall i:int. truncate (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
86
87
88

  axiom Truncate_down_pos:
    forall x:real. x >= 0.0 -> 
89
      from_int (truncate x) <= x < from_int (Int.(+) (truncate x) 1)
MARCHE Claude's avatar
MARCHE Claude committed
90
91
92

  axiom Truncate_up_neg:
    forall x:real. x <= 0.0 -> 
93
      from_int (Int.(-) (truncate x) 1) < x <= from_int (truncate x)
MARCHE Claude's avatar
MARCHE Claude committed
94
95

  axiom Real_of_truncate:
96
    forall x:real. x - 1.0 <= from_int (truncate x) <= x + 1.0
MARCHE Claude's avatar
MARCHE Claude committed
97
98

  axiom Truncate_monotonic:
99
    forall x y:real. x <= y -> Int.(<=) (truncate x) (truncate y)
MARCHE Claude's avatar
MARCHE Claude committed
100
101

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

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

  (* roundings up and down *)

109
110
  logic floor real : int
  logic ceil real : int
MARCHE Claude's avatar
MARCHE Claude committed
111
112

  axiom Floor_int :
113
    forall i:int. floor (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
114
115

  axiom Ceil_int :
116
    forall i:int. floor (from_int i) = i
MARCHE Claude's avatar
MARCHE Claude committed
117
118

  axiom Floor_down:
119
    forall x:real. from_int (floor x) <= x < from_int (Int.(+) (floor x) 1)
MARCHE Claude's avatar
MARCHE Claude committed
120
121

  axiom Ceil_up:
122
    forall x:real. from_int (Int.(-) (ceil x) 1) < x <= from_int (ceil x)
MARCHE Claude's avatar
MARCHE Claude committed
123
124

  axiom Floor_monotonic:
125
    forall x y:real. x <= y -> Int.(<=) (floor x) (floor y)
MARCHE Claude's avatar
MARCHE Claude committed
126
127

  axiom Ceil_monotonic:
128
    forall x y:real. x <= y -> Int.(<=) (ceil x) (ceil y)
129
130
131

end

MARCHE Claude's avatar
MARCHE Claude committed
132

MARCHE Claude's avatar
MARCHE Claude committed
133
134
135
136
theory Square

  use import Real

137
  logic sqr (x : real) : real = x * x
MARCHE Claude's avatar
MARCHE Claude committed
138

139
  logic sqrt real : real
MARCHE Claude's avatar
MARCHE Claude committed
140
141

  axiom Sqrt_positive: 
142
    forall x:real. x >= 0.0 -> sqrt x >= 0.0
MARCHE Claude's avatar
MARCHE Claude committed
143
144

  axiom Sqrt_square:  
145
    forall x:real. x >= 0.0 -> sqr (sqrt x) = x
MARCHE Claude's avatar
MARCHE Claude committed
146
147

  axiom Square_sqrt: 
148
    forall x:real. x >= 0.0 -> sqrt (x*x) = x
149
150
151

end

MARCHE Claude's avatar
MARCHE Claude committed
152
153
154
155
theory SquareTest

  use import Square

156
157
158
  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
159
160
161

end

162
163
theory ExpLog

MARCHE Claude's avatar
MARCHE Claude committed
164
165
  use import Real

166
  logic exp real : real
MARCHE Claude's avatar
MARCHE Claude committed
167
  axiom Exp_zero : exp(0.0) = 1.0
168
  axiom Exp_sum : forall x y:real. exp (x+y) = exp x * exp y
MARCHE Claude's avatar
MARCHE Claude committed
169

170
  logic e : real = exp 1.0
MARCHE Claude's avatar
MARCHE Claude committed
171

172
  logic log real : real
173
  axiom Log_one : log 1.0 = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
174
  axiom Log_mul : 
175
    forall x y:real. x > 0.0 and y > 0.0 -> log (x*y) = log x + log y
MARCHE Claude's avatar
MARCHE Claude committed
176

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

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

181
182
  logic log2 (x : real) : real = log x / log 2.0
  logic log10 (x : real) : real = log x / log 10.0
183
184
185

end

MARCHE Claude's avatar
MARCHE Claude committed
186
187
188
189
theory ExpLogTest

  use import ExpLog

190
  lemma Log_e : log e = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
191
192
193
194

end


195
196
theory Power 

MARCHE Claude's avatar
MARCHE Claude committed
197
198
199
200
  use import Real
  use import Square
  use import ExpLog

201
  logic pow real real : real
MARCHE Claude's avatar
MARCHE Claude committed
202
203

  axiom Pow_zero_y:
204
    forall y:real. y <> 0.0 -> pow 0.0 y = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
205
206

  axiom Pow_x_zero:
207
    forall x:real. x <> 0.0 -> pow x 0.0 = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
208
209

  axiom Pow_x_one:
210
    forall x:real. pow x 1.0 = x
MARCHE Claude's avatar
MARCHE Claude committed
211
212

  axiom Pow_one_y:
213
    forall y:real. pow 1.0 y = 1.0
MARCHE Claude's avatar
MARCHE Claude committed
214
215

  axiom Pow_x_two:
216
    forall x:real. pow x 2.0 = sqr x
MARCHE Claude's avatar
MARCHE Claude committed
217
218

  axiom Pow_half:
219
    forall x:real. x >= 0.0 -> pow x 0.5 = sqrt x  
MARCHE Claude's avatar
MARCHE Claude committed
220
221

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

224
225
end

MARCHE Claude's avatar
MARCHE Claude committed
226
227
228
229
theory PowerTest

  use import Power

230
  lemma Pow_2_2 : pow 2.0 2.0 = 4.0
MARCHE Claude's avatar
MARCHE Claude committed
231
232
233
234
235

end



MARCHE Claude's avatar
MARCHE Claude committed
236
237
238
(** Trigonometric functions 
    [http://en.wikipedia.org/wiki/Trigonometric_function]
*)
MARCHE Claude's avatar
MARCHE Claude committed
239
theory Trigonometry
MARCHE Claude's avatar
MARCHE Claude committed
240
241
242
243
244

  use import Real
  use import Square
  use import Abs

245
246
  logic cos real : real
  logic sin real : real
MARCHE Claude's avatar
MARCHE Claude committed
247
248

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

251
252
  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
253

254
255
  axiom Cos_0: cos 0.0 = 1.0
  axiom Sin_0: sin 0.0 = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
256
257
258

  logic pi : real

MARCHE Claude's avatar
more db    
MARCHE Claude committed
259
260
261
262
263
  axiom Pi_interval:
   3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196
   < pi <
   3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197

264
265
  axiom Cos_pi: cos pi = -1.0
  axiom Sin_pi: sin pi = 0.0
MARCHE Claude's avatar
MARCHE Claude committed
266

267
268
  axiom Cos_pi2: cos (0.5 * pi) = 0.0
  axiom Sin_pi2: sin (0.5 * pi) = 1.0
269

270
271
  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
272

273
274
  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
275
276

  axiom Cos_neg:
277
    forall x:real. cos (-x) = cos x
MARCHE Claude's avatar
MARCHE Claude committed
278
  axiom Sin_neg:
279
    forall x:real. sin (-x) = - sin x
MARCHE Claude's avatar
MARCHE Claude committed
280
281
 
  axiom Cos_sum:
282
    forall x y:real. cos (x+y) = cos x * cos y - sin x * sin y
MARCHE Claude's avatar
MARCHE Claude committed
283
  axiom Sin_sum:
284
    forall x y:real. sin (x+y) = sin x * cos y + cos x * sin y
MARCHE Claude's avatar
MARCHE Claude committed
285

286
287
  logic tan (x : real) : real = sin x / cos x
  logic atan real : real
MARCHE Claude's avatar
MARCHE Claude committed
288
  axiom Tan_atan:
289
    forall x:real. tan (atan x) = x
290
291
292

end

MARCHE Claude's avatar
MARCHE Claude committed
293
294
295
296
297
298
theory TrigonometryTest

  use import Real
  use import Trigonometry
  use import Square

299
  lemma Cos_2_pi : cos (2.0 * pi) = 1.0
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
300
  lemma Sin_2_pi : sin (2.0 * pi) = 0.
301
302
  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
303
304
305

end

MARCHE Claude's avatar
MARCHE Claude committed
306
307
308
(** hyperbolic functions 
    [http://en.wikipedia.org/wiki/Hyperbolic_function]
*)
309
310
theory Hyperbolic

MARCHE Claude's avatar
MARCHE Claude committed
311
312
313
314
  use import Real
  use import Square
  use import ExpLog

315
316
317
  logic sinh (x : real) : real = 0.5 * (exp x - exp (-x))
  logic cosh (x : real) : real = 0.5 * (exp x + exp (-x))
  logic tanh (x : real) : real = sinh x / cosh x
MARCHE Claude's avatar
MARCHE Claude committed
318

319
320
  logic arsinh (x : real) : real = log (x + sqrt (sqr x + 1.0))
  logic arcosh (x : real) : real
MARCHE Claude's avatar
MARCHE Claude committed
321
  axiom Arcosh_def:
322
    forall x:real. x >= 1.0 -> arcosh x = log (x + sqrt (sqr x - 1.0))
323
  logic artanh (x : real) : real
MARCHE Claude's avatar
MARCHE Claude committed
324
  axiom Artanh_def:
325
    forall x:real. -1.0 < x < 1.0 -> artanh x = 0.5 * log ((1.0+x)/(1.0-x))
326
327
328

end

MARCHE Claude's avatar
MARCHE Claude committed
329
330
331
(** polar coordinates: atan2, hypot 
    [http://en.wikipedia.org/wiki/Atan2]
*)
332
333
theory Polar

MARCHE Claude's avatar
MARCHE Claude committed
334
335
  use import Real
  use import Square
MARCHE Claude's avatar
MARCHE Claude committed
336
  use import Trigonometry
MARCHE Claude's avatar
MARCHE Claude committed
337

338
339
  logic hypot (x y : real) : real = sqrt (sqr x + sqr y)
  logic atan2 real real : real
340
 
MARCHE Claude's avatar
MARCHE Claude committed
341
  axiom X_from_polar:
342
    forall x y:real. x = hypot x y * cos (atan2 y x)
MARCHE Claude's avatar
MARCHE Claude committed
343
344

  axiom Y_from_polar:
345
    forall x y:real. y = hypot x y * sin (atan2 y x)
346
347
end