確定是否總和平均分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，和Nat（如果Vect是大小n的）任何Vect和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證明他們不相等。然後可以用{prf}將該證明給onlyModBy5。這延伸到{prf=prf}，其暗含論證Yes的證明，因爲二者都被命名爲prf。