Casting

[pharringtonp19]

I am defining a vector that specifies the number of nodes for each layer of a feed-forward neural network. Are there any potential issues with using unsafe_i_to_n in this way?

def VecNodes (depth: Nat) (features: Nat) (width: Nat) : ((Fin depth) => Nat) = 
    for i:(Fin depth). case (ordinal i == 0 || ordinal i == unsafe_i_to_n ((n_to_i depth) - 1)) of
        True -> case (ordinal i == 0) of 
            True -> features
            False -> 1
        False -> width

nodes = VecNodes 3 12 32 
:t nodes 
((Fin 3) => Nat)

[axch]

No, but the proof is a little subtle: if Dex executes unsafe_i_to_n ((n_to_i depth) - 1), it must be the case that depth > 0, because otherwise the enclosing for would never run. Ergo, (n_to_i depth) - 1 is non-negative, so we have discharged the proof obligation imposed by unsafe_i_to_n.

That said, why not just avoid this situation by computing ordinal i + 1 == depth instead?

[pharringtonp19]

@axch Thanks! Much simpler