real.why 7.02 KB
 Jean-Christophe Filliâtre committed Mar 23, 2010 1 2 3 `````` theory Real `````` MARCHE Claude committed Mar 26, 2010 4 `````` `````` MARCHE Claude committed Mar 24, 2010 5 `````` logic (< )(real, real) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 6 `````` logic (<=)(real, real) `````` MARCHE Claude committed Mar 24, 2010 7 `````` logic (> )(real, real) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 8 9 `````` logic (>=)(real, real) `````` MARCHE Claude committed Mar 24, 2010 10 `````` (* TODO : they are total order relations *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 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 `````` Jean-Christophe Filliâtre committed Mar 26, 2010 28 `````` lemma Abs_le: forall x,y:real. abs(x) <= y <-> -y <= x <= y `````` MARCHE Claude committed Mar 25, 2010 29 `````` `````` MARCHE Claude committed Mar 26, 2010 30 31 `````` lemma Abs_pos: forall x:real. abs(x) >= 0.0 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 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 committed Mar 26, 2010 67 68 69 70 71 72 73 ``````end theory FromIntTest use import FromInt lemma Test1: from_int(2) = 2.0 `````` MARCHE Claude committed Mar 26, 2010 74 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 75 76 77 78 ``````end theory Truncate `````` MARCHE Claude committed Mar 26, 2010 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)) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 131 132 133 `````` end `````` MARCHE Claude committed Mar 26, 2010 134 `````` `````` MARCHE Claude committed Mar 24, 2010 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 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 151 152 153 `````` end `````` MARCHE Claude committed Mar 29, 2010 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 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 164 165 ``````theory ExpLog `````` MARCHE Claude committed Mar 24, 2010 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 committed Mar 25, 2010 172 173 `````` logic e : real = exp(1.0) `````` MARCHE Claude committed Mar 24, 2010 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 committed Mar 25, 2010 183 `````` logic log2(x:real) : real = log(x)/log(2.0) `````` MARCHE Claude committed Mar 24, 2010 184 `````` logic log10(x:real) : real = log(x)/log(10.0) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 185 186 187 `````` end `````` MARCHE Claude committed Mar 29, 2010 188 189 190 191 192 193 194 195 196 ``````theory ExpLogTest use import ExpLog lemma Log_e : log(e) = 1.0 end `````` Jean-Christophe Filliâtre committed Mar 23, 2010 197 198 ``````theory Power `````` MARCHE Claude committed Mar 24, 2010 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 committed Mar 25, 2010 221 `````` forall x:real. x >= 0.0 -> pow(x,0.5) = sqrt(x) `````` MARCHE Claude committed Mar 24, 2010 222 223 `````` axiom Pow_exp_log: `````` Andrei Paskevich committed Mar 24, 2010 224 `````` forall x,y:real. x > 0.0 -> pow(x,y) = exp(y*log(x)) `````` MARCHE Claude committed Mar 24, 2010 225 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 226 227 ``````end `````` MARCHE Claude committed Mar 29, 2010 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 committed Mar 25, 2010 238 239 240 ``````(** Trigonometric functions [http://en.wikipedia.org/wiki/Trigonometric_function] *) `````` MARCHE Claude committed Mar 29, 2010 241 ``````theory Trigonometry `````` MARCHE Claude committed Mar 25, 2010 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 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 266 `````` `````` MARCHE Claude committed Mar 25, 2010 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 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 287 288 289 `````` end `````` MARCHE Claude committed Mar 29, 2010 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 committed Mar 25, 2010 303 304 305 ``````(** hyperbolic functions [http://en.wikipedia.org/wiki/Hyperbolic_function] *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 306 307 ``````theory Hyperbolic `````` MARCHE Claude committed Mar 25, 2010 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: `````` Jean-Christophe Filliâtre committed Mar 26, 2010 322 `````` forall x:real. -1.0 < x < 1.0 -> artanh(x) = 0.5*log((1.0+x)/(1.0-x)) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 323 324 325 `````` end `````` MARCHE Claude committed Mar 25, 2010 326 327 328 ``````(** polar coordinates: atan2, hypot [http://en.wikipedia.org/wiki/Atan2] *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 329 330 ``````theory Polar `````` MARCHE Claude committed Mar 25, 2010 331 332 `````` use import Real use import Square `````` MARCHE Claude committed Mar 29, 2010 333 `````` use import Trigonometry `````` MARCHE Claude committed Mar 25, 2010 334 335 336 `````` logic hypot(x:real,y:real) : real = sqrt(sqr(x)+sqr(y)) logic atan2(real,real) : real `````` Jean-Christophe Filliâtre committed Mar 23, 2010 337 `````` `````` MARCHE Claude committed Mar 25, 2010 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)) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 343 344 ``````end ``````