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?
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
Thank god this should be the lifesaver! Let me test it and see if it works in my case
This "only" provides
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