\documentclass[a4paper,12pt]{article}

\usepackage[T1]{fontenc}

\usepackage{amsmath}

\usepackage{amssymb}

\usepackage[english,french]{babel}

\usepackage{color}

\usepackage{footmisc}

\usepackage{graphicx}

%\usepackage{mathpazo}

\usepackage{multicol}

\usepackage{stmaryrd}

%\usepackage[scaled=.85]{beramono}

\usepackage{../../lib/texinputs/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\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}

\begin{document}

%%% TYPESETTING

%\renewcommand\labelitemi{$\bullet$}

\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}}

\selectlanguage{english}

\title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]

Picking Nits \\[\smallskipamount]

\Large A User's Guide to Nitpick for Isabelle/HOL}

\author{\hbox{} \\

Jasmin Christian 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.

You can also invoke Nitpick from the ``Commands'' submenu of the

``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c C-a

C-n. This is equivalent to entering the \textbf{nitpick} command with no

arguments in the theory text.

Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.6 virtual

machine called \texttt{java}. 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}.

Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.

Nitpick also provides an automatic mode that can be enabled via the ``Auto

Nitpick'' option from the ``Isabelle'' menu in Proof General. In this mode,

Nitpick is run on every newly entered theorem. The time limit for Auto Nitpick

and other automatic tools can be set using the ``Auto Tools Time Limit'' option.

\newbox\boxA

\setbox\boxA=\hbox{\texttt{nospam}}

The examples presented in this manual can be found

in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_Examples/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 Nitpick

or this manual should be directed to

\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak

in.\allowbreak tum.\allowbreak de}.

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

%

%MISSING:

%

%  * Nitpick is part of Isabelle/HOL

%  * but it relies on an external tool called Kodkodi (Kodkod wrapper)

%  * Two options:

%    * if you use a prebuilt Isabelle package, Kodkodi is automatically there

%    * if you work from sources, the latest Kodkodi can be obtained from ...

%      download it, install it in some directory of your choice (e.g.,

%      $ISABELLE_HOME/contrib/kodkodi), and add the absolute path to Kodkodi

%      in your .isabelle/etc/components file

%

%  * If you're not sure, just try the example in the next section

\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 installed, 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

%FIXME: If you get the output:...

%Then do such-and-such.

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 `--'

can be entered as \texttt{-} (hyphen) or

\texttt{\char`\\\char`\<emdash\char`\>}.} \\[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: \textrm{by}~(\textit{metis~theI}) (42 ms).} \\[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. The tedious

task of finding out whether the potentially spurious counterexample is in fact

genuine can be delegated to \textit{auto} by passing \textit{check\_potential}.

For example:

\prew

\textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\

\textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[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}$ \\[2\smallskipamount]

Confirmation by ``\textit{auto}'': The above counterexample is genuine.

\postw

You might wonder why the counterexample is first reported as potentially

spurious. The root of the problem 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 satisfied, the putative lemma

can never be falsified.

Incidentally, if you distrust the so-called genuine counterexamples, you can

enable \textit{check\_\allowbreak genuine} to verify them as well. However, be

aware that \textit{auto} will usually fail to prove that the counterexample is

genuine or spurious.

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

\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 ``Datatype'' 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\_datatypes}] \\[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 Datatypes: \\

\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\_datatypes}] \\[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 Datatypes: \\

\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\_datatypes}] \\[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 Datatypes: \\

\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\_datatypes}] \\[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 Datatypes: \\

\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\_datatypes}] \\[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 Datatypes: \\

\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} = (λx. ?)(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}

While Isabelle regrettably lacks a high-level mechanism for defining coinductive

datatypes, the \textit{Coinductive\_List} theory from Andreas Lochbihler's

\textit{Coinductive} AFP entry \cite{lochbihler-2010} provides a coinductive

``lazy list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick

supports these lazy lists seamlessly and provides a hook, described in

\S\ref{registration-of-coinductive-datatypes}, to register custom coinductive

datatypes.

(Co)intuitively, 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 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{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{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