在 Coq 中用假假设完成证明答案

【问题标题】：Finish proof with false hypothesis in Coq在 Coq 中用假假设完成证明
【发布时间】：2012-07-07 01:39:15
【问题描述】：

所以我在子目标中有一个错误的假设。这是不同构造函数之间的相等性。如何完成子目标？

H: List.Not_Empty Bit.Bit Bit.Zero (List.Empty Bit.Bit) = List.Empty Bit.Bit

【问题讨论】：

标签： coq theorem-proving

【解决方案1】：

这看起来不像我习惯的标准库中的 Coq 列表，因此如果不知道 List.Not_Empty 和 List.Empty 的定义，将很难为您提供帮助。如果我猜对了List.Empty 代表nil 和List.Not_empty 代表cons，那么这只是表明两个构造函数不相等的问题。例如，您可以这样做：

congruence.

或者简单地说：

inversion H.

但是，如果涉及更多内容，这两个可能会失败。所以你想要：

SearchAbout List.Not_Empty.

查看是否存在关于它的引理，或者：

unfold List.Not_Empty, List.Empty in H.

展开定义并计算出细节（如果该子证明不存在，可能会将其保存为引理，因为它看起来很有用）。

【讨论】：

inversion H 成功了。 Empty 和 Not_Empty 只是我的 List 的构造函数。