Ah! I found a bad case for redundant assertions... but also a solution.
Let's simplify your code to the following (unwind_protect is a good idea,
but not relevant to this case):
simp_given( expr, [assumptions]) :=
block([to_forget, val],
to_forget: apply('assume,assumptions),
val: expand(expr, 0, 0),
apply('forget,to_forget),
val ) $
(%i56) simp_given(abs(x),abs(x)>0,x>0);
(%o56) x
(%i57) facts();
(%o57) [abs(x) > 0] <<<< oops! fact
was not forgotten
The problem is that 'forget' simplifies abs(x)>0 to x>0.
simp_given( expr, [assumptions]) :=
block([to_forget, val, simp],
to_forget: apply('assume,assumptions),
val: expand(expr, 0, 0),
simp: false, /* prevent
simplification of abs(x) to x within 'forget' */
apply('forget,to_forget),
val ) $
I would still recommend that you use the 'contexts' system.
-s
On Sat, Jun 2, 2012 at 3:32 PM, Stavros Macrakis <macrakis at alum.mit.edu>wrote:
> I was wrong: your code works correctly with redundant assertions.
>
> I'd recommend you throw an error if member('inconsistent,_ans).
>
> By the way, why are you defining simp_given as a macro?
>
> -s
>
> On Sat, Jun 2, 2012 at 3:00 PM, Richard Hennessy <
> rich.hennessy at verizon.net> wrote:
>
>> Maybe simp_given() could be modified to throw an exception if the facts
>> are inconsistent, I'm not sure. I don't think it is broken. I don?t know
>> of any bugs at all. The behavior with inconsistent assumptions is (maybe)
>> unpredictable but I am not sure if that is a bug. It looks like the
>> behavior when the facts are inconsistent is that is uses the facts given up
>> until it reaches an inconsistency and then just throws that one away and
>> continues with the next assumption in the list. Maybe the help should just
>> say that.
>>
>> kill(all)$
>> load(pwlimit)$
>> simp_given(e, [fcts]) ::= buildq([e,fcts], block([_ans],
>> unwind_protect((_ans:apply(**assume, fcts), expand(e,0,0)),
>> apply(forget,_ans))))$
>> display2d:false$
>> facts();
>> -> []
>> simp_given(signum(a)+signum(b)**,a<0,a>0,b<0);
>> -> -2
>> facts();
>> -> []
>> simp_given(signum(a)+signum(b)**,a<0,a<=b,b<0);
>> -> -2
>> facts();
>> -> []
>> simp_given(signum(a)+signum(b)**,a<0,a<b);
>> -> signum(b)-1
>> facts();
>> -> []
>> simp_given(signum(a)+2*signum(**b)+4*signum(c),a>0,b<c,a>c,a<**c);
>> -> 4*signum(c)+2*signum(b)+1
>> facts();
>> -> []
>> simp_given(signum(a)+2*signum(**b)+4*signum(c),a>0,b>a,c>a,a<**c);
>> -> 7
>> facts();
>> -> []
>> simp_given(signum(a)+2*signum(**b)+4*signum(c),a>0,b>a,c<a,a>**c);
>> -> 4*signum(c)+3
>> facts();
>> -> []
>> simp_given(signum(a)+2*signum(**b)+4*signum(c),a>0,b>a,c>a);
>> -> 7
>> simp_given(signum(a)+2*signum(**b)+4*signum(c),a>0,b>a,c>b);
>> -> 7
>> facts();
>> -> []
>> simp_given(signum(a)+2*signum(**b)+4*signum(c),a>0,b>a,c>b,c<**a);
>> -> 7
>> facts();
>> -> []
>>
>> RVH
>>
>> -----Original Message----- From: Richard Hennessy
>> Sent: Friday, June 01, 2012 8:20 PM
>> To: Stavros Macrakis ; Barton Willis
>>
>> Cc: maxima at math.utexas.edu
>> Subject: Re: [Maxima] pw.mac
>>
>> (%i1) simp_given(signum(a),a>0,a<0);
>> (out1) 1
>> (%i2) facts();
>> (out2) [kind(sinh, one_to_one), kind(log, one_to_one), kind(tanh,
>> one_to_one), kind(log, increasing)]
>>
>> Yes, if the assumptions are inconsistent who knows what you?re going to
>> get
>> and Maxima has a weak assume system anyway. If the assumptions are
>> redundant then I don?t know if it breaks the code. Can you give an
>> example.
>> Seems okay to me.
>>
>> Rich
>>
>> From: Stavros Macrakis
>> Sent: Friday, June 01, 2012 7:04 PM
>> To: Richard Hennessy ; Barton Willis
>> Cc: maxima at math.utexas.edu
>> Subject: Re: [Maxima] pw.mac
>>
>> Richard,
>>
>>
>> I don't know about other issues, but your simp_given won't work right if
>> some of the assumptions are redundant. You should use the context
>> mechanism, as Barton now is (see mail below).
>>
>>
>> I've also encouraged him to rewrite his simp_assuming and with_assumptions
>> functions using contexts.
>>
>>
>> -s
>>
>>
>> ---------- Forwarded message ----------
>> From: Barton Willis <willisb at unk.edu>
>> Date: Wed, May 16, 2012 at 1:57 PM
>> Subject: context based version of abs_integrate--no more
>> simp_assuming
>> To: "maxima at math.utexas.edu" <maxima at math.utexas.edu>
>>
>>
>> I committed a new version of abs_integrate that uses contexts instead of
>> the
>> buggy simp_assuming macro. The new code doesn't have a general purpose
>> with_assumptions function (or macro) replacement for simp_assuming.
>>
>> The new version also fixes some other bugs (rtest_abs_integrate bugs 148
>> and
>> 149).
>>
>> --bw
>>
>> ______________________________**_________________
>> Maxima mailing list
>> Maxima at math.utexas.edu
>> http://www.math.utexas.edu/**mailman/listinfo/maxima<http://www.math.utexas.edu/mailman/listinfo/maxima>;
>>
>>
>> On Fri, Jun 1, 2012 at 6:13 PM, Richard Hennessy <
>> rich.hennessy at verizon.net>
>> wrote:
>>
>> "I don't know what your simp_given function looks like, but
>>
>> (%i27) ctsp(expr,x,c) := limit(expr, x, c, plus) - limit(expr, x, c,
>> minus);
>> (%o27) ctsp(expr, x, c) := limit(expr, x, c, plus) - limit(expr, x, c,
>> minus)
>> (%i28) ctsp(x^2*signum(x-4), x, c);
>> 2 2
>> (%o28) limit x signum(x - 4) - limit x signum(x - 4)
>> x -> c+ x -> c-
>>
>> However, of course:
>>
>> (%i29) ctsp(u^2*signum(u-4), x, c);
>> (%o29) 0
>>
>> Could you have a problem with what the dummy variable is or something?"
>>
>> I forgot to say kill(all). pw.mac was loaded, it changes the answer for
>> some reason. If I start with kill(all) then I get what you get. I don't
>> know why, maybe because of diff and integrate being modified by pw.mac or
>> abs_integrate.mac. Does limit ever call integrate or diff? Either way
>> this
>> method does not work.
>>
>> Rich
>>
>> PS
>> simp_given(e, [fcts]) ::= buildq([e,fcts], block([_ans],
>> unwind_protect((_ans:apply(**assume, fcts), expand(e,0,0)),
>> apply(forget,_ans))));
>>
>>
>>
>> ______________________________**_________________
>> Maxima mailing list
>> Maxima at math.utexas.edu
>> http://www.math.utexas.edu/**mailman/listinfo/maxima<http://www.math.utexas.edu/mailman/listinfo/maxima>;
>>
>>
>> ______________________________**_________________
>> Maxima mailing list
>> Maxima at math.utexas.edu
>> http://www.math.utexas.edu/**mailman/listinfo/maxima<http://www.math.utexas.edu/mailman/listinfo/maxima>;
>>
>
>