\documentclass[a4paper]{scrartcl} %include agda.fmt \usepackage[british]{babel} \usepackage[a4paper]{geometry} \usepackage{hyperref} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{autofe} \usepackage{MnSymbol} \DeclareUnicodeCharacter{955}{$\lambda$} \subtitle{VSTTE'10 Competition Problem 3} \title{Searching a Linked List} \author{Jason S. Reich, University of York \\ \url{http://www-users.cs.york.ac.uk/~jason/}} \date{21st August 2010} \begin{document} \maketitle \tableofcontents \section{Introduction} This is a solution to the third problem presented at the VSTTE'10 verification competition. Full details can be found at \url{http://www.macs.hw.ac.uk/vstte10/comp.pdf}. \paragraph{Description:} Given a linked list representation of a list of integers, find the index of the first element that is equal to 0. \paragraph{Properties:} You have to show that the program returns an index $i$ equal to the length of the list if there is no such element. Otherwise, $i$'th element of the list must be equal to 0, and all the preceding elements must be non-zero. \section{Solution} %TODO: This source of this document is an executable Literate Agda program. \subsection{Library Imports} We need to import some things from the standard libaries. Let us import the naturals and vectors. \begin{code} module Search where open import Data.Nat using -- Naturals (ℕ; zero; suc; _+_) open import Data.Vec using -- Vectors (Vec; []; _∷_) \end{code} Equality, reflection, inequality and congruence. \begin{code} open import Relation.Binary.PropositionalEquality using (_≡_; refl; _≢_; cong) \end{code} Product types with unary existentials. \begin{code} open import Data.Product using -- Pairs (_×_; _,_; -- Existential over one variable ∃) \end{code} Sum types too. \begin{code} open import Data.Sum using -- Sums (_⊎_; inj₁; inj₂) \end{code} \subsection{Specification} I'm not sure if this specification would have satisfied the judges. It certainly contains all the information but might be a little too close to the implementation. A datatype expresses the relevant properties where $x ∈ ys\ at\ i$ means a value $x$ is found in vector $ys$ and index $i$. \begin{code} data _∈_at_ (x : ℕ) : ∀{n} → Vec ℕ n → ℕ → Set where here : ∀ {n} {xs : Vec ℕ n} → x ∈ (x ∷ xs) at 0 there : ∀ {n y i} {ys : Vec ℕ n} → x ∈ ys at i → x ∈ (y ∷ ys) at (suc i) \end{code} Two constructors allow us to inhabit this type. The @here@ constructor can be used where the head of a vector is equivalent to the query. This gives an index of zero, here. The @there@ constructor moves further down the vector where a match is made further on, incrementing the index of the search applied to the tail of the vector. A dual type describes the the non-existence of an element. \begin{code} data _∉_ (x : ℕ) : ∀{n} → Vec ℕ n → Set where stop : x ∉ [] nowhere : ∀{n y} {ys : Vec ℕ n} → x ≢ y → x ∉ ys → x ∉ (y ∷ ys) \end{code} These are combined in what looks like a slightly scary specification of search but its not so bad. Piece by piece, there exists an index $i$ such that it \emph{either} (the $\cupplus$ symbol) $x$ occupying $xs$ at index $i$ \emph{or} (the $\times$ symbol) $x$ not existing in $xs$ and the index being equal to the vector length. \begin{code} SearchSpec : ∀{n} → ℕ → Vec ℕ n → Set SearchSpec {n} x xs = ∃ λ i → (x ∈ xs at i) ⊎ ((x ∉ xs) × (i ≡ n)) \end{code} \subsection{Implementation} The @search@ function takes in a vector of naturals and returns an index and the proof the index satisfies the above specification. \begin{code} search : ∀ {n : ℕ} (xs : Vec ℕ n) → SearchSpec 0 xs \end{code} Base case is trivial. Zero cannot be found in an empty vector so the index returned is one. \begin{code} search [] = (0 , inj₂ (stop , refl)) \end{code} On the inductive case, if the head of the list is zero, job done! Return index zero and the proof that it was here. \begin{code} search (zero ∷ xs) = (0 , inj₁ here) \end{code} Otherwise, apply recursively and increment the index. The proof is produced by extending the recursion result with @there@ or @nowhere@ respectively. The @nowhere@ constructor requires the trivial proof that $zero ≢ suc x$ and the extention of the proof that the recursive call returns an index beyond the bounds of the length. \begin{code} search (suc x ∷ xs) with search xs ... | (i , inj₁ prfS) = (suc i , inj₁ (there prfS)) ... | (i , inj₂ (prfS , prf≡)) = (suc i , inj₂ (nowhere (λ ()) prfS , cong suc prf≡)) \end{code} \end{document}