証明では(同様に) に単純化(negb (negb true))したいと思います。truefalse
Coq の手順は知っていますが、私の教科書では紹介されていないので、 ornegb_involutiveのみを使用して何とかその機能を模倣する必要があると思います。rewriteapply
1 に答える
4
アントンが言ったように、この目標を解決するための典型的な手順はreflexivity、またはその下位バージョンを使用することapply eq_reflです。
Coq はプログラミング言語に基づいていることを思い出してください。この場合、Python や C で返されるのと同じ方法で、実際に の実行~~ (~~ true)が簡単にわかりますtrue(ここでは を省略しています)。~~ x = negb xtrue
apply eq_reflCoqは、一致させるために結合するときに項を「計算」または「削減」しようとするため、目標を解決します。のタイプeq_reflはforall x, x = xであるため、が目標~~ (~~ true)に還元されると になり、解決することができます。この場合、あなたがそれを見るために目標を減らすだけですが、技術的には証明には必要ありません。truetrue = truesimpl
あなたの場合に適用するのは慣用的ではありませんnegb_involutive。この補題はnegb、のように への引数が変数の場合に役立ち~~ (~~ (~~ x)) = ~~ xます
rewrite平等を含むほとんどの目標で使用していることに気付くでしょう。
于 2016-11-14T17:54:12.687 に答える