Helper Функция определить, если Nat `mod` 5 == 0

Question

Xash дала мне полезный ответ на Function to Determine if Nat is Divisible by 5 at Compile-Time (что я переименовал от моего первоначального длинного имени):

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

Предыдущая answer образованных меня как запустить его на РЕПЛ используя 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 (Proof) аргумент в пользу лаконичности. Другими словами, я бы предпочел, чтобы вызывающая сторона этой функции не предоставляла аргумент 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 «s 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.

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

foo : Nat 
foo = onlyModBy5 25 

но отвергают

bar : Nat 
bar = onlyModBy5 4