equivalence proofs for header parser

extractLeadingSpaces

module break2 where

open import Function using (id)
open import Data.Bool using (Bool; true; false)
open import Data.Char using (Char)
open import Data.List using (List; []; _∷_; span)
open import Data.Product as P using (_×_; _,_; map)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
open import Data.Char.Classifier


extract-leading-spaces : List Char → List Char × List Char
extract-leading-spaces [] = [] , []
extract-leading-spaces (c ∷ cs) with isSpace c
... | true  = P.map (_∷_ c) id (extract-leading-spaces cs)
... | false = [] , c ∷ cs

els : List Char → List Char × List Char
els = span isSpace

proof : (xs : List Char) → els xs ≡ extract-leading-spaces xs
proof [] = refl
proof (c ∷ cs) with isSpace c
... | true  = cong (P.map (_∷_ c) id) (proof cs)
... | false = refl