## Stream: Coq users

### Topic: Trivial goal with minus operation

#### Julin S (Apr 29 2023 at 13:19):

Hi.

I was trying to solve this goal:

``````Require Import Arith.

Goal forall p q:nat,
p + p + 1 - (1 + (q + q)) = p + p - (q + q).
intros p q.
ring.
``````

Expected `ring` to be able to take care of this. But I was wrong.

How can this goal be solved? Is there a way other than manually figuring out the correct way commutativity and associativity?

Or could there be a simpler way?

And why is `ring` tactic not able to solve this? It can solve similar goals, right? Is it because of the presence of the `-` operation?

#### Gaëtan Gilbert (Apr 29 2023 at 13:33):

Is it because of the presence of the - operation?

yes
`nat` is only a semiring, ie `-` on `nat` doesn't have the ring equations

Or could there be a simpler way?

you can do

``````  replace (p + p + 1) with (1 + p + p) by ring.
reflexivity.
``````

#### Olivier Laurent (Apr 29 2023 at 13:36):

You could rely on the `lia` tactic (after `Require Import Lia.`).

#### Julin S (Apr 30 2023 at 04:29):

Thanks! Both of those tactics could solve it.

#### Julin S (Apr 30 2023 at 04:30):

In the case of the one with `replace`, the goal became:

``````1 + p + p - (1 + (q + q)) = p + p - (q + q)
``````

And doing `simpl` made it

``````p + p - (q + q) = p + p - (q + q)
``````

How was `simpl` able to get rid of the `1-1`?

#### Paolo Giarrusso (Apr 30 2023 at 04:35):

Printing the definition of minus, that is, `Print Nat.sub.`, should help

#### Paolo Giarrusso (Apr 30 2023 at 05:31):

Better: `1 + n` simplifies to `S n` for any term `n : nat`, and `S m - S n` simplifies to `m - n` for any terms `m, n : nat`

Last updated: Jun 18 2024 at 09:02 UTC