Idris pass proof to a function that arguments are LTE

Question

I have a function which subtracts two Nats. How do I prove that first argument I'm passing to it is actually smaller than the second

dummy : (k : Nat) -> (n : Nat) -> {auto smaller : LTE k n} -> Nat
dummy k n = n - k

I've tried couple of solutions which don't work

smallerThan : (k : Nat) -> (n : Nat) -> Maybe (LTE k n)
smallerThan Z k = Just (LTEZero {right=k})
smallerThan (S k) Z = Nothing
smallerThan (S k) (S n) = case isLTE k n of
                            Yes prf => Just prf
                            No contra => Nothing

smallerThan (S k) (S n) = case smallerThan k n of
                            Nothing => Nothing
                            Just lte => Just (cong lte)

I know that type of my hole smallerThan (S k) (S n) = Just (?hole) is LTE (S k) (S n) but how to properly use fromLteSucc or any other function in order to implement that?

I've found this question but that was solved without the proof I need.

Could you provide a hints of what I'm doing wrong and how to properly implement this kind of check?

Answer 1

In the Just case in your second attempt, you have thanks to recursion a proof that LTE k n, but need, as you state, LTE (S k) (S n). You can find the missing step in two ways. Search in the REPL for a function of that type:

Idris> :search LTE k n -> LTE (S k) (S n)
= Prelude.Nat.LTESucc : LTE left right -> LTE (S left) (S right)
If n <= m, then n + 1 <= m + 1

or even simpler, use the proof search via REPL or the editor (I can just use <space>p to solve ?hole, which is the best feature in Idris IMO!). That will also result in

 smallerThan (S k) (S n) = case smallerThan k n of
                             Nothing => Nothing
                             Just lte => Just (LTESucc lte)

Also, isLTE is smallerThan just with the more powerful Dec than Maybe, because in the negative case you get a proof that k is not smaller or equal to n. So isLTE is free of bugs, while smallerThan could just always return Nothing.

You can use that in the dummy calling function like:

foo : Nat -> Nat -> Nat
foo x y = case isLTE x y of
   Yes prf => dummy x y
   No contra => Z