如何證明b = c if（andb b c = orb b c）in coq？

Question

我是新來的輔酶Q，我試圖證明這一點......

Theorem andb_eq_orb : 
    forall (b c : bool), 
    (andb b c = orb b c) -> (b = c). 

這是我的證明，但我碰到困難時，我得到的目標（假=真 - >假=真）。

Proof. 
intros b c. 
induction c. 
destruct b. 
reflexivity. 
simpl. 
reflexivity. 

我不知道如何重寫該表達式，所以我可以使用反身性。但即使我這樣做，我也不確定它會導致證明。

我能夠解決證明，如果我開始與假設b = c雖然。即...

Theorem andb_eq_orb_rev : 
    forall (b c : bool), 
    (b = c) -> (andb b c = orb b c). 
Proof. 
intros. 
simpl. 
rewrite H. 
destruct c. 
reflexivity. 
reflexivity. 
Qed. 

但我不知道如何解決如果我開始與具有布爾函數的假設。

Answer 1

您不需要歸納，因爲bool不是遞歸數據結構。只需通過b和c的值的不同情況。使用destruct來做到這一點。在兩種情況下，假設H將是true = false類型，您可以使用inversion H完成證明。在另外兩種情況下，目標將是true = true型，可以通過reflexivity來解決。

Theorem andb_eq_orb : forall b c, andb b c = orb b c -> b = c. 
Proof. destruct b,c; intro H; inversion H; reflexivity. Qed. 

Answer 2

你會想要使用intro策略。這會將false = true移動到您的證明背景中，作爲您可以用來重寫的假設。

Answer 3

這可能不是最有效的方法。

在步驟induction c.（其中它的卡住）：

______________________________________(1/2) 
b && true = b || true -> b = true 
______________________________________(2/2) 
b && false = b || false -> b = false 

可以使用在[BOOL] rewrite和基本定理[1]，以簡化的術語如b && true到b，和b || true到true。

這可以將其降低到兩個「微不足道」的子目標：

b : bool 
______________________________________(1/2) 
b = true -> b = true 
______________________________________(2/2) 
false = b -> b = false 

這是使用assumption幾乎微不足道的證據，但它是一個symmetry路程。您可以try如果symmetry會使他們配合使用：

try (symmetry;assumption); try assumption. 

（有人誰真正知道勒柯克可以賜教如何try這個更簡潔）

將其組合在一起：

Require Import Bool. 
Theorem andb_eq_orb : forall b c, andb b c = orb b c -> b = c. 
Proof. 
destruct c; 

try (rewrite andb_true_r); 
try (rewrite orb_true_r); 
try (rewrite andb_false_r); 
try (rewrite orb_false_r); 
intro H; 
try (symmetry;assumption); try assumption. 
Qed. 

一第二種方法是蠻力並使用「真值表」方法。這意味着你可以將所有變量分解爲它們的真值，並簡化爲：destruct b, c; simpl.。這再次給了4個瑣碎的影響，最多一個symmetry到try：

4 subgoal 
______________________________________(1/4) 
true = true -> true = true 
______________________________________(2/4) 
false = true -> true = false 
______________________________________(3/4) 
false = true -> false = true 
______________________________________(4/4) 
false = false -> false = false 

將其組合在一起：

Theorem andb_eq_orb1 : forall b c, andb b c = orb b c -> b = c. 
Proof. 
destruct b, c; simpl; intro; try (symmetry;assumption); try assumption. 
Qed. 

第一種方法是比較麻煩的，但它不涉及枚舉所有的真理錶行（我認爲）。