Реализация isLast с помощью Idris: не в хвосте - PullRequest
Новая
       16

Реализация isLast с помощью Idris: не в хвосте

0 голосов
/ 14 мая 2019

Я работаю над упражнением 2 в разделе 9.1 из Разработка на основе типов с Idris , и я не могу понять, как заполнить последнюю дыру (см. notInTail ниже).

Я прочитал ответы на Реализация isLast с Idris , но я застрял в другом месте. 

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

notInNil : Last [] value -> Void
notInNil LastOne impossible
notInNil (LastCons _) impossible

notLast : (notHere : (x = value) -> Void) -> Last [x] value -> Void
notLast prf LastOne = absurd (prf Refl)
notLast prf (LastCons _) impossible

notInTail : (notThere : Last xs value -> Void) -> Last (x :: xs) value -> Void
notInTail notThere LastOne = ?hole
notInTail notThere (LastCons prf) = notThere prf

isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No notInNil
isLast (x :: []) value = case decEq x value of
                              Yes Refl => Yes LastOne
                              No notHere => No (notLast notHere)
isLast (_ :: xs) value = case isLast xs value of
                              Yes prf => Yes (LastCons prf)
                              No notThere => No (notInTail notThere)

Вот что сообщает Idris: 

- + Main.hole [P]
 `--       phTy : Type
          value : phTy
       notThere : Last [] value -> Void
     -----------------------------------
      Main.hole : Void

1 Ответ

1 голос
/ 14 мая 2019

Я не думаю, что вы можете доказать notInTail как написано, поскольку это не относится к пустым спискам.Однако он применяется для непустых списков: 

notInTail : (c : Last (y :: ys) value -> Void) -> Last (x :: (y :: ys)) value -> Void
notInTail c (LastCons prf) = c prf

Хвост входного списка должен быть непустым в третьем случае isLast, но вы не указываете это.Если вы это сделаете, вы можете подать заявление notInTail: 

isLast (x :: (y :: xs)) value = case isLast (y :: xs) value of
                                     Yes prf => Yes (LastCons prf)
                                     No c => No (notInTail c)
...