Как я могу использовать доказательство, которое я сделал в Idris, чтобы сообщить компилятору, что моя подпись типа верна?

Question

У меня есть функция count в 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:

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