证明索引在给定的列表边界内(索引 + 1)在边界内

Question

假设我们有一个list : List a，我们想使用它的第一个和第二个元素：

case inBounds 1 list of
Yes prf => doSmth (index 0 list) (index 1 list)
No _ => doSmthElse

不幸的是，这不会进行类型检查：事实上，prf是InBounds 1 list成立的证明，但是虽然对我们人类来说很明显，InBounds 0 list立即随之而来，但它仍然需要向类型检查器展示。

当然，人们可能会写一个帮助程序证明

inBoundsDecr : InBounds (S k) xs -> InBounds k xs
inBoundsDecr {k = Z} (InLater y) = InFirst
inBoundsDecr {k = (S k)} (InLater y) = InLater (inBoundsDecr y)

然后在Yes分支中使用它，如下所示：

case inBounds 1 list of
Yes prf => let prf' = inBoundsDecr prf in
doSmth (index 0 list) (index 1 list)
No _ => doSmthElse

但它似乎很冗长。

那么，在伊德里斯中这样做最简洁和/或最惯用的方法是什么？

Answer 1

如果你有一个xs证明，给你一些关于xs的信息，最好使用with而不是case。然后编译器可以看到参数可以由证明确定。请参阅教程中的本章：视图和"with"规则

addHs : List Nat -> Nat
addHs xs with (inBounds 1 xs)
addHs xs | p = ?hole

p上的模式匹配给出Yes prf，然后是Yes (InLater y)，然后是Yes (InLater InFirst)，并将xs更新为(x :: y :: xs)。因此，您可以轻松使用x和y：

addHs : List Nat -> Nat
addHs xs with (inBounds 1 xs)
addHs (x :: y :: xs) | (Yes (InLater InFirst)) = x + y
addHs xs | (No contra) = 0

问题是 - 在这里它无法正常工作。如果您检查addHs是否为总数，编译器会警告您，因为它认为可以达到另一个Yes (InLater p)。不知道为什么，整体检查器不是那么好。但从理论上讲，它应该可以正常工作。:-)

除了您的初始尝试(可能更冗长，但您不太依赖整体性检查器)之外，您当然可以在Yes (InLater p)的情况下添加一个虚拟或停止并执行类似

addHs : List Nat -> Nat
addHs xs with (inBounds 1 xs)
addHs (x :: xs) | (Yes (InLater prf)) = x + (index 0 xs)
addHs xs | (No contra) = 0

或者有些不安全并断言无法到达案例：

addHs : List Nat -> Nat
addHs xs with (inBounds 1 xs) proof q
addHs (x :: y :: xs) | Yes (InLater InFirst) = x + y
addHs (x :: xs) | Yes (InLater p) = assert_unreachable
addHs xs | No _ = 0