Simple dependent type example in lean4

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)
}

The code above gives

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

I'm having a little problem working with dependent types. How can I proceed? I know I need to access the inner Array from ArrayN so it will have .map but I don't know how.

Also I probably need to prove that the returned result is the Public type, but I also don't know how

Solution

Building on my comment above, it is not too tricky to get your Public.fromPrivate method to work:

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
    ⟩
  } 
}

So to get the desired return type, you already made the right call of creating a record containing hashes but then we need to dig deeper. hashes is an ArrayN, for which we can again create a record { array := ... }. The thing that goes into the ... must of the Subtype { array : Array α // array.size = n }. We can create an object for this using the magic angle brackets (we could also use a record once again). First, we need to provide the value priv.keys.array.val.map (fun key => Hash.hash key), which is just a plain Array. Second, we need to provide a proof that .size of this array is really Hash.hashSize HashType but this is not hard to show and follows directly from the corresponding property of priv.keys.array after a bit of simplification. Actually simp will do nothing more than applying Array.size_map here.

Hope this helps! You can find the full example here.