lean4 中的简单依赖类型示例

Question

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 }

我在处理依赖类型时遇到了一些问题。我该如何继续？我知道我需要从

ArrayN

访问内部数组，所以它将有

.map

但我不知道如何。

另外我可能需要证明返回的结果是Public类型，但我也不知道如何

Answer 1

根据我上面的评论，让你的

Public.fromPrivate

方法发挥作用并不是太棘手：

def Public.fromPrivate {K: Type} {HashType: Type} [Hash HashType] (priv: Private K HashType): Public HashType := {
  hashes := { 
    array := ⟨
      priv.keys.array.val.map (fun key => Hash.hash key),
      by simp; exact priv.keys.array.property
    ⟩
  } 
}

因此，为了获得所需的返回类型，您已经正确调用了创建包含

hashes

的记录，但我们需要更深入地挖掘。

hashes

是一个

ArrayN

，我们可以再次为其创建一条记录

{ array := ... }

。进入

...

的东西必须是

Subtype

{ array : Array α // array.size = n }

。我们可以使用魔术尖括号为此创建一个对象（我们也可以再次使用记录）。首先，我们需要提供值

priv.keys.array.val.map (fun key => Hash.hash key)

，它只是一个普通的

Array

。其次，我们需要提供一个证明，证明这个数组的

.size

确实是

Hash.hashSize HashType

，但这并不难证明，并且在经过一些

priv.keys.array

化之后，可以直接从

simp

的相应属性得出。实际上

simp

只会在这里应用

Array.size_map

。

希望这有帮助！ 您可以在此处找到完整示例。