問題タブ [coq-tactic]

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

0 投票する
2 に答える
1187 参照

coq - 差別的な戦術はどのように機能しますか?

discriminate舞台裏で戦術がどのように機能するのか興味がありました。したがって、私はいくつかの実験を行いました。

最初に単純な帰納的定義:

discriminate次に、戦術によって証明できる簡単な補題:

証明がどのように見えるか見てみましょう:

これはかなり複雑に見えますが、ここで何が起こっているのかわかりません。したがって、同じ補題をより明示的に証明しようとしました。

Coqがこれで何を作ったかをもう一度見てみましょう:

今、私は完全に混乱しています。これはさらに複雑です。ここで何が起こっているのか誰でも説明できますか?

0 投票する
2 に答える
200 参照

coq - COQ での 2 つの再帰関数の展開を含む証明

私は Coq の学習を開始し、かなり単純に見えることを証明しようとしています: リストに x が含まれている場合、そのリスト内の x のインスタンスの数は > 0 になります。

次のように、contains 関数と count 関数を定義しました。

私は証明しようとしています:

証明にはcountとcontainsの定義を展開することが含まれることを理解していますが、「containsがtrueであるため、リストをnilにすることはできません。そのため、trueである要素が存在する必要があります」と言いたいxです。少し遊んでみましたが、戦術を使ってこれを行う方法がわかりません。ガイダンスをいただければ幸いです。lbeq_nat h x