Вспомогательная функция для определения, если Nat `mod` 5 == 0

Question

xash предоставил мне полезный ответ на функцию "Определить, может ли Nat делиться на 5 во время компиляции" (которую я переименовал из своего исходного длинного имени):

onlyModBy5 : (n : Nat) -> n `modNat` 5 = 0 -> Nat
onlyModBy5 n prf = n

Предыдущий ответ научил меня, как запустить его на REPL, используя Refl аргумент:

-- 5 % 5 == 0, so it should compile
*Test> onlyModBy5 5 Refl
5 : Nat 

-- 7 % 5 == 2, so it should not compile
*Test> onlyModBy5 7 Refl
(input):1:12:When checking an application of function Main.onlyModBy5:
        Type mismatch between
                x = x (Type of Refl)
        and
                modNat 7 5 = 0 (Expected type)

        Specifically:
                Type mismatch between
                        2
                and
                        0

Затем я попытался определить вспомогательную функцию, которая обеспечивала бы второй prf (доказательство) аргумент для краткости. Другими словами, я бы предпочел, чтобы вызывающая сторона этой функции не предоставляла Refl аргумент.

onlyModBy5Short : (n : Nat) -> Nat
onlyModBy5Short n = onlyModBy5 n Refl

Но он не компилируется:

When checking right hand side of onlyModBy5Short with expected type
        Nat

When checking an application of function Main.onlyModBy5:
        Type mismatch between
                0 = 0 (Type of Refl)
        and
                modNat n 5 = 0 (Expected type)

        Specifically:
                Type mismatch between
                        0
                and
                        Prelude.Nat.modNatNZ, mod' n 4 SIsNotZ n n 4
Holes: Main.onlyModBy5Short

Как, если возможно, можно написать эту функцию?

Answer 1

Ты можешь сделать onlyModBy5Второй аргумент auto аргумент:

onlyModBy5 : (n : Nat) -> {auto prf : n `modNat` 5 = 0} -> Nat
onlyModBy5 n = n

Это работает, потому что для данного буквального значения n, n `modNat` 5 всегда можно уменьшить, и так n `modNat` 5 = 0 всегда будет сводиться к 0 = 0 (в этом случае конструктор Refl имеет правильный тип), если n действительно не делится на 5.

Действительно, это позволит вам проверить тип

foo : Nat
foo = onlyModBy5 25

но отвергнуть

bar : Nat
bar = onlyModBy5 4