natToFin quando ci sono prove che la conversione funziona

Question

La funzione natToFin dalla libreria standard ha la seguente firma:

natToFin : Nat -> (n : Nat) -> Maybe (Fin n) 

natToFin 4 5 rendimenti Just (FS (FS (FS (FS FZ)))) : Maybe (Fin 5), mentre natToFin 5 5 rendimenti Nothing.

Vorrei una funzione con la seguente firma:

myNatToFin : (m : Nat) -> (n : Nat) -> { auto p : n `GT` m } -> Fin n 

Si comporta come la funzione lib standard, ma non ha bisogno di restituire un Maybe perché è sempre possibile generare un Fin n da m dato che n è maggiore di m.

Come si implementa myNatToFin?

Answer 1

Puoi farlo direttamente recursing su m, n, e la prova per n `GT` m allo stesso tempo:

import Data.Fin 

myNatToFin : (m : Nat) -> (n : Nat) -> {auto p : n `GT` m} -> Fin n 
myNatToFin Z (S n) = FZ 
myNatToFin (S m) (S n) {p = LTESucc _} = FS $ myNatToFin m n 

Nota che è necessario pattern match sul p nel secondo caso (anche se la sua valore non viene utilizzato sul lato destro) in modo che l'argomento automatico per la chiamata ricorsiva può essere compilato.