問題タブ [induction]

次のステートメントのいくつかを証明する方法を完全に理解するのに問題があります。

たとえば、次のステートメントがありますn^2logn = O(n^2)。私が間違っている場合は訂正しn^2てbigOくださいn^2logn。n^2よりも速く成長することを意味しn^2lognます。では、これを証明するにはどうすればよいでしょうか。私は、使用しようとしたがその過程で立ち往生した帰納法による証明を使用する必要があると思います。このステートメントを次のように書き直してもらえn^2logn <= n^2ますか?

帰納法を使って何かを反証することは可能ですか? たとえば、反証n!=O(n^n)。それとも、任意の値 (2 より大きいとしましょう) がステートメントを満たさないことを単に示すことによって、ステートメントを反証することは有効ですか?

そして最後に、明確にするために、bigTheta は、正しく成長する場合、方程式は同等であると述べていますか?

問題は、「強い帰納法を使って、2 つ以上の偶数の和が偶数であることを示す」です。さて、普通の誘導でいいのですが、強い誘導の表記に迷ってしまいました。これまでのところ、私は持っています：

BASE: (偶数として 2 を使用します)

シーケンス定義による n=2、A2 = 4 (偶数)

シーケンス定義による n=3、A3 = 6 (偶数)

したがって、P(2) と P(3) が得られます。

ここからどこへ行くべきかわかりません。誰かが私を正しい方向に導くことができれば、それは素晴らしいことです

帰納的述語をどのように説明しますか? それらは何に使用されますか？それらの背後にある理論は何ですか？それらは依存型システムにのみ存在しますか、それとも他のシステムにも存在しますか? それらは何らかの形で GADT に関連していますか? Coqでデフォルトでtrueになっているのはなぜですか?

これは Coq の例です。

この定義をどのように使用しますか? それはデータ型ですか、それとも命題ですか？

不変: 3 行目のループ ガードを評価する直前に、右端の d 桁を削除した n は val と同じです。(数値 0 は、書き出すのに 0 桁が必要であり、書き出すのに 0 桁を必要とする唯一の数字である と仮定します)。

ループ不変式が成り立つことを帰納法を使って証明してください。

今私は常に、帰納法による証明は、方程式内の変数を k で置き換えることによって真になると仮定し、k+1 も真になることを証明しなければならないと常に考えてきました。しかし、私はこの質問で実際に方程式を与えられているわけではなく、コードのブロックだけを与えられています。これが私の基本ケースです：

3 行目のループ ガードを評価する直前では、d は 0 に等しく、2 行目では val == n であるため、n の右端の 0 桁が削除された場合、それは val です。したがって、基本ケースが成り立ちます。

k+1 を証明する方法がわからないので、この後の帰納的ステップの書き方がよくわかりません。

AVL ツリーのノードの最小数を証明するこの ( http://condor.depaul.edu/ntomuro/courses/417/notes/lecture1.html ) ペーパーを読んでいたところです。ただし、O(log n) はノード数をまったく参照していないため、結果の意味がわかりません。これはどのように証明できますか？ただし、最初のステップと、反復がどのように単純化されるかは理解しています。しかし、4番目のステップの後、私は彼が何をしているのか正確に理解できていません（漠然と想像することはできますが）. 最後の数行が何を証明しているか、パート 1 の最後で彼がどのように式を単純化しているか、誰か説明してくれませんか?

ありがとう

ご存じのとおり、新しい型システムを定義するには、次の方法が必要です。

1. 言語構文
2. 入力規則

そして、上記の型付け規則を使用して証明できると思われるいくつかの定理を証明する必要があります。これらの定理を証明するために、1 つの方法は帰納法 (規則帰納法) を使用することです。

たとえば、次のようなシステムがあります。

そして、次のように「Zero」と「Succ」の 2 つのルールを定義します。

次に、定理を提案し、この定理が正しいと信じ、それを証明する必要があります。

この定理は、定義されたルールを使用して簡単に証明できます。それはルール誘導と呼ばれます。

ルール誘導の練習に役立つ情報源を知っている人はいますか?

自然数の偶数性の帰納的および計算上の定義は次のとおりです。

そして、一方が他方を暗示しているという証拠。

最初はこの証明についてあまり考えていませんでしたが、よく見ると厄介なことがわかりました。問題は、reflexivityステップの後にコンテキストが表示されることを期待していることです

しかし、私が実際に得るのは代わりに

定理はそのまま証明可能ですが、仮説が不思議なことに消えていくのを見るのは気がかりです。最初に期待したコンテキストを取得する方法を知りたいです。Web 検索から、これは Coq で構築された項に対する帰納法に関する一般的な問題であることを理解しています。SO に関する提案された解決策の 1 つはremember、仮説を保持するための戦術を使用することを提案しています。しかし、この証明でそれを試すと、

ステップで次のエラー メッセージが表示されますinduction。

私にはよくわかりません。問題は自由変数があることだと思いますが、その場合、も導入せずEに導入する方法がないため、行き詰まります。（それで一般化します）Engeneralize dependent nE

最初に予想されるコンテキストを取得する方法はありますか?