Hask.hs

import Data.List (group)

type TimedWord v = [(Int, v)]


ex1 :: TimedWord Float
ex1 = [(1,3.4),(3,2.1),(3,1.9),(5,6.3)]

-- 1
reps :: Int -> [(Int, v)] -> Int
reps t word = go t word 0
  where
    go _ [] c = c
    go t ((t', _):xs) c
      | t == t' = go t xs (c + 1)
      | otherwise = go t xs c

reps' :: Int -> TimedWord v -> Int
reps' t xs = length [ e | (t', e) <- xs, t == t' ]

reps'' :: Int -> TimedWord v -> Int
reps'' t = length . filter (== t). map fst


-- 2
maxReps :: TimedWord v -> Int
maxReps = maximum . map length . group . map fst
--        maximum (map length (group (map fst word)))


-- 3
psum :: Num v => TimedWord v -> TimedWord v
psum t = zip ts (scanl1 (+) vs)
  where
    (ts, vs) = unzip t

Lists2.agda

_++_ : ∀ {A : Set} → List A → List A → List A
[]       ++ ys  =  ys
(x ∷ xs) ++ ys  =  x ∷ (xs ++ ys)


go : ∀ {A : Set} → List A → List A → List A
go [] ys = ys
go (x ∷ xs) ys = go xs (x ∷ ys)

xrev : ∀ {A : Set} → List A → List A
xrev xs = go xs []

app-Nil : ∀ {A : Set} → (xs : List A) →
  xs ++ [] ≡ xs
app-Nil [] = refl
app-Nil (x ∷ xs) =
  begin
    (x ∷ xs) ++ []
  ≡⟨⟩
    x ∷ (xs ++ [])
  ≡⟨ cong (x ∷_) (app-Nil xs) ⟩ -- Applying Induction hypothesis
    x ∷ xs
  ∎

go : ∀ {A : Set} → List A → List A → List A
go [] ys = ys
go (x ∷ xs) ys = go xs (x ∷ ys)

xrev : ∀ {A : Set} → List A → List A
xrev xs = go xs []

go-lemma : ∀ {A : Set} → (xs ys zs : List A) →
  go (go xs ys) zs ≡ go ys (xs ++ zs)
go-lemma [] ys zs =
  begin
    go (go [] ys) zs
  ≡⟨⟩
    go ys zs
  ≡⟨⟩
    go ys ([] ++ zs)
  ∎
go-lemma (x ∷ xs) ys zs =
  begin
    go (go (x ∷ xs) ys) zs
  ≡⟨⟩
    go (go xs (x ∷ ys)) zs
  ≡⟨ go-lemma xs (x ∷ ys) zs ⟩ -- Applying go-lemma
    go (x ∷ ys) (xs ++ zs)
  ≡⟨⟩
    go ys (x ∷ xs ++ zs)
  ∎



xrev-lemma : ∀ {A : Set} → (xs : List A) →
  xrev (xrev xs) ≡ xs
xrev-lemma [] =
  begin
    xrev (xrev [])
  ≡⟨⟩
    xrev []
  ≡⟨⟩
    []
  ∎
xrev-lemma (x ∷ xs) =
  begin
    xrev (xrev (x ∷ xs))
  ≡⟨⟩
    xrev (go (x ∷ xs) [])
  ≡⟨⟩
    xrev (go xs (x ∷ []))
  ≡⟨⟩
    go (go xs (x ∷ [])) []
  ≡⟨ go-lemma xs (x ∷ []) [] ⟩ -- Applying go-lemma
    go (x ∷ []) (xs ++ [])
  ≡⟨⟩
    go [] (x ∷ (xs ++ []))
  ≡⟨⟩
    x ∷ (xs ++ [])
  ≡⟨ cong (x ∷_) (app-Nil xs) ⟩ -- Applying induction hypothesis
    x ∷ xs
  ∎