Stream: Coq users

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

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

Notification Bot (Nov 09 2021 at 23:12):

Daniel Hilst Selli has marked this topic as resolved.

Notification Bot (Nov 09 2021 at 23:12):

Daniel Hilst Selli has marked this topic as unresolved.

Lessness (Nov 09 2021 at 23:19):

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

Lessness (Nov 09 2021 at 23:22):

But not sure if I understood the question correctly.

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)

Daniel Hilst Selli (Nov 10 2021 at 03:31):

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

Notification Bot (Nov 10 2021 at 03:31):

Daniel Hilst Selli has marked this topic as resolved.

Daniel Hilst Selli (Nov 10 2021 at 03:33):

Not needing parentheses make it look nicer

Last updated: Oct 04 2023 at 19:01 UTC