Julin S (Sep 15 2021 at 17:53): Julin S (Sep 15 2021 at 17:53):If there are common terms in the LHS and RHS of a goal while in proof mode, is it possible to remove them?
As in:
Example a : forall (n m : nat), (S m) + (n + m) = (S m) + (m + n).
Proof.
intros.
when the goal becomes:
S m + (n + m) = S m + (m + n)
Is there a way to remove the S m that is common in both LHS and RHS to make it just
(n + m) = (m + n)
Yes, you can use the f_equal tactic.
Julin S (Sep 15 2021 at 17:55):Thanks!
Using f_equal made it
n + m = m + n
Ju-sh has marked this topic as resolved.
Alexander Gryzlov (Sep 15 2021 at 19:24):You can also use congr (S m + _)
Julin S (Sep 16 2021 at 02:18):Is congr only available for use with ssreflect?
Alexander Gryzlov (Sep 16 2021 at 16:41):Indeed, vanilla Coq's congruence would only work if removing the common term solves the goal.
Last updated: Sep 23 2023 at 06:01 UTC