Helper Funktion zu bestimmen, ob Nat `mod` 5 == 0

Question

Xash mich auf Function to Determine if Nat is Divisible by 5 at Compile-Time eine hilfreiche Antwort zur Verfügung gestellt (die ich von meiner ursprünglichen langen Namen umbenannt):

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

Eine frühere answer mich erzogen wie es auf dem REPL mit dem Refl Argumente auszuführen:

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

Dann habe ich versucht, eine Hilfsfunktion zu definieren, die das zweite prf (Nachweis) Argument für Prägnanz bieten würden. Mit anderen Worten, ich würde bevorzugen, dass der Aufrufer dieser Funktion das Refl Argument nicht bereitstellen muss.

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

Aber es nicht kompiliert:

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 

Wie, wenn möglich, kann diese Funktion geschrieben werden?

Answer 1

Sie können onlyModBy5 ‚zweites Argument machen eine auto argument:

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

Dies funktioniert, weil für einen bestimmten wörtlichen Wert von n kann n `modNat` 5 immer reduziert werden, und so wird n `modNat` 5 = 0 immer reduzieren 0 = 0 (in denen Fall wird der Konstruktor Refl den richtigen Typ hat), es sei denn n von 5.

Tat wirklich nicht teilbar ist, dies ermöglicht es Ihnen

typecheck

foo : Nat 
foo = onlyModBy5 25 

aber ablehnen

bar : Nat 
bar = onlyModBy5 4