David E. Narváez (Jun 02 2025 at 14:24): David E. Narváez (Jun 02 2025 at 14:24):Related to my other question: is there code to break up divisions like (k₁*a₁+...+kₙ*aₙ) div b by grouping multiples of b then using something like div_mult_self4 to simplify the term? It looks like numeral_simprocs.ML has a lot of the code needed (normalize terms, calculate gcd, etc) but the approach there seems to be "all or nothing".
Manuel Eberl (Jun 02 2025 at 18:26):Pretty sure no. There's similar issues with periodic functions like sin, cos, cis, exp where one could possibly identify subterms of the argument to simplify or remove. But it's a bit hard to predict what level of generality is needed and how useful it would ultimately end up being. And, if it is to end up in the standard library, how much it would break. Of course one could just put it in a library somewhere and have people switch it on manually, but that will just lead to noone knowing about it and noone using it.
It's the sort of experiment one could try if one had the spare time, or put a student on it.
Last updated: Jul 05 2025 at 16:25 UTC