timeout and irreducibility

Stream: general

[Patrick Massot]

I don't have much time for careful Zulip reading those days. Could someone write a summary of what has been learned about slow elaboration and also about irreducible definitions? Are there approximate rules one could list?

[Rob Lewis]

We should be better about sealing off definitions by marking them as irreducible after the interface is finished. Irreducible doesn't mean completely opaque, you can always explicitly unfold it. But we're finding slow proofs that are caused by the elaborator doing way too much unfolding. If you run into a proof that seems like it should be fast, but isn't, see if tagging something as irreducible helps it along. This can show up especially when using tactics like assumption, which try to unify lots of things with the goal and depend on that failing quickly.

[Kevin Buzzard]

I remember a while ago when people decided that the reals were better off irreducible, and I was thinking "yeah, I mean, do I even care if they're Cauchy sequences of rationals or Dedekind cuts? Why would anyone ever care about that ever?". Is it the same sort of phenomenon?

[Rob Lewis]

Yes, it's exactly that.

[Rob Lewis]

For some things, the definitional reduction is useful and shouldn't be hidden.

[Rob Lewis]

But lots of things have an interface that, once it's there, removes the need to know how the thing is actually defined.

[Chris Hughes]

And we still mark things as irreducible when we do care about the definition (we care that exp is a power series), because I guess we don't care about it often enough, and there's an equation lemma we can still use.

[Johan Commelin]

Would it make sense to mark polynomial and mv_polynomial as irreducible? Would that speed up things that use them?

[Johan Commelin]

I don't understand enough about irreducible to even make an educated guess of whether this would be a reasonable move.

[Johan Commelin]

(Btw... I've written coeff for mv_polynomial, I'll PR it soonish. That should help having a good API for mv_polynomial if we indeed make it irreducible.)

[Chris Hughes]

I think probably not but possibly. I think the main reason they are slow is because of type class inference. I would do it anyway though, since they shouldn't really be unfolded.