fun_prop unfolding behaviour

Stream: mathlib4

[Michael Rothgang]

I just learned (via #33998) about fun_prop [c] --- according to the documentation there, it will unfold c and then apply fun_prop. However, there are cases in mathlib where replacing unfold foo; fun_prop by fun_prop [foo] does not work. Is this expected/can it be described when this holds? If not, I'm happy to debug further.

[Michael Rothgang]

#34000 has a few working golfs, and comments on the failing golfs.

[Michael Rothgang]

Here is one example that fails, in Mathlib.Data.Real.Sqrt, line 123:

@[continuity, fun_prop]
theorem continuous_sqrt : Continuous (√· : ℝ → ℝ) := by
  -- TODO: why does this fail? fun_prop [sqrt]
  unfold sqrt; fun_prop

(This is not an MWE, as importing mathlib makes it harder to make one.)
Replacing the local notation \sqrt by Real.sqrt does not make a difference.

[Michael Rothgang]

CC @Tomas Skrivan perhaps you can help me investigate this.

[Tomas Skrivan]

Ohh that feature was never really used and tested. Might make sense to remove it, or do you want to keep it and debug it?

[Tomas Skrivan]

My suspicion is that: If sqrt is typeclass field(like other arithmetic operations like +) then fun_prop is likely doing some naive unfolding which just results in structure projection like instSqrtReal.1 which then confuses fun_prop.

[Tomas Skrivan]

Unfortunately, I don't have the time right now to look into the code more deeply

[Jakub Nowak]

Tomas Skrivan said:

My suspicion is that: If sqrt is typeclass field(like other arithmetic operations like +) [...]

It's not.

[Aaron Liu]

aha

[Aaron Liu]

if I make Real.sqrt not irreducible then it works

[Aaron Liu]

oh and I also need to use the full name Real.sqrt instead of just sqrt

[Aaron Liu]

so that's two things

[Michael Stoll]

(Note that Real.sqrt was made irreducible for performance reasons not so long ago.)