module PLFA.Lists where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning
open import Data.Bool using (Bool; true; false; T; _∧_; _∨_; not)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
open import Data.Nat.Properties using
(+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Function using (_∘_)
open import Level using (Level)
open import PLFA.Isomorphism using (_≃_)
-- not exported by Isomorphism:
record _⇔_ (A B : Set) : Set where
field
to : A → B
from : B → A
----------------------------------------------------------------------
data List (A : Set) : Set where
[] : List A -- empty list, no matter what A
_∷_ : A → List A → List A -- non-empty list, with head element of type A
-- ... and tail of type List A
infixr 5 _∷_ -- called `cons`
l0 : List ℕ
l0 = []
l1 : List ℕ
l1 = 1 ∷ [] -- one element list
l2 : List ℕ
l2 = 1 ∷ (2 ∷ []) -- two element lists
{- why the _∷_ operator is right associative:
type error:
lbad : List ℕ
lbad = (1 ∷ 2)
-}
-- tell Agda to use a more efficient internal represenation for lists
{-# BUILTIN LIST List #-}
-- wouldn't it be nice to write [], [ 1 ], [ 1 , 2 ] etc for lists of fixed length?
-- yes, I assume...
{- to use a notation only in expressions, a function definition is sufficient:
[_] : ∀ {A : Set} → A → List A
[_] z = z ∷ []
_ : List ℕ
_ = [ 1 ]
-}
-- but this way, we can also use it in patterns
pattern [_] z = z ∷ []
pattern [_,_] y z = y ∷ z ∷ []
pattern [_,_,_] x y z = x ∷ y ∷ z ∷ []
pattern [_,_,_,_] w x y z = w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_] v w x y z = v ∷ w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_,_] u v w x y z = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []
_ : List ℕ
_ = [ 1 , 2 , 3 , 4 , 5 ]
-- * -- appending two lists (or concatenating lists)
infixr 5 _++_
_++_ : ∀ {A : Set} → List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
++-assoc : ∀ {A : Set} → (xs ys zs : List A) →
(xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc [] ys zs = refl
++-assoc (x ∷ xs) ys zs rewrite ++-assoc xs ys zs = refl
++-identityˡ : ∀ {A : Set} → (xs : List A) →
[] ++ xs ≡ xs
++-identityˡ xs = refl
++-identityʳ : ∀ {A : Set} → (xs : List A) →
xs ++ [] ≡ xs
++-identityʳ [] = refl
++-identityʳ (x ∷ xs) rewrite ++-identityʳ xs = refl
-- * -- length of a list
length : ∀ {A : Set} → List A → ℕ
length [] = 0
length (x ∷ xs) = suc (length xs)
_ : length [ 2 , 3 , 4 ] ≡ 3
_ = refl
length-++ : ∀ {A : Set} → (xs ys : List A) →
length (xs ++ ys) ≡ length xs + length ys
-- lhs: length ([] ++ ys) ≡ length ys
-- rhs: length [] + length ys ≡ 0 + length ys ≡ length ys
length-++ [] ys = refl
length-++ (x ∷ xs) ys rewrite length-++ xs ys = refl
-- * -- reverse a list
reverse : ∀ {A : Set} → List A → List A
reverse [] = []
reverse (x ∷ xs) = reverse xs ++ [ x ]
_ : reverse [ 1 , 2 , 3 ] ≡ [ 3 , 2 , 1 ]
_ = refl
{-
this reverse function is inefficient because given an input list of length n
it appends an element to lists of length 0 , 1, 2, 3, ... n-1
adds up to a quadratic run time!
Can we speed up? Yes:
-}
shunt : ∀ {A : Set} → List A → List A → List A
shunt [] ys = ys
shunt (x ∷ xs) ys = shunt xs (x ∷ ys)
shunt-reverse : ∀ {A : Set} (xs ys : List A) →
shunt xs ys ≡ reverse xs ++ ys
shunt-reverse [] ys = refl
shunt-reverse (x ∷ xs) ys = sym (
begin
reverse (x ∷ xs) ++ ys
≡⟨ ++-assoc (reverse xs) [ x ] ys ⟩
sym (shunt-reverse xs (x ∷ ys)) )
reverse′ : ∀ {A : Set} → List A → List A
reverse′ xs = shunt xs []
reverses== : ∀ {A : Set} → (xs : List A) →
reverse xs ≡ reverse′ xs
reverses== xs = sym (
begin
reverse′ xs
≡⟨⟩
shunt xs []
≡⟨ shunt-reverse xs [] ⟩
reverse xs ++ []
≡⟨ ++-identityʳ (reverse xs) ⟩
reverse xs
∎)
--------------------------------------------------
-- end part 1
--------------------------------------------------
-- * -- map
-- idea: take a function, a list, apply the function to all elements of the list
variable
A B : Set
map : (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs
_ : map suc [ 1 , 2 , 3 ] ≡ [ 2 , 3 , 4 ]
_ = refl
-- * -- fold
-- idea: given a list ( x1 ∷ x2 ∷ x3 ∷ [] ) : List A
-- and a seed value 𝟙 : B
-- and a combination function _⊗_ : A → B → B
-- evaluate: ( x1 ⊗ x2 ⊗ x3 ⊗ 𝟙 ) : B
fold : (A → B → B) → B → List A → B
fold _⊗_ 𝟙 [] = 𝟙
fold _⊗_ 𝟙 (x ∷ xs) = x ⊗ (fold _⊗_ 𝟙 xs)
-- application to calculate the sum of a list of numbers
_ : fold _+_ 0 [ 1 , 2 , 3 , 4 ] ≡ 10
_ = refl
sum : List ℕ → ℕ
sum = fold _+_ 0
fold-cons-nil=id : ∀ (xs : List A) → fold _∷_ [] xs ≡ xs
fold-cons-nil=id [] = refl
fold-cons-nil=id (x ∷ xs) rewrite fold-cons-nil=id xs = refl
length' : List A → ℕ
length' = fold (λ a n → suc n) 0
length=length' : ∀ (xs : List A) → length xs ≡ length' xs
length=length' [] = refl
length=length' (x ∷ xs) rewrite length=length' xs = refl
-- * -- monoids
-- a monoid is a structure with a carrier set A
-- and operations
-- 𝟙 : A
-- _⊙_ : A → A → A
-- obeying the laws of
-- * left identity
-- * right identity
-- * associativity
record IsMonoid {A : Set} (_⊙_ : A → A → A) (𝟙 : A) : Set where
field
assoc : ∀ (a b c : A) → (a ⊙ b) ⊙ c ≡ a ⊙ (b ⊙ c)
identityˡ : ∀ (a : A) → 𝟙 ⊙ a ≡ a
identityʳ : ∀ (a : A) → a ⊙ 𝟙 ≡ a
open IsMonoid
+-monoid : IsMonoid _+_ 0
+-monoid = record {
assoc = +-assoc ;
identityˡ = +-identityˡ ;
identityʳ = +-identityʳ
}
*-monoid : IsMonoid _*_ 1
*-monoid = record {
assoc = *-assoc ;
identityˡ = *-identityˡ ;
identityʳ = *-identityʳ
}
++-monoid : IsMonoid{List B} _++_ []
++-monoid = record {
assoc = ++-assoc ;
identityˡ = ++-identityˡ ;
identityʳ = ++-identityʳ
}
fold-monoid :
(_⊙_ : A → A → A) →
(𝟙 : A) →
IsMonoid _⊙_ 𝟙 →
∀ (xs : List A) (y : A) →
fold _⊙_ y xs ≡ (fold _⊙_ 𝟙 xs) ⊙ y
fold-monoid _⊙_ 𝟙 ⊙-monoid [] y = sym (identityˡ ⊙-monoid y)
fold-monoid _⊙_ 𝟙 ⊙-monoid (x ∷ xs) y
rewrite fold-monoid _⊙_ 𝟙 ⊙-monoid xs y = sym (assoc ⊙-monoid x (fold _⊙_ 𝟙 xs) y)
-- * -- predicates that hold for all or for some elements in a list
data All {A : Set} (P : A → Set) : List A → Set where
[] : All P []
_∷_ : ∀ {x : A} {xs : List A} → P x → All P xs → All P (x ∷ xs)
-- All P xs means that P holds for all elements of xs
data Any {A : Set} (P : A → Set) : List A → Set where
here : ∀ {x : A}{xs : List A} → P x → Any P (x ∷ xs)
there : ∀ {x : A}{xs : List A} → Any P xs → Any P (x ∷ xs)
-- Any P xs means that P holds for some element of xs
-- application: presence of an element in a list
infix 4 _∈_ _∉_
_∈_ _∉_ : (x : A) (xs : List A) → Set
x ∈ xs = Any (x ≡_) xs -- (x ≡_) equiv to λ y → x ≡ y
x ∉ xs = ¬ (x ∈ xs)
_ : 2 ∈ [ 1 , 2 , 3 ]
_ = there (here refl)
_ : 3 ∉ [ 1 , 2 ]
_ = λ{ (there (here ())) ;
(there (there ()))}