The `continuity` tactic and `![f x, g x]`

Stream: mathlib4

[Eric Wieser]

Is it expected that continuity can't handle this?

import Mathlib

attribute [continuity] Continuous.matrixVecCons

-- fails
example : Continuous fun θ : ℝ => ![Real.sin θ, Real.cos θ] := by
  continuity

-- succeeds
example : Continuous fun θ : ℝ => ![Real.sin θ, Real.cos θ] := by
  apply Continuous.matrixVecCons
  · continuity
  apply Continuous.matrixVecCons
  · continuity
  continuity

[Eric Wieser]

(docs#Continuous.matrixVecCons isn't in the web editor nor the docs just yet, but is in master)

[Eric Wieser]

@Tomas Skrivan, is this something that fun_prop can hope to handle?

[Edward van de Meent]

are you maybe missing the Matrix.vecEmpty version?

[Eric Wieser]

Huh, I guess it is surprising that the second · continuity works, but I assume something about Unique is firing (edit: changed to not rely on this)

[Jireh Loreaux]

are there any places where continuity is still preferred to fun_prop at all? My hope would be that we could deprecate continuity sometime soon.

[Eric Wieser]

Edward van de Meent said:

are you maybe missing the Matrix.vecEmpty version?

(continuous_const dispatches this one)

[Tomas Skrivan]

Eric Wieser said:

Tomas Skrivan, is this something that fun_prop can hope to handle?

It is definitely something I want to support. However, last time I wanted to prove differentiability for ![...] I noticed that it is implemented using List which is not a vector space so I wasn't sure how to proceed.

It might be a case that one has to write a sufficiently smart theorem to handle it. I will think about it.

[Eric Wieser]

I think you're getting confused with #[]?

[Eric Wieser]

![ makes no mention of List

[Yury G. Kudryashov]

![ unfolds to docs#Matrix.vecCons and docs#Matrix.vecEmpty

[Tomas Skrivan]

Then marking theorems like Continuous.matrixVecCons with fum_prop should be enough.

[Tomas Skrivan]

I will test it out, there might be an issue and fun_prop might expect the theorem to have the index of the output vector fixed.

[Eric Wieser]

Yes, I get the feeling this is either an indexing problem, or that I have stated the wrong theorem and it expects the one saying that it is jointly continuous in all the arguments

[Eric Wieser]

Tomas Skrivan said:

Then marking theorems like Continuous.matrixVecCons with fum_prop should be enough.

The web editor is now up to date; unfortunately this doesn't work there

[Eric Wieser]

Nevermind, it does work after all!

[Eric Wieser]

Tomas Skrivan said:

However, last time I wanted to prove differentiability for ![...] ...

#20407 should help a lot here, though this only does the FDeriv half and there are some TODOs