Stream: Coq users

Topic: Trivial goal with minus operation


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Olivier Laurent (Apr 29 2023 at 13:36):

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

view this post on Zulip Julin S (Apr 30 2023 at 04:29):

Thanks! Both of those tactics could solve it.

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Apr 30 2023 at 04:35):

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

view this post on Zulip 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