Lean4依赖类型使用问题：Subtype.map报错与类型证明求助

问题代码与报错 #

原始代码 #

import Lean1.Basic

structure ArrayN (n : Nat) (α : Type) where
  array : { array : Array α // array.size = n }

class Hash (HashType: Type) where
  hashSize: Nat
  hash: x -> ArrayN (hashSize) UInt8

structure Private (Key: Type) (HashType: Type) [Hash HashType] where
  keys: ArrayN (Hash.hashSize HashType) Key

structure Public (HashType: Type) [Hash HashType] where
  hashes:
    let n := Hash.hashSize HashType
    ArrayN n (ArrayN n UInt8)

def Public.fromPrivate {K: Type} {HashType: Type} [Hash HashType] (priv: Private K HashType): Public HashType := {
  hashes := priv.keys.array.map (λ key => hash key)
}

报错信息 #

invalid field 'map', the environment does not contain 'Subtype.map'
priv.keys.array
has type
{ array // array.size = Hash.hashSize HashType }

解决方案 #

1. 访问ArrayN内部的Array #

ArrayN中的array字段是依赖类型子类型（Subtype），结构为{ val : α // p val }，需要通过.val访问内部的原始Array实例：

priv.keys.array.val  -- 得到原始的Array Key类型值

2. 证明转换结果符合Public类型要求 #

调用map后得到的是Array (ArrayN n UInt8)，需要将其包装为ArrayN n (ArrayN n UInt8)，核心是证明新数组的大小等于n：

• 原数组priv.keys.array.val的大小等于n（由ArrayN的子类型条件保证）
• Array.map不会改变数组大小，可通过Lean4标准库的Array.map_size定理验证：(arr.map f).size = arr.size

修正后的完整代码 #

import Lean1.Basic

structure ArrayN (n : Nat) (α : Type) where
  array : { array : Array α // array.size = n }

-- 修正Hash类的类型签名，明确hash函数的参数类型
class Hash (α : Type) where
  hashSize : Nat
  hash : α -> ArrayN hashSize UInt8

structure Private (Key: Type) [Hash Key] where
  keys: ArrayN (Hash.hashSize Key) Key

structure Public (Key: Type) [Hash Key] where
  hashes:
    let n := Hash.hashSize Key
    ArrayN n (ArrayN n UInt8)

def Public.fromPrivate {K: Type} [Hash K] (priv: Private K): Public K :=
  let n := Hash.hashSize K
  -- 1. 取出原始数组并调用map
  let mappedArray := priv.keys.array.val.map (λ key => Hash.hash key)
  -- 2. 证明map后的数组大小等于n
  let sizeProof : mappedArray.size = n := by
    rw [Array.map_size]
    exact priv.keys.array.property  -- 原数组的size等于n的证明
  -- 3. 构造ArrayN实例并返回Public结构
  { hashes := ⟨mappedArray, sizeProof⟩ }

关键说明 #

• 修正了Hash类的定义：将HashType改为通用类型参数α，明确hash函数接收α类型参数，符合类型推导逻辑
• 使用by tactic编写证明：通过rw [Array.map_size]引用数组map的大小不变性质，再利用原ArrayN自带的property（即array.size = n的证明）完成推导
• 用⟨mappedArray, sizeProof⟩直接构造Subtype实例，替代手动写{ val := ..., property := ... }的冗长写法

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