\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}