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 ()))}