如何使用我在 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

最大值计数的证明可以返回：

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

如何使用我的证明通知伊德里斯此类型签名是正确的？

Answer 1

现在，伊德里斯找不到(-)的证明{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