# Not a valid ring equation

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?

Flávio.

1 Like

Ok, I got it. I haven’t noticed the minus sign.

hi,
ring is not handling minus but the nia (nonlinear linear integer arithmetic) tactic does :

``````Require Import Lia.

Goal forall n, S (n + S (n + 0) + 1 + S n * S n) = S (S n) * S (S n).
intros.
nia.
Qed.

Goal forall n,  n + S (n + 0) - 0 + n * n = S n * S n.
intros.
nia.
Qed.
``````

Laurent

Ps:
even lia (linear integer arithmetic) solves your goal thanks to its preprocessing.

Hi Laurent,

Very nice. Thank you!