在 Idris 中强制一个参数大于另一个参数答案

【问题标题】：Force one argument to be greater than another in Idris在 Idris 中强制一个参数大于另一个参数
【发布时间】：2015-04-20 21:04:26
【问题描述】：

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

例如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 函数？

【问题讨论】：

标签： idris

【解决方案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 的虚拟实现，因为它应该与原始问题正交）。

【讨论】：

谢谢！我不太了解{p = LTESucc p} 部分。我不相信这是必要的，当我删除它时，代码仍然编译。它的目的是什么？
它可能不是......它被留在那里，因为我在 p 参数上进行大小写拆分以确保其他两种情况是荒谬的。虽然，在mSmallest 的实际实现中，您可能需要它来进行递归调用。
我认为 m > n = True 实际上应该已经足够好了，虽然 Idris 类的狂野西部风味可能会让这难以表达（即，您可能需要显式调用规范的Ord 实例）。然后，您将最终逐案证明，深入研究compare 的实现Nat，以证明模类型类废话n > m = True -> GT n m。假设这是可能的，the 和 %instance 和 @ 和花括号可能会很丑。