Unknown function with arbitrary arguments assumption

Question

Is it possible to define an assumption like this:

$Assumptions=f[__]>0

So that:

Simplify[f[x]+3==0]

(*False*)

Simplify[f[a,b,c]+4==0]

(*False*)

Etc...

The way above doesn't work, but is intended to show what I want to do.

I have this function f, that appears in many coordinate systems, and this way would be nice to avoid adding many assumptions for each set of arguments.

Answer 1

There is another alternative which you could look into: dynamically creating your assumptions. I will try to show it with the simple example you have given. Basically, when you call Simplify[f[a,b,c]+4==0] then you can easily extract the expressions matching your pattern with Cases. For instance

Cases[Hold[Simplify[f[a, b, c] - f[x] == 0]], f[__], Infinity]
(* {f[a, b, c], f[x]} *)

The same is true for your assumptions. You can easily extract the pattern you use. The next may look a bit weird, because we have to create a pattern, that matches a pattern...

Cases[f[__] + 3 > 0 && x + 3 == 2, _[Verbatim[__]], Infinity]
(* {f[__]} *)

Now, the only thing we have to do is to extract the above pattern from your assumptions and use this pattern to find all occurrences that match in your simplify code. Then we built a new, longer assumption of the form

(f[a,b,c] + 3 > 0 && x + 3 == 2) && (f[x] + 3 > 0 && x + 3 == 2)

and use this assumption to evaluate your code. Let's pack this into a function. Note that I have to hold the arguments of this new AssumingAll function because otherwise your Simplify code would be evaluated too soon:

SetAttributes[AssumingAll, {HoldAll}];
AssumingAll[ass_, code_] := 
 With[{patt = First@Cases[{ass}, _Symbol[Verbatim[__]], Infinity]},
  Assuming[
   And @@ (ass /. Verbatim[patt] :> # & /@ 
      Cases[Hold[code], patt, Infinity]),
   code]
]

Now you are free to try it out:

AssumingAll[f[__] == const, Simplify[f[a, b, c] - f[x] == 0]]
(* True *)

or

AssumingAll[f[__] > 0,
 {Simplify[f[x] + 3 == 0], Simplify[f[a, b, c] + 4 == 0]}]
(* {False, False} *)

or

AssumingAll[f[__] == -3,
 {Simplify[f[x] + 3 == 0], Simplify[f[a, b, c] + 4 == 0]}]
(* {True, False} *)

Answer 2

I'll assume that your function has no other definitions associated with it, and you only want to make it behave like a positive function when added to other expressions. This is how I would do it:

ClearAll[f]

Plus[f[x__], r__] ^:= Plus[Exp[Abs[Log[f[x]]]], r]

Simplify[f[x] + 3 == 0]

(* ==> False *)

Simplify[f[a, b, c] + 4 == 0]

(* ==> False *)

Simplify[f[a, b, c] + 4 > 0]

(* ==> True *)

Simplify[f[a, b, c] + 1 > 1]

(* ==> True *)

This uses UpSetDelayed to replace any occurrence of f with arbitrary number of arguments inside a sum by something that's positive but not of definite value. This is done by taking the absolute value of the logarithm, and then exponentiating again. I could have written more simply any expression that is known to be positive - it doesn't really matter what it is as long as we don't add definitions which give f actual values. E.g., Exp[Abs[f[x]] would also work. The last line tests that indeed the assumption $f>0$ is correctly applied because it wouldn't yield True if $f=0$ were allowed.

This method isn't designed to work outside the scope outlined in the question, so for example f isn't recognized to be positive in products.

Answer 3

Try this also:

g[y__] := Simplify[y, Assumptions :> (First@Cases[y, f[__], -1]) > 0] 
g[f[x]+3==0]

(*False*)

g[f[a,b,c]+4==0]

(*False*)