如何在 coq 中证明 b = c if (andb b c = orb b c) ？

Question

我是 coq 新手，我正在努力证明这一点......

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

您可以使用

rewrite

和 [bool][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.

（真正了解 Coq 的人可能会启发我如何更简洁地

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.

。这又给出了四个微不足道的含义，最多一个

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.

第一种方法比较麻烦，但它不涉及枚举所有真值表行（我认为）。

Answer 4

这是我的解决方案：

Theorem andb_eq_orb :
  forall (b c : bool),
  (andb b c = orb b c) -> b = c.
  Proof.
    intros b c.
    destruct b as [|].
    - simpl.
      intros H.
      rewrite <- H.
      reflexivity.
    - simpl.
      intros H.
      rewrite -> H.
      reflexivity.
    Qed.

仅使用

rewrite

和

destruct

。

由于某些原因，如果我把

intros H

放在

destruct

之前，

simpl

不会对第一臂引入的

true && c = true || c

部分生效。