@@ -2,6 +2,7 @@ module prelude.list
22
33import builtins
44
5+import prelude.algebra
56import prelude.maybe
67import prelude.nat
78
@@ -107,6 +108,72 @@ length (x::xs) = 1 + length xs
107108(++) [] right = right
108109(++) (x::xs) right = x :: (xs ++ right)
109110
111+--------------------------------------------------------------------------------
112+-- Instances
113+--------------------------------------------------------------------------------
114+
115+instance (Eq a) => Eq (List a) where
116+ (==) [] [] = True
117+ (==) (x::xs) (y::ys) =
118+ if x == y then
119+ xs == ys
120+ else
121+ False
122+ (==) _ _ = False
123+
124+
125+instance Ord a => Ord (List a) where
126+ compare [] [] = EQ
127+ compare [] _ = LT
128+ compare _ [] = GT
129+ compare (x::xs) (y::ys) =
130+ if x /= y then
131+ compare x y
132+ else
133+ compare xs ys
134+
135+instance Semigroup (List a) where
136+ (<+>) = (++)
137+
138+instance Monoid (List a) where
139+ neutral = []
140+
141+-- XXX: unification failure
142+-- instance VerifiedSemigroup (List a) where
143+-- semigroupOpIsAssociative = appendAssociative
144+
145+--------------------------------------------------------------------------------
146+-- Zips and unzips
147+--------------------------------------------------------------------------------
148+
149+zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->
150+ (length l = length r) -> List c
151+zipWith f [] [] p = []
152+zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)
153+
154+zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
155+ (z : List c) -> (length x = length y) -> (length y = length z) -> List d
156+zipWith3 f [] [] [] p q = []
157+zipWith3 f (x::xs) (y::ys) (z::zs) p q =
158+ f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')
159+
160+zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)
161+zip = zipWith (\x => \y => (x, y))
162+
163+zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) ->
164+ (length y = length z) -> List (a, b, c)
165+zip3 = zipWith3 (\x => \y => \z => (x, y, z))
166+
167+unzip : List (a, b) -> (List a, List b)
168+unzip [] = ([], [])
169+unzip ((l, r)::xs) with (unzip xs)
170+ | (lefts, rights) = (l::lefts, r::rights)
171+
172+unzip3 : List (a, b, c) -> (List a, List b, List c)
173+unzip3 [] = ([], [], [])
174+unzip3 ((l, c, r)::xs) with (unzip3 xs)
175+ | (lefts, centres, rights) = (l::lefts, c::centres, r::rights)
176+
110177--------------------------------------------------------------------------------
111178-- Maps
112179--------------------------------------------------------------------------------
@@ -138,8 +205,12 @@ foldr f e (x::xs) = f x (foldr f e xs)
138205-- Special folds
139206--------------------------------------------------------------------------------
140207
208+mconcat : Monoid a => List a -> a
209+mconcat = foldr (<+>) neutral
210+
141211concat : List (List a) -> List a
142−concat = foldr (++) []
212+concat [] = []
213+concat (x::xs) = x ++ concat xs
143214
144215concatMap : (a -> List b) -> List a -> List b
145216concatMap f [] = []
@@ -403,31 +474,33 @@ catMaybes (x::xs) =
403474 Just j => j :: catMaybes xs
404475
405476--------------------------------------------------------------------------------
406−-- Instances
477+-- Properties
407478--------------------------------------------------------------------------------
408479
409−instance (Eq a) => Eq (List a) where
410− (==) [] [] = True
411− (==) (a::restA) (b::restB) =
412− if a == b
413− then restA == restB
414− else False
415− (==) _ _ = False
416−
480+-- append
481+appendNilRightNeutral : (l : List a) ->
482+ l ++ [] = l
483+appendNilRightNeutral [] = refl
484+appendNilRightNeutral (x::xs) =
485+ let inductiveHypothesis = appendNilRightNeutral xs in
486+ ?appendNilRightNeutralStepCase
417487
418−instance Ord a => Ord (List a) where
419− compare [] [] = EQ
420− compare [] _ = LT
421− compare _ [] = GT
422− compare (a::restA) (b::restB) =
423− if a /= b
424− then compare a b
425− else compare restA restB
488+appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
489+ l ++ (c ++ r) = (l ++ c) ++ r
490+appendAssociative [] c r = refl
491+appendAssociative (x::xs) c r =
492+ let inductiveHypothesis = appendAssociative xs c r in
493+ ?appendAssociativeStepCase
426494
427−--------------------------------------------------------------------------------
428−-- Properties
429−--------------------------------------------------------------------------------
495+-- length
496+lengthAppend : (left : List a) -> (right : List a) ->
497+ length (left ++ right) = length left + length right
498+lengthAppend [] right = refl
499+lengthAppend (x::xs) right =
500+ let inductiveHypothesis = lengthAppend xs right in
501+ ?lengthAppendStepCase
430502
503+-- map
431504mapPreservesLength : (f : a -> b) -> (l : List a) ->
432505 length (map f l) = length l
433506mapPreservesLength f [] = refl
@@ -449,20 +522,7 @@ mapFusion f g (x::xs) =
449522 let inductiveHypothesis = mapFusion f g xs in
450523 ?mapFusionStepCase
451524
452−appendNilRightNeutral : (l : List a) ->
453− l ++ [] = l
454−appendNilRightNeutral [] = refl
455−appendNilRightNeutral (x::xs) =
456− let inductiveHypothesis = appendNilRightNeutral xs in
457− ?appendNilRightNeutralStepCase
458−
459−appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
460− (l ++ c) ++ r = l ++ (c ++ r)
461−appendAssociative [] c r = refl
462−appendAssociative (x::xs) c r =
463− let inductiveHypothesis = appendAssociative xs c r in
464− ?appendAssociativeStepCase
465−
525+-- hasAny
466526hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->
467527 hasAnyBy p [] l = False
468528hasAnyByNilFalse p [] = refl
@@ -470,16 +530,9 @@ hasAnyByNilFalse p (x::xs) =
470530 let inductiveHypothesis = hasAnyByNilFalse p xs in
471531 ?hasAnyByNilFalseStepCase
472532
473−lengthAppend : (left : List a) -> (right : List a) ->
474− length (left ++ right) = length left + length right
475−lengthAppend [] right = refl
476−lengthAppend (x::xs) right =
477− let inductiveHypothesis = lengthAppend xs right in
478− ?lengthAppendStepCase
479−
480533hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
481534hasAnyNilFalse l = ?hasAnyNilFalseBody
482−
535+
483536--------------------------------------------------------------------------------
484537-- Proofs
485538--------------------------------------------------------------------------------
@@ -542,3 +595,21 @@ mapPreservesLengthStepCase = proof {
542595 trivial;
543596}
544597
598+zipWithTailProof = proof {
599+ intros;
600+ rewrite (succInjective (length xs) (length ys) p);
601+ trivial;
602+}
603+
604+zipWith3TailProof = proof {
605+ intros;
606+ rewrite (succInjective (length xs) (length ys) p);
607+ trivial;
608+}
609+
610+zipWith3TailProof' = proof {
611+ intros;
612+ rewrite (succInjective (length ys) (length zs) q);
613+ trivial;
614+}
615+