Coq's ring tactic works with semi-ring where mc.a-t doesn't

[SnarkBoojum]

I was experimenting with the limitations of automatic tactics when I found an example where Coq's ring tactic could solve a goal and algebra-tactics' couldn't.

I could extract a simpler example from my proof script:

From mathcomp Require Import ssreflect ssrnat.

Lemma foo n: n * n.+1 * n.*2.+1 + 6 * n.+1 ^ 2 = n.+1 * n.+2 * (n.+1).*2.+1.
Proof.
Fail ring.
rewrite -!muln2.
ring.
Qed.

From mathcomp.algebra_tactics Require Import ring.

Lemma foo_bis n: n * n.+1 * n.*2.+1 + 6 * n.+1 ^ 2 = n.+1 * n.+2 * (n.+1).*2.+1.
Proof.
Fail ring.
rewrite -!muln2.
Fail ring.
Admitted.

[SnarkBoojum]

Now I find the time to dig a little more: the issue here is that natural numbers don't form a ring.

But they form what is called a semi-ring, so perhaps it's possible to do something about them.

[pi8027]

Duplicate of #40

I would suggest using lia instead.