Coqでnegb trueをfalseに書き換えるにはどうすればよいですか？

Question

Coqでnegb true〜falseを書き換えるにはどうすればよいですか？

私はfalseにnegb trueを書き換えるだけで方法のために図書館で検索してきました。

しかし、私は有用なものは何も見つかりませんでした。

私はsimpl.を知っていますが、より基本的な構文が好きです。

Answer 1

あなたはすでにsimplが実際にはnegb trueからfalseに減少することを知っています。 これは、2つが定義的に同等であるためです。あなたが最初にあなたが必要とする声明を証明することができ、この知識を用いて

、それを書き換える：

assert (H: negb true = false) by reflexivity. 
rewrite H. 

しかし、より良い、あなただけの1行でこのすべてを行うためにreplaceを使用することができます。

replace (negb true) with false by reflexivity. 

どちらの場合も、反射性はサブゴールnegb true = falseを解決します。なぜなら、両辺は（前述のように）定義的に同等であるからです。

Answer 2

補題を検索すると、検索エンジンはインポートされたモジュールのみを検索します。

Require Import Bool. 

その後

Search (negb _ = false). 

になぜ最初に必要です

はあなたがRequire Import Setoid場合は書き換えのための補題を使用することができます補題

negb_false_iff: forall b : bool, negb b = false <-> b = true 

を明らかにする。

Goal negb true = false. 
    rewrite negb_false_iff. reflexivity. Qed. 

あなたは、おそらく、それはあまりにも多くを展開し、大規模な読めない用語が作成されますので、あなたは、いくつかのコンテキストとsimpl台無しアップあなたの目標/仮説をでnegb trueを持っているのでsimplを使用する必要はありません。

simpl (negb true).  (* rewrites `negb true` to `false` in the goal *) 

または

simpl (negb true) in *. (* rewrites `negb true` in the goal and hypotheses *) 

：あなたは simplはこのようにそれを使用することによって適用されるコンテキストを絞り込むことができます