/
ex_9_1.idr
33 lines (26 loc) · 1.23 KB
/
ex_9_1.idr
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
{- 1 -}
data Elem : a -> List a -> Type where
Here : Elem x (x :: xs)
There : Elem x xs -> Elem x (y :: xs)
{- 2 -}
data Last : List a -> a -> Type where
LastOne : Last [value] value
LastCons : (prf : Last xs value) -> Last (x :: xs) value
lastNotNil : (value : a) -> Last [] x -> Void
lastNotNil _ LastOne impossible
lastNotNil _ (LastCons _) impossible
lastNotCons : (contra : Last (x :: xs) value -> Void) ->
Last (y :: (x :: xs)) value -> Void
lastNotCons contra (LastCons prf) = contra prf
lastNotSingleton : (contra : (y = value) -> Void) -> Last [y] value -> Void
lastNotSingleton contra LastOne = contra Refl
lastNotSingleton _ (LastCons LastOne) impossible
lastNotSingleton _ (LastCons (LastCons _)) impossible
isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No (lastNotNil value)
isLast (y :: []) value = case decEq y value of
(Yes Refl) => Yes LastOne
(No contra) => No (lastNotSingleton contra)
isLast (y :: (x :: xs)) value = case isLast (x :: xs) value of
(Yes prf) => Yes (LastCons prf)
(No contra) => No (lastNotCons contra)