确定 Nat `mod` 5 == 0 的辅助函数

Question

Xash provided me with a helpful answer on （我用原来的长名字重新命名）：

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

之前的教我如何使用 Refl 参数在 REPL 上运行它：

-- 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 argument:

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

确定 Nat `mod` 5 == 0 的辅助函数

Helper Function to Determine if Nat `mod` 5 == 0

idris