Hi there,

I’m confused about the ring tactic for Nat. I have two similar exercises for summing up odd Nat numbers. In the first exercises the goal S (n + S (n + 0) + 1 + S n * S n) = S (S n) * S (S n) is solved by the tactic ring. In the second exercise, the goal is n + S (n + 0) - 0 + n * n = S n * S n and the ring tactic is no longer able to solve it: Error: Tactic failure: not a valid ring equation.

Require Import ArithRing.

Fixpoint somaimp_0 n :=

match n with

| 0 => 1

| S k => (2 * n + 1) + somaimp_0 k

end.Lemma soma_imp_0: forall n, somaimp_0 n = (S n) * (S n).

Proof.

induction n.

- simpl.

reflexivity.- simpl somaimp_0.

rewrite IHn.

ring.

Qed.Fixpoint somaimp n :=

match n with

| 0 => 0

| S k => (2 * n - 1) + somaimp k

end.Lemma soma_imp: forall n, somaimp n = n * n.

Proof.

induction n.

- simpl.

reflexivity.- simpl somaimp.

rewrite IHn.

ring.

Why n + S (n + 0) - 0 + n * n = S n * S n is not a valid ring equation?

Thanks in advance!

Flávio.