1 \documentclass[a4paper,12pt]{article}
2 \usepackage[T1]{fontenc}
5 \usepackage[french,english]{babel}
11 %\usepackage[scaled=.85]{beramono}
12 \usepackage{../iman,../pdfsetup}
15 %\evensidemargin=4.6mm
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)}}
28 \def\undef{\textit{undefined}}
30 %\def\unr{\textit{others}}
32 \def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
33 \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
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}
43 \title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]
44 Picking Nits \\[\smallskipamount]
45 \Large A User's Guide to Nitpick for Isabelle/HOL 2010}
47 Jasmin Christian Blanchette \\
48 {\normalsize Fakult\"at f\"ur Informatik, Technische Universit\"at M\"unchen} \\
55 \setlength{\parskip}{.7em plus .2em minus .1em}
56 \setlength{\parindent}{0pt}
57 \setlength{\abovedisplayskip}{\parskip}
58 \setlength{\abovedisplayshortskip}{.9\parskip}
59 \setlength{\belowdisplayskip}{\parskip}
60 \setlength{\belowdisplayshortskip}{.9\parskip}
62 % General-purpose enum environment with correct spacing
63 \newenvironment{enum}%
65 \setlength{\topsep}{.1\parskip}%
66 \setlength{\partopsep}{.1\parskip}%
67 \setlength{\itemsep}{\parskip}%
68 \advance\itemsep by-\parsep}}
71 \def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
72 \advance\rightskip by\leftmargin}
73 \def\post{\vskip0pt plus1ex\endgroup}
75 \def\prew{\pre\advance\rightskip by-\leftmargin}
78 \section{Introduction}
81 Nitpick \cite{blanchette-nipkow-2009} is a counterexample generator for
82 Isabelle/HOL \cite{isa-tutorial} that is designed to handle formulas
83 combining (co)in\-duc\-tive datatypes, (co)in\-duc\-tively defined predicates, and
84 quantifiers. It builds on Kodkod \cite{torlak-jackson-2007}, a highly optimized
85 first-order relational model finder developed by the Software Design Group at
86 MIT. It is conceptually similar to Refute \cite{weber-2008}, from which it
87 borrows many ideas and code fragments, but it benefits from Kodkod's
88 optimizations and a new encoding scheme. The name Nitpick is shamelessly
89 appropriated from a now retired Alloy precursor.
91 Nitpick is easy to use---you simply enter \textbf{nitpick} after a putative
92 theorem and wait a few seconds. Nonetheless, there are situations where knowing
93 how it works under the hood and how it reacts to various options helps
94 increase the test coverage. This manual also explains how to install the tool on
95 your workstation. Should the motivation fail you, think of the many hours of
96 hard work Nitpick will save you. Proving non-theorems is \textsl{hard work}.
98 Another common use of Nitpick is to find out whether the axioms of a locale are
99 satisfiable, while the locale is being developed. To check this, it suffices to
103 \textbf{lemma}~``$\textit{False}$'' \\
104 \textbf{nitpick}~[\textit{show\_all}]
107 after the locale's \textbf{begin} keyword. To falsify \textit{False}, Nitpick
108 must find a model for the axioms. If it finds no model, we have an indication
109 that the axioms might be unsatisfiable.
111 Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.5 virtual
112 machine called \texttt{java}. The examples presented in this manual can be found
113 in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
116 \setbox\boxA=\hbox{\texttt{nospam}}
118 The known bugs and limitations at the time of writing are listed in
119 \S\ref{known-bugs-and-limitations}. Comments and bug reports concerning Nitpick
120 or this manual should be directed to
121 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
122 in.\allowbreak tum.\allowbreak de}.
124 \vskip2.5\smallskipamount
126 \textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
127 suggesting several textual improvements.
128 % and Perry James for reporting a typo.
130 \section{First Steps}
133 This section introduces Nitpick by presenting small examples. If possible, you
134 should try out the examples on your workstation. Your theory file should start
138 \textbf{theory}~\textit{Scratch} \\
139 \textbf{imports}~\textit{Main} \\
143 The results presented here were obtained using the JNI version of MiniSat and
144 with multithreading disabled to reduce nondeterminism. This was done by adding
148 \textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSatJNI}, \,\textit{max\_threads}~= 1]
151 after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
152 Kodkodi and is precompiled for the major platforms. Other SAT solvers can also
153 be installed, as explained in \S\ref{optimizations}. If you have already
154 configured SAT solvers in Isabelle (e.g., for Refute), these will also be
155 available to Nitpick.
157 Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
158 Nitpick also provides an automatic mode that can be enabled by specifying
161 \textbf{nitpick\_params} [\textit{auto}]
164 at the beginning of the theory file. In this mode, Nitpick is run for up to 5
165 seconds (by default) on every newly entered theorem, much like Auto Quickcheck.
167 \subsection{Propositional Logic}
168 \label{propositional-logic}
170 Let's start with a trivial example from propositional logic:
173 \textbf{lemma}~``$P \longleftrightarrow Q$'' \\
177 You should get the following output:
181 Nitpick found a counterexample: \\[2\smallskipamount]
182 \hbox{}\qquad Free variables: \nopagebreak \\
183 \hbox{}\qquad\qquad $P = \textit{True}$ \\
184 \hbox{}\qquad\qquad $Q = \textit{False}$
187 Nitpick can also be invoked on individual subgoals, as in the example below:
190 \textbf{apply}~\textit{auto} \\[2\smallskipamount]
191 {\slshape goal (2 subgoals): \\
192 \ 1. $P\,\Longrightarrow\, Q$ \\
193 \ 2. $Q\,\Longrightarrow\, P$} \\[2\smallskipamount]
194 \textbf{nitpick}~1 \\[2\smallskipamount]
195 {\slshape Nitpick found a counterexample: \\[2\smallskipamount]
196 \hbox{}\qquad Free variables: \nopagebreak \\
197 \hbox{}\qquad\qquad $P = \textit{True}$ \\
198 \hbox{}\qquad\qquad $Q = \textit{False}$} \\[2\smallskipamount]
199 \textbf{nitpick}~2 \\[2\smallskipamount]
200 {\slshape Nitpick found a counterexample: \\[2\smallskipamount]
201 \hbox{}\qquad Free variables: \nopagebreak \\
202 \hbox{}\qquad\qquad $P = \textit{False}$ \\
203 \hbox{}\qquad\qquad $Q = \textit{True}$} \\[2\smallskipamount]
207 \subsection{Type Variables}
208 \label{type-variables}
210 If you are left unimpressed by the previous example, don't worry. The next
211 one is more mind- and computer-boggling:
214 \textbf{lemma} ``$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
216 \pagebreak[2] %% TYPESETTING
218 The putative lemma involves the definite description operator, {THE}, presented
219 in section 5.10.1 of the Isabelle tutorial \cite{isa-tutorial}. The
220 operator is defined by the axiom $(\textrm{THE}~x.\; x = a) = a$. The putative
221 lemma is merely asserting the indefinite description operator axiom with {THE}
222 substituted for {SOME}.
224 The free variable $x$ and the bound variable $y$ have type $'a$. For formulas
225 containing type variables, Nitpick enumerates the possible domains for each type
226 variable, up to a given cardinality (8 by default), looking for a finite
230 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
232 Trying 8 scopes: \nopagebreak \\
233 \hbox{}\qquad \textit{card}~$'a$~= 1; \\
234 \hbox{}\qquad \textit{card}~$'a$~= 2; \\
235 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
236 \hbox{}\qquad \textit{card}~$'a$~= 8. \\[2\smallskipamount]
237 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
238 \hbox{}\qquad Free variables: \nopagebreak \\
239 \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
240 \hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount]
244 Nitpick found a counterexample in which $'a$ has cardinality 3. (For
245 cardinalities 1 and 2, the formula holds.) In the counterexample, the three
246 values of type $'a$ are written $a_1$, $a_2$, and $a_3$.
248 The message ``Trying $n$ scopes: {\ldots}''\ is shown only if the option
249 \textit{verbose} is enabled. You can specify \textit{verbose} each time you
250 invoke \textbf{nitpick}, or you can set it globally using the command
253 \textbf{nitpick\_params} [\textit{verbose}]
256 This command also displays the current default values for all of the options
257 supported by Nitpick. The options are listed in \S\ref{option-reference}.
259 \subsection{Constants}
262 By just looking at Nitpick's output, it might not be clear why the
263 counterexample in \S\ref{type-variables} is genuine. Let's invoke Nitpick again,
264 this time telling it to show the values of the constants that occur in the
268 \textbf{lemma}~``$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$'' \\
269 \textbf{nitpick}~[\textit{show\_consts}] \\[2\smallskipamount]
271 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
272 \hbox{}\qquad Free variables: \nopagebreak \\
273 \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
274 \hbox{}\qquad\qquad $x = a_3$ \\
275 \hbox{}\qquad Constant: \nopagebreak \\
276 \hbox{}\qquad\qquad $\textit{The}~\textsl{fallback} = a_1$
279 We can see more clearly now. Since the predicate $P$ isn't true for a unique
280 value, $\textrm{THE}~y.\;P~y$ can denote any value of type $'a$, even
281 $a_1$. Since $P~a_1$ is false, the entire formula is falsified.
283 As an optimization, Nitpick's preprocessor introduced the special constant
284 ``\textit{The} fallback'' corresponding to $\textrm{THE}~y.\;P~y$ (i.e.,
285 $\mathit{The}~(\lambda y.\;P~y)$) when there doesn't exist a unique $y$
286 satisfying $P~y$. We disable this optimization by passing the
287 \textit{full\_descrs} option:
290 \textbf{nitpick}~[\textit{full\_descrs},\, \textit{show\_consts}] \\[2\smallskipamount]
292 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
293 \hbox{}\qquad Free variables: \nopagebreak \\
294 \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
295 \hbox{}\qquad\qquad $x = a_3$ \\
296 \hbox{}\qquad Constant: \nopagebreak \\
297 \hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$
300 As the result of another optimization, Nitpick directly assigned a value to the
301 subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we
302 disable this second optimization by using the command
305 \textbf{nitpick}~[\textit{dont\_specialize},\, \textit{full\_descrs},\,
306 \textit{show\_consts}]
309 we finally get \textit{The}:
312 \slshape Constant: \nopagebreak \\
313 \hbox{}\qquad $\mathit{The} = \undef{}
314 (\!\begin{aligned}[t]%
315 & \{\} := a_3,\> \{a_3\} := a_3,\> \{a_2\} := a_2, \\[-2pt] %% TYPESETTING
316 & \{a_2, a_3\} := a_1,\> \{a_1\} := a_1,\> \{a_1, a_3\} := a_3, \\[-2pt]
317 & \{a_1, a_2\} := a_3,\> \{a_1, a_2, a_3\} := a_3)\end{aligned}$
320 Notice that $\textit{The}~(\lambda y.\;P~y) = \textit{The}~\{a_2, a_3\} = a_1$,
321 just like before.\footnote{The \undef{} symbol's presence is explained as
322 follows: In higher-order logic, any function can be built from the undefined
323 function using repeated applications of the function update operator $f(x :=
324 y)$, just like any list can be built from the empty list using $x \mathbin{\#}
327 Our misadventures with THE suggest adding `$\exists!x{.}$' (``there exists a
328 unique $x$ such that'') at the front of our putative lemma's assumption:
331 \textbf{lemma}~``$\exists {!}x.\; P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
334 The fix appears to work:
337 \textbf{nitpick} \\[2\smallskipamount]
338 \slshape Nitpick found no counterexample.
341 We can further increase our confidence in the formula by exhausting all
342 cardinalities up to 50:
345 \textbf{nitpick} [\textit{card} $'a$~= 1--50]\footnote{The symbol `--'
346 can be entered as \texttt{-} (hyphen) or
347 \texttt{\char`\\\char`\<midarrow\char`\>}.} \\[2\smallskipamount]
348 \slshape Nitpick found no counterexample.
351 Let's see if Sledgehammer \cite{sledgehammer-2009} can find a proof:
354 \textbf{sledgehammer} \\[2\smallskipamount]
355 {\slshape Sledgehammer: external prover ``$e$'' for subgoal 1: \\
356 $\exists{!}x.\; P~x\,\Longrightarrow\, P~(\hbox{\slshape THE}~y.\; P~y)$ \\
357 Try this command: \textrm{apply}~(\textit{metis~the\_equality})} \\[2\smallskipamount]
358 \textbf{apply}~(\textit{metis~the\_equality\/}) \nopagebreak \\[2\smallskipamount]
359 {\slshape No subgoals!}% \\[2\smallskipamount]
363 This must be our lucky day.
365 \subsection{Skolemization}
366 \label{skolemization}
368 Are all invertible functions onto? Let's find out:
371 \textbf{lemma} ``$\exists g.\; \forall x.~g~(f~x) = x
372 \,\Longrightarrow\, \forall y.\; \exists x.~y = f~x$'' \\
373 \textbf{nitpick} \\[2\smallskipamount]
375 Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\[2\smallskipamount]
376 \hbox{}\qquad Free variable: \nopagebreak \\
377 \hbox{}\qquad\qquad $f = \undef{}(b_1 := a_1)$ \\
378 \hbox{}\qquad Skolem constants: \nopagebreak \\
379 \hbox{}\qquad\qquad $g = \undef{}(a_1 := b_1,\> a_2 := b_1)$ \\
380 \hbox{}\qquad\qquad $y = a_2$
383 Although $f$ is the only free variable occurring in the formula, Nitpick also
384 displays values for the bound variables $g$ and $y$. These values are available
385 to Nitpick because it performs skolemization as a preprocessing step.
387 In the previous example, skolemization only affected the outermost quantifiers.
388 This is not always the case, as illustrated below:
391 \textbf{lemma} ``$\exists x.\; \forall f.\; f~x = x$'' \\
392 \textbf{nitpick} \\[2\smallskipamount]
394 Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
395 \hbox{}\qquad Skolem constant: \nopagebreak \\
396 \hbox{}\qquad\qquad $\lambda x.\; f =
397 \undef{}(\!\begin{aligned}[t]
398 & a_1 := \undef{}(a_1 := a_2,\> a_2 := a_1), \\[-2pt]
399 & a_2 := \undef{}(a_1 := a_1,\> a_2 := a_1))\end{aligned}$
402 The variable $f$ is bound within the scope of $x$; therefore, $f$ depends on
403 $x$, as suggested by the notation $\lambda x.\,f$. If $x = a_1$, then $f$ is the
404 function that maps $a_1$ to $a_2$ and vice versa; otherwise, $x = a_2$ and $f$
405 maps both $a_1$ and $a_2$ to $a_1$. In both cases, $f~x \not= x$.
407 The source of the Skolem constants is sometimes more obscure:
410 \textbf{lemma} ``$\mathit{refl}~r\,\Longrightarrow\, \mathit{sym}~r$'' \\
411 \textbf{nitpick} \\[2\smallskipamount]
413 Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
414 \hbox{}\qquad Free variable: \nopagebreak \\
415 \hbox{}\qquad\qquad $r = \{(a_1, a_1),\, (a_2, a_1),\, (a_2, a_2)\}$ \\
416 \hbox{}\qquad Skolem constants: \nopagebreak \\
417 \hbox{}\qquad\qquad $\mathit{sym}.x = a_2$ \\
418 \hbox{}\qquad\qquad $\mathit{sym}.y = a_1$
421 What happened here is that Nitpick expanded the \textit{sym} constant to its
425 $\mathit{sym}~r \,\equiv\,
426 \forall x\> y.\,\> (x, y) \in r \longrightarrow (y, x) \in r.$
429 As their names suggest, the Skolem constants $\mathit{sym}.x$ and
430 $\mathit{sym}.y$ are simply the bound variables $x$ and $y$
431 from \textit{sym}'s definition.
433 Although skolemization is a useful optimization, you can disable it by invoking
434 Nitpick with \textit{dont\_skolemize}. See \S\ref{optimizations} for details.
436 \subsection{Natural Numbers and Integers}
437 \label{natural-numbers-and-integers}
439 Because of the axiom of infinity, the type \textit{nat} does not admit any
440 finite models. To deal with this, Nitpick considers prefixes $\{0,\, 1,\,
441 \ldots,\, K - 1\}$ of \textit{nat} (where $K = \textit{card}~\textit{nat}$) and
442 maps all other numbers to the undefined value ($\unk$). The type \textit{int} is
443 handled in a similar way: If $K = \textit{card}~\textit{int}$, the subset of
444 \textit{int} known to Nitpick is $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor
445 K/2 \rfloor\}$. Undefined values lead to a three-valued logic.
447 Here is an example involving \textit{int}:
450 \textbf{lemma} ``$\lbrakk i \le j;\> n \le (m{\Colon}\mathit{int})\rbrakk \,\Longrightarrow\, i * n + j * m \le i * m + j * n$'' \\
451 \textbf{nitpick} \\[2\smallskipamount]
452 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
453 \hbox{}\qquad Free variables: \nopagebreak \\
454 \hbox{}\qquad\qquad $i = 0$ \\
455 \hbox{}\qquad\qquad $j = 1$ \\
456 \hbox{}\qquad\qquad $m = 1$ \\
457 \hbox{}\qquad\qquad $n = 0$
460 With infinite types, we don't always have the luxury of a genuine counterexample
461 and must often content ourselves with a potential one. The tedious task of
462 finding out whether the potential counterexample is in fact genuine can be
463 outsourced to \textit{auto} by passing the option \textit{check\_potential}. For
467 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
468 \textbf{nitpick} [\textit{card~nat}~= 100,\, \textit{check\_potential}] \\[2\smallskipamount]
469 \slshape Nitpick found a potential counterexample: \\[2\smallskipamount]
470 \hbox{}\qquad Free variable: \nopagebreak \\
471 \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
472 Confirmation by ``\textit{auto}'': The above counterexample is genuine.
475 You might wonder why the counterexample is first reported as potential. The root
476 of the problem is that the bound variable in $\forall n.\; \textit{Suc}~n
477 \mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds an $n$ such
478 that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
479 \textit{False}; but otherwise, it does not know anything about values of $n \ge
480 \textit{card~nat}$ and must therefore evaluate the assumption to $\unk$, not
481 \textit{True}. Since the assumption can never be satisfied, the putative lemma
482 can never be falsified.
484 Incidentally, if you distrust the so-called genuine counterexamples, you can
485 enable \textit{check\_\allowbreak genuine} to verify them as well. However, be
486 aware that \textit{auto} will often fail to prove that the counterexample is
489 Some conjectures involving elementary number theory make Nitpick look like a
490 giant with feet of clay:
493 \textbf{lemma} ``$P~\textit{Suc}$'' \\
494 \textbf{nitpick} [\textit{card} = 1--6] \\[2\smallskipamount]
496 Nitpick found no counterexample.
499 For any cardinality $k$, \textit{Suc} is the partial function $\{0 \mapsto 1,\,
500 1 \mapsto 2,\, \ldots,\, k - 1 \mapsto \unk\}$, which evaluates to $\unk$ when
501 it is passed as argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$.
502 The next example is similar:
505 \textbf{lemma} ``$P~(\textit{op}~{+}\Colon
506 \textit{nat}\mathbin{\Rightarrow}\textit{nat}\mathbin{\Rightarrow}\textit{nat})$'' \\
507 \textbf{nitpick} [\textit{card nat} = 1] \\[2\smallskipamount]
508 {\slshape Nitpick found a counterexample:} \\[2\smallskipamount]
509 \hbox{}\qquad Free variable: \nopagebreak \\
510 \hbox{}\qquad\qquad $P = \{\}$ \\[2\smallskipamount]
511 \textbf{nitpick} [\textit{card nat} = 2] \\[2\smallskipamount]
512 {\slshape Nitpick found no counterexample.}
515 The problem here is that \textit{op}~+ is total when \textit{nat} is taken to be
516 $\{0\}$ but becomes partial as soon as we add $1$, because $1 + 1 \notin \{0,
519 Because numbers are infinite and are approximated using a three-valued logic,
520 there is usually no need to systematically enumerate domain sizes. If Nitpick
521 cannot find a genuine counterexample for \textit{card~nat}~= $k$, it is very
522 unlikely that one could be found for smaller domains. (The $P~(\textit{op}~{+})$
523 example above is an exception to this principle.) Nitpick nonetheless enumerates
524 all cardinalities from 1 to 8 for \textit{nat}, mainly because smaller
525 cardinalities are fast to handle and give rise to simpler counterexamples. This
526 is explained in more detail in \S\ref{scope-monotonicity}.
528 \subsection{Inductive Datatypes}
529 \label{inductive-datatypes}
531 Like natural numbers and integers, inductive datatypes with recursive
532 constructors admit no finite models and must be approximated by a subterm-closed
533 subset. For example, using a cardinality of 10 for ${'}a~\textit{list}$,
534 Nitpick looks for all counterexamples that can be built using at most 10
537 Let's see with an example involving \textit{hd} (which returns the first element
538 of a list) and $@$ (which concatenates two lists):
541 \textbf{lemma} ``$\textit{hd}~(\textit{xs} \mathbin{@} [y, y]) = \textit{hd}~\textit{xs}$'' \\
542 \textbf{nitpick} \\[2\smallskipamount]
543 \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
544 \hbox{}\qquad Free variables: \nopagebreak \\
545 \hbox{}\qquad\qquad $\textit{xs} = []$ \\
546 \hbox{}\qquad\qquad $\textit{y} = a_3$
549 To see why the counterexample is genuine, we enable \textit{show\_consts}
550 and \textit{show\_\allowbreak datatypes}:
553 {\slshape Datatype:} \\
554 \hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_3, a_3],\, [a_3],\, \unr\}$ \\
555 {\slshape Constants:} \\
556 \hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_3, a_3],\> [a_3, a_3] := \unk,\> [a_3] := \unk)$ \\
557 \hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_3, a_3] := a_3,\> [a_3] := a_3)$
560 Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value,
563 The second constant, $\lambda x_1.\; x_1 \mathbin{@} [y, y]$, is simply the
564 append operator whose second argument is fixed to be $[y, y]$. Appending $[a_3,
565 a_3]$ to $[a_3]$ would normally give $[a_3, a_3, a_3]$, but this value is not
566 representable in the subset of $'a$~\textit{list} considered by Nitpick, which
567 is shown under the ``Datatype'' heading; hence the result is $\unk$. Similarly,
568 appending $[a_3, a_3]$ to itself gives $\unk$.
570 Given \textit{card}~$'a = 3$ and \textit{card}~$'a~\textit{list} = 3$, Nitpick
571 considers the following subsets:
573 \kern-.5\smallskipamount %% TYPESETTING
577 $\{[],\, [a_1],\, [a_2]\}$; \\
578 $\{[],\, [a_1],\, [a_3]\}$; \\
579 $\{[],\, [a_2],\, [a_3]\}$; \\
580 $\{[],\, [a_1],\, [a_1, a_1]\}$; \\
581 $\{[],\, [a_1],\, [a_2, a_1]\}$; \\
582 $\{[],\, [a_1],\, [a_3, a_1]\}$; \\
583 $\{[],\, [a_2],\, [a_1, a_2]\}$; \\
584 $\{[],\, [a_2],\, [a_2, a_2]\}$; \\
585 $\{[],\, [a_2],\, [a_3, a_2]\}$; \\
586 $\{[],\, [a_3],\, [a_1, a_3]\}$; \\
587 $\{[],\, [a_3],\, [a_2, a_3]\}$; \\
588 $\{[],\, [a_3],\, [a_3, a_3]\}$.
592 \kern-2\smallskipamount %% TYPESETTING
594 All subterm-closed subsets of $'a~\textit{list}$ consisting of three values
595 are listed and only those. As an example of a non-subterm-closed subset,
596 consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_3]\}$, and observe
597 that $[a_1, a_3]$ (i.e., $a_1 \mathbin{\#} [a_3]$) has $[a_3] \notin
598 \mathcal{S}$ as a subterm.
600 Here's another m\"ochtegern-lemma that Nitpick can refute without a blink:
603 \textbf{lemma} ``$\lbrakk \textit{length}~\textit{xs} = 1;\> \textit{length}~\textit{ys} = 1
604 \rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$''
606 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
607 \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
608 \hbox{}\qquad Free variables: \nopagebreak \\
609 \hbox{}\qquad\qquad $\textit{xs} = [a_2]$ \\
610 \hbox{}\qquad\qquad $\textit{ys} = [a_3]$ \\
611 \hbox{}\qquad Datatypes: \\
612 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
613 \hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_3],\, [a_2],\, \unr\}$
616 Because datatypes are approximated using a three-valued logic, there is usually
617 no need to systematically enumerate cardinalities: If Nitpick cannot find a
618 genuine counterexample for \textit{card}~$'a~\textit{list}$~= 10, it is very
619 unlikely that one could be found for smaller cardinalities.
621 \subsection{Typedefs, Records, Rationals, and Reals}
622 \label{typedefs-records-rationals-and-reals}
624 Nitpick generally treats types declared using \textbf{typedef} as datatypes
625 whose single constructor is the corresponding \textit{Abs\_\kern.1ex} function.
629 \textbf{typedef}~\textit{three} = ``$\{0\Colon\textit{nat},\, 1,\, 2\}$'' \\
630 \textbf{by}~\textit{blast} \\[2\smallskipamount]
631 \textbf{definition}~$A \mathbin{\Colon} \textit{three}$ \textbf{where} ``\kern-.1em$A \,\equiv\, \textit{Abs\_\allowbreak three}~0$'' \\
632 \textbf{definition}~$B \mathbin{\Colon} \textit{three}$ \textbf{where} ``$B \,\equiv\, \textit{Abs\_three}~1$'' \\
633 \textbf{definition}~$C \mathbin{\Colon} \textit{three}$ \textbf{where} ``$C \,\equiv\, \textit{Abs\_three}~2$'' \\[2\smallskipamount]
634 \textbf{lemma} ``$\lbrakk P~A;\> P~B\rbrakk \,\Longrightarrow\, P~x$'' \\
635 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
636 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
637 \hbox{}\qquad Free variables: \nopagebreak \\
638 \hbox{}\qquad\qquad $P = \{\Abs{1},\, \Abs{0}\}$ \\
639 \hbox{}\qquad\qquad $x = \Abs{2}$ \\
640 \hbox{}\qquad Datatypes: \\
641 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
642 \hbox{}\qquad\qquad $\textit{three} = \{\Abs{2},\, \Abs{1},\, \Abs{0},\, \unr\}$
646 In the output above, $\Abs{n}$ abbreviates $\textit{Abs\_three}~n$.
649 Records, which are implemented as \textbf{typedef}s behind the scenes, are
650 handled in much the same way:
653 \textbf{record} \textit{point} = \\
654 \hbox{}\quad $\textit{Xcoord} \mathbin{\Colon} \textit{int}$ \\
655 \hbox{}\quad $\textit{Ycoord} \mathbin{\Colon} \textit{int}$ \\[2\smallskipamount]
656 \textbf{lemma} ``$\textit{Xcoord}~(p\Colon\textit{point}) = \textit{Xcoord}~(q\Colon\textit{point})$'' \\
657 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
658 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
659 \hbox{}\qquad Free variables: \nopagebreak \\
660 \hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
661 \hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
662 \hbox{}\qquad Datatypes: \\
663 \hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, \unr\}$ \\
664 \hbox{}\qquad\qquad $\textit{point} = \{\lparr\textit{Xcoord} = 1,\>
665 \textit{Ycoord} = 1\rparr,\> \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr,\, \unr\}$\kern-1pt %% QUIET
668 Finally, Nitpick provides rudimentary support for rationals and reals using a
672 \textbf{lemma} ``$4 * x + 3 * (y\Colon\textit{real}) \not= 1/2$'' \\
673 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
674 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
675 \hbox{}\qquad Free variables: \nopagebreak \\
676 \hbox{}\qquad\qquad $x = 1/2$ \\
677 \hbox{}\qquad\qquad $y = -1/2$ \\
678 \hbox{}\qquad Datatypes: \\
679 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, 3,\, 4,\, 5,\, 6,\, 7,\, \unr\}$ \\
680 \hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, 2,\, 3,\, 4,\, -3,\, -2,\, -1,\, \unr\}$ \\
681 \hbox{}\qquad\qquad $\textit{real} = \{1,\, 0,\, 4,\, -3/2,\, 3,\, 2,\, 1/2,\, -1/2,\, \unr\}$
684 \subsection{Inductive and Coinductive Predicates}
685 \label{inductive-and-coinductive-predicates}
687 Inductively defined predicates (and sets) are particularly problematic for
688 counterexample generators. They can make Quickcheck~\cite{berghofer-nipkow-2004}
689 loop forever and Refute~\cite{weber-2008} run out of resources. The crux of
690 the problem is that they are defined using a least fixed point construction.
692 Nitpick's philosophy is that not all inductive predicates are equal. Consider
693 the \textit{even} predicate below:
696 \textbf{inductive}~\textit{even}~\textbf{where} \\
697 ``\textit{even}~0'' $\,\mid$ \\
698 ``\textit{even}~$n\,\Longrightarrow\, \textit{even}~(\textit{Suc}~(\textit{Suc}~n))$''
701 This predicate enjoys the desirable property of being well-founded, which means
702 that the introduction rules don't give rise to infinite chains of the form
705 $\cdots\,\Longrightarrow\, \textit{even}~k''
706 \,\Longrightarrow\, \textit{even}~k'
707 \,\Longrightarrow\, \textit{even}~k.$
710 For \textit{even}, this is obvious: Any chain ending at $k$ will be of length
714 $\textit{even}~0\,\Longrightarrow\, \textit{even}~2\,\Longrightarrow\, \cdots
715 \,\Longrightarrow\, \textit{even}~(k - 2)
716 \,\Longrightarrow\, \textit{even}~k.$
719 Wellfoundedness is desirable because it enables Nitpick to use a very efficient
720 fixed point computation.%
721 \footnote{If an inductive predicate is
722 well-founded, then it has exactly one fixed point, which is simultaneously the
723 least and the greatest fixed point. In these circumstances, the computation of
724 the least fixed point amounts to the computation of an arbitrary fixed point,
725 which can be performed using a straightforward recursive equation.}
726 Moreover, Nitpick can prove wellfoundedness of most well-founded predicates,
727 just as Isabelle's \textbf{function} package usually discharges termination
728 proof obligations automatically.
730 Let's try an example:
733 \textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
734 \textbf{nitpick}~[\textit{card nat}~= 100,\, \textit{verbose}] \\[2\smallskipamount]
735 \slshape The inductive predicate ``\textit{even}'' was proved well-founded.
736 Nitpick can compute it efficiently. \\[2\smallskipamount]
738 \hbox{}\qquad \textit{card nat}~= 100. \\[2\smallskipamount]
739 Nitpick found a potential counterexample for \textit{card nat}~= 100: \\[2\smallskipamount]
740 \hbox{}\qquad Empty assignment \\[2\smallskipamount]
741 Nitpick could not find a better counterexample. \\[2\smallskipamount]
745 No genuine counterexample is possible because Nitpick cannot rule out the
746 existence of a natural number $n \ge 100$ such that both $\textit{even}~n$ and
747 $\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the
748 existential quantifier:
751 \textbf{lemma} ``$\exists n \mathbin{\le} 99.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
752 \textbf{nitpick}~[\textit{card nat}~= 100] \\[2\smallskipamount]
753 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
754 \hbox{}\qquad Empty assignment
757 So far we were blessed by the wellfoundedness of \textit{even}. What happens if
758 we use the following definition instead?
761 \textbf{inductive} $\textit{even}'$ \textbf{where} \\
762 ``$\textit{even}'~(0{\Colon}\textit{nat})$'' $\,\mid$ \\
763 ``$\textit{even}'~2$'' $\,\mid$ \\
764 ``$\lbrakk\textit{even}'~m;\> \textit{even}'~n\rbrakk \,\Longrightarrow\, \textit{even}'~(m + n)$''
767 This definition is not well-founded: From $\textit{even}'~0$ and
768 $\textit{even}'~0$, we can derive that $\textit{even}'~0$. Nonetheless, the
769 predicates $\textit{even}$ and $\textit{even}'$ are equivalent.
771 Let's check a property involving $\textit{even}'$. To make up for the
772 foreseeable computational hurdles entailed by non-wellfoundedness, we decrease
773 \textit{nat}'s cardinality to a mere 10:
776 \textbf{lemma}~``$\exists n \in \{0, 2, 4, 6, 8\}.\;
777 \lnot\;\textit{even}'~n$'' \\
778 \textbf{nitpick}~[\textit{card nat}~= 10,\, \textit{verbose},\, \textit{show\_consts}] \\[2\smallskipamount]
780 The inductive predicate ``$\textit{even}'\!$'' could not be proved well-founded.
781 Nitpick might need to unroll it. \\[2\smallskipamount]
783 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 0; \\
784 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 1; \\
785 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2; \\
786 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 4; \\
787 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 8; \\
788 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 9. \\[2\smallskipamount]
789 Nitpick found a counterexample for \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2: \\[2\smallskipamount]
790 \hbox{}\qquad Constant: \nopagebreak \\
791 \hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t]
792 & 2 := \{0, 2, 4, 6, 8, 1^\Q, 3^\Q, 5^\Q, 7^\Q, 9^\Q\}, \\[-2pt]
793 & 1 := \{0, 2, 4, 1^\Q, 3^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\}, \\[-2pt]
794 & 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\[2\smallskipamount]
798 Nitpick's output is very instructive. First, it tells us that the predicate is
799 unrolled, meaning that it is computed iteratively from the empty set. Then it
800 lists six scopes specifying different bounds on the numbers of iterations:\ 0,
803 The output also shows how each iteration contributes to $\textit{even}'$. The
804 notation $\lambda i.\; \textit{even}'$ indicates that the value of the
805 predicate depends on an iteration counter. Iteration 0 provides the basis
806 elements, $0$ and $2$. Iteration 1 contributes $4$ ($= 2 + 2$). Iteration 2
807 throws $6$ ($= 2 + 4 = 4 + 2$) and $8$ ($= 4 + 4$) into the mix. Further
808 iterations would not contribute any new elements.
810 Some values are marked with superscripted question
811 marks~(`\lower.2ex\hbox{$^\Q$}'). These are the elements for which the
812 predicate evaluates to $\unk$. Thus, $\textit{even}'$ evaluates to either
813 \textit{True} or $\unk$, never \textit{False}.
815 When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, and 24
816 iterations. However, these numbers are bounded by the cardinality of the
817 predicate's domain. With \textit{card~nat}~= 10, no more than 9 iterations are
818 ever needed to compute the value of a \textit{nat} predicate. You can specify
819 the number of iterations using the \textit{iter} option, as explained in
820 \S\ref{scope-of-search}.
822 In the next formula, $\textit{even}'$ occurs both positively and negatively:
825 \textbf{lemma} ``$\textit{even}'~(n - 2) \,\Longrightarrow\, \textit{even}'~n$'' \\
826 \textbf{nitpick} [\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
827 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
828 \hbox{}\qquad Free variable: \nopagebreak \\
829 \hbox{}\qquad\qquad $n = 1$ \\
830 \hbox{}\qquad Constants: \nopagebreak \\
831 \hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t]
832 & 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\
833 \hbox{}\qquad\qquad $\textit{even}' \subseteq \{0, 2, 4, 6, 8, \unr\}$
836 Notice the special constraint $\textit{even}' \subseteq \{0,\, 2,\, 4,\, 6,\,
837 8,\, \unr\}$ in the output, whose right-hand side represents an arbitrary
838 fixed point (not necessarily the least one). It is used to falsify
839 $\textit{even}'~n$. In contrast, the unrolled predicate is used to satisfy
840 $\textit{even}'~(n - 2)$.
842 Coinductive predicates are handled dually. For example:
845 \textbf{coinductive} \textit{nats} \textbf{where} \\
846 ``$\textit{nats}~(x\Colon\textit{nat}) \,\Longrightarrow\, \textit{nats}~x$'' \\[2\smallskipamount]
847 \textbf{lemma} ``$\textit{nats} = \{0, 1, 2, 3, 4\}$'' \\
848 \textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
849 \slshape Nitpick found a counterexample:
850 \\[2\smallskipamount]
851 \hbox{}\qquad Constants: \nopagebreak \\
852 \hbox{}\qquad\qquad $\lambda i.\; \textit{nats} = \undef(0 := \{\!\begin{aligned}[t]
853 & 0^\Q, 1^\Q, 2^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q, \\[-2pt]
854 & \unr\})\end{aligned}$ \\
855 \hbox{}\qquad\qquad $nats \supseteq \{9, 5^\Q, 6^\Q, 7^\Q, 8^\Q, \unr\}$
858 As a special case, Nitpick uses Kodkod's transitive closure operator to encode
859 negative occurrences of non-well-founded ``linear inductive predicates,'' i.e.,
860 inductive predicates for which each the predicate occurs in at most one
861 assumption of each introduction rule. For example:
864 \textbf{inductive} \textit{odd} \textbf{where} \\
865 ``$\textit{odd}~1$'' $\,\mid$ \\
866 ``$\lbrakk \textit{odd}~m;\>\, \textit{even}~n\rbrakk \,\Longrightarrow\, \textit{odd}~(m + n)$'' \\[2\smallskipamount]
867 \textbf{lemma}~``$\textit{odd}~n \,\Longrightarrow\, \textit{odd}~(n - 2)$'' \\
868 \textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
869 \slshape Nitpick found a counterexample:
870 \\[2\smallskipamount]
871 \hbox{}\qquad Free variable: \nopagebreak \\
872 \hbox{}\qquad\qquad $n = 1$ \\
873 \hbox{}\qquad Constants: \nopagebreak \\
874 \hbox{}\qquad\qquad $\textit{even} = \{0, 2, 4, 6, 8, \unr\}$ \\
875 \hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = \{1, \unr\}$ \\
876 \hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \!
878 & \{(0, 0), (0, 2), (0, 4), (0, 6), (0, 8), (1, 1), (1, 3), (1, 5), \\[-2pt]
879 & \phantom{\{} (1, 7), (1, 9), (2, 2), (2, 4), (2, 6), (2, 8), (3, 3),
881 & \phantom{\{} (3, 7), (3, 9), (4, 4), (4, 6), (4, 8), (5, 5), (5, 7), (5, 9), \\[-2pt]
882 & \phantom{\{} (6, 6), (6, 8), (7, 7), (7, 9), (8, 8), (9, 9), \unr\}\end{aligned}$ \\
883 \hbox{}\qquad\qquad $\textit{odd} \subseteq \{1, 3, 5, 7, 9, 8^\Q, \unr\}$
887 In the output, $\textit{odd}_{\textrm{base}}$ represents the base elements and
888 $\textit{odd}_{\textrm{step}}$ is a transition relation that computes new
889 elements from known ones. The set $\textit{odd}$ consists of all the values
890 reachable through the reflexive transitive closure of
891 $\textit{odd}_{\textrm{step}}$ starting with any element from
892 $\textit{odd}_{\textrm{base}}$, namely 1, 3, 5, 7, and 9. Using Kodkod's
893 transitive closure to encode linear predicates is normally either more thorough
894 or more efficient than unrolling (depending on the value of \textit{iter}), but
895 for those cases where it isn't you can disable it by passing the
896 \textit{dont\_star\_linear\_preds} option.
898 \subsection{Coinductive Datatypes}
899 \label{coinductive-datatypes}
901 While Isabelle regrettably lacks a high-level mechanism for defining coinductive
902 datatypes, the \textit{Coinductive\_List} theory provides a coinductive ``lazy
903 list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick supports
904 these lazy lists seamlessly and provides a hook, described in
905 \S\ref{registration-of-coinductive-datatypes}, to register custom coinductive
908 (Co)intuitively, a coinductive datatype is similar to an inductive datatype but
909 allows infinite objects. Thus, the infinite lists $\textit{ps}$ $=$ $[a, a, a,
910 \ldots]$, $\textit{qs}$ $=$ $[a, b, a, b, \ldots]$, and $\textit{rs}$ $=$ $[0,
911 1, 2, 3, \ldots]$ can be defined as lazy lists using the
912 $\textit{LNil}\mathbin{\Colon}{'}a~\textit{llist}$ and
913 $\textit{LCons}\mathbin{\Colon}{'}a \mathbin{\Rightarrow} {'}a~\textit{llist}
914 \mathbin{\Rightarrow} {'}a~\textit{llist}$ constructors.
916 Although it is otherwise no friend of infinity, Nitpick can find counterexamples
917 involving cyclic lists such as \textit{ps} and \textit{qs} above as well as
921 \textbf{lemma} ``$\textit{xs} \not= \textit{LCons}~a~\textit{xs}$'' \\
922 \textbf{nitpick} \\[2\smallskipamount]
923 \slshape Nitpick found a counterexample for {\itshape card}~$'a$ = 1: \\[2\smallskipamount]
924 \hbox{}\qquad Free variables: \nopagebreak \\
925 \hbox{}\qquad\qquad $\textit{a} = a_1$ \\
926 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$
929 The notation $\textrm{THE}~\omega.\; \omega = t(\omega)$ stands
930 for the infinite term $t(t(t(\ldots)))$. Hence, \textit{xs} is simply the
931 infinite list $[a_1, a_1, a_1, \ldots]$.
933 The next example is more interesting:
936 \textbf{lemma}~``$\lbrakk\textit{xs} = \textit{LCons}~a~\textit{xs};\>\,
937 \textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
938 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
939 \slshape The type ``\kern1pt$'a$'' passed the monotonicity test. Nitpick might be able to skip
940 some scopes. \\[2\smallskipamount]
942 \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list}$''~= 1,
943 and \textit{bisim\_depth}~= 0. \\
944 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
945 \hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} ``\kern1pt$'a~\textit{list}$''~= 8,
946 and \textit{bisim\_depth}~= 7. \\[2\smallskipamount]
947 Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
948 \textit{card}~``\kern1pt$'a~\textit{list}$''~= 2, and \textit{bisim\_\allowbreak
950 \\[2\smallskipamount]
951 \hbox{}\qquad Free variables: \nopagebreak \\
952 \hbox{}\qquad\qquad $\textit{a} = a_2$ \\
953 \hbox{}\qquad\qquad $\textit{b} = a_1$ \\
954 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega$ \\
955 \hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_1~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega)$ \\[2\smallskipamount]
959 The lazy list $\textit{xs}$ is simply $[a_2, a_2, a_2, \ldots]$, whereas
960 $\textit{ys}$ is $[a_1, a_2, a_2, a_2, \ldots]$, i.e., a lasso-shaped list with
961 $[a_1]$ as its stem and $[a_2]$ as its cycle. In general, the list segment
962 within the scope of the {THE} binder corresponds to the lasso's cycle, whereas
963 the segment leading to the binder is the stem.
965 A salient property of coinductive datatypes is that two objects are considered
966 equal if and only if they lead to the same observations. For example, the lazy
967 lists $\textrm{THE}~\omega.\; \omega =
968 \textit{LCons}~a~(\textit{LCons}~b~\omega)$ and
969 $\textit{LCons}~a~(\textrm{THE}~\omega.\; \omega =
970 \textit{LCons}~b~(\textit{LCons}~a~\omega))$ are identical, because both lead
971 to the sequence of observations $a$, $b$, $a$, $b$, \hbox{\ldots} (or,
972 equivalently, both encode the infinite list $[a, b, a, b, \ldots]$). This
973 concept of equality for coinductive datatypes is called bisimulation and is
974 defined coinductively.
976 Internally, Nitpick encodes the coinductive bisimilarity predicate as part of
977 the Kodkod problem to ensure that distinct objects lead to different
978 observations. This precaution is somewhat expensive and often unnecessary, so it
979 can be disabled by setting the \textit{bisim\_depth} option to $-1$. The
980 bisimilarity check is then performed \textsl{after} the counterexample has been
981 found to ensure correctness. If this after-the-fact check fails, the
982 counterexample is tagged as ``likely genuine'' and Nitpick recommends to try
983 again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the
984 check for the previous example saves approximately 150~milli\-seconds; the speed
985 gains can be more significant for larger scopes.
987 The next formula illustrates the need for bisimilarity (either as a Kodkod
988 predicate or as an after-the-fact check) to prevent spurious counterexamples:
991 \textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
992 \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
993 \textbf{nitpick} [\textit{bisim\_depth} = $-1$,\, \textit{show\_datatypes}] \\[2\smallskipamount]
994 \slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
995 \hbox{}\qquad Free variables: \nopagebreak \\
996 \hbox{}\qquad\qquad $a = a_2$ \\
997 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
998 \textit{LCons}~a_2~\omega$ \\
999 \hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega$ \\
1000 \hbox{}\qquad Codatatype:\strut \nopagebreak \\
1001 \hbox{}\qquad\qquad $'a~\textit{llist} =
1002 \{\!\begin{aligned}[t]
1003 & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega, \\[-2pt]
1004 & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega,\> \unr\}\end{aligned}$
1005 \\[2\smallskipamount]
1006 Try again with ``\textit{bisim\_depth}'' set to a nonnegative value to confirm
1007 that the counterexample is genuine. \\[2\smallskipamount]
1008 {\upshape\textbf{nitpick}} \\[2\smallskipamount]
1009 \slshape Nitpick found no counterexample.
1012 In the first \textbf{nitpick} invocation, the after-the-fact check discovered
1013 that the two known elements of type $'a~\textit{llist}$ are bisimilar.
1015 A compromise between leaving out the bisimilarity predicate from the Kodkod
1016 problem and performing the after-the-fact check is to specify a lower
1017 nonnegative \textit{bisim\_depth} value than the default one provided by
1018 Nitpick. In general, a value of $K$ means that Nitpick will require all lists to
1019 be distinguished from each other by their prefixes of length $K$. Be aware that
1020 setting $K$ to a too low value can overconstrain Nitpick, preventing it from
1021 finding any counterexamples.
1026 Nitpick normally maps function and product types directly to the corresponding
1027 Kodkod concepts. As a consequence, if $'a$ has cardinality 3 and $'b$ has
1028 cardinality 4, then $'a \times {'}b$ has cardinality 12 ($= 4 \times 3$) and $'a
1029 \Rightarrow {'}b$ has cardinality 64 ($= 4^3$). In some circumstances, it pays
1030 off to treat these types in the same way as plain datatypes, by approximating
1031 them by a subset of a given cardinality. This technique is called ``boxing'' and
1032 is particularly useful for functions passed as arguments to other functions, for
1033 high-arity functions, and for large tuples. Under the hood, boxing involves
1034 wrapping occurrences of the types $'a \times {'}b$ and $'a \Rightarrow {'}b$ in
1035 isomorphic datatypes, as can be seen by enabling the \textit{debug} option.
1037 To illustrate boxing, we consider a formalization of $\lambda$-terms represented
1038 using de Bruijn's notation:
1041 \textbf{datatype} \textit{tm} = \textit{Var}~\textit{nat}~$\mid$~\textit{Lam}~\textit{tm} $\mid$ \textit{App~tm~tm}
1044 The $\textit{lift}~t~k$ function increments all variables with indices greater
1045 than or equal to $k$ by one:
1048 \textbf{primrec} \textit{lift} \textbf{where} \\
1049 ``$\textit{lift}~(\textit{Var}~j)~k = \textit{Var}~(\textrm{if}~j < k~\textrm{then}~j~\textrm{else}~j + 1)$'' $\mid$ \\
1050 ``$\textit{lift}~(\textit{Lam}~t)~k = \textit{Lam}~(\textit{lift}~t~(k + 1))$'' $\mid$ \\
1051 ``$\textit{lift}~(\textit{App}~t~u)~k = \textit{App}~(\textit{lift}~t~k)~(\textit{lift}~u~k)$''
1054 The $\textit{loose}~t~k$ predicate returns \textit{True} if and only if
1055 term $t$ has a loose variable with index $k$ or more:
1058 \textbf{primrec}~\textit{loose} \textbf{where} \\
1059 ``$\textit{loose}~(\textit{Var}~j)~k = (j \ge k)$'' $\mid$ \\
1060 ``$\textit{loose}~(\textit{Lam}~t)~k = \textit{loose}~t~(\textit{Suc}~k)$'' $\mid$ \\
1061 ``$\textit{loose}~(\textit{App}~t~u)~k = (\textit{loose}~t~k \mathrel{\lor} \textit{loose}~u~k)$''
1064 Next, the $\textit{subst}~\sigma~t$ function applies the substitution $\sigma$
1068 \textbf{primrec}~\textit{subst} \textbf{where} \\
1069 ``$\textit{subst}~\sigma~(\textit{Var}~j) = \sigma~j$'' $\mid$ \\
1070 ``$\textit{subst}~\sigma~(\textit{Lam}~t) = {}$\phantom{''} \\
1071 \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$ \\
1072 ``$\textit{subst}~\sigma~(\textit{App}~t~u) = \textit{App}~(\textit{subst}~\sigma~t)~(\textit{subst}~\sigma~u)$''
1075 A substitution is a function that maps variable indices to terms. Observe that
1076 $\sigma$ is a function passed as argument and that Nitpick can't optimize it
1077 away, because the recursive call for the \textit{Lam} case involves an altered
1078 version. Also notice the \textit{lift} call, which increments the variable
1079 indices when moving under a \textit{Lam}.
1081 A reasonable property to expect of substitution is that it should leave closed
1082 terms unchanged. Alas, even this simple property does not hold:
1085 \textbf{lemma}~``$\lnot\,\textit{loose}~t~0 \,\Longrightarrow\, \textit{subst}~\sigma~t = t$'' \\
1086 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
1088 Trying 8 scopes: \nopagebreak \\
1089 \hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 1; \\
1090 \hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 2; \\
1091 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1092 \hbox{}\qquad \textit{card~nat}~= 8, \textit{card tm}~= 8, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 8. \\[2\smallskipamount]
1093 Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6,
1094 and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm}$''~= 6: \\[2\smallskipamount]
1095 \hbox{}\qquad Free variables: \nopagebreak \\
1096 \hbox{}\qquad\qquad $\sigma = \undef(\!\begin{aligned}[t]
1097 & 0 := \textit{Var}~0,\>
1098 1 := \textit{Var}~0,\>
1099 2 := \textit{Var}~0, \\[-2pt]
1100 & 3 := \textit{Var}~0,\>
1101 4 := \textit{Var}~0,\>
1102 5 := \textit{Var}~0)\end{aligned}$ \\
1103 \hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount]
1104 Total time: $4679$ ms.
1107 Using \textit{eval}, we find out that $\textit{subst}~\sigma~t =
1108 \textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional
1109 $\lambda$-term notation, $t$~is
1110 $\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is $\lambda x\, y.\> y$.
1111 The bug is in \textit{subst}: The $\textit{lift}~(\sigma~m)~1$ call should be
1112 replaced with $\textit{lift}~(\sigma~m)~0$.
1114 An interesting aspect of Nitpick's verbose output is that it assigned inceasing
1115 cardinalities from 1 to 8 to the type $\textit{nat} \Rightarrow \textit{tm}$.
1116 For the formula of interest, knowing 6 values of that type was enough to find
1117 the counterexample. Without boxing, $46\,656$ ($= 6^6$) values must be
1118 considered, a hopeless undertaking:
1121 \textbf{nitpick} [\textit{dont\_box}] \\[2\smallskipamount]
1122 {\slshape Nitpick ran out of time after checking 4 of 8 scopes.}
1126 Boxing can be enabled or disabled globally or on a per-type basis using the
1127 \textit{box} option. Moreover, setting the cardinality of a function or
1128 product type implicitly enables boxing for that type. Nitpick usually performs
1129 reasonable choices about which types should be boxed, but option tweaking
1134 \subsection{Scope Monotonicity}
1135 \label{scope-monotonicity}
1137 The \textit{card} option (together with \textit{iter}, \textit{bisim\_depth},
1138 and \textit{max}) controls which scopes are actually tested. In general, to
1139 exhaust all models below a certain cardinality bound, the number of scopes that
1140 Nitpick must consider increases exponentially with the number of type variables
1141 (and \textbf{typedecl}'d types) occurring in the formula. Given the default
1142 cardinality specification of 1--8, no fewer than $8^4 = 4096$ scopes must be
1143 considered for a formula involving $'a$, $'b$, $'c$, and $'d$.
1145 Fortunately, many formulas exhibit a property called \textsl{scope
1146 monotonicity}, meaning that if the formula is falsifiable for a given scope,
1147 it is also falsifiable for all larger scopes \cite[p.~165]{jackson-2006}.
1149 Consider the formula
1152 \textbf{lemma}~``$\textit{length~xs} = \textit{length~ys} \,\Longrightarrow\, \textit{rev}~(\textit{zip~xs~ys}) = \textit{zip~xs}~(\textit{rev~ys})$''
1155 where \textit{xs} is of type $'a~\textit{list}$ and \textit{ys} is of type
1156 $'b~\textit{list}$. A priori, Nitpick would need to consider 512 scopes to
1157 exhaust the specification \textit{card}~= 1--8. However, our intuition tells us
1158 that any counterexample found with a small scope would still be a counterexample
1159 in a larger scope---by simply ignoring the fresh $'a$ and $'b$ values provided
1160 by the larger scope. Nitpick comes to the same conclusion after a careful
1161 inspection of the formula and the relevant definitions:
1164 \textbf{nitpick}~[\textit{verbose}] \\[2\smallskipamount]
1166 The types ``\kern1pt$'a$'' and ``\kern1pt$'b$'' passed the monotonicity test.
1167 Nitpick might be able to skip some scopes.
1168 \\[2\smallskipamount]
1170 \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1,
1171 \textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$
1172 \textit{list}''~= 1, \\
1173 \hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 1, and
1174 \textit{card} ``\kern1pt$'b$ \textit{list}''~= 1. \\
1175 \hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2,
1176 \textit{card} \textit{nat}~= 2, \textit{card} ``$('a \times {'}b)$
1177 \textit{list}''~= 2, \\
1178 \hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 2, and
1179 \textit{card} ``\kern1pt$'b$ \textit{list}''~= 2. \\
1180 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1181 \hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} $'b$~= 8,
1182 \textit{card} \textit{nat}~= 8, \textit{card} ``$('a \times {'}b)$
1183 \textit{list}''~= 8, \\
1184 \hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 8, and
1185 \textit{card} ``\kern1pt$'b$ \textit{list}''~= 8.
1186 \\[2\smallskipamount]
1187 Nitpick found a counterexample for
1188 \textit{card} $'a$~= 5, \textit{card} $'b$~= 5,
1189 \textit{card} \textit{nat}~= 5, \textit{card} ``$('a \times {'}b)$
1190 \textit{list}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list}''~= 5, and
1191 \textit{card} ``\kern1pt$'b$ \textit{list}''~= 5:
1192 \\[2\smallskipamount]
1193 \hbox{}\qquad Free variables: \nopagebreak \\
1194 \hbox{}\qquad\qquad $\textit{xs} = [a_4, a_5]$ \\
1195 \hbox{}\qquad\qquad $\textit{ys} = [b_3, b_3]$ \\[2\smallskipamount]
1196 Total time: 1636 ms.
1199 In theory, it should be sufficient to test a single scope:
1202 \textbf{nitpick}~[\textit{card}~= 8]
1205 However, this is often less efficient in practice and may lead to overly complex
1208 If the monotonicity check fails but we believe that the formula is monotonic (or
1209 we don't mind missing some counterexamples), we can pass the
1210 \textit{mono} option. To convince yourself that this option is risky,
1211 simply consider this example from \S\ref{skolemization}:
1214 \textbf{lemma} ``$\exists g.\; \forall x\Colon 'b.~g~(f~x) = x
1215 \,\Longrightarrow\, \forall y\Colon {'}a.\; \exists x.~y = f~x$'' \\
1216 \textbf{nitpick} [\textit{mono}] \\[2\smallskipamount]
1217 {\slshape Nitpick found no counterexample.} \\[2\smallskipamount]
1218 \textbf{nitpick} \\[2\smallskipamount]
1220 Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\
1221 \hbox{}\qquad $\vdots$
1224 (It turns out the formula holds if and only if $\textit{card}~'a \le
1225 \textit{card}~'b$.) Although this is rarely advisable, the automatic
1226 monotonicity checks can be disabled by passing \textit{non\_mono}
1227 (\S\ref{optimizations}).
1229 As insinuated in \S\ref{natural-numbers-and-integers} and
1230 \S\ref{inductive-datatypes}, \textit{nat}, \textit{int}, and inductive datatypes
1231 are normally monotonic and treated as such. The same is true for record types,
1232 \textit{rat}, \textit{real}, and some \textbf{typedef}'d types. Thus, given the
1233 cardinality specification 1--8, a formula involving \textit{nat}, \textit{int},
1234 \textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
1235 consider only 8~scopes instead of $32\,768$.
1237 \section{Case Studies}
1238 \label{case-studies}
1240 As a didactic device, the previous section focused mostly on toy formulas whose
1241 validity can easily be assessed just by looking at the formula. We will now
1242 review two somewhat more realistic case studies that are within Nitpick's
1243 reach:\ a context-free grammar modeled by mutually inductive sets and a
1244 functional implementation of AA trees. The results presented in this
1245 section were produced with the following settings:
1248 \textbf{nitpick\_params} [\textit{max\_potential}~= 0,\, \textit{max\_threads} = 2]
1251 \subsection{A Context-Free Grammar}
1252 \label{a-context-free-grammar}
1254 Our first case study is taken from section 7.4 in the Isabelle tutorial
1255 \cite{isa-tutorial}. The following grammar, originally due to Hopcroft and
1256 Ullman, produces all strings with an equal number of $a$'s and $b$'s:
1259 \begin{tabular}{@{}r@{$\;\,$}c@{$\;\,$}l@{}}
1260 $S$ & $::=$ & $\epsilon \mid bA \mid aB$ \\
1261 $A$ & $::=$ & $aS \mid bAA$ \\
1262 $B$ & $::=$ & $bS \mid aBB$
1266 The intuition behind the grammar is that $A$ generates all string with one more
1267 $a$ than $b$'s and $B$ generates all strings with one more $b$ than $a$'s.
1269 The alphabet consists exclusively of $a$'s and $b$'s:
1272 \textbf{datatype} \textit{alphabet}~= $a$ $\mid$ $b$
1275 Strings over the alphabet are represented by \textit{alphabet list}s.
1276 Nonterminals in the grammar become sets of strings. The production rules
1277 presented above can be expressed as a mutually inductive definition:
1280 \textbf{inductive\_set} $S$ \textbf{and} $A$ \textbf{and} $B$ \textbf{where} \\
1281 \textit{R1}:\kern.4em ``$[] \in S$'' $\,\mid$ \\
1282 \textit{R2}:\kern.4em ``$w \in A\,\Longrightarrow\, b \mathbin{\#} w \in S$'' $\,\mid$ \\
1283 \textit{R3}:\kern.4em ``$w \in B\,\Longrightarrow\, a \mathbin{\#} w \in S$'' $\,\mid$ \\
1284 \textit{R4}:\kern.4em ``$w \in S\,\Longrightarrow\, a \mathbin{\#} w \in A$'' $\,\mid$ \\
1285 \textit{R5}:\kern.4em ``$w \in S\,\Longrightarrow\, b \mathbin{\#} w \in S$'' $\,\mid$ \\
1286 \textit{R6}:\kern.4em ``$\lbrakk v \in B;\> v \in B\rbrakk \,\Longrightarrow\, a \mathbin{\#} v \mathbin{@} w \in B$''
1289 The conversion of the grammar into the inductive definition was done manually by
1290 Joe Blow, an underpaid undergraduate student. As a result, some errors might
1293 Debugging faulty specifications is at the heart of Nitpick's \textsl{raison
1294 d'\^etre}. A good approach is to state desirable properties of the specification
1295 (here, that $S$ is exactly the set of strings over $\{a, b\}$ with as many $a$'s
1296 as $b$'s) and check them with Nitpick. If the properties are correctly stated,
1297 counterexamples will point to bugs in the specification. For our grammar
1298 example, we will proceed in two steps, separating the soundness and the
1299 completeness of the set $S$. First, soundness:
1302 \textbf{theorem}~\textit{S\_sound}: \\
1303 ``$w \in S \longrightarrow \textit{length}~[x\mathbin{\leftarrow} w.\; x = a] =
1304 \textit{length}~[x\mathbin{\leftarrow} w.\; x = b]$'' \\
1305 \textbf{nitpick} \\[2\smallskipamount]
1306 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1307 \hbox{}\qquad Free variable: \nopagebreak \\
1308 \hbox{}\qquad\qquad $w = [b]$
1311 It would seem that $[b] \in S$. How could this be? An inspection of the
1312 introduction rules reveals that the only rule with a right-hand side of the form
1313 $b \mathbin{\#} {\ldots} \in S$ that could have introduced $[b]$ into $S$ is
1317 ``$w \in S\,\Longrightarrow\, b \mathbin{\#} w \in S$''
1320 On closer inspection, we can see that this rule is wrong. To match the
1321 production $B ::= bS$, the second $S$ should be a $B$. We fix the typo and try
1325 \textbf{nitpick} \\[2\smallskipamount]
1326 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1327 \hbox{}\qquad Free variable: \nopagebreak \\
1328 \hbox{}\qquad\qquad $w = [a, a, b]$
1331 Some detective work is necessary to find out what went wrong here. To get $[a,
1332 a, b] \in S$, we need $[a, b] \in B$ by \textit{R3}, which in turn can only come
1336 ``$\lbrakk v \in B;\> v \in B\rbrakk \,\Longrightarrow\, a \mathbin{\#} v \mathbin{@} w \in B$''
1339 Now, this formula must be wrong: The same assumption occurs twice, and the
1340 variable $w$ is unconstrained. Clearly, one of the two occurrences of $v$ in
1341 the assumptions should have been a $w$.
1343 With the correction made, we don't get any counterexample from Nitpick. Let's
1344 move on and check completeness:
1347 \textbf{theorem}~\textit{S\_complete}: \\
1348 ``$\textit{length}~[x\mathbin{\leftarrow} w.\; x = a] =
1349 \textit{length}~[x\mathbin{\leftarrow} w.\; x = b]
1350 \longrightarrow w \in S$'' \\
1351 \textbf{nitpick} \\[2\smallskipamount]
1352 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1353 \hbox{}\qquad Free variable: \nopagebreak \\
1354 \hbox{}\qquad\qquad $w = [b, b, a, a]$
1357 Apparently, $[b, b, a, a] \notin S$, even though it has the same numbers of
1358 $a$'s and $b$'s. But since our inductive definition passed the soundness check,
1359 the introduction rules we have are probably correct. Perhaps we simply lack an
1360 introduction rule. Comparing the grammar with the inductive definition, our
1361 suspicion is confirmed: Joe Blow simply forgot the production $A ::= bAA$,
1362 without which the grammar cannot generate two or more $b$'s in a row. So we add
1366 ``$\lbrakk v \in A;\> w \in A\rbrakk \,\Longrightarrow\, b \mathbin{\#} v \mathbin{@} w \in A$''
1369 With this last change, we don't get any counterexamples from Nitpick for either
1370 soundness or completeness. We can even generalize our result to cover $A$ and
1374 \textbf{theorem} \textit{S\_A\_B\_sound\_and\_complete}: \\
1375 ``$w \in S \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b]$'' \\
1376 ``$w \in A \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] + 1$'' \\
1377 ``$w \in B \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] + 1$'' \\
1378 \textbf{nitpick} \\[2\smallskipamount]
1379 \slshape Nitpick found no counterexample.
1382 \subsection{AA Trees}
1385 AA trees are a kind of balanced trees discovered by Arne Andersson that provide
1386 similar performance to red-black trees, but with a simpler implementation
1387 \cite{andersson-1993}. They can be used to store sets of elements equipped with
1388 a total order $<$. We start by defining the datatype and some basic extractor
1392 \textbf{datatype} $'a$~\textit{tree} = $\Lambda$ $\mid$ $N$ ``\kern1pt$'a\Colon \textit{linorder}$'' \textit{nat} ``\kern1pt$'a$ \textit{tree}'' ``\kern1pt$'a$ \textit{tree}'' \\[2\smallskipamount]
1393 \textbf{primrec} \textit{data} \textbf{where} \\
1394 ``$\textit{data}~\Lambda = \undef$'' $\,\mid$ \\
1395 ``$\textit{data}~(N~x~\_~\_~\_) = x$'' \\[2\smallskipamount]
1396 \textbf{primrec} \textit{dataset} \textbf{where} \\
1397 ``$\textit{dataset}~\Lambda = \{\}$'' $\,\mid$ \\
1398 ``$\textit{dataset}~(N~x~\_~t~u) = \{x\} \cup \textit{dataset}~t \mathrel{\cup} \textit{dataset}~u$'' \\[2\smallskipamount]
1399 \textbf{primrec} \textit{level} \textbf{where} \\
1400 ``$\textit{level}~\Lambda = 0$'' $\,\mid$ \\
1401 ``$\textit{level}~(N~\_~k~\_~\_) = k$'' \\[2\smallskipamount]
1402 \textbf{primrec} \textit{left} \textbf{where} \\
1403 ``$\textit{left}~\Lambda = \Lambda$'' $\,\mid$ \\
1404 ``$\textit{left}~(N~\_~\_~t~\_) = t$'' \\[2\smallskipamount]
1405 \textbf{primrec} \textit{right} \textbf{where} \\
1406 ``$\textit{right}~\Lambda = \Lambda$'' $\,\mid$ \\
1407 ``$\textit{right}~(N~\_~\_~\_~u) = u$''
1410 The wellformedness criterion for AA trees is fairly complex. Wikipedia states it
1411 as follows \cite{wikipedia-2009-aa-trees}:
1413 \kern.2\parskip %% TYPESETTING
1416 Each node has a level field, and the following invariants must remain true for
1417 the tree to be valid:
1421 \kern-.4\parskip %% TYPESETTING
1426 \item[1.] The level of a leaf node is one.
1427 \item[2.] The level of a left child is strictly less than that of its parent.
1428 \item[3.] The level of a right child is less than or equal to that of its parent.
1429 \item[4.] The level of a right grandchild is strictly less than that of its grandparent.
1430 \item[5.] Every node of level greater than one must have two children.
1435 \kern.4\parskip %% TYPESETTING
1437 The \textit{wf} predicate formalizes this description:
1440 \textbf{primrec} \textit{wf} \textbf{where} \\
1441 ``$\textit{wf}~\Lambda = \textit{True}$'' $\,\mid$ \\
1442 ``$\textit{wf}~(N~\_~k~t~u) =$ \\
1443 \phantom{``}$(\textrm{if}~t = \Lambda~\textrm{then}$ \\
1444 \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))$ \\
1445 \phantom{``$($}$\textrm{else}$ \\
1446 \hbox{}\phantom{``$(\quad$}$\textit{wf}~t \mathrel{\land} \textit{wf}~u
1447 \mathrel{\land} u \not= \Lambda \mathrel{\land} \textit{level}~t < k
1448 \mathrel{\land} \textit{level}~u \le k$ \\
1449 \hbox{}\phantom{``$(\quad$}${\land}\; \textit{level}~(\textit{right}~u) < k)$''
1452 Rebalancing the tree upon insertion and removal of elements is performed by two
1453 auxiliary functions called \textit{skew} and \textit{split}, defined below:
1456 \textbf{primrec} \textit{skew} \textbf{where} \\
1457 ``$\textit{skew}~\Lambda = \Lambda$'' $\,\mid$ \\
1458 ``$\textit{skew}~(N~x~k~t~u) = {}$ \\
1459 \phantom{``}$(\textrm{if}~t \not= \Lambda \mathrel{\land} k =
1460 \textit{level}~t~\textrm{then}$ \\
1461 \phantom{``(\quad}$N~(\textit{data}~t)~k~(\textit{left}~t)~(N~x~k~
1462 (\textit{right}~t)~u)$ \\
1463 \phantom{``(}$\textrm{else}$ \\
1464 \phantom{``(\quad}$N~x~k~t~u)$''
1468 \textbf{primrec} \textit{split} \textbf{where} \\
1469 ``$\textit{split}~\Lambda = \Lambda$'' $\,\mid$ \\
1470 ``$\textit{split}~(N~x~k~t~u) = {}$ \\
1471 \phantom{``}$(\textrm{if}~u \not= \Lambda \mathrel{\land} k =
1472 \textit{level}~(\textit{right}~u)~\textrm{then}$ \\
1473 \phantom{``(\quad}$N~(\textit{data}~u)~(\textit{Suc}~k)~
1474 (N~x~k~t~(\textit{left}~u))~(\textit{right}~u)$ \\
1475 \phantom{``(}$\textrm{else}$ \\
1476 \phantom{``(\quad}$N~x~k~t~u)$''
1479 Performing a \textit{skew} or a \textit{split} should have no impact on the set
1480 of elements stored in the tree:
1483 \textbf{theorem}~\textit{dataset\_skew\_split}:\\
1484 ``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
1485 ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
1486 \textbf{nitpick} \\[2\smallskipamount]
1487 {\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
1490 Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
1491 should not alter the tree:
1494 \textbf{theorem}~\textit{wf\_skew\_split}:\\
1495 ``$\textit{wf}~t\,\Longrightarrow\, \textit{skew}~t = t$'' \\
1496 ``$\textit{wf}~t\,\Longrightarrow\, \textit{split}~t = t$'' \\
1497 \textbf{nitpick} \\[2\smallskipamount]
1498 {\slshape Nitpick found no counterexample.}
1501 Insertion is implemented recursively. It preserves the sort order:
1504 \textbf{primrec}~\textit{insort} \textbf{where} \\
1505 ``$\textit{insort}~\Lambda~x = N~x~1~\Lambda~\Lambda$'' $\,\mid$ \\
1506 ``$\textit{insort}~(N~y~k~t~u)~x =$ \\
1507 \phantom{``}$({*}~(\textit{split} \circ \textit{skew})~{*})~(N~y~k~(\textrm{if}~x < y~\textrm{then}~\textit{insort}~t~x~\textrm{else}~t)$ \\
1508 \phantom{``$({*}~(\textit{split} \circ \textit{skew})~{*})~(N~y~k~$}$(\textrm{if}~x > y~\textrm{then}~\textit{insort}~u~x~\textrm{else}~u))$''
1511 Notice that we deliberately commented out the application of \textit{skew} and
1512 \textit{split}. Let's see if this causes any problems:
1515 \textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
1516 \textbf{nitpick} \\[2\smallskipamount]
1517 \slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
1518 \hbox{}\qquad Free variables: \nopagebreak \\
1519 \hbox{}\qquad\qquad $t = N~a_3~1~\Lambda~\Lambda$ \\
1520 \hbox{}\qquad\qquad $x = a_4$ \\[2\smallskipamount]
1521 Hint: Maybe you forgot a type constraint?
1524 It's hard to see why this is a counterexample. The hint is of no help here. To
1525 improve readability, we will restrict the theorem to \textit{nat}, so that we
1526 don't need to look up the value of the $\textit{op}~{<}$ constant to find out
1527 which element is smaller than the other. In addition, we will tell Nitpick to
1528 display the value of $\textit{insort}~t~x$ using the \textit{eval} option. This
1532 \textbf{theorem} \textit{wf\_insort\_nat}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\
1533 \textbf{nitpick} [\textit{eval} = ``$\textit{insort}~t~x$''] \\[2\smallskipamount]
1534 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1535 \hbox{}\qquad Free variables: \nopagebreak \\
1536 \hbox{}\qquad\qquad $t = N~1~1~\Lambda~\Lambda$ \\
1537 \hbox{}\qquad\qquad $x = 0$ \\
1538 \hbox{}\qquad Evaluated term: \\
1539 \hbox{}\qquad\qquad $\textit{insort}~t~x = N~1~1~(N~0~1~\Lambda~\Lambda)~\Lambda$
1542 Nitpick's output reveals that the element $0$ was added as a left child of $1$,
1543 where both have a level of 1. This violates the second AA tree invariant, which
1544 states that a left child's level must be less than its parent's. This shouldn't
1545 come as a surprise, considering that we commented out the tree rebalancing code.
1546 Reintroducing the code seems to solve the problem:
1549 \textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
1550 \textbf{nitpick} \\[2\smallskipamount]
1551 {\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
1554 Insertion should transform the set of elements represented by the tree in the
1558 \textbf{theorem} \textit{dataset\_insort}:\kern.4em
1559 ``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
1560 \textbf{nitpick} \\[2\smallskipamount]
1561 {\slshape Nitpick ran out of time after checking 5 of 8 scopes.}
1564 We could continue like this and sketch a complete theory of AA trees without
1565 performing a single proof. Once the definitions and main theorems are in place
1566 and have been thoroughly tested using Nitpick, we could start working on the
1567 proofs. Developing theories this way usually saves time, because faulty theorems
1568 and definitions are discovered much earlier in the process.
1570 \section{Option Reference}
1571 \label{option-reference}
1573 \def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
1574 \def\qty#1{$\left<\textit{#1}\right>$}
1575 \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
1576 \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1577 \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1578 \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1579 \def\ops#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
1580 \def\opt#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
1581 \def\opu#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
1582 \def\opusmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
1584 Nitpick's behavior can be influenced by various options, which can be specified
1585 in brackets after the \textbf{nitpick} command. Default values can be set
1586 using \textbf{nitpick\_\allowbreak params}. For example:
1589 \textbf{nitpick\_params} [\textit{verbose}, \,\textit{timeout} = 60$\,s$]
1592 The options are categorized as follows:\ mode of operation
1593 (\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output
1594 format (\S\ref{output-format}), automatic counterexample checks
1595 (\S\ref{authentication}), optimizations
1596 (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
1598 The number of options can be overwhelming at first glance. Do not let that worry
1599 you: Nitpick's defaults have been chosen so that it almost always does the right
1600 thing, and the most important options have been covered in context in
1601 \S\ref{first-steps}.
1603 The descriptions below refer to the following syntactic quantities:
1606 \item[$\bullet$] \qtybf{string}: A string.
1607 \item[$\bullet$] \qtybf{bool}: \textit{true} or \textit{false}.
1608 \item[$\bullet$] \qtybf{bool\_or\_smart}: \textit{true}, \textit{false}, or \textit{smart}.
1609 \item[$\bullet$] \qtybf{int}: An integer. Negative integers are prefixed with a hyphen.
1610 \item[$\bullet$] \qtybf{int\_or\_smart}: An integer or \textit{smart}.
1611 \item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
1612 of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<midarrow\char`\>}.
1614 \item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
1615 \item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
1616 (milliseconds), or the keyword \textit{none} ($\infty$ years).
1617 \item[$\bullet$] \qtybf{const}: The name of a HOL constant.
1618 \item[$\bullet$] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
1619 \item[$\bullet$] \qtybf{term\_list}: A space-separated list of HOL terms (e.g.,
1620 ``$f~x$''~``$g~y$'').
1621 \item[$\bullet$] \qtybf{type}: A HOL type.
1624 Default values are indicated in square brackets. Boolean options have a negated
1625 counterpart (e.g., \textit{auto} vs.\ \textit{no\_auto}). When setting Boolean
1626 options, ``= \textit{true}'' may be omitted.
1628 \subsection{Mode of Operation}
1629 \label{mode-of-operation}
1632 \opfalse{auto}{no\_auto}
1633 Specifies whether Nitpick should be run automatically on newly entered theorems.
1634 For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}) and
1635 \textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
1636 \textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
1637 (\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
1638 disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
1639 \textit{auto\_timeout} (\S\ref{timeouts}) is used as the time limit instead of
1640 \textit{timeout} (\S\ref{timeouts}). The output is also more concise.
1643 {\small See also \textit{auto\_timeout} (\S\ref{timeouts}).}
1645 \optrue{blocking}{non\_blocking}
1646 Specifies whether the \textbf{nitpick} command should operate synchronously.
1647 The asynchronous (non-blocking) mode lets the user start proving the putative
1648 theorem while Nitpick looks for a counterexample, but it can also be more
1649 confusing. For technical reasons, automatic runs currently always block.
1652 {\small See also \textit{auto} (\S\ref{mode-of-operation}).}
1654 \optrue{falsify}{satisfy}
1655 Specifies whether Nitpick should look for falsifying examples (countermodels) or
1656 satisfying examples (models). This manual assumes throughout that
1657 \textit{falsify} is enabled.
1659 \opsmart{user\_axioms}{no\_user\_axioms}
1660 Specifies whether the user-defined axioms (specified using
1661 \textbf{axiomatization} and \textbf{axioms}) should be considered. If the option
1662 is set to \textit{smart}, Nitpick performs an ad hoc axiom selection based on
1663 the constants that occur in the formula to falsify. The option is implicitly set
1664 to \textit{true} for automatic runs.
1666 \textbf{Warning:} If the option is set to \textit{true}, Nitpick might
1667 nonetheless ignore some polymorphic axioms. Counterexamples generated under
1668 these conditions are tagged as ``likely genuine.'' The \textit{debug}
1669 (\S\ref{output-format}) option can be used to find out which axioms were
1673 {\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{assms}
1674 (\S\ref{mode-of-operation}), and \textit{debug} (\S\ref{output-format}).}
1676 \optrue{assms}{no\_assms}
1677 Specifies whether the relevant assumptions in structured proof should be
1678 considered. The option is implicitly enabled for automatic runs.
1681 {\small See also \textit{auto} (\S\ref{mode-of-operation})
1682 and \textit{user\_axioms} (\S\ref{mode-of-operation}).}
1684 \opfalse{overlord}{no\_overlord}
1685 Specifies whether Nitpick should put its temporary files in
1686 \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
1687 debugging Nitpick but also unsafe if several instances of the tool are run
1688 simultaneously. This option is disabled by default unless your home directory
1689 ends with \texttt{blanchet} or \texttt{blanchette}.
1690 %``I thought there was only one overlord.'' --- Tobias Nipkow
1693 {\small See also \textit{debug} (\S\ref{output-format}).}
1696 \subsection{Scope of Search}
1697 \label{scope-of-search}
1700 \opu{card}{type}{int\_seq}
1701 Specifies the sequence of cardinalities to use for a given type. For
1702 \textit{nat} and \textit{int}, the cardinality fully specifies the subset used
1703 to approximate the type. For example:
1705 $$\hbox{\begin{tabular}{@{}rll@{}}%
1706 \textit{card nat} = 4 & induces & $\{0,\, 1,\, 2,\, 3\}$ \\
1707 \textit{card int} = 4 & induces & $\{-1,\, 0,\, +1,\, +2\}$ \\
1708 \textit{card int} = 5 & induces & $\{-2,\, -1,\, 0,\, +1,\, +2\}.$%
1713 $$\hbox{\begin{tabular}{@{}rll@{}}%
1714 \textit{card nat} = $K$ & induces & $\{0,\, \ldots,\, K - 1\}$ \\
1715 \textit{card int} = $K$ & induces & $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor K/2 \rfloor\}.$%
1718 For free types, and often also for \textbf{typedecl}'d types, it usually makes
1719 sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
1720 Although function and product types are normally mapped directly to the
1721 corresponding Kodkod concepts, setting
1722 the cardinality of such types is also allowed and implicitly enables ``boxing''
1723 for them, as explained in the description of the \textit{box}~\qty{type}
1724 and \textit{box} (\S\ref{scope-of-search}) options.
1727 {\small See also \textit{mono} (\S\ref{scope-of-search}).}
1729 \opt{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
1730 Specifies the default sequence of cardinalities to use. This can be overridden
1731 on a per-type basis using the \textit{card}~\qty{type} option described above.
1733 \opu{max}{const}{int\_seq}
1734 Specifies the sequence of maximum multiplicities to use for a given
1735 (co)in\-duc\-tive datatype constructor. A constructor's multiplicity is the
1736 number of distinct values that it can construct. Nonsensical values (e.g.,
1737 \textit{max}~[]~$=$~2) are silently repaired. This option is only available for
1738 datatypes equipped with several constructors.
1741 Specifies the default sequence of maximum multiplicities to use for
1742 (co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor
1743 basis using the \textit{max}~\qty{const} option described above.
1745 \opusmart{wf}{const}{non\_wf}
1746 Specifies whether the specified (co)in\-duc\-tively defined predicate is
1747 well-founded. The option can take the following values:
1750 \item[$\bullet$] \textbf{\textit{true}}: Tentatively treat the (co)in\-duc\-tive
1751 predicate as if it were well-founded. Since this is generally not sound when the
1752 predicate is not well-founded, the counterexamples are tagged as ``likely
1755 \item[$\bullet$] \textbf{\textit{false}}: Treat the (co)in\-duc\-tive predicate
1756 as if it were not well-founded. The predicate is then unrolled as prescribed by
1757 the \textit{star\_linear\_preds}, \textit{iter}~\qty{const}, and \textit{iter}
1760 \item[$\bullet$] \textbf{\textit{smart}}: Try to prove that the inductive
1761 predicate is well-founded using Isabelle's \textit{lexicographic\_order} and
1762 \textit{sizechange} tactics. If this succeeds (or the predicate occurs with an
1763 appropriate polarity in the formula to falsify), use an efficient fixed point
1764 equation as specification of the predicate; otherwise, unroll the predicates
1765 according to the \textit{iter}~\qty{const} and \textit{iter} options.
1769 {\small See also \textit{iter} (\S\ref{scope-of-search}),
1770 \textit{star\_linear\_preds} (\S\ref{optimizations}), and \textit{tac\_timeout}
1771 (\S\ref{timeouts}).}
1773 \opsmart{wf}{non\_wf}
1774 Specifies the default wellfoundedness setting to use. This can be overridden on
1775 a per-predicate basis using the \textit{wf}~\qty{const} option above.
1777 \opu{iter}{const}{int\_seq}
1778 Specifies the sequence of iteration counts to use when unrolling a given
1779 (co)in\-duc\-tive predicate. By default, unrolling is applied for inductive
1780 predicates that occur negatively and coinductive predicates that occur
1781 positively in the formula to falsify and that cannot be proved to be
1782 well-founded, but this behavior is influenced by the \textit{wf} option. The
1783 iteration counts are automatically bounded by the cardinality of the predicate's
1786 {\small See also \textit{wf} (\S\ref{scope-of-search}) and
1787 \textit{star\_linear\_preds} (\S\ref{optimizations}).}
1789 \opt{iter}{int\_seq}{$\mathbf{1{,}2{,}4{,}8{,}12{,}16{,}24{,}32}$}
1790 Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive
1791 predicates. This can be overridden on a per-predicate basis using the
1792 \textit{iter} \qty{const} option above.
1794 \opt{bisim\_depth}{int\_seq}{$\mathbf{7}$}
1795 Specifies the sequence of iteration counts to use when unrolling the
1796 bisimilarity predicate generated by Nitpick for coinductive datatypes. A value
1797 of $-1$ means that no predicate is generated, in which case Nitpick performs an
1798 after-the-fact check to see if the known coinductive datatype values are
1799 bidissimilar. If two values are found to be bisimilar, the counterexample is
1800 tagged as ``likely genuine.'' The iteration counts are automatically bounded by
1801 the sum of the cardinalities of the coinductive datatypes occurring in the
1804 \opusmart{box}{type}{dont\_box}
1805 Specifies whether Nitpick should attempt to wrap (``box'') a given function or
1806 product type in an isomorphic datatype internally. Boxing is an effective mean
1807 to reduce the search space and speed up Nitpick, because the isomorphic datatype
1808 is approximated by a subset of the possible function or pair values;
1809 like other drastic optimizations, it can also prevent the discovery of
1810 counterexamples. The option can take the following values:
1813 \item[$\bullet$] \textbf{\textit{true}}: Box the specified type whenever
1815 \item[$\bullet$] \textbf{\textit{false}}: Never box the type.
1816 \item[$\bullet$] \textbf{\textit{smart}}: Box the type only in contexts where it
1817 is likely to help. For example, $n$-tuples where $n > 2$ and arguments to
1818 higher-order functions are good candidates for boxing.
1821 Setting the \textit{card}~\qty{type} option for a function or product type
1822 implicitly enables boxing for that type.
1825 {\small See also \textit{verbose} (\S\ref{output-format})
1826 and \textit{debug} (\S\ref{output-format}).}
1828 \opsmart{box}{dont\_box}
1829 Specifies the default boxing setting to use. This can be overridden on a
1830 per-type basis using the \textit{box}~\qty{type} option described above.
1832 \opusmart{mono}{type}{non\_mono}
1833 Specifies whether the specified type should be considered monotonic when
1834 enumerating scopes. If the option is set to \textit{smart}, Nitpick performs a
1835 monotonicity check on the type. Setting this option to \textit{true} can reduce
1836 the number of scopes tried, but it also diminishes the theoretical chance of
1837 finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}.
1840 {\small See also \textit{card} (\S\ref{scope-of-search}),
1841 \textit{coalesce\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
1842 (\S\ref{output-format}).}
1844 \opsmart{mono}{non\_box}
1845 Specifies the default monotonicity setting to use. This can be overridden on a
1846 per-type basis using the \textit{mono}~\qty{type} option described above.
1848 \opfalse{coalesce\_type\_vars}{dont\_coalesce\_type\_vars}
1849 Specifies whether type variables with the same sort constraints should be
1850 merged. Setting this option to \textit{true} can reduce the number of scopes
1851 tried and the size of the generated Kodkod formulas, but it also diminishes the
1852 theoretical chance of finding a counterexample.
1854 {\small See also \textit{mono} (\S\ref{scope-of-search}).}
1857 \subsection{Output Format}
1858 \label{output-format}
1861 \opfalse{verbose}{quiet}
1862 Specifies whether the \textbf{nitpick} command should explain what it does. This
1863 option is useful to determine which scopes are tried or which SAT solver is
1864 used. This option is implicitly disabled for automatic runs.
1867 {\small See also \textit{auto} (\S\ref{mode-of-operation}).}
1869 \opfalse{debug}{no\_debug}
1870 Specifies whether Nitpick should display additional debugging information beyond
1871 what \textit{verbose} already displays. Enabling \textit{debug} also enables
1872 \textit{verbose} and \textit{show\_all} behind the scenes. The \textit{debug}
1873 option is implicitly disabled for automatic runs.
1876 {\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{overlord}
1877 (\S\ref{mode-of-operation}), and \textit{batch\_size} (\S\ref{optimizations}).}
1879 \optrue{show\_skolems}{hide\_skolem}
1880 Specifies whether the values of Skolem constants should be displayed as part of
1881 counterexamples. Skolem constants correspond to bound variables in the original
1882 formula and usually help us to understand why the counterexample falsifies the
1886 {\small See also \textit{skolemize} (\S\ref{optimizations}).}
1888 \opfalse{show\_datatypes}{hide\_datatypes}
1889 Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
1890 be displayed as part of counterexamples. Such subsets are sometimes helpful when
1891 investigating whether a potential counterexample is genuine or spurious, but
1892 their potential for clutter is real.
1894 \opfalse{show\_consts}{hide\_consts}
1895 Specifies whether the values of constants occurring in the formula (including
1896 its axioms) should be displayed along with any counterexample. These values are
1897 sometimes helpful when investigating why a counterexample is
1898 genuine, but they can clutter the output.
1900 \opfalse{show\_all}{dont\_show\_all}
1901 Enabling this option effectively enables \textit{show\_skolems},
1902 \textit{show\_datatypes}, and \textit{show\_consts}.
1904 \opt{max\_potential}{int}{$\mathbf{1}$}
1905 Specifies the maximum number of potential counterexamples to display. Setting
1906 this option to 0 speeds up the search for a genuine counterexample. This option
1907 is implicitly set to 0 for automatic runs. If you set this option to a value
1908 greater than 1, you will need an incremental SAT solver: For efficiency, it is
1909 recommended to install the JNI version of MiniSat and set \textit{sat\_solver} =
1910 \textit{MiniSatJNI}. Also be aware that many of the counterexamples may look
1911 identical, unless the \textit{show\_all} (\S\ref{output-format}) option is
1915 {\small See also \textit{auto} (\S\ref{mode-of-operation}),
1916 \textit{check\_potential} (\S\ref{authentication}), and
1917 \textit{sat\_solver} (\S\ref{optimizations}).}
1919 \opt{max\_genuine}{int}{$\mathbf{1}$}
1920 Specifies the maximum number of genuine counterexamples to display. If you set
1921 this option to a value greater than 1, you will need an incremental SAT solver:
1922 For efficiency, it is recommended to install the JNI version of MiniSat and set
1923 \textit{sat\_solver} = \textit{MiniSatJNI}. Also be aware that many of the
1924 counterexamples may look identical, unless the \textit{show\_all}
1925 (\S\ref{output-format}) option is enabled.
1928 {\small See also \textit{check\_genuine} (\S\ref{authentication}) and
1929 \textit{sat\_solver} (\S\ref{optimizations}).}
1931 \ops{eval}{term\_list}
1932 Specifies the list of terms whose values should be displayed along with
1933 counterexamples. This option suffers from an ``observer effect'': Nitpick might
1934 find different counterexamples for different values of this option.
1936 \opu{format}{term}{int\_seq}
1937 Specifies how to uncurry the value displayed for a variable or constant.
1938 Uncurrying sometimes increases the readability of the output for high-arity
1939 functions. For example, given the variable $y \mathbin{\Colon} {'a}\Rightarrow
1940 {'b}\Rightarrow {'c}\Rightarrow {'d}\Rightarrow {'e}\Rightarrow {'f}\Rightarrow
1941 {'g}$, setting \textit{format}~$y$ = 3 tells Nitpick to group the last three
1942 arguments, as if the type had been ${'a}\Rightarrow {'b}\Rightarrow
1943 {'c}\Rightarrow {'d}\times {'e}\times {'f}\Rightarrow {'g}$. In general, a list
1944 of values $n_1,\ldots,n_k$ tells Nitpick to show the last $n_k$ arguments as an
1945 $n_k$-tuple, the previous $n_{k-1}$ arguments as an $n_{k-1}$-tuple, and so on;
1946 arguments that are not accounted for are left alone, as if the specification had
1947 been $1,\ldots,1,n_1,\ldots,n_k$.
1950 {\small See also \textit{uncurry} (\S\ref{optimizations}).}
1952 \opt{format}{int\_seq}{$\mathbf{1}$}
1953 Specifies the default format to use. Irrespective of the default format, the
1954 extra arguments to a Skolem constant corresponding to the outer bound variables
1955 are kept separated from the remaining arguments, the \textbf{for} arguments of
1956 an inductive definitions are kept separated from the remaining arguments, and
1957 the iteration counter of an unrolled inductive definition is shown alone. The
1958 default format can be overridden on a per-variable or per-constant basis using
1959 the \textit{format}~\qty{term} option described above.
1962 %% MARK: Authentication
1963 \subsection{Authentication}
1964 \label{authentication}
1967 \opfalse{check\_potential}{trust\_potential}
1968 Specifies whether potential counterexamples should be given to Isabelle's
1969 \textit{auto} tactic to assess their validity. If a potential counterexample is
1970 shown to be genuine, Nitpick displays a message to this effect and terminates.
1973 {\small See also \textit{max\_potential} (\S\ref{output-format}) and
1974 \textit{auto\_timeout} (\S\ref{timeouts}).}
1976 \opfalse{check\_genuine}{trust\_genuine}
1977 Specifies whether genuine and likely genuine counterexamples should be given to
1978 Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine''
1979 counterexample is shown to be spurious, the user is kindly asked to send a bug
1980 report to the author at
1981 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@in.tum.de}.
1984 {\small See also \textit{max\_genuine} (\S\ref{output-format}) and
1985 \textit{auto\_timeout} (\S\ref{timeouts}).}
1987 \ops{expect}{string}
1988 Specifies the expected outcome, which must be one of the following:
1991 \item[$\bullet$] \textbf{\textit{genuine}}: Nitpick found a genuine counterexample.
1992 \item[$\bullet$] \textbf{\textit{likely\_genuine}}: Nitpick found a ``likely
1993 genuine'' counterexample (i.e., a counterexample that is genuine unless
1994 it contradicts a missing axiom or a dangerous option was used inappropriately).
1995 \item[$\bullet$] \textbf{\textit{potential}}: Nitpick found a potential counterexample.
1996 \item[$\bullet$] \textbf{\textit{none}}: Nitpick found no counterexample.
1997 \item[$\bullet$] \textbf{\textit{unknown}}: Nitpick encountered some problem (e.g.,
1998 Kodkod ran out of memory).
2001 Nitpick emits an error if the actual outcome differs from the expected outcome.
2002 This option is useful for regression testing.
2005 \subsection{Optimizations}
2006 \label{optimizations}
2008 \def\cpp{C\nobreak\raisebox{.1ex}{+}\nobreak\raisebox{.1ex}{+}}
2013 \opt{sat\_solver}{string}{smart}
2014 Specifies which SAT solver to use. SAT solvers implemented in C or \cpp{} tend
2015 to be faster than their Java counterparts, but they can be more difficult to
2016 install. Also, if you set the \textit{max\_potential} (\S\ref{output-format}) or
2017 \textit{max\_genuine} (\S\ref{output-format}) option to a value greater than 1,
2018 you will need an incremental SAT solver, such as \textit{MiniSatJNI}
2019 (recommended) or \textit{SAT4J}.
2021 The supported solvers are listed below:
2025 \item[$\bullet$] \textbf{\textit{MiniSat}}: MiniSat is an efficient solver
2026 written in \cpp{}. To use MiniSat, set the environment variable
2027 \texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
2028 executable. The \cpp{} sources and executables for MiniSat are available at
2029 \url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
2030 and 2.0 beta (2007-07-21).
2032 \item[$\bullet$] \textbf{\textit{MiniSatJNI}}: The JNI (Java Native Interface)
2033 version of MiniSat is bundled in \texttt{nativesolver.\allowbreak tgz}, which
2034 you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
2035 version of MiniSat, the JNI version can be used incrementally.
2037 \item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver
2038 written in C. It is bundled with Kodkodi and requires no further installation or
2039 configuration steps. Alternatively, you can install a standard version of
2040 PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
2041 that contains the \texttt{picosat} executable. The C sources for PicoSAT are
2042 available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
2043 Nitpick has been tested with version 913.
2045 \item[$\bullet$] \textbf{\textit{zChaff}}: zChaff is an efficient solver written
2046 in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
2047 the directory that contains the \texttt{zchaff} executable. The \cpp{} sources
2048 and executables for zChaff are available at
2049 \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
2050 versions 2004-05-13, 2004-11-15, and 2007-03-12.
2052 \item[$\bullet$] \textbf{\textit{zChaffJNI}}: The JNI version of zChaff is
2053 bundled in \texttt{native\-solver.\allowbreak tgz}, which you will find on
2054 Kodkod's web site \cite{kodkod-2009}.
2056 \item[$\bullet$] \textbf{\textit{RSat}}: RSat is an efficient solver written in
2057 \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
2058 directory that contains the \texttt{rsat} executable. The \cpp{} sources for
2059 RSat are available at \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been
2060 tested with version 2.01.
2062 \item[$\bullet$] \textbf{\textit{BerkMin}}: BerkMin561 is an efficient solver
2063 written in C. To use BerkMin, set the environment variable
2064 \texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561}
2065 executable. The BerkMin executables are available at
2066 \url{http://eigold.tripod.com/BerkMin.html}.
2068 \item[$\bullet$] \textbf{\textit{BerkMinAlloy}}: Variant of BerkMin that is
2069 included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
2070 version of BerkMin, set the environment variable
2071 \texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
2074 \item[$\bullet$] \textbf{\textit{Jerusat}}: Jerusat 1.3 is an efficient solver
2075 written in C. To use Jerusat, set the environment variable
2076 \texttt{JERUSAT\_HOME} to the directory that contains the \texttt{Jerusat1.3}
2077 executable. The C sources for Jerusat are available at
2078 \url{http://www.cs.tau.ac.il/~ale1/Jerusat1.3.tgz}.
2080 \item[$\bullet$] \textbf{\textit{SAT4J}}: SAT4J is a reasonably efficient solver
2081 written in Java that can be used incrementally. It is bundled with Kodkodi and
2082 requires no further installation or configuration steps. Do not attempt to
2083 install the official SAT4J packages, because their API is incompatible with
2086 \item[$\bullet$] \textbf{\textit{SAT4JLight}}: Variant of SAT4J that is
2087 optimized for small problems. It can also be used incrementally.
2089 \item[$\bullet$] \textbf{\textit{HaifaSat}}: HaifaSat 1.0 beta is an
2090 experimental solver written in \cpp. To use HaifaSat, set the environment
2091 variable \texttt{HAIFASAT\_\allowbreak HOME} to the directory that contains the
2092 \texttt{HaifaSat} executable. The \cpp{} sources for HaifaSat are available at
2093 \url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}.
2095 \item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
2096 \textit{smart}, Nitpick selects the first solver among MiniSat, PicoSAT, zChaff,
2097 RSat, BerkMin, BerkMinAlloy, and Jerusat that is recognized by Isabelle. If none
2098 is found, it falls back on SAT4J, which should always be available. If
2099 \textit{verbose} is enabled, Nitpick displays which SAT solver was chosen.
2104 \opt{batch\_size}{int\_or\_smart}{smart}
2105 Specifies the maximum number of Kodkod problems that should be lumped together
2106 when invoking Kodkodi. Each problem corresponds to one scope. Lumping problems
2107 together ensures that Kodkodi is launched less often, but it makes the verbose
2108 output less readable and is sometimes detrimental to performance. If
2109 \textit{batch\_size} is set to \textit{smart}, the actual value used is 1 if
2110 \textit{debug} (\S\ref{output-format}) is set and 64 otherwise.
2112 \optrue{destroy\_constrs}{dont\_destroy\_constrs}
2113 Specifies whether formulas involving (co)in\-duc\-tive datatype constructors should
2114 be rewritten to use (automatically generated) discriminators and destructors.
2115 This optimization can drastically reduce the size of the Boolean formulas given
2119 {\small See also \textit{debug} (\S\ref{output-format}).}
2121 \optrue{specialize}{dont\_specialize}
2122 Specifies whether functions invoked with static arguments should be specialized.
2123 This optimization can drastically reduce the search space, especially for
2124 higher-order functions.
2127 {\small See also \textit{debug} (\S\ref{output-format}) and
2128 \textit{show\_consts} (\S\ref{output-format}).}
2130 \optrue{skolemize}{dont\_skolemize}
2131 Specifies whether the formula should be skolemized. For performance reasons,
2132 (positive) $\forall$-quanti\-fiers that occur in the scope of a higher-order
2133 (positive) $\exists$-quanti\-fier are left unchanged.
2136 {\small See also \textit{debug} (\S\ref{output-format}) and
2137 \textit{show\_skolems} (\S\ref{output-format}).}
2139 \optrue{star\_linear\_preds}{dont\_star\_linear\_preds}
2140 Specifies whether Nitpick should use Kodkod's transitive closure operator to
2141 encode non-well-founded ``linear inductive predicates,'' i.e., inductive
2142 predicates for which each the predicate occurs in at most one assumption of each
2143 introduction rule. Using the reflexive transitive closure is in principle
2144 equivalent to setting \textit{iter} to the cardinality of the predicate's
2145 domain, but it is usually more efficient.
2147 {\small See also \textit{wf} (\S\ref{scope-of-search}), \textit{debug}
2148 (\S\ref{output-format}), and \textit{iter} (\S\ref{scope-of-search}).}
2150 \optrue{uncurry}{dont\_uncurry}
2151 Specifies whether Nitpick should uncurry functions. Uncurrying has on its own no
2152 tangible effect on efficiency, but it creates opportunities for the boxing
2156 {\small See also \textit{box} (\S\ref{scope-of-search}), \textit{debug}
2157 (\S\ref{output-format}), and \textit{format} (\S\ref{output-format}).}
2159 \optrue{fast\_descrs}{full\_descrs}
2160 Specifies whether Nitpick should optimize the definite and indefinite
2161 description operators (THE and SOME). The optimized versions usually help
2162 Nitpick generate more counterexamples or at least find them faster, but only the
2163 unoptimized versions are complete when all types occurring in the formula are
2166 {\small See also \textit{debug} (\S\ref{output-format}).}
2168 \optrue{peephole\_optim}{no\_peephole\_optim}
2169 Specifies whether Nitpick should simplify the generated Kodkod formulas using a
2170 peephole optimizer. These optimizations can make a significant difference.
2171 Unless you are tracking down a bug in Nitpick or distrust the peephole
2172 optimizer, you should leave this option enabled.
2174 \opt{sym\_break}{int}{20}
2175 Specifies an upper bound on the number of relations for which Kodkod generates
2176 symmetry breaking predicates. According to the Kodkod documentation
2177 \cite{kodkod-2009-options}, ``in general, the higher this value, the more
2178 symmetries will be broken, and the faster the formula will be solved. But,
2179 setting the value too high may have the opposite effect and slow down the
2182 \opt{sharing\_depth}{int}{3}
2183 Specifies the depth to which Kodkod should check circuits for equivalence during
2184 the translation to SAT. The default of 3 is the same as in Alloy. The minimum
2185 allowed depth is 1. Increasing the sharing may result in a smaller SAT problem,
2186 but can also slow down Kodkod.
2188 \opfalse{flatten\_props}{dont\_flatten\_props}
2189 Specifies whether Kodkod should try to eliminate intermediate Boolean variables.
2190 Although this might sound like a good idea, in practice it can drastically slow
2193 \opt{max\_threads}{int}{0}
2194 Specifies the maximum number of threads to use in Kodkod. If this option is set
2195 to 0, Kodkod will compute an appropriate value based on the number of processor
2199 {\small See also \textit{batch\_size} (\S\ref{optimizations}) and
2200 \textit{timeout} (\S\ref{timeouts}).}
2203 \subsection{Timeouts}
2207 \opt{timeout}{time}{$\mathbf{30}$ s}
2208 Specifies the maximum amount of time that the \textbf{nitpick} command should
2209 spend looking for a counterexample. Nitpick tries to honor this constraint as
2210 well as it can but offers no guarantees. For automatic runs,
2211 \textit{auto\_timeout} is used instead.
2214 {\small See also \textit{auto} (\S\ref{mode-of-operation})
2215 and \textit{max\_threads} (\S\ref{optimizations}).}
2217 \opt{auto\_timeout}{time}{$\mathbf{5}$ s}
2218 Specifies the maximum amount of time that Nitpick should use to find a
2219 counterexample when running automatically. Nitpick tries to honor this
2220 constraint as well as it can but offers no guarantees.
2223 {\small See also \textit{auto} (\S\ref{mode-of-operation}).}
2225 \opt{tac\_timeout}{time}{$\mathbf{500}$ ms}
2226 Specifies the maximum amount of time that the \textit{auto} tactic should use
2227 when checking a counterexample, and similarly that \textit{lexicographic\_order}
2228 and \textit{sizechange} should use when checking whether a (co)in\-duc\-tive
2229 predicate is well-founded. Nitpick tries to honor this constraint as well as it
2230 can but offers no guarantees.
2233 {\small See also \textit{wf} (\S\ref{scope-of-search}),
2234 \textit{check\_potential} (\S\ref{authentication}),
2235 and \textit{check\_genuine} (\S\ref{authentication}).}
2238 \section{Attribute Reference}
2239 \label{attribute-reference}
2241 Nitpick needs to consider the definitions of all constants occurring in a
2242 formula in order to falsify it. For constants introduced using the
2243 \textbf{definition} command, the definition is simply the associated
2244 \textit{\_def} axiom. In contrast, instead of using the internal representation
2245 of functions synthesized by Isabelle's \textbf{primrec}, \textbf{function}, and
2246 \textbf{nominal\_primrec} packages, Nitpick relies on the more natural
2247 equational specification entered by the user.
2249 Behind the scenes, Isabelle's built-in packages and theories rely on the
2250 following attributes to affect Nitpick's behavior:
2253 \flushitem{\textit{nitpick\_def}}
2256 This attribute specifies an alternative definition of a constant. The
2257 alternative definition should be logically equivalent to the constant's actual
2258 axiomatic definition and should be of the form
2260 \qquad $c~{?}x_1~\ldots~{?}x_n \,\equiv\, t$,
2262 where ${?}x_1, \ldots, {?}x_n$ are distinct variables and $c$ does not occur in
2265 \flushitem{\textit{nitpick\_simp}}
2268 This attribute specifies the equations that constitute the specification of a
2269 constant. For functions defined using the \textbf{primrec}, \textbf{function},
2270 and \textbf{nominal\_\allowbreak primrec} packages, this corresponds to the
2271 \textit{simps} rules. The equations must be of the form
2273 \qquad $c~t_1~\ldots\ t_n \,=\, u.$
2275 \flushitem{\textit{nitpick\_psimp}}
2278 This attribute specifies the equations that constitute the partial specification
2279 of a constant. For functions defined using the \textbf{function} package, this
2280 corresponds to the \textit{psimps} rules. The conditional equations must be of
2283 \qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,=\, u$.
2285 \flushitem{\textit{nitpick\_intro}}
2288 This attribute specifies the introduction rules of a (co)in\-duc\-tive predicate.
2289 For predicates defined using the \textbf{inductive} or \textbf{coinductive}
2290 command, this corresponds to the \textit{intros} rules. The introduction rules
2293 \qquad $\lbrakk P_1;\> \ldots;\> P_m;\> M~(c\ t_{11}\ \ldots\ t_{1n});\>
2294 \ldots;\> M~(c\ t_{k1}\ \ldots\ t_{kn})\rbrakk \,\Longrightarrow\, c\ u_1\
2297 where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an
2298 optional monotonic operator. The order of the assumptions is irrelevant.
2302 When faced with a constant, Nitpick proceeds as follows:
2305 \item[1.] If the \textit{nitpick\_simp} set associated with the constant
2306 is not empty, Nitpick uses these rules as the specification of the constant.
2308 \item[2.] Otherwise, if the \textit{nitpick\_psimp} set associated with
2309 the constant is not empty, it uses these rules as the specification of the
2312 \item[3.] Otherwise, it looks up the definition of the constant:
2315 \item[1.] If the \textit{nitpick\_def} set associated with the constant
2316 is not empty, it uses the latest rule added to the set as the definition of the
2317 constant; otherwise it uses the actual definition axiom.
2318 \item[2.] If the definition is of the form
2320 \qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{lfp}~(\lambda f.\; t)$,
2322 then Nitpick assumes that the definition was made using an inductive package and
2323 based on the introduction rules marked with \textit{nitpick\_\allowbreak
2324 ind\_\allowbreak intros} tries to determine whether the definition is
2329 As an illustration, consider the inductive definition
2332 \textbf{inductive}~\textit{odd}~\textbf{where} \\
2333 ``\textit{odd}~1'' $\,\mid$ \\
2334 ``\textit{odd}~$n\,\Longrightarrow\, \textit{odd}~(\textit{Suc}~(\textit{Suc}~n))$''
2337 Isabelle automatically attaches the \textit{nitpick\_intro} attribute to
2338 the above rules. Nitpick then uses the \textit{lfp}-based definition in
2339 conjunction with these rules. To override this, we can specify an alternative
2340 definition as follows:
2343 \textbf{lemma} $\mathit{odd\_def}'$ [\textit{nitpick\_def}]: ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
2346 Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2
2347 = 1$. Alternatively, we can specify an equational specification of the constant:
2350 \textbf{lemma} $\mathit{odd\_simp}'$ [\textit{nitpick\_simp}]: ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
2353 Such tweaks should be done with great care, because Nitpick will assume that the
2354 constant is completely defined by its equational specification. For example, if
2355 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
2356 $\textit{odd}~n$ arbitrarily for even values of $n$. The \textit{debug}
2357 (\S\ref{output-format}) option is extremely useful to understand what is going
2358 on when experimenting with \textit{nitpick\_} attributes.
2360 \section{Standard ML Interface}
2361 \label{standard-ml-interface}
2363 Nitpick provides a rich Standard ML interface used mainly for internal purposes
2364 and debugging. Among the most interesting functions exported by Nitpick are
2365 those that let you invoke the tool programmatically and those that let you
2366 register and unregister custom coinductive datatypes.
2368 \subsection{Invocation of Nitpick}
2369 \label{invocation-of-nitpick}
2371 The \textit{Nitpick} structure offers the following functions for invoking your
2372 favorite counterexample generator:
2375 $\textbf{val}\,~\textit{pick\_nits\_in\_term} : \\
2376 \hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{term~list} \rightarrow \textit{term} \\
2377 \hbox{}\quad{\rightarrow}\; \textit{string} * \textit{Proof.state}$ \\
2378 $\textbf{val}\,~\textit{pick\_nits\_in\_subgoal} : \\
2379 \hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{int} \rightarrow \textit{string} * \textit{Proof.state}$
2382 The return value is a new proof state paired with an outcome string
2383 (``genuine'', ``likely\_genuine'', ``potential'', ``none'', or ``unknown''). The
2384 \textit{params} type is a large record that lets you set Nitpick's options. The
2385 current default options can be retrieved by calling the following function
2386 defined in the \textit{NitpickIsar} structure:
2389 $\textbf{val}\,~\textit{default\_params} :\,
2390 \textit{theory} \rightarrow (\textit{string} * \textit{string})~\textit{list} \rightarrow \textit{params}$
2393 The second argument lets you override option values before they are parsed and
2394 put into a \textit{params} record. Here is an example:
2397 $\textbf{val}\,~\textit{params} = \textit{NitpickIsar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
2398 $\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t]
2399 & \textit{state}~\textit{params}~\textit{false} \\[-2pt]
2400 & \textit{subgoal}\end{aligned}$
2403 \subsection{Registration of Coinductive Datatypes}
2404 \label{registration-of-coinductive-datatypes}
2408 If you have defined a custom coinductive datatype, you can tell Nitpick about
2409 it, so that it can use an efficient Kodkod axiomatization similar to the one it
2410 uses for lazy lists. The interface for registering and unregistering coinductive
2411 datatypes consists of the following pair of functions defined in the
2412 \textit{Nitpick} structure:
2415 $\textbf{val}\,~\textit{register\_codatatype} :\,
2416 \textit{typ} \rightarrow \textit{string} \rightarrow \textit{styp~list} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\
2417 $\textbf{val}\,~\textit{unregister\_codatatype} :\,
2418 \textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$
2421 The type $'a~\textit{llist}$ of lazy lists is already registered; had it
2422 not been, you could have told Nitpick about it by adding the following line
2423 to your theory file:
2426 $\textbf{setup}~\,\{{*}\,~\!\begin{aligned}[t]
2427 & \textit{Nitpick.register\_codatatype} \\[-2pt]
2428 & \qquad @\{\antiq{typ}~``\kern1pt'a~\textit{llist}\textrm{''}\}~@\{\antiq{const\_name}~ \textit{llist\_case}\} \\[-2pt] %% TYPESETTING
2429 & \qquad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])\,\ {*}\}\end{aligned}$
2432 The \textit{register\_codatatype} function takes a coinductive type, its case
2433 function, and the list of its constructors. The case function must take its
2434 arguments in the order that the constructors are listed. If no case function
2435 with the correct signature is available, simply pass the empty string.
2437 On the other hand, if your goal is to cripple Nitpick, add the following line to
2438 your theory file and try to check a few conjectures about lazy lists:
2441 $\textbf{setup}~\,\{{*}\,~\textit{Nitpick.unregister\_codatatype}~@\{\antiq{typ}~``
2442 \kern1pt'a~\textit{list}\textrm{''}\}\ \,{*}\}$
2445 \section{Known Bugs and Limitations}
2446 \label{known-bugs-and-limitations}
2448 Here are the known bugs and limitations in Nitpick at the time of writing:
2451 \item[$\bullet$] Underspecified functions defined using the \textbf{primrec},
2452 \textbf{function}, or \textbf{nominal\_\allowbreak primrec} packages can lead
2453 Nitpick to generate spurious counterexamples for theorems that refer to values
2454 for which the function is not defined. For example:
2457 \textbf{primrec} \textit{prec} \textbf{where} \\
2458 ``$\textit{prec}~(\textit{Suc}~n) = n$'' \\[2\smallskipamount]
2459 \textbf{lemma} ``$\textit{prec}~0 = \undef$'' \\
2460 \textbf{nitpick} \\[2\smallskipamount]
2461 \quad{\slshape Nitpick found a counterexample for \textit{card nat}~= 2:
2463 \\[2\smallskipamount]
2464 \hbox{}\qquad Empty assignment} \nopagebreak\\[2\smallskipamount]
2465 \textbf{by}~(\textit{auto simp}: \textit{prec\_def})
2468 Such theorems are considered bad style because they rely on the internal
2469 representation of functions synthesized by Isabelle, which is an implementation
2472 \item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
2473 \textbf{guess} command in a structured proof.
2475 \item[$\bullet$] The \textit{nitpick\_} attributes and the
2476 \textit{Nitpick.register\_} functions can cause havoc if used improperly.
2478 \item[$\bullet$] Local definitions are not supported and result in an error.
2480 \item[$\bullet$] All constants and types whose names start with
2481 \textit{Nitpick}{.} are reserved for internal use.
2485 \bibliography{../manual}{}
2486 \bibliographystyle{abbrv}