Lean4中为GetElem类生成NonEmptyList实例的问题咨询

核心原因：直接引用NonEmptyList.inBounds时的隐式参数与部分应用错误 #

1. 直接使用NonEmptyList.inBounds的类型矛盾 #

NonEmptyList.inBounds的完整类型为：

{α : Type} → NonEmptyList α → Nat → Prop

它需要依次接收：隐式类型参数α、NonEmptyList α实例、索引Nat，最终返回Prop。

在教材的实例声明中：

instance : GetElem' (NonEmptyList α) Nat α NonEmptyList.inBounds where
  getElem' := NonEmptyList.get

Lean会自动填充隐式的α参数，但此时错误地将实例的类型参数NonEmptyList α当成了NonEmptyList.inBounds的第一个显式参数（即xs : NonEmptyList α），导致NonEmptyList.inBounds被部分应用后，剩余类型变为Nat → Prop——这与GetElem'要求的NonEmptyList α → Nat → Prop完全不符，因此抛出类型不匹配错误。

2. λ表达式的修复逻辑 #

改用λ表达式后：

instance : GetElem' (NonEmptyList α) Nat α (λ coll idx => coll.inBounds idx) where
  getElem := NonEmptyList.get

• 这个λ表达式明确定义了一个二元函数，参数为coll : NonEmptyList α和idx : Nat。
• 通过点记法coll.inBounds访问时，Lean会自动从coll的类型中推导α参数，并将coll作为inBounds的第一个参数，最终整个λ函数的类型正好是NonEmptyList α → Nat → Prop，完美匹配GetElem'中inBounds参数的类型要求。

验证结果 #

修改后的实例可以正常通过测试：

#eval GetElem'.getElem idahoSpiders 0 (by decide) -- 输出 "Banded Garden Spider"
#eval GetElem'.getElem idahoSpiders 1 (by decide) -- 输出 "Long-legged Sac Spider"

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