問題タブ [coq-tactic]

型の誘導原理は、命題に関する定理にすぎないと読みましたP。そこでList、正しい (または逆の) リスト コンストラクター に基づいて の誘導原理を構築しました。

誘導原理自体は次のとおりです。

しかし今、私は定理を使うのに苦労しています。induction戦術と同じことを達成するためにそれを呼び出す方法はわかりません。

たとえば、私は試しました：

しかし、最後の行で、私は得ました：

のようなカスタム誘導原理を定義して適用するための正しい手順は何list_ind_rconsですか?

ありがとう

exist私の質問は、条件/仮説のセットで用語を構築する方法に関連しています。

次の中間証明状態があります。

H0のおかげで、xが の証人であることはわかっているので(exists x : X, P x -> False)、名前を紹介したいと思います。

上記の推論に基づいて、それを とともに使用して、仮説でapply H in wを生成し、最後にを生成します。FalseinversionFalse

しかし、上記の証人を紹介するためにどの戦術/構文を使用すればよいかわかりませんw。これまでに到達できる最高のものはCheck (ex_intro _ (fun x => P x -> False) x H0)).、False.

誰かが存在条件を導入する方法、または証明を完了するための代替方法を説明できますか?

ありがとう。

PS定理全体を証明するために私が持っているのは次のとおりです。

idtacコマンドが成功した後にのみ、Ltac でメッセージを (? を使用して) 出力する方法はありますか? 何かのようなもの

これは、複数のサブゴールによって複数のメッセージが出力されることを除いて、ほとんど機能します。

最初の目標だけでフィルタリングするとうまくいくようです...

...そうでない場合を除いて：

おそらく両方のパターンを 1 つに組み合わせることができますが、100% のペナルティ ヒットにはあまり熱心ではありません。それでも、目標を完全に達成する戦術のケースは解決されません。

(私は主に 8.5 より前の Coq に対する回答に関心があります。8.5Infoなどではこれに適した機能が提供されているためです。それでも 8.5 であっても、特定の時点でのみデバッグ メッセージを出力できると興味深いでしょう)

私はCoq証明システムの初心者です（約4日）。一生懸命やってみたのですが、以下のことを証明できませんでした。

私の知る限り、+ の全単射性を証明する必要があるので、どうにかして を使用できますf(b) = f(c) -> b = c。これを行うにはどうすればよいですか?

以下に、さらに 3 つのサブゴールがある証明を示します。証明は、ここで示されている単純な算術言語での最適化の正しさについてplus 0です。は「算術式」であり、「算術評価」です。optimize_0plusaexpaeval

は次のoptimize_0plusとおりです。

私の戦争計画はoptimize_0plus、現在のサブゴールの LHS に適用し、以下を取得することです。

（しかし、Coqでこれを行う方法がわかりません）。

次に、 some を通じてsimpl、以下を取得します。

帰納法仮説を適用IHa1しIHa2、証明を完成させます。

私の質問は：

optimize_0plusCoq に の定義を1 回だけ適用し、それ以上もそれ以下も行わないようにするにはどうすればよいでしょうか?

私は試しましたが、それはあまりにも多くのことをしているように見えるsimpl optimize_0plus長いステートメントで何かを与えます. そして、補題を確立するために毎回タクティックmatchを使用するのは好きではありません。なぜなら、この計算は紙と鉛筆を使った正確な 1 ステップだからです。rewrite

ノート：

1.これは以前の質問 hereに関連していますが、使用に関する回答はここでは機能してsimpl XXXいないようです。これはより複雑なケースのようです。

2.元のウェブサイトは、機能する証拠を提供しています。a1しかし、そこにある証明は、用語などのケース分析を開始するため、必要以上に複雑であるように思われます.

したがって、私の関心事は、この単純な定理を実際に証明することではなく、紙の上で行うように直感的に証明する方法です。

- アップデート -

@gallais のおかげで、元の計画は変更される可能性があるため正しくありません

に

a1でない場合のみANum 0。この0ケースはdestruct a1.、注 2 で引用したコースの Web サイトと同様に、個別に処理する必要があります。

ただし、以下にリストされている他のケースについても同じ質問があり、元の計画はうまくいくはずです。

betaこれらの 5 つのケースのそれぞれについて、 の 1 つの適用 (削減??) により、たとえば ( に対して)optimize_0plusを変更できるように思われます。AMinus

に

、 右？

もしそうなら、どうすればこのワンステップの削減を行うことができますか?

追記：やってみた

そして、私は証明でaeval (AMinus (optimize_0plus a1) (optimize_0plus a2))a を使いたいと思っても得られませんでした。Eval

Coqでプルーフを読んだりテストしたりしています

特定の関数/定義は使用されないため、重要ではありません。いくつかのステップの後、定理は、内部の存在量指定子がユニバーサルに変更された形式に変換されます。

これは基本的に、

これは正確に逐語的に置き換えているわけではありませんが、ちょっと驚いていますexists i。forall iこの種の存在量指定子を普遍的なものに置き換えることは常に可能か、それともいつ可能になるのか疑問に思っていました. この変換の一般的なルール/テクニックは何ですか?

（スコーレミゼーションと呼ばれるものをぼんやりと覚えていますが、それを学習したときはよくわかりませんでした。）

Coq (8.4) で定理を変換する手順は次のとおりです。