Определить, равномерна ли сумма очков Vect n Nat's 5?

Question

Cactus продемонстрировал, как ответить на мой вопрос: Helper Function to Determine if Nat `mod` 5 == 0.

Он писал:

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

Затем я попытался использовать эту функцию, чтобы применить onlyModBy5 на суммы Vect n Nat «с.

foo : (n : Nat) -> Vect n Nat -> Nat 
foo n xs = onlyModBy5 $ sum xs 

Но я получил это ошибка времени компиляции:

When checking right hand side of foo with expected type 
     Nat 

When checking argument prf to function Main.onlyModBy5: 
     Can't find a value of type 
       Prelude.Nat.modNatNZ, mod' (foldrImpl (\meth => 
                 \meth => 
                  plus meth meth) 
                 0 
                 id 
                 xs) 
              4 
              SIsNotZ 
              (foldrImpl (\meth => 
                 \meth => 
                  plus meth meth) 
                 0 
                 id 
                 xs) 
              (foldrImpl (\meth => 
                 \meth => 
                  plus meth meth) 
                 0 
                 id 
                 xs) 
              4 = 
       0 
Holes: Main.foo 

Как я могу использовать выше onlyModBy5 функцию с foo?

Answer 1

Это зависит от того, чего вы хотите достичь. foo : (n : Nat) -> Vect n Nat -> Nat говорит, что вы можете применить любой Nat к foo и любой Vect из Nat (если Vect имеет размер n) и foo возвратит Nat.

Прежде всего, вам не нужен явный аргумент (n : Nat). Если вы напишете только foo : Vect n Nat -> Nat, Идрис превратит n внутренне в неявный аргумент: foo : {n : Nat} -> Vect n Nat -> Nat.

В аргументах нет ничего о элементах Vect, и поэтому ничего о нем sum. Вы можете применить [1,2,2], а также [1,1], тогда как последний не имеет доказательства prf : (sum [1,1])`modNat`5 == 0), поэтому, очевидно, вы не можете применить сумму к onlyModBy5.

Вы можете либо потребовать доказательства этого в качестве аргумента, как и раньше:

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

Или пусть это решить, на основе суммы:

foo : Vect n Nat -> Maybe Nat 
foo xs = foo' (sum xs) 
    where 
    foo' : Nat -> Maybe Nat 
    foo' k with (decEq (k `modNat` 5) 0) 
     | Yes prf = Just (onlyModBy5 k {prf}) 
     | No _ = Nothing 

decEq решает, являются ли propositionally равны два значения (в этом случае, если они являются одинаковыми Nat), либо либо возвращает Yes с (prf : n`modNat`5 = 0), что они равны, или No с доказательством того, что они не равны. Затем это доказательство можно дать onlyModBy5 с {prf}. Это продолжается до {prf=prf}, что дает неявный аргумент доказательства Yes, так как оба названы prf.