简化假设 [英] Simplify assumption

问题描述

我想证明以下术语：

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以重写我的目标？

推荐答案

回答您的直接问题：

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

(1)仅使用simpl in A.(在simpl之后有关键字)。

(2)另一个变体是

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

---

(3)考虑OP中源代码中的第一个注释：

反身性。(*我不确定为什么这是可行的，但我假设是因为暗示*)

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

(4)我还应该注意到，您不必考虑4种可能的参数变体，因为andb在short-circuit style中定义了。 有关更多详细信息，请参阅this question。所以，使用问题中使用的策略，我将写下证明如下：

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

这篇关于简化假设的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！