\documentclass[a4paper,12pt]{article}
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[english]{babel}
\usepackage{color}
\usepackage{footmisc}
\usepackage{graphicx}
%\usepackage{mathpazo}
\usepackage{multicol}
\usepackage{stmaryrd}
%\usepackage[scaled=.85]{beramono}
\usepackage{isabelle,iman,pdfsetup}
%\oddsidemargin=4.6mm
%\evensidemargin=4.6mm
%\textwidth=150mm
%\topmargin=4.6mm
%\headheight=0mm
%\headsep=0mm
%\textheight=234mm
\def\Colon{\mathord{:\mkern-1.5mu:}}
%\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
%\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
\def\lparr{\mathopen{(\mkern-4mu\mid}}
\def\rparr{\mathclose{\mid\mkern-4mu)}}
%\def\unk{{?}}
\def\unk{{\_}}
\def\unkef{(\lambda x.\; \unk)}
\def\undef{(\lambda x.\; \_)}
%\def\unr{\textit{others}}
\def\unr{\ldots}
\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
\hyphenation{Mini-Sat size-change First-Steps grand-parent nit-pick
counter-example counter-examples data-type data-types co-data-type
co-data-types in-duc-tive co-in-duc-tive}
\urlstyle{tt}
\renewcommand\_{\hbox{\textunderscore\kern-.05ex}}
\begin{document}
%%% TYPESETTING
%\renewcommand\labelitemi{$\bullet$}
\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}}
\title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]
Picking Nits \\[\smallskipamount]
\Large A User's Guide to Nitpick for Isabelle/HOL}
\author{\hbox{} \\
Jasmin Blanchette \\
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
\hbox{}}
\maketitle
\tableofcontents
\setlength{\parskip}{.7em plus .2em minus .1em}
\setlength{\parindent}{0pt}
\setlength{\abovedisplayskip}{\parskip}
\setlength{\abovedisplayshortskip}{.9\parskip}
\setlength{\belowdisplayskip}{\parskip}
\setlength{\belowdisplayshortskip}{.9\parskip}
% General-purpose enum environment with correct spacing
\newenvironment{enum}%
{\begin{list}{}{%
\setlength{\topsep}{.1\parskip}%
\setlength{\partopsep}{.1\parskip}%
\setlength{\itemsep}{\parskip}%
\advance\itemsep by-\parsep}}
{\end{list}}
\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
\advance\rightskip by\leftmargin}
\def\post{\vskip0pt plus1ex\endgroup}
\def\prew{\pre\advance\rightskip by-\leftmargin}
\def\postw{\post}
\section{Introduction}
\label{introduction}
Nitpick \cite{blanchette-nipkow-2010} is a counterexample generator for
Isabelle/HOL \cite{isa-tutorial} that is designed to handle formulas
combining (co)in\-duc\-tive datatypes, (co)in\-duc\-tively defined predicates, and
quantifiers. It builds on Kodkod \cite{torlak-jackson-2007}, a highly optimized
first-order relational model finder developed by the Software Design Group at
MIT. It is conceptually similar to Refute \cite{weber-2008}, from which it
borrows many ideas and code fragments, but it benefits from Kodkod's
optimizations and a new encoding scheme. The name Nitpick is shamelessly
appropriated from a now retired Alloy precursor.
Nitpick is easy to use---you simply enter \textbf{nitpick} after a putative
theorem and wait a few seconds. Nonetheless, there are situations where knowing
how it works under the hood and how it reacts to various options helps
increase the test coverage. This manual also explains how to install the tool on
your workstation. Should the motivation fail you, think of the many hours of
hard work Nitpick will save you. Proving non-theorems is \textsl{hard work}.
Another common use of Nitpick is to find out whether the axioms of a locale are
satisfiable, while the locale is being developed. To check this, it suffices to
write
\prew
\textbf{lemma}~``$\textit{False\/}$'' \\
\textbf{nitpick}~[\textit{show\_all}]
\postw
after the locale's \textbf{begin} keyword. To falsify \textit{False}, Nitpick
must find a model for the axioms. If it finds no model, we have an indication
that the axioms might be unsatisfiable.
Nitpick provides an automatic mode that can be enabled via the ``Auto Nitpick''
option under ``Plugins > Plugin Options > Isabelle > General'' in
Isabelle/jEdit. In this mode, Nitpick is run on every newly entered theorem.
\newbox\boxA
\setbox\boxA=\hbox{\texttt{nospam}}
\newcommand\authoremail{\texttt{jasmin.blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
inria\allowbreak .\allowbreak fr}}
To run Nitpick, you must also make sure that the theory \textit{Nitpick} is
imported---this is rarely a problem in practice since it is part of
\textit{Main}. The examples presented in this manual can be found
in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_\allowbreak Examples/\allowbreak Manual\_Nits.thy} theory.
The known bugs and limitations at the time of writing are listed in
\S\ref{known-bugs-and-limitations}. Comments and bug reports concerning
the tool or the manual should be directed to the author at \authoremail.
\vskip2.5\smallskipamount
\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
suggesting several textual improvements.
% and Perry James for reporting a typo.
\section{Installation}
\label{installation}
Nitpick is part of Isabelle, so you do not need to install it. It relies on a
third-party Kodkod front-end called Kodkodi, which in turn requires a Java
virtual machine. Both are provided as official Isabelle components.
%There are two main ways of installing Kodkodi:
%
%\begin{enum}
%\item[\labelitemi] If you installed an official Isabelle package,
%it should already include a properly setup version of Kodkodi.
%
%\item[\labelitemi] If you use a repository or snapshot version of Isabelle, you
%an official Isabelle package, you can download the Isabelle-aware Kodkodi package
%from \url{http://www21.in.tum.de/~blanchet/\#software}. Extract the archive, then add a
%line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}%
%\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
%startup. Its value can be retrieved by executing \texttt{isabelle}
%\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
%file with the absolute path to Kodkodi. For example, if the
%\texttt{components} file does not exist yet and you extracted Kodkodi to
%\texttt{/usr/local/kodkodi-1.5.2}, create it with the single line
%
%\prew
%\texttt{/usr/local/kodkodi-1.5.2}
%\postw
%
%(including an invisible newline character) in it.
%\end{enum}
To check whether Kodkodi is successfully installed, you can try out the example
in \S\ref{propositional-logic}.
\section{First Steps}
\label{first-steps}
This section introduces Nitpick by presenting small examples. If possible, you
should try out the examples on your workstation. Your theory file should start
as follows:
\prew
\textbf{theory}~\textit{Scratch} \\
\textbf{imports}~\textit{Main~Quotient\_Product~RealDef} \\
\textbf{begin}
\postw
The results presented here were obtained using the JNI (Java Native Interface)
version of MiniSat and with multithreading disabled to reduce nondeterminism.
This was done by adding the line
\prew
\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1]
\postw
after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
Kodkodi and is precompiled for Linux, Mac~OS~X, and Windows (Cygwin). Other SAT
solvers can also be used, as explained in \S\ref{optimizations}. If you
have already configured SAT solvers in Isabelle (e.g., for Refute), these will
also be available to Nitpick.
\subsection{Propositional Logic}
\label{propositional-logic}
Let's start with a trivial example from propositional logic:
\prew
\textbf{lemma}~``$P \longleftrightarrow Q$'' \\
\textbf{nitpick}
\postw
You should get the following output:
\prew
\slshape
Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $P = \textit{True}$ \\
\hbox{}\qquad\qquad $Q = \textit{False}$
\postw
Nitpick can also be invoked on individual subgoals, as in the example below:
\prew
\textbf{apply}~\textit{auto} \\[2\smallskipamount]
{\slshape goal (2 subgoals): \\
\phantom{0}1. $P\,\Longrightarrow\, Q$ \\
\phantom{0}2. $Q\,\Longrightarrow\, P$} \\[2\smallskipamount]
\textbf{nitpick}~1 \\[2\smallskipamount]
{\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $P = \textit{True}$ \\
\hbox{}\qquad\qquad $Q = \textit{False}$} \\[2\smallskipamount]
\textbf{nitpick}~2 \\[2\smallskipamount]
{\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $P = \textit{False}$ \\
\hbox{}\qquad\qquad $Q = \textit{True}$} \\[2\smallskipamount]
\textbf{oops}
\postw
\subsection{Type Variables}
\label{type-variables}
If you are left unimpressed by the previous example, don't worry. The next
one is more mind- and computer-boggling:
\prew
\textbf{lemma} ``$x \in A\,\Longrightarrow\, (\textrm{THE}~y.\;y \in A) \in A$''
\postw
\pagebreak[2] %% TYPESETTING
The putative lemma involves the definite description operator, {THE}, presented
in section 5.10.1 of the Isabelle tutorial \cite{isa-tutorial}. The
operator is defined by the axiom $(\textrm{THE}~x.\; x = a) = a$. The putative
lemma is merely asserting the indefinite description operator axiom with {THE}
substituted for {SOME}.
The free variable $x$ and the bound variable $y$ have type $'a$. For formulas
containing type variables, Nitpick enumerates the possible domains for each type
variable, up to a given cardinality (10 by default), looking for a finite
countermodel:
\prew
\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
\slshape
Trying 10 scopes: \nopagebreak \\
\hbox{}\qquad \textit{card}~$'a$~= 1; \\
\hbox{}\qquad \textit{card}~$'a$~= 2; \\
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
\hbox{}\qquad \textit{card}~$'a$~= 10 \\[2\smallskipamount]
Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $A = \{a_2,\, a_3\}$ \\
\hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount]
Total time: 963 ms
\postw
Nitpick found a counterexample in which $'a$ has cardinality 3. (For
cardinalities 1 and 2, the formula holds.) In the counterexample, the three
values of type $'a$ are written $a_1$, $a_2$, and $a_3$.
The message ``Trying $n$ scopes: {\ldots}''\ is shown only if the option
\textit{verbose} is enabled. You can specify \textit{verbose} each time you
invoke \textbf{nitpick}, or you can set it globally using the command
\prew
\textbf{nitpick\_params} [\textit{verbose}]
\postw
This command also displays the current default values for all of the options
supported by Nitpick. The options are listed in \S\ref{option-reference}.
\subsection{Constants}
\label{constants}
By just looking at Nitpick's output, it might not be clear why the
counterexample in \S\ref{type-variables} is genuine. Let's invoke Nitpick again,
this time telling it to show the values of the constants that occur in the
formula:
\prew
\textbf{lemma} ``$x \in A\,\Longrightarrow\, (\textrm{THE}~y.\;y \in A) \in A$'' \\
\textbf{nitpick}~[\textit{show\_consts}] \\[2\smallskipamount]
\slshape
Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $A = \{a_2,\, a_3\}$ \\
\hbox{}\qquad\qquad $x = a_3$ \\
\hbox{}\qquad Constant: \nopagebreak \\
\hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;y \in A = a_1$
\postw
As the result of an optimization, Nitpick directly assigned a value to the
subterm $\textrm{THE}~y.\;y \in A$, rather than to the \textit{The} constant. We
can disable this optimization by using the command
\prew
\textbf{nitpick}~[\textit{dont\_specialize},\, \textit{show\_consts}]
\postw
Our misadventures with THE suggest adding `$\exists!x{.}$' (``there exists a
unique $x$ such that'') at the front of our putative lemma's assumption:
\prew
\textbf{lemma} ``$\exists {!}x.\; x \in A\,\Longrightarrow\, (\textrm{THE}~y.\;y \in A) \in A$''
\postw
The fix appears to work:
\prew
\textbf{nitpick} \\[2\smallskipamount]
\slshape Nitpick found no counterexample
\postw
We can further increase our confidence in the formula by exhausting all
cardinalities up to 50:
\prew
\textbf{nitpick} [\textit{card} $'a$~= 1--50]\footnote{The symbol `--'
is entered as \texttt{-} (hyphen).} \\[2\smallskipamount]
\slshape Nitpick found no counterexample.
\postw
Let's see if Sledgehammer can find a proof:
\prew
\textbf{sledgehammer} \\[2\smallskipamount]
{\slshape Sledgehammer: ``$e$'' on goal \\
Try this: \textbf{by}~(\textit{metis~theI}) (42 ms)} \\
\hbox{}\qquad\vdots \\[2\smallskipamount]
\textbf{by}~(\textit{metis~theI\/})
\postw
This must be our lucky day.
\subsection{Skolemization}
\label{skolemization}
Are all invertible functions onto? Let's find out:
\prew
\textbf{lemma} ``$\exists g.\; \forall x.~g~(f~x) = x
\,\Longrightarrow\, \forall y.\; \exists x.~y = f~x$'' \\
\textbf{nitpick} \\[2\smallskipamount]
\slshape
Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\[2\smallskipamount]
\hbox{}\qquad Free variable: \nopagebreak \\
\hbox{}\qquad\qquad $f = \undef{}(b_1 := a_1)$ \\
\hbox{}\qquad Skolem constants: \nopagebreak \\
\hbox{}\qquad\qquad $g = \undef{}(a_1 := b_1,\> a_2 := b_1)$ \\
\hbox{}\qquad\qquad $y = a_2$
\postw
(The Isabelle/HOL notation $f(x := y)$ denotes the function that maps $x$ to $y$
and that otherwise behaves like $f$.)
Although $f$ is the only free variable occurring in the formula, Nitpick also
displays values for the bound variables $g$ and $y$. These values are available
to Nitpick because it performs skolemization as a preprocessing step.
In the previous example, skolemization only affected the outermost quantifiers.
This is not always the case, as illustrated below:
\prew
\textbf{lemma} ``$\exists x.\; \forall f.\; f~x = x$'' \\
\textbf{nitpick} \\[2\smallskipamount]
\slshape
Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
\hbox{}\qquad Skolem constant: \nopagebreak \\
\hbox{}\qquad\qquad $\lambda x.\; f =
\undef{}(\!\begin{aligned}[t]
& a_1 := \undef{}(a_1 := a_2,\> a_2 := a_1), \\[-2pt]
& a_2 := \undef{}(a_1 := a_1,\> a_2 := a_1))\end{aligned}$
\postw
The variable $f$ is bound within the scope of $x$; therefore, $f$ depends on
$x$, as suggested by the notation $\lambda x.\,f$. If $x = a_1$, then $f$ is the
function that maps $a_1$ to $a_2$ and vice versa; otherwise, $x = a_2$ and $f$
maps both $a_1$ and $a_2$ to $a_1$. In both cases, $f~x \not= x$.
The source of the Skolem constants is sometimes more obscure:
\prew
\textbf{lemma} ``$\mathit{refl}~r\,\Longrightarrow\, \mathit{sym}~r$'' \\
\textbf{nitpick} \\[2\smallskipamount]
\slshape
Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
\hbox{}\qquad Free variable: \nopagebreak \\
\hbox{}\qquad\qquad $r = \{(a_1, a_1),\, (a_2, a_1),\, (a_2, a_2)\}$ \\
\hbox{}\qquad Skolem constants: \nopagebreak \\
\hbox{}\qquad\qquad $\mathit{sym}.x = a_2$ \\
\hbox{}\qquad\qquad $\mathit{sym}.y = a_1$
\postw
What happened here is that Nitpick expanded \textit{sym} to its definition:
\prew
$\mathit{sym}~r \,\equiv\,
\forall x\> y.\,\> (x, y) \in r \longrightarrow (y, x) \in r.$
\postw
As their names suggest, the Skolem constants $\mathit{sym}.x$ and
$\mathit{sym}.y$ are simply the bound variables $x$ and $y$
from \textit{sym}'s definition.
\subsection{Natural Numbers and Integers}
\label{natural-numbers-and-integers}
Because of the axiom of infinity, the type \textit{nat} does not admit any
finite models. To deal with this, Nitpick's approach is to consider finite
subsets $N$ of \textit{nat} and maps all numbers $\notin N$ to the undefined
value (displayed as `$\unk$'). The type \textit{int} is handled similarly.
Internally, undefined values lead to a three-valued logic.
Here is an example involving \textit{int\/}:
\prew
\textbf{lemma} ``$\lbrakk i \le j;\> n \le (m{\Colon}\mathit{int})\rbrakk \,\Longrightarrow\, i * n + j * m \le i * m + j * n$'' \\
\textbf{nitpick} \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $i = 0$ \\
\hbox{}\qquad\qquad $j = 1$ \\
\hbox{}\qquad\qquad $m = 1$ \\
\hbox{}\qquad\qquad $n = 0$
\postw
Internally, Nitpick uses either a unary or a binary representation of numbers.
The unary representation is more efficient but only suitable for numbers very
close to zero. By default, Nitpick attempts to choose the more appropriate
encoding by inspecting the formula at hand. This behavior can be overridden by
passing either \textit{unary\_ints} or \textit{binary\_ints} as option. For
binary notation, the number of bits to use can be specified using
the \textit{bits} option. For example:
\prew
\textbf{nitpick} [\textit{binary\_ints}, \textit{bits}${} = 16$]
\postw
With infinite types, we don't always have the luxury of a genuine counterexample
and must often content ourselves with a potentially spurious one.
For example:
\prew
\textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
\textbf{nitpick} [\textit{card~nat}~= 50] \\[2\smallskipamount]
\slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
fragment; only potentially spurious counterexamples may be found \\[2\smallskipamount]
Nitpick found a potentially spurious counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variable: \nopagebreak \\
\hbox{}\qquad\qquad $P = \textit{False}$
\postw
The issue is that the bound variable in $\forall n.\;
\textit{Suc}~n \mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds
an $n$ such that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
\textit{False}; but otherwise, it does not know anything about values of $n \ge
\textit{card~nat}$ and must therefore evaluate the assumption to~$\unk$, not
\textit{True}. Since the assumption can never be fully satisfied by Nitpick,
the putative lemma can never be falsified.
Some conjectures involving elementary number theory make Nitpick look like a
giant with feet of clay:
\prew
\textbf{lemma} ``$P~\textit{Suc\/}$'' \\
\textbf{nitpick} \\[2\smallskipamount]
\slshape
Nitpick found no counterexample
\postw
On any finite set $N$, \textit{Suc} is a partial function; for example, if $N =
\{0, 1, \ldots, k\}$, then \textit{Suc} is $\{0 \mapsto 1,\, 1 \mapsto 2,\,
\ldots,\, k \mapsto \unk\}$, which evaluates to $\unk$ when passed as
argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$. The next
example is similar:
\prew
\textbf{lemma} ``$P~(\textit{op}~{+}\Colon
\textit{nat}\mathbin{\Rightarrow}\textit{nat}\mathbin{\Rightarrow}\textit{nat})$'' \\
\textbf{nitpick} [\textit{card nat} = 1] \\[2\smallskipamount]
{\slshape Nitpick found a counterexample:} \\[2\smallskipamount]
\hbox{}\qquad Free variable: \nopagebreak \\
\hbox{}\qquad\qquad $P = \unkef(\unkef(0 := \unkef(0 := 0)) := \mathit{False})$ \\[2\smallskipamount]
\textbf{nitpick} [\textit{card nat} = 2] \\[2\smallskipamount]
{\slshape Nitpick found no counterexample.}
\postw
The problem here is that \textit{op}~+ is total when \textit{nat} is taken to be
$\{0\}$ but becomes partial as soon as we add $1$, because
$1 + 1 \notin \{0, 1\}$.
Because numbers are infinite and are approximated using a three-valued logic,
there is usually no need to systematically enumerate domain sizes. If Nitpick
cannot find a genuine counterexample for \textit{card~nat}~= $k$, it is very
unlikely that one could be found for smaller domains. (The $P~(\textit{op}~{+})$
example above is an exception to this principle.) Nitpick nonetheless enumerates
all cardinalities from 1 to 10 for \textit{nat}, mainly because smaller
cardinalities are fast to handle and give rise to simpler counterexamples. This
is explained in more detail in \S\ref{scope-monotonicity}.
\subsection{Inductive Datatypes}
\label{inductive-datatypes}
Like natural numbers and integers, inductive datatypes with recursive
constructors admit no finite models and must be approximated by a subterm-closed
subset. For example, using a cardinality of 10 for ${'}a~\textit{list}$,
Nitpick looks for all counterexamples that can be built using at most 10
different lists.
Let's see with an example involving \textit{hd} (which returns the first element
of a list) and $@$ (which concatenates two lists):
\prew
\textbf{lemma} ``$\textit{hd}~(\textit{xs} \mathbin{@} [y, y]) = \textit{hd}~\textit{xs\/}$'' \\
\textbf{nitpick} \\[2\smallskipamount]
\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $\textit{xs} = []$ \\
\hbox{}\qquad\qquad $\textit{y} = a_1$
\postw
To see why the counterexample is genuine, we enable \textit{show\_consts}
and \textit{show\_\allowbreak datatypes}:
\prew
{\slshape Type:} \\
\hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_1],\, [a_1, a_1],\, \unr\}$ \\
{\slshape Constants:} \\
\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \unkef([] := [a_1, a_1])$ \\
\hbox{}\qquad $\textit{hd} = \unkef([] := a_2,\> [a_1] := a_1,\> [a_1, a_1] := a_1)$
\postw
Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value,
including $a_2$.
The second constant, $\lambda x_1.\; x_1 \mathbin{@} [y, y]$, is simply the
append operator whose second argument is fixed to be $[y, y]$. Appending $[a_1,
a_1]$ to $[a_1]$ would normally give $[a_1, a_1, a_1]$, but this value is not
representable in the subset of $'a$~\textit{list} considered by Nitpick, which
is shown under the ``Type'' heading; hence the result is $\unk$. Similarly,
appending $[a_1, a_1]$ to itself gives $\unk$.
Given \textit{card}~$'a = 3$ and \textit{card}~$'a~\textit{list} = 3$, Nitpick
considers the following subsets:
\kern-.5\smallskipamount %% TYPESETTING
\prew
\begin{multicols}{3}
$\{[],\, [a_1],\, [a_2]\}$; \\
$\{[],\, [a_1],\, [a_3]\}$; \\
$\{[],\, [a_2],\, [a_3]\}$; \\
$\{[],\, [a_1],\, [a_1, a_1]\}$; \\
$\{[],\, [a_1],\, [a_2, a_1]\}$; \\
$\{[],\, [a_1],\, [a_3, a_1]\}$; \\
$\{[],\, [a_2],\, [a_1, a_2]\}$; \\
$\{[],\, [a_2],\, [a_2, a_2]\}$; \\
$\{[],\, [a_2],\, [a_3, a_2]\}$; \\
$\{[],\, [a_3],\, [a_1, a_3]\}$; \\
$\{[],\, [a_3],\, [a_2, a_3]\}$; \\
$\{[],\, [a_3],\, [a_3, a_3]\}$.
\end{multicols}
\postw
\kern-2\smallskipamount %% TYPESETTING
All subterm-closed subsets of $'a~\textit{list}$ consisting of three values
are listed and only those. As an example of a non-subterm-closed subset,
consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_2]\}$, and observe
that $[a_1, a_2]$ (i.e., $a_1 \mathbin{\#} [a_2]$) has $[a_2] \notin
\mathcal{S}$ as a subterm.
Here's another m\"ochtegern-lemma that Nitpick can refute without a blink:
\prew
\textbf{lemma} ``$\lbrakk \textit{length}~\textit{xs} = 1;\> \textit{length}~\textit{ys} = 1
\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys\/}$''
\\
\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $\textit{xs} = [a_2]$ \\
\hbox{}\qquad\qquad $\textit{ys} = [a_1]$ \\
\hbox{}\qquad Types: \\
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
\hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_1],\, [a_2],\, \unr\}$
\postw
Because datatypes are approximated using a three-valued logic, there is usually
no need to systematically enumerate cardinalities: If Nitpick cannot find a
genuine counterexample for \textit{card}~$'a~\textit{list}$~= 10, it is very
unlikely that one could be found for smaller cardinalities.
\subsection{Typedefs, Quotient Types, Records, Rationals, and Reals}
\label{typedefs-quotient-types-records-rationals-and-reals}
Nitpick generally treats types declared using \textbf{typedef} as datatypes
whose single constructor is the corresponding \textit{Abs\_\kern.1ex} function.
For example:
\prew
\textbf{typedef}~\textit{three} = ``$\{0\Colon\textit{nat},\, 1,\, 2\}$'' \\
\textbf{by}~\textit{blast} \\[2\smallskipamount]
\textbf{definition}~$A \mathbin{\Colon} \textit{three}$ \textbf{where} ``\kern-.1em$A \,\equiv\, \textit{Abs\_\allowbreak three}~0$'' \\
\textbf{definition}~$B \mathbin{\Colon} \textit{three}$ \textbf{where} ``$B \,\equiv\, \textit{Abs\_three}~1$'' \\
\textbf{definition}~$C \mathbin{\Colon} \textit{three}$ \textbf{where} ``$C \,\equiv\, \textit{Abs\_three}~2$'' \\[2\smallskipamount]
\textbf{lemma} ``$\lbrakk A \in X;\> B \in X\rbrakk \,\Longrightarrow\, c \in X$'' \\
\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $X = \{\Abs{0},\, \Abs{1}\}$ \\
\hbox{}\qquad\qquad $c = \Abs{2}$ \\
\hbox{}\qquad Types: \\
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
\hbox{}\qquad\qquad $\textit{three} = \{\Abs{0},\, \Abs{1},\, \Abs{2},\, \unr\}$
\postw
In the output above, $\Abs{n}$ abbreviates $\textit{Abs\_three}~n$.
Quotient types are handled in much the same way. The following fragment defines
the integer type \textit{my\_int} by encoding the integer $x$ by a pair of
natural numbers $(m, n)$ such that $x + n = m$:
\prew
\textbf{fun} \textit{my\_int\_rel} \textbf{where} \\
``$\textit{my\_int\_rel}~(x,\, y)~(u,\, v) = (x + v = u + y)$'' \\[2\smallskipamount]
%
\textbf{quotient\_type}~\textit{my\_int} = ``$\textit{nat} \times \textit{nat\/}$''$\;{/}\;$\textit{my\_int\_rel} \\
\textbf{by}~(\textit{auto simp add\/}:\ \textit{equivp\_def fun\_eq\_iff}) \\[2\smallskipamount]
%
\textbf{definition}~\textit{add\_raw}~\textbf{where} \\
``$\textit{add\_raw} \,\equiv\, \lambda(x,\, y)~(u,\, v).\; (x + (u\Colon\textit{nat}), y + (v\Colon\textit{nat}))$'' \\[2\smallskipamount]
%
\textbf{quotient\_definition} ``$\textit{add\/}\Colon\textit{my\_int} \Rightarrow \textit{my\_int} \Rightarrow \textit{my\_int\/}$'' \textbf{is} \textit{add\_raw} \\[2\smallskipamount]
%
\textbf{lemma} ``$\textit{add}~x~y = \textit{add}~x~x$'' \\
\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $x = \Abs{(0,\, 0)}$ \\
\hbox{}\qquad\qquad $y = \Abs{(0,\, 1)}$ \\
\hbox{}\qquad Types: \\
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, \unr\}$ \\
\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat}~[\textsl{boxed\/}] = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
\hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(0,\, 1)},\> \unr\}$
\postw
The values $\Abs{(0,\, 0)}$ and $\Abs{(0,\, 1)}$ represent the
integers $0$ and $-1$, respectively. Other representants would have been
possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(11,\, 12)}$. If we are going to
use \textit{my\_int} extensively, it pays off to install a term postprocessor
that converts the pair notation to the standard mathematical notation:
\prew
$\textbf{ML}~\,\{{*} \\
\!\begin{aligned}[t]
%& ({*}~\,\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \\[-2pt]
%& \phantom{(*}~\,{\rightarrow}\;\textit{term}~\,{*}) \\[-2pt]
& \textbf{fun}\,~\textit{my\_int\_postproc}~\_~\_~\_~T~(\textit{Const}~\_~\$~(\textit{Const}~\_~\$~\textit{t1}~\$~\textit{t2\/})) = {} \\[-2pt]
& \phantom{fun}\,~\textit{HOLogic.mk\_number}~T~(\textit{snd}~(\textit{HOLogic.dest\_number~t1}) \\[-2pt]
& \phantom{fun\,~\textit{HOLogic.mk\_number}~T~(}{-}~\textit{snd}~(\textit{HOLogic.dest\_number~t2\/})) \\[-2pt]
& \phantom{fun}\!{\mid}\,~\textit{my\_int\_postproc}~\_~\_~\_~\_~t = t \\[-2pt]
{*}\}\end{aligned}$ \\[2\smallskipamount]
$\textbf{declaration}~\,\{{*} \\
\!\begin{aligned}[t]
& \textit{Nitpick\_Model.register\_term\_postprocessor}~\!\begin{aligned}[t]
& @\{\textrm{typ}~\textit{my\_int}\} \\[-2pt]
& \textit{my\_int\_postproc}\end{aligned} \\[-2pt]
{*}\}\end{aligned}$
\postw
Records are handled as datatypes with a single constructor:
\prew
\textbf{record} \textit{point} = \\
\hbox{}\quad $\textit{Xcoord} \mathbin{\Colon} \textit{int}$ \\
\hbox{}\quad $\textit{Ycoord} \mathbin{\Colon} \textit{int}$ \\[2\smallskipamount]
\textbf{lemma} ``$\textit{Xcoord}~(p\Colon\textit{point}) = \textit{Xcoord}~(q\Colon\textit{point})$'' \\
\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
\hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
\hbox{}\qquad Types: \\
\hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, \unr\}$ \\
\hbox{}\qquad\qquad $\textit{point} = \{\!\begin{aligned}[t]
& \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr, \\[-2pt] %% TYPESETTING
& \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
\postw
Finally, Nitpick provides rudimentary support for rationals and reals using a
similar approach:
\prew
\textbf{lemma} ``$4 * x + 3 * (y\Colon\textit{real}) \not= 1/2$'' \\
\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $x = 1/2$ \\
\hbox{}\qquad\qquad $y = -1/2$ \\
\hbox{}\qquad Types: \\
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, 3,\, 4,\, 5,\, 6,\, 7,\, \unr\}$ \\
\hbox{}\qquad\qquad $\textit{int} = \{-3,\, -2,\, -1,\, 0,\, 1,\, 2,\, 3,\, 4,\, \unr\}$ \\
\hbox{}\qquad\qquad $\textit{real} = \{-3/2,\, -1/2,\, 0,\, 1/2,\, 1,\, 2,\, 3,\, 4,\, \unr\}$
\postw
\subsection{Inductive and Coinductive Predicates}
\label{inductive-and-coinductive-predicates}
Inductively defined predicates (and sets) are particularly problematic for
counterexample generators. They can make Quickcheck~\cite{berghofer-nipkow-2004}
loop forever and Refute~\cite{weber-2008} run out of resources. The crux of
the problem is that they are defined using a least fixed-point construction.
Nitpick's philosophy is that not all inductive predicates are equal. Consider
the \textit{even} predicate below:
\prew
\textbf{inductive}~\textit{even}~\textbf{where} \\
``\textit{even}~0'' $\,\mid$ \\
``\textit{even}~$n\,\Longrightarrow\, \textit{even}~(\textit{Suc}~(\textit{Suc}~n))$''
\postw
This predicate enjoys the desirable property of being well-founded, which means
that the introduction rules don't give rise to infinite chains of the form
\prew
$\cdots\,\Longrightarrow\, \textit{even}~k''
\,\Longrightarrow\, \textit{even}~k'
\,\Longrightarrow\, \textit{even}~k.$
\postw
For \textit{even}, this is obvious: Any chain ending at $k$ will be of length
$k/2 + 1$:
\prew
$\textit{even}~0\,\Longrightarrow\, \textit{even}~2\,\Longrightarrow\, \cdots
\,\Longrightarrow\, \textit{even}~(k - 2)
\,\Longrightarrow\, \textit{even}~k.$
\postw
Wellfoundedness is desirable because it enables Nitpick to use a very efficient
fixed-point computation.%
\footnote{If an inductive predicate is
well-founded, then it has exactly one fixed point, which is simultaneously the
least and the greatest fixed point. In these circumstances, the computation of
the least fixed point amounts to the computation of an arbitrary fixed point,
which can be performed using a straightforward recursive equation.}
Moreover, Nitpick can prove wellfoundedness of most well-founded predicates,
just as Isabelle's \textbf{function} package usually discharges termination
proof obligations automatically.
Let's try an example:
\prew
\textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
\textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
\slshape The inductive predicate ``\textit{even}'' was proved well-founded;
Nitpick can compute it efficiently \\[2\smallskipamount]
Trying 1 scope: \\
\hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported fragment; only
potentially spurious counterexamples may be found \\[2\smallskipamount]
Nitpick found a potentially spurious counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
\hbox{}\qquad Empty assignment \\[2\smallskipamount]
Nitpick could not find a better counterexample
It checked 1 of 1 scope \\[2\smallskipamount]
Total time: 1.62 s.
\postw
No genuine counterexample is possible because Nitpick cannot rule out the
existence of a natural number $n \ge 50$ such that both $\textit{even}~n$ and
$\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the
existential quantifier:
\prew
\textbf{lemma} ``$\exists n \mathbin{\le} 49.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
\textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Empty assignment
\postw
So far we were blessed by the wellfoundedness of \textit{even}. What happens if
we use the following definition instead?
\prew
\textbf{inductive} $\textit{even}'$ \textbf{where} \\
``$\textit{even}'~(0{\Colon}\textit{nat})$'' $\,\mid$ \\
``$\textit{even}'~2$'' $\,\mid$ \\
``$\lbrakk\textit{even}'~m;\> \textit{even}'~n\rbrakk \,\Longrightarrow\, \textit{even}'~(m + n)$''
\postw
This definition is not well-founded: From $\textit{even}'~0$ and
$\textit{even}'~0$, we can derive that $\textit{even}'~0$. Nonetheless, the
predicates $\textit{even}$ and $\textit{even}'$ are equivalent.
Let's check a property involving $\textit{even}'$. To make up for the
foreseeable computational hurdles entailed by non-wellfoundedness, we decrease
\textit{nat}'s cardinality to a mere 10:
\prew
\textbf{lemma}~``$\exists n \in \{0, 2, 4, 6, 8\}.\;
\lnot\;\textit{even}'~n$'' \\
\textbf{nitpick}~[\textit{card nat}~= 10,\, \textit{verbose},\, \textit{show\_consts}] \\[2\smallskipamount]
\slshape
The inductive predicate ``$\textit{even}'\!$'' could not be proved well-founded; Nitpick might need to unroll it \\[2\smallskipamount]
Trying 6 scopes: \\
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 0; \\
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 1; \\
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2; \\
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 4; \\
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 8; \\
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 9 \\[2\smallskipamount]
Nitpick found a counterexample for \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2: \\[2\smallskipamount]
\hbox{}\qquad Constant: \nopagebreak \\
\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\unkef(\!\begin{aligned}[t]
& 0 := \unkef(0 := \textit{True},\, 2 := \textit{True}),\, \\[-2pt]
& 1 := \unkef(0 := \textit{True},\, 2 := \textit{True},\, 4 := \textit{True}),\, \\[-2pt]
& 2 := \unkef(0 := \textit{True},\, 2 := \textit{True},\, 4 := \textit{True},\, \\[-2pt]
& \phantom{2 := \unkef(}6 := \textit{True},\, 8 := \textit{True}))\end{aligned}$ \\[2\smallskipamount]
Total time: 1.87 s.
\postw
Nitpick's output is very instructive. First, it tells us that the predicate is
unrolled, meaning that it is computed iteratively from the empty set. Then it
lists six scopes specifying different bounds on the numbers of iterations:\ 0,
1, 2, 4, 8, and~9.
The output also shows how each iteration contributes to $\textit{even}'$. The
notation $\lambda i.\; \textit{even}'$ indicates that the value of the
predicate depends on an iteration counter. Iteration 0 provides the basis
elements, $0$ and $2$. Iteration 1 contributes $4$ ($= 2 + 2$). Iteration 2
throws $6$ ($= 2 + 4 = 4 + 2$) and $8$ ($= 4 + 4$) into the mix. Further
iterations would not contribute any new elements.
The predicate $\textit{even}'$ evaluates to either \textit{True} or $\unk$,
never \textit{False}.
%Some values are marked with superscripted question
%marks~(`\lower.2ex\hbox{$^\Q$}'). These are the elements for which the
%predicate evaluates to $\unk$.
When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, 20, 24, and 28
iterations. However, these numbers are bounded by the cardinality of the
predicate's domain. With \textit{card~nat}~= 10, no more than 9 iterations are
ever needed to compute the value of a \textit{nat} predicate. You can specify
the number of iterations using the \textit{iter} option, as explained in
\S\ref{scope-of-search}.
In the next formula, $\textit{even}'$ occurs both positively and negatively:
\prew
\textbf{lemma} ``$\textit{even}'~(n - 2) \,\Longrightarrow\, \textit{even}'~n$'' \\
\textbf{nitpick} [\textit{card nat} = 10, \textit{show\_consts}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variable: \nopagebreak \\
\hbox{}\qquad\qquad $n = 1$ \\
\hbox{}\qquad Constants: \nopagebreak \\
\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\unkef(\!\begin{aligned}[t]
& 0 := \unkef(0 := \mathit{True},\, 2 := \mathit{True}))\end{aligned}$ \\
\hbox{}\qquad\qquad $\textit{even}' \leq \unkef(\!\begin{aligned}[t]
& 0 := \mathit{True},\, 1 := \mathit{False},\, 2 := \mathit{True},\, \\[-2pt]
& 4 := \mathit{True},\, 6 := \mathit{True},\, 8 := \mathit{True})\end{aligned}$
\postw
Notice the special constraint $\textit{even}' \leq \ldots$ in the output, whose
right-hand side represents an arbitrary fixed point (not necessarily the least
one). It is used to falsify $\textit{even}'~n$. In contrast, the unrolled
predicate is used to satisfy $\textit{even}'~(n - 2)$.
Coinductive predicates are handled dually. For example:
\prew
\textbf{coinductive} \textit{nats} \textbf{where} \\
``$\textit{nats}~(x\Colon\textit{nat}) \,\Longrightarrow\, \textit{nats}~x$'' \\[2\smallskipamount]
\textbf{lemma} ``$\textit{nats} = (\lambda n.\; n \mathbin\in \{0, 1, 2, 3, 4\})$'' \\
\textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample:
\\[2\smallskipamount]
\hbox{}\qquad Constants: \nopagebreak \\
\hbox{}\qquad\qquad $\lambda i.\; \textit{nats} = \unkef(0 := \unkef,\, 1 := \unkef,\, 2 := \unkef)$ \\
\hbox{}\qquad\qquad $\textit{nats} \geq \unkef(3 := \textit{True},\, 4 := \textit{False},\, 5 := \textit{True})$
\postw
As a special case, Nitpick uses Kodkod's transitive closure operator to encode
negative occurrences of non-well-founded ``linear inductive predicates,'' i.e.,
inductive predicates for which each the predicate occurs in at most one
assumption of each introduction rule. For example:
\prew
\textbf{inductive} \textit{odd} \textbf{where} \\
``$\textit{odd}~1$'' $\,\mid$ \\
``$\lbrakk \textit{odd}~m;\>\, \textit{even}~n\rbrakk \,\Longrightarrow\, \textit{odd}~(m + n)$'' \\[2\smallskipamount]
\textbf{lemma}~``$\textit{odd}~n \,\Longrightarrow\, \textit{odd}~(n - 2)$'' \\
\textbf{nitpick}~[\textit{card nat} = 4,\, \textit{show\_consts}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample:
\\[2\smallskipamount]
\hbox{}\qquad Free variable: \nopagebreak \\
\hbox{}\qquad\qquad $n = 1$ \\
\hbox{}\qquad Constants: \nopagebreak \\
\hbox{}\qquad\qquad $\textit{even} = \unkef(0 := True, 1 := False, 2 := True, 3 := False)$ \\
\hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = {}$ \\
\hbox{}\qquad\qquad\quad $\unkef(0 := \textit{False},\, 1 := \textit{True},\, 2 := \textit{False},\, 3 := \textit{False})$ \\
\hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \unkef$\\
\hbox{}\qquad\qquad\quad $(
\!\begin{aligned}[t]
& 0 := \unkef(0 := \textit{True},\, 1 := \textit{False},\, 2 := \textit{True},\, 3 := \textit{False}), \\[-2pt]
& 1 := \unkef(0 := \textit{False},\, 1 := \textit{True},\, 2 := \textit{False},\, 3 := \textit{True}), \\[-2pt]
& 2 := \unkef(0 := \textit{False},\, 1 := \textit{False},\, 2 := \textit{True},\, 3 := \textit{False}), \\[-2pt]
& 3 := \unkef(0 := \textit{False},\, 1 := \textit{False},\, 2 := \textit{False},\, 3 := \textit{True}))
\end{aligned}$ \\
\hbox{}\qquad\qquad $\textit{odd} \leq \unkef(0 := \textit{False},\, 1 := \textit{True},\, 2 := \textit{False},\, 3 := \textit{True})$
\postw
\noindent
In the output, $\textit{odd}_{\textrm{base}}$ represents the base elements and
$\textit{odd}_{\textrm{step}}$ is a transition relation that computes new
elements from known ones. The set $\textit{odd}$ consists of all the values
reachable through the reflexive transitive closure of
$\textit{odd}_{\textrm{step}}$ starting with any element from
$\textit{odd}_{\textrm{base}}$, namely 1 and 3. Using Kodkod's
transitive closure to encode linear predicates is normally either more thorough
or more efficient than unrolling (depending on the value of \textit{iter}), but
you can disable it by passing the \textit{dont\_star\_linear\_preds} option.
\subsection{Coinductive Datatypes}
\label{coinductive-datatypes}
A coinductive datatype is similar to an inductive datatype but
allows infinite objects. Thus, the infinite lists $\textit{ps}$ $=$ $[a, a, a,
\ldots]$, $\textit{qs}$ $=$ $[a, b, a, b, \ldots]$, and $\textit{rs}$ $=$ $[0,
1, 2, 3, \ldots]$ can be defined as coinductive lists, or ``lazy lists,'' using the
$\textit{LNil}\mathbin{\Colon}{'}a~\textit{llist}$ and
$\textit{LCons}\mathbin{\Colon}{'}a \mathbin{\Rightarrow} {'}a~\textit{llist}
\mathbin{\Rightarrow} {'}a~\textit{llist}$ constructors.
Although it is otherwise no friend of infinity, Nitpick can find counterexamples
involving cyclic lists such as \textit{ps} and \textit{qs} above as well as
finite lists:
\prew
\textbf{codatatype} $'a$ \textit{llist} = \textit{LNil}~$\mid$~\textit{LCons}~$'a$~``$'a\;\textit{llist}$'' \\[2\smallskipamount]
\textbf{lemma} ``$\textit{xs} \not= \textit{LCons}~a~\textit{xs\/}$'' \\
\textbf{nitpick} \\[2\smallskipamount]
\slshape Nitpick found a counterexample for {\itshape card}~$'a$ = 1: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $\textit{a} = a_1$ \\
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$
\postw
The notation $\textrm{THE}~\omega.\; \omega = t(\omega)$ stands
for the infinite term $t(t(t(\ldots)))$. Hence, \textit{xs} is simply the
infinite list $[a_1, a_1, a_1, \ldots]$.
The next example is more interesting:
\prew
\textbf{primcorec}~$\textit{iterates}$~\textbf{where} \\
``$\textit{iterates}~f\>a = \textit{LCons}~a~(\textit{iterates}~f\>(f\>a))$'' \\[2\smallskipamount]
\textbf{lemma}~``$\lbrakk\textit{xs} = \textit{LCons}~a~\textit{xs};\>\,
\textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys\/}$'' \\
\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
\slshape The type $'a$ passed the monotonicity test; Nitpick might be able to skip
some scopes \\[2\smallskipamount]
Trying 10 scopes: \\
\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 1,
and \textit{bisim\_depth}~= 0; \\
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
\hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 10,
and \textit{bisim\_depth}~= 9 \\[2\smallskipamount]
Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
\textit{card}~``\kern1pt$'a~\textit{llist\/}$''~= 2, and \textit{bisim\_\allowbreak
depth}~= 1:
\\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $\textit{a} = a_1$ \\
\hbox{}\qquad\qquad $\textit{b} = a_2$ \\
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount]
Total time: 1.11 s
\postw
The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas
$\textit{ys}$ is $[a_2, a_1, a_1, a_1, \ldots]$, i.e., a lasso-shaped list with
$[a_2]$ as its stem and $[a_1]$ as its cycle. In general, the list segment
within the scope of the {THE} binder corresponds to the lasso's cycle, whereas
the segment leading to the binder is the stem.
A salient property of coinductive datatypes is that two objects are considered
equal if and only if they lead to the same observations. For example, the two
lazy lists
%
\begin{gather*}
\textrm{THE}~\omega.\; \omega = \textit{LCons}~a~(\textit{LCons}~b~\omega) \\
\textit{LCons}~a~(\textrm{THE}~\omega.\; \omega = \textit{LCons}~b~(\textit{LCons}~a~\omega))
\end{gather*}
%
are identical, because both lead
to the sequence of observations $a$, $b$, $a$, $b$, \hbox{\ldots} (or,
equivalently, both encode the infinite list $[a, b, a, b, \ldots]$). This
concept of equality for coinductive datatypes is called bisimulation and is
defined coinductively.
Internally, Nitpick encodes the coinductive bisimilarity predicate as part of
the Kodkod problem to ensure that distinct objects lead to different
observations. This precaution is somewhat expensive and often unnecessary, so it
can be disabled by setting the \textit{bisim\_depth} option to $-1$. The
bisimilarity check is then performed \textsl{after} the counterexample has been
found to ensure correctness. If this after-the-fact check fails, the
counterexample is tagged as ``quasi genuine'' and Nitpick recommends to try
again with \textit{bisim\_depth} set to a nonnegative integer.
The next formula illustrates the need for bisimilarity (either as a Kodkod
predicate or as an after-the-fact check) to prevent spurious counterexamples:
\prew
\textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
\,\Longrightarrow\, \textit{xs} = \textit{ys\/}$'' \\
\textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_types}] \\[2\smallskipamount]
\slshape Nitpick found a quasi genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $a = a_1$ \\
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
\textit{LCons}~a_1~\omega$ \\
\hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
\hbox{}\qquad Type:\strut \nopagebreak \\
\hbox{}\qquad\qquad $'a~\textit{llist} =
\{\!\begin{aligned}[t]
& \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega, \\[-2pt]
& \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega,\> \unr\}\end{aligned}$
\\[2\smallskipamount]
Try again with ``\textit{bisim\_depth}'' set to a nonnegative value to confirm
that the counterexample is genuine \\[2\smallskipamount]
{\upshape\textbf{nitpick}} \\[2\smallskipamount]
\slshape Nitpick found no counterexample
\postw
In the first \textbf{nitpick} invocation, the after-the-fact check discovered
that the two known elements of type $'a~\textit{llist}$ are bisimilar, prompting
Nitpick to label the example as only ``quasi genuine.''
A compromise between leaving out the bisimilarity predicate from the Kodkod
problem and performing the after-the-fact check is to specify a low
nonnegative \textit{bisim\_depth} value. In general, a value of $K$ means that
Nitpick will require all lists to be distinguished from each other by their
prefixes of length $K$. However, setting $K$ to a too low value can
overconstrain Nitpick, preventing it from finding any counterexamples.
\subsection{Boxing}
\label{boxing}
Nitpick normally maps function and product types directly to the corresponding
Kodkod concepts. As a consequence, if $'a$ has cardinality 3 and $'b$ has
cardinality 4, then $'a \times {'}b$ has cardinality 12 ($= 4 \times 3$) and $'a
\Rightarrow {'}b$ has cardinality 64 ($= 4^3$). In some circumstances, it pays
off to treat these types in the same way as plain datatypes, by approximating
them by a subset of a given cardinality. This technique is called ``boxing'' and
is particularly useful for functions passed as arguments to other functions, for
high-arity functions, and for large tuples. Under the hood, boxing involves
wrapping occurrences of the types $'a \times {'}b$ and $'a \Rightarrow {'}b$ in
isomorphic datatypes, as can be seen by enabling the \textit{debug} option.
To illustrate boxing, we consider a formalization of $\lambda$-terms represented
using de Bruijn's notation:
\prew
\textbf{datatype} \textit{tm} = \textit{Var}~\textit{nat}~$\mid$~\textit{Lam}~\textit{tm} $\mid$ \textit{App~tm~tm}
\postw
The $\textit{lift}~t~k$ function increments all variables with indices greater
than or equal to $k$ by one:
\prew
\textbf{primrec} \textit{lift} \textbf{where} \\
``$\textit{lift}~(\textit{Var}~j)~k = \textit{Var}~(\textrm{if}~j < k~\textrm{then}~j~\textrm{else}~j + 1)$'' $\mid$ \\
``$\textit{lift}~(\textit{Lam}~t)~k = \textit{Lam}~(\textit{lift}~t~(k + 1))$'' $\mid$ \\
``$\textit{lift}~(\textit{App}~t~u)~k = \textit{App}~(\textit{lift}~t~k)~(\textit{lift}~u~k)$''
\postw
The $\textit{loose}~t~k$ predicate returns \textit{True} if and only if
term $t$ has a loose variable with index $k$ or more:
\prew
\textbf{primrec}~\textit{loose} \textbf{where} \\
``$\textit{loose}~(\textit{Var}~j)~k = (j \ge k)$'' $\mid$ \\
``$\textit{loose}~(\textit{Lam}~t)~k = \textit{loose}~t~(\textit{Suc}~k)$'' $\mid$ \\
``$\textit{loose}~(\textit{App}~t~u)~k = (\textit{loose}~t~k \mathrel{\lor} \textit{loose}~u~k)$''
\postw
Next, the $\textit{subst}~\sigma~t$ function applies the substitution $\sigma$
on $t$:
\prew
\textbf{primrec}~\textit{subst} \textbf{where} \\
``$\textit{subst}~\sigma~(\textit{Var}~j) = \sigma~j$'' $\mid$ \\
``$\textit{subst}~\sigma~(\textit{Lam}~t) = {}$\phantom{''} \\
\phantom{``}$\textit{Lam}~(\textit{subst}~(\lambda n.\> \textrm{case}~n~\textrm{of}~0 \Rightarrow \textit{Var}~0 \mid \textit{Suc}~m \Rightarrow \textit{lift}~(\sigma~m)~1)~t)$'' $\mid$ \\
``$\textit{subst}~\sigma~(\textit{App}~t~u) = \textit{App}~(\textit{subst}~\sigma~t)~(\textit{subst}~\sigma~u)$''
\postw
A substitution is a function that maps variable indices to terms. Observe that
$\sigma$ is a function passed as argument and that Nitpick can't optimize it
away, because the recursive call for the \textit{Lam} case involves an altered
version. Also notice the \textit{lift} call, which increments the variable
indices when moving under a \textit{Lam}.
A reasonable property to expect of substitution is that it should leave closed
terms unchanged. Alas, even this simple property does not hold:
\pre
\textbf{lemma}~``$\lnot\,\textit{loose}~t~0 \,\Longrightarrow\, \textit{subst}~\sigma~t = t$'' \\
\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
\slshape
Trying 10 scopes: \nopagebreak \\
\hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm\/}$'' = 1; \\
\hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm\/}$'' = 2; \\
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
\hbox{}\qquad \textit{card~nat}~= 10, \textit{card tm}~= 10, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm\/}$'' = 10 \\[2\smallskipamount]
Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6,
and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm\/}$''~= 6: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $\sigma = \unkef(\!\begin{aligned}[t]
& 0 := \textit{Var}~0,\>
1 := \textit{Var}~0,\>
2 := \textit{Var}~0, \\[-2pt]
& 3 := \textit{Var}~0,\>
4 := \textit{Var}~0,\>
5 := \textit{Lam}~(\textit{Lam}~(\textit{Var}~0)))\end{aligned}$ \\
\hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount]
Total time: 3.08 s
\postw
Using \textit{eval}, we find out that $\textit{subst}~\sigma~t =
\textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional
$\lambda$-calculus notation, $t$ is
$\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is (wrongly) $\lambda x\, y.\> y$.
The bug is in \textit{subst\/}: The $\textit{lift}~(\sigma~m)~1$ call should be
replaced with $\textit{lift}~(\sigma~m)~0$.
An interesting aspect of Nitpick's verbose output is that it assigned inceasing
cardinalities from 1 to 10 to the type $\textit{nat} \Rightarrow \textit{tm}$
of the higher-order argument $\sigma$ of \textit{subst}.
For the formula of interest, knowing 6 values of that type was enough to find
the counterexample. Without boxing, $6^6 = 46\,656$ values must be
considered, a hopeless undertaking:
\prew
\textbf{nitpick} [\textit{dont\_box}] \\[2\smallskipamount]
{\slshape Nitpick ran out of time after checking 3 of 10 scopes}
\postw
Boxing can be enabled or disabled globally or on a per-type basis using the
\textit{box} option. Nitpick usually performs reasonable choices about which
types should be boxed, but option tweaking sometimes helps.
%A related optimization,
%``finitization,'' attempts to wrap functions that are constant at all but finitely
%many points (e.g., finite sets); see the documentation for the \textit{finitize}
%option in \S\ref{scope-of-search} for details.
\subsection{Scope Monotonicity}
\label{scope-monotonicity}
The \textit{card} option (together with \textit{iter}, \textit{bisim\_depth},
and \textit{max}) controls which scopes are actually tested. In general, to
exhaust all models below a certain cardinality bound, the number of scopes that
Nitpick must consider increases exponentially with the number of type variables
(and \textbf{typedecl}'d types) occurring in the formula. Given the default
cardinality specification of 1--10, no fewer than $10^4 = 10\,000$ scopes must be
considered for a formula involving $'a$, $'b$, $'c$, and $'d$.
Fortunately, many formulas exhibit a property called \textsl{scope
monotonicity}, meaning that if the formula is falsifiable for a given scope,
it is also falsifiable for all larger scopes \cite[p.~165]{jackson-2006}.
Consider the formula
\prew
\textbf{lemma}~``$\textit{length~xs} = \textit{length~ys} \,\Longrightarrow\, \textit{rev}~(\textit{zip~xs~ys}) = \textit{zip~xs}~(\textit{rev~ys})$''
\postw
where \textit{xs} is of type $'a~\textit{list}$ and \textit{ys} is of type
$'b~\textit{list}$. A priori, Nitpick would need to consider $1\,000$ scopes to
exhaust the specification \textit{card}~= 1--10 (10 cardinalies for $'a$
$\times$ 10 cardinalities for $'b$ $\times$ 10 cardinalities for the datatypes).
However, our intuition tells us that any counterexample found with a small scope
would still be a counterexample in a larger scope---by simply ignoring the fresh
$'a$ and $'b$ values provided by the larger scope. Nitpick comes to the same
conclusion after a careful inspection of the formula and the relevant
definitions:
\prew
\textbf{nitpick}~[\textit{verbose}] \\[2\smallskipamount]
\slshape
The types $'a$ and $'b$ passed the monotonicity test; Nitpick might be able to skip some scopes.
\\[2\smallskipamount]
Trying 10 scopes: \\
\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1,
\textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$
\textit{list\/}''~= 1, \\
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 1, and
\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 1; \\
\hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2,
\textit{card} \textit{nat}~= 2, \textit{card} ``$('a \times {'}b)$
\textit{list\/}''~= 2, \\
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 2, and
\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 2; \\
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
\hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} $'b$~= 10,
\textit{card} \textit{nat}~= 10, \textit{card} ``$('a \times {'}b)$
\textit{list\/}''~= 10, \\
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 10, and
\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 10
\\[2\smallskipamount]
Nitpick found a counterexample for
\textit{card} $'a$~= 5, \textit{card} $'b$~= 5,
\textit{card} \textit{nat}~= 5, \textit{card} ``$('a \times {'}b)$
\textit{list\/}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 5, and
\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 5:
\\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\
\hbox{}\qquad\qquad $\textit{ys} = [b_1, b_1]$ \\[2\smallskipamount]
Total time: 1.63 s.
\postw
In theory, it should be sufficient to test a single scope:
\prew
\textbf{nitpick}~[\textit{card}~= 10]
\postw
However, this is often less efficient in practice and may lead to overly complex
counterexamples.
If the monotonicity check fails but we believe that the formula is monotonic (or
we don't mind missing some counterexamples), we can pass the
\textit{mono} option. To convince yourself that this option is risky,
simply consider this example from \S\ref{skolemization}:
\prew
\textbf{lemma} ``$\exists g.\; \forall x\Colon 'b.~g~(f~x) = x
\,\Longrightarrow\, \forall y\Colon {'}a.\; \exists x.~y = f~x$'' \\
\textbf{nitpick} [\textit{mono}] \\[2\smallskipamount]
{\slshape Nitpick found no counterexample} \\[2\smallskipamount]
\textbf{nitpick} \\[2\smallskipamount]
\slshape
Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\
\hbox{}\qquad $\vdots$
\postw
(It turns out the formula holds if and only if $\textit{card}~'a \le
\textit{card}~'b$.) Although this is rarely advisable, the automatic
monotonicity checks can be disabled by passing \textit{non\_mono}
(\S\ref{optimizations}).
As insinuated in \S\ref{natural-numbers-and-integers} and
\S\ref{inductive-datatypes}, \textit{nat}, \textit{int}, and inductive datatypes
are normally monotonic and treated as such. The same is true for record types,
\textit{rat}, and \textit{real}. Thus, given the
cardinality specification 1--10, a formula involving \textit{nat}, \textit{int},
\textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
consider only 10~scopes instead of $10^4 = 10\,000$. On the other hand,
\textbf{typedef}s and quotient types are generally nonmonotonic.
\subsection{Inductive Properties}
\label{inductive-properties}
Inductive properties are a particular pain to prove, because the failure to
establish an induction step can mean several things:
%
\begin{enumerate}
\item The property is invalid.
\item The property is valid but is too weak to support the induction step.
\item The property is valid and strong enough; it's just that we haven't found
the proof yet.
\end{enumerate}
%
Depending on which scenario applies, we would take the appropriate course of
action:
%
\begin{enumerate}
\item Repair the statement of the property so that it becomes valid.
\item Generalize the property and/or prove auxiliary properties.
\item Work harder on a proof.
\end{enumerate}
%
How can we distinguish between the three scenarios? Nitpick's normal mode of
operation can often detect scenario 1, and Isabelle's automatic tactics help with
scenario 3. Using appropriate techniques, it is also often possible to use
Nitpick to identify scenario 2. Consider the following transition system,
in which natural numbers represent states:
\prew
\textbf{inductive\_set}~\textit{reach}~\textbf{where} \\
``$(4\Colon\textit{nat}) \in \textit{reach\/}$'' $\mid$ \\
``$\lbrakk n < 4;\> n \in \textit{reach\/}\rbrakk \,\Longrightarrow\, 3 * n + 1 \in \textit{reach\/}$'' $\mid$ \\
``$n \in \textit{reach} \,\Longrightarrow n + 2 \in \textit{reach\/}$''
\postw
We will try to prove that only even numbers are reachable:
\prew
\textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n$''
\postw
Does this property hold? Nitpick cannot find a counterexample within 30 seconds,
so let's attempt a proof by induction:
\prew
\textbf{apply}~(\textit{induct~set}{:}~\textit{reach\/}) \\
\textbf{apply}~\textit{auto}
\postw
This leaves us in the following proof state:
\prew
{\slshape goal (2 subgoals): \\
\phantom{0}1. ${\bigwedge}n.\;\, \lbrakk n \in \textit{reach\/};\, n < 4;\, 2~\textsl{dvd}~n\rbrakk \,\Longrightarrow\, 2~\textsl{dvd}~\textit{Suc}~(3 * n)$ \\
\phantom{0}2. ${\bigwedge}n.\;\, \lbrakk n \in \textit{reach\/};\, 2~\textsl{dvd}~n\rbrakk \,\Longrightarrow\, 2~\textsl{dvd}~\textit{Suc}~(\textit{Suc}~n)$
}
\postw
If we run Nitpick on the first subgoal, it still won't find any
counterexample; and yet, \textit{auto} fails to go further, and \textit{arith}
is helpless. However, notice the $n \in \textit{reach}$ assumption, which
strengthens the induction hypothesis but is not immediately usable in the proof.
If we remove it and invoke Nitpick, this time we get a counterexample:
\prew
\textbf{apply}~(\textit{thin\_tac}~``$n \in \textit{reach\/}$'') \\
\textbf{nitpick} \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Skolem constant: \nopagebreak \\
\hbox{}\qquad\qquad $n = 0$
\postw
Indeed, 0 < 4, 2 divides 0, but 2 does not divide 1. We can use this information
to strength the lemma:
\prew
\textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \not= 0$''
\postw
Unfortunately, the proof by induction still gets stuck, except that Nitpick now
finds the counterexample $n = 2$. We generalize the lemma further to
\prew
\textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \ge 4$''
\postw
and this time \textit{arith} can finish off the subgoals.
\section{Case Studies}
\label{case-studies}
As a didactic device, the previous section focused mostly on toy formulas whose
validity can easily be assessed just by looking at the formula. We will now
review two somewhat more realistic case studies that are within Nitpick's
reach:\ a context-free grammar modeled by mutually inductive sets and a
functional implementation of AA trees. The results presented in this
section were produced with the following settings:
\prew
\textbf{nitpick\_params} [\textit{max\_potential}~= 0]
\postw
\subsection{A Context-Free Grammar}
\label{a-context-free-grammar}
Our first case study is taken from section 7.4 in the Isabelle tutorial
\cite{isa-tutorial}. The following grammar, originally due to Hopcroft and
Ullman, produces all strings with an equal number of $a$'s and $b$'s:
\prew
\begin{tabular}{@{}r@{$\;\,$}c@{$\;\,$}l@{}}
$S$ & $::=$ & $\epsilon \mid bA \mid aB$ \\
$A$ & $::=$ & $aS \mid bAA$ \\
$B$ & $::=$ & $bS \mid aBB$
\end{tabular}
\postw
The intuition behind the grammar is that $A$ generates all strings with one more
$a$ than $b$'s and $B$ generates all strings with one more $b$ than $a$'s.
The alphabet consists exclusively of $a$'s and $b$'s:
\prew
\textbf{datatype} \textit{alphabet}~= $a$ $\mid$ $b$
\postw
Strings over the alphabet are represented by \textit{alphabet list}s.
Nonterminals in the grammar become sets of strings. The production rules
presented above can be expressed as a mutually inductive definition:
\prew
\textbf{inductive\_set} $S$ \textbf{and} $A$ \textbf{and} $B$ \textbf{where} \\
\textit{R1}:\kern.4em ``$[] \in S$'' $\,\mid$ \\
\textit{R2}:\kern.4em ``$w \in A\,\Longrightarrow\, b \mathbin{\#} w \in S$'' $\,\mid$ \\
\textit{R3}:\kern.4em ``$w \in B\,\Longrightarrow\, a \mathbin{\#} w \in S$'' $\,\mid$ \\
\textit{R4}:\kern.4em ``$w \in S\,\Longrightarrow\, a \mathbin{\#} w \in A$'' $\,\mid$ \\
\textit{R5}:\kern.4em ``$w \in S\,\Longrightarrow\, b \mathbin{\#} w \in S$'' $\,\mid$ \\
\textit{R6}:\kern.4em ``$\lbrakk v \in B;\> v \in B\rbrakk \,\Longrightarrow\, a \mathbin{\#} v \mathbin{@} w \in B$''
\postw
The conversion of the grammar into the inductive definition was done manually by
Joe Blow, an underpaid undergraduate student. As a result, some errors might
have sneaked in.
Debugging faulty specifications is at the heart of Nitpick's \textsl{raison
d'\^etre}. A good approach is to state desirable properties of the specification
(here, that $S$ is exactly the set of strings over $\{a, b\}$ with as many $a$'s
as $b$'s) and check them with Nitpick. If the properties are correctly stated,
counterexamples will point to bugs in the specification. For our grammar
example, we will proceed in two steps, separating the soundness and the
completeness of the set $S$. First, soundness:
\prew
\textbf{theorem}~\textit{S\_sound\/}: \\
``$w \in S \longrightarrow \textit{length}~[x\mathbin{\leftarrow} w.\; x = a] =
\textit{length}~[x\mathbin{\leftarrow} w.\; x = b]$'' \\
\textbf{nitpick} \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variable: \nopagebreak \\
\hbox{}\qquad\qquad $w = [b]$
\postw
It would seem that $[b] \in S$. How could this be? An inspection of the
introduction rules reveals that the only rule with a right-hand side of the form
$b \mathbin{\#} {\ldots} \in S$ that could have introduced $[b]$ into $S$ is
\textit{R5}:
\prew
``$w \in S\,\Longrightarrow\, b \mathbin{\#} w \in S$''
\postw
On closer inspection, we can see that this rule is wrong. To match the
production $B ::= bS$, the second $S$ should be a $B$. We fix the typo and try
again:
\prew
\textbf{nitpick} \\[2\smallskipamount]
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.46 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
