CODEWITHSUNDEEP
functional-programmingcoq
Shuzheng
Shuzheng

Reputation: 14018

Coq: How do I replace terms like "n + 1" with "S n"?

For using reflexivity, I must somehow transform n + 1 to (S n).

This should be a rather simple transformation, but I don't know how to tell Coq to do it.

How do I proceed?

Upvotes: 2

Views: 737

Answers (1)

Vinz
Vinz

Reputation: 6057

Since they are not equal, just equivalent, you can use replace (n + 1) with (S n) which will ask you to prove that fact. Or you can use rewrite with the correct lemma from the std lib, which is add_1_r iirc.

Upvotes: 4

Related Questions