Stream: Coq users

Topic: ✔ How to do replace ... by (rewrite some_lemma)?


view this post on Zulip Daniel Hilst Selli (Nov 09 2021 at 23:11):

Hi folds, I want to do something like this replace (m + n) with (n + m) by (rewrite add_comm), but this is not valid syntax. I would like to keep replace solution closer to the replace call

view this post on Zulip Notification Bot (Nov 09 2021 at 23:12):

Daniel Hilst Selli has marked this topic as resolved.

view this post on Zulip Notification Bot (Nov 09 2021 at 23:12):

Daniel Hilst Selli has marked this topic as unresolved.

view this post on Zulip Lessness (Nov 09 2021 at 23:19):

replace (m+n) with (n+m) by (rewrite add_comm; auto) works.

view this post on Zulip Lessness (Nov 09 2021 at 23:22):

But not sure if I understood the question correctly.

view this post on Zulip Ana de Almeida Borges (Nov 09 2021 at 23:45):

Yeah, whatever you put after by needs to actually solve the goal.
replace (n + m) with (m + n) by now rewrite add_comm. works as well (no need for the parentheses if there are no semicolons)

view this post on Zulip Daniel Hilst Selli (Nov 10 2021 at 03:31):

Ohh I tried with . instead of ;, thank you Lessness, and thank you Ana!

view this post on Zulip Notification Bot (Nov 10 2021 at 03:31):

Daniel Hilst Selli has marked this topic as resolved.

view this post on Zulip Daniel Hilst Selli (Nov 10 2021 at 03:33):

Not needing parentheses make it look nicer


Last updated: Feb 06 2023 at 12:04 UTC