Stream: math-comp users

Topic: Tactics for solving GRing equations?


view this post on Zulip 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?

view this post on Zulip Reynald Affeldt (Aug 25 2022 at 02:26):

Maybe https://github.com/math-comp/mczify

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Aug 26 2022 at 05:12):

that seems the job of coq-mathcomp-algebra-tactics

view this post on Zulip Enrico Tassi (Aug 26 2022 at 05:13):

https://github.com/math-comp/algebra-tactics

view this post on Zulip 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

view this post on Zulip 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