問題タブ [coq-tactic]

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

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

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

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

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

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

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

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

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

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

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