gpt4 book ai didi

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

转载 作者:行者123 更新时间:2023-12-04 09:42:13 37 4
gpt4 key购买 nike

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

但是如果我从具有 bool 函数的假设开始,我无法弄清楚如何解决。

最佳答案

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

关于coq - 如果 (andb b c = orb b c) 在 coq 中,我将如何证明 b = c?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/32292029/

37 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com