\input{lagda-preamble}

\title{Minimisers}

\begin{document}

\maketitle

This file defines a function that finds the smallest element of a
nonempty decidable subset of the natural numbers.  In more detail, the
input consists of
\begin{itemize}
 \item A map \verb+P : ℕ → Set+.  We treat \verb+P n+ as a proposition
  in the usual way, so we can consider the set $S$ of numbers $n$
  such that \verb+P n+ is nonempty.  This is the set whose minimum
  element we wish to find.
 \item A term \verb+P?+ of type \verb+Decidable P+ (which is defined
  in \verb+Relation.Unary+).  This means that for each natural number
  $n$ we have a term \verb+P? n+ which has the form \verb+yes p+ (with
  \verb+p+ of type \verb+P n+) or \verb+no q+ (with \verb+q+ of type
  \verb+¬ P n+).  In other words, \verb+P?+ is a proof that \verb+P+
  is decidable. 
 \item A natural number \verb+n+ and a term \verb+p+ of type \verb+P n+,
  witnessing the fact that $S$ is nonempty.
\end{itemize}

The output consists of
\begin{itemize}
 \item A natural number \verb+n+.
 \item A term \verb+Pn+ of type \verb+P n+, proving that $n\in S$.
 \item A proof that no smaller number lies in $S$.
\end{itemize}

The definition of our function is roughly as follows.
\begin{itemize}
 \item If $0\in S$ then we just have to provide a vacuous proof
  that all smaller numbers are not in $S$.
 \item Otherwise $n$ will be $n'+1$ for some $n'$.  We then find the
  smallest element of the set $S'=\{k\in ℕ : k+1\in S\}$ and add one
  to it.  The main work is just in preparing the auxiliary information
  for $S'$ from the auxiliary information for $S$, and then performing
  the reverse translation for the minimal element.
\end{itemize}
 
We start with the module header and import statements:

\begin{code}

module Extra.Data.Nat.Minimiser where

open import Data.Empty
open import Data.Nat
open import Relation.Nullary
open import Relation.Unary
import Level 

\end{code}

We now define an ℕ-set to be a decidable subset of ℕ, encoded as a
record consisting of terms \verb+P+ and \verb+P?+ as discussed
previously.  As a slight complication, we need to allow for the values
of \verb+P+ to be sets of an arbitrary but specified level \verb+c+,
which is supplied as an implicit argument.  I do not understand all
the issues about levels, but the code below seems to do the job.  

The line \verb+constructor _,_+ just declares an abbreviated syntax
for definining ℕ-sets.  We will see examples below.

\begin{code}
record ℕ-set {c} : Set (Level.suc c) where
  constructor _,_
  field
    P : ℕ → Set c
    P? : Decidable P
\end{code}

We now declare another record type \verb+Minimiser S+ depending on an
ℕ-set $S$.  A term of this type packages the smallest element of $S$
together with evidence that it is the smallest element.

\begin{code}
record Minimiser (S : ℕ-set) : Set where 
  constructor _,_,_
  open ℕ-set S
  field
    n : ℕ
    Pn : P n
    minimal : (k : ℕ) →  (k < n) → ¬ (P k)
\end{code}

We now define a function \verb+0-min+.  This takes an ℕ-set $S$, and a
proof that $0$ is an element of that ℕ-set, and wraps it up with some
trivial data to produce a term of type \verb+Minimiser S+.

\begin{code}
0-min : {S : ℕ-set} → (P0 : (ℕ-set.P S zero)) → Minimiser S
0-min P0 = 0 , P0 , λ k → λ ()
\end{code}

We can now define the function that is the main point of this module.

\begin{code}
minimiser : (S : ℕ-set) → (n : ℕ) → (ℕ-set.P S n) → (Minimiser S)
minimiser S 0 P0 = 0-min P0 
minimiser S (suc m) Q with (ℕ-set.P? S) 0
... | yes P0 = 0-min P0
... | no ¬P0 = suc n′ , P′n′ , minimal where 
    P′ : ℕ → Set
    P′ k = (ℕ-set.P S) (suc k)
    P′? : Decidable P′ 
    P′? k = (ℕ-set.P? S) (suc k)
    S′ : ℕ-set
    S′ = P′ , P′?
    M′ = minimiser S′ m Q
    n′ = Minimiser.n M′
    P′n′ = Minimiser.Pn M′
    minimal′ = Minimiser.minimal M′
    minimal : (k : ℕ) →  (k < suc n′) → ¬ ((ℕ-set.P S) k)
    minimal 0 _ = ¬P0
    minimal (suc k) (s≤s k<n′) = minimal′ k k<n′ 
\end{code}

\end{document}