Coq：我如何用“S n”替换“n + 1”这样的词？

对于使用reflexivity，我必须以某种方式将n + 1转换为(S n)。Coq：我如何用“S n”替换“n + 1”这样的词？

这应该是一个相当简单的转换，但我不知道如何告诉Coq做到这一点。

我该如何继续？

2016-11-15 user111854

可能的重复[如何重写“+ 1”（加一）到“S”（succ）在Coq？]（http://stackoverflow.com/questions/40313702/how-can-i-rewrite -1加1到s-succ-in-coq） – gallais

'1 + n'通过归一化等于'S n'，所以如果你有一个证明加法的交换性的引理，你可以去'n + 1'=>'1 + n' =>'S n'。 – Cactus

由于它们不相等，只是等价，您可以使用replace (n + 1) with (S n)这将要求您证明这一事实。或者，您可以使用rewrite以及来自标准库的正确引理，即add_1_r iirc。

来源

2016-11-15 16:00:57 Vinz

那么我将如何证明0 +（S j）=（S j）？ – user111854

这应该可以直接使用'reflexivity'来证明：'+'的定义是通过对第一个参数进行递归完成的，所以这里Coq知道如何在不重写的情况下将'0 + foobar'简化为'foobar'。你最初的问题是你想重写'n + 1'，而不是'1 + n'。为了证明'1 + n'等于'S n'，你不需要做任何事情，这正是定义。 – Vinz

Coq：我如何用“S n”替换“n + 1”这样的词？

回答

相关问题