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?

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

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.

is there alternative channel of communication to ask these kind of questions?

This looks like the right place to me.

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.

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

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

Thank god this should be the lifesaver! Let me test it and see if it works in my case

EDIT: it works!!!!!

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

abab9579 has marked this topic as resolved.

Last updated: Jul 15 2024 at 20:02 UTC