如何对Coq中的列表长度进行案例分析？

Question

在证明过程中，我需要对列表l的长度进行案例分析。

1. 当使用length l < 2时，只有一种情况(在这种情况下，像+这样的二进制操作不适用)
2. 如果是length l >= 2，则是另一种情况(在这种情况下，应用二进制操作)

我如何使用destruct或其他一些策略来做到这一点，并获得两个情况，即真假？

我试过：

destruct (length l < 2).

destruct (lt (length l) 2).

remember (length l < 2).
destruct HeqP.

但都没起作用。

Answer 1

您需要一个“建设性”版本的<，因为标准版本在Prop中，所以不能对其执行案例分析。您可以使用compare、le_lt_dec或布尔版本的< (在文档中搜索所有选项，最简单的选项应该是这一个)。

如果您真的需要针对2测试长度，您还可以销毁length n 3次，并手动处理前3种情况。

Answer 2

文兹的答案是对的。当您需要考虑两个“知道不同”的情况时，通常是因为它们是可判定的，所以寻找以_dec结尾的引理。在本例中，lt_dec是在Compare_dec中定义的，您在导入Arith时会得到它。所以：

Require Import Arith.

Goal forall (l:list nat), True.

intro. destruct (lt_dec (length l) 2).

现在第一个目标是

l : list nat
l0 : length l < 2
============================
 True

第二个目标是

l : list nat
n : ~ length l < 2
============================
 True