doc-src/Nitpick/nitpick.tex
author blanchet
Wed Feb 17 14:11:41 2010 +0100 (2010-02-17)
changeset 35189 250fe9541fb2
parent 35185 9b8f351cced6
child 35220 2bcdae5f4fdb
permissions -rw-r--r--
added gotcha to Nitpick manual regarding nonstandard models of "nat"
     1 \documentclass[a4paper,12pt]{article}
     2 \usepackage[T1]{fontenc}
     3 \usepackage{amsmath}
     4 \usepackage{amssymb}
     5 \usepackage[english,french]{babel}
     6 \usepackage{color}
     7 \usepackage{graphicx}
     8 %\usepackage{mathpazo}
     9 \usepackage{multicol}
    10 \usepackage{stmaryrd}
    11 %\usepackage[scaled=.85]{beramono}
    12 \usepackage{../iman,../pdfsetup}
    13 
    14 %\oddsidemargin=4.6mm
    15 %\evensidemargin=4.6mm
    16 %\textwidth=150mm
    17 %\topmargin=4.6mm
    18 %\headheight=0mm
    19 %\headsep=0mm
    20 %\textheight=234mm
    21 
    22 \def\Colon{\mathord{:\mkern-1.5mu:}}
    23 %\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
    24 %\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
    25 \def\lparr{\mathopen{(\mkern-4mu\mid}}
    26 \def\rparr{\mathclose{\mid\mkern-4mu)}}
    27 
    28 \def\unk{{?}}
    29 \def\undef{(\lambda x.\; \unk)}
    30 %\def\unr{\textit{others}}
    31 \def\unr{\ldots}
    32 \def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
    33 \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
    34 
    35 \hyphenation{Mini-Sat size-change First-Steps grand-parent nit-pick
    36 counter-example counter-examples data-type data-types co-data-type 
    37 co-data-types in-duc-tive co-in-duc-tive}
    38 
    39 \urlstyle{tt}
    40 
    41 \begin{document}
    42 
    43 \selectlanguage{english}
    44 
    45 \title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]
    46 Picking Nits \\[\smallskipamount]
    47 \Large A User's Guide to Nitpick for Isabelle/HOL}
    48 \author{\hbox{} \\
    49 Jasmin Christian Blanchette \\
    50 {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
    51 \hbox{}}
    52 
    53 \maketitle
    54 
    55 \tableofcontents
    56 
    57 \setlength{\parskip}{.7em plus .2em minus .1em}
    58 \setlength{\parindent}{0pt}
    59 \setlength{\abovedisplayskip}{\parskip}
    60 \setlength{\abovedisplayshortskip}{.9\parskip}
    61 \setlength{\belowdisplayskip}{\parskip}
    62 \setlength{\belowdisplayshortskip}{.9\parskip}
    63 
    64 % General-purpose enum environment with correct spacing
    65 \newenvironment{enum}%
    66     {\begin{list}{}{%
    67         \setlength{\topsep}{.1\parskip}%
    68         \setlength{\partopsep}{.1\parskip}%
    69         \setlength{\itemsep}{\parskip}%
    70         \advance\itemsep by-\parsep}}
    71     {\end{list}}
    72 
    73 \def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
    74 \advance\rightskip by\leftmargin}
    75 \def\post{\vskip0pt plus1ex\endgroup}
    76 
    77 \def\prew{\pre\advance\rightskip by-\leftmargin}
    78 \def\postw{\post}
    79 
    80 \section{Introduction}
    81 \label{introduction}
    82 
    83 Nitpick \cite{blanchette-nipkow-2009} is a counterexample generator for
    84 Isabelle/HOL \cite{isa-tutorial} that is designed to handle formulas
    85 combining (co)in\-duc\-tive datatypes, (co)in\-duc\-tively defined predicates, and
    86 quantifiers. It builds on Kodkod \cite{torlak-jackson-2007}, a highly optimized
    87 first-order relational model finder developed by the Software Design Group at
    88 MIT. It is conceptually similar to Refute \cite{weber-2008}, from which it
    89 borrows many ideas and code fragments, but it benefits from Kodkod's
    90 optimizations and a new encoding scheme. The name Nitpick is shamelessly
    91 appropriated from a now retired Alloy precursor.
    92 
    93 Nitpick is easy to use---you simply enter \textbf{nitpick} after a putative
    94 theorem and wait a few seconds. Nonetheless, there are situations where knowing
    95 how it works under the hood and how it reacts to various options helps
    96 increase the test coverage. This manual also explains how to install the tool on
    97 your workstation. Should the motivation fail you, think of the many hours of
    98 hard work Nitpick will save you. Proving non-theorems is \textsl{hard work}.
    99 
   100 Another common use of Nitpick is to find out whether the axioms of a locale are
   101 satisfiable, while the locale is being developed. To check this, it suffices to
   102 write
   103 
   104 \prew
   105 \textbf{lemma}~``$\textit{False}$'' \\
   106 \textbf{nitpick}~[\textit{show\_all}]
   107 \postw
   108 
   109 after the locale's \textbf{begin} keyword. To falsify \textit{False}, Nitpick
   110 must find a model for the axioms. If it finds no model, we have an indication
   111 that the axioms might be unsatisfiable.
   112 
   113 Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.5 virtual
   114 machine called \texttt{java}. The examples presented in this manual can be found
   115 in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
   116 
   117 Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
   118 Nitpick also provides an automatic mode that can be enabled using the
   119 ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof General. In this
   120 mode, Nitpick is run on every newly entered theorem, much like Auto Quickcheck.
   121 The collective time limit for Auto Nitpick and Auto Quickcheck can be set using
   122 the ``Auto Counterexample Time Limit'' option.
   123 
   124 \newbox\boxA
   125 \setbox\boxA=\hbox{\texttt{nospam}}
   126 
   127 The known bugs and limitations at the time of writing are listed in
   128 \S\ref{known-bugs-and-limitations}. Comments and bug reports concerning Nitpick
   129 or this manual should be directed to
   130 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
   131 in.\allowbreak tum.\allowbreak de}.
   132 
   133 \vskip2.5\smallskipamount
   134 
   135 \textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
   136 suggesting several textual improvements.
   137 % and Perry James for reporting a typo.
   138 
   139 \section{First Steps}
   140 \label{first-steps}
   141 
   142 This section introduces Nitpick by presenting small examples. If possible, you
   143 should try out the examples on your workstation. Your theory file should start
   144 the standard way:
   145 
   146 \prew
   147 \textbf{theory}~\textit{Scratch} \\
   148 \textbf{imports}~\textit{Main} \\
   149 \textbf{begin}
   150 \postw
   151 
   152 The results presented here were obtained using the JNI version of MiniSat and
   153 with multithreading disabled to reduce nondeterminism. This was done by adding
   154 the line
   155 
   156 \prew
   157 \textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1]
   158 \postw
   159 
   160 after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
   161 Kodkodi and is precompiled for the major platforms. Other SAT solvers can also
   162 be installed, as explained in \S\ref{optimizations}. If you have already
   163 configured SAT solvers in Isabelle (e.g., for Refute), these will also be
   164 available to Nitpick.
   165 
   166 \subsection{Propositional Logic}
   167 \label{propositional-logic}
   168 
   169 Let's start with a trivial example from propositional logic:
   170 
   171 \prew
   172 \textbf{lemma}~``$P \longleftrightarrow Q$'' \\
   173 \textbf{nitpick}
   174 \postw
   175 
   176 You should get the following output:
   177 
   178 \prew
   179 \slshape
   180 Nitpick found a counterexample: \\[2\smallskipamount]
   181 \hbox{}\qquad Free variables: \nopagebreak \\
   182 \hbox{}\qquad\qquad $P = \textit{True}$ \\
   183 \hbox{}\qquad\qquad $Q = \textit{False}$
   184 \postw
   185 
   186 Nitpick can also be invoked on individual subgoals, as in the example below:
   187 
   188 \prew
   189 \textbf{apply}~\textit{auto} \\[2\smallskipamount]
   190 {\slshape goal (2 subgoals): \\
   191 \phantom{0}1. $P\,\Longrightarrow\, Q$ \\
   192 \phantom{0}2. $Q\,\Longrightarrow\, P$} \\[2\smallskipamount]
   193 \textbf{nitpick}~1 \\[2\smallskipamount]
   194 {\slshape Nitpick found a counterexample: \\[2\smallskipamount]
   195 \hbox{}\qquad Free variables: \nopagebreak \\
   196 \hbox{}\qquad\qquad $P = \textit{True}$ \\
   197 \hbox{}\qquad\qquad $Q = \textit{False}$} \\[2\smallskipamount]
   198 \textbf{nitpick}~2 \\[2\smallskipamount]
   199 {\slshape Nitpick found a counterexample: \\[2\smallskipamount]
   200 \hbox{}\qquad Free variables: \nopagebreak \\
   201 \hbox{}\qquad\qquad $P = \textit{False}$ \\
   202 \hbox{}\qquad\qquad $Q = \textit{True}$} \\[2\smallskipamount]
   203 \textbf{oops}
   204 \postw
   205 
   206 \subsection{Type Variables}
   207 \label{type-variables}
   208 
   209 If you are left unimpressed by the previous example, don't worry. The next
   210 one is more mind- and computer-boggling:
   211 
   212 \prew
   213 \textbf{lemma} ``$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
   214 \postw
   215 \pagebreak[2] %% TYPESETTING
   216 
   217 The putative lemma involves the definite description operator, {THE}, presented
   218 in section 5.10.1 of the Isabelle tutorial \cite{isa-tutorial}. The
   219 operator is defined by the axiom $(\textrm{THE}~x.\; x = a) = a$. The putative
   220 lemma is merely asserting the indefinite description operator axiom with {THE}
   221 substituted for {SOME}.
   222 
   223 The free variable $x$ and the bound variable $y$ have type $'a$. For formulas
   224 containing type variables, Nitpick enumerates the possible domains for each type
   225 variable, up to a given cardinality (8 by default), looking for a finite
   226 countermodel:
   227 
   228 \prew
   229 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
   230 \slshape
   231 Trying 8 scopes: \nopagebreak \\
   232 \hbox{}\qquad \textit{card}~$'a$~= 1; \\
   233 \hbox{}\qquad \textit{card}~$'a$~= 2; \\
   234 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
   235 \hbox{}\qquad \textit{card}~$'a$~= 8. \\[2\smallskipamount]
   236 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
   237 \hbox{}\qquad Free variables: \nopagebreak \\
   238 \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
   239 \hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount]
   240 Total time: 580 ms.
   241 \postw
   242 
   243 Nitpick found a counterexample in which $'a$ has cardinality 3. (For
   244 cardinalities 1 and 2, the formula holds.) In the counterexample, the three
   245 values of type $'a$ are written $a_1$, $a_2$, and $a_3$.
   246 
   247 The message ``Trying $n$ scopes: {\ldots}''\ is shown only if the option
   248 \textit{verbose} is enabled. You can specify \textit{verbose} each time you
   249 invoke \textbf{nitpick}, or you can set it globally using the command
   250 
   251 \prew
   252 \textbf{nitpick\_params} [\textit{verbose}]
   253 \postw
   254 
   255 This command also displays the current default values for all of the options
   256 supported by Nitpick. The options are listed in \S\ref{option-reference}.
   257 
   258 \subsection{Constants}
   259 \label{constants}
   260 
   261 By just looking at Nitpick's output, it might not be clear why the
   262 counterexample in \S\ref{type-variables} is genuine. Let's invoke Nitpick again,
   263 this time telling it to show the values of the constants that occur in the
   264 formula:
   265 
   266 \prew
   267 \textbf{lemma}~``$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$'' \\
   268 \textbf{nitpick}~[\textit{show\_consts}] \\[2\smallskipamount]
   269 \slshape
   270 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
   271 \hbox{}\qquad Free variables: \nopagebreak \\
   272 \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
   273 \hbox{}\qquad\qquad $x = a_3$ \\
   274 \hbox{}\qquad Constant: \nopagebreak \\
   275 \hbox{}\qquad\qquad $\textit{The}~\textsl{fallback} = a_1$
   276 \postw
   277 
   278 We can see more clearly now. Since the predicate $P$ isn't true for a unique
   279 value, $\textrm{THE}~y.\;P~y$ can denote any value of type $'a$, even
   280 $a_1$. Since $P~a_1$ is false, the entire formula is falsified.
   281 
   282 As an optimization, Nitpick's preprocessor introduced the special constant
   283 ``\textit{The} fallback'' corresponding to $\textrm{THE}~y.\;P~y$ (i.e.,
   284 $\mathit{The}~(\lambda y.\;P~y)$) when there doesn't exist a unique $y$
   285 satisfying $P~y$. We disable this optimization by passing the
   286 \textit{full\_descrs} option:
   287 
   288 \prew
   289 \textbf{nitpick}~[\textit{full\_descrs},\, \textit{show\_consts}] \\[2\smallskipamount]
   290 \slshape
   291 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
   292 \hbox{}\qquad Free variables: \nopagebreak \\
   293 \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
   294 \hbox{}\qquad\qquad $x = a_3$ \\
   295 \hbox{}\qquad Constant: \nopagebreak \\
   296 \hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$
   297 \postw
   298 
   299 As the result of another optimization, Nitpick directly assigned a value to the
   300 subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we
   301 disable this second optimization by using the command
   302 
   303 \prew
   304 \textbf{nitpick}~[\textit{dont\_specialize},\, \textit{full\_descrs},\,
   305 \textit{show\_consts}]
   306 \postw
   307 
   308 we finally get \textit{The}:
   309 
   310 \prew
   311 \slshape Constant: \nopagebreak \\
   312 \hbox{}\qquad $\mathit{The} = \undef{}
   313     (\!\begin{aligned}[t]%
   314     & \{a_1, a_2, a_3\} := a_3,\> \{a_1, a_2\} := a_3,\> \{a_1, a_3\} := a_3, \\[-2pt] %% TYPESETTING
   315     & \{a_1\} := a_1,\> \{a_2, a_3\} := a_1,\> \{a_2\} := a_2, \\[-2pt]
   316     & \{a_3\} := a_3,\> \{\} := a_3)\end{aligned}$
   317 \postw
   318 
   319 Notice that $\textit{The}~(\lambda y.\;P~y) = \textit{The}~\{a_2, a_3\} = a_1$,
   320 just like before.\footnote{The Isabelle/HOL notation $f(x :=
   321 y)$ denotes the function that maps $x$ to $y$ and that otherwise behaves like
   322 $f$.}
   323 
   324 Our misadventures with THE suggest adding `$\exists!x{.}$' (``there exists a
   325 unique $x$ such that'') at the front of our putative lemma's assumption:
   326 
   327 \prew
   328 \textbf{lemma}~``$\exists {!}x.\; P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
   329 \postw
   330 
   331 The fix appears to work:
   332 
   333 \prew
   334 \textbf{nitpick} \\[2\smallskipamount]
   335 \slshape Nitpick found no counterexample.
   336 \postw
   337 
   338 We can further increase our confidence in the formula by exhausting all
   339 cardinalities up to 50:
   340 
   341 \prew
   342 \textbf{nitpick} [\textit{card} $'a$~= 1--50]\footnote{The symbol `--'
   343 can be entered as \texttt{-} (hyphen) or
   344 \texttt{\char`\\\char`\<midarrow\char`\>}.} \\[2\smallskipamount]
   345 \slshape Nitpick found no counterexample.
   346 \postw
   347 
   348 Let's see if Sledgehammer \cite{sledgehammer-2009} can find a proof:
   349 
   350 \prew
   351 \textbf{sledgehammer} \\[2\smallskipamount]
   352 {\slshape Sledgehammer: external prover ``$e$'' for subgoal 1: \\
   353 $\exists{!}x.\; P~x\,\Longrightarrow\, P~(\hbox{\slshape THE}~y.\; P~y)$ \\
   354 Try this command: \textrm{apply}~(\textit{metis~the\_equality})} \\[2\smallskipamount]
   355 \textbf{apply}~(\textit{metis~the\_equality\/}) \nopagebreak \\[2\smallskipamount]
   356 {\slshape No subgoals!}% \\[2\smallskipamount]
   357 %\textbf{done}
   358 \postw
   359 
   360 This must be our lucky day.
   361 
   362 \subsection{Skolemization}
   363 \label{skolemization}
   364 
   365 Are all invertible functions onto? Let's find out:
   366 
   367 \prew
   368 \textbf{lemma} ``$\exists g.\; \forall x.~g~(f~x) = x
   369  \,\Longrightarrow\, \forall y.\; \exists x.~y = f~x$'' \\
   370 \textbf{nitpick} \\[2\smallskipamount]
   371 \slshape
   372 Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\[2\smallskipamount]
   373 \hbox{}\qquad Free variable: \nopagebreak \\
   374 \hbox{}\qquad\qquad $f = \undef{}(b_1 := a_1)$ \\
   375 \hbox{}\qquad Skolem constants: \nopagebreak \\
   376 \hbox{}\qquad\qquad $g = \undef{}(a_1 := b_1,\> a_2 := b_1)$ \\
   377 \hbox{}\qquad\qquad $y = a_2$
   378 \postw
   379 
   380 Although $f$ is the only free variable occurring in the formula, Nitpick also
   381 displays values for the bound variables $g$ and $y$. These values are available
   382 to Nitpick because it performs skolemization as a preprocessing step.
   383 
   384 In the previous example, skolemization only affected the outermost quantifiers.
   385 This is not always the case, as illustrated below:
   386 
   387 \prew
   388 \textbf{lemma} ``$\exists x.\; \forall f.\; f~x = x$'' \\
   389 \textbf{nitpick} \\[2\smallskipamount]
   390 \slshape
   391 Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
   392 \hbox{}\qquad Skolem constant: \nopagebreak \\
   393 \hbox{}\qquad\qquad $\lambda x.\; f =
   394     \undef{}(\!\begin{aligned}[t]
   395     & a_1 := \undef{}(a_1 := a_2,\> a_2 := a_1), \\[-2pt]
   396     & a_2 := \undef{}(a_1 := a_1,\> a_2 := a_1))\end{aligned}$
   397 \postw
   398 
   399 The variable $f$ is bound within the scope of $x$; therefore, $f$ depends on
   400 $x$, as suggested by the notation $\lambda x.\,f$. If $x = a_1$, then $f$ is the
   401 function that maps $a_1$ to $a_2$ and vice versa; otherwise, $x = a_2$ and $f$
   402 maps both $a_1$ and $a_2$ to $a_1$. In both cases, $f~x \not= x$.
   403 
   404 The source of the Skolem constants is sometimes more obscure:
   405 
   406 \prew
   407 \textbf{lemma} ``$\mathit{refl}~r\,\Longrightarrow\, \mathit{sym}~r$'' \\
   408 \textbf{nitpick} \\[2\smallskipamount]
   409 \slshape
   410 Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
   411 \hbox{}\qquad Free variable: \nopagebreak \\
   412 \hbox{}\qquad\qquad $r = \{(a_1, a_1),\, (a_2, a_1),\, (a_2, a_2)\}$ \\
   413 \hbox{}\qquad Skolem constants: \nopagebreak \\
   414 \hbox{}\qquad\qquad $\mathit{sym}.x = a_2$ \\
   415 \hbox{}\qquad\qquad $\mathit{sym}.y = a_1$
   416 \postw
   417 
   418 What happened here is that Nitpick expanded the \textit{sym} constant to its
   419 definition:
   420 
   421 \prew
   422 $\mathit{sym}~r \,\equiv\,
   423  \forall x\> y.\,\> (x, y) \in r \longrightarrow (y, x) \in r.$
   424 \postw
   425 
   426 As their names suggest, the Skolem constants $\mathit{sym}.x$ and
   427 $\mathit{sym}.y$ are simply the bound variables $x$ and $y$
   428 from \textit{sym}'s definition.
   429 
   430 Although skolemization is a useful optimization, you can disable it by invoking
   431 Nitpick with \textit{dont\_skolemize}. See \S\ref{optimizations} for details.
   432 
   433 \subsection{Natural Numbers and Integers}
   434 \label{natural-numbers-and-integers}
   435 
   436 Because of the axiom of infinity, the type \textit{nat} does not admit any
   437 finite models. To deal with this, Nitpick's approach is to consider finite
   438 subsets $N$ of \textit{nat} and maps all numbers $\notin N$ to the undefined
   439 value (displayed as `$\unk$'). The type \textit{int} is handled similarly.
   440 Internally, undefined values lead to a three-valued logic.
   441 
   442 Here is an example involving \textit{int}:
   443 
   444 \prew
   445 \textbf{lemma} ``$\lbrakk i \le j;\> n \le (m{\Colon}\mathit{int})\rbrakk \,\Longrightarrow\, i * n + j * m \le i * m + j * n$'' \\
   446 \textbf{nitpick} \\[2\smallskipamount]
   447 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
   448 \hbox{}\qquad Free variables: \nopagebreak \\
   449 \hbox{}\qquad\qquad $i = 0$ \\
   450 \hbox{}\qquad\qquad $j = 1$ \\
   451 \hbox{}\qquad\qquad $m = 1$ \\
   452 \hbox{}\qquad\qquad $n = 0$
   453 \postw
   454 
   455 Internally, Nitpick uses either a unary or a binary representation of numbers.
   456 The unary representation is more efficient but only suitable for numbers very
   457 close to zero. By default, Nitpick attempts to choose the more appropriate
   458 encoding by inspecting the formula at hand. This behavior can be overridden by
   459 passing either \textit{unary\_ints} or \textit{binary\_ints} as option. For
   460 binary notation, the number of bits to use can be specified using
   461 the \textit{bits} option. For example:
   462 
   463 \prew
   464 \textbf{nitpick} [\textit{binary\_ints}, \textit{bits}${} = 16$]
   465 \postw
   466 
   467 With infinite types, we don't always have the luxury of a genuine counterexample
   468 and must often content ourselves with a potential one. The tedious task of
   469 finding out whether the potential counterexample is in fact genuine can be
   470 outsourced to \textit{auto} by passing \textit{check\_potential}. For example:
   471 
   472 \prew
   473 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
   474 \textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
   475 \slshape Warning: The conjecture either trivially holds or (more likely) lies outside Nitpick's supported
   476 fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
   477 Nitpick found a potential counterexample: \\[2\smallskipamount]
   478 \hbox{}\qquad Free variable: \nopagebreak \\
   479 \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
   480 Confirmation by ``\textit{auto}'': The above counterexample is genuine.
   481 \postw
   482 
   483 You might wonder why the counterexample is first reported as potential. The root
   484 of the problem is that the bound variable in $\forall n.\; \textit{Suc}~n
   485 \mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds an $n$ such
   486 that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
   487 \textit{False}; but otherwise, it does not know anything about values of $n \ge
   488 \textit{card~nat}$ and must therefore evaluate the assumption to $\unk$, not
   489 \textit{True}. Since the assumption can never be satisfied, the putative lemma
   490 can never be falsified.
   491 
   492 Incidentally, if you distrust the so-called genuine counterexamples, you can
   493 enable \textit{check\_\allowbreak genuine} to verify them as well. However, be
   494 aware that \textit{auto} will usually fail to prove that the counterexample is
   495 genuine or spurious.
   496 
   497 Some conjectures involving elementary number theory make Nitpick look like a
   498 giant with feet of clay:
   499 
   500 \prew
   501 \textbf{lemma} ``$P~\textit{Suc}$'' \\
   502 \textbf{nitpick} [\textit{card} = 1--6] \\[2\smallskipamount]
   503 \slshape
   504 Nitpick found no counterexample.
   505 \postw
   506 
   507 On any finite set $N$, \textit{Suc} is a partial function; for example, if $N =
   508 \{0, 1, \ldots, k\}$, then \textit{Suc} is $\{0 \mapsto 1,\, 1 \mapsto 2,\,
   509 \ldots,\, k \mapsto \unk\}$, which evaluates to $\unk$ when passed as
   510 argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$. The next
   511 example is similar:
   512 
   513 \prew
   514 \textbf{lemma} ``$P~(\textit{op}~{+}\Colon
   515 \textit{nat}\mathbin{\Rightarrow}\textit{nat}\mathbin{\Rightarrow}\textit{nat})$'' \\
   516 \textbf{nitpick} [\textit{card nat} = 1] \\[2\smallskipamount]
   517 {\slshape Nitpick found a counterexample:} \\[2\smallskipamount]
   518 \hbox{}\qquad Free variable: \nopagebreak \\
   519 \hbox{}\qquad\qquad $P = \{\}$ \\[2\smallskipamount]
   520 \textbf{nitpick} [\textit{card nat} = 2] \\[2\smallskipamount]
   521 {\slshape Nitpick found no counterexample.}
   522 \postw
   523 
   524 The problem here is that \textit{op}~+ is total when \textit{nat} is taken to be
   525 $\{0\}$ but becomes partial as soon as we add $1$, because $1 + 1 \notin \{0,
   526 1\}$.
   527 
   528 Because numbers are infinite and are approximated using a three-valued logic,
   529 there is usually no need to systematically enumerate domain sizes. If Nitpick
   530 cannot find a genuine counterexample for \textit{card~nat}~= $k$, it is very
   531 unlikely that one could be found for smaller domains. (The $P~(\textit{op}~{+})$
   532 example above is an exception to this principle.) Nitpick nonetheless enumerates
   533 all cardinalities from 1 to 8 for \textit{nat}, mainly because smaller
   534 cardinalities are fast to handle and give rise to simpler counterexamples. This
   535 is explained in more detail in \S\ref{scope-monotonicity}.
   536 
   537 \subsection{Inductive Datatypes}
   538 \label{inductive-datatypes}
   539 
   540 Like natural numbers and integers, inductive datatypes with recursive
   541 constructors admit no finite models and must be approximated by a subterm-closed
   542 subset. For example, using a cardinality of 10 for ${'}a~\textit{list}$,
   543 Nitpick looks for all counterexamples that can be built using at most 10
   544 different lists.
   545 
   546 Let's see with an example involving \textit{hd} (which returns the first element
   547 of a list) and $@$ (which concatenates two lists):
   548 
   549 \prew
   550 \textbf{lemma} ``$\textit{hd}~(\textit{xs} \mathbin{@} [y, y]) = \textit{hd}~\textit{xs}$'' \\
   551 \textbf{nitpick} \\[2\smallskipamount]
   552 \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
   553 \hbox{}\qquad Free variables: \nopagebreak \\
   554 \hbox{}\qquad\qquad $\textit{xs} = []$ \\
   555 \hbox{}\qquad\qquad $\textit{y} = a_1$
   556 \postw
   557 
   558 To see why the counterexample is genuine, we enable \textit{show\_consts}
   559 and \textit{show\_\allowbreak datatypes}:
   560 
   561 \prew
   562 {\slshape Datatype:} \\
   563 \hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_1],\, [a_1, a_1],\, \unr\}$ \\
   564 {\slshape Constants:} \\
   565 \hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_1, a_1])$ \\
   566 \hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_1] := a_1,\> [a_1, a_1] := a_1)$
   567 \postw
   568 
   569 Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value,
   570 including $a_2$.
   571 
   572 The second constant, $\lambda x_1.\; x_1 \mathbin{@} [y, y]$, is simply the
   573 append operator whose second argument is fixed to be $[y, y]$. Appending $[a_1,
   574 a_1]$ to $[a_1]$ would normally give $[a_1, a_1, a_1]$, but this value is not
   575 representable in the subset of $'a$~\textit{list} considered by Nitpick, which
   576 is shown under the ``Datatype'' heading; hence the result is $\unk$. Similarly,
   577 appending $[a_1, a_1]$ to itself gives $\unk$.
   578 
   579 Given \textit{card}~$'a = 3$ and \textit{card}~$'a~\textit{list} = 3$, Nitpick
   580 considers the following subsets:
   581 
   582 \kern-.5\smallskipamount %% TYPESETTING
   583 
   584 \prew
   585 \begin{multicols}{3}
   586 $\{[],\, [a_1],\, [a_2]\}$; \\
   587 $\{[],\, [a_1],\, [a_3]\}$; \\
   588 $\{[],\, [a_2],\, [a_3]\}$; \\
   589 $\{[],\, [a_1],\, [a_1, a_1]\}$; \\
   590 $\{[],\, [a_1],\, [a_2, a_1]\}$; \\
   591 $\{[],\, [a_1],\, [a_3, a_1]\}$; \\
   592 $\{[],\, [a_2],\, [a_1, a_2]\}$; \\
   593 $\{[],\, [a_2],\, [a_2, a_2]\}$; \\
   594 $\{[],\, [a_2],\, [a_3, a_2]\}$; \\
   595 $\{[],\, [a_3],\, [a_1, a_3]\}$; \\
   596 $\{[],\, [a_3],\, [a_2, a_3]\}$; \\
   597 $\{[],\, [a_3],\, [a_3, a_3]\}$.
   598 \end{multicols}
   599 \postw
   600 
   601 \kern-2\smallskipamount %% TYPESETTING
   602 
   603 All subterm-closed subsets of $'a~\textit{list}$ consisting of three values
   604 are listed and only those. As an example of a non-subterm-closed subset,
   605 consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_2]\}$, and observe
   606 that $[a_1, a_2]$ (i.e., $a_1 \mathbin{\#} [a_2]$) has $[a_2] \notin
   607 \mathcal{S}$ as a subterm.
   608 
   609 Here's another m\"ochtegern-lemma that Nitpick can refute without a blink:
   610 
   611 \prew
   612 \textbf{lemma} ``$\lbrakk \textit{length}~\textit{xs} = 1;\> \textit{length}~\textit{ys} = 1
   613 \rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$''
   614 \\
   615 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
   616 \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
   617 \hbox{}\qquad Free variables: \nopagebreak \\
   618 \hbox{}\qquad\qquad $\textit{xs} = [a_1]$ \\
   619 \hbox{}\qquad\qquad $\textit{ys} = [a_2]$ \\
   620 \hbox{}\qquad Datatypes: \\
   621 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
   622 \hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_1],\, [a_2],\, \unr\}$
   623 \postw
   624 
   625 Because datatypes are approximated using a three-valued logic, there is usually
   626 no need to systematically enumerate cardinalities: If Nitpick cannot find a
   627 genuine counterexample for \textit{card}~$'a~\textit{list}$~= 10, it is very
   628 unlikely that one could be found for smaller cardinalities.
   629 
   630 \subsection{Typedefs, Records, Rationals, and Reals}
   631 \label{typedefs-records-rationals-and-reals}
   632 
   633 Nitpick generally treats types declared using \textbf{typedef} as datatypes
   634 whose single constructor is the corresponding \textit{Abs\_\kern.1ex} function.
   635 For example:
   636 
   637 \prew
   638 \textbf{typedef}~\textit{three} = ``$\{0\Colon\textit{nat},\, 1,\, 2\}$'' \\
   639 \textbf{by}~\textit{blast} \\[2\smallskipamount]
   640 \textbf{definition}~$A \mathbin{\Colon} \textit{three}$ \textbf{where} ``\kern-.1em$A \,\equiv\, \textit{Abs\_\allowbreak three}~0$'' \\
   641 \textbf{definition}~$B \mathbin{\Colon} \textit{three}$ \textbf{where} ``$B \,\equiv\, \textit{Abs\_three}~1$'' \\
   642 \textbf{definition}~$C \mathbin{\Colon} \textit{three}$ \textbf{where} ``$C \,\equiv\, \textit{Abs\_three}~2$'' \\[2\smallskipamount]
   643 \textbf{lemma} ``$\lbrakk P~A;\> P~B\rbrakk \,\Longrightarrow\, P~x$'' \\
   644 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
   645 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
   646 \hbox{}\qquad Free variables: \nopagebreak \\
   647 \hbox{}\qquad\qquad $P = \{\Abs{0},\, \Abs{1}\}$ \\
   648 \hbox{}\qquad\qquad $x = \Abs{2}$ \\
   649 \hbox{}\qquad Datatypes: \\
   650 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
   651 \hbox{}\qquad\qquad $\textit{three} = \{\Abs{0},\, \Abs{1},\, \Abs{2},\, \unr\}$
   652 \postw
   653 
   654 %% MARK
   655 In the output above, $\Abs{n}$ abbreviates $\textit{Abs\_three}~n$.
   656 
   657 %% MARK
   658 Records, which are implemented as \textbf{typedef}s behind the scenes, are
   659 handled in much the same way:
   660 
   661 \prew
   662 \textbf{record} \textit{point} = \\
   663 \hbox{}\quad $\textit{Xcoord} \mathbin{\Colon} \textit{int}$ \\
   664 \hbox{}\quad $\textit{Ycoord} \mathbin{\Colon} \textit{int}$ \\[2\smallskipamount]
   665 \textbf{lemma} ``$\textit{Xcoord}~(p\Colon\textit{point}) = \textit{Xcoord}~(q\Colon\textit{point})$'' \\
   666 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
   667 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
   668 \hbox{}\qquad Free variables: \nopagebreak \\
   669 \hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
   670 \hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
   671 \hbox{}\qquad Datatypes: \\
   672 \hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, \unr\}$ \\
   673 \hbox{}\qquad\qquad $\textit{point} = \{\!\begin{aligned}[t]
   674 & \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr, \\[-2pt] %% TYPESETTING
   675 & \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
   676 \postw
   677 
   678 Finally, Nitpick provides rudimentary support for rationals and reals using a
   679 similar approach:
   680 
   681 \prew
   682 \textbf{lemma} ``$4 * x + 3 * (y\Colon\textit{real}) \not= 1/2$'' \\
   683 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
   684 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
   685 \hbox{}\qquad Free variables: \nopagebreak \\
   686 \hbox{}\qquad\qquad $x = 1/2$ \\
   687 \hbox{}\qquad\qquad $y = -1/2$ \\
   688 \hbox{}\qquad Datatypes: \\
   689 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, 3,\, 4,\, 5,\, 6,\, 7,\, \unr\}$ \\
   690 \hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, 2,\, 3,\, 4,\, -3,\, -2,\, -1,\, \unr\}$ \\
   691 \hbox{}\qquad\qquad $\textit{real} = \{1,\, 0,\, 4,\, -3/2,\, 3,\, 2,\, 1/2,\, -1/2,\, \unr\}$
   692 \postw
   693 
   694 \subsection{Inductive and Coinductive Predicates}
   695 \label{inductive-and-coinductive-predicates}
   696 
   697 Inductively defined predicates (and sets) are particularly problematic for
   698 counterexample generators. They can make Quickcheck~\cite{berghofer-nipkow-2004}
   699 loop forever and Refute~\cite{weber-2008} run out of resources. The crux of
   700 the problem is that they are defined using a least fixed point construction.
   701 
   702 Nitpick's philosophy is that not all inductive predicates are equal. Consider
   703 the \textit{even} predicate below:
   704 
   705 \prew
   706 \textbf{inductive}~\textit{even}~\textbf{where} \\
   707 ``\textit{even}~0'' $\,\mid$ \\
   708 ``\textit{even}~$n\,\Longrightarrow\, \textit{even}~(\textit{Suc}~(\textit{Suc}~n))$''
   709 \postw
   710 
   711 This predicate enjoys the desirable property of being well-founded, which means
   712 that the introduction rules don't give rise to infinite chains of the form
   713 
   714 \prew
   715 $\cdots\,\Longrightarrow\, \textit{even}~k''
   716        \,\Longrightarrow\, \textit{even}~k'
   717        \,\Longrightarrow\, \textit{even}~k.$
   718 \postw
   719 
   720 For \textit{even}, this is obvious: Any chain ending at $k$ will be of length
   721 $k/2 + 1$:
   722 
   723 \prew
   724 $\textit{even}~0\,\Longrightarrow\, \textit{even}~2\,\Longrightarrow\, \cdots
   725        \,\Longrightarrow\, \textit{even}~(k - 2)
   726        \,\Longrightarrow\, \textit{even}~k.$
   727 \postw
   728 
   729 Wellfoundedness is desirable because it enables Nitpick to use a very efficient
   730 fixed point computation.%
   731 \footnote{If an inductive predicate is
   732 well-founded, then it has exactly one fixed point, which is simultaneously the
   733 least and the greatest fixed point. In these circumstances, the computation of
   734 the least fixed point amounts to the computation of an arbitrary fixed point,
   735 which can be performed using a straightforward recursive equation.}
   736 Moreover, Nitpick can prove wellfoundedness of most well-founded predicates,
   737 just as Isabelle's \textbf{function} package usually discharges termination
   738 proof obligations automatically.
   739 
   740 Let's try an example:
   741 
   742 \prew
   743 \textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
   744 \textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
   745 \slshape The inductive predicate ``\textit{even}'' was proved well-founded.
   746 Nitpick can compute it efficiently. \\[2\smallskipamount]
   747 Trying 1 scope: \\
   748 \hbox{}\qquad \textit{card nat}~= 100. \\[2\smallskipamount]
   749 Nitpick found a potential counterexample for \textit{card nat}~= 100: \\[2\smallskipamount]
   750 \hbox{}\qquad Empty assignment \\[2\smallskipamount]
   751 Nitpick could not find a better counterexample. \\[2\smallskipamount]
   752 Total time: 2274 ms.
   753 \postw
   754 
   755 No genuine counterexample is possible because Nitpick cannot rule out the
   756 existence of a natural number $n \ge 100$ such that both $\textit{even}~n$ and
   757 $\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the
   758 existential quantifier:
   759 
   760 \prew
   761 \textbf{lemma} ``$\exists n \mathbin{\le} 99.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
   762 \textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}] \\[2\smallskipamount]
   763 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
   764 \hbox{}\qquad Empty assignment
   765 \postw
   766 
   767 So far we were blessed by the wellfoundedness of \textit{even}. What happens if
   768 we use the following definition instead?
   769 
   770 \prew
   771 \textbf{inductive} $\textit{even}'$ \textbf{where} \\
   772 ``$\textit{even}'~(0{\Colon}\textit{nat})$'' $\,\mid$ \\
   773 ``$\textit{even}'~2$'' $\,\mid$ \\
   774 ``$\lbrakk\textit{even}'~m;\> \textit{even}'~n\rbrakk \,\Longrightarrow\, \textit{even}'~(m + n)$''
   775 \postw
   776 
   777 This definition is not well-founded: From $\textit{even}'~0$ and
   778 $\textit{even}'~0$, we can derive that $\textit{even}'~0$. Nonetheless, the
   779 predicates $\textit{even}$ and $\textit{even}'$ are equivalent.
   780 
   781 Let's check a property involving $\textit{even}'$. To make up for the
   782 foreseeable computational hurdles entailed by non-wellfoundedness, we decrease
   783 \textit{nat}'s cardinality to a mere 10:
   784 
   785 \prew
   786 \textbf{lemma}~``$\exists n \in \{0, 2, 4, 6, 8\}.\;
   787 \lnot\;\textit{even}'~n$'' \\
   788 \textbf{nitpick}~[\textit{card nat}~= 10,\, \textit{verbose},\, \textit{show\_consts}] \\[2\smallskipamount]
   789 \slshape
   790 The inductive predicate ``$\textit{even}'\!$'' could not be proved well-founded.
   791 Nitpick might need to unroll it. \\[2\smallskipamount]
   792 Trying 6 scopes: \\
   793 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 0; \\
   794 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 1; \\
   795 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2; \\
   796 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 4; \\
   797 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 8; \\
   798 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 9. \\[2\smallskipamount]
   799 Nitpick found a counterexample for \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2: \\[2\smallskipamount]
   800 \hbox{}\qquad Constant: \nopagebreak \\
   801 \hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t]
   802 & 2 := \{0, 2, 4, 6, 8, 1^\Q, 3^\Q, 5^\Q, 7^\Q, 9^\Q\}, \\[-2pt]
   803 & 1 := \{0, 2, 4, 1^\Q, 3^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\}, \\[-2pt]
   804 & 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\[2\smallskipamount]
   805 Total time: 1140 ms.
   806 \postw
   807 
   808 Nitpick's output is very instructive. First, it tells us that the predicate is
   809 unrolled, meaning that it is computed iteratively from the empty set. Then it
   810 lists six scopes specifying different bounds on the numbers of iterations:\ 0,
   811 1, 2, 4, 8, and~9.
   812 
   813 The output also shows how each iteration contributes to $\textit{even}'$. The
   814 notation $\lambda i.\; \textit{even}'$ indicates that the value of the
   815 predicate depends on an iteration counter. Iteration 0 provides the basis
   816 elements, $0$ and $2$. Iteration 1 contributes $4$ ($= 2 + 2$). Iteration 2
   817 throws $6$ ($= 2 + 4 = 4 + 2$) and $8$ ($= 4 + 4$) into the mix. Further
   818 iterations would not contribute any new elements.
   819 
   820 Some values are marked with superscripted question
   821 marks~(`\lower.2ex\hbox{$^\Q$}'). These are the elements for which the
   822 predicate evaluates to $\unk$. Thus, $\textit{even}'$ evaluates to either
   823 \textit{True} or $\unk$, never \textit{False}.
   824 
   825 When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, and 24
   826 iterations. However, these numbers are bounded by the cardinality of the
   827 predicate's domain. With \textit{card~nat}~= 10, no more than 9 iterations are
   828 ever needed to compute the value of a \textit{nat} predicate. You can specify
   829 the number of iterations using the \textit{iter} option, as explained in
   830 \S\ref{scope-of-search}.
   831 
   832 In the next formula, $\textit{even}'$ occurs both positively and negatively:
   833 
   834 \prew
   835 \textbf{lemma} ``$\textit{even}'~(n - 2) \,\Longrightarrow\, \textit{even}'~n$'' \\
   836 \textbf{nitpick} [\textit{card nat} = 10, \textit{show\_consts}] \\[2\smallskipamount]
   837 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
   838 \hbox{}\qquad Free variable: \nopagebreak \\
   839 \hbox{}\qquad\qquad $n = 1$ \\
   840 \hbox{}\qquad Constants: \nopagebreak \\
   841 \hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t]
   842 & 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$  \\
   843 \hbox{}\qquad\qquad $\textit{even}' \subseteq \{0, 2, 4, 6, 8, \unr\}$
   844 \postw
   845 
   846 Notice the special constraint $\textit{even}' \subseteq \{0,\, 2,\, 4,\, 6,\,
   847 8,\, \unr\}$ in the output, whose right-hand side represents an arbitrary
   848 fixed point (not necessarily the least one). It is used to falsify
   849 $\textit{even}'~n$. In contrast, the unrolled predicate is used to satisfy
   850 $\textit{even}'~(n - 2)$.
   851 
   852 Coinductive predicates are handled dually. For example:
   853 
   854 \prew
   855 \textbf{coinductive} \textit{nats} \textbf{where} \\
   856 ``$\textit{nats}~(x\Colon\textit{nat}) \,\Longrightarrow\, \textit{nats}~x$'' \\[2\smallskipamount]
   857 \textbf{lemma} ``$\textit{nats} = \{0, 1, 2, 3, 4\}$'' \\
   858 \textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
   859 \slshape Nitpick found a counterexample:
   860 \\[2\smallskipamount]
   861 \hbox{}\qquad Constants: \nopagebreak \\
   862 \hbox{}\qquad\qquad $\lambda i.\; \textit{nats} = \undef(0 := \{\!\begin{aligned}[t]
   863 & 0^\Q, 1^\Q, 2^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q, \\[-2pt]
   864 & \unr\})\end{aligned}$ \\
   865 \hbox{}\qquad\qquad $nats \supseteq \{9, 5^\Q, 6^\Q, 7^\Q, 8^\Q, \unr\}$
   866 \postw
   867 
   868 As a special case, Nitpick uses Kodkod's transitive closure operator to encode
   869 negative occurrences of non-well-founded ``linear inductive predicates,'' i.e.,
   870 inductive predicates for which each the predicate occurs in at most one
   871 assumption of each introduction rule. For example:
   872 
   873 \prew
   874 \textbf{inductive} \textit{odd} \textbf{where} \\
   875 ``$\textit{odd}~1$'' $\,\mid$ \\
   876 ``$\lbrakk \textit{odd}~m;\>\, \textit{even}~n\rbrakk \,\Longrightarrow\, \textit{odd}~(m + n)$'' \\[2\smallskipamount]
   877 \textbf{lemma}~``$\textit{odd}~n \,\Longrightarrow\, \textit{odd}~(n - 2)$'' \\
   878 \textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
   879 \slshape Nitpick found a counterexample:
   880 \\[2\smallskipamount]
   881 \hbox{}\qquad Free variable: \nopagebreak \\
   882 \hbox{}\qquad\qquad $n = 1$ \\
   883 \hbox{}\qquad Constants: \nopagebreak \\
   884 \hbox{}\qquad\qquad $\textit{even} = \{0, 2, 4, 6, 8, \unr\}$ \\
   885 \hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = \{1, \unr\}$ \\
   886 \hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \!
   887 \!\begin{aligned}[t]
   888   & \{(0, 0), (0, 2), (0, 4), (0, 6), (0, 8), (1, 1), (1, 3), (1, 5), \\[-2pt]
   889   & \phantom{\{} (1, 7), (1, 9), (2, 2), (2, 4), (2, 6), (2, 8), (3, 3),
   890        (3, 5), \\[-2pt]
   891   & \phantom{\{} (3, 7), (3, 9), (4, 4), (4, 6), (4, 8), (5, 5), (5, 7), (5, 9), \\[-2pt]
   892   & \phantom{\{} (6, 6), (6, 8), (7, 7), (7, 9), (8, 8), (9, 9), \unr\}\end{aligned}$ \\
   893 \hbox{}\qquad\qquad $\textit{odd} \subseteq \{1, 3, 5, 7, 9, 8^\Q, \unr\}$
   894 \postw
   895 
   896 \noindent
   897 In the output, $\textit{odd}_{\textrm{base}}$ represents the base elements and
   898 $\textit{odd}_{\textrm{step}}$ is a transition relation that computes new
   899 elements from known ones. The set $\textit{odd}$ consists of all the values
   900 reachable through the reflexive transitive closure of
   901 $\textit{odd}_{\textrm{step}}$ starting with any element from
   902 $\textit{odd}_{\textrm{base}}$, namely 1, 3, 5, 7, and 9. Using Kodkod's
   903 transitive closure to encode linear predicates is normally either more thorough
   904 or more efficient than unrolling (depending on the value of \textit{iter}), but
   905 for those cases where it isn't you can disable it by passing the
   906 \textit{dont\_star\_linear\_preds} option.
   907 
   908 \subsection{Coinductive Datatypes}
   909 \label{coinductive-datatypes}
   910 
   911 While Isabelle regrettably lacks a high-level mechanism for defining coinductive
   912 datatypes, the \textit{Coinductive\_List} theory provides a coinductive ``lazy
   913 list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick supports
   914 these lazy lists seamlessly and provides a hook, described in
   915 \S\ref{registration-of-coinductive-datatypes}, to register custom coinductive
   916 datatypes.
   917 
   918 (Co)intuitively, a coinductive datatype is similar to an inductive datatype but
   919 allows infinite objects. Thus, the infinite lists $\textit{ps}$ $=$ $[a, a, a,
   920 \ldots]$, $\textit{qs}$ $=$ $[a, b, a, b, \ldots]$, and $\textit{rs}$ $=$ $[0,
   921 1, 2, 3, \ldots]$ can be defined as lazy lists using the
   922 $\textit{LNil}\mathbin{\Colon}{'}a~\textit{llist}$ and
   923 $\textit{LCons}\mathbin{\Colon}{'}a \mathbin{\Rightarrow} {'}a~\textit{llist}
   924 \mathbin{\Rightarrow} {'}a~\textit{llist}$ constructors.
   925 
   926 Although it is otherwise no friend of infinity, Nitpick can find counterexamples
   927 involving cyclic lists such as \textit{ps} and \textit{qs} above as well as
   928 finite lists:
   929 
   930 \prew
   931 \textbf{lemma} ``$\textit{xs} \not= \textit{LCons}~a~\textit{xs}$'' \\
   932 \textbf{nitpick} \\[2\smallskipamount]
   933 \slshape Nitpick found a counterexample for {\itshape card}~$'a$ = 1: \\[2\smallskipamount]
   934 \hbox{}\qquad Free variables: \nopagebreak \\
   935 \hbox{}\qquad\qquad $\textit{a} = a_1$ \\
   936 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$
   937 \postw
   938 
   939 The notation $\textrm{THE}~\omega.\; \omega = t(\omega)$ stands
   940 for the infinite term $t(t(t(\ldots)))$. Hence, \textit{xs} is simply the
   941 infinite list $[a_1, a_1, a_1, \ldots]$.
   942 
   943 The next example is more interesting:
   944 
   945 \prew
   946 \textbf{lemma}~``$\lbrakk\textit{xs} = \textit{LCons}~a~\textit{xs};\>\,
   947 \textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
   948 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
   949 \slshape The type ``\kern1pt$'a$'' passed the monotonicity test. Nitpick might be able to skip
   950 some scopes. \\[2\smallskipamount]
   951 Trying 8 scopes: \\
   952 \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list}$''~= 1,
   953 and \textit{bisim\_depth}~= 0. \\
   954 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
   955 \hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} ``\kern1pt$'a~\textit{list}$''~= 8,
   956 and \textit{bisim\_depth}~= 7. \\[2\smallskipamount]
   957 Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
   958 \textit{card}~``\kern1pt$'a~\textit{list}$''~= 2, and \textit{bisim\_\allowbreak
   959 depth}~= 1:
   960 \\[2\smallskipamount]
   961 \hbox{}\qquad Free variables: \nopagebreak \\
   962 \hbox{}\qquad\qquad $\textit{a} = a_1$ \\
   963 \hbox{}\qquad\qquad $\textit{b} = a_2$ \\
   964 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
   965 \hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount]
   966 Total time: 726 ms.
   967 \postw
   968 
   969 The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas
   970 $\textit{ys}$ is $[a_2, a_1, a_1, a_1, \ldots]$, i.e., a lasso-shaped list with
   971 $[a_2]$ as its stem and $[a_1]$ as its cycle. In general, the list segment
   972 within the scope of the {THE} binder corresponds to the lasso's cycle, whereas
   973 the segment leading to the binder is the stem.
   974 
   975 A salient property of coinductive datatypes is that two objects are considered
   976 equal if and only if they lead to the same observations. For example, the lazy
   977 lists $\textrm{THE}~\omega.\; \omega =
   978 \textit{LCons}~a~(\textit{LCons}~b~\omega)$ and
   979 $\textit{LCons}~a~(\textrm{THE}~\omega.\; \omega =
   980 \textit{LCons}~b~(\textit{LCons}~a~\omega))$ are identical, because both lead
   981 to the sequence of observations $a$, $b$, $a$, $b$, \hbox{\ldots} (or,
   982 equivalently, both encode the infinite list $[a, b, a, b, \ldots]$). This
   983 concept of equality for coinductive datatypes is called bisimulation and is
   984 defined coinductively.
   985 
   986 Internally, Nitpick encodes the coinductive bisimilarity predicate as part of
   987 the Kodkod problem to ensure that distinct objects lead to different
   988 observations. This precaution is somewhat expensive and often unnecessary, so it
   989 can be disabled by setting the \textit{bisim\_depth} option to $-1$. The
   990 bisimilarity check is then performed \textsl{after} the counterexample has been
   991 found to ensure correctness. If this after-the-fact check fails, the
   992 counterexample is tagged as ``likely genuine'' and Nitpick recommends to try
   993 again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the
   994 check for the previous example saves approximately 150~milli\-seconds; the speed
   995 gains can be more significant for larger scopes.
   996 
   997 The next formula illustrates the need for bisimilarity (either as a Kodkod
   998 predicate or as an after-the-fact check) to prevent spurious counterexamples:
   999 
  1000 \prew
  1001 \textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
  1002 \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
  1003 \textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
  1004 \slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
  1005 \hbox{}\qquad Free variables: \nopagebreak \\
  1006 \hbox{}\qquad\qquad $a = a_1$ \\
  1007 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
  1008 \textit{LCons}~a_1~\omega$ \\
  1009 \hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
  1010 \hbox{}\qquad Codatatype:\strut \nopagebreak \\
  1011 \hbox{}\qquad\qquad $'a~\textit{llist} =
  1012 \{\!\begin{aligned}[t]
  1013   & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega, \\[-2pt]
  1014   & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega,\> \unr\}\end{aligned}$
  1015 \\[2\smallskipamount]
  1016 Try again with ``\textit{bisim\_depth}'' set to a nonnegative value to confirm
  1017 that the counterexample is genuine. \\[2\smallskipamount]
  1018 {\upshape\textbf{nitpick}} \\[2\smallskipamount]
  1019 \slshape Nitpick found no counterexample.
  1020 \postw
  1021 
  1022 In the first \textbf{nitpick} invocation, the after-the-fact check discovered 
  1023 that the two known elements of type $'a~\textit{llist}$ are bisimilar.
  1024 
  1025 A compromise between leaving out the bisimilarity predicate from the Kodkod
  1026 problem and performing the after-the-fact check is to specify a lower
  1027 nonnegative \textit{bisim\_depth} value than the default one provided by
  1028 Nitpick. In general, a value of $K$ means that Nitpick will require all lists to
  1029 be distinguished from each other by their prefixes of length $K$. Be aware that
  1030 setting $K$ to a too low value can overconstrain Nitpick, preventing it from
  1031 finding any counterexamples.
  1032 
  1033 \subsection{Boxing}
  1034 \label{boxing}
  1035 
  1036 Nitpick normally maps function and product types directly to the corresponding
  1037 Kodkod concepts. As a consequence, if $'a$ has cardinality 3 and $'b$ has
  1038 cardinality 4, then $'a \times {'}b$ has cardinality 12 ($= 4 \times 3$) and $'a
  1039 \Rightarrow {'}b$ has cardinality 64 ($= 4^3$). In some circumstances, it pays
  1040 off to treat these types in the same way as plain datatypes, by approximating
  1041 them by a subset of a given cardinality. This technique is called ``boxing'' and
  1042 is particularly useful for functions passed as arguments to other functions, for
  1043 high-arity functions, and for large tuples. Under the hood, boxing involves
  1044 wrapping occurrences of the types $'a \times {'}b$ and $'a \Rightarrow {'}b$ in
  1045 isomorphic datatypes, as can be seen by enabling the \textit{debug} option.
  1046 
  1047 To illustrate boxing, we consider a formalization of $\lambda$-terms represented
  1048 using de Bruijn's notation:
  1049 
  1050 \prew
  1051 \textbf{datatype} \textit{tm} = \textit{Var}~\textit{nat}~$\mid$~\textit{Lam}~\textit{tm} $\mid$ \textit{App~tm~tm}
  1052 \postw
  1053 
  1054 The $\textit{lift}~t~k$ function increments all variables with indices greater
  1055 than or equal to $k$ by one:
  1056 
  1057 \prew
  1058 \textbf{primrec} \textit{lift} \textbf{where} \\
  1059 ``$\textit{lift}~(\textit{Var}~j)~k = \textit{Var}~(\textrm{if}~j < k~\textrm{then}~j~\textrm{else}~j + 1)$'' $\mid$ \\
  1060 ``$\textit{lift}~(\textit{Lam}~t)~k = \textit{Lam}~(\textit{lift}~t~(k + 1))$'' $\mid$ \\
  1061 ``$\textit{lift}~(\textit{App}~t~u)~k = \textit{App}~(\textit{lift}~t~k)~(\textit{lift}~u~k)$''
  1062 \postw
  1063 
  1064 The $\textit{loose}~t~k$ predicate returns \textit{True} if and only if
  1065 term $t$ has a loose variable with index $k$ or more:
  1066 
  1067 \prew
  1068 \textbf{primrec}~\textit{loose} \textbf{where} \\
  1069 ``$\textit{loose}~(\textit{Var}~j)~k = (j \ge k)$'' $\mid$ \\
  1070 ``$\textit{loose}~(\textit{Lam}~t)~k = \textit{loose}~t~(\textit{Suc}~k)$'' $\mid$ \\
  1071 ``$\textit{loose}~(\textit{App}~t~u)~k = (\textit{loose}~t~k \mathrel{\lor} \textit{loose}~u~k)$''
  1072 \postw
  1073 
  1074 Next, the $\textit{subst}~\sigma~t$ function applies the substitution $\sigma$
  1075 on $t$:
  1076 
  1077 \prew
  1078 \textbf{primrec}~\textit{subst} \textbf{where} \\
  1079 ``$\textit{subst}~\sigma~(\textit{Var}~j) = \sigma~j$'' $\mid$ \\
  1080 ``$\textit{subst}~\sigma~(\textit{Lam}~t) = {}$\phantom{''} \\
  1081 \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$ \\
  1082 ``$\textit{subst}~\sigma~(\textit{App}~t~u) = \textit{App}~(\textit{subst}~\sigma~t)~(\textit{subst}~\sigma~u)$''
  1083 \postw
  1084 
  1085 A substitution is a function that maps variable indices to terms. Observe that
  1086 $\sigma$ is a function passed as argument and that Nitpick can't optimize it
  1087 away, because the recursive call for the \textit{Lam} case involves an altered
  1088 version. Also notice the \textit{lift} call, which increments the variable
  1089 indices when moving under a \textit{Lam}.
  1090 
  1091 A reasonable property to expect of substitution is that it should leave closed
  1092 terms unchanged. Alas, even this simple property does not hold:
  1093 
  1094 \pre
  1095 \textbf{lemma}~``$\lnot\,\textit{loose}~t~0 \,\Longrightarrow\, \textit{subst}~\sigma~t = t$'' \\
  1096 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
  1097 \slshape
  1098 Trying 8 scopes: \nopagebreak \\
  1099 \hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 1; \\
  1100 \hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 2; \\
  1101 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
  1102 \hbox{}\qquad \textit{card~nat}~= 8, \textit{card tm}~= 8, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 8. \\[2\smallskipamount]
  1103 Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6,
  1104 and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm}$''~= 6: \\[2\smallskipamount]
  1105 \hbox{}\qquad Free variables: \nopagebreak \\
  1106 \hbox{}\qquad\qquad $\sigma = \undef(\!\begin{aligned}[t]
  1107 & 0 := \textit{Var}~0,\>
  1108   1 := \textit{Var}~0,\>
  1109   2 := \textit{Var}~0, \\[-2pt]
  1110 & 3 := \textit{Var}~0,\>
  1111   4 := \textit{Var}~0,\>
  1112   5 := \textit{Var}~0)\end{aligned}$ \\
  1113 \hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount]
  1114 Total time: $4679$ ms.
  1115 \postw
  1116 
  1117 Using \textit{eval}, we find out that $\textit{subst}~\sigma~t =
  1118 \textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional
  1119 $\lambda$-term notation, $t$~is
  1120 $\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is $\lambda x\, y.\> y$.
  1121 The bug is in \textit{subst}: The $\textit{lift}~(\sigma~m)~1$ call should be
  1122 replaced with $\textit{lift}~(\sigma~m)~0$.
  1123 
  1124 An interesting aspect of Nitpick's verbose output is that it assigned inceasing
  1125 cardinalities from 1 to 8 to the type $\textit{nat} \Rightarrow \textit{tm}$.
  1126 For the formula of interest, knowing 6 values of that type was enough to find
  1127 the counterexample. Without boxing, $46\,656$ ($= 6^6$) values must be
  1128 considered, a hopeless undertaking:
  1129 
  1130 \prew
  1131 \textbf{nitpick} [\textit{dont\_box}] \\[2\smallskipamount]
  1132 {\slshape Nitpick ran out of time after checking 4 of 8 scopes.}
  1133 \postw
  1134 
  1135 {\looseness=-1
  1136 Boxing can be enabled or disabled globally or on a per-type basis using the
  1137 \textit{box} option. Moreover, setting the cardinality of a function or
  1138 product type implicitly enables boxing for that type. Nitpick usually performs
  1139 reasonable choices about which types should be boxed, but option tweaking
  1140 sometimes helps.
  1141 
  1142 }
  1143 
  1144 \subsection{Scope Monotonicity}
  1145 \label{scope-monotonicity}
  1146 
  1147 The \textit{card} option (together with \textit{iter}, \textit{bisim\_depth},
  1148 and \textit{max}) controls which scopes are actually tested. In general, to
  1149 exhaust all models below a certain cardinality bound, the number of scopes that
  1150 Nitpick must consider increases exponentially with the number of type variables
  1151 (and \textbf{typedecl}'d types) occurring in the formula. Given the default
  1152 cardinality specification of 1--8, no fewer than $8^4 = 4096$ scopes must be
  1153 considered for a formula involving $'a$, $'b$, $'c$, and $'d$.
  1154 
  1155 Fortunately, many formulas exhibit a property called \textsl{scope
  1156 monotonicity}, meaning that if the formula is falsifiable for a given scope,
  1157 it is also falsifiable for all larger scopes \cite[p.~165]{jackson-2006}.
  1158 
  1159 Consider the formula
  1160 
  1161 \prew
  1162 \textbf{lemma}~``$\textit{length~xs} = \textit{length~ys} \,\Longrightarrow\, \textit{rev}~(\textit{zip~xs~ys}) = \textit{zip~xs}~(\textit{rev~ys})$''
  1163 \postw
  1164 
  1165 where \textit{xs} is of type $'a~\textit{list}$ and \textit{ys} is of type
  1166 $'b~\textit{list}$. A priori, Nitpick would need to consider 512 scopes to
  1167 exhaust the specification \textit{card}~= 1--8. However, our intuition tells us
  1168 that any counterexample found with a small scope would still be a counterexample
  1169 in a larger scope---by simply ignoring the fresh $'a$ and $'b$ values provided
  1170 by the larger scope. Nitpick comes to the same conclusion after a careful
  1171 inspection of the formula and the relevant definitions:
  1172 
  1173 \prew
  1174 \textbf{nitpick}~[\textit{verbose}] \\[2\smallskipamount]
  1175 \slshape
  1176 The types ``\kern1pt$'a$'' and ``\kern1pt$'b$'' passed the monotonicity test.
  1177 Nitpick might be able to skip some scopes.
  1178  \\[2\smallskipamount]
  1179 Trying 8 scopes: \\
  1180 \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1,
  1181 \textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$
  1182 \textit{list}''~= 1, \\
  1183 \hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 1, and
  1184 \textit{card} ``\kern1pt$'b$ \textit{list}''~= 1. \\
  1185 \hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2,
  1186 \textit{card} \textit{nat}~= 2, \textit{card} ``$('a \times {'}b)$
  1187 \textit{list}''~= 2, \\
  1188 \hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 2, and
  1189 \textit{card} ``\kern1pt$'b$ \textit{list}''~= 2. \\
  1190 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
  1191 \hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} $'b$~= 8,
  1192 \textit{card} \textit{nat}~= 8, \textit{card} ``$('a \times {'}b)$
  1193 \textit{list}''~= 8, \\
  1194 \hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 8, and
  1195 \textit{card} ``\kern1pt$'b$ \textit{list}''~= 8.
  1196 \\[2\smallskipamount]
  1197 Nitpick found a counterexample for
  1198 \textit{card} $'a$~= 5, \textit{card} $'b$~= 5,
  1199 \textit{card} \textit{nat}~= 5, \textit{card} ``$('a \times {'}b)$
  1200 \textit{list}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list}''~= 5, and
  1201 \textit{card} ``\kern1pt$'b$ \textit{list}''~= 5:
  1202 \\[2\smallskipamount]
  1203 \hbox{}\qquad Free variables: \nopagebreak \\
  1204 \hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\
  1205 \hbox{}\qquad\qquad $\textit{ys} = [b_1, b_1]$ \\[2\smallskipamount]
  1206 Total time: 1636 ms.
  1207 \postw
  1208 
  1209 In theory, it should be sufficient to test a single scope:
  1210 
  1211 \prew
  1212 \textbf{nitpick}~[\textit{card}~= 8]
  1213 \postw
  1214 
  1215 However, this is often less efficient in practice and may lead to overly complex
  1216 counterexamples.
  1217 
  1218 If the monotonicity check fails but we believe that the formula is monotonic (or
  1219 we don't mind missing some counterexamples), we can pass the
  1220 \textit{mono} option. To convince yourself that this option is risky,
  1221 simply consider this example from \S\ref{skolemization}:
  1222 
  1223 \prew
  1224 \textbf{lemma} ``$\exists g.\; \forall x\Colon 'b.~g~(f~x) = x
  1225  \,\Longrightarrow\, \forall y\Colon {'}a.\; \exists x.~y = f~x$'' \\
  1226 \textbf{nitpick} [\textit{mono}] \\[2\smallskipamount]
  1227 {\slshape Nitpick found no counterexample.} \\[2\smallskipamount]
  1228 \textbf{nitpick} \\[2\smallskipamount]
  1229 \slshape
  1230 Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\
  1231 \hbox{}\qquad $\vdots$
  1232 \postw
  1233 
  1234 (It turns out the formula holds if and only if $\textit{card}~'a \le
  1235 \textit{card}~'b$.) Although this is rarely advisable, the automatic
  1236 monotonicity checks can be disabled by passing \textit{non\_mono}
  1237 (\S\ref{optimizations}).
  1238 
  1239 As insinuated in \S\ref{natural-numbers-and-integers} and
  1240 \S\ref{inductive-datatypes}, \textit{nat}, \textit{int}, and inductive datatypes
  1241 are normally monotonic and treated as such. The same is true for record types,
  1242 \textit{rat}, \textit{real}, and some \textbf{typedef}'d types. Thus, given the
  1243 cardinality specification 1--8, a formula involving \textit{nat}, \textit{int},
  1244 \textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
  1245 consider only 8~scopes instead of $32\,768$.
  1246 
  1247 \subsection{Inductive Properties}
  1248 \label{inductive-properties}
  1249 
  1250 Inductive properties are a particular pain to prove, because the failure to
  1251 establish an induction step can mean several things:
  1252 %
  1253 \begin{enumerate}
  1254 \item The property is invalid.
  1255 \item The property is valid but is too weak to support the induction step.
  1256 \item The property is valid and strong enough; it's just that we haven't found
  1257 the proof yet.
  1258 \end{enumerate}
  1259 %
  1260 Depending on which scenario applies, we would take the appropriate course of
  1261 action:
  1262 %
  1263 \begin{enumerate}
  1264 \item Repair the statement of the property so that it becomes valid.
  1265 \item Generalize the property and/or prove auxiliary properties.
  1266 \item Work harder on a proof.
  1267 \end{enumerate}
  1268 %
  1269 How can we distinguish between the three scenarios? Nitpick's normal mode of
  1270 operation can often detect scenario 1, and Isabelle's automatic tactics help with
  1271 scenario 3. Using appropriate techniques, it is also often possible to use
  1272 Nitpick to identify scenario 2. Consider the following transition system,
  1273 in which natural numbers represent states:
  1274 
  1275 \prew
  1276 \textbf{inductive\_set}~\textit{reach}~\textbf{where} \\
  1277 ``$(4\Colon\textit{nat}) \in \textit{reach\/}$'' $\mid$ \\
  1278 ``$\lbrakk n < 4;\> n \in \textit{reach\/}\rbrakk \,\Longrightarrow\, 3 * n + 1 \in \textit{reach\/}$'' $\mid$ \\
  1279 ``$n \in \textit{reach} \,\Longrightarrow n + 2 \in \textit{reach\/}$''
  1280 \postw
  1281 
  1282 We will try to prove that only even numbers are reachable:
  1283 
  1284 \prew
  1285 \textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n$''
  1286 \postw
  1287 
  1288 Does this property hold? Nitpick cannot find a counterexample within 30 seconds,
  1289 so let's attempt a proof by induction:
  1290 
  1291 \prew
  1292 \textbf{apply}~(\textit{induct~set}{:}~\textit{reach\/}) \\
  1293 \textbf{apply}~\textit{auto}
  1294 \postw
  1295 
  1296 This leaves us in the following proof state:
  1297 
  1298 \prew
  1299 {\slshape goal (2 subgoals): \\
  1300 \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)$ \\
  1301 \phantom{0}2. ${\bigwedge}n.\;\, \lbrakk n \in \textit{reach\/};\, 2~\textsl{dvd}~n\rbrakk \,\Longrightarrow\, 2~\textsl{dvd}~\textit{Suc}~(\textit{Suc}~n)$
  1302 }
  1303 \postw
  1304 
  1305 If we run Nitpick on the first subgoal, it still won't find any
  1306 counterexample; and yet, \textit{auto} fails to go further, and \textit{arith}
  1307 is helpless. However, notice the $n \in \textit{reach}$ assumption, which
  1308 strengthens the induction hypothesis but is not immediately usable in the proof.
  1309 If we remove it and invoke Nitpick, this time we get a counterexample:
  1310 
  1311 \prew
  1312 \textbf{apply}~(\textit{thin\_tac}~``$n \in \textit{reach\/}$'') \\
  1313 \textbf{nitpick} \\[2\smallskipamount]
  1314 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
  1315 \hbox{}\qquad Skolem constant: \nopagebreak \\
  1316 \hbox{}\qquad\qquad $n = 0$
  1317 \postw
  1318 
  1319 Indeed, 0 < 4, 2 divides 0, but 2 does not divide 1. We can use this information
  1320 to strength the lemma:
  1321 
  1322 \prew
  1323 \textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \not= 0$''
  1324 \postw
  1325 
  1326 Unfortunately, the proof by induction still gets stuck, except that Nitpick now
  1327 finds the counterexample $n = 2$. We generalize the lemma further to
  1328 
  1329 \prew
  1330 \textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \ge 4$''
  1331 \postw
  1332 
  1333 and this time \textit{arith} can finish off the subgoals.
  1334 
  1335 A similar technique can be employed for structural induction. The
  1336 following mini formalization of full binary trees will serve as illustration:
  1337 
  1338 \prew
  1339 \textbf{datatype} $\kern1pt'a$~\textit{bin\_tree} = $\textit{Leaf}~{\kern1pt'a}$ $\mid$ $\textit{Branch}$ ``\kern1pt$'a$ \textit{bin\_tree}'' ``\kern1pt$'a$ \textit{bin\_tree}'' \\[2\smallskipamount]
  1340 \textbf{primrec}~\textit{labels}~\textbf{where} \\
  1341 ``$\textit{labels}~(\textit{Leaf}~a) = \{a\}$'' $\mid$ \\
  1342 ``$\textit{labels}~(\textit{Branch}~t~u) = \textit{labels}~t \mathrel{\cup} \textit{labels}~u$'' \\[2\smallskipamount]
  1343 \textbf{primrec}~\textit{swap}~\textbf{where} \\
  1344 ``$\textit{swap}~(\textit{Leaf}~c)~a~b =$ \\
  1345 \phantom{``}$(\textrm{if}~c = a~\textrm{then}~\textit{Leaf}~b~\textrm{else~if}~c = b~\textrm{then}~\textit{Leaf}~a~\textrm{else}~\textit{Leaf}~c)$'' $\mid$ \\
  1346 ``$\textit{swap}~(\textit{Branch}~t~u)~a~b = \textit{Branch}~(\textit{swap}~t~a~b)~(\textit{swap}~u~a~b)$''
  1347 \postw
  1348 
  1349 The \textit{labels} function returns the set of labels occurring on leaves of a
  1350 tree, and \textit{swap} exchanges two labels. Intuitively, if two distinct
  1351 labels $a$ and $b$ occur in a tree $t$, they should also occur in the tree
  1352 obtained by swapping $a$ and $b$:
  1353 
  1354 \prew
  1355 \textbf{lemma} $``\{a, b\} \subseteq \textit{labels}~t \,\Longrightarrow\, \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
  1356 \postw
  1357 
  1358 Nitpick can't find any counterexample, so we proceed with induction
  1359 (this time favoring a more structured style):
  1360 
  1361 \prew
  1362 \textbf{proof}~(\textit{induct}~$t$) \\
  1363 \hbox{}\quad \textbf{case}~\textit{Leaf}~\textbf{thus}~\textit{?case}~\textbf{by}~\textit{simp} \\
  1364 \textbf{next} \\
  1365 \hbox{}\quad \textbf{case}~$(\textit{Branch}~t~u)$~\textbf{thus} \textit{?case}
  1366 \postw
  1367 
  1368 Nitpick can't find any counterexample at this point either, but it makes the
  1369 following suggestion:
  1370 
  1371 \prew
  1372 \slshape
  1373 Hint: To check that the induction hypothesis is general enough, try this command:
  1374 \textbf{nitpick}~[\textit{non\_std}, \textit{show\_all}].
  1375 \postw
  1376 
  1377 If we follow the hint, we get a ``nonstandard'' counterexample for the step:
  1378 
  1379 \prew
  1380 \slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 3: \\[2\smallskipamount]
  1381 \hbox{}\qquad Free variables: \nopagebreak \\
  1382 \hbox{}\qquad\qquad $a = a_1$ \\
  1383 \hbox{}\qquad\qquad $b = a_2$ \\
  1384 \hbox{}\qquad\qquad $t = \xi_1$ \\
  1385 \hbox{}\qquad\qquad $u = \xi_2$ \\
  1386 \hbox{}\qquad Datatype: \nopagebreak \\
  1387 \hbox{}\qquad\qquad $\alpha~\textit{btree} = \{\xi_1 \mathbin{=} \textit{Branch}~\xi_1~\xi_1,\> \xi_2 \mathbin{=} \textit{Branch}~\xi_2~\xi_2,\> \textit{Branch}~\xi_1~\xi_2\}$ \\
  1388 \hbox{}\qquad {\slshape Constants:} \nopagebreak \\
  1389 \hbox{}\qquad\qquad $\textit{labels} = \undef
  1390     (\!\begin{aligned}[t]%
  1391     & \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[-2pt]
  1392     & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\
  1393 \hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
  1394     (\!\begin{aligned}[t]%
  1395     & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
  1396     & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
  1397 The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
  1398 even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
  1399 \postw
  1400 
  1401 Reading the Nitpick manual is a most excellent idea.
  1402 But what's going on? The \textit{non\_std} option told the tool to look for
  1403 nonstandard models of binary trees, which means that new ``nonstandard'' trees
  1404 $\xi_1, \xi_2, \ldots$, are now allowed in addition to the standard trees
  1405 generated by the \textit{Leaf} and \textit{Branch} constructors.%
  1406 \footnote{Notice the similarity between allowing nonstandard trees here and
  1407 allowing unreachable states in the preceding example (by removing the ``$n \in
  1408 \textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
  1409 set of objects over which the induction is performed while doing the step
  1410 in order to test the induction hypothesis's strength.}
  1411 Unlike standard trees, these new trees contain cycles. We will see later that
  1412 every property of acyclic trees that can be proved without using induction also
  1413 holds for cyclic trees. Hence,
  1414 %
  1415 \begin{quote}
  1416 \textsl{If the induction
  1417 hypothesis is strong enough, the induction step will hold even for nonstandard
  1418 objects, and Nitpick won't find any nonstandard counterexample.}
  1419 \end{quote}
  1420 %
  1421 But here the tool find some nonstandard trees $t = \xi_1$
  1422 and $u = \xi_2$ such that $a \notin \textit{labels}~t$, $b \in
  1423 \textit{labels}~t$, $a \in \textit{labels}~u$, and $b \notin \textit{labels}~u$.
  1424 Because neither tree contains both $a$ and $b$, the induction hypothesis tells
  1425 us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
  1426 and as a result we know nothing about the labels of the tree
  1427 $\textit{swap}~(\textit{Branch}~t~u)~a~b$, which by definition equals
  1428 $\textit{Branch}$ $(\textit{swap}~t~a~b)$ $(\textit{swap}~u~a~b)$, whose
  1429 labels are $\textit{labels}$ $(\textit{swap}~t~a~b) \mathrel{\cup}
  1430 \textit{labels}$ $(\textit{swap}~u~a~b)$.
  1431 
  1432 The solution is to ensure that we always know what the labels of the subtrees
  1433 are in the inductive step, by covering the cases where $a$ and/or~$b$ is not in
  1434 $t$ in the statement of the lemma:
  1435 
  1436 \prew
  1437 \textbf{lemma} ``$\textit{labels}~(\textit{swap}~t~a~b) = {}$ \\
  1438 \phantom{\textbf{lemma} ``}$(\textrm{if}~a \in \textit{labels}~t~\textrm{then}$ \nopagebreak \\
  1439 \phantom{\textbf{lemma} ``(\quad}$\textrm{if}~b \in \textit{labels}~t~\textrm{then}~\textit{labels}~t~\textrm{else}~(\textit{labels}~t - \{a\}) \mathrel{\cup} \{b\}$ \\
  1440 \phantom{\textbf{lemma} ``(}$\textrm{else}$ \\
  1441 \phantom{\textbf{lemma} ``(\quad}$\textrm{if}~b \in \textit{labels}~t~\textrm{then}~(\textit{labels}~t - \{b\}) \mathrel{\cup} \{a\}~\textrm{else}~\textit{labels}~t)$''
  1442 \postw
  1443 
  1444 This time, Nitpick won't find any nonstandard counterexample, and we can perform
  1445 the induction step using \textit{auto}.
  1446 
  1447 \section{Case Studies}
  1448 \label{case-studies}
  1449 
  1450 As a didactic device, the previous section focused mostly on toy formulas whose
  1451 validity can easily be assessed just by looking at the formula. We will now
  1452 review two somewhat more realistic case studies that are within Nitpick's
  1453 reach:\ a context-free grammar modeled by mutually inductive sets and a
  1454 functional implementation of AA trees. The results presented in this
  1455 section were produced with the following settings:
  1456 
  1457 \prew
  1458 \textbf{nitpick\_params} [\textit{max\_potential}~= 0,\, \textit{max\_threads} = 2]
  1459 \postw
  1460 
  1461 \subsection{A Context-Free Grammar}
  1462 \label{a-context-free-grammar}
  1463 
  1464 Our first case study is taken from section 7.4 in the Isabelle tutorial
  1465 \cite{isa-tutorial}. The following grammar, originally due to Hopcroft and
  1466 Ullman, produces all strings with an equal number of $a$'s and $b$'s:
  1467 
  1468 \prew
  1469 \begin{tabular}{@{}r@{$\;\,$}c@{$\;\,$}l@{}}
  1470 $S$ & $::=$ & $\epsilon \mid bA \mid aB$ \\
  1471 $A$ & $::=$ & $aS \mid bAA$ \\
  1472 $B$ & $::=$ & $bS \mid aBB$
  1473 \end{tabular}
  1474 \postw
  1475 
  1476 The intuition behind the grammar is that $A$ generates all string with one more
  1477 $a$ than $b$'s and $B$ generates all strings with one more $b$ than $a$'s.
  1478 
  1479 The alphabet consists exclusively of $a$'s and $b$'s:
  1480 
  1481 \prew
  1482 \textbf{datatype} \textit{alphabet}~= $a$ $\mid$ $b$
  1483 \postw
  1484 
  1485 Strings over the alphabet are represented by \textit{alphabet list}s.
  1486 Nonterminals in the grammar become sets of strings. The production rules
  1487 presented above can be expressed as a mutually inductive definition:
  1488 
  1489 \prew
  1490 \textbf{inductive\_set} $S$ \textbf{and} $A$ \textbf{and} $B$ \textbf{where} \\
  1491 \textit{R1}:\kern.4em ``$[] \in S$'' $\,\mid$ \\
  1492 \textit{R2}:\kern.4em ``$w \in A\,\Longrightarrow\, b \mathbin{\#} w \in S$'' $\,\mid$ \\
  1493 \textit{R3}:\kern.4em ``$w \in B\,\Longrightarrow\, a \mathbin{\#} w \in S$'' $\,\mid$ \\
  1494 \textit{R4}:\kern.4em ``$w \in S\,\Longrightarrow\, a \mathbin{\#} w \in A$'' $\,\mid$ \\
  1495 \textit{R5}:\kern.4em ``$w \in S\,\Longrightarrow\, b \mathbin{\#} w \in S$'' $\,\mid$ \\
  1496 \textit{R6}:\kern.4em ``$\lbrakk v \in B;\> v \in B\rbrakk \,\Longrightarrow\, a \mathbin{\#} v \mathbin{@} w \in B$''
  1497 \postw
  1498 
  1499 The conversion of the grammar into the inductive definition was done manually by
  1500 Joe Blow, an underpaid undergraduate student. As a result, some errors might
  1501 have sneaked in.
  1502 
  1503 Debugging faulty specifications is at the heart of Nitpick's \textsl{raison
  1504 d'\^etre}. A good approach is to state desirable properties of the specification
  1505 (here, that $S$ is exactly the set of strings over $\{a, b\}$ with as many $a$'s
  1506 as $b$'s) and check them with Nitpick. If the properties are correctly stated,
  1507 counterexamples will point to bugs in the specification. For our grammar
  1508 example, we will proceed in two steps, separating the soundness and the
  1509 completeness of the set $S$. First, soundness:
  1510 
  1511 \prew
  1512 \textbf{theorem}~\textit{S\_sound}: \\
  1513 ``$w \in S \longrightarrow \textit{length}~[x\mathbin{\leftarrow} w.\; x = a] =
  1514   \textit{length}~[x\mathbin{\leftarrow} w.\; x = b]$'' \\
  1515 \textbf{nitpick} \\[2\smallskipamount]
  1516 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
  1517 \hbox{}\qquad Free variable: \nopagebreak \\
  1518 \hbox{}\qquad\qquad $w = [b]$
  1519 \postw
  1520 
  1521 It would seem that $[b] \in S$. How could this be? An inspection of the
  1522 introduction rules reveals that the only rule with a right-hand side of the form
  1523 $b \mathbin{\#} {\ldots} \in S$ that could have introduced $[b]$ into $S$ is
  1524 \textit{R5}:
  1525 
  1526 \prew
  1527 ``$w \in S\,\Longrightarrow\, b \mathbin{\#} w \in S$''
  1528 \postw
  1529 
  1530 On closer inspection, we can see that this rule is wrong. To match the
  1531 production $B ::= bS$, the second $S$ should be a $B$. We fix the typo and try
  1532 again:
  1533 
  1534 \prew
  1535 \textbf{nitpick} \\[2\smallskipamount]
  1536 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
  1537 \hbox{}\qquad Free variable: \nopagebreak \\
  1538 \hbox{}\qquad\qquad $w = [a, a, b]$
  1539 \postw
  1540 
  1541 Some detective work is necessary to find out what went wrong here. To get $[a,
  1542 a, b] \in S$, we need $[a, b] \in B$ by \textit{R3}, which in turn can only come
  1543 from \textit{R6}:
  1544 
  1545 \prew
  1546 ``$\lbrakk v \in B;\> v \in B\rbrakk \,\Longrightarrow\, a \mathbin{\#} v \mathbin{@} w \in B$''
  1547 \postw
  1548 
  1549 Now, this formula must be wrong: The same assumption occurs twice, and the
  1550 variable $w$ is unconstrained. Clearly, one of the two occurrences of $v$ in
  1551 the assumptions should have been a $w$.
  1552 
  1553 With the correction made, we don't get any counterexample from Nitpick. Let's
  1554 move on and check completeness:
  1555 
  1556 \prew
  1557 \textbf{theorem}~\textit{S\_complete}: \\
  1558 ``$\textit{length}~[x\mathbin{\leftarrow} w.\; x = a] =
  1559    \textit{length}~[x\mathbin{\leftarrow} w.\; x = b]
  1560   \longrightarrow w \in S$'' \\
  1561 \textbf{nitpick} \\[2\smallskipamount]
  1562 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
  1563 \hbox{}\qquad Free variable: \nopagebreak \\
  1564 \hbox{}\qquad\qquad $w = [b, b, a, a]$
  1565 \postw
  1566 
  1567 Apparently, $[b, b, a, a] \notin S$, even though it has the same numbers of
  1568 $a$'s and $b$'s. But since our inductive definition passed the soundness check,
  1569 the introduction rules we have are probably correct. Perhaps we simply lack an
  1570 introduction rule. Comparing the grammar with the inductive definition, our
  1571 suspicion is confirmed: Joe Blow simply forgot the production $A ::= bAA$,
  1572 without which the grammar cannot generate two or more $b$'s in a row. So we add
  1573 the rule
  1574 
  1575 \prew
  1576 ``$\lbrakk v \in A;\> w \in A\rbrakk \,\Longrightarrow\, b \mathbin{\#} v \mathbin{@} w \in A$''
  1577 \postw
  1578 
  1579 With this last change, we don't get any counterexamples from Nitpick for either
  1580 soundness or completeness. We can even generalize our result to cover $A$ and
  1581 $B$ as well:
  1582 
  1583 \prew
  1584 \textbf{theorem} \textit{S\_A\_B\_sound\_and\_complete}: \\
  1585 ``$w \in S \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b]$'' \\
  1586 ``$w \in A \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] + 1$'' \\
  1587 ``$w \in B \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] + 1$'' \\
  1588 \textbf{nitpick} \\[2\smallskipamount]
  1589 \slshape Nitpick found no counterexample.
  1590 \postw
  1591 
  1592 \subsection{AA Trees}
  1593 \label{aa-trees}
  1594 
  1595 AA trees are a kind of balanced trees discovered by Arne Andersson that provide
  1596 similar performance to red-black trees, but with a simpler implementation
  1597 \cite{andersson-1993}. They can be used to store sets of elements equipped with
  1598 a total order $<$. We start by defining the datatype and some basic extractor
  1599 functions:
  1600 
  1601 \prew
  1602 \textbf{datatype} $'a$~\textit{aa\_tree} = \\
  1603 \hbox{}\quad $\Lambda$ $\mid$ $N$ ``\kern1pt$'a\Colon \textit{linorder}$'' \textit{nat} ``\kern1pt$'a$ \textit{aa\_tree}'' ``\kern1pt$'a$ \textit{aa\_tree}''  \\[2\smallskipamount]
  1604 \textbf{primrec} \textit{data} \textbf{where} \\
  1605 ``$\textit{data}~\Lambda = \undef$'' $\,\mid$ \\
  1606 ``$\textit{data}~(N~x~\_~\_~\_) = x$'' \\[2\smallskipamount]
  1607 \textbf{primrec} \textit{dataset} \textbf{where} \\
  1608 ``$\textit{dataset}~\Lambda = \{\}$'' $\,\mid$ \\
  1609 ``$\textit{dataset}~(N~x~\_~t~u) = \{x\} \cup \textit{dataset}~t \mathrel{\cup} \textit{dataset}~u$'' \\[2\smallskipamount]
  1610 \textbf{primrec} \textit{level} \textbf{where} \\
  1611 ``$\textit{level}~\Lambda = 0$'' $\,\mid$ \\
  1612 ``$\textit{level}~(N~\_~k~\_~\_) = k$'' \\[2\smallskipamount]
  1613 \textbf{primrec} \textit{left} \textbf{where} \\
  1614 ``$\textit{left}~\Lambda = \Lambda$'' $\,\mid$ \\
  1615 ``$\textit{left}~(N~\_~\_~t~\_) = t$'' \\[2\smallskipamount]
  1616 \textbf{primrec} \textit{right} \textbf{where} \\
  1617 ``$\textit{right}~\Lambda = \Lambda$'' $\,\mid$ \\
  1618 ``$\textit{right}~(N~\_~\_~\_~u) = u$''
  1619 \postw
  1620 
  1621 The wellformedness criterion for AA trees is fairly complex. Wikipedia states it
  1622 as follows \cite{wikipedia-2009-aa-trees}:
  1623 
  1624 \kern.2\parskip %% TYPESETTING
  1625 
  1626 \pre
  1627 Each node has a level field, and the following invariants must remain true for
  1628 the tree to be valid:
  1629 
  1630 \raggedright
  1631 
  1632 \kern-.4\parskip %% TYPESETTING
  1633 
  1634 \begin{enum}
  1635 \item[]
  1636 \begin{enum}
  1637 \item[1.] The level of a leaf node is one.
  1638 \item[2.] The level of a left child is strictly less than that of its parent.
  1639 \item[3.] The level of a right child is less than or equal to that of its parent.
  1640 \item[4.] The level of a right grandchild is strictly less than that of its grandparent.
  1641 \item[5.] Every node of level greater than one must have two children.
  1642 \end{enum}
  1643 \end{enum}
  1644 \post
  1645 
  1646 \kern.4\parskip %% TYPESETTING
  1647 
  1648 The \textit{wf} predicate formalizes this description:
  1649 
  1650 \prew
  1651 \textbf{primrec} \textit{wf} \textbf{where} \\
  1652 ``$\textit{wf}~\Lambda = \textit{True}$'' $\,\mid$ \\
  1653 ``$\textit{wf}~(N~\_~k~t~u) =$ \\
  1654 \phantom{``}$(\textrm{if}~t = \Lambda~\textrm{then}$ \\
  1655 \phantom{``$(\quad$}$k = 1 \mathrel{\land} (u = \Lambda \mathrel{\lor} (\textit{level}~u = 1 \mathrel{\land} \textit{left}~u = \Lambda \mathrel{\land} \textit{right}~u = \Lambda))$ \\
  1656 \phantom{``$($}$\textrm{else}$ \\
  1657 \hbox{}\phantom{``$(\quad$}$\textit{wf}~t \mathrel{\land} \textit{wf}~u
  1658 \mathrel{\land} u \not= \Lambda \mathrel{\land} \textit{level}~t < k
  1659 \mathrel{\land} \textit{level}~u \le k$ \\
  1660 \hbox{}\phantom{``$(\quad$}${\land}\; \textit{level}~(\textit{right}~u) < k)$''
  1661 \postw
  1662 
  1663 Rebalancing the tree upon insertion and removal of elements is performed by two
  1664 auxiliary functions called \textit{skew} and \textit{split}, defined below:
  1665 
  1666 \prew
  1667 \textbf{primrec} \textit{skew} \textbf{where} \\
  1668 ``$\textit{skew}~\Lambda = \Lambda$'' $\,\mid$ \\
  1669 ``$\textit{skew}~(N~x~k~t~u) = {}$ \\
  1670 \phantom{``}$(\textrm{if}~t \not= \Lambda \mathrel{\land} k =
  1671 \textit{level}~t~\textrm{then}$ \\
  1672 \phantom{``(\quad}$N~(\textit{data}~t)~k~(\textit{left}~t)~(N~x~k~
  1673 (\textit{right}~t)~u)$ \\
  1674 \phantom{``(}$\textrm{else}$ \\
  1675 \phantom{``(\quad}$N~x~k~t~u)$''
  1676 \postw
  1677 
  1678 \prew
  1679 \textbf{primrec} \textit{split} \textbf{where} \\
  1680 ``$\textit{split}~\Lambda = \Lambda$'' $\,\mid$ \\
  1681 ``$\textit{split}~(N~x~k~t~u) = {}$ \\
  1682 \phantom{``}$(\textrm{if}~u \not= \Lambda \mathrel{\land} k =
  1683 \textit{level}~(\textit{right}~u)~\textrm{then}$ \\
  1684 \phantom{``(\quad}$N~(\textit{data}~u)~(\textit{Suc}~k)~
  1685 (N~x~k~t~(\textit{left}~u))~(\textit{right}~u)$ \\
  1686 \phantom{``(}$\textrm{else}$ \\
  1687 \phantom{``(\quad}$N~x~k~t~u)$''
  1688 \postw
  1689 
  1690 Performing a \textit{skew} or a \textit{split} should have no impact on the set
  1691 of elements stored in the tree:
  1692 
  1693 \prew
  1694 \textbf{theorem}~\textit{dataset\_skew\_split}:\\
  1695 ``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
  1696 ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
  1697 \textbf{nitpick} \\[2\smallskipamount]
  1698 {\slshape Nitpick found no counterexample.}
  1699 \postw
  1700 
  1701 Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
  1702 should not alter the tree:
  1703 
  1704 \prew
  1705 \textbf{theorem}~\textit{wf\_skew\_split}:\\
  1706 ``$\textit{wf}~t\,\Longrightarrow\, \textit{skew}~t = t$'' \\
  1707 ``$\textit{wf}~t\,\Longrightarrow\, \textit{split}~t = t$'' \\
  1708 \textbf{nitpick} \\[2\smallskipamount]
  1709 {\slshape Nitpick found no counterexample.}
  1710 \postw
  1711 
  1712 Insertion is implemented recursively. It preserves the sort order:
  1713 
  1714 \prew
  1715 \textbf{primrec}~\textit{insort} \textbf{where} \\
  1716 ``$\textit{insort}~\Lambda~x = N~x~1~\Lambda~\Lambda$'' $\,\mid$ \\
  1717 ``$\textit{insort}~(N~y~k~t~u)~x =$ \\
  1718 \phantom{``}$({*}~(\textit{split} \circ \textit{skew})~{*})~(N~y~k~(\textrm{if}~x < y~\textrm{then}~\textit{insort}~t~x~\textrm{else}~t)$ \\
  1719 \phantom{``$({*}~(\textit{split} \circ \textit{skew})~{*})~(N~y~k~$}$(\textrm{if}~x > y~\textrm{then}~\textit{insort}~u~x~\textrm{else}~u))$''
  1720 \postw
  1721 
  1722 Notice that we deliberately commented out the application of \textit{skew} and
  1723 \textit{split}. Let's see if this causes any problems:
  1724 
  1725 \prew
  1726 \textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
  1727 \textbf{nitpick} \\[2\smallskipamount]
  1728 \slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
  1729 \hbox{}\qquad Free variables: \nopagebreak \\
  1730 \hbox{}\qquad\qquad $t = N~a_1~1~\Lambda~\Lambda$ \\
  1731 \hbox{}\qquad\qquad $x = a_2$
  1732 \postw
  1733 
  1734 It's hard to see why this is a counterexample. To improve readability, we will
  1735 restrict the theorem to \textit{nat}, so that we don't need to look up the value
  1736 of the $\textit{op}~{<}$ constant to find out which element is smaller than the
  1737 other. In addition, we will tell Nitpick to display the value of
  1738 $\textit{insort}~t~x$ using the \textit{eval} option. This gives
  1739 
  1740 \prew
  1741 \textbf{theorem} \textit{wf\_insort\_nat}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\
  1742 \textbf{nitpick} [\textit{eval} = ``$\textit{insort}~t~x$''] \\[2\smallskipamount]
  1743 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
  1744 \hbox{}\qquad Free variables: \nopagebreak \\
  1745 \hbox{}\qquad\qquad $t = N~1~1~\Lambda~\Lambda$ \\
  1746 \hbox{}\qquad\qquad $x = 0$ \\
  1747 \hbox{}\qquad Evaluated term: \\
  1748 \hbox{}\qquad\qquad $\textit{insort}~t~x = N~1~1~(N~0~1~\Lambda~\Lambda)~\Lambda$
  1749 \postw
  1750 
  1751 Nitpick's output reveals that the element $0$ was added as a left child of $1$,
  1752 where both have a level of 1. This violates the second AA tree invariant, which
  1753 states that a left child's level must be less than its parent's. This shouldn't
  1754 come as a surprise, considering that we commented out the tree rebalancing code.
  1755 Reintroducing the code seems to solve the problem:
  1756 
  1757 \prew
  1758 \textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
  1759 \textbf{nitpick} \\[2\smallskipamount]
  1760 {\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
  1761 \postw
  1762 
  1763 Insertion should transform the set of elements represented by the tree in the
  1764 obvious way:
  1765 
  1766 \prew
  1767 \textbf{theorem} \textit{dataset\_insort}:\kern.4em
  1768 ``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
  1769 \textbf{nitpick} \\[2\smallskipamount]
  1770 {\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
  1771 \postw
  1772 
  1773 We could continue like this and sketch a complete theory of AA trees. Once the
  1774 definitions and main theorems are in place and have been thoroughly tested using
  1775 Nitpick, we could start working on the proofs. Developing theories this way
  1776 usually saves time, because faulty theorems and definitions are discovered much
  1777 earlier in the process.
  1778 
  1779 \section{Option Reference}
  1780 \label{option-reference}
  1781 
  1782 \def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
  1783 \def\qty#1{$\left<\textit{#1}\right>$}
  1784 \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
  1785 \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
  1786 \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
  1787 \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
  1788 \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
  1789 \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
  1790 \def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
  1791 \def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
  1792 \def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
  1793 
  1794 Nitpick's behavior can be influenced by various options, which can be specified
  1795 in brackets after the \textbf{nitpick} command. Default values can be set
  1796 using \textbf{nitpick\_\allowbreak params}. For example:
  1797 
  1798 \prew
  1799 \textbf{nitpick\_params} [\textit{verbose}, \,\textit{timeout} = 60$\,s$]
  1800 \postw
  1801 
  1802 The options are categorized as follows:\ mode of operation
  1803 (\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output
  1804 format (\S\ref{output-format}), automatic counterexample checks
  1805 (\S\ref{authentication}), optimizations
  1806 (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
  1807 
  1808 You can instruct Nitpick to run automatically on newly entered theorems by
  1809 enabling the ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof
  1810 General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation})
  1811 and \textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
  1812 \textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
  1813 (\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
  1814 disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
  1815 \textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Counterexample
  1816 Time Limit'' in Proof General's ``Isabelle'' menu. Nitpick's output is also more
  1817 concise.
  1818 
  1819 The number of options can be overwhelming at first glance. Do not let that worry
  1820 you: Nitpick's defaults have been chosen so that it almost always does the right
  1821 thing, and the most important options have been covered in context in
  1822 \S\ref{first-steps}.
  1823 
  1824 The descriptions below refer to the following syntactic quantities:
  1825 
  1826 \begin{enum}
  1827 \item[$\bullet$] \qtybf{string}: A string.
  1828 \item[$\bullet$] \qtybf{bool}: \textit{true} or \textit{false}.
  1829 \item[$\bullet$] \qtybf{bool\_or\_smart}: \textit{true}, \textit{false}, or \textit{smart}.
  1830 \item[$\bullet$] \qtybf{int}: An integer. Negative integers are prefixed with a hyphen.
  1831 \item[$\bullet$] \qtybf{int\_or\_smart}: An integer or \textit{smart}.
  1832 \item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
  1833 of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<midarrow\char`\>}.
  1834 
  1835 \item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
  1836 \item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
  1837 (milliseconds), or the keyword \textit{none} ($\infty$ years).
  1838 \item[$\bullet$] \qtybf{const}: The name of a HOL constant.
  1839 \item[$\bullet$] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
  1840 \item[$\bullet$] \qtybf{term\_list}: A space-separated list of HOL terms (e.g.,
  1841 ``$f~x$''~``$g~y$'').
  1842 \item[$\bullet$] \qtybf{type}: A HOL type.
  1843 \end{enum}
  1844 
  1845 Default values are indicated in square brackets. Boolean options have a negated
  1846 counterpart (e.g., \textit{blocking} vs.\ \textit{no\_blocking}). When setting
  1847 Boolean options, ``= \textit{true}'' may be omitted.
  1848 
  1849 \subsection{Mode of Operation}
  1850 \label{mode-of-operation}
  1851 
  1852 \begin{enum}
  1853 \optrue{blocking}{non\_blocking}
  1854 Specifies whether the \textbf{nitpick} command should operate synchronously.
  1855 The asynchronous (non-blocking) mode lets the user start proving the putative
  1856 theorem while Nitpick looks for a counterexample, but it can also be more
  1857 confusing. For technical reasons, automatic runs currently always block.
  1858 
  1859 \optrue{falsify}{satisfy}
  1860 Specifies whether Nitpick should look for falsifying examples (countermodels) or
  1861 satisfying examples (models). This manual assumes throughout that
  1862 \textit{falsify} is enabled.
  1863 
  1864 \opsmart{user\_axioms}{no\_user\_axioms}
  1865 Specifies whether the user-defined axioms (specified using 
  1866 \textbf{axiomatization} and \textbf{axioms}) should be considered. If the option
  1867 is set to \textit{smart}, Nitpick performs an ad hoc axiom selection based on
  1868 the constants that occur in the formula to falsify. The option is implicitly set
  1869 to \textit{true} for automatic runs.
  1870 
  1871 \textbf{Warning:} If the option is set to \textit{true}, Nitpick might
  1872 nonetheless ignore some polymorphic axioms. Counterexamples generated under
  1873 these conditions are tagged as ``likely genuine.'' The \textit{debug}
  1874 (\S\ref{output-format}) option can be used to find out which axioms were
  1875 considered.
  1876 
  1877 \nopagebreak
  1878 {\small See also \textit{assms} (\S\ref{mode-of-operation}) and \textit{debug}
  1879 (\S\ref{output-format}).}
  1880 
  1881 \optrue{assms}{no\_assms}
  1882 Specifies whether the relevant assumptions in structured proof should be
  1883 considered. The option is implicitly enabled for automatic runs.
  1884 
  1885 \nopagebreak
  1886 {\small See also \textit{user\_axioms} (\S\ref{mode-of-operation}).}
  1887 
  1888 \opfalse{overlord}{no\_overlord}
  1889 Specifies whether Nitpick should put its temporary files in
  1890 \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
  1891 debugging Nitpick but also unsafe if several instances of the tool are run
  1892 simultaneously. The files are identified by the extensions
  1893 \texttt{.kki}, \texttt{.cnf}, \texttt{.out}, and
  1894 \texttt{.err}; you may safely remove them after Nitpick has run.
  1895 
  1896 \nopagebreak
  1897 {\small See also \textit{debug} (\S\ref{output-format}).}
  1898 \end{enum}
  1899 
  1900 \subsection{Scope of Search}
  1901 \label{scope-of-search}
  1902 
  1903 \begin{enum}
  1904 \oparg{card}{type}{int\_seq}
  1905 Specifies the sequence of cardinalities to use for a given type.
  1906 For free types, and often also for \textbf{typedecl}'d types, it usually makes
  1907 sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
  1908 Although function and product types are normally mapped directly to the
  1909 corresponding Kodkod concepts, setting
  1910 the cardinality of such types is also allowed and implicitly enables ``boxing''
  1911 for them, as explained in the description of the \textit{box}~\qty{type}
  1912 and \textit{box} (\S\ref{scope-of-search}) options.
  1913 
  1914 \nopagebreak
  1915 {\small See also \textit{mono} (\S\ref{scope-of-search}).}
  1916 
  1917 \opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
  1918 Specifies the default sequence of cardinalities to use. This can be overridden
  1919 on a per-type basis using the \textit{card}~\qty{type} option described above.
  1920 
  1921 \oparg{max}{const}{int\_seq}
  1922 Specifies the sequence of maximum multiplicities to use for a given
  1923 (co)in\-duc\-tive datatype constructor. A constructor's multiplicity is the
  1924 number of distinct values that it can construct. Nonsensical values (e.g.,
  1925 \textit{max}~[]~$=$~2) are silently repaired. This option is only available for
  1926 datatypes equipped with several constructors.
  1927 
  1928 \opnodefault{max}{int\_seq}
  1929 Specifies the default sequence of maximum multiplicities to use for
  1930 (co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor
  1931 basis using the \textit{max}~\qty{const} option described above.
  1932 
  1933 \opsmart{binary\_ints}{unary\_ints}
  1934 Specifies whether natural numbers and integers should be encoded using a unary
  1935 or binary notation. In unary mode, the cardinality fully specifies the subset
  1936 used to approximate the type. For example:
  1937 %
  1938 $$\hbox{\begin{tabular}{@{}rll@{}}%
  1939 \textit{card nat} = 4 & induces & $\{0,\, 1,\, 2,\, 3\}$ \\
  1940 \textit{card int} = 4 & induces & $\{-1,\, 0,\, +1,\, +2\}$ \\
  1941 \textit{card int} = 5 & induces & $\{-2,\, -1,\, 0,\, +1,\, +2\}.$%
  1942 \end{tabular}}$$
  1943 %
  1944 In general:
  1945 %
  1946 $$\hbox{\begin{tabular}{@{}rll@{}}%
  1947 \textit{card nat} = $K$ & induces & $\{0,\, \ldots,\, K - 1\}$ \\
  1948 \textit{card int} = $K$ & induces & $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor K/2 \rfloor\}.$%
  1949 \end{tabular}}$$
  1950 %
  1951 In binary mode, the cardinality specifies the number of distinct values that can
  1952 be constructed. Each of these value is represented by a bit pattern whose length
  1953 is specified by the \textit{bits} (\S\ref{scope-of-search}) option. By default,
  1954 Nitpick attempts to choose the more appropriate encoding by inspecting the
  1955 formula at hand, preferring the binary notation for problems involving
  1956 multiplicative operators or large constants.
  1957 
  1958 \textbf{Warning:} For technical reasons, Nitpick always reverts to unary for
  1959 problems that refer to the types \textit{rat} or \textit{real} or the constants
  1960 \textit{Suc}, \textit{gcd}, or \textit{lcm}.
  1961 
  1962 {\small See also \textit{bits} (\S\ref{scope-of-search}) and
  1963 \textit{show\_datatypes} (\S\ref{output-format}).}
  1964 
  1965 \opdefault{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$}
  1966 Specifies the number of bits to use to represent natural numbers and integers in
  1967 binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
  1968 
  1969 {\small See also \textit{binary\_ints} (\S\ref{scope-of-search}).}
  1970 
  1971 \opargboolorsmart{wf}{const}{non\_wf}
  1972 Specifies whether the specified (co)in\-duc\-tively defined predicate is
  1973 well-founded. The option can take the following values:
  1974 
  1975 \begin{enum}
  1976 \item[$\bullet$] \textbf{\textit{true}}: Tentatively treat the (co)in\-duc\-tive
  1977 predicate as if it were well-founded. Since this is generally not sound when the
  1978 predicate is not well-founded, the counterexamples are tagged as ``likely
  1979 genuine.''
  1980 
  1981 \item[$\bullet$] \textbf{\textit{false}}: Treat the (co)in\-duc\-tive predicate
  1982 as if it were not well-founded. The predicate is then unrolled as prescribed by
  1983 the \textit{star\_linear\_preds}, \textit{iter}~\qty{const}, and \textit{iter}
  1984 options.
  1985 
  1986 \item[$\bullet$] \textbf{\textit{smart}}: Try to prove that the inductive
  1987 predicate is well-founded using Isabelle's \textit{lexicographic\_order} and
  1988 \textit{size\_change} tactics. If this succeeds (or the predicate occurs with an
  1989 appropriate polarity in the formula to falsify), use an efficient fixed point
  1990 equation as specification of the predicate; otherwise, unroll the predicates
  1991 according to the \textit{iter}~\qty{const} and \textit{iter} options.
  1992 \end{enum}
  1993 
  1994 \nopagebreak
  1995 {\small See also \textit{iter} (\S\ref{scope-of-search}),
  1996 \textit{star\_linear\_preds} (\S\ref{optimizations}), and \textit{tac\_timeout}
  1997 (\S\ref{timeouts}).}
  1998 
  1999 \opsmart{wf}{non\_wf}
  2000 Specifies the default wellfoundedness setting to use. This can be overridden on
  2001 a per-predicate basis using the \textit{wf}~\qty{const} option above.
  2002 
  2003 \oparg{iter}{const}{int\_seq}
  2004 Specifies the sequence of iteration counts to use when unrolling a given
  2005 (co)in\-duc\-tive predicate. By default, unrolling is applied for inductive
  2006 predicates that occur negatively and coinductive predicates that occur
  2007 positively in the formula to falsify and that cannot be proved to be
  2008 well-founded, but this behavior is influenced by the \textit{wf} option. The
  2009 iteration counts are automatically bounded by the cardinality of the predicate's
  2010 domain.
  2011 
  2012 {\small See also \textit{wf} (\S\ref{scope-of-search}) and
  2013 \textit{star\_linear\_preds} (\S\ref{optimizations}).}
  2014 
  2015 \opdefault{iter}{int\_seq}{$\mathbf{1{,}2{,}4{,}8{,}12{,}16{,}24{,}32}$}
  2016 Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive
  2017 predicates. This can be overridden on a per-predicate basis using the
  2018 \textit{iter} \qty{const} option above.
  2019 
  2020 \opdefault{bisim\_depth}{int\_seq}{$\mathbf{7}$}
  2021 Specifies the sequence of iteration counts to use when unrolling the
  2022 bisimilarity predicate generated by Nitpick for coinductive datatypes. A value
  2023 of $-1$ means that no predicate is generated, in which case Nitpick performs an
  2024 after-the-fact check to see if the known coinductive datatype values are
  2025 bidissimilar. If two values are found to be bisimilar, the counterexample is
  2026 tagged as ``likely genuine.'' The iteration counts are automatically bounded by
  2027 the sum of the cardinalities of the coinductive datatypes occurring in the
  2028 formula to falsify.
  2029 
  2030 \opargboolorsmart{box}{type}{dont\_box}
  2031 Specifies whether Nitpick should attempt to wrap (``box'') a given function or
  2032 product type in an isomorphic datatype internally. Boxing is an effective mean
  2033 to reduce the search space and speed up Nitpick, because the isomorphic datatype
  2034 is approximated by a subset of the possible function or pair values;
  2035 like other drastic optimizations, it can also prevent the discovery of
  2036 counterexamples. The option can take the following values:
  2037 
  2038 \begin{enum}
  2039 \item[$\bullet$] \textbf{\textit{true}}: Box the specified type whenever
  2040 practicable.
  2041 \item[$\bullet$] \textbf{\textit{false}}: Never box the type.
  2042 \item[$\bullet$] \textbf{\textit{smart}}: Box the type only in contexts where it
  2043 is likely to help. For example, $n$-tuples where $n > 2$ and arguments to
  2044 higher-order functions are good candidates for boxing.
  2045 \end{enum}
  2046 
  2047 Setting the \textit{card}~\qty{type} option for a function or product type
  2048 implicitly enables boxing for that type.
  2049 
  2050 \nopagebreak
  2051 {\small See also \textit{verbose} (\S\ref{output-format})
  2052 and \textit{debug} (\S\ref{output-format}).}
  2053 
  2054 \opsmart{box}{dont\_box}
  2055 Specifies the default boxing setting to use. This can be overridden on a
  2056 per-type basis using the \textit{box}~\qty{type} option described above.
  2057 
  2058 \opargboolorsmart{mono}{type}{non\_mono}
  2059 Specifies whether the given type should be considered monotonic when
  2060 enumerating scopes. If the option is set to \textit{smart}, Nitpick performs a
  2061 monotonicity check on the type. Setting this option to \textit{true} can reduce
  2062 the number of scopes tried, but it also diminishes the theoretical chance of
  2063 finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}.
  2064 
  2065 \nopagebreak
  2066 {\small See also \textit{card} (\S\ref{scope-of-search}),
  2067 \textit{merge\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
  2068 (\S\ref{output-format}).}
  2069 
  2070 \opsmart{mono}{non\_box}
  2071 Specifies the default monotonicity setting to use. This can be overridden on a
  2072 per-type basis using the \textit{mono}~\qty{type} option described above.
  2073 
  2074 \opfalse{merge\_type\_vars}{dont\_merge\_type\_vars}
  2075 Specifies whether type variables with the same sort constraints should be
  2076 merged. Setting this option to \textit{true} can reduce the number of scopes
  2077 tried and the size of the generated Kodkod formulas, but it also diminishes the
  2078 theoretical chance of finding a counterexample.
  2079 
  2080 {\small See also \textit{mono} (\S\ref{scope-of-search}).}
  2081 
  2082 \opargbool{std}{type}{non\_std}
  2083 Specifies whether the given (recursive) datatype should be given standard
  2084 models. Nonstandard models are unsound but can help debug structural induction
  2085 proofs, as explained in \S\ref{inductive-properties}.
  2086 %This option is not supported for the type \textit{nat}.
  2087 
  2088 \optrue{std}{non\_std}
  2089 Specifies the default standardness to use. This can be overridden on a per-type
  2090 basis using the \textit{std}~\qty{type} option described above.
  2091 \end{enum}
  2092 
  2093 \subsection{Output Format}
  2094 \label{output-format}
  2095 
  2096 \begin{enum}
  2097 \opfalse{verbose}{quiet}
  2098 Specifies whether the \textbf{nitpick} command should explain what it does. This
  2099 option is useful to determine which scopes are tried or which SAT solver is
  2100 used. This option is implicitly disabled for automatic runs.
  2101 
  2102 \opfalse{debug}{no\_debug}
  2103 Specifies whether Nitpick should display additional debugging information beyond
  2104 what \textit{verbose} already displays. Enabling \textit{debug} also enables
  2105 \textit{verbose} and \textit{show\_all} behind the scenes. The \textit{debug}
  2106 option is implicitly disabled for automatic runs.
  2107 
  2108 \nopagebreak
  2109 {\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
  2110 \textit{batch\_size} (\S\ref{optimizations}).}
  2111 
  2112 \optrue{show\_skolems}{hide\_skolem}
  2113 Specifies whether the values of Skolem constants should be displayed as part of
  2114 counterexamples. Skolem constants correspond to bound variables in the original
  2115 formula and usually help us to understand why the counterexample falsifies the
  2116 formula.
  2117 
  2118 \nopagebreak
  2119 {\small See also \textit{skolemize} (\S\ref{optimizations}).}
  2120 
  2121 \opfalse{show\_datatypes}{hide\_datatypes}
  2122 Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
  2123 be displayed as part of counterexamples. Such subsets are sometimes helpful when
  2124 investigating whether a potential counterexample is genuine or spurious, but
  2125 their potential for clutter is real.
  2126 
  2127 \opfalse{show\_consts}{hide\_consts}
  2128 Specifies whether the values of constants occurring in the formula (including
  2129 its axioms) should be displayed along with any counterexample. These values are
  2130 sometimes helpful when investigating why a counterexample is
  2131 genuine, but they can clutter the output.
  2132 
  2133 \opfalse{show\_all}{dont\_show\_all}
  2134 Enabling this option effectively enables \textit{show\_skolems},
  2135 \textit{show\_datatypes}, and \textit{show\_consts}.
  2136 
  2137 \opdefault{max\_potential}{int}{$\mathbf{1}$}
  2138 Specifies the maximum number of potential counterexamples to display. Setting
  2139 this option to 0 speeds up the search for a genuine counterexample. This option
  2140 is implicitly set to 0 for automatic runs. If you set this option to a value
  2141 greater than 1, you will need an incremental SAT solver: For efficiency, it is
  2142 recommended to install the JNI version of MiniSat and set \textit{sat\_solver} =
  2143 \textit{MiniSat\_JNI}. Also be aware that many of the counterexamples may look
  2144 identical, unless the \textit{show\_all} (\S\ref{output-format}) option is
  2145 enabled.
  2146 
  2147 \nopagebreak
  2148 {\small See also \textit{check\_potential} (\S\ref{authentication}) and
  2149 \textit{sat\_solver} (\S\ref{optimizations}).}
  2150 
  2151 \opdefault{max\_genuine}{int}{$\mathbf{1}$}
  2152 Specifies the maximum number of genuine counterexamples to display. If you set
  2153 this option to a value greater than 1, you will need an incremental SAT solver:
  2154 For efficiency, it is recommended to install the JNI version of MiniSat and set
  2155 \textit{sat\_solver} = \textit{MiniSat\_JNI}. Also be aware that many of the
  2156 counterexamples may look identical, unless the \textit{show\_all}
  2157 (\S\ref{output-format}) option is enabled.
  2158 
  2159 \nopagebreak
  2160 {\small See also \textit{check\_genuine} (\S\ref{authentication}) and
  2161 \textit{sat\_solver} (\S\ref{optimizations}).}
  2162 
  2163 \opnodefault{eval}{term\_list}
  2164 Specifies the list of terms whose values should be displayed along with
  2165 counterexamples. This option suffers from an ``observer effect'': Nitpick might
  2166 find different counterexamples for different values of this option.
  2167 
  2168 \oparg{format}{term}{int\_seq}
  2169 Specifies how to uncurry the value displayed for a variable or constant.
  2170 Uncurrying sometimes increases the readability of the output for high-arity
  2171 functions. For example, given the variable $y \mathbin{\Colon} {'a}\Rightarrow
  2172 {'b}\Rightarrow {'c}\Rightarrow {'d}\Rightarrow {'e}\Rightarrow {'f}\Rightarrow
  2173 {'g}$, setting \textit{format}~$y$ = 3 tells Nitpick to group the last three
  2174 arguments, as if the type had been ${'a}\Rightarrow {'b}\Rightarrow
  2175 {'c}\Rightarrow {'d}\times {'e}\times {'f}\Rightarrow {'g}$. In general, a list
  2176 of values $n_1,\ldots,n_k$ tells Nitpick to show the last $n_k$ arguments as an
  2177 $n_k$-tuple, the previous $n_{k-1}$ arguments as an $n_{k-1}$-tuple, and so on;
  2178 arguments that are not accounted for are left alone, as if the specification had
  2179 been $1,\ldots,1,n_1,\ldots,n_k$.
  2180 
  2181 \nopagebreak
  2182 {\small See also \textit{uncurry} (\S\ref{optimizations}).}
  2183 
  2184 \opdefault{format}{int\_seq}{$\mathbf{1}$}
  2185 Specifies the default format to use. Irrespective of the default format, the
  2186 extra arguments to a Skolem constant corresponding to the outer bound variables
  2187 are kept separated from the remaining arguments, the \textbf{for} arguments of
  2188 an inductive definitions are kept separated from the remaining arguments, and
  2189 the iteration counter of an unrolled inductive definition is shown alone. The
  2190 default format can be overridden on a per-variable or per-constant basis using
  2191 the \textit{format}~\qty{term} option described above.
  2192 \end{enum}
  2193 
  2194 %% MARK: Authentication
  2195 \subsection{Authentication}
  2196 \label{authentication}
  2197 
  2198 \begin{enum}
  2199 \opfalse{check\_potential}{trust\_potential}
  2200 Specifies whether potential counterexamples should be given to Isabelle's
  2201 \textit{auto} tactic to assess their validity. If a potential counterexample is
  2202 shown to be genuine, Nitpick displays a message to this effect and terminates.
  2203 
  2204 \nopagebreak
  2205 {\small See also \textit{max\_potential} (\S\ref{output-format}).}
  2206 
  2207 \opfalse{check\_genuine}{trust\_genuine}
  2208 Specifies whether genuine and likely genuine counterexamples should be given to
  2209 Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine''
  2210 counterexample is shown to be spurious, the user is kindly asked to send a bug
  2211 report to the author at
  2212 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@in.tum.de}.
  2213 
  2214 \nopagebreak
  2215 {\small See also \textit{max\_genuine} (\S\ref{output-format}).}
  2216 
  2217 \opnodefault{expect}{string}
  2218 Specifies the expected outcome, which must be one of the following:
  2219 
  2220 \begin{enum}
  2221 \item[$\bullet$] \textbf{\textit{genuine}}: Nitpick found a genuine counterexample.
  2222 \item[$\bullet$] \textbf{\textit{likely\_genuine}}: Nitpick found a ``likely
  2223 genuine'' counterexample (i.e., a counterexample that is genuine unless
  2224 it contradicts a missing axiom or a dangerous option was used inappropriately).
  2225 \item[$\bullet$] \textbf{\textit{potential}}: Nitpick found a potential counterexample.
  2226 \item[$\bullet$] \textbf{\textit{none}}: Nitpick found no counterexample.
  2227 \item[$\bullet$] \textbf{\textit{unknown}}: Nitpick encountered some problem (e.g.,
  2228 Kodkod ran out of memory).
  2229 \end{enum}
  2230 
  2231 Nitpick emits an error if the actual outcome differs from the expected outcome.
  2232 This option is useful for regression testing.
  2233 \end{enum}
  2234 
  2235 \subsection{Optimizations}
  2236 \label{optimizations}
  2237 
  2238 \def\cpp{C\nobreak\raisebox{.1ex}{+}\nobreak\raisebox{.1ex}{+}}
  2239 
  2240 \sloppy
  2241 
  2242 \begin{enum}
  2243 \opdefault{sat\_solver}{string}{smart}
  2244 Specifies which SAT solver to use. SAT solvers implemented in C or \cpp{} tend
  2245 to be faster than their Java counterparts, but they can be more difficult to
  2246 install. Also, if you set the \textit{max\_potential} (\S\ref{output-format}) or
  2247 \textit{max\_genuine} (\S\ref{output-format}) option to a value greater than 1,
  2248 you will need an incremental SAT solver, such as \textit{MiniSat\_JNI}
  2249 (recommended) or \textit{SAT4J}.
  2250 
  2251 The supported solvers are listed below:
  2252 
  2253 \begin{enum}
  2254 
  2255 \item[$\bullet$] \textbf{\textit{MiniSat}}: MiniSat is an efficient solver
  2256 written in \cpp{}. To use MiniSat, set the environment variable
  2257 \texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
  2258 executable. The \cpp{} sources and executables for MiniSat are available at
  2259 \url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
  2260 and 2.0 beta (2007-07-21).
  2261 
  2262 \item[$\bullet$] \textbf{\textit{MiniSat\_JNI}}: The JNI (Java Native Interface)
  2263 version of MiniSat is bundled in \texttt{nativesolver.\allowbreak tgz}, which
  2264 you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
  2265 version of MiniSat, the JNI version can be used incrementally.
  2266 
  2267 %%% No longer true:
  2268 %%% "It is bundled with Kodkodi and requires no further installation or
  2269 %%% configuration steps. Alternatively,"
  2270 \item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver
  2271 written in C. You can install a standard version of
  2272 PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
  2273 that contains the \texttt{picosat} executable. The C sources for PicoSAT are
  2274 available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
  2275 Nitpick has been tested with version 913.
  2276 
  2277 \item[$\bullet$] \textbf{\textit{zChaff}}: zChaff is an efficient solver written
  2278 in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
  2279 the directory that contains the \texttt{zchaff} executable. The \cpp{} sources
  2280 and executables for zChaff are available at
  2281 \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
  2282 versions 2004-05-13, 2004-11-15, and 2007-03-12.
  2283 
  2284 \item[$\bullet$] \textbf{\textit{zChaff\_JNI}}: The JNI version of zChaff is
  2285 bundled in \texttt{native\-solver.\allowbreak tgz}, which you will find on
  2286 Kodkod's web site \cite{kodkod-2009}.
  2287 
  2288 \item[$\bullet$] \textbf{\textit{RSat}}: RSat is an efficient solver written in
  2289 \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
  2290 directory that contains the \texttt{rsat} executable. The \cpp{} sources for
  2291 RSat are available at \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been
  2292 tested with version 2.01.
  2293 
  2294 \item[$\bullet$] \textbf{\textit{BerkMin}}: BerkMin561 is an efficient solver
  2295 written in C. To use BerkMin, set the environment variable
  2296 \texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561}
  2297 executable. The BerkMin executables are available at
  2298 \url{http://eigold.tripod.com/BerkMin.html}.
  2299 
  2300 \item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}}: Variant of BerkMin that is
  2301 included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
  2302 version of BerkMin, set the environment variable
  2303 \texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
  2304 executable.
  2305 
  2306 \item[$\bullet$] \textbf{\textit{Jerusat}}: Jerusat 1.3 is an efficient solver
  2307 written in C. To use Jerusat, set the environment variable
  2308 \texttt{JERUSAT\_HOME} to the directory that contains the \texttt{Jerusat1.3}
  2309 executable. The C sources for Jerusat are available at
  2310 \url{http://www.cs.tau.ac.il/~ale1/Jerusat1.3.tgz}.
  2311 
  2312 \item[$\bullet$] \textbf{\textit{SAT4J}}: SAT4J is a reasonably efficient solver
  2313 written in Java that can be used incrementally. It is bundled with Kodkodi and
  2314 requires no further installation or configuration steps. Do not attempt to
  2315 install the official SAT4J packages, because their API is incompatible with
  2316 Kodkod.
  2317 
  2318 \item[$\bullet$] \textbf{\textit{SAT4J\_Light}}: Variant of SAT4J that is
  2319 optimized for small problems. It can also be used incrementally.
  2320 
  2321 \item[$\bullet$] \textbf{\textit{HaifaSat}}: HaifaSat 1.0 beta is an
  2322 experimental solver written in \cpp. To use HaifaSat, set the environment
  2323 variable \texttt{HAIFASAT\_\allowbreak HOME} to the directory that contains the
  2324 \texttt{HaifaSat} executable. The \cpp{} sources for HaifaSat are available at
  2325 \url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}.
  2326 
  2327 \item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
  2328 \textit{smart}, Nitpick selects the first solver among MiniSat,
  2329 PicoSAT, zChaff, RSat, BerkMin, BerkMin\_Alloy, Jerusat, MiniSat\_JNI, and zChaff\_JNI
  2330 that is recognized by Isabelle. If none is found, it falls back on SAT4J, which
  2331 should always be available. If \textit{verbose} (\S\ref{output-format}) is
  2332 enabled, Nitpick displays which SAT solver was chosen.
  2333 \end{enum}
  2334 \fussy
  2335 
  2336 \opdefault{batch\_size}{int\_or\_smart}{smart}
  2337 Specifies the maximum number of Kodkod problems that should be lumped together
  2338 when invoking Kodkodi. Each problem corresponds to one scope. Lumping problems
  2339 together ensures that Kodkodi is launched less often, but it makes the verbose
  2340 output less readable and is sometimes detrimental to performance. If
  2341 \textit{batch\_size} is set to \textit{smart}, the actual value used is 1 if
  2342 \textit{debug} (\S\ref{output-format}) is set and 64 otherwise.
  2343 
  2344 \optrue{destroy\_constrs}{dont\_destroy\_constrs}
  2345 Specifies whether formulas involving (co)in\-duc\-tive datatype constructors should
  2346 be rewritten to use (automatically generated) discriminators and destructors.
  2347 This optimization can drastically reduce the size of the Boolean formulas given
  2348 to the SAT solver.
  2349 
  2350 \nopagebreak
  2351 {\small See also \textit{debug} (\S\ref{output-format}).}
  2352 
  2353 \optrue{specialize}{dont\_specialize}
  2354 Specifies whether functions invoked with static arguments should be specialized.
  2355 This optimization can drastically reduce the search space, especially for
  2356 higher-order functions.
  2357 
  2358 \nopagebreak
  2359 {\small See also \textit{debug} (\S\ref{output-format}) and
  2360 \textit{show\_consts} (\S\ref{output-format}).}
  2361 
  2362 \optrue{skolemize}{dont\_skolemize}
  2363 Specifies whether the formula should be skolemized. For performance reasons,
  2364 (positive) $\forall$-quanti\-fiers that occur in the scope of a higher-order
  2365 (positive) $\exists$-quanti\-fier are left unchanged.
  2366 
  2367 \nopagebreak
  2368 {\small See also \textit{debug} (\S\ref{output-format}) and
  2369 \textit{show\_skolems} (\S\ref{output-format}).}
  2370 
  2371 \optrue{star\_linear\_preds}{dont\_star\_linear\_preds}
  2372 Specifies whether Nitpick should use Kodkod's transitive closure operator to
  2373 encode non-well-founded ``linear inductive predicates,'' i.e., inductive
  2374 predicates for which each the predicate occurs in at most one assumption of each
  2375 introduction rule. Using the reflexive transitive closure is in principle
  2376 equivalent to setting \textit{iter} to the cardinality of the predicate's
  2377 domain, but it is usually more efficient.
  2378 
  2379 {\small See also \textit{wf} (\S\ref{scope-of-search}), \textit{debug}
  2380 (\S\ref{output-format}), and \textit{iter} (\S\ref{scope-of-search}).}
  2381 
  2382 \optrue{uncurry}{dont\_uncurry}
  2383 Specifies whether Nitpick should uncurry functions. Uncurrying has on its own no
  2384 tangible effect on efficiency, but it creates opportunities for the boxing 
  2385 optimization.
  2386 
  2387 \nopagebreak
  2388 {\small See also \textit{box} (\S\ref{scope-of-search}), \textit{debug}
  2389 (\S\ref{output-format}), and \textit{format} (\S\ref{output-format}).}
  2390 
  2391 \optrue{fast\_descrs}{full\_descrs}
  2392 Specifies whether Nitpick should optimize the definite and indefinite
  2393 description operators (THE and SOME). The optimized versions usually help
  2394 Nitpick generate more counterexamples or at least find them faster, but only the
  2395 unoptimized versions are complete when all types occurring in the formula are
  2396 finite.
  2397 
  2398 {\small See also \textit{debug} (\S\ref{output-format}).}
  2399 
  2400 \optrue{peephole\_optim}{no\_peephole\_optim}
  2401 Specifies whether Nitpick should simplify the generated Kodkod formulas using a
  2402 peephole optimizer. These optimizations can make a significant difference.
  2403 Unless you are tracking down a bug in Nitpick or distrust the peephole
  2404 optimizer, you should leave this option enabled.
  2405 
  2406 \opdefault{sym\_break}{int}{20}
  2407 Specifies an upper bound on the number of relations for which Kodkod generates
  2408 symmetry breaking predicates. According to the Kodkod documentation
  2409 \cite{kodkod-2009-options}, ``in general, the higher this value, the more
  2410 symmetries will be broken, and the faster the formula will be solved. But,
  2411 setting the value too high may have the opposite effect and slow down the
  2412 solving.''
  2413 
  2414 \opdefault{sharing\_depth}{int}{3}
  2415 Specifies the depth to which Kodkod should check circuits for equivalence during
  2416 the translation to SAT. The default of 3 is the same as in Alloy. The minimum
  2417 allowed depth is 1. Increasing the sharing may result in a smaller SAT problem,
  2418 but can also slow down Kodkod.
  2419 
  2420 \opfalse{flatten\_props}{dont\_flatten\_props}
  2421 Specifies whether Kodkod should try to eliminate intermediate Boolean variables.
  2422 Although this might sound like a good idea, in practice it can drastically slow
  2423 down Kodkod.
  2424 
  2425 \opdefault{max\_threads}{int}{0}
  2426 Specifies the maximum number of threads to use in Kodkod. If this option is set
  2427 to 0, Kodkod will compute an appropriate value based on the number of processor
  2428 cores available.
  2429 
  2430 \nopagebreak
  2431 {\small See also \textit{batch\_size} (\S\ref{optimizations}) and
  2432 \textit{timeout} (\S\ref{timeouts}).}
  2433 \end{enum}
  2434 
  2435 \subsection{Timeouts}
  2436 \label{timeouts}
  2437 
  2438 \begin{enum}
  2439 \opdefault{timeout}{time}{$\mathbf{30}$ s}
  2440 Specifies the maximum amount of time that the \textbf{nitpick} command should
  2441 spend looking for a counterexample. Nitpick tries to honor this constraint as
  2442 well as it can but offers no guarantees. For automatic runs,
  2443 \textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share
  2444 a time slot whose length is specified by the ``Auto Counterexample Time
  2445 Limit'' option in Proof General.
  2446 
  2447 \nopagebreak
  2448 {\small See also \textit{max\_threads} (\S\ref{optimizations}).}
  2449 
  2450 \opdefault{tac\_timeout}{time}{$\mathbf{500}$\,ms}
  2451 Specifies the maximum amount of time that the \textit{auto} tactic should use
  2452 when checking a counterexample, and similarly that \textit{lexicographic\_order}
  2453 and \textit{size\_change} should use when checking whether a (co)in\-duc\-tive
  2454 predicate is well-founded. Nitpick tries to honor this constraint as well as it
  2455 can but offers no guarantees.
  2456 
  2457 \nopagebreak
  2458 {\small See also \textit{wf} (\S\ref{scope-of-search}),
  2459 \textit{check\_potential} (\S\ref{authentication}),
  2460 and \textit{check\_genuine} (\S\ref{authentication}).}
  2461 \end{enum}
  2462 
  2463 \section{Attribute Reference}
  2464 \label{attribute-reference}
  2465 
  2466 Nitpick needs to consider the definitions of all constants occurring in a
  2467 formula in order to falsify it. For constants introduced using the
  2468 \textbf{definition} command, the definition is simply the associated
  2469 \textit{\_def} axiom. In contrast, instead of using the internal representation
  2470 of functions synthesized by Isabelle's \textbf{primrec}, \textbf{function}, and
  2471 \textbf{nominal\_primrec} packages, Nitpick relies on the more natural
  2472 equational specification entered by the user.
  2473 
  2474 Behind the scenes, Isabelle's built-in packages and theories rely on the
  2475 following attributes to affect Nitpick's behavior:
  2476 
  2477 \begin{itemize}
  2478 \flushitem{\textit{nitpick\_def}}
  2479 
  2480 \nopagebreak
  2481 This attribute specifies an alternative definition of a constant. The
  2482 alternative definition should be logically equivalent to the constant's actual
  2483 axiomatic definition and should be of the form
  2484 
  2485 \qquad $c~{?}x_1~\ldots~{?}x_n \,\equiv\, t$,
  2486 
  2487 where ${?}x_1, \ldots, {?}x_n$ are distinct variables and $c$ does not occur in
  2488 $t$.
  2489 
  2490 \flushitem{\textit{nitpick\_simp}}
  2491 
  2492 \nopagebreak
  2493 This attribute specifies the equations that constitute the specification of a
  2494 constant. For functions defined using the \textbf{primrec}, \textbf{function},
  2495 and \textbf{nominal\_\allowbreak primrec} packages, this corresponds to the
  2496 \textit{simps} rules. The equations must be of the form
  2497 
  2498 \qquad $c~t_1~\ldots\ t_n \,=\, u.$
  2499 
  2500 \flushitem{\textit{nitpick\_psimp}}
  2501 
  2502 \nopagebreak
  2503 This attribute specifies the equations that constitute the partial specification
  2504 of a constant. For functions defined using the \textbf{function} package, this
  2505 corresponds to the \textit{psimps} rules. The conditional equations must be of
  2506 the form
  2507 
  2508 \qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,=\, u$.
  2509 
  2510 \flushitem{\textit{nitpick\_intro}}
  2511 
  2512 \nopagebreak
  2513 This attribute specifies the introduction rules of a (co)in\-duc\-tive predicate.
  2514 For predicates defined using the \textbf{inductive} or \textbf{coinductive}
  2515 command, this corresponds to the \textit{intros} rules. The introduction rules
  2516 must be of the form
  2517 
  2518 \qquad $\lbrakk P_1;\> \ldots;\> P_m;\> M~(c\ t_{11}\ \ldots\ t_{1n});\>
  2519 \ldots;\> M~(c\ t_{k1}\ \ldots\ t_{kn})\rbrakk \,\Longrightarrow\, c\ u_1\
  2520 \ldots\ u_n$,
  2521 
  2522 where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an
  2523 optional monotonic operator. The order of the assumptions is irrelevant.
  2524 
  2525 \end{itemize}
  2526 
  2527 When faced with a constant, Nitpick proceeds as follows:
  2528 
  2529 \begin{enum}
  2530 \item[1.] If the \textit{nitpick\_simp} set associated with the constant
  2531 is not empty, Nitpick uses these rules as the specification of the constant.
  2532 
  2533 \item[2.] Otherwise, if the \textit{nitpick\_psimp} set associated with
  2534 the constant is not empty, it uses these rules as the specification of the
  2535 constant.
  2536 
  2537 \item[3.] Otherwise, it looks up the definition of the constant:
  2538 
  2539 \begin{enum}
  2540 \item[1.] If the \textit{nitpick\_def} set associated with the constant
  2541 is not empty, it uses the latest rule added to the set as the definition of the
  2542 constant; otherwise it uses the actual definition axiom.
  2543 \item[2.] If the definition is of the form
  2544 
  2545 \qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{lfp}~(\lambda f.\; t)$,
  2546 
  2547 then Nitpick assumes that the definition was made using an inductive package and
  2548 based on the introduction rules marked with \textit{nitpick\_\allowbreak
  2549 ind\_\allowbreak intros} tries to determine whether the definition is
  2550 well-founded.
  2551 \end{enum}
  2552 \end{enum}
  2553 
  2554 As an illustration, consider the inductive definition
  2555 
  2556 \prew
  2557 \textbf{inductive}~\textit{odd}~\textbf{where} \\
  2558 ``\textit{odd}~1'' $\,\mid$ \\
  2559 ``\textit{odd}~$n\,\Longrightarrow\, \textit{odd}~(\textit{Suc}~(\textit{Suc}~n))$''
  2560 \postw
  2561 
  2562 Isabelle automatically attaches the \textit{nitpick\_intro} attribute to
  2563 the above rules. Nitpick then uses the \textit{lfp}-based definition in
  2564 conjunction with these rules. To override this, we can specify an alternative
  2565 definition as follows:
  2566 
  2567 \prew
  2568 \textbf{lemma} $\mathit{odd\_def}'$ [\textit{nitpick\_def}]: ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
  2569 \postw
  2570 
  2571 Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2
  2572 = 1$. Alternatively, we can specify an equational specification of the constant:
  2573 
  2574 \prew
  2575 \textbf{lemma} $\mathit{odd\_simp}'$ [\textit{nitpick\_simp}]: ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
  2576 \postw
  2577 
  2578 Such tweaks should be done with great care, because Nitpick will assume that the
  2579 constant is completely defined by its equational specification. For example, if
  2580 you make ``$\textit{odd}~(2 * k + 1)$'' a \textit{nitpick\_simp} rule and neglect to provide rules to handle the $2 * k$ case, Nitpick will define
  2581 $\textit{odd}~n$ arbitrarily for even values of $n$. The \textit{debug}
  2582 (\S\ref{output-format}) option is extremely useful to understand what is going
  2583 on when experimenting with \textit{nitpick\_} attributes.
  2584 
  2585 \section{Standard ML Interface}
  2586 \label{standard-ml-interface}
  2587 
  2588 Nitpick provides a rich Standard ML interface used mainly for internal purposes
  2589 and debugging. Among the most interesting functions exported by Nitpick are
  2590 those that let you invoke the tool programmatically and those that let you
  2591 register and unregister custom coinductive datatypes.
  2592 
  2593 \subsection{Invocation of Nitpick}
  2594 \label{invocation-of-nitpick}
  2595 
  2596 The \textit{Nitpick} structure offers the following functions for invoking your
  2597 favorite counterexample generator:
  2598 
  2599 \prew
  2600 $\textbf{val}\,~\textit{pick\_nits\_in\_term} : \\
  2601 \hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{term~list} \rightarrow \textit{term} \\
  2602 \hbox{}\quad{\rightarrow}\; \textit{string} * \textit{Proof.state}$ \\
  2603 $\textbf{val}\,~\textit{pick\_nits\_in\_subgoal} : \\
  2604 \hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{int} \rightarrow \textit{string} * \textit{Proof.state}$
  2605 \postw
  2606 
  2607 The return value is a new proof state paired with an outcome string
  2608 (``genuine'', ``likely\_genuine'', ``potential'', ``none'', or ``unknown''). The
  2609 \textit{params} type is a large record that lets you set Nitpick's options. The
  2610 current default options can be retrieved by calling the following function
  2611 defined in the \textit{Nitpick\_Isar} structure:
  2612 
  2613 \prew
  2614 $\textbf{val}\,~\textit{default\_params} :\,
  2615 \textit{theory} \rightarrow (\textit{string} * \textit{string})~\textit{list} \rightarrow \textit{params}$
  2616 \postw
  2617 
  2618 The second argument lets you override option values before they are parsed and
  2619 put into a \textit{params} record. Here is an example:
  2620 
  2621 \prew
  2622 $\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
  2623 $\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t]
  2624 & \textit{state}~\textit{params}~\textit{false} \\[-2pt]
  2625 & \textit{subgoal}\end{aligned}$
  2626 \postw
  2627 
  2628 \let\antiq=\textrm
  2629 
  2630 \subsection{Registration of Coinductive Datatypes}
  2631 \label{registration-of-coinductive-datatypes}
  2632 
  2633 If you have defined a custom coinductive datatype, you can tell Nitpick about
  2634 it, so that it can use an efficient Kodkod axiomatization similar to the one it
  2635 uses for lazy lists. The interface for registering and unregistering coinductive
  2636 datatypes consists of the following pair of functions defined in the
  2637 \textit{Nitpick} structure:
  2638 
  2639 \prew
  2640 $\textbf{val}\,~\textit{register\_codatatype} :\,
  2641 \textit{typ} \rightarrow \textit{string} \rightarrow \textit{styp~list} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\
  2642 $\textbf{val}\,~\textit{unregister\_codatatype} :\,
  2643 \textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$
  2644 \postw
  2645 
  2646 The type $'a~\textit{llist}$ of lazy lists is already registered; had it
  2647 not been, you could have told Nitpick about it by adding the following line
  2648 to your theory file:
  2649 
  2650 \prew
  2651 $\textbf{setup}~\,\{{*}\,~\!\begin{aligned}[t]
  2652 & \textit{Nitpick.register\_codatatype} \\[-2pt]
  2653 & \qquad @\{\antiq{typ}~``\kern1pt'a~\textit{llist}\textrm{''}\}~@\{\antiq{const\_name}~ \textit{llist\_case}\} \\[-2pt] %% TYPESETTING
  2654 & \qquad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])\,\ {*}\}\end{aligned}$
  2655 \postw
  2656 
  2657 The \textit{register\_codatatype} function takes a coinductive type, its case
  2658 function, and the list of its constructors. The case function must take its
  2659 arguments in the order that the constructors are listed. If no case function
  2660 with the correct signature is available, simply pass the empty string.
  2661 
  2662 On the other hand, if your goal is to cripple Nitpick, add the following line to
  2663 your theory file and try to check a few conjectures about lazy lists:
  2664 
  2665 \prew
  2666 $\textbf{setup}~\,\{{*}\,~\textit{Nitpick.unregister\_codatatype}~@\{\antiq{typ}~``
  2667 \kern1pt'a~\textit{list}\textrm{''}\}\ \,{*}\}$
  2668 \postw
  2669 
  2670 Inductive datatypes can be registered as coinductive datatypes, given
  2671 appropriate coinductive constructors. However, doing so precludes
  2672 the use of the inductive constructors---Nitpick will generate an error if they
  2673 are needed.
  2674 
  2675 \section{Known Bugs and Limitations}
  2676 \label{known-bugs-and-limitations}
  2677 
  2678 Here are the known bugs and limitations in Nitpick at the time of writing:
  2679 
  2680 \begin{enum}
  2681 \item[$\bullet$] Underspecified functions defined using the \textbf{primrec},
  2682 \textbf{function}, or \textbf{nominal\_\allowbreak primrec} packages can lead
  2683 Nitpick to generate spurious counterexamples for theorems that refer to values
  2684 for which the function is not defined. For example:
  2685 
  2686 \prew
  2687 \textbf{primrec} \textit{prec} \textbf{where} \\
  2688 ``$\textit{prec}~(\textit{Suc}~n) = n$'' \\[2\smallskipamount]
  2689 \textbf{lemma} ``$\textit{prec}~0 = \undef$'' \\
  2690 \textbf{nitpick} \\[2\smallskipamount]
  2691 \quad{\slshape Nitpick found a counterexample for \textit{card nat}~= 2: 
  2692 \nopagebreak
  2693 \\[2\smallskipamount]
  2694 \hbox{}\qquad Empty assignment} \nopagebreak\\[2\smallskipamount]
  2695 \textbf{by}~(\textit{auto simp}:~\textit{prec\_def})
  2696 \postw
  2697 
  2698 Such theorems are considered bad style because they rely on the internal
  2699 representation of functions synthesized by Isabelle, which is an implementation
  2700 detail.
  2701 
  2702 \item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions,
  2703 which can become invalid if you change the definition of an inductive predicate
  2704 that is registered in the cache. To clear the cache,
  2705 run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
  2706 501$\,\textit{ms}$).
  2707 
  2708 \item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
  2709 \textbf{guess} command in a structured proof.
  2710 
  2711 \item[$\bullet$] The \textit{nitpick\_} attributes and the
  2712 \textit{Nitpick.register\_} functions can cause havoc if used improperly.
  2713 
  2714 \item[$\bullet$] Although this has never been observed, arbitrary theorem
  2715 morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
  2716 
  2717 \item[$\bullet$] Local definitions are not supported and result in an error.
  2718 
  2719 %\item[$\bullet$] All constants and types whose names start with
  2720 %\textit{Nitpick}{.} are reserved for internal use.
  2721 \end{enum}
  2722 
  2723 \let\em=\sl
  2724 \bibliography{../manual}{}
  2725 \bibliographystyle{abbrv}
  2726 
  2727 \end{document}