Skip to content

perf(Game/IGame): speedup multiplication theorems#294

Open
plp127 wants to merge 8 commits intovihdzp:masterfrom
plp127:aliu/fast_mul
Open

perf(Game/IGame): speedup multiplication theorems#294
plp127 wants to merge 8 commits intovihdzp:masterfrom
plp127:aliu/fast_mul

Conversation

@plp127
Copy link
Contributor

@plp127 plp127 commented Jan 6, 2026

Speedup multiplication theorems in Game/IGame

I measured

  • private theorem mul_comm' goes from 1500ms to 50ms
  • private theorem neg_mul' goes from 1000ms to 220ms

@plp127 plp127 changed the title perf(IGame): speedup multiplication theorems perf(Game/IGame): speedup multiplication theorems Jan 6, 2026
@plp127
Copy link
Contributor Author

plp127 commented Jan 6, 2026

The private theorem zero_mul' is 80ms, so that one is fine, but private theorem one_mul' is 3000ms. I didn't touch one_mul' because the proof is so short, but should I try speeding that up too?

@vihdzp
Copy link
Owner

vihdzp commented Jan 6, 2026

I'd personally feel sad replacing a succinct proof for a fifteen-line case bash in favor of like two seconds of build-time. But if you can find terse proofs (or proofs that are no worse) that are faster, then that's obviously a net positive.

Copy link
Owner

@vihdzp vihdzp left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not all too sure how I feel about mul_eq'' having a "manual proof", to be honest. I'll leave the decision of merging this up to @tristan-f-r.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants