real.mlw 9.66 KB
 Jean-Christophe Filliâtre committed Mar 23, 2010 1 `````` `````` Guillaume Melquiond committed Jul 18, 2012 2 ``````(** {1 Theory of reals} `````` MARCHE Claude committed Apr 19, 2012 3 `````` `````` 4 5 ``````This file provides the basic theory of real numbers, and several additional theories for classical real functions. `````` MARCHE Claude committed Apr 19, 2012 6 7 8 9 `````` *) (** {2 Real numbers and the basic unary and binary operators} *) `````` 10 `````` `````` Andrei Paskevich committed Dec 22, 2017 11 ``````module Real `````` MARCHE Claude committed Mar 26, 2010 12 `````` `````` Jean-Christophe Filliatre committed Feb 06, 2012 13 14 `````` constant zero : real = 0.0 constant one : real = 1.0 `````` MARCHE Claude committed Oct 19, 2010 15 `````` `````` MARCHE Claude committed Mar 07, 2016 16 17 18 19 20 21 22 23 24 25 26 `````` val (=) (x y : real) : bool ensures { result <-> x = y } val function (-_) real : real val function (+) real real : real val function (*) real real : real val predicate (<) real real : bool let (-) (x y : real) = x + -y let predicate (>) (x y : real) = y < x let predicate (<=) (x y : real) = x < y || x = y let predicate (>=) (x y : real) = y <= x `````` MARCHE Claude committed Oct 19, 2010 27 `````` `````` Andrei Paskevich committed Jun 29, 2011 28 `````` clone export algebra.OrderedField with type t = real, `````` MARCHE Claude committed Mar 07, 2016 29 30 `````` constant zero = zero, constant one = one, function (-_) = (-_), function (+) = (+), `````` Andrei Paskevich committed Jun 14, 2018 31 `````` function (*) = (*), predicate (<=) = (<=) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 32 `````` `````` MARCHE Claude committed Mar 07, 2016 33 34 35 36 `````` val (/) (x y:real) : real requires { y <> 0.0 } ensures { result = x / y } `````` MARCHE Claude committed Apr 19, 2012 37 ``````(*** `````` MARCHE Claude committed Sep 04, 2011 38 `````` lemma sub_zero: forall x y:real. x - y = 0.0 -> x = y `````` MARCHE Claude committed Sep 05, 2011 39 ``````*) `````` MARCHE Claude committed Sep 04, 2011 40 `````` `````` MARCHE Claude committed Oct 19, 2010 41 42 ``````end `````` 43 ``````(** {2 Alternative Infix Operators} `````` MARCHE Claude committed Apr 19, 2012 44 `````` `````` 45 46 ``````This theory should be used instead of Real when one wants to use both integer and real binary operators. `````` MARCHE Claude committed Apr 19, 2012 47 48 49 `````` *) `````` Andrei Paskevich committed Dec 22, 2017 50 ``````module RealInfix `````` MARCHE Claude committed Oct 19, 2010 51 `````` `````` Andrei Paskevich committed Jun 15, 2018 52 `````` use Real `````` MARCHE Claude committed Oct 19, 2010 53 `````` `````` MARCHE Claude committed Mar 07, 2016 54 55 56 `````` let function (+.) (x:real) (y:real) : real = x + y let function (-.) (x:real) (y:real) : real = x - y let function ( *.) (x:real) (y:real) : real = x * y `````` Andrei Paskevich committed Jun 29, 2011 57 `````` function (/.) (x:real) (y:real) : real = x / y `````` MARCHE Claude committed Mar 07, 2016 58 `````` let function (-._) (x:real) : real = - x `````` MARCHE Claude committed Mar 21, 2012 59 `````` function inv (x:real) : real = Real.inv x `````` MARCHE Claude committed Oct 19, 2010 60 `````` `````` MARCHE Claude committed Mar 07, 2016 61 62 63 64 `````` let predicate (<=.) (x:real) (y:real) = x <= y let predicate (>=.) (x:real) (y:real) = x >= y let predicate ( <.) (x:real) (y:real) = x < y let predicate ( >.) (x:real) (y:real) = x > y `````` MARCHE Claude committed Oct 19, 2010 65 `````` `````` MARCHE Claude committed Mar 07, 2016 66 67 68 `````` val (/.) (x y:real) : real requires { y <> 0.0 } ensures { result = x /. y } `````` MARCHE Claude committed Oct 19, 2010 69 70 `````` end `````` Jean-Christophe Filliâtre committed Mar 23, 2010 71 `````` `````` MARCHE Claude committed Apr 19, 2012 72 73 ``````(** {2 Absolute Value} *) `````` Andrei Paskevich committed Dec 22, 2017 74 ``````module Abs `````` Jean-Christophe Filliâtre committed Mar 23, 2010 75 `````` `````` Andrei Paskevich committed Jun 15, 2018 76 `````` use Real `````` Jean-Christophe Filliâtre committed Mar 23, 2010 77 `````` `````` Andrei Paskevich committed Jun 29, 2011 78 `````` function abs(x : real) : real = if x >= 0.0 then x else -x `````` Jean-Christophe Filliâtre committed Mar 23, 2010 79 `````` `````` Andrei Paskevich committed Jun 21, 2010 80 `````` lemma Abs_le: forall x y:real. abs x <= y <-> -y <= x <= y `````` MARCHE Claude committed Mar 25, 2010 81 `````` `````` Andrei Paskevich committed Jun 21, 2010 82 `````` lemma Abs_pos: forall x:real. abs x >= 0.0 `````` MARCHE Claude committed Mar 26, 2010 83 `````` `````` MARCHE Claude committed Apr 19, 2012 84 ``````(*** `````` MARCHE Claude committed Sep 04, 2011 85 `````` lemma Abs_zero: forall x:real. abs x = 0.0 -> x = 0.0 `````` MARCHE Claude committed Sep 05, 2011 86 ``````*) `````` MARCHE Claude committed Sep 04, 2011 87 `````` `````` MARCHE Claude committed Nov 30, 2011 88 89 90 91 92 93 94 `````` 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) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 95 96 ``````end `````` MARCHE Claude committed Apr 19, 2012 97 98 ``````(** {2 Minimum and Maximum} *) `````` Andrei Paskevich committed Dec 22, 2017 99 ``````module MinMax `````` Jean-Christophe Filliâtre committed Mar 23, 2010 100 `````` `````` Andrei Paskevich committed Jun 15, 2018 101 `````` use Real `````` Andrei Paskevich committed Jun 15, 2018 102 `````` clone export relations.MinMax with type t = real, predicate le = (<=), goal . `````` Jean-Christophe Filliâtre committed Mar 23, 2010 103 104 105 `````` end `````` MARCHE Claude committed Apr 19, 2012 106 107 ``````(** {2 Injection of integers into reals} *) `````` Andrei Paskevich committed Dec 22, 2017 108 ``````module FromInt `````` Jean-Christophe Filliâtre committed Mar 23, 2010 109 `````` `````` Andrei Paskevich committed Jun 15, 2018 110 `````` use int.Int as Int `````` Andrei Paskevich committed Jun 15, 2018 111 `````` use Real `````` Jean-Christophe Filliâtre committed Mar 23, 2010 112 `````` `````` Andrei Paskevich committed Jun 29, 2011 113 `````` function from_int int : real `````` Jean-Christophe Filliâtre committed Mar 23, 2010 114 `````` `````` Andrei Paskevich committed Jun 21, 2010 115 116 `````` axiom Zero: from_int 0 = 0.0 axiom One: from_int 1 = 1.0 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 117 `````` `````` MARCHE Claude committed Oct 19, 2010 118 `````` axiom Add: `````` Andrei Paskevich committed Jun 21, 2010 119 `````` forall x y:int. from_int (Int.(+) x y) = from_int x + from_int y `````` MARCHE Claude committed Oct 19, 2010 120 `````` axiom Sub: `````` Andrei Paskevich committed Jun 21, 2010 121 `````` forall x y:int. from_int (Int.(-) x y) = from_int x - from_int y `````` MARCHE Claude committed Oct 19, 2010 122 `````` axiom Mul: `````` Andrei Paskevich committed Jun 21, 2010 123 `````` forall x y:int. from_int (Int.(*) x y) = from_int x * from_int y `````` MARCHE Claude committed Oct 19, 2010 124 `````` axiom Neg: `````` MARCHE Claude committed Sep 03, 2012 125 `````` forall x:int. from_int (Int.(-_) (x)) = - from_int x `````` Jean-Christophe Filliâtre committed Mar 23, 2010 126 `````` `````` Raphael Rieu-Helft committed Feb 14, 2018 127 `````` lemma Injective: `````` Raphael Rieu-Helft committed Dec 22, 2017 128 `````` forall x y: int. from_int x = from_int y -> x = y `````` Clément Fumex committed Oct 19, 2016 129 130 131 `````` axiom Monotonic: forall x y:int. Int.(<=) x y -> from_int x <= from_int y `````` MARCHE Claude committed Mar 26, 2010 132 133 ``````end `````` MARCHE Claude committed Apr 19, 2012 134 135 ``````(** {2 Various truncation functions} *) `````` Andrei Paskevich committed Dec 22, 2017 136 ``````module Truncate `````` Jean-Christophe Filliâtre committed Mar 23, 2010 137 `````` `````` Andrei Paskevich committed Jun 15, 2018 138 139 `````` use Real use FromInt `````` MARCHE Claude committed Mar 26, 2010 140 `````` `````` MARCHE Claude committed Apr 19, 2012 141 `````` (** truncate: rounds towards zero *) `````` MARCHE Claude committed Mar 26, 2010 142 `````` `````` Andrei Paskevich committed Jun 29, 2011 143 `````` function truncate real : int `````` MARCHE Claude committed Mar 26, 2010 144 145 `````` axiom Truncate_int : `````` Andrei Paskevich committed Jun 21, 2010 146 `````` forall i:int. truncate (from_int i) = i `````` MARCHE Claude committed Mar 26, 2010 147 148 `````` axiom Truncate_down_pos: `````` MARCHE Claude committed Oct 19, 2010 149 `````` forall x:real. x >= 0.0 -> `````` Andrei Paskevich committed Jun 21, 2010 150 `````` from_int (truncate x) <= x < from_int (Int.(+) (truncate x) 1) `````` MARCHE Claude committed Mar 26, 2010 151 152 `````` axiom Truncate_up_neg: `````` MARCHE Claude committed Oct 19, 2010 153 `````` forall x:real. x <= 0.0 -> `````` Andrei Paskevich committed Jun 21, 2010 154 `````` from_int (Int.(-) (truncate x) 1) < x <= from_int (truncate x) `````` MARCHE Claude committed Mar 26, 2010 155 156 `````` axiom Real_of_truncate: `````` Andrei Paskevich committed Jun 21, 2010 157 `````` forall x:real. x - 1.0 <= from_int (truncate x) <= x + 1.0 `````` MARCHE Claude committed Mar 26, 2010 158 159 `````` axiom Truncate_monotonic: `````` Andrei Paskevich committed Jun 21, 2010 160 `````` forall x y:real. x <= y -> Int.(<=) (truncate x) (truncate y) `````` MARCHE Claude committed Mar 26, 2010 161 162 `````` axiom Truncate_monotonic_int1: `````` Andrei Paskevich committed Jun 21, 2010 163 `````` forall x:real, i:int. x <= from_int i -> Int.(<=) (truncate x) i `````` MARCHE Claude committed Mar 26, 2010 164 165 `````` axiom Truncate_monotonic_int2: `````` Andrei Paskevich committed Jun 21, 2010 166 `````` forall x:real, i:int. from_int i <= x -> Int.(<=) i (truncate x) `````` MARCHE Claude committed Mar 26, 2010 167 `````` `````` MARCHE Claude committed Apr 19, 2012 168 `````` (** roundings up and down *) `````` MARCHE Claude committed Mar 26, 2010 169 `````` `````` Andrei Paskevich committed Jun 29, 2011 170 171 `````` function floor real : int function ceil real : int `````` MARCHE Claude committed Mar 26, 2010 172 173 `````` axiom Floor_int : `````` Andrei Paskevich committed Jun 21, 2010 174 `````` forall i:int. floor (from_int i) = i `````` MARCHE Claude committed Mar 26, 2010 175 176 `````` axiom Ceil_int : `````` Guillaume Melquiond committed Nov 29, 2011 177 `````` forall i:int. ceil (from_int i) = i `````` MARCHE Claude committed Mar 26, 2010 178 179 `````` axiom Floor_down: `````` Andrei Paskevich committed Jun 21, 2010 180 `````` forall x:real. from_int (floor x) <= x < from_int (Int.(+) (floor x) 1) `````` MARCHE Claude committed Mar 26, 2010 181 182 `````` axiom Ceil_up: `````` Andrei Paskevich committed Jun 21, 2010 183 `````` forall x:real. from_int (Int.(-) (ceil x) 1) < x <= from_int (ceil x) `````` MARCHE Claude committed Mar 26, 2010 184 185 `````` axiom Floor_monotonic: `````` Andrei Paskevich committed Jun 21, 2010 186 `````` forall x y:real. x <= y -> Int.(<=) (floor x) (floor y) `````` MARCHE Claude committed Mar 26, 2010 187 188 `````` axiom Ceil_monotonic: `````` Andrei Paskevich committed Jun 21, 2010 189 `````` forall x y:real. x <= y -> Int.(<=) (ceil x) (ceil y) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 190 191 192 `````` end `````` MARCHE Claude committed Apr 19, 2012 193 ``````(** {2 Square and Square Root} *) `````` MARCHE Claude committed Mar 26, 2010 194 `````` `````` Andrei Paskevich committed Dec 22, 2017 195 ``````module Square `````` MARCHE Claude committed Mar 24, 2010 196 `````` `````` Andrei Paskevich committed Jun 15, 2018 197 `````` use Real `````` MARCHE Claude committed Mar 24, 2010 198 `````` `````` Andrei Paskevich committed Jun 29, 2011 199 `````` function sqr (x : real) : real = x * x `````` MARCHE Claude committed Mar 24, 2010 200 `````` `````` Andrei Paskevich committed Jun 29, 2011 201 `````` function sqrt real : real `````` MARCHE Claude committed Mar 24, 2010 202 `````` `````` MARCHE Claude committed Oct 19, 2010 203 `````` axiom Sqrt_positive: `````` Andrei Paskevich committed Jun 21, 2010 204 `````` forall x:real. x >= 0.0 -> sqrt x >= 0.0 `````` MARCHE Claude committed Mar 24, 2010 205 `````` `````` MARCHE Claude committed Oct 19, 2010 206 `````` axiom Sqrt_square: `````` Andrei Paskevich committed Jun 21, 2010 207 `````` forall x:real. x >= 0.0 -> sqr (sqrt x) = x `````` MARCHE Claude committed Mar 24, 2010 208 `````` `````` MARCHE Claude committed Oct 19, 2010 209 `````` axiom Square_sqrt: `````` Andrei Paskevich committed Jun 21, 2010 210 `````` forall x:real. x >= 0.0 -> sqrt (x*x) = x `````` Jean-Christophe Filliâtre committed Mar 23, 2010 211 `````` `````` MARCHE Claude committed May 18, 2012 212 213 214 215 216 217 218 `````` 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 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 219 220 ``````end `````` MARCHE Claude committed Apr 19, 2012 221 222 ``````(** {2 Exponential and Logarithm} *) `````` Andrei Paskevich committed Dec 22, 2017 223 ``````module ExpLog `````` Jean-Christophe Filliâtre committed Mar 23, 2010 224 `````` `````` Andrei Paskevich committed Jun 15, 2018 225 `````` use Real `````` MARCHE Claude committed Mar 24, 2010 226 `````` `````` Andrei Paskevich committed Jun 29, 2011 227 `````` function exp real : real `````` MARCHE Claude committed Mar 24, 2010 228 `````` axiom Exp_zero : exp(0.0) = 1.0 `````` Andrei Paskevich committed Jun 21, 2010 229 `````` axiom Exp_sum : forall x y:real. exp (x+y) = exp x * exp y `````` MARCHE Claude committed Mar 24, 2010 230 `````` `````` Jean-Christophe Filliatre committed Feb 06, 2012 231 `````` constant e : real = exp 1.0 `````` MARCHE Claude committed Mar 25, 2010 232 `````` `````` Andrei Paskevich committed Jun 29, 2011 233 `````` function log real : real `````` Andrei Paskevich committed Jun 21, 2010 234 `````` axiom Log_one : log 1.0 = 0.0 `````` MARCHE Claude committed Oct 19, 2010 235 `````` axiom Log_mul : `````` Andrei Paskevich committed Jun 29, 2011 236 `````` forall x y:real. x > 0.0 /\ y > 0.0 -> log (x*y) = log x + log y `````` MARCHE Claude committed Mar 24, 2010 237 `````` `````` Andrei Paskevich committed Jun 21, 2010 238 `````` axiom Log_exp: forall x:real. log (exp x) = x `````` MARCHE Claude committed Mar 24, 2010 239 `````` `````` Andrei Paskevich committed Jun 21, 2010 240 `````` axiom Exp_log: forall x:real. x > 0.0 -> exp (log x) = x `````` MARCHE Claude committed Mar 24, 2010 241 `````` `````` Andrei Paskevich committed Jun 29, 2011 242 243 `````` function log2 (x : real) : real = log x / log 2.0 function log10 (x : real) : real = log x / log 10.0 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 244 245 246 `````` end `````` MARCHE Claude committed Apr 19, 2012 247 ``````(** {2 Power of a real to an integer} *) `````` 248 `````` `````` Andrei Paskevich committed Dec 22, 2017 249 ``````module PowerInt `````` MARCHE Claude committed Mar 21, 2012 250 `````` `````` Andrei Paskevich committed Jun 15, 2018 251 252 `````` use int.Int use RealInfix `````` MARCHE Claude committed Mar 21, 2012 253 254 `````` clone export int.Exponentiation with `````` Guillaume Melquiond committed Sep 03, 2012 255 `````` type t = real, constant one = Real.one, function (*) = Real.(*), `````` Andrei Paskevich committed Jun 14, 2018 256 `````` goal Assoc, goal Unit_def_l, goal Unit_def_r, axiom Power_0, axiom Power_s `````` MARCHE Claude committed Mar 21, 2012 257 `````` `````` MARCHE Claude committed Sep 11, 2012 258 `````` lemma Pow_ge_one: `````` Andrei Paskevich committed Oct 20, 2012 259 `````` forall x:real, n:int. 0 <= n /\ 1.0 <=. x -> 1.0 <=. power x n `````` MARCHE Claude committed Sep 11, 2012 260 `````` `````` MARCHE Claude committed Mar 21, 2012 261 262 ``````end `````` MARCHE Claude committed Apr 19, 2012 263 ``````(** {2 Power of a real to a real exponent} *) `````` 264 `````` `````` Andrei Paskevich committed Dec 22, 2017 265 ``````module PowerReal `````` Jean-Christophe Filliâtre committed Mar 23, 2010 266 `````` `````` Andrei Paskevich committed Jun 15, 2018 267 268 `````` use Real use ExpLog `````` MARCHE Claude committed Mar 24, 2010 269 `````` `````` Andrei Paskevich committed Jun 29, 2011 270 `````` function pow real real : real `````` MARCHE Claude committed Mar 24, 2010 271 `````` `````` 272 273 274 275 276 277 278 279 `````` 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 committed Mar 24, 2010 280 `````` `````` 281 282 `````` lemma Pow_mult : forall x y z. x > 0.0 -> pow (pow x y) z = pow x (y * z) `````` MARCHE Claude committed Mar 24, 2010 283 `````` `````` 284 285 `````` lemma Pow_x_zero: forall x:real. x > 0.0 -> pow x 0.0 = 1.0 `````` MARCHE Claude committed Mar 24, 2010 286 `````` `````` 287 288 289 290 `````` lemma Pow_x_one: forall x:real. x > 0.0 -> pow x 1.0 = x lemma Pow_one_y: `````` Andrei Paskevich committed Jun 21, 2010 291 `````` forall y:real. pow 1.0 y = 1.0 `````` MARCHE Claude committed Mar 24, 2010 292 `````` `````` Andrei Paskevich committed Jun 15, 2018 293 `````` use Square `````` MARCHE Claude committed Mar 24, 2010 294 `````` `````` 295 296 `````` lemma Pow_x_two: forall x:real. x > 0.0 -> pow x 2.0 = sqr x `````` MARCHE Claude committed Mar 24, 2010 297 `````` `````` 298 299 `````` lemma Pow_half: forall x:real. x > 0.0 -> pow x 0.5 = sqrt x `````` MARCHE Claude committed Mar 24, 2010 300 `````` `````` Andrei Paskevich committed Jun 15, 2018 301 302 `````` use FromInt use int.Power `````` Raphael Rieu-Helft committed Jan 08, 2018 303 `````` `````` Raphael Rieu-Helft committed Jan 16, 2018 304 `````` lemma pow_from_int: forall x y: int. Int.(<) 0 x -> Int.(<=) 0 y -> `````` Raphael Rieu-Helft committed Jan 08, 2018 305 306 307 `````` pow (from_int x) (from_int y) = from_int (power x y) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 308 309 ``````end `````` MARCHE Claude committed Apr 19, 2012 310 ``````(** {2 Trigonometric Functions} `````` MARCHE Claude committed Apr 19, 2012 311 `````` `````` 312 313 ``````See the {h wikipedia page}. `````` MARCHE Claude committed Mar 25, 2010 314 ``````*) `````` 315 `````` `````` Andrei Paskevich committed Dec 22, 2017 316 ``````module Trigonometry `````` MARCHE Claude committed Mar 25, 2010 317 `````` `````` Andrei Paskevich committed Jun 15, 2018 318 319 320 `````` use Real use Square use Abs `````` MARCHE Claude committed Mar 25, 2010 321 `````` `````` Andrei Paskevich committed Jun 29, 2011 322 323 `````` function cos real : real function sin real : real `````` MARCHE Claude committed Mar 25, 2010 324 325 `````` axiom Pythagorean_identity: `````` Andrei Paskevich committed Jun 21, 2010 326 `````` forall x:real. sqr (cos x) + sqr (sin x) = 1.0 `````` MARCHE Claude committed Mar 25, 2010 327 `````` `````` Andrei Paskevich committed Jun 21, 2010 328 329 `````` 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 committed Mar 25, 2010 330 `````` `````` Andrei Paskevich committed Jun 21, 2010 331 332 `````` axiom Cos_0: cos 0.0 = 1.0 axiom Sin_0: sin 0.0 = 0.0 `````` MARCHE Claude committed Mar 25, 2010 333 `````` `````` Jean-Christophe Filliatre committed Feb 06, 2012 334 `````` constant pi : real `````` MARCHE Claude committed Mar 25, 2010 335 `````` `````` MARCHE Claude committed Oct 16, 2015 336 337 338 `````` axiom Pi_double_precision_bounds: 0x1.921fb54442d18p+1 < pi < 0x1.921fb54442d19p+1 (* `````` MARCHE Claude committed Apr 08, 2010 339 340 341 342 `````` axiom Pi_interval: 3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 < pi < 3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197 `````` MARCHE Claude committed Oct 16, 2015 343 ``````*) `````` MARCHE Claude committed Apr 08, 2010 344 `````` `````` Andrei Paskevich committed Jun 21, 2010 345 346 `````` axiom Cos_pi: cos pi = -1.0 axiom Sin_pi: sin pi = 0.0 `````` MARCHE Claude committed Mar 25, 2010 347 `````` `````` Andrei Paskevich committed Jun 21, 2010 348 349 `````` 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 350 `````` `````` Andrei Paskevich committed Jun 21, 2010 351 352 `````` 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 committed Mar 25, 2010 353 `````` `````` Andrei Paskevich committed Jun 21, 2010 354 355 `````` 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 committed Mar 25, 2010 356 357 `````` axiom Cos_neg: `````` Andrei Paskevich committed Jun 21, 2010 358 `````` forall x:real. cos (-x) = cos x `````` MARCHE Claude committed Mar 25, 2010 359 `````` axiom Sin_neg: `````` Andrei Paskevich committed Jun 21, 2010 360 `````` forall x:real. sin (-x) = - sin x `````` MARCHE Claude committed Oct 19, 2010 361 `````` `````` MARCHE Claude committed Mar 25, 2010 362 `````` axiom Cos_sum: `````` Andrei Paskevich committed Jun 21, 2010 363 `````` forall x y:real. cos (x+y) = cos x * cos y - sin x * sin y `````` MARCHE Claude committed Mar 25, 2010 364 `````` axiom Sin_sum: `````` Andrei Paskevich committed Jun 21, 2010 365 `````` forall x y:real. sin (x+y) = sin x * cos y + cos x * sin y `````` MARCHE Claude committed Mar 25, 2010 366 `````` `````` Andrei Paskevich committed Jun 29, 2011 367 368 `````` function tan (x : real) : real = sin x / cos x function atan real : real `````` MARCHE Claude committed Mar 25, 2010 369 `````` axiom Tan_atan: `````` Andrei Paskevich committed Jun 21, 2010 370 `````` forall x:real. tan (atan x) = x `````` Jean-Christophe Filliâtre committed Mar 23, 2010 371 372 373 `````` end `````` MARCHE Claude committed Apr 19, 2012 374 ``````(** {2 Hyperbolic Functions} `````` 375 376 377 `````` See the {h wikipedia page}. `````` MARCHE Claude committed Mar 25, 2010 378 ``````*) `````` 379 `````` `````` Andrei Paskevich committed Dec 22, 2017 380 ``````module Hyperbolic `````` Jean-Christophe Filliâtre committed Mar 23, 2010 381 `````` `````` Andrei Paskevich committed Jun 15, 2018 382 383 384 `````` use Real use Square use ExpLog `````` MARCHE Claude committed Mar 25, 2010 385 `````` `````` Andrei Paskevich committed Jun 29, 2011 386 387 388 `````` 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 committed Mar 25, 2010 389 `````` `````` Andrei Paskevich committed Jun 29, 2011 390 391 `````` function asinh (x : real) : real = log (x + sqrt (sqr x + 1.0)) function acosh (x : real) : real `````` MARCHE Claude committed Dec 15, 2010 392 393 `````` axiom Acosh_def: forall x:real. x >= 1.0 -> acosh x = log (x + sqrt (sqr x - 1.0)) `````` Andrei Paskevich committed Jun 29, 2011 394 `````` function atanh (x : real) : real `````` MARCHE Claude committed Dec 15, 2010 395 396 `````` axiom Atanh_def: forall x:real. -1.0 < x < 1.0 -> atanh x = 0.5 * log ((1.0+x)/(1.0-x)) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 397 398 399 `````` end `````` MARCHE Claude committed Apr 19, 2012 400 ``````(** {2 Polar Coordinates} `````` 401 402 403 `````` See the {h wikipedia page}. `````` MARCHE Claude committed Mar 25, 2010 404 ``````*) `````` 405 `````` `````` Andrei Paskevich committed Dec 22, 2017 406 ``````module Polar `````` Jean-Christophe Filliâtre committed Mar 23, 2010 407 `````` `````` Andrei Paskevich committed Jun 15, 2018 408 409 410 `````` use Real use Square use Trigonometry `````` MARCHE Claude committed Mar 25, 2010 411 `````` `````` Andrei Paskevich committed Jun 29, 2011 412 413 `````` function hypot (x y : real) : real = sqrt (sqr x + sqr y) function atan2 real real : real `````` MARCHE Claude committed Oct 19, 2010 414 `````` `````` MARCHE Claude committed Mar 25, 2010 415 `````` axiom X_from_polar: `````` Andrei Paskevich committed Jun 21, 2010 416 `````` forall x y:real. x = hypot x y * cos (atan2 y x) `````` MARCHE Claude committed Mar 25, 2010 417 418 `````` axiom Y_from_polar: `````` Andrei Paskevich committed Jun 21, 2010 419 `````` forall x y:real. y = hypot x y * sin (atan2 y x) `````` 420 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 421 ``end``