当 x 和 xs 是静态已知的时证明不是 (Elem x xs)答案

【问题标题】：Proving Not (Elem x xs) when x and xs are statically known当 x 和 xs 是静态已知的时证明不是 (Elem x xs)
【发布时间】：2016-09-04 02:18:28
【问题描述】：

在Type Driven Development with Idris 的第 9 章中，我们介绍了带有构造函数 Here 和 There 的 Elem 谓词，用于证明元素是向量的成员。例如

oneInVector : Elem 1 [1, 2, 3]
oneInVector = Here

twoInVector : Elem 2 [1, 2, 3]
twoInVector = There Here

我想知道如何在向量中显示一个元素不是。也许应该通过为这种类型提供解决方案：

notThere : Elem 4 [1, 2, 3] -> Void
notThere = ?rhs

表达式/证明搜索在这种情况下没有给出答案，给出：

notThere : Elem 4 [1,2,3] -> Void
notThere = \__pi_arg => ?rhs1

Scanning through the library for Data.Vect，这些定义看起来很有用（但我不确定如何连接这些点）：

||| Nothing can be in an empty Vect
noEmptyElem : {x : a} -> Elem x [] -> Void
noEmptyElem Here impossible

Uninhabited (Elem x []) where
  uninhabited = noEmptyElem

【问题讨论】：

标签： idris theorem-proving

【解决方案1】：

Elem 关系是Decidable（如果元素类型有Decidable Eqality 本身），使用isElem：

isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)

这个想法是使用 isElem 4 [1, 2, 3] 让 Idris 计算 Not (Elem 4 [1, 2, 3]) 的证明。我们需要建立一些类似于 Agda 的 Relation.Nullary.Decidable.toWitnessFalse 的机制，以便我们可以从（否定的）Dec 结果中提取证据：

fromFalse : (d : Dec p) -> {auto isFalse : decAsBool d = False} -> Not p
fromFalse (Yes _) {isFalse = Refl} impossible
fromFalse (No contra) = contra

然后我们可以在您的notThere 定义中使用它：

notThere : Not (Elem 4 [1, 2, 3])
notThere = fromFalse (isElem 4 [1, 2, 3])

【讨论】：

【解决方案2】：

与其为notThere 指定我自己的rhs，不如使用Idris 的编辑器支持：

开始于：

notThere : Elem 4 [1, 2, 3] -> Void

在notThere上添加定义：

notThere : Elem 4 [1, 2, 3] -> Void
notThere x = ?notThere_rhs

x 上的案例拆分：

notThere : Elem 4 [1, 2, 3] -> Void
notThere (There later) = ?notThere_rhs

later 上的案例拆分：

notThere : Elem 4 [1, 2, 3] -> Void
notThere (There (There later)) = ?notThere_rhs

later 上的案例拆分：

notThere : Elem 4 [1, 2, 3] -> Void
notThere (There (There There later))) = ?notThere_rhs

later 上的案例拆分：

notThere : Elem 4 [1,2,3] -> Void
notThere (There (There (There Here))) impossible
notThere (There (There (There (There _)))) impossible

这个定义是完整的，所以我们完成了：

*Elem> :total notThere
Main.notThere is Total

如果有更好的解决方案使用Data.Vect 中的noEmptyElem 和/或uninhabited，我仍然会感兴趣。

【讨论】：