idris - 在 Idris 中强制一个参数大于另一个参数

Question

我正在尝试编写一个函数，该函数mSmallest采用两个自然数作为输入n并m产生一个向量。输出向量包含具有m成员的有限集的最小n成员。

例如mSmallest 5 3应该产生[FS (FS Z), FS Z, Z]哪个是Vect 3 (Fin 5)

我想将输入参数限制m为小于n. 我试过这样的事情：

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

由于输入，第二种情况不应该是可能的p。我如何才能Z (S k)消除这种情况？

另外，有没有更好的方法来定义mSmallest函数？

Answer 1

我认为n > m = True不够有建设性；如果您改用该GT命题，​​则可以消除前两个分支，因为在这种情况下无法进行模式匹配p：

-- 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

（这个对有趣的案例使用了一个虚拟实现，mSmallest因为这应该与原始问题正交）。