我如何使用我在 Idris 中制作的证明来通知编译器我的类型签名是正确的？

Question

我在 idris 中有一个函数计数，定义为：

count : Eq a => a -> Vect n a -> Nat
count x [] = Z
count x (y::ys) = with (x == y)
  | True = S (count x ys)
  | False = count x ys

而最大值计数的证明可以return:

countLTELen : Eq a => (x : a) -> (l : Vect n a) -> LTE (count x l) n
countLTELen x [] = lteRefl
countLteLen x (y::ys) with (x == y)
  | True = LTESucc (countLTELen x ys)
  | False = lteSuccRight (countLTELen x ys)

一切都很好。我现在想编写一个函数，从列表中删除所有元素，removeAll :

removeAll : Eq a => (x : a) -> (l : Vect n a) -> Vect (n - (count x l)) a
removeAll x [] = []
removeAll x (y::ys) with (x == y)
  | True = removeAll x ys
  | False = x :: removeAll x ys

但是这个定义给出了一个错误：

   |
56 | removeAll : Eq a => (x : a) -> (l : Vect n a) -> Vect (n - (count x l)) a
   |                                                          ^
When checking type of Proof.removeAll:
When checking argument smaller to function Prelude.Nat.-:
    Can't find a value of type 
            LTE (count a n constraint x l) n

我如何使用我的证明来通知 Idris 此类型签名是正确的？

Answer 1

目前，Idris 找不到 {auto smaller : LTE n m} (-) 的证明。

所以要么你需要明确：

removeAll : Eq a => (x : a) -> (l : Vect n a) ->
                    Vect ((-) {smaller=countLTELen x l} n (count x l) ) a

或者，因为 smaller 是一个 auto 参数，您可以提示编译器使用您的证明函数。然后在auto时会尝试这个函数——为LTE (count x l) n.

找一个值

%hint
countLTELen : Eq a => (x : a) -> (l : Vect n a) -> LTE (count x l) n

我如何使用我在 Idris 中制作的证明来通知编译器我的类型签名是正确的？

How can I use a proof I've made in Idris to inform the compiler that my type signature is correct?

idris

proof-of-correctness