# How to use ForAll to prove things about functions?

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.

• 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. – Sjoerd C. de Vries Aug 4 '15 at 5:30
• 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... – John Horton Aug 4 '15 at 5:31
• You could try setting an upvalue for f using UpSet or TagSet or their delayed versions. – Sjoerd C. de Vries Aug 4 '15 at 5:37

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.

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