@@ -9,6 +9,7 @@ import Prelude.Classes
99import Prelude.Foldable
1010import Prelude.Functor
1111import Prelude.Maybe
12+import Prelude.Uninhabited
1213import Prelude.Nat
1314
1415%access public
@@ -41,6 +42,37 @@ isCons : List a -> Bool
4142isCons [] = False
4243isCons (x::xs) = True
4344
45+--------------------------------------------------------------------------------
46+-- Decidable Predicates
47+--------------------------------------------------------------------------------
48+
49+data NonEmpty : List a -> Type where
50+ IsNonEmpty : NonEmpty (x :: xs)
51+
52+private
53+nonEmptyNil : NonEmpty [] -> Void
54+nonEmptyNil IsNonEmpty impossible
55+
56+nonEmpty : (xs : List a) -> Dec (NonEmpty xs)
57+nonEmpty [] = No nonEmptyNil
58+nonEmpty (x :: xs) = Yes IsNonEmpty
59+
60+data InBounds : Nat -> List a -> Type where
61+ InFirst : InBounds Z (x :: xs)
62+ InLater : InBounds k xs -> InBounds (S k) (x :: xs)
63+
64+instance Uninhabited (InBounds k []) where
65+ uninhabited InFirst impossible
66+
67+inBounds : (n : Nat) -> (xs : List a) -> Dec (InBounds n xs)
68+inBounds k [] = No uninhabited
69+inBounds Z (x :: xs) = Yes InFirst
70+inBounds (S k) (x :: xs) with (inBounds k xs)
71+ inBounds (S k) (x :: xs) | (Yes prf) = Yes (InLater prf)
72+ inBounds (S k) (x :: xs) | (No contra)
73+ = No (\p => case p of
74+ InLater y => contra y)
75+
4476--------------------------------------------------------------------------------
4577-- Length
4678--------------------------------------------------------------------------------
@@ -59,10 +91,9 @@ length (x::xs) = 1 + length xs
5991||| Find a particular element of a list.
6092|||
6193||| @ ok a proof that the index is within bounds
62−index : (n : Nat) -> (l : List a) -> (ok : lt n (length l) = True) -> a
63−index Z (x::xs) p = x
64−index (S n) (x::xs) p = index n xs ?indexTailProof
65−index _ [] Refl impossible
94+index : (n : Nat) -> (xs : List a) -> {auto ok : InBounds n xs} -> a
95+index Z (x :: xs) {ok} = x
96+index (S k) (x :: xs) {ok = InLater p} = index k xs
6697
6798||| Attempt to find a particular element of a list.
6899|||
@@ -74,8 +105,8 @@ index' _ [] = Nothing
74105
75106||| Get the first element of a non-empty list
76107||| @ ok proof that the list is non-empty
77−head : (l : List a) -> {auto ok : isCons l = True} -> a
78−head [] {ok=Refl} impossible
108+head : (l : List a) -> {auto ok : NonEmpty l} -> a
109+head [] {ok=IsNonEmpty} impossible
79110head (x::xs) {ok=p} = x
80111
81112||| Attempt to get the first element of a list. If the list is empty, return
@@ -86,8 +117,8 @@ head' (x::xs) = Just x
86117
87118||| Get the tail of a non-empty list.
88119||| @ ok proof that the list is non-empty
89−tail : (l : List a) -> {auto ok : isCons l = True} -> List a
90−tail [] {ok=Refl} impossible
120+tail : (l : List a) -> {auto ok : NonEmpty l} -> List a
121+tail [] {ok=IsNonEmpty} impossible
91122tail (x::xs) {ok=p} = xs
92123
93124||| Attempt to get the tail of a list.
@@ -99,10 +130,10 @@ tail' (x::xs) = Just xs
99130
100131||| Retrieve the last element of a non-empty list.
101132||| @ ok proof that the list is non-empty
102−last : (l : List a) -> {auto ok : isCons l = True} -> a
103−last [] {ok=Refl} impossible
133+last : (l : List a) -> {auto ok : NonEmpty l} -> a
134+last [] {ok=IsNonEmpty} impossible
104135last [x] {ok=p} = x
105−last (x::y::ys) {ok=p} = last (y::ys) {ok=Refl}
136+last (x::y::ys) {ok=p} = last (y::ys) {ok=IsNonEmpty}
106137
107138||| Attempt to retrieve the last element of a non-empty list.
108139|||
@@ -116,10 +147,10 @@ last' (x::xs) =
116147
117148||| Return all but the last element of a non-empty list.
118149||| @ ok proof that the list is non-empty
119−init : (l : List a) -> {auto ok : isCons l = True} -> List a
120−init [] {ok=Refl} impossible
150+init : (l : List a) -> {auto ok : NonEmpty l} -> List a
151+init [] {ok=IsNonEmpty} impossible
121152init [x] {ok=p} = []
122−init (x::y::ys) {ok=p} = x :: init (y::ys) {ok=Refl}
153+init (x::y::ys) {ok=p} = x :: init (y::ys) {ok=IsNonEmpty}
123154
124155||| Attempt to Return all but the last element of a list.
125156|||
@@ -823,12 +854,6 @@ foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs
823854-- Proofs
824855--------------------------------------------------------------------------------
825856
826−indexTailProof = proof {
827− intros;
828− rewrite sym p;
829− trivial;
830−}
831−
832857lengthAppendStepCase = proof {
833858 intros;
834859 rewrite inductiveHypothesis;