share/fourier_elim/rtest_fourier_elim.mac

   1 /* Let's place the known bugs at the end. */
   2
   3 (kill(all), reset(), load("fourier_elim"), 0);
   4 0$
   5
   6 fourier_elim([max(x,0) > 0],[x]);
   7 [0 < x]$
   8
   9 fourier_elim([max(x,0) >= 0],[x]);
  10 universalset$
  11
  12 fourier_elim([min(x,0) >= 0],[x]);
  13 [x=0] or [0 < x]$
  14
  15 fourier_elim([abs(x) <= 1],[x]);
  16 [x=1] or [x=-1] or [-1<x,x<1]$
  17
  18 fourier_elim([0 < 1],[]);
  19 universalset$
  20
  21 fourier_elim([0 < 1],[x]);
  22 universalset$
  23
  24 fourier_elim([0 >= 1],[]);
  25 emptyset$
  26
  27 fourier_elim([0 > 1],[x]);
  28 emptyset$
  29
  30 fourier_elim([abs(x) < 1],[x]);
  31 [-1 < x, x < 1]$
  32
  33 fourier_elim([],[]);
  34 universalset$
  35
  36 fourier_elim([x # inf],[x]);
  37 universalset$
  38
  39 fourier_elim([-x # inf],[x]);
  40 universalset$
  41
  42 fourier_elim([x # minf],[x,y]);
  43 universalset$
  44
  45 fourier_elim([-x # minf],[x,y]);
  46 universalset$
  47
  48 fourier_elim([x # %i],[x,y,z]);
  49 universalset$
  50
  51 fourier_elim([-x # %i],[x]);
  52 universalset$
  53
  54 fourier_elim([x # 0],[x]);
  55 [x < 0] or [0 < x]$
  56
  57 fourier_elim([-x # 0],[x]);
  58 [0 < x] or [x < 0]$
  59
  60 fourier_elim([x # 10],[x]);
  61 [x < 10] or [10 < x]$
  62
  63 fourier_elim([-x # 10],[x]);
  64 [-10 < x] or [x < -10]$
  65
  66 fourier_elim([x^2 # 100],[x]);
  67 [-10 < x,x < 10] or [10 < x] or [x < -10]$
  68
  69 fourier_elim([-x^2 # 100],[x]);
  70 universalset$
  71
  72 fourier_elim([x = 5, x <= 5],[x]);
  73 [x=5]$
  74
  75 fourier_elim([x = 5, x >= 5],[x]);
  76 [x=5]$
  77
  78 fourier_elim([x = 5, x < 5],[x]);
  79 emptyset$
  80
  81 fourier_elim([x = 5],[x]);
  82 [x = 5]$
  83
  84 fourier_elim([x = 5, x = 6],[x]);
  85 emptyset$
  86
  87 fourier_elim([x = 5, x < 6],[x]);
  88 [x = 5]$
  89
  90 fourier_elim([x = 5, x > 6],[x]);
  91 emptyset$
  92
  93 fourier_elim([x = 5, x >= 5],[x]);
  94 [x = 5]$
  95
  96 fourier_elim([x = 5, x >= 0],[x]);
  97 [x = 5]$
  98
  99 fourier_elim([x = y, y = 7],[x,y]);
 100 [x=7, y=7]$
 101
 102 fourier_elim([x = 2*y + 1, y = 7],[x,y]);
 103 [x=15, y=7]$
 104
 105 fourier_elim([x + y = 2, x - y = 0],[x,y]);
 106 [x=1, y=1]$
 107
 108 fourier_elim([x + y = 2, x - y = 0],[]);
 109 [y-x=0,y+x-2=0]$
 110
 111 (eqs : [0 < x, x < 1, 0 < y, y < 1, 0 < z, x+y+z < 4],0);
 112 0$
 113
 114 fourier_elim(eqs,[z,y,x]);
 115 [0<z,z<-y-x+4,0<y,y<1,0<x,x<1]$
 116
 117 fourier_elim(eqs,[x,y,z]);
 118 [0<x,x<min(1,-z-y+4),0<y,y<min(1,4-z),0<z,z<4]$
 119
 120 fourier_elim(fourier_elim(eqs,[y,x,z]),[z,y,x]);
 121 [0<z,z<-y-x+4,0<y,y<1,0<x,x<1]$
 122
 123 (remvalue(eqs),0);
 124 0$
 125
 126 fourier_elim([x^2 > 0],[x]);
 127 [x < 0] or [0 < x]$
 128
 129 fourier_elim([x^3 > 0],[x]);
 130 [0 < x]$
 131
 132 fourier_elim([x^4 > 0],[x]);
 133 [x < 0] or [0 < x]$
 134
 135 fourier_elim([x^2 >= 0],[x]);
 136 'universalset$
 137
 138 fourier_elim([x^2 <= 0],[x]);
 139 [x = 0]$
 140
 141 fourier_elim([x^2 + 1 < 0], [x]);
 142 'emptyset$
 143
 144 fourier_elim([x^2 + 1 > 0], [x]);
 145 'universalset$
 146
 147 fourier_elim([x^2 + 1 >= 0], [x]);
 148 'universalset$
 149
 150 fourier_elim([x^2 + 1 # 0], [x]);
 151 'universalset$
 152
 153 fourier_elim([2^x < 2^y], [x, y]);
 154 [x < y]$
 155
 156 fourier_elim([1.5^x > 1.5^y], [x, y]);
 157 [y < x]$
 158
 159 fourier_elim([a * b > 0],[a,b]);
 160 [0<a,0<b] or [a<0,b<0]$
 161
 162 fourier_elim([x >= x],[x]);
 163 'universalset$
 164
 165 fourier_elim([1 >= 1/10],[]);
 166 'universalset$
 167
 168 fourier_elim([x^2 # 100],[x]);
 169 [-10 < x,x < 10] or [10 < x] or [x < -10]$
 170
 171 fourier_elim([x # inf, x # minf],[]);
 172 'universalset$
 173
 174 fourier_elim([x # inf],[]);
 175 'universalset$
 176
 177 fourier_elim([x # %i],[]);
 178 'universalset$
 179
 180 fourier_elim([1-x > 0, x - %e > 0],[x]);
 181 'emptyset$
 182
 183 fourier_elim([-1/a > 0],[a]);
 184 [a < 0]$
 185
 186 fourier_elim([x # infinity],[x]);
 187 'universalset$
 188
 189 fourier_elim([x^2-1 < 0],[x]);
 190 [-1 < x, x < 1]$
 191
 192 fourier_elim([(x^2+1) < 0],[x]);
 193 'emptyset$
 194
 195 fourier_elim([x^2 < 0],[x]);
 196 'emptyset$
 197
 198 fourier_elim([x^2+1 = 0],[x]);
 199 'emptyset$
 200
 201 fourier_elim([x /(1 + x^2) <  1],[x]);
 202 [x^2-x+1>0]$
 203
 204 fourier_elim([x*(1-x) > 0, (x-12) * (1/2-x) > 0],[x]);
 205 [1/2 < x,x < 1]$
 206
 207 fourier_elim([(x-12) * (1/2-x) > 0],[x]);
 208 [1/2 < x, x < 12]$
 209
 210 fourier_elim([y >= 0, y <= 0],[y]);
 211 [y = 0]$
 212
 213 fourier_elim([(x-5) / (x-7) <= 10],[x]);
 214 [x = 65/9] or [65/9 < x] or [x < 7]$
 215
 216 fourier_elim([x*(1-x) < 0, (x-6)*(10-x) < 0],[x]);
 217 [10 < x] or [1 < x,x < 6] or [x < 0]$
 218
 219 fourier_elim([x*y*z < 0],[x,y,z]);
 220 [x<0,0<y,0<z] or [0<x,y<0,0<z] or [0<x,0<y,z<0] or [x<0,y<0,z<0]$
 221
 222 fourier_elim([1 = 1],[]);
 223 'universalset$
 224
 225 fourier_elim([1 = 1, x + y < 1, x - y > 1],[x,y]);
 226 [y+1<x,x<1-y,y<0]$
 227
 228 fourier_elim([1 = -1, x + y < 1, x - y > 1],[x,y]);
 229 emptyset$
 230
 231 fourier_elim([1 = 0],[]);
 232 'emptyset$
 233
 234 fourier_elim([inf = 0],[]);
 235 'emptyset$
 236
 237 fourier_elim([inf = minf],[]);
 238 'emptyset$
 239
 240 fourier_elim([sqrt(2) = sqrt(5)],[]);
 241 'emptyset$
 242
 243 fourier_elim([sqrt(2) # sqrt(5)],[]);
 244 'universalset$
 245
 246 fourier_elim([max(x,y) < 1, min(x,y) > -1],[x,y]);
 247 [-1<x,x<1,-1<y,y<1]$
 248
 249
 250 fourier_elim([min(x,0) > 0],[x]);
 251 'emptyset$
 252
 253 fourier_elim([x[1] + x[2] < 1, x[1] - x[2] > -1], [x[1], x[2]]);
 254 [x[2]-1<x[1],x[1]<1-x[2],x[2]<1]$
 255
 256 fourier_elim([rat(x+y) < 1, x - y > -1],[x, rat(y)]);
 257 [y-1<x,x<1-y,y<1]$
 258
 259 fourier_elim([rat(x*(1-x)) < 0, rat((x-6)*(10-x)) < 0],[x]);
 260 [10 < x] or [1 < x,x < 6] or [x < 0]$
 261
 262 fourier_elim([x * (x+1) * (x+2) < 0],[y,x]);
 263 [-1 < x,x < 0] or [x < -2]$
 264
 265 fourier_elim([x * (x+1) * (x+2) < 0, x > -2],[y,x]);
 266 [-1 < x,x < 0]$
 267
 268 fourier_elim([x * (x+1) * (x+2) < 0, x > -2, x > 0],[y,x]);
 269 'emptyset$
 270
 271 fourier_elim([x < 1 and x > 5],[x]);
 272 'emptyset$
 273
 274 fourier_elim([x < 1 or x > 5],[x]);
 275 [5 < x] or [x < 1]$
 276
 277 fourier_elim([y+x=2,x-y=0, y < 8],[x,y]);
 278 [x = 1,y = 1]$
 279
 280 fourier_elim([y+x=2,x-y=0, y < 1],[x,y]);
 281 'emptyset$
 282
 283 fourier_elim([y+x=2,x-y=0, y < 8],[x,y]);
 284 [x = 1,y = 1]$
 285
 286 fourier_elim([abs(x) + abs(x/2) + abs(x/3) =  1],[x]);
 287 [x=-6/11] or [x=6/11]$
 288
 289 fourier_elim([abs(x) + abs(x/2) + abs(x/3) #  1],[x]);
 290 [x = 0] or [0 < x,x < 6/11] or [-6/11 < x,x < 0] or [x < -6/11] or [6/11 < x]$
 291
 292 fourier_elim([max(x,6) < max(x,7)],[x]);
 293 [x<6] or [x=6] or [6<x,x<7]$
 294
 295 fourier_elim([max(x,6) < max(x,7) - 1],[x]);
 296 'emptyset$
 297
 298 fourier_elim([max(x,-x) = abs(x)],[x]);
 299 'universalset$
 300
 301 fourier_elim([max(x,-x) # abs(x)],[x]);
 302 'emptyset$
 303
 304 fourier_elim([max(x,-x) < abs(x)],[x]);
 305 'emptyset$
 306
 307 fourier_elim([min(x,1) < max(x,1)],[x]);
 308 [1<x] or [x<1]$
 309
 310 fourier_elim([max(x,-x/2) < 1],[x]);
 311 [-2<x,x<1]$
 312
 313 fourier_elim([abs(x - abs(x-1)) + abs(x) < 1],[x]);
 314 [0<x,x<1/2] or [x=1/2] or [1/2<x,x<2/3]$  /* [0 < x, x < 2/3] is better */
 315
 316 fourier_elim([x * (x-1) < a * (a - 1)],[x,a]);
 317 [1-a<x,x<a,1/2<a] or [a<x,x<1-a,a<1/2]$
 318
 319 fourier_elim([x < 3.14], [x]);
 320 [x < 3.14]$
 321
 322 fourier_elim([x > 3.14],[x]);
 323 [3.14 < x]$
 324
 325 fourier_elim([2.78b0 *  x > 3.14b0],[x]);
 326 [1.129496402877698b0 < x]$
 327
 328 fourier_elim([min(x,0) >= 0],[x]);
 329 [x=0] or [0<x]$
 330
 331 /* This answer isn't wrong, but it could be simplified. */
 332
 333 fourier_elim([abs(x - abs(x - abs(x - 23))) > abs(x-1)],[x]);
 334 [x<1] or [x=1] or [1<x,x<6] or [11<x,x<23/2] or [x=23/2] or [23/2<x,x<12]$
 335
 336 fourier_elim([sqrt(5) * x < 1],[x]);
 337 [x<1/sqrt(5)]$
 338
 339 fourier_elim([sqrt(2) < x + y, x < sqrt(5), y  < 1],[x,y]);
 340 [sqrt(2)-y<x,x<sqrt(5),sqrt(2)-sqrt(5)<y,y<1]$
 341
 342 fourier_elim([max(x,y) < min(x,y)],[x,y]);
 343 'emptyset$
 344
 345 fourier_elim([min(x,y) < max(x,y)],[x,y]);
 346 [x<y] or [y<x]$
 347
 348 fourier_elim([min(x,y) <= max(x,y)],[x,y]);
 349 [x=y] or [x<y] or [y<x]$
 350
 351 fourier_elim([0>=x,0=z],[x,z]);
 352 [x=0,z=0] or [z=0,x<0]$
 353
 354 fourier_elim(x < 1 and x >= 1,[x]);
 355 'emptyset$
 356
 357 fourier_elim(x <= 1 and x >= 1,[x]);
 358 [x = 1]$
 359
 360 fourier_elim([log(x) > log(a)],[x, a]);
 361 [a<x,0<a]$
 362
 363 /* SF bug 1952642 */
 364
 365 fourier_elim([abs(x)>1], [x]);
 366 [x<-1] or [1<x]$
 367
 368 /* SF bug 2030675 */
 369
 370 fourier_elim([f(abs(x)) < 0],[x]);
 371 [- f(abs(x)) > 0]$
 372
 373 fourier_elim([f(abs(x)) > 0],[x]);
 374 [f(abs(x)) > 0]$
 375
 376 fourier_elim([log(x) < log(a)],[x,a]);
 377 [0 < x, x < a, 0 < a]$
 378
 379 /* affine_p tests */
 380
 381 affine_p(0,[]);
 382 true$
 383
 384 affine_p(2*%pi*%i,[x,y,z]);
 385 true$
 386
 387 affine_p(0,[x]);
 388 true$
 389
 390 affine_p(x,[x]);
 391 true$
 392
 393 affine_p(x[1],[x[1]]);
 394 true$
 395
 396 affine_p(y,[x]);
 397 true$
 398
 399 affine_p(a*x,[x]);
 400 true$
 401
 402 affine_p(a*x,[x,y]);
 403 true$
 404
 405 affine_p(a*x+y,[x,y]);
 406 true$
 407
 408 affine_p(a*x+y*sin(q),[x,y]);
 409 true$
 410
 411 affine_p((x-y)/(a-b),[x,y]);
 412 true$
 413
 414 affine_p((x^2-y^2)/(x-y),[x,y]);
 415 true$
 416
 417 affine_p(sin(x),[x]);
 418 false$
 419
 420 affine_p(x*y,[x,y]);
 421 false$
 422
 423 affine_p(1/x,[x]);
 424 false$
 425
 426 affine_p([1,2],[]);
 427 false$
 428
 429 affine_p(x=y,[]);
 430 false$
 431
 432 affine_p(taylor(x,x,0,1),[x]);
 433 false$
 434
 435 affine_p((x^2+y^2)/(x-y),[x,y]);
 436 false$
 437
 438 affine_p(x[1]^2,[x[1]]);
 439 false$
 440
 441 affine_p(x[1]*y[1],[x[1],y[1]]);
 442 false$
 443
 444 /* actual regressions */
 445
 446 fourier_elim(x = y*z,[x,y,z]); /* #2628 fourier elimination on equality */
 447 [y*z-x=0]$
 448
 449 /* known bugs!  */
 450 fourier_elim([x < 1/a],[x]);
 451 [x < 1/a]$
 452
 453 fourier_elim([x - cos(z) < 0],[x]);
 454 [x < cos(z)]$
 455
 456 fourier_elim([x - z^42 < 0],[x]);
 457 [x < z^42]$
 458
 459 /* I think this bug is related to linsolve([x=3.14],[x]) --> [x = 157/50]. Even when
 460 keepfloat is true, linsolve converts floats to rationals. */
 461 fourier_elim([x<=3.14],[x]);
 462 [x = 3.14] or [x < 3.14]$
 463
 464 /* end of known bugs */
 465
 466 /* #3799 fourier_elim returns non-(in)equations */
 467
 468 fourier_elim([x0 + 2*x1 + 2 <= 0, -3*x0 + 4*x1 - 4 <= 0], [x0,x1]);
 469 [x0=-8/5,x1=-1/5] or [x0=(4*x1-4)/3,x1<-1/5] or [x0=-2*x1-2,x1<-1/5] or [(4*x1)/3-4/3<x0,x0<-2*x1-2,x1<-1/5]$
 470
 471 xxx : fourier_elim([x0 + 2*x1 + 2 <= 0, -3*x0 + 4*x1 - 4 <= 0], [x0]);
 472 [x0=-2*x1-2,5*x1+1=0] or [x0=(4*x1-4)/3,-6*(5*x1+1)>0] or [x0=-2*x1-2,-2*(5*x1+1)>0] or [(4*x1)/3-4/3<x0,x0<-2*x1-2,-
 473 6*(5*x1+1)>0]$
 474
 475 fourier_elim(subst(x1=-1/5, xxx),[x0]);
 476 [x0=-8/5]$
 477
 478 fourier_elim(subst(x1=-1/5, [x0 + 2*x1 + 2 <= 0, -3*x0 + 4*x1 - 4 <= 0]), [x0]);
 479 [x0=-8/5]$
 480
 481 fourier_elim([a=0],[a]);
 482 [a=0]$
 483
 484 fourier_elim([a=0],[]);
 485 [a=0]$
 486
 487 fourier_elim([a=k,a>k],[a]);
 488 emptyset$
 489
 490 fourier_elim([a=k,a>k],[k]);
 491 emptyset$
 492
 493 fourier_elim([a=k,a>k],[]);
 494 [a-k>0,k-a=0]$
 495
 496 fourier_elim([0<=b+x,b<=x],[b,x]);
 497 [b=0,x=0] or [b=x,0<x] or [b=-x,0<x] or [-x<b,b<x,0<x]$
 498
 499 fourier_elim([0<=b+x,b<=x],[x,b]);
 500 [x=0,b=0] or [x=b,0<b] or [x=-b,b<0] or [max(-b,b)<x]$
 501
 502 xxx : fourier_elim([0<=b+x,b<=x],[b]);
 503 [b=x,x=0] or [b=x,2*x>0] or [b=-x,2*x>0] or [-x<b,b<x,2*x>0]$
 504
 505 fourier_elim(xxx,[b,x]);
 506 [-x<b,b<x,0<x] or [b=-x,0<x] or [b=x,0<x] or [b=0,x=0]$
 507
 508 xxx : fourier_elim([0<=b+x,b<=x],[b]);
 509 [b=x,x=0] or [b=x,2*x>0] or [b=-x,2*x>0] or [-x<b,b<x,2*x>0]$
 510
 511 fourier_elim(subst(x=107,xxx),[b]);
 512 [-107<b,b<107] or [b=-107] or [b=107]$
 513
 514 /* #2783 fourier_elim and "domain : complex"  */
 515
 516 block([domain : complex], fourier_elim((x-1)/(x-5) <= 1/3,[x]));
 517  [x=-1] or [-1<x,x<5]$
 518
 519 (remvalue(xxx),0);
 520 0$
 521
 522 values;
 523 []$
 524
 525 contexts;
 526 [initial,global]$
 527
 528
 529