Julin S (Apr 29 2023 at 13:19): 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.
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: Apr 20 2024 at 15:01 UTC