open import Data.Nat using (ℕ ; zero ; suc ; _+_) open import Data.List using (List ; [] ; [_] ; _∷_ ; map ; length ; _++_ ; foldr) open import Relation.Binary.PropositionalEquality hiding ([_]) open ≡-Reasoning -- See Relation.Binary.PropositionalEquality.Core: -- https://github.com/agda/agda-stdlib/blob/master/src/Relation/Binary/PropositionalEquality/Core.agda#L90 +-assoc : (x y z : ℕ) → (x + y) + z ≡ x + (y + z) +-assoc zero y z = refl +-assoc (suc x) y z = cong suc (+-assoc x y z) data Tree (A : Set) : Set where Empty : Tree A Node : Tree A → A → Tree A → Tree A flatten : {A : Set} → Tree A → List A flatten Empty = [] flatten (Node l x r) = flatten l ++ [ x ] ++ flatten r size : {A : Set} → Tree A → ℕ size Empty = 0 size (Node l x r) = size l + 1 + size r length-++ : {A : Set} → (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys length-++ [] ys = refl length-++ (x ∷ xs) ys = cong suc (length-++ xs ys) flatten-size : {A : Set} → (t : Tree A) → length (flatten t) ≡ size t flatten-size Empty = refl flatten-size (Node l x r) = begin length (flatten l ++ [ x ] ++ flatten r) ≡⟨ length-++ (flatten l) (x ∷ flatten r) ⟩ length (flatten l) + length ([ x ] ++ flatten r) ≡⟨ cong (λ k → length (flatten l) + k) refl ⟩ length (flatten l) + (length ([ x ]) + length (flatten r)) ≡⟨⟩ -- abbreviation for ≡⟨ refl ⟩ length (flatten l) + (1 + length (flatten r)) ≡⟨ cong (λ k → k + (1 + length (flatten r))) (flatten-size l) ⟩ size l + (1 + length (flatten r)) ≡⟨ cong (λ k → size l + (1 + k)) (flatten-size r) ⟩ size l + (1 + size r) ≡˘⟨ +-assoc (size l) 1 (size r) ⟩ -- C-u C-x = to find out -- about a unicode char -- ≡⟨ sym (+-assoc (size l) 1 (size r)) ⟩ (size l + 1) + size r ∎ -- \qed size-flatten : {A : Set} → (t : Tree A) → size t ≡ length (flatten t) size-flatten t = sym (flatten-size t)