Force one argument to be greater than another in Idris

Question

I am trying to write a function mSmallest that takes two natural numbers, n and m as inputs and produces a vector. The output vector contains the m smallest members of the finite set with n members.

For example mSmallest 5 3 is supposed to produce [FS (FS Z), FS Z, Z] which is a Vect 3 (Fin 5)

I would like to restrict the input argument m to be less than n. I tried something like this:

mSmallest : (n : Nat) -> (m : Nat) -> {auto p : n > m = True} -> Vect m (Fin n)
mSmallest Z Z = ?c_3                                                                   
mSmallest Z (S k) = ?c_5                                                               
mSmallest (S k) m = ?c_2

The second case should not be possible because of the input p. How do I make it so that the Z (S k) case is eliminated?

Also, is there a better way of defining the mSmallest function?

Answer 1

I don't think n > m = True is constructive enough; if you use the GT proposition instead, you can eliminate the first two branches since there's no way to pattern-match on p in that case:

-- Note that mSmallest is accepted as total with just this one case!
total mSmallest : (n : Nat) -> (m : Nat) -> {auto p : n `GT` m} -> Vect m (Fin n)
mSmallest (S k) m {p = LTESucc p} = replicate m FZ

(this one uses a dummy implementation of mSmallest for the interesting case since that should be orthogonal to the original question).