Using fun_prop for the sum of two continuous functions

Stream: mathlib4

[Yongxi Lin (Aaron)]

Why does the first one work but the second one does not?

import Mathlib

theorem add {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) :
    Continuous (fun x => f x + g x) := by fun_prop

theorem add' {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) :
    Continuous (f + g) := by fun_prop

[David Loeffler]

We have a convention that certain lemmas about properties of functions are supposed to be formulated twice, once in "eta-expanded" form and once not; see e.g. docs#Differentiable.add and docs#Differentiable.fun_add. (The latter is autogenerated from the former using the @[to_fun] decorator.)

It looks like this wasn't carried out for Continuous.add.

[Yongxi Lin (Aaron)]

I can make a PR to address this

[Floris van Doorn]

David Loeffler said:

We have a convention that certain lemmas about properties of functions are supposed to be formulated twice, once in "eta-expanded" form and once not; see e.g. docs#Differentiable.add and docs#Differentiable.fun_add. (The latter is autogenerated from the former using the @[to_fun] decorator.)

It looks like this wasn't carried out for Continuous.add.

I don't think we have that convention at all. We allow this in situations where it's really necessary, but there is no consensus that we want to duplicate all such lemmas.

I am actually surprised that fun_prop fails for the second one, I thought that it had logic to deal with this.

[Snir Broshi]

Floris van Doorn said:

David Loeffler said:
I don't think we have that convention at all. We allow this in situations where it's really necessary, but there is no consensus that we want to duplicate all such lemmas.

#mathlib4 > Convention for `f * g` and / or `fun x ↦ f x * g x` @ 💬 caused this to be added to the naming convention, and the @[to_fun] attribute.
In the same thread at #mathlib4 > Convention for `f * g` and / or `fun x ↦ f x * g x` @ 💬 it was said that fun_ shouldn't be added to names if the unexpanded form will never exist.
It was never said explicitly, but the conclusion of that thread does seem to imply we should use @[to_fun] wherever possible.

[Snir Broshi]

Yongxi Lin (Aaron) said:

I can make a PR to address this

To cross-link, this happened in #35306

[Michael Rothgang]

You have a fair point: the naming conventions do say

If there is no need to disambiguate because a lemma is given using only the expanded form, the prefix fun_ is not required.

That does not imply "we need to duplicate each lemma every time". (And I would disagree with that.)

[Michael Rothgang]

My favourite outcome would be that

• we find out why fun_prop fails in the second example
• we fix this underlying cause, and
• we revert #35306 as it is no longer necessary.

[Michael Rothgang]

For the root cause: my understanding was the fun_prop uses the refined discrimination tree by @Jovan Gerbscheid, and that treats f * g and its eta-expanded version the same --- so fun_prop should treat them the same. Perhaps you can comment on that, Jovan and @Tomas Skrivan?

[Jovan Gerbscheid]

It was originally my idea to have the discrimination tree treat f * g the same as fun x => f x * g x. But typically for performance, we want to run unification in the reducible transparency, and unfortunately we need the reducible_and_instances transparency to unify these two forms. So this idea is not actually used now.

[Jovan Gerbscheid]

I could imagine a world where pull fun _ => _ is part of the preprocessing that fun_prop does whenever the function in question is not a lambda function. This way, we only need the fun version of any lemma to be tagged with fun_prop.

[Jireh Loreaux]

But you would also have to do that preprocessing to local hypotheses, no?

[Jovan Gerbscheid]

If we do that, then fun_prop will also be able to solve this:

example (f : ℝ → ℝ) (h : Continuous (f + g)) : Continuous (fun x ↦ f x + g x) := by
  fun_prop

[Jovan Gerbscheid]

Hmm, in that case what should be the syntax for creating a fun_ lemma and tagging only that version with fun_prop. Should it be the to_fun_prop attribute? :sweat_smile:

[Tomas Skrivan]

Michael Rothgang said:

For the root cause: my understanding was the fun_prop uses the refined discrimination tree by Jovan Gerbscheid, and that treats f * g and its eta-expanded version the same --- so fun_prop should treat them the same. Perhaps you can comment on that, Jovan and Tomas Skrivan?

The issue is not with eta expansion but the the reduction (f + g) x ==> f x + g x. fun_prop internally changes the functions to fun x => (f + g) x but it won't do the reduction to fun x => f x + g x.

fun_prop keeps track of the indices of the function arguments it knows something about. The theorem docs#Continuous.fun_add is compositional form for the first and second argument of +/HAdd.hAdd, the theorem docs#Continuous.add is simple form for the third argument.

Compositional form for all three arguments would be

theorem add'' {f g : ℝ → ℝ → ℝ} {h : ℝ → ℝ} (hf : Continuous ↿f) (hg : Continuous ↿g) (hh : Continuous h) :
    Continuous (fun x => ((f x) + (g x)) (h x)) := by fun_prop

which is still not solvable purely by fun_prop and needs dsimp or something before.

[Jovan Gerbscheid]

In this example too, using pull fun _ => _ does the trick:

module
import Mathlib

theorem add'' {f g : ℝ → ℝ → ℝ} {h : ℝ → ℝ} (hf : Continuous ↿f) (hg : Continuous ↿g) (hh : Continuous h) :
    Continuous (fun x => ((f x) + (g x)) (h x)) := by
  pull fun _ ↦ _ -- changes the goal to `Continuous fun x => f x (h x) + g x (h x)`
  fun_prop

[Tomas Skrivan]

Yes, whatever is capable of doing the reduction (f + g) x = f x + g x

[Tomas Skrivan]

We could experiment with adding and option to preprocess the function with a custom conv tactic like pull or simp.