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?

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.
```

You could rely on the `lia`

tactic (after `Require Import Lia.`

).

Thanks! Both of those tactics could solve it.

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`

?

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

, should help

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