如何在Coq中將negb true重寫爲false？

Question

如何重寫negb true到false在勒柯克？

我一直在尋找一個簡單的方法來重寫negb true到false庫。

但是，我還沒有找到任何有用的東西。

我知道simpl.，但我更喜歡更基本的語法。

Answer 1

您已經知道simpl確實會將negb true減少爲false。 這是因爲這兩個定義是等價的。

有了這些知識，你可以先證明你所需要的語句，然後用它改寫：

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

但更好的是，你可以使用replace做這一切在短短一行：

replace (negb true) with false by reflexivity. 

在這兩種情況下，反身將解決子目標negb true = false因爲雙方（如前面mentionned）definitionally等效。

Answer 2

當您搜索引號時，搜索引擎僅在導入的模塊中查找。

這就是爲什麼你需要先

Require Import Bool. 

然後

Search (negb _ = false). 

揭示了引理

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

可以使用引理重寫，如果你Require Import Setoid。

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

你，也許不希望使用simpl因爲你在某些方面和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 *)