Re: Re: Simplifying inequalities
- To: mathgroup at smc.vnet.net
- Subject: [mg36833] Re: [mg36817] Re: [mg36790] Simplifying inequalities
- From: Adam Strzebonski <adams at wolfram.com>
- Date: Sat, 28 Sep 2002 04:34:32 -0400 (EDT)
- References: <1B05A609-D21F-11D6-8439-00039311C1CC@tuins.ac.jp>
- Sender: owner-wri-mathgroup at wolfram.com
Both Simplify and ImpliesQ need the assumption that all variables
are real in order to use the CAD algorithm. However, Simplify
uses many other methods trying to simplify each subexpression
of the input, while ImpliesQ only tries to prove that the whole
input is implied by the assumptions.
Here is the series of simplifications that Simplify does in this
example.
- An inequality simplification heuristic using the inequality
assumption y6 >= -1 is applied to the whole system. We get
simplification:
y4 >= -1 && y6 >= -1 && y6 <= y5 <= 1 + y4 + y6 ->
1 + y4 >= 0 && y5 >= y6 && 1 + y4 + y6 >= y5
- We go into simplification of subexpressions, and get these
simplifications using reduction modulo a GroebnerBasis of
equation assumptions y4 == -1 and y5 == y6 (Simplify keeps
the result of this transformation even if it has the same
complexity as the original expression.)
1 + y4 -> 0
y5 -> y6
1 + y4 + y6 -> y6
y5 -> y6
- As the result of subexpression simplifications the three
inequalities become then:
1 + y4 >= 0 -> 0 >= 0
y5 >= y6 -> y6 >= y6
1 + y4 + y6 >= y5 -> y6 >= y6
- 0 >= 0 evaluates to True, y6 >= y6 is simplified to True
using transformation x >= y -> x - y >= 0.
Best Regards,
Adam Strzebonski
Wolfram Research
Andrzej Kozlowski wrote:
>
> That makes everything clear, except for just one small mystery:
>
> In[1]:=
> << "Experimental`"
>
> In[2]:=
> FullSimplify[y4 >= -1 && y6 >= -1 &&
> y6 <= y5 <= 1 + y4 + y6, y4 == -1 && y6 >= -1 && y5 == y6]
>
> Out[2]=
> True
>
> In[3]:=
> ImpliesQ[y4 == -1 && y6 >= -1 && y5 == y6,
> y4 >= -1 && y6 >= -1 && y6 <= y5 <= 1 + y4 + y6]
>
> Out[3]=
> False
>
> I now understand why the last one returns False, but why does the
> second one return True? Should not the same arument apply in both
> cases? Or is it because FullSimplify does not actually need the
> assumption that the variables are real while ImliesQ does?
>
> Andrzej
>
> On Friday, September 27, 2002, at 05:15 PM, Adam Strzebonski wrote:
>
> > Actually, the reason why ImpliesQ (and FullSimplify) fail to
> > prove the implication is not that the hypothesis is a disjunction.
> > To use the cylindrical algebraic decomposition algorithm they
> > need to know that the assumptions imply that all variables are
> > real.
> >
> > The assumptions mechanism infers variable domains in a purely
> > syntactical way, i.e. v is assumed to be real if there is
> > an Element[v, Reals] statement or v appears in an inequality.
> > It does not attempt to analyze assumptions further, to figure
> > out that, say y6 >= -1 implies that y6 is real, and then if
> > we have y5 == y6 then y5 must be real too. Doing such an analysis
> > in general would require solving the assumptions over complex
> > numbers, and then finding out which variables need to be real.
> > This would be in general too time consuming to do, but analyzing
> > linear dependencies like the ones in your example is a possible
> > future improvement.
> >
> > ImpliesQ cannot prove the implication here, because it knows only
> > that y6 is real.
> >
> > In[1]:= <<Experimental`
> >
> > In[2]:= ImpliesQ[y4 == -1 && y6 >= -1 && y5 == y6,
> > y4 >= -1 && y6 >= -1 && y6 <= y5 <= 1 + y4 + y6]
> >
> > Out[2]= False
> >
> > If we add an explicit assumption that y4 and y5 are real, ImpliesQ
> > (and FullSimplify) can prove this implication, and the full version
> > of your example.
> >
> > In[3]:= ImpliesQ[Element[y4|y5, Reals] && y4 == -1 && y6 >= -1 && y5 ==
> > y6,
> > y4 >= -1 && y6 >= -1 && y6 <= y5 <= 1 + y4 + y6]
> >
> > Out[3]= True
> >
> > In[4]:= ImpliesQ[Element[y4|y5, Reals] && (y4 == -1 && y6 >= -1 &&
> > y5 == y6 || y4 > -1 && y6 >= -1 && y6 <= y5 <= 1 + y4 + y6),
> > y4 >= -1 && y6 >= -1 && y6 <= y5 <= 1 + y4 + y6]
> >
> > Out[4]=
> > True
> >
> > In[5]:= FullSimplify[y4 >= -1 && y6 >= -1 && y6 <= y5 <= 1 + y4 + y6,
> > Element[y4|y5, Reals] && (y4 == -1 && y6 >= -1 && y5 == y6 ||
> > y4 > -1 && y6 >= -1 && y6 <= y5 <= 1 + y4 + y6)]
> >
> > Out[5]=
> > True
> >
> >
> > Best Regards,
> >
> > Adam Strzebonski
> > Wolfram Research
> >
> >
> > Andrzej Kozlowski wrote:
> >>
> >> On second thoughts I realized that there seems to be an inherent
> >> ambiguity about what one coudl mean by using alternatives (statements
> >> joned by Or) assumptions. In fact it now seems to me that the
> >> reasonable intertpretation for ImpliesQ and FullSimplify ought to
> >> perhaps be different. It seems to me that ImpliesQ[Or[a,b],c] ought to
> >> return True if aand only if ImpliesQ[a,c] and ImpliesQ[b,c] both
> >> return
> >> True. If so this could be acomplished by adding the rule
> >> ImpliesQ[Or[a,b],c] = And[ImpliesQ[a,c],ImpliesQ[b,c]]. That could
> >> then
> >> be used in proving that the two answers to the system of inequalities
> >> that of Vincent's original posting are equivalent. On the other hand
> >> probably FullSimplify[a, Or[p,q]] ought to return
> >> Or[FullSimplify[a,p],FullSimplify[a,q]] (or do nothing as it doe
> >> snow).
> >> The first approach would seem to be consistent with the way
> >> FullSimplify works with domain specifications but would however have
> >> the strange effect of returning True if just one of the alternatives
> >> were true and the other false. So perhaps after all it is best to
> >> leave FullSimplify as it is. However, it seems to me that ImpliesQ
> >> shoud be able to handle such cases (?)
> >>
> >> Andrzej Kozlowski
> >> Toyama International University
> >> JAPAN
> >>
> >> On Thursday, September 26, 2002, at 03:06 PM, Andrzej Kozlowski wrote:
> >>
> >>> The modification to FullSimplify that I sent earlier works correctly
> >>> only for assumptions of the form Or[a,b] (and even then not is not
> >>> always what one would like). For what it's worth here is a better
> >>> (but
> >>> slow) version:
> >>>
> >>> In[1]:=
> >>> Unprotect[FullSimplify];
> >>>
> >>> In[2]:=
> >>> FullSimplify[expr_, x_ || y__] := FullSimplify[
> >>> FullSimplify[expr, x] || FullSimplify[expr, Or[y]]];
> >>>
> >>> In[3]:=
> >>> Protect[FullSimplify];
> >>>
> >>> For example:
> >>>
> >>> In[4]:=
> >>> FullSimplify[Sqrt[(x - 1)^2] + Sqrt[(x - 2)^2] +
> >>> Sqrt[(x - 3)^2], x > 1 || x > 2 || x > 3]
> >>>
> >>> Out[4]=
> >>> -1 + x + Abs[-3 + x] + Abs[-2 + x] ||
> >>> -3 + 2*x + Abs[-3 + x] || 3*(-2 + x)
> >>>
> >>> Andrzej Kozlowski
> >>> Toyama International University
> >>> JAPAN
> >>>
> >>>
> >>>
> >>> On Thursday, September 26, 2002, at 11:14 AM, Andrzej Kozlowski
> >>> wrote:
> >>>
> >>>> The reason why InequalitySolve returns it's answer in what sometimes
> >>>> turns out to be unnecessarily complicated form is that the
> >>>> underlying
> >>>> algorithm, Cylindrical Agebraic Decomposition (CAD) returns its
> >>>> answers in this form. Unfortunately it seems to me unlikely that a
> >>>> simplification of the kind you need can be can be accomplished in
> >>>> any
> >>>> general way. To see why observe the following. First of all:
> >>>>
> >>>> In[1]:=
> >>>> FullSimplify[x > 0 || x == 0]
> >>>>
> >>>> Out[1]=
> >>>> x >= 0
> >>>>
> >>>> This is fine. However:
> >>>>
> >>>> In[2]:=
> >>>> FullSimplify[x > 0 && x < 2 || x == 0 && x < 2]
> >>>>
> >>>> Out[2]=
> >>>> x == 0 || 0 < x < 2
> >>>>
> >>>> Of course what you would like is simply 0 <= x < 2. One reason why
> >>>> you can't get it is that while Mathematica can perform a
> >>>> "LogicalExpand", as in:
> >>>> In[3]:=
> >>>> LogicalExpand[(x > 0 || x == 0) && x < 2]
> >>>>
> >>>> Out[3]=
> >>>> x == 0 && x < 2 || x > 0 && x < 2
> >>>>
> >>>> There i no "LogicalFactor" or anything similar that would reverse
> >>>> what LogicalExpand does. if there was then you could perform the
> >>>> sort
> >>>> of simplifications you need for:
> >>>>
> >>>> In[4]:=
> >>>> FullSimplify[(x > 0 || x == 0) && x < 2]
> >>>>
> >>>> Out[4]=
> >>>> 0 <= x < 2
> >>>>
> >>>> However, it does not seem to me very likely that such "logical
> >>>> factoring" can be performed by a general enough algorithm (though I
> >>>> am no expert in this field). In any case, certainly Mathematica
> >>>> can't
> >>>> do this.
> >>>>
> >>>> I also noticed that Mathematica seems unable to show that the answer
> >>>> it returns to your problem is actually equivalent to your simpler
> >>>> one. In fact this looks like a possible bug in Mathematica. Let's
> >>>> first try the function ImpliesQ from the Experimental context:
> >>>>
> >>>> << Experimental`
> >>>>
> >>>> Now Mathematica correctly gives:
> >>>>
> >>>> In[6]:=
> >>>> ImpliesQ[y4 >= -1 && y6 >= -1 && y6 <= y5 <= 1 + y4 + y6,
> >>>> y4 == -1 && y6 >= -1 && y5 == y6 || y4 > -1 && y6 >= -1 && y6 <=
> >>>> y5
> >>>> <= 1 + y4 + y6]
> >>>>
> >>>> Out[6]=
> >>>> True
> >>>>
> >>>> However:
> >>>>
> >>>> In[7]:=
> >>>> ImpliesQ[y4 == -1 && y6 >= -1 && y5 == y6 || y4 > -1 && y6 >= -1 &&
> >>>> y6 <= y5 <= 1 + y4 + y6, y4 >= -1 && y6 >= -1 && y6 <= y5 <= 1 +
> >>>> y4 + y6]
> >>>>
> >>>> Out[7]=
> >>>> False
> >>>>
> >>>> That simply means that ImpliesQ cannot show the implication, not
> >>>> that
> >>>> it does not hold. ImpliesQ relies on CAD, as does FullSimplify.
> >>>> Switching to FullSimplify we see that:
> >>>>
> >>>>
> >>>>
> >>>> In[8]:=
> >>>> FullSimplify[y4 == -1 && y6 >= -1 && y5 == y6 || y4 > -1 && y6 >= -1
> >>>> &&
> >>>> y6 <= y5 <= 1 + y4 + y6, y4 >= -1 && y6 >= -1 && y6 <= y5 <= 1 +
> >>>> y4 + y6]
> >>>>
> >>>> Out[8]=
> >>>> True
> >>>>
> >>>> while
> >>>>
> >>>> In[9]:=
> >>>> FullSimplify[y4 >= -1 && y6 >= -1 && y6 <= y5 <= 1 + y4 + y6,
> >>>> y4 == -1 && y6 >= -1 && y5 == y6 || y4 > -1 && y6 >= -1 && y6 <=
> >>>> y5
> >>>> <= 1 + y4 + y6]
> >>>>
> >>>> Out[9]=
> >>>> y4 >= -1 && y6 <= y5 <= 1 + y4 + y6
> >>>>
> >>>> On the other hand, taking just the individual summands of Or as
> >>>> hypotheses;
> >>>> In[10]:=
> >>>> FullSimplify[y4 >= -1 && y6 >= -1 && y6 <= y5 <= 1 + y4 + y6,
> >>>> y4 > -1 && y6 >= -1 && y6 <= y5 <= 1 + y4 + y6]
> >>>>
> >>>> Out[10]=
> >>>> True
> >>>>
> >>>> In[11]:=
> >>>> FullSimplify[y4 >= -1 && y6 >= -1 && y6 <= y5 <= 1 + y4 + y6,
> >>>> y4 == -1 && y6 >= -1 && y5 == y6 ]
> >>>>
> >>>> Out[11]=
> >>>> True
> >>>>
> >>>> In fact FullSimplify is unable to use Or in assumptions, which can
> >>>> be
> >>>> demonstrated on an abstract example:
> >>>>
> >>>>
> >>>> In[12]:=
> >>>> FullSimplify[C,(A||B)&&(C)]
> >>>>
> >>>> Out[12]=
> >>>> True
> >>>>
> >>>> In[13]:=
> >>>> FullSimplify[C,LogicalExpand[(A||B)&&(C)]]
> >>>>
> >>>> Out[13]=
> >>>> C
> >>>>
> >>>> This could be fixed by modifying FullSimplify:
> >>>>
> >>>> In[14]:=
> >>>> Unprotect[FullSimplify];
> >>>>
> >>>> In[14]:=
> >>>> FullSimplify[expr_,Or[x_,y__]]:=Or[FullSimplify[expr,x],FullSimplify
> >>>> [e
> >>>> xpr,y]];
> >>>>
> >>>> In[15]:=
> >>>> Protect[FullSimplify];
> >>>>
> >>>> Now at least we get as before:
> >>>>
> >>>> In[16]:=
> >>>> FullSimplify[y4 == -1 && y6 >= -1 && y5 == y6 || y4 > -1 && y6 >= -1
> >>>> &&
> >>>> y6 <= y5 <= 1 + y4 + y6, y4 >= -1 && y6 >= -1 && y6 <= y5 <= 1 +
> >>>> y4 + y6]
> >>>>
> >>>> Out[16]=
> >>>> True
> >>>>
> >>>> but also:
> >>>>
> >>>> In[17]:=
> >>>> FullSimplify[y4 >= -1 && y6 >= -1 && y6 <= y5 <= 1 + y4 + y6,
> >>>> y4 == -1 && y6 >= -1 && y5 == y6 || y4 > -1 && y6 >= -1 && y6 <=
> >>>> y5
> >>>> <= 1 + y4 + y6]
> >>>>
> >>>> Out[17]=
> >>>> True
> >>>>
> >>>> This seems to me a possible worthwhile improvement in FullSimplify,
> >>>> though of course not really helpful for your problem.
> >>>>
> >>>>
> >>>> Andrzej Kozlowski
> >>>> Toyama International University
> >>>> JAPAN
> >>>>
> >>>>
> >>>> On Wednesday, September 25, 2002, at 02:51 PM, Vincent Bouchard
> >>>> wrote:
> >>>>
> >>>>> I have a set of inequalities that I solve with InequalitySolve. But
> >>>>> then
> >>>>> it gives a complete set of solutions, but not in the way I would
> >>>>> like it
> >>>>> to be! :-) For example, the simple following calculation will give:
> >>>>>
> >>>>> In[1]:= ineq = {y4 >= -1, y5 >= -1, y6 + y4 >= y5 - 1, y5 >= y6, y6
> >>>>>> = -1};
> >>>>> InequalitySolve[ineq,{y4,y6,y5}]
> >>>>>
> >>>>> Out[1]:= y4 == -1 && y6 >= -1 && y5 == y6 ||
> >>>>> y4 > -1 && y6 >= -1 && y6 <= y5 <= 1 + y4 + y6
> >>>>>
> >>>>> the result is good, but I would like it to be in the simpler but
> >>>>> equivalent form
> >>>>>
> >>>>> y4 >= -1 && y6 >= -1 && y6 <= y5 <= 1 + y4 + y6
> >>>>>
> >>>>> How can I tell InequalitySolve to do that? It is simple for this
> >>>>> example,
> >>>>> but for a large set of simple inequalities InequalitySolve gives
> >>>>> lines and
> >>>>> lines of results instead of a simple result.
> >>>>>
> >>>>> Thanks,
> >>>>>
> >>>>> Vincent Bouchard
> >>>>> DPHil student in theoretical physics in University of Oxford
> >>>>>
> >>>>>
> >>>>>
> >>>>>
> >>>>
> >>>>
> >>>
> >>>
> >
> >
> >
> Andrzej Kozlowski
> Toyama International University
> JAPAN