問題タブ [induction]

わかりやすいように編集

特殊な種類の木の特性を証明しようとしています。このツリーは次のようなものです。問題は、Coq によって生成された誘導原理が、ツリーのプロパティを証明するには不十分であることです。より簡単な例として、次のタイプがすべての「ツリー」を表すとします。

次に、すべてのツリーの健全性を証明するには (含意など)、次の補題を証明する必要があります。

そのためには、ツリーの構造に帰納法を適用する必要があります。ただし、intros;induction H.そうすると、最初のサブゴールは(E,G,R |= f --> g)、必要な f と g の構造に関する情報が失われることです (必要です(E,G,R |= a --> a))。(また、帰納の場合、帰納仮説は と述べています(E,G,R |= f --> g)が、これは私には奇妙に思えます)。

私が試みた別のアプローチは(G |- f ---> g)、 f と g の構造を利用可能にしておくために を覚えておくことです。その後、証明は次のように進みます。intros;remember (G |- f --> g) as stmt in H.induction H.次に、基本ケースに期待するような目標と環境を取得します。ただし、ケース TRA を証明するために、次の証明コンテキストを取得します。

私は誘導仮説が

古いテキスト

特殊な種類の木の特性を証明しようとしています。このツリーは、21 の異なるルールを使用して構築できます (ここではすべてを繰り返しません)。問題は、Coq によって生成された誘導原理が、ツリーのプロパティを証明するには不十分であることです。

ツリーは次のように構築されます

これらのコンストラクタの 1 つが

私の目標は証明することです

makeStatement G f gそうしないと、f と g の構造に関する情報が失われるので、これを行うために覚えています。次に、ツリーに誘導を適用します。すべてのケースを個別の補題として証明しました。これは、基本ケースにうまく使用できます。ただし、帰納的なケースでは、Coq によって提示された帰納仮説は使用できません。

たとえば、前述の CTX コンストラクターの場合、次の帰納仮説が得られます。

私は使用できません。代わりに、次のようなものが欲しい

誰かがこれを修正する方法を私に説明できますか? これまでのところ、私は prv_tree で独自の誘導原理を定義しようとしましたが、これは同じ問題を引き起こすので、これは間違っていたのでしょうか?

私自身の誘導原理におけるCTXのステートメントは次のとおりです。

私たちは教室でプロローグを学び始めたばかりで、最初の演習は次のようになります。

問題：

注: a と b のようなアトムは無限にあるのではなく、2 つだけであると仮定します。

a) 命題論理式の帰納的定義を翻訳する (つまり、定義 1 を翻訳する) プロローグ プログラムを作成します。これには、次を使用する必要があります。

1.) 原子式を表す単項述語 "at" (つまり、"at(f)" は "F は原子式である" を意味します。ここで、f は定数です)。

2.) 式を示すための単項述語「fmla」(つまり、「fmla(F)」は「F は式である」を意味します)。

3.) 否定を表す単項演算「neg」(つまり、「neg(F)」は ¬F を表します)。

4.) 二項演算「or」は、2 つの式の論理和を表します (つまり、「or(F,G)」は (F∨G) を表します)。

試み：

有効な式の例: (~A v B) ---> or(neg(a), b)。

プログラムを構築した方法は正しいと思いますが、再帰部分は機能しません(シングルトンエラーも発生しています)。私はこれを何時間も理解しようとしましたが、役に立ちませんでした。どんな助けでも大歓迎です。

長さ「l」の文字列が含まれる配列「line」と、長さ「p」の文字列が含まれる配列「nl」があります。注: "l" と "p" は、対応する各配列の長さである必要はありません。パラメーター "at" は、挿入が "line" 内で行われる位置になります。再開: 長さ "p" の配列が "line" に挿入され、位置 (at,i,at+p),'p' の位置の間で "line" のすべての文字が右に移動して挿入されます。

保証の私のロジックは、「行」に挿入された要素が同じ順序であり、「nl」に含まれる文字と同じであるかどうかを確認することです。

コードは次のとおりです。

これが私が受け取っている エラーです。

ありがとう。

私は Dafny を使用して、あなたが受け取る削除メソッドを作成しています:

• 文字配列line

• 配列の長さl

• 位置at

• 削除する文字数p

最初に at から to までの行の文字を削除し、次にtoat + pの右側のすべての文字を移動する必要があります。at + pat

たとえば、[e][s][p][e][r][m][a]、 、at = 3、およびp = 3がある場合、最終結果は次のようになります。[e][s][p][a]

私は次のような意味のある事後条件を証明しようとしています:

ensures forall j :: (at<=j<l) ==> line[j] == old(line[j+p]);

at + p の右側からのすべての文字が新しい位置にあることを確認します。

しかし、Dafny は 2 つのエラーを出力します。

範囲外のインデックス 7 53

このリターン パスでは事後条件が保持されない可能性があります。19 2

rise4funのプログラムはこちら

質問：

basecase pであることを証明してくださいindstep p。forAllNat p

私が理解していないのは、 ifbasecase pと、もちろんindstep pそうforAllNat pあるべきだということです。True

私basecase pはそれP(0)が真実であると indstep p言い、P(Succ n)どちらが真実であると言い、それが真実であるかP(n+1)を証明する必要があると思いP(n)ます。私は正しいですか？これを行う方法について何か提案はありますか?

私は持っています: T(n) = T(n/2) + T(n/4) + T(n/8) + cn; c > 0。

これは私の誘導ステップです: T(n) が O(n) にあることを証明したい、つまり、いくつかの d > 0 および n0 であるため、すべての n > n0 および T(n) < dn

T(n) = T(n/2) + T(n/4) + T(n/8) + cn <= d(n/4) + d(n/4) + d (n/8) + cn = dn(7/8) + cn = dn(7/8) + cn <= dn ... = 8c <= d

私はベースケースで行き詰まりましたが、これは私の先生が私にそれを説明した方法です: n0 = 8 T(8) = T(4) + T(2) + T(1) + c8 <= 8T(4) + 8T(2) + 8T(1) + C8 < d8 を試してください。

誰かが私に基本的なケースを説明できますか? ありがとうございました！