coq - 在 Coq 中用假假设完成证明

Question

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

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

Answer 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.

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