real.why 5.15 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 `````` MARCHE Claude committed Mar 25, 2010 28 29 `````` lemma Abs_le: forall x,y:real. abs(x) <= y <-> -y <= x and x <= y `````` 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 `````` lemma Test: from_int(2) = 2.0 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 69 70 71 72 73 74 75 76 ``````end theory Truncate (* TODO: truncate, floor, ceil *) end `````` MARCHE Claude committed Mar 24, 2010 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 ``````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 93 94 95 96 97 `````` end theory ExpLog `````` MARCHE Claude committed Mar 24, 2010 98 99 100 101 102 103 `````` 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 104 105 `````` logic e : real = exp(1.0) `````` MARCHE Claude committed Mar 24, 2010 106 107 108 109 110 111 112 `````` 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 `````` MARCHE Claude committed Mar 25, 2010 113 114 `````` lemma Log_e : log(e) = 1.0 `````` MARCHE Claude committed Mar 24, 2010 115 116 `````` axiom Exp_log: forall x:real. x > 0.0 -> exp(log(x)) = x `````` MARCHE Claude committed Mar 25, 2010 117 `````` logic log2(x:real) : real = log(x)/log(2.0) `````` MARCHE Claude committed Mar 24, 2010 118 `````` logic log10(x:real) : real = log(x)/log(10.0) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 119 120 121 122 123 `````` end theory Power `````` MARCHE Claude committed Mar 24, 2010 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 `````` 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 146 `````` forall x:real. x >= 0.0 -> pow(x,0.5) = sqrt(x) `````` MARCHE Claude committed Mar 24, 2010 147 148 `````` axiom Pow_exp_log: `````` Andrei Paskevich committed Mar 24, 2010 149 `````` forall x,y:real. x > 0.0 -> pow(x,y) = exp(y*log(x)) `````` MARCHE Claude committed Mar 24, 2010 150 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 151 152 ``````end `````` MARCHE Claude committed Mar 25, 2010 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 ``````(** Trigonometric functions [http://en.wikipedia.org/wiki/Trigonometric_function] *) theory Trigonometric 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 181 `````` `````` MARCHE Claude committed Mar 25, 2010 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 `````` 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 202 203 204 `````` end `````` MARCHE Claude committed Mar 25, 2010 205 206 207 ``````(** hyperbolic functions [http://en.wikipedia.org/wiki/Hyperbolic_function] *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 208 209 ``````theory Hyperbolic `````` MARCHE Claude committed Mar 25, 2010 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 `````` 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: forall x:real. -1.0 < x and x < 1.0 -> artanh(x) = 0.5*log((1.0+x)/(1.0-x)) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 225 226 227 `````` end `````` MARCHE Claude committed Mar 25, 2010 228 229 230 ``````(** polar coordinates: atan2, hypot [http://en.wikipedia.org/wiki/Atan2] *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 231 232 ``````theory Polar `````` MARCHE Claude committed Mar 25, 2010 233 234 `````` use import Real use import Square `````` MARCHE Claude committed Mar 25, 2010 235 `````` use import Trigonometric `````` MARCHE Claude committed Mar 25, 2010 236 237 238 `````` 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 239 `````` `````` MARCHE Claude committed Mar 25, 2010 240 241 242 243 244 `````` 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 245 246 ``````end ``````