在伊德里斯强制一个参数大于另一个参数

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用于有趣案例的虚拟实现,因为它应该与原始问题正交).