Zulip Chat Archive

Stream: general

Topic: continuous bilinear map application is noncomputable

Eric Wieser (Mar 16 2022 at 10:48):

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 (Mar 16 2022 at 10:55):

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

Eric Wieser (Mar 16 2022 at 10:55):

Should all structure base class projections be tagged inline?

Reid Barton (Mar 16 2022 at 13:26):

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 (Mar 16 2022 at 16:11):

@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 (Jun 28 2022 at 11:49):

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 (Jun 28 2022 at 12:06):

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

Eric Wieser (Jun 28 2022 at 12:13):


Last updated: Dec 20 2023 at 11:08 UTC