natToFin gdy istnieją dowody na to, że konwersja będzie działać

Question

Funkcja natToFin ze standardowej biblioteki ma następujący podpis:

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

natToFin 4 5 powraca Just (FS (FS (FS (FS FZ)))) : Maybe (Fin 5), natomiast natToFin 5 5 zwrotów Nothing.

Chciałbym funkcję z następującym podpisem:

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

Zachowuje się tak samo jak standardowej funkcji lib ale nie musi zwracać Maybe ponieważ zawsze istnieje możliwość wygenerowania Fin n od m biorąc pod uwagę, że n jest większa niż m.

Jak mogę wdrożyć myNatToFin?

Answer 1

Można to zrobić bezpośrednio recursing na m, n, a dowody na n `GT` m w tym samym czasie:

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 

Uwaga że trzeba wzór spotkanie na p w drugim przypadku (choć jego wartość nie jest używana po prawej stronie), aby można było wprowadzić automatyczny argument dla wywołania rekursywnego.