5
$\begingroup$

Suppose I first declare:

$Assumptions = ForAll[{a,b}, b > a, f[b] > f[a]]

I (wrongly, as it turns out) assume that that this would cause

FullSimplify[f[4] > f[3]] 

to evaluate to

True 

but it does not (it just returns f[4] > f[3]). I've tried adding more to the assumptions i.e., that a & b are in reals, that for all x, f[x] is real and so on, but I'm just spitballing and these changes don't make a difference.

$\endgroup$
3
  • 2
    $\begingroup$ The documentation of Assumptions says: "The assumptions can be equations, inequalities, or domain specifications, or lists or logical combinations of these." I read this as implying ForAll is not included. $\endgroup$ – Sjoerd C. de Vries Aug 4 '15 at 5:30
  • $\begingroup$ I see - thanks. Perhaps there is some other way to approach this? It certainly seems like the kind of thing Mathematica is more than capable of... $\endgroup$ – John Horton Aug 4 '15 at 5:31
  • $\begingroup$ You could try setting an upvalue for f using UpSet or TagSet or their delayed versions. $\endgroup$ – Sjoerd C. de Vries Aug 4 '15 at 5:37
7
$\begingroup$

The documentation of Assumptions says: "The assumptions can be equations, inequalities, or domain specifications, or lists or logical combinations of these." I read this as implying ForAll is not included.

An approach that seems to work is the following:

f[x_] > f[y_] ^:= Piecewise[{{True, x > y}}, False]

f[3] > f[4]

(* False *)

f[4] > f[3]

(* True *)

A probably better definition would be:

f[x_] > f[y_] ^:= x > y

Note that you'll have to make definitions for the other comparison functions (GreaterEqual, Less, LessEqual) as well, as the above only defines the Greater operator in relation to f.

$\endgroup$
5
$\begingroup$

You can also use the TransformationFunctions if you don't want f evaluating outside of FullSimplify.

expr = f[4] > f[3];

mysimp[e_] := e /. {(Greater | GreaterEqual)[f[b_], f[a_]] /; b > a -> True, 
                    (Less | LessEqual)[f[b_], f[a_]] /; b < a -> True};

FullSimplify[expr, TransformationFunctions -> {mysimp, Automatic}]
True
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.