Not a valid ring equation

Using Coq
1

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.

1 Like
2

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

3

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.

4

Hi Laurent,

Very nice. Thank you!