defeq abuse in `WithLp`

Stream: mathlib4

[Jireh Loreaux]

A few months ago, I helped Jon Bannon clean up some defeq abuse related to EuclideanSpace 𝕜 n in files relating to Hermitian elements. This was causing tremendous pain.

Just this weekend, I realized there is a lot of defeq abuse that occurs in docs#WithLp, and moreover, it's intentional! For instance, given x : WithLp 2 (E × F), we write x.fst even though WithLp.fst doesn't exist. Instead, Lean sees through the type synonym and applies Prod.fst instead, which, in my opinion, is terrible type hygiene. We then have a series of lemmas which copy the usual Prod simplification lemmas from Prod to this defeq abused WithLp.

This then concludes with these simp lemmas which transform type-correct terms into the defeq abused ones (presumably so that the lemmas just stated previously will then apply).

I will grant that some care has been taken here, as it includes the comment:

/-! Note that the unapplied versions of these lemmas are deliberately omitted, as they break
the use of the type synonym. -/

However, to me, this just seems like design that is liable to cause headaches down the line. I'm asking because I'm creating a type synonym for docs#CStarModule, and I noticed these abuses when copying some of the code from docs#WithLp.

[Jireh Loreaux]

@Eric Wieser I would like your opinion specifically on the topic above.

[Eric Wieser]

This f.fst stuff for f : WithLp 2 (E × F) is indeed somewhat abusive, and was copied from the prior f 0 stuff for f : WithLp 2 (Fin 2 -> F)

[Eric Wieser]

I think there's arguably something special about defeq abuse of function application (we also use it for matrices, Injective, etc), and so we took .fst and .snd along for the ride for consistency

[Jireh Loreaux]

Hmmm.... It's exactly the function application defeq abuse that was causing the pain with EuclideanSpace.

[Eric Wieser]

Was it? I thought it was the function introduction defeq (via fun _ => _or ![_, _, ...]) that caused the pain

[Jireh Loreaux]

And we don't use it for docs#Function.Injective, right? The underlying object gets coerced to a function, so there's no abuse.

[Eric Wieser]

Sure we do, we write hinj hxy when hinj : Function.Injective f and hxy : x = y, and there's no coercion there

[Yaël Dillies]

I think Jireh means Injective ⇑f

[Jireh Loreaux]

oh, that's what you mean.

[Eric Wieser]

Eric Wieser said:

I think there's arguably something special about defeq abuse of function application (we also use it for matrices, Injective, etc), and so we took .fst and .snd along for the ride for consistency

I guess Injective is quite different to Matrix and WithLp, since the latter two are data and so defeq matters

[Jireh Loreaux]

Eric Wieser said:

Was it? I thought it was the function introduction defeq (via fun _ => _or ![_, _, ...]) that caused the pain

I think it was that we only had one direction of the Equiv around (the other deleted by defeq abuse), and so things wouldn't cancel properly.

[Jireh Loreaux]

So regardless of "which direction" goes away, both are problematic.

[Eric Wieser]

I don't fully remember the situation you're thinking of, but I think we fixed it by adding some missing simp lemmas? I think this defeq abuse is sufficiently convenient that we should have a concrete example of the issue it causes on master before spending lots of effort to change the defeq and make things less convenient.

[Eric Wieser]

The defeq abuse that matters with WithLp is that we never want to end up with @norm (WithLp p V) _ v where v : V

[Jireh Loreaux]

Eric Wieser said:

but I think we fixed it by adding some missing simp lemmas?

no, we fixed it by adding a CoeFun instance to PiLp and explicitly using ⇑ where needed so that Lean didn't see through the type synonym automatically.

[Jireh Loreaux]

But it's possible it only mattered in situations where the "function" was unapplied.

[Yaël Dillies]

I guess the difference is that we have CoeToFun but not CoeToProd

[Jireh Loreaux]

Well, sure, you don't have a convenient way to state it, but that's sort of beside the point. You could still write the equiv in there manually.

[Eric Wieser]

Jireh Loreaux said:

no, we fixed it by adding a CoeFun instance to PiLp and explicitly using ⇑ where needed so that Lean didn't see through the type synonym automatically.

Did we? Where's the instance?

[Jireh Loreaux]

docs#instCoeFunPiLpForall

[Jireh Loreaux]

I think probably the difference between the two situations is exactly what the comment in the WithLp file is getting at: when it's applied (i.e., with fst or snd, or an argument to the function), it's (maybe?) okay to commit the defeq abuse (because the type of the complete expression is the same with or without the abuse, but without it we would have to create new defs on the synonym in order for it to make sense), but when it's unapplied, then it would just be blatant defeq abuse (and the types of the resulting expression are different) and could lead to problems like you mentioned above with the norm.

[Eric Wieser]

Thanks, I had forgotten about #11943. I agree the situation is less compelling for the prod case then.

[Jireh Loreaux]

In the case of EuclideanSpace, we we definitely dealing with the unapplied situation a lot, because we were consider eigenvectors as terms in EuclideanSpace 𝕜 n, but then sometimes the defeq abuse was leading them to be considered as terms of type n → 𝕜.

[Jireh Loreaux]

Eric, we still have the corresponding lemmas for PiLp (i.e., the PiLp versions of the lemmas I mentioned in the original post).

[Jireh Loreaux]

I think I'm going to tentatively stick with the WithLp approach of mild defeq abuse here. It does seem to work okay.

[Eric Wieser]

Jireh Loreaux said:

Eric, we still have the corresponding lemmas for PiLp (i.e., the PiLp versions of the lemmas I mentioned in the original post).

WithLp.equiv_pi_apply, you mean? From the source code it looks to me like the CoeFun instance is useless and doesn't actually ever apply.

[Jireh Loreaux]

No, the lemmas directly above that.

[Jireh Loreaux]

Note, the CoeFun instance is useless for applied functions because of the lemma you mentioned. It's not useless so that you can write ⇑x to get from x : WithLp p (Π i, V i) to Π i, V i without writing WithLp.equiv p _ x (assuming Lean can infer the type correctly there).

[Eric Wieser]

I don't think it's useless because of those lemmas, but rather because x i elaborates without ever doing an instance search

[Eric Wieser]

But good point about the ⇑f coercion being handy

[Jireh Loreaux]

Eric Wieser said:

I don't think it's useless because of those lemmas, but rather because x i elaborates without ever doing an instance search

indeed, also that.

[Yury G. Kudryashov]

What do you think about making WithLp a one-field structure, or even split it back into WithLpPi and WithLpProd (both structures)?

[Yury G. Kudryashov]

My reason: the distance on WithLp 0 _ defines a topology that doesn't agree with the usual one.

[Yury G. Kudryashov]

Also, as we discussed some time ago, we may want to redefine the distance on WithLp p _, p < 1, so that it becomes an additive normed group which is a p-space.

[Yury G. Kudryashov]

This way we'll get a normed group for all p.

[Yury G. Kudryashov]

And a homeomorphism to the usual (indexed) product for p ≠ 0.

[Tomas Skrivan]

From my experience, dealing with type synonyms is super hard when writing tactics. Things just break randomly and it is super hard to fix. For the purpose of automatic differentiation I gave up on using WithLp and Id monad. I would strongly prefer those to be one element structures.

[Jireh Loreaux]

@Tomas Skrivan that sounds (to me, though I'm not particularly experienced) that you're just dealing with things at the wrong level of transparency. If you're dealing with everything at reducible transparency, as I think there has been some consensus that automated tactics should do, this wouldn't be a problem.

[Jireh Loreaux]

Yury G. Kudryashov said:

What do you think about making WithLp a one-field structure, or even split it back into WithLpPi and WithLpProd (both structures)?

A one-field structure would be okay with me, but I really don't think we should split it.

[Eric Wieser]

I think we should develop some more metaprogramming infrastructure for one-field structures before investing the effort of making WithLp (and Matrix?) such a structure

[Jireh Loreaux]

Yury G. Kudryashov said:

My reason: the distance on WithLp 0 _ defines a topology that doesn't agree with the usual one.

I don't see what that has to do with making it a one-field structure.

Yury G. Kudryashov said:

Also, as we discussed some time ago, we may want to redefine the distance on WithLp p _, p < 1, so that it becomes an additive normed group which is a p-space.

This is fine, but we need to define quasi-metrics and quasi-norms first. And I also don't see what it has to do with making WithLp a structure.

[Jireh Loreaux]

Eric Wieser said:

I think we should develop some more metaprogramming infrastructure for one-field structures before investing the effort of making WithLp (and Matrix?) such a structure

Don't we have a transfer tactic for things like this?

[Eric Wieser]

I'm thinking more machinery to generate all the rfl lemmas about the canonical equivalence

[Eric Wieser]

transfer is pretty useless, I think.

[Yury G. Kudryashov]

Jireh Loreaux said:

Yury G. Kudryashov said:

My reason: the distance on WithLp 0 _ defines a topology that doesn't agree with the usual one.

I don't see what that has to do with making it a one-field structure.

Currently, we abuse the definitional equality of TopologicalSpace instances here and there (at least, we used to do it in the manifold library in Mathlib 3). Using one field structures will force us to avoid it, and it will print readable error messages instead of "these things that look the same aren't equal".

[Jireh Loreaux]

(deleted)

[Yury G. Kudryashov]

About p < 1: why do we need quasimetric? If we redefine the norm to be ∑ i, ‖x i‖^p for 0 < p < 1, then we get a usual normed group which is a p-space instead of a NormedSpace.

[Jireh Loreaux]

no we don't? It doesn't satisfy the triangle inequality if 0 < p < 1.

[Jireh Loreaux]

oh sorry, I misread / assumed I knew what you wrote.

[Jireh Loreaux]

If you want to refactor the definition of the distance and norm on WithLp to do a case split on p < 1 vs. 1 ≤ p, I'm okay with that if we get some buy-in from other maintainers.

[Tomas Skrivan]

Recently, @ZhiKai Pong is trying to prove some basic theorems about vector calculus is it very easy to get yourself into a corner by abusing defeq between EuclideanSpace ℝ (Fin 3) and Fin 3 → ℝ.

For example it took quite some time before we figured out how to prove

theorem EuclideanSpace.contDiff_apply {ι} [Fintype ι] (i : ι) :
    ContDiff ℝ n (fun f : EuclideanSpace 𝕜 ι => f i) := ...

(discussed in How to do differentiation on concrete multivariable function)

Or in this example it is all too easy to apply fderiv_pi and then be baffled why simp can't apply ContinuousLinearMap.pi_apply.

import Mathlib

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)
open InnerProductSpace
noncomputable def curl (f : ℝ³ → ℝ³) :
    ℝ³ → ℝ³ := fun x =>
  -- get i-th component of `f`
  let fi i x := ⟪f x, EuclideanSpace.single i (1:ℝ)⟫_ℝ
  -- derivative of i-th component in j-th coordinate
  -- ∂fᵢ/∂xⱼ
  let df i j x := fderiv ℝ (fi i) x (EuclideanSpace.single j (1:ℝ))
  fun i =>
    match i with
    | 0 => df 1 2 x - df 2 1 x
    | 1 => df 2 0 x - df 0 2 x
    | 2 => df 0 1 x - df 1 0 x

variable {ft : ℝ → ℝ³ → ℝ³}

example (x : ℝ³) : curl (fderiv ℝ (fun t => (ft t)) t 1) x = fderiv ℝ (fun t => curl (ft t) x) t 1 := by
  ext i
  rw [fderiv_pi (ι:=Fin 3) (h:=by sorry)]
  simp only [ContinuousLinearMap.pi_apply]
  sorry

(discussed in simplify a match pattern nested within another function)

Also one should write (WithLp.equiv 2 (Fin 3 → ℝ)).symm fun i => in the definition of curl but it does not save you from anything as rw [fderiv_pi] will be applied anyway.

Not sure what the solution or lesson is here. Is it a problem of missing API? Is the problem the defeq abuse? I'm just leaving it here as an evidence that people hit this problem and it should be dealt with one way or another.

[Matthew Ballard]

I am very skeptical of docs#EuclideanSpace being an abbrev...

[Tomas Skrivan]

Yeah EuclideanSpace is abbrev of PiLp which is abbrev of WithLp which I think is fine. However, I personally think that WithLp should be one field structure and we should have proper tooling to deal with such structures. In the process, we will realize that writing (WithLp.equiv p (Fin n → ℝ)).symm fun i => ... instead of fun i => ... is really painful and we will be forced to come up with a solution that combines the best of both worlds. (The same for product type)

[Yaël Dillies]

For a start, I do not know why WithLp.equiv takes explicit arguments. Compare to eg docs#OrderDual.toDual whose arguments are all implicit

[Yaël Dillies]

Secondly, the interesting equiv is usually the forward one (from the original space to the type synonym), because it is overall more common to have an element of the original generic type, and turn it into an element of the type synonym. So turn WithLp.equiv around.

[Jireh Loreaux]

I've had this feeling before too. Let me find the thread where we discussed it.

[Yaël Dillies]

Thirdly, the name of the equivalence should be toSynonym/ofSynonym, or a shortening thereof. Here, WithLp.toLp would be a great name which is as short as four characters once you open WithLp.

[Jireh Loreaux]

oh wait, that's this thread. :face_palm:

[Yaël Dillies]

Finally, it's sometimes useful to have the reverse equivalence too. I am not sure we want it badly here, but in case we do it could be WithLp.ofLp

[Paul Lezeau]

Yaël Dillies said:

For a start, I do not know why WithLp.equiv takes explicit arguments. Compare to eg docs#OrderDual.toDual whose arguments are all implicit

I’d be happy to have a go at fixing that! (edit: started here: #24261)

[Eric Wieser]

If we're going to rename anyway it would be less annoying for downstream code if we leave things explicit in the old name

[Paul Lezeau]

Eric Wieser said:

If we're going to rename anyway it would be less annoying for downstream code if we leave things explicit in the old name

Is your suggestion to add a WithLp.toLp, and keep WithLp.equiv (possibly with a deprecation warning) ?

[Yury G. Kudryashov]

I think, that's reasonable. Also, I like the idea of making WithLp a 1-field structure.

[Eric Wieser]

I think we should do the structure refactor separately, rather than at the same time

[Yury G. Kudryashov]

I agree, separating refactors increase chances of both of them going through.

[Jireh Loreaux]

Do we have this problem with docs#Lex too? I'm wondering if all parametric type synonyms which use Π i, X i should actually be 1-field structures?

[Eric Wieser]

Matrix too

[Filippo A. E. Nuccio]

What's the advantage of turning it into a 1-field structure?

[Eric Wieser]

It makes it impossible to defeq abuse

[Eric Wieser]

We normally catch defeq abuse in review, but this doesn't stop it tripping up new users

[Aaron Liu]

For functions that eat a function, you get to use a funlike coercion instead of defeq abuse by default

[Tomas Skrivan]

Aaron Liu said:

For functions that eat a function, you get to use a funlike coercion instead of defeq abuse by default

Also having explicit coercion like this makes it easier to write tactics.