David E. Narváez (May 29 2025 at 10:41): David E. Narváez (May 29 2025 at 10:41):Are there specialized simprocs to deal with [a_0+a_1+...+a_m = b_0+b_1+...+b_n](mod k)? All the necessary theory is in Cong.thy but simply adding those lemmas to simp loops.
Manuel Eberl (May 30 2025 at 15:32):Not to my knowledge. I typically just use the rules like cong_add etc. manually. What did you have in mind?
David E. Narváez (May 30 2025 at 16:15):I was hoping for a simproc that does precisely what one would do when facing a congruence problem: check if there are terms that vanish, reduce terms that are over the modulus, etc. For the particular need I currently have it would be enough to detect numerals in the mod and in the terms and apply the necessary rules, I am a quarter of the way towards writing that. In general it would be good to have that for any reasonable term (so something like [5m + k=z-m] (mod m) would simplify to [k=z] (mod m) for example).
Manuel Eberl (May 30 2025 at 19:40):The proper way to do this would be with a "rewriting modulo congruences" procedure, i.e. generalising the simplifier to work with congruences other than equality. This has been something that people have wanted to have for a long time, and I think there was even once a prototype implementation by @Simon Roßkopf.
Manuel Eberl (May 30 2025 at 19:41):One could probably make a custom-made procedure just for Cong.cong and package it as a simproc. I don't think anyone has ever done that.
David E. Narváez (May 30 2025 at 21:00):Manuel Eberl said:
The proper way to do this would be with a "rewriting modulo congruences" procedure, i.e. generalising the simplifier to work with congruences other than equality. This has been something that people have wanted to have for a long time, and I think there was even once a prototype implementation by Simon Roßkopf.
Do you mean a [cong] rule?
Last updated: Jul 05 2025 at 20:22 UTC