如何對Coq中的列表長度進行案例分析？

Question

我在證明的情況下需要對列表的長度進行案例分析l。

1. 當length l < 2這是一個情況下（其中像+二元運算不適用）
2. 當length l >= 2它的另一種情況（其中二元運算適用）

怎麼辦我使用destruct或其他一些策略來做到這一點，並獲得兩種情況，即True和False？

我想：

destruct (length l < 2). 

destruct (lt (length l) 2). 

remember (length l < 2). 
destruct HeqP. 

但沒有奏效。

Answer 1

您需要<的「建設性」版本，因爲標準版本是Prop，所以您無法對其執行案例分析。 您可以使用compare,le_lt_dec或<的布爾版本（通過文檔搜索所有選項，最簡單的應該是this one）。

如果你真的需要測試2的長度，你也可以3次破壞length n並手工處理3個第一種情況。

Answer 2

Vinz答案是正確的。當你需要考慮兩個你「知道不同」的案例時，通常是因爲它們是可判定的，所以尋找以_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