@@ -14,9 +14,12 @@ import Prelude.Nat
15infixr 7 ::,++
15infixr 7 ::,++
17−%elim data List a
18+%elim data List a =
19− | (::) a (List a)
22+ (::) a (List a)
21-- Name hints for interactive editing
24-- Name hints for interactive editing
22%name List xs, ys, zs, ws
25%name List xs, ys, zs, ws
@@ -25,10 +28,12 @@ infixr 7 ::,++
25-- Syntactic tests
28-- Syntactic tests
26--------------------------------------------------------------------------------
29--------------------------------------------------------------------------------
31+||| Returns `True` iff the argument is empty
28isNil : List a -> Bool
32isNil : List a -> Bool
29isNil [] = True
33isNil [] = True
30isNil (x::xs) = False
34isNil (x::xs) = False
36+||| Returns `True` iff the argument is not empty
32isCons : List a -> Bool
37isCons : List a -> Bool
33isCons [] = False
38isCons [] = False
34isCons (x::xs) = True
39isCons (x::xs) = True
@@ -37,6 +42,9 @@ isCons (x::xs) = True
38--------------------------------------------------------------------------------
43--------------------------------------------------------------------------------
45+||| Compute the length of a list.
47+||| Runs in linear time
40length : List a -> Nat
48length : List a -> Nat
41length [] = 0
49length [] = 0
42length (x::xs) = 1 + length xs
50length (x::xs) = 1 + length xs
@@ -45,49 +53,74 @@ length (x::xs) = 1 + length xs
45-- Indexing into lists
53-- Indexing into lists
46--------------------------------------------------------------------------------
54--------------------------------------------------------------------------------
56+||| Find a particular element of a list.
58+||| @ ok a proof that the index is within bounds
48−index : (n : Nat) -> (l : List a) -> (lt n (length l) = True) -> a
59+index : (n : Nat) -> (l : List a) -> (ok : lt n (length l) = True) -> a
49index Z (x::xs) p = x
60index Z (x::xs) p = x
50index (S n) (x::xs) p = index n xs ?indexTailProof
61index (S n) (x::xs) p = index n xs ?indexTailProof
51index _ [] refl impossible
62index _ [] refl impossible
64+||| Attempt to find a particular element of a list.
66+||| If the provided index is out of bounds, return Nothing.
53index' : (n : Nat) -> (l : List a) -> Maybe a
67index' : (n : Nat) -> (l : List a) -> Maybe a
54index' Z (x::xs) = Just x
68index' Z (x::xs) = Just x
55index' (S n) (x::xs) = index' n xs
69index' (S n) (x::xs) = index' n xs
56index' _ [] = Nothing
70index' _ [] = Nothing
72+||| Get the first element of a non-empty list
73+||| @ ok proof that the list is non-empty
58−head : (l : List a) -> (isCons l = True) -> a
74+head : (l : List a) -> (ok : isCons l = True) -> a
59head [] refl impossible
75head [] refl impossible
60head (x::xs) p = x
76head (x::xs) p = x
78+||| Attempt to get the first element of a list. If the list is empty, return
62head' : (l : List a) -> Maybe a
80head' : (l : List a) -> Maybe a
63head' [] = Nothing
81head' [] = Nothing
64head' (x::xs) = Just x
82head' (x::xs) = Just x
84+||| Get the tail of a non-empty list.
85+||| @ ok proof that the list is non-empty
66−tail : (l : List a) -> (isCons l = True) -> List a
86+tail : (l : List a) -> (ok : isCons l = True) -> List a
67tail [] refl impossible
87tail [] refl impossible
68tail (x::xs) p = xs
88tail (x::xs) p = xs
90+||| Attempt to get the tail of a list.
92+||| If the list is empty, return `Nothing`.
70tail' : (l : List a) -> Maybe (List a)
93tail' : (l : List a) -> Maybe (List a)
71tail' [] = Nothing
94tail' [] = Nothing
72tail' (x::xs) = Just xs
95tail' (x::xs) = Just xs
97+||| Retrieve the last element of a non-empty list.
98+||| @ ok proof that the list is non-empty
74−last : (l : List a) -> (isCons l = True) -> a
99+last : (l : List a) -> (ok : isCons l = True) -> a
75last [] refl impossible
100last [] refl impossible
76last [x] p = x
101last [x] p = x
77last (x::y::ys) p = last (y::ys) refl
102last (x::y::ys) p = last (y::ys) refl
104+||| Attempt to retrieve the last element of a non-empty list.
106+||| If the list is empty, return `Nothing`.
79last' : (l : List a) -> Maybe a
107last' : (l : List a) -> Maybe a
80last' [] = Nothing
108last' [] = Nothing
81−last' (x::xs) =
109+last' (x::xs) =
82 case xs of
110 case xs of
83 [] => Just x
111 [] => Just x
84 y :: ys => last' xs
112 y :: ys => last' xs
114+||| Return all but the last element of a non-empty list.
115+||| @ ok proof that the list is non-empty
86−init : (l : List a) -> (isCons l = True) -> List a
116+init : (l : List a) -> (ok : isCons l = True) -> List a
87init [] refl impossible
117init [] refl impossible
88init [x] p = []
118init [x] p = []
89init (x::y::ys) p = x :: init (y::ys) refl
119init (x::y::ys) p = x :: init (y::ys) refl
121+||| Attempt to Return all but the last element of a list.
123+||| If the list is empty, return `Nothing`.
91init' : (l : List a) -> Maybe (List a)
124init' : (l : List a) -> Maybe (List a)
92init' [] = Nothing
125init' [] = Nothing
93init' (x::xs) =
126init' (x::xs) =
@@ -103,21 +136,39 @@ init' (x::xs) =
103-- Sublists
136-- Sublists
104--------------------------------------------------------------------------------
137--------------------------------------------------------------------------------
139+||| Take the first `n` elements of `xs`
141+||| If there are not enough elements, return the whole list.
142+||| @ n how many elements to take
143+||| @ xs the list to take them from
106−take : Nat -> List a -> List a
144+take : (n : Nat) -> (xs : List a) -> List a
107take Z xs = []
145take Z xs = []
108take (S n) [] = []
146take (S n) [] = []
109take (S n) (x::xs) = x :: take n xs
147take (S n) (x::xs) = x :: take n xs
149+||| Drop the first `n` elements of `xs`
151+||| If there are not enough elements, return the empty list.
152+||| @ n how many elements to drop
153+||| @ xs the list to drop them from
111−drop : Nat -> List a -> List a
154+drop : (n : Nat) -> (xs : List a) -> List a
112drop Z xs = xs
155drop Z xs = xs
113drop (S n) [] = []
156drop (S n) [] = []
114drop (S n) (x::xs) = drop n xs
157drop (S n) (x::xs) = drop n xs
159+||| Take the longest prefix of a list such that all elements satsify some
160+||| Boolean predicate.
162+||| @ p the predicate
116−takeWhile : (a -> Bool) -> List a -> List a
163+takeWhile : (p : a -> Bool) -> List a -> List a
117takeWhile p [] = []
164takeWhile p [] = []
118takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []
165takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []
167+||| Remove the longest prefix of a list such that all removed elements satsify some
168+||| Boolean predicate.
170+||| @ p the predicate
120−dropWhile : (a -> Bool) -> List a -> List a
171+dropWhile : (p : a -> Bool) -> List a -> List a
121dropWhile p [] = []
172dropWhile p [] = []
122dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
173dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
@@ -125,7 +176,12 @@ dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
126--------------------------------------------------------------------------------
177--------------------------------------------------------------------------------
179+||| Simply-typed recursion operator for lists.
181+||| @ nil what to return at the end of the list
182+||| @ cons what to do at each step of recursion
183+||| @ xs the list to recurse over
128−list : a -> (a -> List a -> a) -> List a -> a
184+list : (nil : a) -> (cons : a -> List a -> a) -> (xs : List a) -> a
129list nil cons [] = nil
185list nil cons [] = nil
130list nil cons (x::xs) = cons x xs
186list nil cons (x::xs) = cons x xs
@@ -133,16 +189,23 @@ list nil cons (x::xs) = cons x xs
133-- Building (bigger) lists
189-- Building (bigger) lists
134--------------------------------------------------------------------------------
190--------------------------------------------------------------------------------
136(++) : List a -> List a -> List a
193(++) : List a -> List a -> List a
137−(++) [] right = right
194+(++) [] right = right
138(++) (x::xs) right = x :: (xs ++ right)
195(++) (x::xs) right = x :: (xs ++ right)
197+||| Create an infinite sequence of some item.
199+||| Consider using a `Stream` instead.
141repeat : a -> List a
201repeat : a -> List a
142repeat x = x :: lazy (repeat x)
202repeat x = x :: lazy (repeat x)
204+||| Construct a list with `n` copies of `x`
205+||| @ n how many copies
206+||| @ x the element to replicate
144−replicate : Nat -> a -> List a
207+replicate : (n : Nat) -> (x : a) -> List a
145−replicate Z x = []
208+replicate Z x = []
146replicate (S n) x = x :: replicate n x
209replicate (S n) x = x :: replicate n x
148--------------------------------------------------------------------------------
211--------------------------------------------------------------------------------
@@ -187,15 +250,27 @@ instance Functor List where
187-- Zips and unzips
250-- Zips and unzips
188--------------------------------------------------------------------------------
251--------------------------------------------------------------------------------
253+||| Combine two lists of the same length elementwise using some function.
254+||| @ f the function to combine elements with
255+||| @ l the first list
256+||| @ r the second list
257+||| @ ok a proof that the lengths of the inputs are equal
190zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->
258zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->
191− (length l = length r) -> List c
259+ (ok : length l = length r) -> List c
192zipWith f [] (y::ys) refl impossible
260zipWith f [] (y::ys) refl impossible
193zipWith f (x::xs) [] refl impossible
261zipWith f (x::xs) [] refl impossible
194zipWith f [] [] p = []
262zipWith f [] [] p = []
195zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)
263zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)
265+||| Combine three lists of the same length elementwise using some function.
266+||| @ f the function to combine elements with
267+||| @ x the first list
268+||| @ y the second list
269+||| @ z the third list
270+||| @ ok a proof that the lengths of the first two inputs are equal
271+||| @ ok' a proof that the lengths of the second and third inputs are equal
197zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
272zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
198− (z : List c) -> (length x = length y) -> (length y = length z) -> List d
273+ (z : List c) -> (ok : length x = length y) -> (ok' : length y = length z) -> List d
199zipWith3 f _ [] (z::zs) p refl impossible
274zipWith3 f _ [] (z::zs) p refl impossible
200zipWith3 f _ (y::ys) [] p refl impossible
275zipWith3 f _ (y::ys) [] p refl impossible
201zipWith3 f [] (y::ys) _ refl q impossible
276zipWith3 f [] (y::ys) _ refl q impossible
@@ -204,18 +279,22 @@ zipWith3 f [] [] [] p q = []
204zipWith3 f (x::xs) (y::ys) (z::zs) p q =
279zipWith3 f (x::xs) (y::ys) (z::zs) p q =
205 f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')
280 f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')
282+||| Combine two lists elementwise into pairs
207zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)
283zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)
208zip = zipWith (\x => \y => (x, y))
284zip = zipWith (\x => \y => (x, y))
286+||| Combine three lists elementwise into tuples
210zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) ->
287zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) ->
211 (length y = length z) -> List (a, b, c)
288 (length y = length z) -> List (a, b, c)
212zip3 = zipWith3 (\x => \y => \z => (x, y, z))
289zip3 = zipWith3 (\x => \y => \z => (x, y, z))
291+||| Split a list of pairs into two lists
214unzip : List (a, b) -> (List a, List b)
292unzip : List (a, b) -> (List a, List b)
215unzip [] = ([], [])
293unzip [] = ([], [])
216unzip ((l, r)::xs) with (unzip xs)
294unzip ((l, r)::xs) with (unzip xs)
217 | (lefts, rights) = (l::lefts, r::rights)
295 | (lefts, rights) = (l::lefts, r::rights)
297+||| Split a list of triples into three lists
219unzip3 : List (a, b, c) -> (List a, List b, List c)
298unzip3 : List (a, b, c) -> (List a, List b, List c)
220unzip3 [] = ([], [], [])
299unzip3 [] = ([], [], [])
221unzip3 ((l, c, r)::xs) with (unzip3 xs)
300unzip3 ((l, c, r)::xs) with (unzip3 xs)
@@ -225,6 +304,8 @@ unzip3 ((l, c, r)::xs) with (unzip3 xs)
226--------------------------------------------------------------------------------
305--------------------------------------------------------------------------------
307+||| Apply a partial function to the elements of a list, keeping the ones at which
228mapMaybe : (a -> Maybe b) -> List a -> List b
309mapMaybe : (a -> Maybe b) -> List a -> List b
229mapMaybe f [] = []
310mapMaybe f [] = []
230mapMaybe f (x::xs) =
311mapMaybe f (x::xs) =
@@ -236,6 +317,7 @@ mapMaybe f (x::xs) =
237--------------------------------------------------------------------------------
318--------------------------------------------------------------------------------
320+||| A tail recursive right fold on Lists.
239total foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> List t -> acc
321total foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> List t -> acc
240foldrImpl f e go [] = go e
322foldrImpl f e go [] = go e
241foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
323foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
@@ -247,6 +329,7 @@ instance Foldable List where
247-- Special folds
329-- Special folds
248--------------------------------------------------------------------------------
330--------------------------------------------------------------------------------
332+||| Convert any Foldable structure to a list.
250toList : Foldable t => t a -> List a
333toList : Foldable t => t a -> List a
251toList = foldr (::) []
334toList = foldr (::) []
@@ -254,6 +337,7 @@ toList = foldr (::) []
254-- Transformations
337-- Transformations
255--------------------------------------------------------------------------------
338--------------------------------------------------------------------------------
340+||| Return the elements of a list in reverse order.
257reverse : List a -> List a
341reverse : List a -> List a
258reverse = reverse' []
342reverse = reverse' []
@@ -261,6 +345,7 @@ reverse = reverse' []
261 reverse' acc [] = acc
345 reverse' acc [] = acc
262 reverse' acc (x::xs) = reverse' (x::acc) xs
346 reverse' acc (x::xs) = reverse' (x::acc) xs
348+||| Insert some separator between the elements of a list.
264intersperse : a -> List a -> List a
349intersperse : a -> List a -> List a
265intersperse sep [] = []
350intersperse sep [] = []
266intersperse sep (x::xs) = x :: intersperse' sep xs
351intersperse sep (x::xs) = x :: intersperse' sep xs
@@ -274,13 +359,13 @@ intercalate sep l = concat $ intersperse sep l
275||| Transposes rows and columns of a list of lists.
360||| Transposes rows and columns of a list of lists.
277−||| > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]
362+||| > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]
279||| This also works for non square scenarios, thus
364||| This also works for non square scenarios, thus
280||| involution does not always hold:
365||| involution does not always hold:
282−||| > transpose [[], [1, 2]] = [[1], [2]]
367+||| > transpose [[], [1, 2]] = [[1], [2]]
283−||| > transpose (transpose [[], [1, 2]]) = [[1, 2]]
368+||| > transpose (transpose [[], [1, 2]]) = [[1, 2]]
285||| TODO: Solution which satisfies the totality checker?
370||| TODO: Solution which satisfies the totality checker?
286%assert_total
371%assert_total
@@ -293,6 +378,7 @@ transpose ((x::xs) :: xss) = (x :: (mapMaybe head' xss)) :: (transpose (xs :: (m
293-- Membership tests
378-- Membership tests
294--------------------------------------------------------------------------------
379--------------------------------------------------------------------------------
381+||| Check if something is a member of a list using a custom comparison.
296elemBy : (a -> a -> Bool) -> a -> List a -> Bool
382elemBy : (a -> a -> Bool) -> a -> List a -> Bool
297elemBy p e [] = False
383elemBy p e [] = False
298elemBy p e (x::xs) =
384elemBy p e (x::xs) =
@@ -301,9 +387,11 @@ elemBy p e (x::xs) =
302 elemBy p e xs
388 elemBy p e xs
390+||| Check if something is a member of a list using the default Boolean equality.
304elem : Eq a => a -> List a -> Bool
391elem : Eq a => a -> List a -> Bool
305elem = elemBy (==)
392elem = elemBy (==)
394+||| Find associated information in a list using a custom comparison.
307lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
395lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
308lookupBy p e [] = Nothing
396lookupBy p e [] = Nothing
309lookupBy p e (x::xs) =
397lookupBy p e (x::xs) =
@@ -313,9 +401,12 @@ lookupBy p e (x::xs) =
314 lookupBy p e xs
402 lookupBy p e xs
404+||| Find associated information in a list using Boolean equality.
316lookup : Eq a => a -> List (a, b) -> Maybe b
405lookup : Eq a => a -> List (a, b) -> Maybe b
317lookup = lookupBy (==)
406lookup = lookupBy (==)
408+||| Check if any elements of the first list are found in the second, using
409+||| a custom comparison.
319hasAnyBy : (a -> a -> Bool) -> List a -> List a -> Bool
410hasAnyBy : (a -> a -> Bool) -> List a -> List a -> Bool
320hasAnyBy p elems [] = False
411hasAnyBy p elems [] = False
321hasAnyBy p elems (x::xs) =
412hasAnyBy p elems (x::xs) =
@@ -324,6 +415,8 @@ hasAnyBy p elems (x::xs) =
325 hasAnyBy p elems xs
416 hasAnyBy p elems xs
418+||| Check if any elements of the first list are found in the second, using
419+||| Boolean equality.
327hasAny : Eq a => List a -> List a -> Bool
420hasAny : Eq a => List a -> List a -> Bool
328hasAny = hasAnyBy (==)
421hasAny = hasAnyBy (==)
@@ -331,6 +424,7 @@ hasAny = hasAnyBy (==)
331-- Searching with a predicate
424-- Searching with a predicate
332--------------------------------------------------------------------------------
425--------------------------------------------------------------------------------
427+||| Find the first element of a list that satisfies a predicate, or `Nothing` if none do.
334find : (a -> Bool) -> List a -> Maybe a
428find : (a -> Bool) -> List a -> Maybe a
335find p [] = Nothing
429find p [] = Nothing
336find p (x::xs) =
430find p (x::xs) =
@@ -339,6 +433,8 @@ find p (x::xs) =
340 find p xs
434 find p xs
436+||| Find the index of the first element of a list that satisfies a predicate, or
437+||| `Nothing` if none do.
342findIndex : (a -> Bool) -> List a -> Maybe Nat
438findIndex : (a -> Bool) -> List a -> Maybe Nat
343findIndex = findIndex' Z
439findIndex = findIndex' Z
@@ -350,6 +446,7 @@ findIndex = findIndex' Z
351 findIndex' (S cnt) p xs
447 findIndex' (S cnt) p xs
449+||| Find the indices of all elements that satisfy some predicate.
353findIndices : (a -> Bool) -> List a -> List Nat
450findIndices : (a -> Bool) -> List a -> List Nat
354findIndices = findIndices' Z
451findIndices = findIndices' Z
@@ -403,6 +500,8 @@ nub = nubBy (==)
403-- Splitting and breaking lists
500-- Splitting and breaking lists
404--------------------------------------------------------------------------------
501--------------------------------------------------------------------------------
503+||| Given a list and a predicate, returns a pair consisting of the longest
504+||| prefix of the list that satisfies a predicate and the rest of the list.
406span : (a -> Bool) -> List a -> (List a, List a)
505span : (a -> Bool) -> List a -> (List a, List a)
407span p [] = ([], [])
506span p [] = ([], [])
408span p (x::xs) =
507span p (x::xs) =
@@ -501,6 +600,7 @@ sort xs = let (x, y) = split xs in
501-- Conversions
600-- Conversions
502--------------------------------------------------------------------------------
601--------------------------------------------------------------------------------
603+||| Either return the head of a list, or `Nothing` if it is empty.
504listToMaybe : List a -> Maybe a
604listToMaybe : List a -> Maybe a
505listToMaybe [] = Nothing
605listToMaybe [] = Nothing
506listToMaybe (x::xs) = Just x
606listToMaybe (x::xs) = Just x
@@ -520,7 +620,7 @@ catMaybes (x::xs) =
520-- Properties
620-- Properties
521--------------------------------------------------------------------------------
621--------------------------------------------------------------------------------
523−-- append
623+||| The empty list is a right identity for append.
524appendNilRightNeutral : (l : List a) ->
624appendNilRightNeutral : (l : List a) ->
525 l ++ [] = l
625 l ++ [] = l
526appendNilRightNeutral [] = refl
626appendNilRightNeutral [] = refl
@@ -528,6 +628,7 @@ appendNilRightNeutral (x::xs) =
528 let inductiveHypothesis = appendNilRightNeutral xs in
628 let inductiveHypothesis = appendNilRightNeutral xs in
529 ?appendNilRightNeutralStepCase
629 ?appendNilRightNeutralStepCase
631+||| Appending lists is associative.
531appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
632appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
532 l ++ (c ++ r) = (l ++ c) ++ r
633 l ++ (c ++ r) = (l ++ c) ++ r
533appendAssociative [] c r = refl
634appendAssociative [] c r = refl
@@ -535,7 +636,8 @@ appendAssociative (x::xs) c r =
535 let inductiveHypothesis = appendAssociative xs c r in
636 let inductiveHypothesis = appendAssociative xs c r in
536 ?appendAssociativeStepCase
637 ?appendAssociativeStepCase
538−-- length
639+||| The length of two lists that are appended is the sum of the lengths
640+||| of the input lists.
539lengthAppend : (left : List a) -> (right : List a) ->
641lengthAppend : (left : List a) -> (right : List a) ->
540 length (left ++ right) = length left + length right
642 length (left ++ right) = length left + length right
541lengthAppend [] right = refl
643lengthAppend [] right = refl
@@ -543,7 +645,7 @@ lengthAppend (x::xs) right =
543 let inductiveHypothesis = lengthAppend xs right in
645 let inductiveHypothesis = lengthAppend xs right in
544 ?lengthAppendStepCase
646 ?lengthAppendStepCase
546−-- map
648+||| Mapping a function over a list doesn't change its length.
547mapPreservesLength : (f : a -> b) -> (l : List a) ->
649mapPreservesLength : (f : a -> b) -> (l : List a) ->
548 length (map f l) = length l
650 length (map f l) = length l
549mapPreservesLength f [] = refl
651mapPreservesLength f [] = refl
@@ -551,6 +653,8 @@ mapPreservesLength f (x::xs) =
551 let inductiveHypothesis = mapPreservesLength f xs in
653 let inductiveHypothesis = mapPreservesLength f xs in
552 ?mapPreservesLengthStepCase
654 ?mapPreservesLengthStepCase
656+||| Mapping a function over two lists and appending them is equivalent
657+||| to appending them and then mapping the function.
554mapDistributesOverAppend : (f : a -> b) -> (l : List a) -> (r : List a) ->
658mapDistributesOverAppend : (f : a -> b) -> (l : List a) -> (r : List a) ->
555 map f (l ++ r) = map f l ++ map f r
659 map f (l ++ r) = map f l ++ map f r
556mapDistributesOverAppend f [] r = refl
660mapDistributesOverAppend f [] r = refl
@@ -558,6 +662,7 @@ mapDistributesOverAppend f (x::xs) r =
558 let inductiveHypothesis = mapDistributesOverAppend f xs r in
662 let inductiveHypothesis = mapDistributesOverAppend f xs r in
559 ?mapDistributesOverAppendStepCase
663 ?mapDistributesOverAppendStepCase
665+||| Mapping two functions is the same as mapping their composition.
561mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) ->
666mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) ->
562 map f (map g l) = map (f . g) l
667 map f (map g l) = map (f . g) l
563mapFusion f g [] = refl
668mapFusion f g [] = refl
@@ -565,7 +670,7 @@ mapFusion f g (x::xs) =
565 let inductiveHypothesis = mapFusion f g xs in
670 let inductiveHypothesis = mapFusion f g xs in
566 ?mapFusionStepCase
671 ?mapFusionStepCase
568−-- hasAny
673+||| No list contains an element of the empty list by any predicate.
569hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->
674hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->
570 hasAnyBy p [] l = False
675 hasAnyBy p [] l = False
571hasAnyByNilFalse p [] = refl
676hasAnyByNilFalse p [] = refl
@@ -573,6 +678,7 @@ hasAnyByNilFalse p (x::xs) =
573 let inductiveHypothesis = hasAnyByNilFalse p xs in
678 let inductiveHypothesis = hasAnyByNilFalse p xs in
574 ?hasAnyByNilFalseStepCase
679 ?hasAnyByNilFalseStepCase
681+||| No list contains an element of the empty list.
576hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
682hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
577hasAnyNilFalse l = ?hasAnyNilFalseBody
683hasAnyNilFalse l = ?hasAnyNilFalseBody