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?
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).