coq - 如何将 A = B -> C = D 形式的 Coq 假设应用于 A = B 形式的子目标

Question

我正在做一个证明，我目前被困在这个问题上。我有一个假设，内容如下：

T1E : tree1 = EmptyTree -> isEmpty (leftChild (Node tree1 tree2)) = true

我也有一个假设：

H2 : isEmpty (leftChild (Node tree1 tree2)) = true

我目前的子目标是

tree1 = EmptyTree

看来我应该能够做到

rewrite <- T1E

为了将子目标更改为

isEmpty (leftChild (Node tree1 tree2)) = true

但是当我尝试这样做时，Coq 说

Error: Found no subterm matching "true" in the current goal.

如何使用 T1E 和 H2 证明我当前的子目标？

Answer 1

您可能无法使用T1E. 本质上，您试图证明A知道“如果A为真，B则为真”。

但是，查看您的上下文，在我看来，您应该能够简化H2并获得关于 的矛盾或更多信息tree1，无论如何这应该会产生您想要的结果。