0

我在证明期间处于需要对列表长度进行案例分析的情况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.

但没有一个奏效。

4

2 回答 2

2

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

如果您确实需要针对 2 测试长度，您还可以破坏length n3 次并手动处理前 3 个案例。

于 2015-12-01T10:39:32.270 回答
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
于 2015-12-01T19:58:35.620 回答