代码之家 › 专栏 › 技术社区 › Lodewijk Bogaards

完全证明如果列表中的最后一个列表元素不在列表中,则prepending不会使其成为

idris

0

Lodewijk Bogaards · 技术社区 · 8 年前

在用Idris完成了书籍类型驱动开发的练习9.1之后,我无法得到一个完整的证明。练习是使 isLast 功能工作。它应该返回一个值是 List . 很有效,但不幸的是 notLastInTailEqNotLast 不是全部。

data Last : List a -> a -> Type where
     LastOne : Last [value] value
     LastCons : (prf : Last xs value) -> Last (x :: xs) value

lastNotNil : Last [] value -> Void
lastNotNil _ impossible

lastNotEq : (contra : (lastValue = value) -> Void) -> Last [lastValue] value -> Void
lastNotEq contra LastOne = contra Refl
lastNotEq _ (LastCons LastOne) impossible
lastNotEq _ (LastCons (LastCons _)) impossible

notLastInTailEqNotLast : (notLastInTail : Last xs value -> Void) ->
                         Last (y :: xs) value -> Void
notLastInTailEqNotLast notLastInTail LastOne = ?hole
notLastInTailEqNotLast notLastInTail (LastCons prf) = notLastInTail prf


isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No lastNotNil
isLast [lastValue] value = case decEq lastValue value of
  Yes Refl => Yes LastOne
  No contra => No (lastNotEq contra)
isLast (x :: xs) value = case isLast xs value of
  Yes last => Yes (LastCons last)
  No notLastInTail => No (notLastInTailEqNotLast notLastInTail)

我该怎么填 ?hole ?

我在这里看到了解决方案: https://github.com/edwinb/TypeDD-Samples/blob/master/Chapter9/Exercises/ex_9_1.idr . 我知道这是怎么解决我的问题的 lastNotCons 我可以用这种方法解决问题,但这看起来像是一种解决办法。我想提供的证据对我来说似乎微不足道:如果我有证据表明一个元素不是列表中的最后一个元素,那么附加了该列表的另一个列表将仍然没有该元素作为列表中的最后一个元素(即。 notLastInTailEqNotLast上一个 ).

非常感谢你的帮助。

1 回复 | 直到 8 年前

1

2

Anton Trunov 8 年前

不可能证明 notLastInTailEqNotLast ,因为它不正确。下面是一个反例: 0 不是空列表的最后一个元素 [] ,但如果你准备好了 零 你突然明白了 零 是新列表的最后一个元素。

另一种看问题的方法是当你试图填写 ?hole ,你有 Void 作为你的目标,所以这一定意味着你应该在你的上下文中有一个矛盾,但是上下文看起来是这样的

`--   phTy : Type
      value : phTy
      notLastInTail : Last [] value -> Void
     ---------------------------------------

但你唯一的矛盾候选人是 notLastInTail . 如果你斜视它的类型,你会发现它只是你的 lastNotNil 定理,也就是说,它并不矛盾。