coq - Coq：无法统一

Question

这里的学生，刚开始学习 Coq。我本质上是想证明 [] = a::l 其中 (a:A) 和 (l: list A) 是 False，解决所有子目标。我找到了一个名为 nil_cons 的漂亮 Coq 库函数，但在尝试应用它时出现错误。有人有建议吗？提前致谢！

错误信息在这里

证明尝试

标签： coqcoq-tactic

Answer 1

我不能确切地说出你试图证明的结果意味着什么，但nil_cons可能不是要走的路。False当您已经确定 时，该引理允许您推导出[] = a :: l。另一方面，您的目标希望您证明[] = a :: l假设一组不同的假设。