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

Question

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

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

Expression/Proof 在这种情况下搜索没有得出答案，给出：

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

Answer 1

与其为 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

如果有更好的解决方案使用 noEmptyElem and/or uninhabited 来自 Data.Vect.

，我仍然会感兴趣

Answer 2

Elem 关系是 Decidable（如果元素类型本身具有 Decidable Eq 性质），使用 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])

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

Proving Not (Elem x xs) when x and xs are statically known

theorem-proving

idris