module 5-ProofsAboutEquality where
open import Prelude
infixr 5 _++_
_++_ : ∀ {A} → List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
length : ∀ {A} → List A → ℕ
length [] = zero
length (x ∷ xs) = suc (length xs)
-- Let's try proving the theorem
-- length (xs ++ ys) = length xs + length ys
-- But how do you talk about equality in Agda?
-- See _≡_ in Prelude.agda.
-- The proposition we want to prove:
-- ∀{A} (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys
-- Of course, the first thing to do is to do case analysis on xs.
-- Afterwards, there are several ways to proceed.
-- 0. Use congruence.
length-++-0 : ∀{A} (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys
length-++-0 [] ys = refl
length-++-0 (x ∷ xs) ys = cong suc (length-++-0 xs ys)
-- 1. Use rewrite.
length-++-1 : ∀{A} (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys
length-++-1 [] ys = refl
length-++-1 (x ∷ xs) ys rewrite length-++-1 xs ys = refl
-- 2. Use equational reasoning (and cong).
length-++-2 : ∀{A} (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys
length-++-2 [] ys = refl
length-++-2 (x ∷ xs) ys =
length ((x ∷ xs) ++ ys)
≡⟨ refl ⟩
length (x ∷ xs ++ ys)
≡⟨ refl ⟩
suc (length (xs ++ ys))
≡⟨ cong suc (length-++-2 xs ys) ⟩
suc (length xs + length ys)
≡⟨ refl ⟩
suc (length xs) + length ys
≡⟨ refl ⟩
length (x ∷ xs) + length ys □
+-suc : ∀ m n → m + suc n ≡ suc (m + n)
+-suc zero n = refl
+-suc (suc m) n rewrite +-suc m n = refl
+-zero : ∀ n → n ≡ n + zero
+-zero zero = refl
+-zero (suc n) = cong suc (+-zero n)
+-comm : ∀ m n → m + n ≡ n + m
+-comm zero n = +-zero n
+-comm (suc m) n rewrite +-suc n m | +-comm m n = refl
+-assoc : ∀ m n k → m + (n + k) ≡ (m + n) + k
+-assoc zero n k = refl
+-assoc (suc m) n k = cong suc (+-assoc m n k)
sum : List ℕ → ℕ
sum [] = 0
sum (x ∷ xs) = x + sum xs
map : ∀{A B} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs
concat : ∀ {A} → List (List A) → List A
concat [] = []
concat (xs ∷ xss) = xs ++ concat xss
sum-++ : ∀ xs ys → sum (xs ++ ys) ≡ (sum xs + sum ys)
sum-++ = {! !}
sum-concat : ∀ xss → sum (concat xss) ≡ sum (map sum xss)
sum-concat = {! !}
take : ∀ {A} → ℕ → List A → List A
take zero xs = []
take (suc n) [] = []
take (suc n) (x ∷ xs) = x ∷ take n xs
drop : ∀ {A} → ℕ → List A → List A
drop zero xs = xs
drop (suc n) [] = []
drop (suc n) (x ∷ xs) = drop n xs
take-drop : ∀ {A} n (xs : List A) → take n xs ++ drop n xs ≡ xs
take-drop = {! !}
-- Vectors: lists indexed by their lengths
double : ∀ {A n} → Vec A n → Vec A (n + n)
double = {! !}
interleave : ∀ {A m n} → Vec A m → Vec A n → Vec A (m + n)
interleave = {! !}