問題タブ [logical-foundations]

Coq について学ぶために、オンライン ブックの「Software Foundations」を使用しています。

第 2 章では、「plus_assoc」定理を証明するよう求められます。

以前に証明された 2 つの定理を使用します。

n の帰納法を使用して plus_assoc 定理を証明します。

この時点で、コンテキスト (*) は次のとおりです。

plus_comm を使用して取得したい

次に plus_n_sm

そして再び plus_n_sm

plus_comm を 2 回使用して証明を終了し、次に reflexivity を使用します。

ちょっとした質問は、plus_comm を (S n' + m) に適用する方法がわからないということです。

問題は、なぜ発行するのかということです。

即座に証明を終了します (与えられた文脈 (*) において) ?

明確にしていただきありがとうございます。

ファビアン・パイケ

回文の帰納的な定義は次のとおりです。

そして、 Software Foundationsから、私が証明したい定理:

証明の非公式な概要は次のとおりです。

が のような任意l0のリストであるとしl0 = rev l0ます。その場合、次の 3 つのケースのいずれかが成り立つ必要があります。l0もっている：

(a) ゼロ要素。この場合、定義により回文です。

(b) 1 つの要素。この場合、定義上は回文でもあります。

(c) 2つ以上のl0 = x :: l1 ++ [x]要素。xl1l1 = rev l1

からl1 = rev l1、次の 3 つのケースのいずれかが成立する必要があります...

l0再帰的なケース分析は、分析されたリストの長さが反復ごとに 2 ずつ減少するため、有限リストに対して終了します。任意の list で終了する場合、 回文の両端に 2 つの同一の要素を追加して作成されたリストも回文であるため、lnまでの外側のリストもすべて回文です。l0

その理由付けは正しいと思いますが、それを形式化する方法がわかりません。Coqで証明に変えられますか? 使用された戦術がどのように機能するかについてのいくつかの説明は、特に役立ちます。

apply ... with ...Pierce の「Software Foundations」から、戦術に関するいくつかの簡単な例を実行しようとしています。

本の例は私にはうまくいかないようです:

trans_eq_example'エラーで失敗しました:

Coq バージョンに関する追加情報:

このエラーを修正するにはどうすればよいですか?