Stream: Coq users

Topic: ✔ Eliminate common terms in LHS & RHS of goal


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

view this post on Zulip Pierre-Marie Pédrot (Sep 15 2021 at 17:54):

Yes, you can use the f_equal tactic.

view this post on Zulip Julin S (Sep 15 2021 at 17:55):

Thanks!

Using f_equal made it

n + m = m + n

view this post on Zulip Notification Bot (Sep 15 2021 at 17:55):

Ju-sh has marked this topic as resolved.

view this post on Zulip Alexander Gryzlov (Sep 15 2021 at 19:24):

You can also use congr (S m + _)

view this post on Zulip Julin S (Sep 16 2021 at 02:18):

Is congr only available for use with ssreflect?

view this post on Zulip 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: Jan 31 2023 at 12:01 UTC