完成证据与虚假假设在Coq

Question

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

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

Answer 1

这看起来并不像我从标准库使用的勒柯克列表，所以这将是很难帮助你不知道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. 

展开定义和工作的细节（可能保存此subproof作为引理如果它不存在，因为它似乎很有用）。