为 Agda 函数提供证明答案

【问题标题】：Providing proof to Agda functions为 Agda 函数提供证明
【发布时间】：2017-08-04 02:27:14
【问题描述】：

给出以下片段（取自 Ulf Norell 的教程和 James Chapman），我了解 lookup 的调用者必须提供所需项目的索引 ix 有效的证明，但我只是找不到正确的表格去做吧。

data Proven-n : Set where
record Proven-y : Set where

-- using the name 'isProven' instead of 'isTrue' of the tutorial
isProven : Bool -> Set 
isProven true = Proven-y
isProven false = Proven-n

lookup : {A : Set}(xs : List A)(ix : Nat) -> isProven (n < length xs) -> A

我已经设法解决了下面的特殊情况，但是我对 lookup 的更一般应用的所有尝试（其中向量和查找索引是在另一个函数中生成的）都失败了。我想了解传递证明的概念。请帮忙。

aList : List Bool
aList = true :: false :: []

aTest: Bool 
aTest = lookup aList 0 (record {})

【问题讨论】：

您能否提供一个不适合您的lookup 示例应用程序，包括任何相关定义（如_<_）？我不清楚你到底卡在哪里了。
例如，我希望 aTest 接收 ix 作为参数：aTest (ix : Nat) -> Bool。我如何转发 ix 有效的证明以进行查找：lookup aList ix ??>。 () 是 Nat 的正常小于运算符。
你确定要aTest : Nat -> Bool吗？这意味着aTest 为any Nat 生成Bool 的值。我猜你想要像aTest : Nat -> Maybe Bool 这样的东西，如果给定的索引超出范围，则返回nothing。
您可以而且应该在 OP 中提供一个经过全面类型检查的 Agda 程序，因为就目前而言，它使回答者的工作变得更加艰难。您缺少必需的导入和lookup 的定义。（将查找声明为postulate 也是合适的。）并且lookup 和aTest 包含（显然？）错别字。我对 OP 的建议（但被拒绝）编辑是 here。

标签： agda

【解决方案1】：

编辑：以下内容作为对编辑here的问题的回应更有意义。

我猜你想要aTest : Nat -> Maybe Bool 之类的东西，如果给定索引超出范围，则返回nothing。在这种情况下，将执行以下操作：

data Decide (P : Set) : Set where
  yes : P -> Decide P
  no : (P -> Proven-n) -> Decide P

okay? : ∀ {A : Set} (xs : List A) (ix : Nat) -> Decide (isProven (ix < length xs))
okay? [] ix = no λ ()
okay? (_ ∷ xs) zero = yes record {}
okay? (_ ∷ xs) (suc ix) = okay? xs ix

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A -> Maybe A

aTest : Nat -> Maybe Bool
aTest ix with okay? aList ix
... | yes ix<len = just (lookup aList ix ix<len)
... | no ix≥len = nothing

在上面，aTest 使用okay? 来决定索引是否在范围内。如果是，则将证明（由Decide 携带）传递给lookup。

【讨论】：

看起来就像我做的那样，相同（或非常相似）的证明做了两次，一次是okay?，另一次是lookup。我不确定这是否会影响性能，或者，如果确实如此，那么究竟是修复它的最佳方法。但这是一个不同的问题。