简化假设

Question

我想证明以下术语：

Goal forall x y, andb x y = true -> x = true.

相当于

Goal forall x y, ((andb x y) = true) -> (x = true).

因此，我在纸上的方法是检查 x 和 y 的所有选项，并表明只要左侧为真 (true = true)，右侧也为真 (true = true) , 这将满足蕴涵的要求。

Proof.
  intros x y A. destruct x.
  - destruct y.
    + reflexivity.
    + reflexivity. (*I am not certain why this works but I assume due to the implication*)
  - destruct y.
   (* here I am lost*)
Qed.

我需要简化假设，因为目前有 A:(false && true)%bool = true 和 && 的评估，并且会产生 false，因此，A:false = true 和我可以重写目标以显示 false = false，这可以用 reflexivity 解决。但是使用 simpl A. 会产生 Error: Cannot coerce A to an evaluable reference. 而直接 rewrite A 会产生 Error: Found no subterm matching "(false && true)%bool" in the current goal.

如何将我的假设 A 从 (false && true)%bool = true 简化为 false = true 以重写我的目标？

Answer 1

回答你的直接问题：

How can I simplify my assumption A from (false && true)%bool = true to false = true to rewrite my goal?

(1)就用simpl in A.([=15=后面有关键字"in" ]).

(2) 另一种变体是

rewrite <- A. (* notice the arrow which shows rewriting direction *)
reflexivity.  (* this will also perform simplification *)

(3) 考虑到 OP 中源代码中的第一条评论：

reflexivity. (* I am not certain why this works but I assume due to the implication *)

该行之所以有效，是因为 true = true（查看目标），就像在第一个子目标中一样。您实际上不需要对第二个参数进行结构化（在这种情况下 x = true 并且（非正式地）您已经证明了您的目标），但是由于您这样做 destruct y. 您需要证明 true = true两次，因此需要使用 reflexivity 两次。

(4) 我还应该注意到您不必考虑参数的 4 种可能变体，因为 andb 是在 [=24= 中定义的]. 有关更多详细信息，请参阅 this question。所以，利用题目中已经用到的技巧，我将证明写成如下：

intros x y A.
destruct x.
  - reflexivity.                         (* x = true *)
  - simpl in A. rewrite A. reflexivity.  (* x = false *)

简化假设

Simplify assumption

coq