96 lines
3.0 KiB
Agda
96 lines
3.0 KiB
Agda
module Lists
|
|
|
|
-- From the "Lists" chapter of Programming Language Foundations in Agda
|
|
-- https://plfa.github.io/Lists/
|
|
|
|
data Nat : U where
|
|
Z : Nat
|
|
S : Nat -> Nat
|
|
|
|
infixl 7 _+_
|
|
_+_ : Nat -> Nat -> Nat
|
|
Z + m = m
|
|
S n + m = S (n + m)
|
|
|
|
infixr 3 _::_
|
|
data List : U -> U where
|
|
Nil : {A : U} -> List A
|
|
_::_ : {A : U} -> A -> List A -> List A
|
|
|
|
length : {A : U} -> List A -> Nat
|
|
length Nil = Z
|
|
length (x :: xs) = S (length xs)
|
|
|
|
infixl 2 _++_
|
|
|
|
_++_ : {A : U} -> List A -> List A -> List A
|
|
Nil ++ ys = ys
|
|
x :: xs ++ ys = x :: (xs ++ ys)
|
|
|
|
infixl 1 _≡_
|
|
data _≡_ : {A : U} -> A -> A -> U where
|
|
Refl : {A : U} {a : A} -> a ≡ a
|
|
|
|
sym : {A : U} {a b : A} -> a ≡ b -> b ≡ a
|
|
sym Refl = Refl
|
|
|
|
trans : {A : U} {a b c : A} -> a ≡ b -> b ≡ c -> a ≡ c
|
|
trans Refl x = x
|
|
|
|
replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
|
|
replace p Refl x = x
|
|
|
|
cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
|
|
|
|
length-++ : {A : U} (xs ys : List A) -> length (xs ++ ys) ≡ length xs + length ys
|
|
length-++ Nil ys = Refl
|
|
length-++ (x :: xs) ys = cong S (length-++ xs ys)
|
|
|
|
-- PLFA definition
|
|
reverse : {A : U} -> (xs : List A) -> List A
|
|
reverse Nil = Nil
|
|
reverse (x :: xs) = reverse xs ++ (x :: Nil)
|
|
|
|
++-identity : {A : U} -> (xs : List A) -> xs ++ Nil ≡ xs
|
|
++-identity Nil = Refl
|
|
++-identity (x :: xs) = cong (_::_ x) (++-identity xs)
|
|
|
|
++-associative : {A : U} (xs ys zs : List A) -> xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
|
|
|
|
-- TODO port equational reasoning
|
|
reverse-++-distrib : {A : U} -> (xs ys : List A) -> reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
|
|
reverse-++-distrib Nil ys = sym (++-identity (reverse ys))
|
|
reverse-++-distrib (x :: xs) ys =
|
|
trans (cong (\ z => z ++ (x :: Nil)) (reverse-++-distrib xs ys))
|
|
(sym (++-associative (reverse ys) (reverse xs) (x :: Nil)))
|
|
|
|
-- rewrite version
|
|
reverse-++-distrib' : {A : U} -> (xs ys : List A) -> reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
|
|
reverse-++-distrib' Nil ys = sym (++-identity (reverse ys))
|
|
reverse-++-distrib' {A} (x :: xs) ys =
|
|
replace (\ z => (reverse (xs ++ ys) ++ (x :: Nil)) ≡ z)
|
|
(sym (++-associative (reverse ys) (reverse xs) (x :: Nil)))
|
|
(replace (\ z => (reverse (xs ++ ys)) ++ (x :: Nil) ≡ z ++ (x :: Nil)) (reverse-++-distrib' xs ys) Refl)
|
|
|
|
reverse-involutive : {A : U} -> (xs : List A) -> reverse (reverse xs) ≡ xs
|
|
reverse-involutive Nil = Refl
|
|
reverse-involutive (x :: xs) =
|
|
trans (reverse-++-distrib (reverse xs) (x :: Nil))
|
|
(cong (_::_ x) (reverse-involutive xs))
|
|
|
|
shunt : {A : U} -> List A -> List A -> List A
|
|
shunt Nil ys = ys
|
|
shunt (x :: xs) ys = shunt xs (x :: ys)
|
|
|
|
shunt-reverse : {A : U} (xs ys : List A) -> shunt xs ys ≡ reverse xs ++ ys
|
|
shunt-reverse Nil ys = Refl
|
|
shunt-reverse (x :: xs) ys =
|
|
trans (shunt-reverse xs (x :: ys))
|
|
(++-associative (reverse xs) (x :: Nil) ys)
|
|
|
|
reverse' : {A : U} -> List A -> List A
|
|
reverse' xs = shunt xs Nil
|
|
|
|
reverses : {A : U} → (xs : List A) → reverse' xs ≡ reverse xs
|
|
reverses xs = trans (shunt-reverse xs Nil) (++-identity _)
|