問題タブ [logical-foundations]

これが私が得たものです：

私は前の定理を証明しました：

H1に適用したかったのですが、

エラーが発生します：

式に「m」が見つからないのはなぜeven (n + m)ですか? 直し方？

アップデート

非常に奇妙な結果が得られます。

H1から2への仮説を変換すると思いました：

しかし、代わりに 2 つのサブゴールが与えられました。証明する必要がある 2 番目のサブゴールは、最初のものよりも複雑です。

ここで何が起こっているのですか？

次の補題を証明しようとしています。

最後に得たものは次のとおりです。

coq で "even 0" を true に、"even 1" を false に評価するようにします。を試しましsimplたapply ev_0 in H.が、エラーが発生します。何をすべきか？

これまでに得たものは次のとおりです。

ここで、H1 と H2 を結合するかexists s : list T, s =~ App re1 re2、ゴールを 2 つのサブゴールに分解し、H1 と H2 を使用してそれらを別々に証明する必要があります。しかし、私はそれを行う方法がわからない。