verified left-pad in agda

leftpad.agda

module HillelVerificationProblems where

open import Data.Nat
open import Data.Nat.Properties.Simple using (+-right-identity; +-comm)
open import Data.List
open import Data.List.All
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality

-- NB. (a ∸ b) is saturating subtraction and (a ⊔ b) is max(a,b).

-- The one-line definition of leftPad is:
leftPad' : ∀{Char : Set} -> Char -> ℕ -> List Char -> List Char
leftPad' c n str = replicate (n ∸ length str) c ++ str
-- Now let's prove this correct.

-- First, we'll need some general lemmas about arithmetic and lists.
+∸=⊔ : ∀ m {n} → m + (n ∸ m) ≡ n ⊔ m
+∸=⊔ zero {zero} = refl
+∸=⊔ zero {suc _} = refl
+∸=⊔ (suc m) {zero} = cong suc (+-right-identity m)
+∸=⊔ (suc m) {suc n} = cong suc (+∸=⊔ m)

module _ {a : Set} {rest : List a} where
  take-++ : ∀{l n} -> n ≡ length l -> take n (l ++ rest) ≡ l
  take-++ {[]} refl = refl
  take-++ {x ∷ l} refl = cong (_∷_ x) (take-++ refl)

  drop-++ : ∀ l {n} -> n ≡ length l -> drop n (l ++ rest) ≡ rest
  drop-++ [] refl = refl
  drop-++ (x ∷ l) refl = drop-++ l refl

all-replicate : ∀{n} {a : Set} {c : a} -> All (_≡_ c) (replicate n c)
all-replicate {zero} = []
all-replicate {suc n} = refl ∷ all-replicate

-- Now let's move on to things specific to leftPad.
module _ {Char : Set} (c : Char) (n : ℕ) (str : List Char) where
  padLen = n ∸ length str
  pad = replicate padLen c
  leftPad = pad ++ str      -- the padded result.

  -- Lemmas.
  length-pad : length pad ≡ padLen
  length-pad = length-replicate padLen

  -- Correctness theorem #1: `leftPad` has the right length.
  leftPadLength : length leftPad ≡ n ⊔ length str
  leftPadLength = begin
       length leftPad
    ≡⟨ length-++ pad ⟩
       length pad + length str
    ≡⟨ cong₂ _+_ length-pad refl ⟩
       padLen + length str
    ≡⟨ +-comm padLen _ ⟩
       length str + padLen
    ≡⟨ +∸=⊔ (length str) ⟩
       n ⊔ length str ∎
    where open ≡-Reasoning

  -- Correctness theorem #2: The initial fragment of `leftPad` is all `c`s.
  initialOk : All (_≡_ c) (take padLen leftPad)
  initialOk = subst (λ r → All _ r) has-padding all-replicate
    where has-padding : pad ≡ take padLen leftPad
          has-padding = sym (take-++ (sym length-pad))

  -- Correctness theorem #3: The final fragment of `leftPad` is `str`.
  finalOk : drop padLen leftPad ≡ str
  finalOk = drop-++ pad (sym length-pad)