continuous bilinear map application is noncomputable

Stream: general

[Eric Wieser]

I was surprised to find that lean claims this is noncomputable:

import analysis.normed_space.operator_norm

variables {𝕜 𝕜₂ 𝕜₃ E F G : Type*}
  [semi_normed_group E] [semi_normed_group F] [semi_normed_group G]
  [nondiscrete_normed_field 𝕜] [nondiscrete_normed_field 𝕜₂] [nondiscrete_normed_field 𝕜₃]
  [normed_space 𝕜 E] [normed_space 𝕜₂ F] [normed_space 𝕜₃ G]
  {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [ring_hom_isometric σ₂₃] [ring_hom_isometric σ₁₃]

noncomputable example (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x : E) : F →SL[σ₂₃] G  :=
f x

@Kyle Miller, do you think we can relax the computability checker somehow to allow this?

[Eric Wieser]

Oh weird; attribute [inline] continuous_linear_map.to_linear_map continuous_linear_map.to_fun fixes it

[Eric Wieser]

Should all structure base class projections be tagged inline?

[Reid Barton]

Do you expect to be able to #eval linear maps between normed spaces over nondiscrete normed fields? Maybe there are other things more deserving of your attention.

[Kyle Miller]

@Eric Wieser I was going to suggest finding well-placed inlines -- that gets things to unfold to the point that the noncomputable stuff appears only as arguments to constructors, and specifically those that are parameters of an inductive type. The VM compiler will automatically inline certain simple definitions, but for others you need the inline annotation.

It might be interesting to explore being able to tag arguments as being computationally irrelevant. I haven't needed this yet, since inline has been fine for my use: instances with a single computationally relevant field.

[Eric Wieser]

I had a quick look at using inline to make multiset.to_finsupp computable; what I found is that pretty much every def producing a bundled morphism needs to be tagged as inline

[Eric Wieser]

I'll make a PR shortly to demonstrate the impact up to add_equiv

[Eric Wieser]

#15028