代码之家 › 专栏 › 技术社区 › Albtzrly

如果(and b b c=orb b c)在coq中,我如何证明b=c?

proof-of-correctness proof coq

Albtzrly · 技术社区 · 9 年前

我是coq的新手,我想证明这一点。。。

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

这是我的证明,但当我到达目标时,我会陷入困境(false=true->false=true)。

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.

但是,如果我从具有布尔函数的假设开始,我就不知道如何解决。

3 回复 | 直到 9 年前

larsr 9 年前

你不需要诱导,因为 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.

Matt 9 年前

您需要使用 intro 策略这会移动 false = true 作为一个假设,您可以使用它来重写。

thor BabarQB 9 年前

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

在台阶处 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 如果 对称性 将使用以下方法使其匹配:

try (symmetry;assumption); try assumption.

(真正了解Coq的人可能会启发我如何 尝试 这更简洁)

将其放在一起:

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 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.

第一种方法更麻烦,但它不涉及枚举所有真值表行(我认为)。