时间戳

首页 > 解决方案 > 完整证明如果最后一个列表元素不在列表中，则前置不会如此

idris - 完整证明如果最后一个列表元素不在列表中，则前置不会如此

问题描述

完成 Idris 的类型驱动开发一书的练习 9.1 后，我无法完成我的一个证明。练习是使isLast功​​能起作用。它应该返回一个值是 a 的最后一个值的证明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）。

非常感谢您的帮助。

标签： idris

解决方案

不可能证明notLastInTailEqNotLast，因为它不正确。这是一个反例：0is not the last element of the empty list []，但是如果您0将其添加到空列表中，您会突然发现它0是新列表的最后一个元素。

另一种看待它的方式是，当您尝试填写时?hole，您Void的目标是，因此这一定意味着您的上下文中应该有矛盾，但是上下文看起来像这样

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

但是你唯一的矛盾对象是notLastInTail. 如果你眯着眼睛看它的类型，你会发现它只是你的lastNotNil定理，即它并不矛盾。

推荐阅读