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

Question

在使用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

在这种情况下,表达/证明搜索没有得出答案,给出:

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

扫描库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

该Elem关系是Decidable(如果元素类型本身具有Decidable uality Eq),使用isElem:

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

这个想法是用来isElem 4 [1, 2, 3]让伊德里斯计算出来的证明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])