コック：？「書き換え」または「適用」を使用して、真の簡素化（NEGB（neqb真）証明で

Question

が、私は(negb (negb true))）も同様にfalseと（trueにを簡素化したい

私はコックのnegb_involutive手順を知っています、。しかし、私の教科書は、それを導入していないので、私は私が何とかのみrewriteまたはapplyを使用してその機能を模倣するために管理する必要があることだと思う。

Answer 1

アントンは、この目標を解決するための典型的な手順はreflexivityを使用することで、またはそのう、言ったように下位バージョンapply eq_refl。

コックは、（私は ~~ x = negb xを省略する場合）プログラミング言語に基づいており、この場合、実際 ~~ (~~ true)の実行が容易 trueあると見られている、同じように、それは、PythonまたはC

で true

を返すこと

リコールapply eq_reflは、Coqが条件を一致させるために結びつけるときに用語を「計算する」または「減らす」ことを試みるため、目標を解決します。 eq_reflのタイプはforall x, x = xなので、~~ (~~ true)をtrueに減らすと、あなたの目標はtrue = trueになり、解決できます。この場合、simplはあなたの目に見える目標を減らすだけですが、証明には技術的には必要ありません。

negb_involutiveを適用するのは慣用ではありません。negbの引数が~~ (~~ (~~ x)) = ~~ xのような場合、この補助定法は便利です。

rewriteを使用すると、ほとんどの目的が同等であることがわかります。