Coq：「n + 1」などの用語を「S n」に置き換えるにはどうすればよいですか？

reflexivityを使用するには、どういうわけかn + 1を(S n)に変換する必要があります。Coq：「n + 1」などの用語を「S n」に置き換えるにはどうすればよいですか？

これは簡単な変換であるはずですが、私はCoqにそれを行う方法を知らない。

どうすればいいですか？

2016-11-15 user111854

Coqの "S"（succ）に "+ 1"（+ 1）を書き換えるにはどうすればいいですか？]（http://stackoverflow.com/questions/40313702/how-can-i-rewrite -1 + 1-to-s-succ-in-coq） – gallais

'1 + n'は正規化によって' S n 'に等しくなるので、追加の可換性を証明する補題があれば 'n + 1 '=>' 1 + n '=> 'S n'である。 – Cactus

等価ではないので、等価であるので、replace (n + 1) with (S n)を使用すると、その事実を証明するように求められます。あるいは、rewriteをstd libの正しい字句と一緒に使うことができます。これはadd_1_r iircです。

出典

2016-11-15 16:00:57 Vinz

どうすれば0 +（Sj）=（Sj）を証明できますか？ – user111854

これは 'reflexivity'を使って直接的に証明できるはずです。' + 'の定義は最初の引数の再帰によって行われるので、ここでCoqは' 0 + foobar'を書き直すことなく 'foobar'に単純化する方法を知っています。あなたの最初の質問の問題は、 '1 + n'の代わりに' n + 1'を書き直したいということです。 '1 + n'が' S n'に等しいことを証明するために、何もする必要はありません。それはまさに定義です。 – Vinz

Coq：「n + 1」などの用語を「S n」に置き換えるにはどうすればよいですか？

答えて

関連する問題