real.why 7.02 KB
Newer Older
1 2 3


theory Real 
MARCHE Claude's avatar
MARCHE Claude committed
4

MARCHE Claude's avatar
MARCHE Claude committed
5
  logic (< )(real, real)
6
  logic (<=)(real, real)
MARCHE Claude's avatar
MARCHE Claude committed
7
  logic (> )(real, real)
8 9
  logic (>=)(real, real)
  
MARCHE Claude's avatar
MARCHE Claude committed
10
  (* TODO : they are total order relations *)
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27

  logic zero : real = 0.0
  logic one  : real = 1.0
  
  clone export algebra.Field with 
     type t = real, logic zero = zero, logic one = one
end 

theory Abs

  use import Real

  logic abs(real) : real

  axiom Pos: forall x:real. x >= 0.0 -> abs(x) = x
  axiom Neg: forall x:real. x <= 0.0 -> abs(x) = -x

28
  lemma Abs_le: forall x,y:real. abs(x) <= y <-> -y <= x <= y
MARCHE Claude's avatar
MARCHE Claude committed
29

MARCHE Claude's avatar
MARCHE Claude committed
30 31
  lemma Abs_pos: forall x:real. abs(x) >= 0.0

32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66
end

theory MinMax

  use import Real

  logic min(real,real) : real
  logic max(real,real) : real

  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

end

theory FromInt

  use int.Int
  use import Real

  logic from_int(int) : real

  axiom Zero: from_int(0) = 0.0
  axiom One: from_int(1) = 1.0

  axiom Add: 
    forall x,y:int. from_int(Int.(+)(x,y)) = from_int(x) + from_int(y)
  axiom Sub: 
    forall x,y:int. from_int(Int.(-)(x,y)) = from_int(x) - from_int(y)
  axiom Mul: 
    forall x,y:int. from_int(Int.(*)(x,y)) = from_int(x) * from_int(y)
  axiom Neg: 
    forall x,y:int. from_int(Int.(-_)(x)) = - from_int(x)

MARCHE Claude's avatar
MARCHE Claude committed
67 68 69 70 71 72 73
end

theory FromIntTest

  use import FromInt

  lemma Test1: from_int(2) = 2.0
MARCHE Claude's avatar
MARCHE Claude committed
74

75 76 77 78
end

theory Truncate

MARCHE Claude's avatar
MARCHE Claude committed
79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130
  use import Real
  use import FromInt

  (* truncate: rounds towards zero *)

  logic truncate(real) : int

  axiom Truncate_int :
    forall i:int. truncate(from_int(i)) = i

  axiom Truncate_down_pos:
    forall x:real. x >= 0.0 -> 
      from_int(truncate(x)) <= x < from_int(Int.(+)(truncate(x),1))

  axiom Truncate_up_neg:
    forall x:real. x <= 0.0 -> 
      from_int(Int.(-)(truncate(x),1)) < x <= from_int(truncate(x))

  axiom Real_of_truncate:
    forall x:real. x - 1.0 <= from_int(truncate(x)) <= x + 1.0

  axiom Truncate_monotonic:
    forall x,y:real. x <= y -> Int.(<=)(truncate(x),truncate(y))

  axiom Truncate_monotonic_int1:
    forall x:real, i:int. x <= from_int(i) -> Int.(<=)(truncate(x),i)

  axiom Truncate_monotonic_int2:
    forall x:real, i:int. from_int(i) <= x -> Int.(<=)(i,truncate(x))

  (* roundings up and down *)

  logic floor(real) : int
  logic ceil(real) : int

  axiom Floor_int :
    forall i:int. floor(from_int(i)) = i

  axiom Ceil_int :
    forall i:int. floor(from_int(i)) = i

  axiom Floor_down:
    forall x:real. from_int(floor(x)) <= x < from_int(Int.(+)(floor(x),1))

  axiom Ceil_up:
    forall x:real. from_int(Int.(-)(ceil(x),1)) < x <= from_int(ceil(x))

  axiom Floor_monotonic:
    forall x,y:real. x <= y -> Int.(<=)(floor(x),floor(y))

  axiom Ceil_monotonic:
    forall x,y:real. x <= y -> Int.(<=)(ceil(x),ceil(y))
131 132 133

end

MARCHE Claude's avatar
MARCHE Claude committed
134

MARCHE Claude's avatar
MARCHE Claude committed
135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150
theory Square

  use import Real

  logic sqr(x:real):real = x * x

  logic sqrt(real):real

  axiom Sqrt_positive: 
    forall x:real. x >= 0.0 -> sqrt(x) >= 0.0

  axiom Sqrt_square:  
    forall x:real. x >= 0.0 -> sqr(sqrt(x)) = x

  axiom Square_sqrt: 
    forall x:real. x >= 0.0 -> sqrt(x*x) = x
151 152 153

end

MARCHE Claude's avatar
MARCHE Claude committed
154 155 156 157 158 159 160 161 162 163
theory SquareTest

  use import Square

  lemma Sqrt_zero: sqrt(0.0) = 0.0
  lemma Sqrt_one: sqrt(1.0) = 1.0
  lemma Sqrt_four: sqrt(4.0) = 2.0

end

164 165
theory ExpLog

MARCHE Claude's avatar
MARCHE Claude committed
166 167 168 169 170 171
  use import Real

  logic exp(real) : real
  axiom Exp_zero : exp(0.0) = 1.0
  axiom Exp_sum : forall x,y:real. exp(x+y) = exp(x)*exp(y)

MARCHE Claude's avatar
MARCHE Claude committed
172 173
  logic e : real = exp(1.0)

MARCHE Claude's avatar
MARCHE Claude committed
174 175 176 177 178 179 180 181 182
  logic log(real) : real
  axiom Log_one : log(1.0) = 0.0
  axiom Log_mul : 
    forall x,y:real. x > 0.0 and y > 0.0 -> log(x*y) = log(x)+log(y)

  axiom Log_exp: forall x:real. log(exp(x)) = x

  axiom Exp_log: forall x:real. x > 0.0 -> exp(log(x)) = x

MARCHE Claude's avatar
MARCHE Claude committed
183
  logic log2(x:real) : real = log(x)/log(2.0)
MARCHE Claude's avatar
MARCHE Claude committed
184
  logic log10(x:real) : real = log(x)/log(10.0)
185 186 187

end

MARCHE Claude's avatar
MARCHE Claude committed
188 189 190 191 192 193 194 195 196
theory ExpLogTest

  use import ExpLog

  lemma Log_e : log(e) = 1.0

end


197 198
theory Power 

MARCHE Claude's avatar
MARCHE Claude committed
199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220
  use import Real
  use import Square
  use import ExpLog

  logic pow(real,real) : real

  axiom Pow_zero_y:
    forall y:real. y <> 0.0 -> pow(0.0,y) = 0.0

  axiom Pow_x_zero:
    forall x:real. x <> 0.0 -> pow(x,0.0) = 1.0

  axiom Pow_x_one:
    forall x:real. pow(x,1.0) = x

  axiom Pow_one_y:
    forall y:real. pow(1.0,y) = 1.0

  axiom Pow_x_two:
    forall x:real. pow(x,2.0) = sqr(x)

  axiom Pow_half:
MARCHE Claude's avatar
MARCHE Claude committed
221
    forall x:real. x >= 0.0 -> pow(x,0.5) = sqrt(x)  
MARCHE Claude's avatar
MARCHE Claude committed
222 223

  axiom Pow_exp_log:
Andrei Paskevich's avatar
Andrei Paskevich committed
224
    forall x,y:real. x > 0.0 -> pow(x,y) = exp(y*log(x))
MARCHE Claude's avatar
MARCHE Claude committed
225

226 227
end

MARCHE Claude's avatar
MARCHE Claude committed
228 229 230 231 232 233 234 235 236 237
theory PowerTest

  use import Power

  lemma Pow_2_2 : pow(2.0,2.0) = 4.0

end



MARCHE Claude's avatar
MARCHE Claude committed
238 239 240
(** Trigonometric functions 
    [http://en.wikipedia.org/wiki/Trigonometric_function]
*)
MARCHE Claude's avatar
MARCHE Claude committed
241
theory Trigonometry
MARCHE Claude's avatar
MARCHE Claude committed
242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265

  use import Real
  use import Square
  use import Abs

  logic cos(real) : real
  logic sin(real) : real

  axiom Pythagorean_identity:
    forall x:real. sqr(cos(x))+sqr(sin(x)) = 1.0

  lemma Cos_le_one: forall x:real. abs(cos(x)) <= 1.0
  lemma Sin_le_one: forall x:real. abs(sin(x)) <= 1.0

  axiom Cos_0: cos(0.0) = 1.0
  axiom Sin_0: sin(0.0) = 0.0

  logic pi : real

  axiom Cos_pi: cos(pi) = -1.0
  axiom Sin_pi: sin(pi) = 0.0

  axiom Cos_pi2: cos(0.5*pi) = 0.0
  axiom Sin_pi2: sin(0.5*pi) = 1.0
266

MARCHE Claude's avatar
MARCHE Claude committed
267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286
  axiom Cos_plus_pi: forall x:real. cos(x+pi) = -cos(x)
  axiom Sin_plus_pi: forall x:real. sin(x+pi) = -sin(x)

  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)

  axiom Cos_neg:
    forall x:real. cos(-x) = cos(x)
  axiom Sin_neg:
    forall x:real. sin(-x) = -sin(x)
 
  axiom Cos_sum:
    forall x,y:real. cos(x+y) = cos(x)*cos(y)-sin(x)*sin(y)
  axiom Sin_sum:
    forall x,y:real. sin(x+y) = sin(x)*cos(y)+cos(x)*sin(y)

  logic tan(x:real) : real = sin(x) / cos(x)
  logic atan(real) : real
  axiom Tan_atan:
    forall x:real. tan(atan(x)) = x
287 288 289

end

MARCHE Claude's avatar
MARCHE Claude committed
290 291 292 293 294 295 296 297 298 299 300 301 302
theory TrigonometryTest

  use import Real
  use import Trigonometry
  use import Square

  lemma Cos_2_pi : cos(2.0 * pi) = 1.0
  lemma Sin_2_pi : cos(2.0 * pi) = 0.
  lemma Tan_pi_3 : tan(pi / 2.0) = sqrt(3.0)
  lemma Atan_1 : atan(1.0) = pi / 4.0

end

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

MARCHE Claude's avatar
MARCHE Claude committed
308 309 310 311 312 313 314 315 316 317 318 319 320 321
  use import Real
  use import Square
  use import ExpLog

  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)

  logic arsinh(x:real) : real = log(x+sqrt(sqr(x)+1.0))
  logic arcosh(x:real) : real
  axiom Arcosh_def:
    forall x:real. x >= 1.0 -> arcosh(x) = log(x+sqrt(sqr(x)-1.0))
  logic artanh(x:real) : real
  axiom Artanh_def:
322
    forall x:real. -1.0 < x < 1.0 -> artanh(x) = 0.5*log((1.0+x)/(1.0-x))
323 324 325

end

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

MARCHE Claude's avatar
MARCHE Claude committed
331 332
  use import Real
  use import Square
MARCHE Claude's avatar
MARCHE Claude committed
333
  use import Trigonometry
MARCHE Claude's avatar
MARCHE Claude committed
334 335 336

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

  axiom Y_from_polar:
    forall x,y:real. y = hypot(x,y)*sin(atan2(y,x))
343 344
end