TensorProduct.lift - noncomputable

Stream: mathlib4

[Antoine Chambert-Loir]

Why has docs#TensorProduct.lift been tagged as noncomputable?

[Yaël Dillies]

Because it being assumed computable by Lean takes up precious seconds in CI. And it's not like we will ever evaluate it anyway.

[Eric Wieser]

It's more that it and everything dowstream of it takes up precious minutes in everyone's editors when trying to prove things

[Eric Wieser]

I don't agree with the "we'll never evaluate it" claim, but I think we can put off doing so until the "new compiler" appears and solves all our problems :tm:

[Antoine Chambert-Loir]

The issue for me is that I had taken time to define one function using a right inverse if it was given, and that function was computable, and suddenly, merging master makes it noncomputable.

[Antoine Chambert-Loir]

So I have a function tagged noncomputable whose docstring says that this is computable because we provide the right inverse…

[Ruben Van de Velde]

Could you explain what made you bother making it computable in the first place?

[Eric Wieser]

Even if it's not computable, providing the right inverse is still a good idea because it means it reduces, possibly with nice defeqs

[Eric Wieser]

If you conjure the inverse non-constructively, usually you end up having to prove it's equal to a particular right inverse eventually, so in the long run it's best to do it up front. This is a bit like how Quotient.out should usually be a last resort, because by the time you've proved the interesting things about it you've already done all the work you would have done to use Quotient.lift (admittedly the right inverse case isn't as strong an argument).

[Antoine Chambert-Loir]

Eric gave good reasons.
I give two other ones :

• I am annoyed at the prospect of using a proof assistant in an expensive computer and not being able to compute simple things
• If mathlib cared (much more) about computability, someone could write a toposify tactic that would take most of it and transfer it to general results in toposes, so that it wouldn't be necessary to make constructions on sheaves that already exist for sets/rings/modules…

[Eric Wieser]

@Antoine Chambert-Loir, for what it's worth the noncomputable everywhere also really annoys me; but the performance implication was outrageously bad, and until we can tell lean "don't compile things until you need them", the tradeoff was just too hard to justify

[Eric Wieser]

TensorProduct.lift should be really easy to compile, it's just "iterate over a list and sum"; so the fact it's awfully slow in the first place suggests that there is probably a nasty bug hiding in the compiler here somewhere.

[Kevin Buzzard]

And nobody is motivated to find it because we're all waiting for the new compiler, which apparently isn't a priority.

[Eric Wieser]

I suppose its possible we could work around this with an @[implemented_by] attribute on TensorProduct.lift

[Eric Wieser]

(where the implementation would be to use Quotient.unquot and List.sum)

[Eric Wieser]

I'll try that out in #7649

[Antoine Chambert-Loir]

Eric Wieser said:

Antoine Chambert-Loir, for what it's worth the noncomputable everywhere also really annoys me; but the performance implication was outrageously bad, and until we can tell lean "don't compile things until you need them", the tradeoff was just too hard to justify

That I can understand.
At least I hope than whenever TensorProduct.lift is made computable again, the compiler will complain that some functions can lose their noncomputable tag.

[Eric Wieser]

Sadly it won't

[Alex J. Best]

It would be easy to write a metaprogram to find computables marked as noncomputable though.

Also as much as I'd love a toposify tactic I think that will likely take longer than the new compiler / fixing the old compiler bug before we'll be using it on tensor products!

[Alex J. Best]

Also I'm not sure marking things noncomputable would have any effect on toposify, what matters for that is simply that classical axioms aren't used, not whether or not Lean compiles code for the definition.

[Junyan Xu]

At least I hope than whenever TensorProduct.lift is made computable again, the compiler will complain that some functions can lose their noncomputable tag.

The temporary solution is to use suppress_compilation rather than adding noncomputable to every declaration, which will be easier to remove in the future.