Lean 4.12中《Lean函数式编程》非空列表示例报错：未解决目标

你遇到的问题是Lean 4版本迭代中simp策略默认规则的调整导致的：在Lean 4.1中，simp会自动展开数组（Array）的length定义并计算具体值，但到了4.12版本，默认的简化规则不再包含这一步，所以无法自动完成证明。

以下是几种可行的解决方式：

1. 使用rfl策略 #

rfl可以直接证明由计算得出的等式或不等式，因为xs.length是可计算的具体值，rfl能直接确认[1].length = 1，进而证明1 > 0：

def xs := [1]
theorem xs_not_empty : xs.length > 0 := by rfl

2. 使用decide策略 #

decide会自动判定可计算命题的真假，适合这类简单的数值不等式证明：

def xs := [1]
theorem xs_not_empty : xs.length > 0 := by decide

3. 显式指定simp展开Array.length #

如果坚持想用simp，可以显式把Array.length加入简化规则，让simp展开长度定义并计算：

def xs := [1]
theorem xs_not_empty : xs.length > 0 := by simp [Array.length]

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