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
EDIT: it works!!!!!

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).

view this post on Zulip Notification Bot (Sep 08 2022 at 04:48):

abab9579 has marked this topic as resolved.


Last updated: Jul 15 2024 at 20:02 UTC