Trashy theorems

Stream: general

[Chris B]

Wasn't sure what to call this one lol. Of the items in mathlib, finset.sum_range_sub_of_monotone and composition_as_set_equiv._proof_5 produce the largest number of garbage/intermediate items while passing through the kernel (8x and 5x the runners up respectively). I don't think it's a problem or anything since in absolute terms it's not a huge amount of memory being consumed, I'm just curious if anyone with an understanding of these parts of mathlib had any insight into what about these items might be the underlying cause. Guesses/conjecture are also welcome.
Thanks!

[Scott Morrison]

How are you measuring this?

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/236449-Program-verification/topic/Arena.20allocation.20for.20ITPs/near/206617336

[Kevin Buzzard]

and you're in the clear -- it's all polynomials, and computing pi to 6 decimal places

[Chris B]

Scott Morrison said:

How are you measuring this?

He beat me to it, but it's an independent type checker. In terms of inference and equality checks it follows Lean's kernel pretty closely, so I'm fairly confident these numbers are close to what you would actually get in Lean 3. I'm using Lean 4's strategy for inductive and quotient reduction, but not the nat stuff yet.

[Chris B]

Also it seems like suspicions in the other thread are converging on the omega tactic.

[Jalex Stark]

from my experience writing the next_coeff proof, the omegas were the part I was saddest about. I tried extracting specialized arithmetic statements, stuff that really seemed to me like they shouldn't be named lemmas, and I had difficulty proving them concisely without omega.

[Jalex Stark]

i think a slightly better "control flow" in the argument could cut down on duplicated omega work, among other things. The whole proof feels like it's screaming out for more automation. I think i recently saw a pair of Coq tactics for "pull the nth summation symbol to be the innermost / outermost sum". I guess that really doesn't apply to the thing we're doing with the double sum here.