@@ -9,6 +9,7 @@ import Prelude.Classes
9import Prelude.Foldable
9import Prelude.Foldable
10import Prelude.Functor
10import Prelude.Functor
11import Prelude.Maybe
11import Prelude.Maybe
12+import Prelude.Uninhabited
12import Prelude.Nat
13import Prelude.Nat
14%access public
15%access public
@@ -41,6 +42,37 @@ isCons : List a -> Bool
41isCons [] = False
42isCons [] = False
42isCons (x::xs) = True
43isCons (x::xs) = True
45+--------------------------------------------------------------------------------
46+-- Decidable Predicates
47+--------------------------------------------------------------------------------
49+data NonEmpty : List a -> Type where
50+ IsNonEmpty : NonEmpty (x :: xs)
53+nonEmptyNil : NonEmpty [] -> Void
54+nonEmptyNil IsNonEmpty impossible
56+nonEmpty : (xs : List a) -> Dec (NonEmpty xs)
57+nonEmpty [] = No nonEmptyNil
58+nonEmpty (x :: xs) = Yes IsNonEmpty
60+data InBounds : Nat -> List a -> Type where
61+ InFirst : InBounds Z (x :: xs)
62+ InLater : InBounds k xs -> InBounds (S k) (x :: xs)
64+instance Uninhabited (InBounds k []) where
65+ uninhabited InFirst impossible
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)
44--------------------------------------------------------------------------------
76--------------------------------------------------------------------------------
46--------------------------------------------------------------------------------
78--------------------------------------------------------------------------------
@@ -59,10 +91,9 @@ length (x::xs) = 1 + length xs
59||| Find a particular element of a list.
91||| Find a particular element of a list.
61||| @ ok a proof that the index is within bounds
93||| @ ok a proof that the index is within bounds
62−index : (n : Nat) -> (l : List a) -> (ok : lt n (length l) = True) -> a
94+index : (n : Nat) -> (xs : List a) -> {auto ok : InBounds n xs} -> a
63−index Z (x::xs) p = x
95+index Z (x :: xs) {ok} = x
64−index (S n) (x::xs) p = index n xs ?indexTailProof
96+index (S k) (x :: xs) {ok = InLater p} = index k xs
65−index _ [] Refl impossible
67||| Attempt to find a particular element of a list.
98||| Attempt to find a particular element of a list.
@@ -74,8 +105,8 @@ index' _ [] = Nothing
75||| Get the first element of a non-empty list
106||| Get the first element of a non-empty list
76||| @ ok proof that the list is non-empty
107||| @ ok proof that the list is non-empty
77−head : (l : List a) -> {auto ok : isCons l = True} -> a
108+head : (l : List a) -> {auto ok : NonEmpty l} -> a
78−head [] {ok=Refl} impossible
109+head [] {ok=IsNonEmpty} impossible
79head (x::xs) {ok=p} = x
110head (x::xs) {ok=p} = x
81||| Attempt to get the first element of a list. If the list is empty, return
112||| Attempt to get the first element of a list. If the list is empty, return
@@ -86,8 +117,8 @@ head' (x::xs) = Just x
87||| Get the tail of a non-empty list.
118||| Get the tail of a non-empty list.
88||| @ ok proof that the list is non-empty
119||| @ ok proof that the list is non-empty
89−tail : (l : List a) -> {auto ok : isCons l = True} -> List a
120+tail : (l : List a) -> {auto ok : NonEmpty l} -> List a
90−tail [] {ok=Refl} impossible
121+tail [] {ok=IsNonEmpty} impossible
91tail (x::xs) {ok=p} = xs
122tail (x::xs) {ok=p} = xs
93||| Attempt to get the tail of a list.
124||| Attempt to get the tail of a list.
@@ -99,10 +130,10 @@ tail' (x::xs) = Just xs
100||| Retrieve the last element of a non-empty list.
131||| Retrieve the last element of a non-empty list.
101||| @ ok proof that the list is non-empty
132||| @ ok proof that the list is non-empty
102−last : (l : List a) -> {auto ok : isCons l = True} -> a
133+last : (l : List a) -> {auto ok : NonEmpty l} -> a
103−last [] {ok=Refl} impossible
134+last [] {ok=IsNonEmpty} impossible
104last [x] {ok=p} = x
135last [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}
107||| Attempt to retrieve the last element of a non-empty list.
138||| Attempt to retrieve the last element of a non-empty list.
@@ -116,10 +147,10 @@ last' (x::xs) =
117||| Return all but the last element of a non-empty list.
148||| Return all but the last element of a non-empty list.
118||| @ ok proof that the list is non-empty
149||| @ ok proof that the list is non-empty
119−init : (l : List a) -> {auto ok : isCons l = True} -> List a
150+init : (l : List a) -> {auto ok : NonEmpty l} -> List a
120−init [] {ok=Refl} impossible
151+init [] {ok=IsNonEmpty} impossible
121init [x] {ok=p} = []
152init [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}
124||| Attempt to Return all but the last element of a list.
155||| Attempt to Return all but the last element of a list.
@@ -823,12 +854,6 @@ foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs
824--------------------------------------------------------------------------------
855--------------------------------------------------------------------------------
826−indexTailProof = proof {
832lengthAppendStepCase = proof {
857lengthAppendStepCase = proof {
834 rewrite inductiveHypothesis;
859 rewrite inductiveHypothesis;