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

展开定义并计算出详细信息(如果它不存在,可能会将此子证据保存为引理,因为它似乎很有用).