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足够有 build 性；如果您使用 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 的虚拟实现，因为它应该与原始问题正交)。