如何在Idris2中生成可判定的LTE不等式证明并截取列表前n元素？

核心思路是借助Idris的依赖类型证明，通过decide生成LTE n (length xs)的决策结果（存在证明/不存在证明），分支处理实现安全截取：

1. 基础实现（返回Maybe） #

这个版本会在列表长度不足时返回Nothing，足够时返回截取后的Vect n a：

takeN : List a -> Nat -> Maybe (Vect n a)
takeN xs n = 
  let len = length xs
  in case decide (LTE n len) of
       Yes prf => Just (take n (fromList xs) {prf})
       No _ => Nothing

关键细节解释 #

• decide (LTE n len)：自动生成LTE n len的决策结果，返回Dec (LTE n len)类型，即Yes (prf : LTE n len)（存在n≤len的证明）或No (contra : LTE n len -> Void)（不存在该证明）。
• fromList xs：因为已知列表长度为len，可以安全转换为Vect len a，Idris能自动推导这个长度匹配的证明。
• take n ... {prf}：Vect的take函数需要证明截取长度n不超过原Vect长度，这里传递prf : LTE n len满足依赖类型约束，保证操作安全。

2. 带错误信息的版本（返回Either） #

如果需要明确返回错误原因，可改用Either类型：

takeN' : List a -> Nat -> Either String (Vect n a)
takeN' xs n = 
  let len = length xs
  in case decide (LTE n len) of
       Yes prf => Right (take n (fromList xs) {prf})
       No _ => Left $"List length ({show len}) is less than {show n}"

3. 依赖类型约束的严格版本 #

如果希望函数仅接受长度≥n的列表，可以将证明作为显式参数，确保调用时必须满足条件：

takeNProof : (xs : List a) -> (n : Nat) -> (prf : LTE n (length xs)) -> Vect n a
takeNProof xs n prf = take n (fromList xs) {prf}

调用时可通过decide生成证明分支处理：

example : Vect 3 Int
example = 
  case decide (LTE 3 (length [1,2,3,4])) of
    Yes prf => takeNProof [1,2,3,4] 3 prf
    No _ => impossible  -- 已知列表长度为4≥3，该分支不会触发

内容的提问来源于stack exchange，提问作者thor