abab9579 (Aug 25 2022 at 01:03): abab9579 (Aug 25 2022 at 01:03):I found myself yearning for lia while proving simple equations (like a + b = b -> a = 0).
Are there useful tactics to solve such equations in rings/lmodules?
By the way, is there alternative channel of communication to ask these kind of questions? It seems like not so much discussion is happening here, so I feel guilty of "spamming" this channel with my questions. Are there a better one for questions / lightweight talks?
Reynald Affeldt (Aug 25 2022 at 02:26):Maybe https://github.com/math-comp/mczify
Reynald Affeldt (Aug 25 2022 at 02:27):Otherwise your example can be proved as move/(congr1 (fun x => x - b)); rewrite subrr addrK. or move/esym/eqP; rewrite -subr_eq subrr => /eqP. but there is certainly a shorter script.
Reynald Affeldt (Aug 25 2022 at 02:30):is there alternative channel of communication to ask these kind of questions?
This looks like the right place to me.
abab9579 (Aug 26 2022 at 01:49):Thank you! Sadly, it seems like mczify only contains instances for concrete types like int. What I needed was a tactic to solve equations on GRings. I guess I have to prove manually, even though it might be time-consuming.
Enrico Tassi (Aug 26 2022 at 05:12):that seems the job of coq-mathcomp-algebra-tactics
Enrico Tassi (Aug 26 2022 at 05:13):https://github.com/math-comp/algebra-tactics
abab9579 (Aug 26 2022 at 05:19):Thank god this should be the lifesaver! Let me test it and see if it works in my case
Pierre Roux (Aug 26 2022 at 06:38):This "only" provides ring and field though. We are still missing lra (but this should come "soon" https://github.com/math-comp/algebra-tactics/pull/54).
Last updated: Feb 08 2023 at 07:02 UTC