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」這樣的詞？

回答

相關問題