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

0
votes

I have a function count in idris, defined as :

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

And a proof of the maximum value count can 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)

which is all well and good. I now want to write a function which removes all of an element from a list, 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

But this definition gives an error:

   |
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

How can I use my proof to inform Idris that this type signature is correct?

1
idrisproof-of-correctness
1) countLTELen is not necessary here, I think. 2) I’d use a Fin n for the output of count, but it doesn’t really matter. 3) I don’t have the ability to write out a full answer, but if you replace the two RHSs of the with block with holes, you should see that you only need some basic proofs about (-). – HTNW
@HTNW Sorry, I should've been more clear- this definition gives a type check error, which I've now included in the original question. – Samuel Barr

1 Answers

4
votes

Right now, Idris can't find the proof {auto smaller : LTE n m} for (-).

So either you need to be explicit:

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

Or, because smaller is an auto-argument, you can hint the compiler to your proof function. Then this function will be tried when auto-finding a value for LTE (count x l) n.

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