fun_prop fails exponentially slowly

Stream: mathlib4

[Floris van Doorn]

When fun_prop succeeds, it is very quick, and in my experience much quicker than the aesop-alternatives like measurability/continuity and so on.
However, when looking at the trace of a failed fun_prop call, you can see many duplicated steps, so I was already worried for a while that fun_prop would be slow to fail.
For example, when looking through the trace of this example

import Mathlib.Tactic

set_option trace.Meta.Tactic.fun_prop true
set_option profiler true
example (f g: ℝ → ℝ) : Continuous (fun x ↦ f x + g x) := by fun_prop

fun_prop is actually trying to prove that f is continuous thrice, once after calling Continuous.add, and twice after calling Continuous.comp' (I don't even know why that is tried twice). This looks bad, since fun_prop tries multiple paths at every operation.

And indeed, fun_prop succeeds very quickly, but fails very slowly:

import Mathlib.Tactic

set_option trace.Meta.Tactic.fun_prop true
set_option profiler true

example (f : ℝ → ℝ) (hf : Continuous f) :
    Continuous (fun x ↦ f (x + 3)) := by fun_prop -- succeeds in 18ms
example (f : ℝ → ℝ) (hf : Continuous f) :
    Continuous (fun x ↦ (f (x + 3)) ^ 2) := by fun_prop -- succeeds in 27ms
example (f : ℝ → ℝ) (hf : Continuous f) :
    Continuous (fun x ↦ (f (x + 3)) ^ 2 * f (x + 1)) := by fun_prop -- succeeds in 39ms
example (f : ℝ → ℝ) (hf : Continuous f) :
    Continuous (fun x ↦ (f (x + 3)) ^ 2 * f (x + 1) + x) := by fun_prop -- succeeds in 42ms
example (f : ℝ → ℝ) (hf : Continuous f) :
    Continuous (fun x ↦ (f (x + 3)) ^ 2 * f (x + 1) + x + 1) := by fun_prop -- succeeds in 46ms

example (f : ℝ → ℝ) :
    Continuous (fun x ↦ f (x + 3)) := by fun_prop -- fails in 18ms
example (f : ℝ → ℝ) :
    Continuous (fun x ↦ (f (x + 3)) ^ 2) := by fun_prop -- fails in 100ms
example (f : ℝ → ℝ) :
    Continuous (fun x ↦ (f (x + 3)) ^ 2 * f (x + 1)) := by fun_prop -- fails in 590ms
example (f : ℝ → ℝ) :
    Continuous (fun x ↦ (f (x + 3)) ^ 2 * f (x + 1) + x) := by fun_prop -- fails in 2720ms
example (f : ℝ → ℝ) :
    Continuous (fun x ↦ (f (x + 3)) ^ 2 * f (x + 1) + x + 1) := by fun_prop -- fails in 10600ms

When the tracing is turned off, the times are a bit quicker, but it's still exponentially slowing down.

@Tomas Skrivan, is there a way to (re)design fun_prop to improve this? Can the @[fun_prop] attribute check that we don't add "duplicate" paths?

I conjectured this behavior recently in #18874 and this was also mentioned in #19032.

cc @Jireh Loreaux

[Tomas Skrivan]

This is something I encountered as well and have a use case where I really want fun_prop to fail fast. I do not know the solution yet. I was thinking about adding a cache for failed goals to exactly prevent trying a goal multiple times.

[Tomas Skrivan]

Thanks for the examples, I will investigate them and see if something can be done to improve on them.

[Floris van Doorn]

A cache of failed goals also sounds like a good idea.
Do you think it's also good to become more hygienic with our @[fun_prop] tagging? It seems that a large part of the branching factor comes from two "equivalent" lemmas being tagged.

[Jireh Loreaux]

A cache of successful goals seems worthwhile too, although less important.

[Tomas Skrivan]

Successful goals should be cached already.

[Tomas Skrivan]

Also there is an option maxTransitionDepth which controls how many times you can switch function property e.g. inferring continuity from differentiability and that from linearity. Setting it to zero improved failure times for me in a few scenarios.

[Tomas Skrivan]

I can also try to do something about the simple vs compositional form theorems, such that adding both does not introduce too much branching. However, I am not sure how to robustly detect that a theorem is a compositional version of another theorem.

[Tomas Skrivan]

But I think the exponential blow up should go away with catching failed goals and still having "duplicate" theorems.

[Jireh Loreaux]

I think the only value of the simple theorems for fun_prop would be for outputting the proof via a fun_prop? with Try this: (to be honest, this would be nice to have even in cases when fun_prop fails, so that you can get a partial proof).

Another nice thing to have would befun_prop? 1, which gives a Try this: for all the immediately applicable fun_proplemmas.

But I'll shut up now since I'm just asking for features without (currently) offering to implement them.

[Tomas Skrivan]

The reasons for supporting the simple theorems is more of a user friendly feature. Writing the compositional form is a chore and feels really weird for functions like sin, exp etc. Also in SciLean I generate the theorems automatically and right now I do it only in the simple form.

[Jireh Loreaux]

I don't think Mathlib minds writing the compositional form. We do it most of the time anyway for our own convenience (generally because of dot notation).

[Floris van Doorn]

If fun_prop becomes amazing and we don't have to prove these things manually, I'm happy to get rid of the compositional forms!

[Jireh Loreaux]

you mean simple forms?

[Floris van Doorn]

I didn't. But honestly it's not important until we never have to prove simple continuity lemmas ourselves anymore.

[Tomas Skrivan]

I added the cache for failed goals and it seems to fix the problem: #19107

[Tomas Skrivan]

In #19112 I added a command #print_fun_prop_theorems HDiv.hDiv to print out all fun_prop theorem attached to for example division. This should make it easier to maintain fun_prop attributes.

---

So far the function with the highest number of theorems I have found is HPow.hPow:

#print_fun_prop_theorems HPow.hPow Continuous

prints

Continuous
  Continuous.pow, args: [4], form: compositional
  Continuous.zpow₀, args: [4], form: compositional
  Continuous.zpow, args: [4], form: compositional
  ENNReal.continuous_pow, args: [4], form: simple
  ENNReal.continuous_zpow, args: [4], form: simple
  continuous_const_cpow, args: [5], form: simple
  Real.continuous_rpow_const, args: [4], form: simple
  NNReal.continuous_rpow_const, args: [4], form: simple
  ENNReal.continuous_rpow_const, args: [4], form: simple
  NNReal.continuous_nnrpow_const, args: [4], form: simple

---

I have found out that fun_prop does not check if you mark a theorem twice :)

#print_fun_prop_theorems HAdd.hAdd Differentiable

prints

Differentiable
  Differentiable.add, args: [4, 5], form: compositional
  Differentiable.add_const, args: [4], form: compositional
  Differentiable.const_add, args: [5], form: compositional
  Differentiable.add, args: [4, 5], form: compositional

This comes from Tactic.FunProp.Differentiable which is an old file that should be removed. This would cause Differentiable.add to be tried twice in case of failure thus making the situation worse.