CODEWITHSUNDEEP
idrisproof-of-correctness
Samuel Barr
Samuel Barr

Reputation: 444

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

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?

Upvotes: 0

Views: 205

Answers (1)

xash
xash

Reputation: 3722

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

Upvotes: 4

Related Questions