#3172 Problems related to "assume"

[gb89]

Consider block(local(x), assume(x<0), sign(x)); facts(); sign(x);
Then maxima says that there is a fact x < 0 but after the end of block this fact should be removed as this is an assumption with respect to a local variable (there is the command "forget" to do this).
At the end sign(x) says that the sign of x is unknown which is the correct result.

Let me now explain two other problems:
assume(x > 0); asksign(x + 1); Here maxima knows that the sign is pos.
assume(a>b); asksign (a-b+1); Here maxima does not know the sign.

assume(x>0); assume(0 > x + 1); Here maxima knows that this is inconsistent.
assume(a>b); assume(b > a + 1); Here maxima does not see a problem.

Since asksign is often used by other functions it were nice if these things would work.
Often the only way to stop a function to ask signs is to say that it is zero because if you say for example that a-b+1 is positive, it will ask you the sign of a-b+2 etc.

My suggestion for the implementation, explained on the examples:
assume(a>b);

asksign (a-b+1);

1) declare res, x as local variables, assume(x > 0) (local assumption, they should be removed when going out of the block)
2) Search through all facts (in my example there is just the fact assume(a>b))
a) Bring it under the form a - b > 0
b) res : ratsubst(x, a-b, a-b+1);
c) If sign(res) is not equal to pnz, then return sign(res).

If at the end no sign has been determined, ask the user.

Remark: res = x + 1 so sign(res) = sign(x + 1) = pos

To test if it works, try
1) assume(-x^2+y+2z<0); asksign(-2z-y+x^2+1); The result should be pos.
2) assume(u-3v>0); asksign(-(u-3v)-1); The result should be neg.

Fact: assume(a>b);

We enter next: assume(b > a + 1);

1) declare res, x as local variables, assume(x > 0) (local assumption, they should be removed when going out of the block)
2) Bring b > a + 1 under the form b - a - 1 > 0
2) Search through all facts (in my example there is just the fact assume(a>b))
a) Bring it under the form a - b > 0
b) res : ratsubst(x, a-b, b - a - 1);
c) If sign(res) is not pos, then return [inconsistent].

If at the end no problem has been determined, then save the new assumption.

Remark: res = -x-1 so sign(res) = neg and [inconsistent] is returned.

Best regards

[Stavros Macrakis]

local does not work for "assume" variables, because assume maintains a global database. To control visibility of assumptions, use the context family of functions (?? context). The problem here is that local does not actually create a new local variable. It reuses the existing one, and saves and restores its properties. All problematic....