Zulip Chat Archive

Stream: new members

Topic: excessive memory consumption in lemma statement

Joachim Breitner (Mar 07 2022 at 19:13):

Hmm, I’m getting

(deterministic) timeout

in one of my proofs, which is rather innocent looking. I bisected the proof lines (by inserting sorrys) to an application of

    refine bsupr_le _,

if I move the sorry above that line, it works.
I tried making that line fully explicit:

    refine @bsupr_le (submonoid M) ι _ (noncomm_pi_coprod ϕ hcomm).mrange (λ i, i  finset.univ) (λ i _, (ϕ i).mrange) _ ,

but that did not help.

I know this is not a #mwe, but maybe any hints so far?

Before some refactoring, the proof worked.

Eric Rodriguez (Mar 07 2022 at 19:22):

I think if making the line fully explicit didn't help, then I think a mwe or even the full code would be helpful

Eric Rodriguez (Mar 07 2022 at 19:23):

I'd be tempted to just work round it with a suffices : _, { exact bsupr_le this } instead of bothering figuring out why, though

Eric Rodriguez (Mar 07 2022 at 19:26):

also, is that first _ an instance search?

Joachim Breitner (Mar 07 2022 at 20:40):

Hmm, that work-around does not help, it seems

Joachim Breitner (Mar 07 2022 at 20:41):

That first _ is the complete_lattice instance for submonoid, but passing that explicitly doesn’t help either.

Kevin Buzzard (Mar 07 2022 at 20:45):

My hint is to stop saying "I know this is not a #mwe" and to let others see the code (e.g. are we on a mathlib branch?) Timeouts are hard to debug and can be caused by several things, but there are experts here.

Joachim Breitner (Mar 07 2022 at 20:47):

Absolutely right, I was about to do that, just making it a bit more presentable :-)

Joachim Breitner (Mar 07 2022 at 20:56):

This is the line that causes issues:
(branch joachim/pi_nom, file src/group_theory/noncomm_pi_coprod.lean, lemma noncomm_pi_coprod_mrange).
Help appreciated!

Joachim Breitner (Mar 07 2022 at 20:59):

Oh, I think I have it

Joachim Breitner (Mar 07 2022 at 21:00):

Because of the refactoring I no longer have a bsupr, but just a bsupr. So if I use supr_le instead of bsupr_le, it works…

Joachim Breitner (Mar 07 2022 at 21:00):


Kevin Buzzard (Mar 07 2022 at 21:12):

So this is probably one of those situations where what was happening was that Lean was trying to prove that bsupr ... = supr ... and kept unfolding and unfolding and for some reason never gave up and said "wait a minute, this actually doesn't match". I've certainly seen this sort of thing happen before.

Yaël Dillies (Mar 07 2022 at 23:31):

Also in general bsupr_le, bUnion_subset and a few lemmas around them are particularly brittle because of the precise order of elaboration. What's even more infuriating is that their duals, binfi_le, bInter_subset... don't elaborate the same way because the LHS and RHS are swapped.

Last updated: Dec 20 2023 at 11:08 UTC