1 \documentclass[a4paper,12pt]{article}
2 \usepackage[T1]{fontenc}
5 \usepackage[english,french]{babel}
12 %\usepackage[scaled=.85]{beramono}
13 \usepackage{../iman,../pdfsetup}
16 %\evensidemargin=4.6mm
23 \def\Colon{\mathord{:\mkern-1.5mu:}}
24 %\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
25 %\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
26 \def\lparr{\mathopen{(\mkern-4mu\mid}}
27 \def\rparr{\mathclose{\mid\mkern-4mu)}}
30 \def\undef{(\lambda x.\; \unk)}
31 %\def\unr{\textit{others}}
33 \def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
34 \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
36 \hyphenation{Mini-Sat size-change First-Steps grand-parent nit-pick
37 counter-example counter-examples data-type data-types co-data-type
38 co-data-types in-duc-tive co-in-duc-tive}
44 \selectlanguage{english}
46 \title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]
47 Picking Nits \\[\smallskipamount]
48 \Large A User's Guide to Nitpick for Isabelle/HOL}
50 Jasmin Christian Blanchette \\
51 {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
58 \setlength{\parskip}{.7em plus .2em minus .1em}
59 \setlength{\parindent}{0pt}
60 \setlength{\abovedisplayskip}{\parskip}
61 \setlength{\abovedisplayshortskip}{.9\parskip}
62 \setlength{\belowdisplayskip}{\parskip}
63 \setlength{\belowdisplayshortskip}{.9\parskip}
65 % General-purpose enum environment with correct spacing
66 \newenvironment{enum}%
68 \setlength{\topsep}{.1\parskip}%
69 \setlength{\partopsep}{.1\parskip}%
70 \setlength{\itemsep}{\parskip}%
71 \advance\itemsep by-\parsep}}
74 \def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
75 \advance\rightskip by\leftmargin}
76 \def\post{\vskip0pt plus1ex\endgroup}
78 \def\prew{\pre\advance\rightskip by-\leftmargin}
81 \section{Introduction}
84 Nitpick \cite{blanchette-nipkow-2009} is a counterexample generator for
85 Isabelle/HOL \cite{isa-tutorial} that is designed to handle formulas
86 combining (co)in\-duc\-tive datatypes, (co)in\-duc\-tively defined predicates, and
87 quantifiers. It builds on Kodkod \cite{torlak-jackson-2007}, a highly optimized
88 first-order relational model finder developed by the Software Design Group at
89 MIT. It is conceptually similar to Refute \cite{weber-2008}, from which it
90 borrows many ideas and code fragments, but it benefits from Kodkod's
91 optimizations and a new encoding scheme. The name Nitpick is shamelessly
92 appropriated from a now retired Alloy precursor.
94 Nitpick is easy to use---you simply enter \textbf{nitpick} after a putative
95 theorem and wait a few seconds. Nonetheless, there are situations where knowing
96 how it works under the hood and how it reacts to various options helps
97 increase the test coverage. This manual also explains how to install the tool on
98 your workstation. Should the motivation fail you, think of the many hours of
99 hard work Nitpick will save you. Proving non-theorems is \textsl{hard work}.
101 Another common use of Nitpick is to find out whether the axioms of a locale are
102 satisfiable, while the locale is being developed. To check this, it suffices to
106 \textbf{lemma}~``$\textit{False}$'' \\
107 \textbf{nitpick}~[\textit{show\_all}]
110 after the locale's \textbf{begin} keyword. To falsify \textit{False}, Nitpick
111 must find a model for the axioms. If it finds no model, we have an indication
112 that the axioms might be unsatisfiable.
114 Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.5 virtual
115 machine called \texttt{java}. The examples presented in this manual can be found
116 in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
118 Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
119 Nitpick also provides an automatic mode that can be enabled using the
120 ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof General. In this
121 mode, Nitpick is run on every newly entered theorem, much like Auto Quickcheck.
122 The collective time limit for Auto Nitpick and Auto Quickcheck can be set using
123 the ``Auto Counterexample Time Limit'' option.
126 \setbox\boxA=\hbox{\texttt{nospam}}
128 The known bugs and limitations at the time of writing are listed in
129 \S\ref{known-bugs-and-limitations}. Comments and bug reports concerning Nitpick
130 or this manual should be directed to
131 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
132 in.\allowbreak tum.\allowbreak de}.
134 \vskip2.5\smallskipamount
136 \textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
137 suggesting several textual improvements.
138 % and Perry James for reporting a typo.
140 \section{First Steps}
143 This section introduces Nitpick by presenting small examples. If possible, you
144 should try out the examples on your workstation. Your theory file should start
148 \textbf{theory}~\textit{Scratch} \\
149 \textbf{imports}~\textit{Main~Quotient\_Product~RealDef} \\
153 The results presented here were obtained using the JNI (Java Native Interface)
154 version of MiniSat and with multithreading disabled to reduce nondeterminism.
155 This was done by adding the line
158 \textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1]
161 after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
162 Kodkodi and is precompiled for the major platforms. Other SAT solvers can also
163 be installed, as explained in \S\ref{optimizations}. If you have already
164 configured SAT solvers in Isabelle (e.g., for Refute), these will also be
165 available to Nitpick.
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 \phantom{0}1. $P\,\Longrightarrow\, Q$ \\
193 \phantom{0}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_1, a_2, a_3\} := a_3,\> \{a_1, a_2\} := a_3,\> \{a_1, a_3\} := a_3, \\[-2pt] %% TYPESETTING
316 & \{a_1\} := a_1,\> \{a_2, a_3\} := a_1,\> \{a_2\} := a_2, \\[-2pt]
317 & \{a_3\} := 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 Isabelle/HOL notation $f(x :=
322 y)$ denotes the function that maps $x$ to $y$ and that otherwise behaves like
325 Our misadventures with THE suggest adding `$\exists!x{.}$' (``there exists a
326 unique $x$ such that'') at the front of our putative lemma's assumption:
329 \textbf{lemma}~``$\exists {!}x.\; P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
332 The fix appears to work:
335 \textbf{nitpick} \\[2\smallskipamount]
336 \slshape Nitpick found no counterexample.
339 We can further increase our confidence in the formula by exhausting all
340 cardinalities up to 50:
343 \textbf{nitpick} [\textit{card} $'a$~= 1--50]\footnote{The symbol `--'
344 can be entered as \texttt{-} (hyphen) or
345 \texttt{\char`\\\char`\<midarrow\char`\>}.} \\[2\smallskipamount]
346 \slshape Nitpick found no counterexample.
349 Let's see if Sledgehammer \cite{sledgehammer-2009} can find a proof:
352 \textbf{sledgehammer} \\[2\smallskipamount]
353 {\slshape Sledgehammer: external prover ``$e$'' for subgoal 1: \\
354 $\exists{!}x.\; P~x\,\Longrightarrow\, P~(\hbox{\slshape THE}~y.\; P~y)$ \\
355 Try this command: \textrm{apply}~(\textit{metis~the\_equality})} \\[2\smallskipamount]
356 \textbf{apply}~(\textit{metis~the\_equality\/}) \nopagebreak \\[2\smallskipamount]
357 {\slshape No subgoals!}% \\[2\smallskipamount]
361 This must be our lucky day.
363 \subsection{Skolemization}
364 \label{skolemization}
366 Are all invertible functions onto? Let's find out:
369 \textbf{lemma} ``$\exists g.\; \forall x.~g~(f~x) = x
370 \,\Longrightarrow\, \forall y.\; \exists x.~y = f~x$'' \\
371 \textbf{nitpick} \\[2\smallskipamount]
373 Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\[2\smallskipamount]
374 \hbox{}\qquad Free variable: \nopagebreak \\
375 \hbox{}\qquad\qquad $f = \undef{}(b_1 := a_1)$ \\
376 \hbox{}\qquad Skolem constants: \nopagebreak \\
377 \hbox{}\qquad\qquad $g = \undef{}(a_1 := b_1,\> a_2 := b_1)$ \\
378 \hbox{}\qquad\qquad $y = a_2$
381 Although $f$ is the only free variable occurring in the formula, Nitpick also
382 displays values for the bound variables $g$ and $y$. These values are available
383 to Nitpick because it performs skolemization as a preprocessing step.
385 In the previous example, skolemization only affected the outermost quantifiers.
386 This is not always the case, as illustrated below:
389 \textbf{lemma} ``$\exists x.\; \forall f.\; f~x = x$'' \\
390 \textbf{nitpick} \\[2\smallskipamount]
392 Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
393 \hbox{}\qquad Skolem constant: \nopagebreak \\
394 \hbox{}\qquad\qquad $\lambda x.\; f =
395 \undef{}(\!\begin{aligned}[t]
396 & a_1 := \undef{}(a_1 := a_2,\> a_2 := a_1), \\[-2pt]
397 & a_2 := \undef{}(a_1 := a_1,\> a_2 := a_1))\end{aligned}$
400 The variable $f$ is bound within the scope of $x$; therefore, $f$ depends on
401 $x$, as suggested by the notation $\lambda x.\,f$. If $x = a_1$, then $f$ is the
402 function that maps $a_1$ to $a_2$ and vice versa; otherwise, $x = a_2$ and $f$
403 maps both $a_1$ and $a_2$ to $a_1$. In both cases, $f~x \not= x$.
405 The source of the Skolem constants is sometimes more obscure:
408 \textbf{lemma} ``$\mathit{refl}~r\,\Longrightarrow\, \mathit{sym}~r$'' \\
409 \textbf{nitpick} \\[2\smallskipamount]
411 Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
412 \hbox{}\qquad Free variable: \nopagebreak \\
413 \hbox{}\qquad\qquad $r = \{(a_1, a_1),\, (a_2, a_1),\, (a_2, a_2)\}$ \\
414 \hbox{}\qquad Skolem constants: \nopagebreak \\
415 \hbox{}\qquad\qquad $\mathit{sym}.x = a_2$ \\
416 \hbox{}\qquad\qquad $\mathit{sym}.y = a_1$
419 What happened here is that Nitpick expanded the \textit{sym} constant to its
423 $\mathit{sym}~r \,\equiv\,
424 \forall x\> y.\,\> (x, y) \in r \longrightarrow (y, x) \in r.$
427 As their names suggest, the Skolem constants $\mathit{sym}.x$ and
428 $\mathit{sym}.y$ are simply the bound variables $x$ and $y$
429 from \textit{sym}'s definition.
431 Although skolemization is a useful optimization, you can disable it by invoking
432 Nitpick with \textit{dont\_skolemize}. See \S\ref{optimizations} for details.
434 \subsection{Natural Numbers and Integers}
435 \label{natural-numbers-and-integers}
437 Because of the axiom of infinity, the type \textit{nat} does not admit any
438 finite models. To deal with this, Nitpick's approach is to consider finite
439 subsets $N$ of \textit{nat} and maps all numbers $\notin N$ to the undefined
440 value (displayed as `$\unk$'). The type \textit{int} is handled similarly.
441 Internally, undefined values lead to a three-valued logic.
443 Here is an example involving \textit{int\/}:
446 \textbf{lemma} ``$\lbrakk i \le j;\> n \le (m{\Colon}\mathit{int})\rbrakk \,\Longrightarrow\, i * n + j * m \le i * m + j * n$'' \\
447 \textbf{nitpick} \\[2\smallskipamount]
448 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
449 \hbox{}\qquad Free variables: \nopagebreak \\
450 \hbox{}\qquad\qquad $i = 0$ \\
451 \hbox{}\qquad\qquad $j = 1$ \\
452 \hbox{}\qquad\qquad $m = 1$ \\
453 \hbox{}\qquad\qquad $n = 0$
456 Internally, Nitpick uses either a unary or a binary representation of numbers.
457 The unary representation is more efficient but only suitable for numbers very
458 close to zero. By default, Nitpick attempts to choose the more appropriate
459 encoding by inspecting the formula at hand. This behavior can be overridden by
460 passing either \textit{unary\_ints} or \textit{binary\_ints} as option. For
461 binary notation, the number of bits to use can be specified using
462 the \textit{bits} option. For example:
465 \textbf{nitpick} [\textit{binary\_ints}, \textit{bits}${} = 16$]
468 With infinite types, we don't always have the luxury of a genuine counterexample
469 and must often content ourselves with a potential one. The tedious task of
470 finding out whether the potential counterexample is in fact genuine can be
471 outsourced to \textit{auto} by passing \textit{check\_potential}. For example:
474 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
475 \textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[2\smallskipamount]
476 \slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
477 fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
478 Nitpick found a potential counterexample: \\[2\smallskipamount]
479 \hbox{}\qquad Free variable: \nopagebreak \\
480 \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
481 Confirmation by ``\textit{auto}'': The above counterexample is genuine.
484 You might wonder why the counterexample is first reported as potential. The root
485 of the problem is that the bound variable in $\forall n.\; \textit{Suc}~n
486 \mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds an $n$ such
487 that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
488 \textit{False}; but otherwise, it does not know anything about values of $n \ge
489 \textit{card~nat}$ and must therefore evaluate the assumption to $\unk$, not
490 \textit{True}. Since the assumption can never be satisfied, the putative lemma
491 can never be falsified.
493 Incidentally, if you distrust the so-called genuine counterexamples, you can
494 enable \textit{check\_\allowbreak genuine} to verify them as well. However, be
495 aware that \textit{auto} will usually fail to prove that the counterexample is
498 Some conjectures involving elementary number theory make Nitpick look like a
499 giant with feet of clay:
502 \textbf{lemma} ``$P~\textit{Suc}$'' \\
503 \textbf{nitpick} \\[2\smallskipamount]
505 Nitpick found no counterexample.
508 On any finite set $N$, \textit{Suc} is a partial function; for example, if $N =
509 \{0, 1, \ldots, k\}$, then \textit{Suc} is $\{0 \mapsto 1,\, 1 \mapsto 2,\,
510 \ldots,\, k \mapsto \unk\}$, which evaluates to $\unk$ when passed as
511 argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$. The next
515 \textbf{lemma} ``$P~(\textit{op}~{+}\Colon
516 \textit{nat}\mathbin{\Rightarrow}\textit{nat}\mathbin{\Rightarrow}\textit{nat})$'' \\
517 \textbf{nitpick} [\textit{card nat} = 1] \\[2\smallskipamount]
518 {\slshape Nitpick found a counterexample:} \\[2\smallskipamount]
519 \hbox{}\qquad Free variable: \nopagebreak \\
520 \hbox{}\qquad\qquad $P = \{\}$ \\[2\smallskipamount]
521 \textbf{nitpick} [\textit{card nat} = 2] \\[2\smallskipamount]
522 {\slshape Nitpick found no counterexample.}
525 The problem here is that \textit{op}~+ is total when \textit{nat} is taken to be
526 $\{0\}$ but becomes partial as soon as we add $1$, because $1 + 1 \notin \{0,
529 Because numbers are infinite and are approximated using a three-valued logic,
530 there is usually no need to systematically enumerate domain sizes. If Nitpick
531 cannot find a genuine counterexample for \textit{card~nat}~= $k$, it is very
532 unlikely that one could be found for smaller domains. (The $P~(\textit{op}~{+})$
533 example above is an exception to this principle.) Nitpick nonetheless enumerates
534 all cardinalities from 1 to 8 for \textit{nat}, mainly because smaller
535 cardinalities are fast to handle and give rise to simpler counterexamples. This
536 is explained in more detail in \S\ref{scope-monotonicity}.
538 \subsection{Inductive Datatypes}
539 \label{inductive-datatypes}
541 Like natural numbers and integers, inductive datatypes with recursive
542 constructors admit no finite models and must be approximated by a subterm-closed
543 subset. For example, using a cardinality of 10 for ${'}a~\textit{list}$,
544 Nitpick looks for all counterexamples that can be built using at most 10
547 Let's see with an example involving \textit{hd} (which returns the first element
548 of a list) and $@$ (which concatenates two lists):
551 \textbf{lemma} ``$\textit{hd}~(\textit{xs} \mathbin{@} [y, y]) = \textit{hd}~\textit{xs}$'' \\
552 \textbf{nitpick} \\[2\smallskipamount]
553 \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
554 \hbox{}\qquad Free variables: \nopagebreak \\
555 \hbox{}\qquad\qquad $\textit{xs} = []$ \\
556 \hbox{}\qquad\qquad $\textit{y} = a_1$
559 To see why the counterexample is genuine, we enable \textit{show\_consts}
560 and \textit{show\_\allowbreak datatypes}:
563 {\slshape Datatype:} \\
564 \hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_1],\, [a_1, a_1],\, \unr\}$ \\
565 {\slshape Constants:} \\
566 \hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_1, a_1])$ \\
567 \hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_1] := a_1,\> [a_1, a_1] := a_1)$
570 Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value,
573 The second constant, $\lambda x_1.\; x_1 \mathbin{@} [y, y]$, is simply the
574 append operator whose second argument is fixed to be $[y, y]$. Appending $[a_1,
575 a_1]$ to $[a_1]$ would normally give $[a_1, a_1, a_1]$, but this value is not
576 representable in the subset of $'a$~\textit{list} considered by Nitpick, which
577 is shown under the ``Datatype'' heading; hence the result is $\unk$. Similarly,
578 appending $[a_1, a_1]$ to itself gives $\unk$.
580 Given \textit{card}~$'a = 3$ and \textit{card}~$'a~\textit{list} = 3$, Nitpick
581 considers the following subsets:
583 \kern-.5\smallskipamount %% TYPESETTING
587 $\{[],\, [a_1],\, [a_2]\}$; \\
588 $\{[],\, [a_1],\, [a_3]\}$; \\
589 $\{[],\, [a_2],\, [a_3]\}$; \\
590 $\{[],\, [a_1],\, [a_1, a_1]\}$; \\
591 $\{[],\, [a_1],\, [a_2, a_1]\}$; \\
592 $\{[],\, [a_1],\, [a_3, a_1]\}$; \\
593 $\{[],\, [a_2],\, [a_1, a_2]\}$; \\
594 $\{[],\, [a_2],\, [a_2, a_2]\}$; \\
595 $\{[],\, [a_2],\, [a_3, a_2]\}$; \\
596 $\{[],\, [a_3],\, [a_1, a_3]\}$; \\
597 $\{[],\, [a_3],\, [a_2, a_3]\}$; \\
598 $\{[],\, [a_3],\, [a_3, a_3]\}$.
602 \kern-2\smallskipamount %% TYPESETTING
604 All subterm-closed subsets of $'a~\textit{list}$ consisting of three values
605 are listed and only those. As an example of a non-subterm-closed subset,
606 consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_2]\}$, and observe
607 that $[a_1, a_2]$ (i.e., $a_1 \mathbin{\#} [a_2]$) has $[a_2] \notin
608 \mathcal{S}$ as a subterm.
610 Here's another m\"ochtegern-lemma that Nitpick can refute without a blink:
613 \textbf{lemma} ``$\lbrakk \textit{length}~\textit{xs} = 1;\> \textit{length}~\textit{ys} = 1
614 \rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$''
616 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
617 \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
618 \hbox{}\qquad Free variables: \nopagebreak \\
619 \hbox{}\qquad\qquad $\textit{xs} = [a_1]$ \\
620 \hbox{}\qquad\qquad $\textit{ys} = [a_2]$ \\
621 \hbox{}\qquad Datatypes: \\
622 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
623 \hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_1],\, [a_2],\, \unr\}$
626 Because datatypes are approximated using a three-valued logic, there is usually
627 no need to systematically enumerate cardinalities: If Nitpick cannot find a
628 genuine counterexample for \textit{card}~$'a~\textit{list}$~= 10, it is very
629 unlikely that one could be found for smaller cardinalities.
631 \subsection{Typedefs, Quotient Types, Records, Rationals, and Reals}
632 \label{typedefs-quotient-types-records-rationals-and-reals}
634 Nitpick generally treats types declared using \textbf{typedef} as datatypes
635 whose single constructor is the corresponding \textit{Abs\_\kern.1ex} function.
639 \textbf{typedef}~\textit{three} = ``$\{0\Colon\textit{nat},\, 1,\, 2\}$'' \\
640 \textbf{by}~\textit{blast} \\[2\smallskipamount]
641 \textbf{definition}~$A \mathbin{\Colon} \textit{three}$ \textbf{where} ``\kern-.1em$A \,\equiv\, \textit{Abs\_\allowbreak three}~0$'' \\
642 \textbf{definition}~$B \mathbin{\Colon} \textit{three}$ \textbf{where} ``$B \,\equiv\, \textit{Abs\_three}~1$'' \\
643 \textbf{definition}~$C \mathbin{\Colon} \textit{three}$ \textbf{where} ``$C \,\equiv\, \textit{Abs\_three}~2$'' \\[2\smallskipamount]
644 \textbf{lemma} ``$\lbrakk P~A;\> P~B\rbrakk \,\Longrightarrow\, P~x$'' \\
645 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
646 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
647 \hbox{}\qquad Free variables: \nopagebreak \\
648 \hbox{}\qquad\qquad $P = \{\Abs{0},\, \Abs{1}\}$ \\
649 \hbox{}\qquad\qquad $x = \Abs{2}$ \\
650 \hbox{}\qquad Datatypes: \\
651 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
652 \hbox{}\qquad\qquad $\textit{three} = \{\Abs{0},\, \Abs{1},\, \Abs{2},\, \unr\}$
655 In the output above, $\Abs{n}$ abbreviates $\textit{Abs\_three}~n$.
657 Quotient types are handled in much the same way. The following fragment defines
658 the integer type \textit{my\_int} by encoding the integer $x$ by a pair of
659 natural numbers $(m, n)$ such that $x + n = m$:
662 \textbf{fun} \textit{my\_int\_rel} \textbf{where} \\
663 ``$\textit{my\_int\_rel}~(x,\, y)~(u,\, v) = (x + v = u + y)$'' \\[2\smallskipamount]
665 \textbf{quotient\_type}~\textit{my\_int} = ``$\textit{nat} \times \textit{nat\/}$''$\;{/}\;$\textit{my\_int\_rel} \\
666 \textbf{by}~(\textit{auto simp add\/}:\ \textit{equivp\_def expand\_fun\_eq}) \\[2\smallskipamount]
668 \textbf{definition}~\textit{add\_raw}~\textbf{where} \\
669 ``$\textit{add\_raw} \,\equiv\, \lambda(x,\, y)~(u,\, v).\; (x + (u\Colon\textit{nat}), y + (v\Colon\textit{nat}))$'' \\[2\smallskipamount]
671 \textbf{quotient\_definition} ``$\textit{add\/}\Colon\textit{my\_int} \Rightarrow \textit{my\_int} \Rightarrow \textit{my\_int\/}$'' \textbf{is} \textit{add\_raw} \\[2\smallskipamount]
673 \textbf{lemma} ``$\textit{add}~x~y = \textit{add}~x~x$'' \\
674 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
675 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
676 \hbox{}\qquad Free variables: \nopagebreak \\
677 \hbox{}\qquad\qquad $x = \Abs{(0,\, 0)}$ \\
678 \hbox{}\qquad\qquad $y = \Abs{(1,\, 0)}$ \\
679 \hbox{}\qquad Datatypes: \\
680 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, \unr\}$ \\
681 \hbox{}\qquad\qquad $\textit{nat} \times \textit{nat}~[\textsl{boxed\/}] = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
682 \hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(1,\, 0)},\> \unr\}$
685 In the counterexample, $\Abs{(0,\, 0)}$ and $\Abs{(1,\, 0)}$ represent the
686 integers $0$ and $1$, respectively. Other representants would have been
687 possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$. If we are going to
688 use \textit{my\_int} extensively, it pays off to install a term postprocessor
689 that converts the pair notation to the standard mathematical notation:
692 $\textbf{ML}~\,\{{*} \\
694 %& ({*}~\,\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \\[-2pt]
695 %& \phantom{(*}~\,{\rightarrow}\;\textit{term}~\,{*}) \\[-2pt]
696 & \textbf{fun}\,~\textit{my\_int\_postproc}~\_~\_~\_~T~(\textit{Const}~\_~\$~(\textit{Const}~\_~\$~\textit{t1}~\$~\textit{t2\/})) = {} \\[-2pt]
697 & \phantom{fun}\,~\textit{HOLogic.mk\_number}~T~(\textit{snd}~(\textit{HOLogic.dest\_number~t1}) \\[-2pt]
698 & \phantom{fun\,~\textit{HOLogic.mk\_number}~T~(}{-}~\textit{snd}~(\textit{HOLogic.dest\_number~t2\/})) \\[-2pt]
699 & \phantom{fun}\!{\mid}\,~\textit{my\_int\_postproc}~\_~\_~\_~\_~t = t \\[-2pt]
700 {*}\}\end{aligned}$ \\[2\smallskipamount]
701 $\textbf{setup}~\,\{{*} \\
703 & \textit{Nitpick.register\_term\_postprocessor}~\!\begin{aligned}[t]
704 & @\{\textrm{typ}~\textit{my\_int}\}~\textit{my\_int\_postproc}\end{aligned} \\[-2pt]
708 Records are also handled as datatypes with a single constructor:
711 \textbf{record} \textit{point} = \\
712 \hbox{}\quad $\textit{Xcoord} \mathbin{\Colon} \textit{int}$ \\
713 \hbox{}\quad $\textit{Ycoord} \mathbin{\Colon} \textit{int}$ \\[2\smallskipamount]
714 \textbf{lemma} ``$\textit{Xcoord}~(p\Colon\textit{point}) = \textit{Xcoord}~(q\Colon\textit{point})$'' \\
715 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
716 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
717 \hbox{}\qquad Free variables: \nopagebreak \\
718 \hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
719 \hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
720 \hbox{}\qquad Datatypes: \\
721 \hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, \unr\}$ \\
722 \hbox{}\qquad\qquad $\textit{point} = \{\!\begin{aligned}[t]
723 & \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr, \\[-2pt] %% TYPESETTING
724 & \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
727 Finally, Nitpick provides rudimentary support for rationals and reals using a
731 \textbf{lemma} ``$4 * x + 3 * (y\Colon\textit{real}) \not= 1/2$'' \\
732 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
733 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
734 \hbox{}\qquad Free variables: \nopagebreak \\
735 \hbox{}\qquad\qquad $x = 1/2$ \\
736 \hbox{}\qquad\qquad $y = -1/2$ \\
737 \hbox{}\qquad Datatypes: \\
738 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, 3,\, 4,\, 5,\, 6,\, 7,\, \unr\}$ \\
739 \hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, 2,\, 3,\, 4,\, -3,\, -2,\, -1,\, \unr\}$ \\
740 \hbox{}\qquad\qquad $\textit{real} = \{1,\, 0,\, 4,\, -3/2,\, 3,\, 2,\, 1/2,\, -1/2,\, \unr\}$
743 \subsection{Inductive and Coinductive Predicates}
744 \label{inductive-and-coinductive-predicates}
746 Inductively defined predicates (and sets) are particularly problematic for
747 counterexample generators. They can make Quickcheck~\cite{berghofer-nipkow-2004}
748 loop forever and Refute~\cite{weber-2008} run out of resources. The crux of
749 the problem is that they are defined using a least fixed point construction.
751 Nitpick's philosophy is that not all inductive predicates are equal. Consider
752 the \textit{even} predicate below:
755 \textbf{inductive}~\textit{even}~\textbf{where} \\
756 ``\textit{even}~0'' $\,\mid$ \\
757 ``\textit{even}~$n\,\Longrightarrow\, \textit{even}~(\textit{Suc}~(\textit{Suc}~n))$''
760 This predicate enjoys the desirable property of being well-founded, which means
761 that the introduction rules don't give rise to infinite chains of the form
764 $\cdots\,\Longrightarrow\, \textit{even}~k''
765 \,\Longrightarrow\, \textit{even}~k'
766 \,\Longrightarrow\, \textit{even}~k.$
769 For \textit{even}, this is obvious: Any chain ending at $k$ will be of length
773 $\textit{even}~0\,\Longrightarrow\, \textit{even}~2\,\Longrightarrow\, \cdots
774 \,\Longrightarrow\, \textit{even}~(k - 2)
775 \,\Longrightarrow\, \textit{even}~k.$
778 Wellfoundedness is desirable because it enables Nitpick to use a very efficient
779 fixed point computation.%
780 \footnote{If an inductive predicate is
781 well-founded, then it has exactly one fixed point, which is simultaneously the
782 least and the greatest fixed point. In these circumstances, the computation of
783 the least fixed point amounts to the computation of an arbitrary fixed point,
784 which can be performed using a straightforward recursive equation.}
785 Moreover, Nitpick can prove wellfoundedness of most well-founded predicates,
786 just as Isabelle's \textbf{function} package usually discharges termination
787 proof obligations automatically.
789 Let's try an example:
792 \textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
793 \textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
794 \slshape The inductive predicate ``\textit{even}'' was proved well-founded.
795 Nitpick can compute it efficiently. \\[2\smallskipamount]
797 \hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
798 Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
799 \hbox{}\qquad Empty assignment \\[2\smallskipamount]
800 Nitpick could not find a better counterexample. \\[2\smallskipamount]
804 No genuine counterexample is possible because Nitpick cannot rule out the
805 existence of a natural number $n \ge 50$ such that both $\textit{even}~n$ and
806 $\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the
807 existential quantifier:
810 \textbf{lemma} ``$\exists n \mathbin{\le} 49.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
811 \textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}] \\[2\smallskipamount]
812 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
813 \hbox{}\qquad Empty assignment
816 So far we were blessed by the wellfoundedness of \textit{even}. What happens if
817 we use the following definition instead?
820 \textbf{inductive} $\textit{even}'$ \textbf{where} \\
821 ``$\textit{even}'~(0{\Colon}\textit{nat})$'' $\,\mid$ \\
822 ``$\textit{even}'~2$'' $\,\mid$ \\
823 ``$\lbrakk\textit{even}'~m;\> \textit{even}'~n\rbrakk \,\Longrightarrow\, \textit{even}'~(m + n)$''
826 This definition is not well-founded: From $\textit{even}'~0$ and
827 $\textit{even}'~0$, we can derive that $\textit{even}'~0$. Nonetheless, the
828 predicates $\textit{even}$ and $\textit{even}'$ are equivalent.
830 Let's check a property involving $\textit{even}'$. To make up for the
831 foreseeable computational hurdles entailed by non-wellfoundedness, we decrease
832 \textit{nat}'s cardinality to a mere 10:
835 \textbf{lemma}~``$\exists n \in \{0, 2, 4, 6, 8\}.\;
836 \lnot\;\textit{even}'~n$'' \\
837 \textbf{nitpick}~[\textit{card nat}~= 10,\, \textit{verbose},\, \textit{show\_consts}] \\[2\smallskipamount]
839 The inductive predicate ``$\textit{even}'\!$'' could not be proved well-founded.
840 Nitpick might need to unroll it. \\[2\smallskipamount]
842 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 0; \\
843 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 1; \\
844 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2; \\
845 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 4; \\
846 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 8; \\
847 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 9. \\[2\smallskipamount]
848 Nitpick found a counterexample for \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2: \\[2\smallskipamount]
849 \hbox{}\qquad Constant: \nopagebreak \\
850 \hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t]
851 & 2 := \{0, 2, 4, 6, 8, 1^\Q, 3^\Q, 5^\Q, 7^\Q, 9^\Q\}, \\[-2pt]
852 & 1 := \{0, 2, 4, 1^\Q, 3^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\}, \\[-2pt]
853 & 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\[2\smallskipamount]
857 Nitpick's output is very instructive. First, it tells us that the predicate is
858 unrolled, meaning that it is computed iteratively from the empty set. Then it
859 lists six scopes specifying different bounds on the numbers of iterations:\ 0,
862 The output also shows how each iteration contributes to $\textit{even}'$. The
863 notation $\lambda i.\; \textit{even}'$ indicates that the value of the
864 predicate depends on an iteration counter. Iteration 0 provides the basis
865 elements, $0$ and $2$. Iteration 1 contributes $4$ ($= 2 + 2$). Iteration 2
866 throws $6$ ($= 2 + 4 = 4 + 2$) and $8$ ($= 4 + 4$) into the mix. Further
867 iterations would not contribute any new elements.
869 Some values are marked with superscripted question
870 marks~(`\lower.2ex\hbox{$^\Q$}'). These are the elements for which the
871 predicate evaluates to $\unk$. Thus, $\textit{even}'$ evaluates to either
872 \textit{True} or $\unk$, never \textit{False}.
874 When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, and 24
875 iterations. However, these numbers are bounded by the cardinality of the
876 predicate's domain. With \textit{card~nat}~= 10, no more than 9 iterations are
877 ever needed to compute the value of a \textit{nat} predicate. You can specify
878 the number of iterations using the \textit{iter} option, as explained in
879 \S\ref{scope-of-search}.
881 In the next formula, $\textit{even}'$ occurs both positively and negatively:
884 \textbf{lemma} ``$\textit{even}'~(n - 2) \,\Longrightarrow\, \textit{even}'~n$'' \\
885 \textbf{nitpick} [\textit{card nat} = 10, \textit{show\_consts}] \\[2\smallskipamount]
886 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
887 \hbox{}\qquad Free variable: \nopagebreak \\
888 \hbox{}\qquad\qquad $n = 1$ \\
889 \hbox{}\qquad Constants: \nopagebreak \\
890 \hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t]
891 & 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\
892 \hbox{}\qquad\qquad $\textit{even}' \subseteq \{0, 2, 4, 6, 8, \unr\}$
895 Notice the special constraint $\textit{even}' \subseteq \{0,\, 2,\, 4,\, 6,\,
896 8,\, \unr\}$ in the output, whose right-hand side represents an arbitrary
897 fixed point (not necessarily the least one). It is used to falsify
898 $\textit{even}'~n$. In contrast, the unrolled predicate is used to satisfy
899 $\textit{even}'~(n - 2)$.
901 Coinductive predicates are handled dually. For example:
904 \textbf{coinductive} \textit{nats} \textbf{where} \\
905 ``$\textit{nats}~(x\Colon\textit{nat}) \,\Longrightarrow\, \textit{nats}~x$'' \\[2\smallskipamount]
906 \textbf{lemma} ``$\textit{nats} = \{0, 1, 2, 3, 4\}$'' \\
907 \textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
908 \slshape Nitpick found a counterexample:
909 \\[2\smallskipamount]
910 \hbox{}\qquad Constants: \nopagebreak \\
911 \hbox{}\qquad\qquad $\lambda i.\; \textit{nats} = \undef(0 := \{\!\begin{aligned}[t]
912 & 0^\Q, 1^\Q, 2^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q, \\[-2pt]
913 & \unr\})\end{aligned}$ \\
914 \hbox{}\qquad\qquad $nats \supseteq \{9, 5^\Q, 6^\Q, 7^\Q, 8^\Q, \unr\}$
917 As a special case, Nitpick uses Kodkod's transitive closure operator to encode
918 negative occurrences of non-well-founded ``linear inductive predicates,'' i.e.,
919 inductive predicates for which each the predicate occurs in at most one
920 assumption of each introduction rule. For example:
923 \textbf{inductive} \textit{odd} \textbf{where} \\
924 ``$\textit{odd}~1$'' $\,\mid$ \\
925 ``$\lbrakk \textit{odd}~m;\>\, \textit{even}~n\rbrakk \,\Longrightarrow\, \textit{odd}~(m + n)$'' \\[2\smallskipamount]
926 \textbf{lemma}~``$\textit{odd}~n \,\Longrightarrow\, \textit{odd}~(n - 2)$'' \\
927 \textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
928 \slshape Nitpick found a counterexample:
929 \\[2\smallskipamount]
930 \hbox{}\qquad Free variable: \nopagebreak \\
931 \hbox{}\qquad\qquad $n = 1$ \\
932 \hbox{}\qquad Constants: \nopagebreak \\
933 \hbox{}\qquad\qquad $\textit{even} = \{0, 2, 4, 6, 8, \unr\}$ \\
934 \hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = \{1, \unr\}$ \\
935 \hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \!
937 & \{(0, 0), (0, 2), (0, 4), (0, 6), (0, 8), (1, 1), (1, 3), (1, 5), \\[-2pt]
938 & \phantom{\{} (1, 7), (1, 9), (2, 2), (2, 4), (2, 6), (2, 8), (3, 3),
940 & \phantom{\{} (3, 7), (3, 9), (4, 4), (4, 6), (4, 8), (5, 5), (5, 7), (5, 9), \\[-2pt]
941 & \phantom{\{} (6, 6), (6, 8), (7, 7), (7, 9), (8, 8), (9, 9), \unr\}\end{aligned}$ \\
942 \hbox{}\qquad\qquad $\textit{odd} \subseteq \{1, 3, 5, 7, 9, 8^\Q, \unr\}$
946 In the output, $\textit{odd}_{\textrm{base}}$ represents the base elements and
947 $\textit{odd}_{\textrm{step}}$ is a transition relation that computes new
948 elements from known ones. The set $\textit{odd}$ consists of all the values
949 reachable through the reflexive transitive closure of
950 $\textit{odd}_{\textrm{step}}$ starting with any element from
951 $\textit{odd}_{\textrm{base}}$, namely 1, 3, 5, 7, and 9. Using Kodkod's
952 transitive closure to encode linear predicates is normally either more thorough
953 or more efficient than unrolling (depending on the value of \textit{iter}), but
954 for those cases where it isn't you can disable it by passing the
955 \textit{dont\_star\_linear\_preds} option.
957 \subsection{Coinductive Datatypes}
958 \label{coinductive-datatypes}
960 While Isabelle regrettably lacks a high-level mechanism for defining coinductive
961 datatypes, the \textit{Coinductive\_List} theory from Andreas Lochbihler's
962 \textit{Coinductive} AFP entry \cite{lochbihler-2010} provides a coinductive
963 ``lazy list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick
964 supports these lazy lists seamlessly and provides a hook, described in
965 \S\ref{registration-of-coinductive-datatypes}, to register custom coinductive
968 (Co)intuitively, a coinductive datatype is similar to an inductive datatype but
969 allows infinite objects. Thus, the infinite lists $\textit{ps}$ $=$ $[a, a, a,
970 \ldots]$, $\textit{qs}$ $=$ $[a, b, a, b, \ldots]$, and $\textit{rs}$ $=$ $[0,
971 1, 2, 3, \ldots]$ can be defined as lazy lists using the
972 $\textit{LNil}\mathbin{\Colon}{'}a~\textit{llist}$ and
973 $\textit{LCons}\mathbin{\Colon}{'}a \mathbin{\Rightarrow} {'}a~\textit{llist}
974 \mathbin{\Rightarrow} {'}a~\textit{llist}$ constructors.
976 Although it is otherwise no friend of infinity, Nitpick can find counterexamples
977 involving cyclic lists such as \textit{ps} and \textit{qs} above as well as
981 \textbf{lemma} ``$\textit{xs} \not= \textit{LCons}~a~\textit{xs}$'' \\
982 \textbf{nitpick} \\[2\smallskipamount]
983 \slshape Nitpick found a counterexample for {\itshape card}~$'a$ = 1: \\[2\smallskipamount]
984 \hbox{}\qquad Free variables: \nopagebreak \\
985 \hbox{}\qquad\qquad $\textit{a} = a_1$ \\
986 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$
989 The notation $\textrm{THE}~\omega.\; \omega = t(\omega)$ stands
990 for the infinite term $t(t(t(\ldots)))$. Hence, \textit{xs} is simply the
991 infinite list $[a_1, a_1, a_1, \ldots]$.
993 The next example is more interesting:
996 \textbf{lemma}~``$\lbrakk\textit{xs} = \textit{LCons}~a~\textit{xs};\>\,
997 \textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
998 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
999 \slshape The type ``\kern1pt$'a$'' passed the monotonicity test. Nitpick might be able to skip
1000 some scopes. \\[2\smallskipamount]
1002 \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 1,
1003 and \textit{bisim\_depth}~= 0. \\
1004 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1005 \hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 8,
1006 and \textit{bisim\_depth}~= 7. \\[2\smallskipamount]
1007 Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
1008 \textit{card}~``\kern1pt$'a~\textit{list\/}$''~= 2, and \textit{bisim\_\allowbreak
1010 \\[2\smallskipamount]
1011 \hbox{}\qquad Free variables: \nopagebreak \\
1012 \hbox{}\qquad\qquad $\textit{a} = a_1$ \\
1013 \hbox{}\qquad\qquad $\textit{b} = a_2$ \\
1014 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
1015 \hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount]
1019 The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas
1020 $\textit{ys}$ is $[a_2, a_1, a_1, a_1, \ldots]$, i.e., a lasso-shaped list with
1021 $[a_2]$ as its stem and $[a_1]$ as its cycle. In general, the list segment
1022 within the scope of the {THE} binder corresponds to the lasso's cycle, whereas
1023 the segment leading to the binder is the stem.
1025 A salient property of coinductive datatypes is that two objects are considered
1026 equal if and only if they lead to the same observations. For example, the lazy
1027 lists $\textrm{THE}~\omega.\; \omega =
1028 \textit{LCons}~a~(\textit{LCons}~b~\omega)$ and
1029 $\textit{LCons}~a~(\textrm{THE}~\omega.\; \omega =
1030 \textit{LCons}~b~(\textit{LCons}~a~\omega))$ are identical, because both lead
1031 to the sequence of observations $a$, $b$, $a$, $b$, \hbox{\ldots} (or,
1032 equivalently, both encode the infinite list $[a, b, a, b, \ldots]$). This
1033 concept of equality for coinductive datatypes is called bisimulation and is
1034 defined coinductively.
1036 Internally, Nitpick encodes the coinductive bisimilarity predicate as part of
1037 the Kodkod problem to ensure that distinct objects lead to different
1038 observations. This precaution is somewhat expensive and often unnecessary, so it
1039 can be disabled by setting the \textit{bisim\_depth} option to $-1$. The
1040 bisimilarity check is then performed \textsl{after} the counterexample has been
1041 found to ensure correctness. If this after-the-fact check fails, the
1042 counterexample is tagged as ``quasi genuine'' and Nitpick recommends to try
1043 again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the
1044 check for the previous example saves approximately 150~milli\-seconds; the speed
1045 gains can be more significant for larger scopes.
1047 The next formula illustrates the need for bisimilarity (either as a Kodkod
1048 predicate or as an after-the-fact check) to prevent spurious counterexamples:
1051 \textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
1052 \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
1053 \textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
1054 \slshape Nitpick found a quasi genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
1055 \hbox{}\qquad Free variables: \nopagebreak \\
1056 \hbox{}\qquad\qquad $a = a_1$ \\
1057 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
1058 \textit{LCons}~a_1~\omega$ \\
1059 \hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
1060 \hbox{}\qquad Codatatype:\strut \nopagebreak \\
1061 \hbox{}\qquad\qquad $'a~\textit{llist} =
1062 \{\!\begin{aligned}[t]
1063 & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega, \\[-2pt]
1064 & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega,\> \unr\}\end{aligned}$
1065 \\[2\smallskipamount]
1066 Try again with ``\textit{bisim\_depth}'' set to a nonnegative value to confirm
1067 that the counterexample is genuine. \\[2\smallskipamount]
1068 {\upshape\textbf{nitpick}} \\[2\smallskipamount]
1069 \slshape Nitpick found no counterexample.
1072 In the first \textbf{nitpick} invocation, the after-the-fact check discovered
1073 that the two known elements of type $'a~\textit{llist}$ are bisimilar.
1075 A compromise between leaving out the bisimilarity predicate from the Kodkod
1076 problem and performing the after-the-fact check is to specify a lower
1077 nonnegative \textit{bisim\_depth} value than the default one provided by
1078 Nitpick. In general, a value of $K$ means that Nitpick will require all lists to
1079 be distinguished from each other by their prefixes of length $K$. Be aware that
1080 setting $K$ to a too low value can overconstrain Nitpick, preventing it from
1081 finding any counterexamples.
1086 Nitpick normally maps function and product types directly to the corresponding
1087 Kodkod concepts. As a consequence, if $'a$ has cardinality 3 and $'b$ has
1088 cardinality 4, then $'a \times {'}b$ has cardinality 12 ($= 4 \times 3$) and $'a
1089 \Rightarrow {'}b$ has cardinality 64 ($= 4^3$). In some circumstances, it pays
1090 off to treat these types in the same way as plain datatypes, by approximating
1091 them by a subset of a given cardinality. This technique is called ``boxing'' and
1092 is particularly useful for functions passed as arguments to other functions, for
1093 high-arity functions, and for large tuples. Under the hood, boxing involves
1094 wrapping occurrences of the types $'a \times {'}b$ and $'a \Rightarrow {'}b$ in
1095 isomorphic datatypes, as can be seen by enabling the \textit{debug} option.
1097 To illustrate boxing, we consider a formalization of $\lambda$-terms represented
1098 using de Bruijn's notation:
1101 \textbf{datatype} \textit{tm} = \textit{Var}~\textit{nat}~$\mid$~\textit{Lam}~\textit{tm} $\mid$ \textit{App~tm~tm}
1104 The $\textit{lift}~t~k$ function increments all variables with indices greater
1105 than or equal to $k$ by one:
1108 \textbf{primrec} \textit{lift} \textbf{where} \\
1109 ``$\textit{lift}~(\textit{Var}~j)~k = \textit{Var}~(\textrm{if}~j < k~\textrm{then}~j~\textrm{else}~j + 1)$'' $\mid$ \\
1110 ``$\textit{lift}~(\textit{Lam}~t)~k = \textit{Lam}~(\textit{lift}~t~(k + 1))$'' $\mid$ \\
1111 ``$\textit{lift}~(\textit{App}~t~u)~k = \textit{App}~(\textit{lift}~t~k)~(\textit{lift}~u~k)$''
1114 The $\textit{loose}~t~k$ predicate returns \textit{True} if and only if
1115 term $t$ has a loose variable with index $k$ or more:
1118 \textbf{primrec}~\textit{loose} \textbf{where} \\
1119 ``$\textit{loose}~(\textit{Var}~j)~k = (j \ge k)$'' $\mid$ \\
1120 ``$\textit{loose}~(\textit{Lam}~t)~k = \textit{loose}~t~(\textit{Suc}~k)$'' $\mid$ \\
1121 ``$\textit{loose}~(\textit{App}~t~u)~k = (\textit{loose}~t~k \mathrel{\lor} \textit{loose}~u~k)$''
1124 Next, the $\textit{subst}~\sigma~t$ function applies the substitution $\sigma$
1128 \textbf{primrec}~\textit{subst} \textbf{where} \\
1129 ``$\textit{subst}~\sigma~(\textit{Var}~j) = \sigma~j$'' $\mid$ \\
1130 ``$\textit{subst}~\sigma~(\textit{Lam}~t) = {}$\phantom{''} \\
1131 \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$ \\
1132 ``$\textit{subst}~\sigma~(\textit{App}~t~u) = \textit{App}~(\textit{subst}~\sigma~t)~(\textit{subst}~\sigma~u)$''
1135 A substitution is a function that maps variable indices to terms. Observe that
1136 $\sigma$ is a function passed as argument and that Nitpick can't optimize it
1137 away, because the recursive call for the \textit{Lam} case involves an altered
1138 version. Also notice the \textit{lift} call, which increments the variable
1139 indices when moving under a \textit{Lam}.
1141 A reasonable property to expect of substitution is that it should leave closed
1142 terms unchanged. Alas, even this simple property does not hold:
1145 \textbf{lemma}~``$\lnot\,\textit{loose}~t~0 \,\Longrightarrow\, \textit{subst}~\sigma~t = t$'' \\
1146 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
1148 Trying 8 scopes: \nopagebreak \\
1149 \hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 1; \\
1150 \hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 2; \\
1151 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1152 \hbox{}\qquad \textit{card~nat}~= 8, \textit{card tm}~= 8, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 8. \\[2\smallskipamount]
1153 Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6,
1154 and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm}$''~= 6: \\[2\smallskipamount]
1155 \hbox{}\qquad Free variables: \nopagebreak \\
1156 \hbox{}\qquad\qquad $\sigma = \undef(\!\begin{aligned}[t]
1157 & 0 := \textit{Var}~0,\>
1158 1 := \textit{Var}~0,\>
1159 2 := \textit{Var}~0, \\[-2pt]
1160 & 3 := \textit{Var}~0,\>
1161 4 := \textit{Var}~0,\>
1162 5 := \textit{Var}~0)\end{aligned}$ \\
1163 \hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount]
1164 Total time: $4679$ ms.
1167 Using \textit{eval}, we find out that $\textit{subst}~\sigma~t =
1168 \textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional
1169 $\lambda$-term notation, $t$~is
1170 $\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is $\lambda x\, y.\> y$.
1171 The bug is in \textit{subst\/}: The $\textit{lift}~(\sigma~m)~1$ call should be
1172 replaced with $\textit{lift}~(\sigma~m)~0$.
1174 An interesting aspect of Nitpick's verbose output is that it assigned inceasing
1175 cardinalities from 1 to 8 to the type $\textit{nat} \Rightarrow \textit{tm}$.
1176 For the formula of interest, knowing 6 values of that type was enough to find
1177 the counterexample. Without boxing, $46\,656$ ($= 6^6$) values must be
1178 considered, a hopeless undertaking:
1181 \textbf{nitpick} [\textit{dont\_box}] \\[2\smallskipamount]
1182 {\slshape Nitpick ran out of time after checking 4 of 8 scopes.}
1186 Boxing can be enabled or disabled globally or on a per-type basis using the
1187 \textit{box} option. Nitpick usually performs reasonable choices about which
1188 types should be boxed, but option tweaking sometimes helps. A related optimization,
1189 ``finalization,'' attempts to wrap functions that constant at all but finitely
1190 many points (e.g., finite sets); see the documentation for the \textit{finalize}
1191 option in \S\ref{scope-of-search} for details.
1195 \subsection{Scope Monotonicity}
1196 \label{scope-monotonicity}
1198 The \textit{card} option (together with \textit{iter}, \textit{bisim\_depth},
1199 and \textit{max}) controls which scopes are actually tested. In general, to
1200 exhaust all models below a certain cardinality bound, the number of scopes that
1201 Nitpick must consider increases exponentially with the number of type variables
1202 (and \textbf{typedecl}'d types) occurring in the formula. Given the default
1203 cardinality specification of 1--8, no fewer than $8^4 = 4096$ scopes must be
1204 considered for a formula involving $'a$, $'b$, $'c$, and $'d$.
1206 Fortunately, many formulas exhibit a property called \textsl{scope
1207 monotonicity}, meaning that if the formula is falsifiable for a given scope,
1208 it is also falsifiable for all larger scopes \cite[p.~165]{jackson-2006}.
1210 Consider the formula
1213 \textbf{lemma}~``$\textit{length~xs} = \textit{length~ys} \,\Longrightarrow\, \textit{rev}~(\textit{zip~xs~ys}) = \textit{zip~xs}~(\textit{rev~ys})$''
1216 where \textit{xs} is of type $'a~\textit{list}$ and \textit{ys} is of type
1217 $'b~\textit{list}$. A priori, Nitpick would need to consider 512 scopes to
1218 exhaust the specification \textit{card}~= 1--8. However, our intuition tells us
1219 that any counterexample found with a small scope would still be a counterexample
1220 in a larger scope---by simply ignoring the fresh $'a$ and $'b$ values provided
1221 by the larger scope. Nitpick comes to the same conclusion after a careful
1222 inspection of the formula and the relevant definitions:
1225 \textbf{nitpick}~[\textit{verbose}] \\[2\smallskipamount]
1227 The types ``\kern1pt$'a$'' and ``\kern1pt$'b$'' passed the monotonicity test.
1228 Nitpick might be able to skip some scopes.
1229 \\[2\smallskipamount]
1231 \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1,
1232 \textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$
1233 \textit{list\/}''~= 1, \\
1234 \hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 1, and
1235 \textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 1. \\
1236 \hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2,
1237 \textit{card} \textit{nat}~= 2, \textit{card} ``$('a \times {'}b)$
1238 \textit{list\/}''~= 2, \\
1239 \hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 2, and
1240 \textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 2. \\
1241 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1242 \hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} $'b$~= 8,
1243 \textit{card} \textit{nat}~= 8, \textit{card} ``$('a \times {'}b)$
1244 \textit{list\/}''~= 8, \\
1245 \hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 8, and
1246 \textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 8.
1247 \\[2\smallskipamount]
1248 Nitpick found a counterexample for
1249 \textit{card} $'a$~= 5, \textit{card} $'b$~= 5,
1250 \textit{card} \textit{nat}~= 5, \textit{card} ``$('a \times {'}b)$
1251 \textit{list\/}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 5, and
1252 \textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 5:
1253 \\[2\smallskipamount]
1254 \hbox{}\qquad Free variables: \nopagebreak \\
1255 \hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\
1256 \hbox{}\qquad\qquad $\textit{ys} = [b_1, b_1]$ \\[2\smallskipamount]
1257 Total time: 1636 ms.
1260 In theory, it should be sufficient to test a single scope:
1263 \textbf{nitpick}~[\textit{card}~= 8]
1266 However, this is often less efficient in practice and may lead to overly complex
1269 If the monotonicity check fails but we believe that the formula is monotonic (or
1270 we don't mind missing some counterexamples), we can pass the
1271 \textit{mono} option. To convince yourself that this option is risky,
1272 simply consider this example from \S\ref{skolemization}:
1275 \textbf{lemma} ``$\exists g.\; \forall x\Colon 'b.~g~(f~x) = x
1276 \,\Longrightarrow\, \forall y\Colon {'}a.\; \exists x.~y = f~x$'' \\
1277 \textbf{nitpick} [\textit{mono}] \\[2\smallskipamount]
1278 {\slshape Nitpick found no counterexample.} \\[2\smallskipamount]
1279 \textbf{nitpick} \\[2\smallskipamount]
1281 Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\
1282 \hbox{}\qquad $\vdots$
1285 (It turns out the formula holds if and only if $\textit{card}~'a \le
1286 \textit{card}~'b$.) Although this is rarely advisable, the automatic
1287 monotonicity checks can be disabled by passing \textit{non\_mono}
1288 (\S\ref{optimizations}).
1290 As insinuated in \S\ref{natural-numbers-and-integers} and
1291 \S\ref{inductive-datatypes}, \textit{nat}, \textit{int}, and inductive datatypes
1292 are normally monotonic and treated as such. The same is true for record types,
1293 \textit{rat}, \textit{real}, and some \textbf{typedef}'d types. Thus, given the
1294 cardinality specification 1--8, a formula involving \textit{nat}, \textit{int},
1295 \textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
1296 consider only 8~scopes instead of $32\,768$.
1298 \subsection{Inductive Properties}
1299 \label{inductive-properties}
1301 Inductive properties are a particular pain to prove, because the failure to
1302 establish an induction step can mean several things:
1305 \item The property is invalid.
1306 \item The property is valid but is too weak to support the induction step.
1307 \item The property is valid and strong enough; it's just that we haven't found
1311 Depending on which scenario applies, we would take the appropriate course of
1315 \item Repair the statement of the property so that it becomes valid.
1316 \item Generalize the property and/or prove auxiliary properties.
1317 \item Work harder on a proof.
1320 How can we distinguish between the three scenarios? Nitpick's normal mode of
1321 operation can often detect scenario 1, and Isabelle's automatic tactics help with
1322 scenario 3. Using appropriate techniques, it is also often possible to use
1323 Nitpick to identify scenario 2. Consider the following transition system,
1324 in which natural numbers represent states:
1327 \textbf{inductive\_set}~\textit{reach}~\textbf{where} \\
1328 ``$(4\Colon\textit{nat}) \in \textit{reach\/}$'' $\mid$ \\
1329 ``$\lbrakk n < 4;\> n \in \textit{reach\/}\rbrakk \,\Longrightarrow\, 3 * n + 1 \in \textit{reach\/}$'' $\mid$ \\
1330 ``$n \in \textit{reach} \,\Longrightarrow n + 2 \in \textit{reach\/}$''
1333 We will try to prove that only even numbers are reachable:
1336 \textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n$''
1339 Does this property hold? Nitpick cannot find a counterexample within 30 seconds,
1340 so let's attempt a proof by induction:
1343 \textbf{apply}~(\textit{induct~set}{:}~\textit{reach\/}) \\
1344 \textbf{apply}~\textit{auto}
1347 This leaves us in the following proof state:
1350 {\slshape goal (2 subgoals): \\
1351 \phantom{0}1. ${\bigwedge}n.\;\, \lbrakk n \in \textit{reach\/};\, n < 4;\, 2~\textsl{dvd}~n\rbrakk \,\Longrightarrow\, 2~\textsl{dvd}~\textit{Suc}~(3 * n)$ \\
1352 \phantom{0}2. ${\bigwedge}n.\;\, \lbrakk n \in \textit{reach\/};\, 2~\textsl{dvd}~n\rbrakk \,\Longrightarrow\, 2~\textsl{dvd}~\textit{Suc}~(\textit{Suc}~n)$
1356 If we run Nitpick on the first subgoal, it still won't find any
1357 counterexample; and yet, \textit{auto} fails to go further, and \textit{arith}
1358 is helpless. However, notice the $n \in \textit{reach}$ assumption, which
1359 strengthens the induction hypothesis but is not immediately usable in the proof.
1360 If we remove it and invoke Nitpick, this time we get a counterexample:
1363 \textbf{apply}~(\textit{thin\_tac}~``$n \in \textit{reach\/}$'') \\
1364 \textbf{nitpick} \\[2\smallskipamount]
1365 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1366 \hbox{}\qquad Skolem constant: \nopagebreak \\
1367 \hbox{}\qquad\qquad $n = 0$
1370 Indeed, 0 < 4, 2 divides 0, but 2 does not divide 1. We can use this information
1371 to strength the lemma:
1374 \textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \not= 0$''
1377 Unfortunately, the proof by induction still gets stuck, except that Nitpick now
1378 finds the counterexample $n = 2$. We generalize the lemma further to
1381 \textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \ge 4$''
1384 and this time \textit{arith} can finish off the subgoals.
1386 A similar technique can be employed for structural induction. The
1387 following mini formalization of full binary trees will serve as illustration:
1390 \textbf{datatype} $\kern1pt'a$~\textit{bin\_tree} = $\textit{Leaf}~{\kern1pt'a}$ $\mid$ $\textit{Branch}$ ``\kern1pt$'a$ \textit{bin\_tree}'' ``\kern1pt$'a$ \textit{bin\_tree}'' \\[2\smallskipamount]
1391 \textbf{primrec}~\textit{labels}~\textbf{where} \\
1392 ``$\textit{labels}~(\textit{Leaf}~a) = \{a\}$'' $\mid$ \\
1393 ``$\textit{labels}~(\textit{Branch}~t~u) = \textit{labels}~t \mathrel{\cup} \textit{labels}~u$'' \\[2\smallskipamount]
1394 \textbf{primrec}~\textit{swap}~\textbf{where} \\
1395 ``$\textit{swap}~(\textit{Leaf}~c)~a~b =$ \\
1396 \phantom{``}$(\textrm{if}~c = a~\textrm{then}~\textit{Leaf}~b~\textrm{else~if}~c = b~\textrm{then}~\textit{Leaf}~a~\textrm{else}~\textit{Leaf}~c)$'' $\mid$ \\
1397 ``$\textit{swap}~(\textit{Branch}~t~u)~a~b = \textit{Branch}~(\textit{swap}~t~a~b)~(\textit{swap}~u~a~b)$''
1400 The \textit{labels} function returns the set of labels occurring on leaves of a
1401 tree, and \textit{swap} exchanges two labels. Intuitively, if two distinct
1402 labels $a$ and $b$ occur in a tree $t$, they should also occur in the tree
1403 obtained by swapping $a$ and $b$:
1406 \textbf{lemma} $``\{a, b\} \subseteq \textit{labels}~t \,\Longrightarrow\, \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
1409 Nitpick can't find any counterexample, so we proceed with induction
1410 (this time favoring a more structured style):
1413 \textbf{proof}~(\textit{induct}~$t$) \\
1414 \hbox{}\quad \textbf{case}~\textit{Leaf}~\textbf{thus}~\textit{?case}~\textbf{by}~\textit{simp} \\
1416 \hbox{}\quad \textbf{case}~$(\textit{Branch}~t~u)$~\textbf{thus} \textit{?case}
1419 Nitpick can't find any counterexample at this point either, but it makes the
1420 following suggestion:
1424 Hint: To check that the induction hypothesis is general enough, try this command:
1425 \textbf{nitpick}~[\textit{non\_std}, \textit{show\_all}].
1428 If we follow the hint, we get a ``nonstandard'' counterexample for the step:
1431 \slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 3: \\[2\smallskipamount]
1432 \hbox{}\qquad Free variables: \nopagebreak \\
1433 \hbox{}\qquad\qquad $a = a_1$ \\
1434 \hbox{}\qquad\qquad $b = a_2$ \\
1435 \hbox{}\qquad\qquad $t = \xi_1$ \\
1436 \hbox{}\qquad\qquad $u = \xi_2$ \\
1437 \hbox{}\qquad Datatype: \nopagebreak \\
1438 \hbox{}\qquad\qquad $\alpha~\textit{btree} = \{\xi_1 \mathbin{=} \textit{Branch}~\xi_1~\xi_1,\> \xi_2 \mathbin{=} \textit{Branch}~\xi_2~\xi_2,\> \textit{Branch}~\xi_1~\xi_2\}$ \\
1439 \hbox{}\qquad {\slshape Constants:} \nopagebreak \\
1440 \hbox{}\qquad\qquad $\textit{labels} = \undef
1441 (\!\begin{aligned}[t]%
1442 & \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[-2pt]
1443 & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\
1444 \hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
1445 (\!\begin{aligned}[t]%
1446 & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
1447 & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
1448 The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
1449 even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
1452 Reading the Nitpick manual is a most excellent idea.
1453 But what's going on? The \textit{non\_std} option told the tool to look for
1454 nonstandard models of binary trees, which means that new ``nonstandard'' trees
1455 $\xi_1, \xi_2, \ldots$, are now allowed in addition to the standard trees
1456 generated by the \textit{Leaf} and \textit{Branch} constructors.%
1457 \footnote{Notice the similarity between allowing nonstandard trees here and
1458 allowing unreachable states in the preceding example (by removing the ``$n \in
1459 \textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
1460 set of objects over which the induction is performed while doing the step
1461 in order to test the induction hypothesis's strength.}
1462 Unlike standard trees, these new trees contain cycles. We will see later that
1463 every property of acyclic trees that can be proved without using induction also
1464 holds for cyclic trees. Hence,
1467 \textsl{If the induction
1468 hypothesis is strong enough, the induction step will hold even for nonstandard
1469 objects, and Nitpick won't find any nonstandard counterexample.}
1472 But here the tool find some nonstandard trees $t = \xi_1$
1473 and $u = \xi_2$ such that $a \notin \textit{labels}~t$, $b \in
1474 \textit{labels}~t$, $a \in \textit{labels}~u$, and $b \notin \textit{labels}~u$.
1475 Because neither tree contains both $a$ and $b$, the induction hypothesis tells
1476 us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
1477 and as a result we know nothing about the labels of the tree
1478 $\textit{swap}~(\textit{Branch}~t~u)~a~b$, which by definition equals
1479 $\textit{Branch}$ $(\textit{swap}~t~a~b)$ $(\textit{swap}~u~a~b)$, whose
1480 labels are $\textit{labels}$ $(\textit{swap}~t~a~b) \mathrel{\cup}
1481 \textit{labels}$ $(\textit{swap}~u~a~b)$.
1483 The solution is to ensure that we always know what the labels of the subtrees
1484 are in the inductive step, by covering the cases where $a$ and/or~$b$ is not in
1485 $t$ in the statement of the lemma:
1488 \textbf{lemma} ``$\textit{labels}~(\textit{swap}~t~a~b) = {}$ \\
1489 \phantom{\textbf{lemma} ``}$(\textrm{if}~a \in \textit{labels}~t~\textrm{then}$ \nopagebreak \\
1490 \phantom{\textbf{lemma} ``(\quad}$\textrm{if}~b \in \textit{labels}~t~\textrm{then}~\textit{labels}~t~\textrm{else}~(\textit{labels}~t - \{a\}) \mathrel{\cup} \{b\}$ \\
1491 \phantom{\textbf{lemma} ``(}$\textrm{else}$ \\
1492 \phantom{\textbf{lemma} ``(\quad}$\textrm{if}~b \in \textit{labels}~t~\textrm{then}~(\textit{labels}~t - \{b\}) \mathrel{\cup} \{a\}~\textrm{else}~\textit{labels}~t)$''
1495 This time, Nitpick won't find any nonstandard counterexample, and we can perform
1496 the induction step using \textit{auto}.
1498 \section{Case Studies}
1499 \label{case-studies}
1501 As a didactic device, the previous section focused mostly on toy formulas whose
1502 validity can easily be assessed just by looking at the formula. We will now
1503 review two somewhat more realistic case studies that are within Nitpick's
1504 reach:\ a context-free grammar modeled by mutually inductive sets and a
1505 functional implementation of AA trees. The results presented in this
1506 section were produced with the following settings:
1509 \textbf{nitpick\_params} [\textit{max\_potential}~= 0,\, \textit{max\_threads} = 2]
1512 \subsection{A Context-Free Grammar}
1513 \label{a-context-free-grammar}
1515 Our first case study is taken from section 7.4 in the Isabelle tutorial
1516 \cite{isa-tutorial}. The following grammar, originally due to Hopcroft and
1517 Ullman, produces all strings with an equal number of $a$'s and $b$'s:
1520 \begin{tabular}{@{}r@{$\;\,$}c@{$\;\,$}l@{}}
1521 $S$ & $::=$ & $\epsilon \mid bA \mid aB$ \\
1522 $A$ & $::=$ & $aS \mid bAA$ \\
1523 $B$ & $::=$ & $bS \mid aBB$
1527 The intuition behind the grammar is that $A$ generates all string with one more
1528 $a$ than $b$'s and $B$ generates all strings with one more $b$ than $a$'s.
1530 The alphabet consists exclusively of $a$'s and $b$'s:
1533 \textbf{datatype} \textit{alphabet}~= $a$ $\mid$ $b$
1536 Strings over the alphabet are represented by \textit{alphabet list}s.
1537 Nonterminals in the grammar become sets of strings. The production rules
1538 presented above can be expressed as a mutually inductive definition:
1541 \textbf{inductive\_set} $S$ \textbf{and} $A$ \textbf{and} $B$ \textbf{where} \\
1542 \textit{R1}:\kern.4em ``$[] \in S$'' $\,\mid$ \\
1543 \textit{R2}:\kern.4em ``$w \in A\,\Longrightarrow\, b \mathbin{\#} w \in S$'' $\,\mid$ \\
1544 \textit{R3}:\kern.4em ``$w \in B\,\Longrightarrow\, a \mathbin{\#} w \in S$'' $\,\mid$ \\
1545 \textit{R4}:\kern.4em ``$w \in S\,\Longrightarrow\, a \mathbin{\#} w \in A$'' $\,\mid$ \\
1546 \textit{R5}:\kern.4em ``$w \in S\,\Longrightarrow\, b \mathbin{\#} w \in S$'' $\,\mid$ \\
1547 \textit{R6}:\kern.4em ``$\lbrakk v \in B;\> v \in B\rbrakk \,\Longrightarrow\, a \mathbin{\#} v \mathbin{@} w \in B$''
1550 The conversion of the grammar into the inductive definition was done manually by
1551 Joe Blow, an underpaid undergraduate student. As a result, some errors might
1554 Debugging faulty specifications is at the heart of Nitpick's \textsl{raison
1555 d'\^etre}. A good approach is to state desirable properties of the specification
1556 (here, that $S$ is exactly the set of strings over $\{a, b\}$ with as many $a$'s
1557 as $b$'s) and check them with Nitpick. If the properties are correctly stated,
1558 counterexamples will point to bugs in the specification. For our grammar
1559 example, we will proceed in two steps, separating the soundness and the
1560 completeness of the set $S$. First, soundness:
1563 \textbf{theorem}~\textit{S\_sound\/}: \\
1564 ``$w \in S \longrightarrow \textit{length}~[x\mathbin{\leftarrow} w.\; x = a] =
1565 \textit{length}~[x\mathbin{\leftarrow} w.\; x = b]$'' \\
1566 \textbf{nitpick} \\[2\smallskipamount]
1567 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1568 \hbox{}\qquad Free variable: \nopagebreak \\
1569 \hbox{}\qquad\qquad $w = [b]$
1572 It would seem that $[b] \in S$. How could this be? An inspection of the
1573 introduction rules reveals that the only rule with a right-hand side of the form
1574 $b \mathbin{\#} {\ldots} \in S$ that could have introduced $[b]$ into $S$ is
1578 ``$w \in S\,\Longrightarrow\, b \mathbin{\#} w \in S$''
1581 On closer inspection, we can see that this rule is wrong. To match the
1582 production $B ::= bS$, the second $S$ should be a $B$. We fix the typo and try
1586 \textbf{nitpick} \\[2\smallskipamount]
1587 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1588 \hbox{}\qquad Free variable: \nopagebreak \\
1589 \hbox{}\qquad\qquad $w = [a, a, b]$
1592 Some detective work is necessary to find out what went wrong here. To get $[a,
1593 a, b] \in S$, we need $[a, b] \in B$ by \textit{R3}, which in turn can only come
1597 ``$\lbrakk v \in B;\> v \in B\rbrakk \,\Longrightarrow\, a \mathbin{\#} v \mathbin{@} w \in B$''
1600 Now, this formula must be wrong: The same assumption occurs twice, and the
1601 variable $w$ is unconstrained. Clearly, one of the two occurrences of $v$ in
1602 the assumptions should have been a $w$.
1604 With the correction made, we don't get any counterexample from Nitpick. Let's
1605 move on and check completeness:
1608 \textbf{theorem}~\textit{S\_complete}: \\
1609 ``$\textit{length}~[x\mathbin{\leftarrow} w.\; x = a] =
1610 \textit{length}~[x\mathbin{\leftarrow} w.\; x = b]
1611 \longrightarrow w \in S$'' \\
1612 \textbf{nitpick} \\[2\smallskipamount]
1613 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1614 \hbox{}\qquad Free variable: \nopagebreak \\
1615 \hbox{}\qquad\qquad $w = [b, b, a, a]$
1618 Apparently, $[b, b, a, a] \notin S$, even though it has the same numbers of
1619 $a$'s and $b$'s. But since our inductive definition passed the soundness check,
1620 the introduction rules we have are probably correct. Perhaps we simply lack an
1621 introduction rule. Comparing the grammar with the inductive definition, our
1622 suspicion is confirmed: Joe Blow simply forgot the production $A ::= bAA$,
1623 without which the grammar cannot generate two or more $b$'s in a row. So we add
1627 ``$\lbrakk v \in A;\> w \in A\rbrakk \,\Longrightarrow\, b \mathbin{\#} v \mathbin{@} w \in A$''
1630 With this last change, we don't get any counterexamples from Nitpick for either
1631 soundness or completeness. We can even generalize our result to cover $A$ and
1635 \textbf{theorem} \textit{S\_A\_B\_sound\_and\_complete}: \\
1636 ``$w \in S \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b]$'' \\
1637 ``$w \in A \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] + 1$'' \\
1638 ``$w \in B \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] + 1$'' \\
1639 \textbf{nitpick} \\[2\smallskipamount]
1640 \slshape Nitpick ran out of time after checking 7 of 8 scopes.
1643 \subsection{AA Trees}
1646 AA trees are a kind of balanced trees discovered by Arne Andersson that provide
1647 similar performance to red-black trees, but with a simpler implementation
1648 \cite{andersson-1993}. They can be used to store sets of elements equipped with
1649 a total order $<$. We start by defining the datatype and some basic extractor
1653 \textbf{datatype} $'a$~\textit{aa\_tree} = \\
1654 \hbox{}\quad $\Lambda$ $\mid$ $N$ ``\kern1pt$'a\Colon \textit{linorder}$'' \textit{nat} ``\kern1pt$'a$ \textit{aa\_tree}'' ``\kern1pt$'a$ \textit{aa\_tree}'' \\[2\smallskipamount]
1655 \textbf{primrec} \textit{data} \textbf{where} \\
1656 ``$\textit{data}~\Lambda = \undef$'' $\,\mid$ \\
1657 ``$\textit{data}~(N~x~\_~\_~\_) = x$'' \\[2\smallskipamount]
1658 \textbf{primrec} \textit{dataset} \textbf{where} \\
1659 ``$\textit{dataset}~\Lambda = \{\}$'' $\,\mid$ \\
1660 ``$\textit{dataset}~(N~x~\_~t~u) = \{x\} \cup \textit{dataset}~t \mathrel{\cup} \textit{dataset}~u$'' \\[2\smallskipamount]
1661 \textbf{primrec} \textit{level} \textbf{where} \\
1662 ``$\textit{level}~\Lambda = 0$'' $\,\mid$ \\
1663 ``$\textit{level}~(N~\_~k~\_~\_) = k$'' \\[2\smallskipamount]
1664 \textbf{primrec} \textit{left} \textbf{where} \\
1665 ``$\textit{left}~\Lambda = \Lambda$'' $\,\mid$ \\
1666 ``$\textit{left}~(N~\_~\_~t~\_) = t$'' \\[2\smallskipamount]
1667 \textbf{primrec} \textit{right} \textbf{where} \\
1668 ``$\textit{right}~\Lambda = \Lambda$'' $\,\mid$ \\
1669 ``$\textit{right}~(N~\_~\_~\_~u) = u$''
1672 The wellformedness criterion for AA trees is fairly complex. Wikipedia states it
1673 as follows \cite{wikipedia-2009-aa-trees}:
1675 \kern.2\parskip %% TYPESETTING
1678 Each node has a level field, and the following invariants must remain true for
1679 the tree to be valid:
1683 \kern-.4\parskip %% TYPESETTING
1688 \item[1.] The level of a leaf node is one.
1689 \item[2.] The level of a left child is strictly less than that of its parent.
1690 \item[3.] The level of a right child is less than or equal to that of its parent.
1691 \item[4.] The level of a right grandchild is strictly less than that of its grandparent.
1692 \item[5.] Every node of level greater than one must have two children.
1697 \kern.4\parskip %% TYPESETTING
1699 The \textit{wf} predicate formalizes this description:
1702 \textbf{primrec} \textit{wf} \textbf{where} \\
1703 ``$\textit{wf}~\Lambda = \textit{True}$'' $\,\mid$ \\
1704 ``$\textit{wf}~(N~\_~k~t~u) =$ \\
1705 \phantom{``}$(\textrm{if}~t = \Lambda~\textrm{then}$ \\
1706 \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))$ \\
1707 \phantom{``$($}$\textrm{else}$ \\
1708 \hbox{}\phantom{``$(\quad$}$\textit{wf}~t \mathrel{\land} \textit{wf}~u
1709 \mathrel{\land} u \not= \Lambda \mathrel{\land} \textit{level}~t < k
1710 \mathrel{\land} \textit{level}~u \le k$ \\
1711 \hbox{}\phantom{``$(\quad$}${\land}\; \textit{level}~(\textit{right}~u) < k)$''
1714 Rebalancing the tree upon insertion and removal of elements is performed by two
1715 auxiliary functions called \textit{skew} and \textit{split}, defined below:
1718 \textbf{primrec} \textit{skew} \textbf{where} \\
1719 ``$\textit{skew}~\Lambda = \Lambda$'' $\,\mid$ \\
1720 ``$\textit{skew}~(N~x~k~t~u) = {}$ \\
1721 \phantom{``}$(\textrm{if}~t \not= \Lambda \mathrel{\land} k =
1722 \textit{level}~t~\textrm{then}$ \\
1723 \phantom{``(\quad}$N~(\textit{data}~t)~k~(\textit{left}~t)~(N~x~k~
1724 (\textit{right}~t)~u)$ \\
1725 \phantom{``(}$\textrm{else}$ \\
1726 \phantom{``(\quad}$N~x~k~t~u)$''
1730 \textbf{primrec} \textit{split} \textbf{where} \\
1731 ``$\textit{split}~\Lambda = \Lambda$'' $\,\mid$ \\
1732 ``$\textit{split}~(N~x~k~t~u) = {}$ \\
1733 \phantom{``}$(\textrm{if}~u \not= \Lambda \mathrel{\land} k =
1734 \textit{level}~(\textit{right}~u)~\textrm{then}$ \\
1735 \phantom{``(\quad}$N~(\textit{data}~u)~(\textit{Suc}~k)~
1736 (N~x~k~t~(\textit{left}~u))~(\textit{right}~u)$ \\
1737 \phantom{``(}$\textrm{else}$ \\
1738 \phantom{``(\quad}$N~x~k~t~u)$''
1741 Performing a \textit{skew} or a \textit{split} should have no impact on the set
1742 of elements stored in the tree:
1745 \textbf{theorem}~\textit{dataset\_skew\_split\/}:\\
1746 ``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
1747 ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
1748 \textbf{nitpick} \\[2\smallskipamount]
1749 {\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
1752 Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
1753 should not alter the tree:
1756 \textbf{theorem}~\textit{wf\_skew\_split\/}:\\
1757 ``$\textit{wf}~t\,\Longrightarrow\, \textit{skew}~t = t$'' \\
1758 ``$\textit{wf}~t\,\Longrightarrow\, \textit{split}~t = t$'' \\
1759 \textbf{nitpick} \\[2\smallskipamount]
1760 {\slshape Nitpick found no counterexample.}
1763 Insertion is implemented recursively. It preserves the sort order:
1766 \textbf{primrec}~\textit{insort} \textbf{where} \\
1767 ``$\textit{insort}~\Lambda~x = N~x~1~\Lambda~\Lambda$'' $\,\mid$ \\
1768 ``$\textit{insort}~(N~y~k~t~u)~x =$ \\
1769 \phantom{``}$({*}~(\textit{split} \circ \textit{skew})~{*})~(N~y~k~(\textrm{if}~x < y~\textrm{then}~\textit{insort}~t~x~\textrm{else}~t)$ \\
1770 \phantom{``$({*}~(\textit{split} \circ \textit{skew})~{*})~(N~y~k~$}$(\textrm{if}~x > y~\textrm{then}~\textit{insort}~u~x~\textrm{else}~u))$''
1773 Notice that we deliberately commented out the application of \textit{skew} and
1774 \textit{split}. Let's see if this causes any problems:
1777 \textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
1778 \textbf{nitpick} \\[2\smallskipamount]
1779 \slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
1780 \hbox{}\qquad Free variables: \nopagebreak \\
1781 \hbox{}\qquad\qquad $t = N~a_1~1~\Lambda~\Lambda$ \\
1782 \hbox{}\qquad\qquad $x = a_2$
1785 It's hard to see why this is a counterexample. To improve readability, we will
1786 restrict the theorem to \textit{nat}, so that we don't need to look up the value
1787 of the $\textit{op}~{<}$ constant to find out which element is smaller than the
1788 other. In addition, we will tell Nitpick to display the value of
1789 $\textit{insort}~t~x$ using the \textit{eval} option. This gives
1792 \textbf{theorem} \textit{wf\_insort\_nat\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\
1793 \textbf{nitpick} [\textit{eval} = ``$\textit{insort}~t~x$''] \\[2\smallskipamount]
1794 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1795 \hbox{}\qquad Free variables: \nopagebreak \\
1796 \hbox{}\qquad\qquad $t = N~1~1~\Lambda~\Lambda$ \\
1797 \hbox{}\qquad\qquad $x = 0$ \\
1798 \hbox{}\qquad Evaluated term: \\
1799 \hbox{}\qquad\qquad $\textit{insort}~t~x = N~1~1~(N~0~1~\Lambda~\Lambda)~\Lambda$
1802 Nitpick's output reveals that the element $0$ was added as a left child of $1$,
1803 where both have a level of 1. This violates the second AA tree invariant, which
1804 states that a left child's level must be less than its parent's. This shouldn't
1805 come as a surprise, considering that we commented out the tree rebalancing code.
1806 Reintroducing the code seems to solve the problem:
1809 \textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
1810 \textbf{nitpick} \\[2\smallskipamount]
1811 {\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
1814 Insertion should transform the set of elements represented by the tree in the
1818 \textbf{theorem} \textit{dataset\_insort\/}:\kern.4em
1819 ``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
1820 \textbf{nitpick} \\[2\smallskipamount]
1821 {\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
1824 We could continue like this and sketch a complete theory of AA trees. Once the
1825 definitions and main theorems are in place and have been thoroughly tested using
1826 Nitpick, we could start working on the proofs. Developing theories this way
1827 usually saves time, because faulty theorems and definitions are discovered much
1828 earlier in the process.
1830 \section{Option Reference}
1831 \label{option-reference}
1833 \def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
1834 \def\qty#1{$\left<\textit{#1}\right>$}
1835 \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
1836 \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1837 \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1838 \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1839 \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
1840 \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
1841 \def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
1842 \def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
1843 \def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
1845 Nitpick's behavior can be influenced by various options, which can be specified
1846 in brackets after the \textbf{nitpick} command. Default values can be set
1847 using \textbf{nitpick\_\allowbreak params}. For example:
1850 \textbf{nitpick\_params} [\textit{verbose}, \,\textit{timeout} = 60$\,s$]
1853 The options are categorized as follows:\ mode of operation
1854 (\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output
1855 format (\S\ref{output-format}), automatic counterexample checks
1856 (\S\ref{authentication}), optimizations
1857 (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
1859 You can instruct Nitpick to run automatically on newly entered theorems by
1860 enabling the ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof
1861 General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation})
1862 and \textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
1863 \textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
1864 (\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
1865 disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
1866 \textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Counterexample
1867 Time Limit'' in Proof General's ``Isabelle'' menu. Nitpick's output is also more
1870 The number of options can be overwhelming at first glance. Do not let that worry
1871 you: Nitpick's defaults have been chosen so that it almost always does the right
1872 thing, and the most important options have been covered in context in
1873 \S\ref{first-steps}.
1875 The descriptions below refer to the following syntactic quantities:
1878 \item[$\bullet$] \qtybf{string}: A string.
1879 \item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
1880 \item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}.
1881 \item[$\bullet$] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
1882 \item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
1883 \item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
1884 of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<midarrow\char`\>}.
1886 \item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
1887 \item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
1888 (milliseconds), or the keyword \textit{none} ($\infty$ years).
1889 \item[$\bullet$] \qtybf{const\/}: The name of a HOL constant.
1890 \item[$\bullet$] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
1891 \item[$\bullet$] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g.,
1892 ``$f~x$''~``$g~y$'').
1893 \item[$\bullet$] \qtybf{type}: A HOL type.
1896 Default values are indicated in square brackets. Boolean options have a negated
1897 counterpart (e.g., \textit{blocking} vs.\ \textit{no\_blocking}). When setting
1898 Boolean options, ``= \textit{true}'' may be omitted.
1900 \subsection{Mode of Operation}
1901 \label{mode-of-operation}
1904 \optrue{blocking}{non\_blocking}
1905 Specifies whether the \textbf{nitpick} command should operate synchronously.
1906 The asynchronous (non-blocking) mode lets the user start proving the putative
1907 theorem while Nitpick looks for a counterexample, but it can also be more
1908 confusing. For technical reasons, automatic runs currently always block.
1910 \optrue{falsify}{satisfy}
1911 Specifies whether Nitpick should look for falsifying examples (countermodels) or
1912 satisfying examples (models). This manual assumes throughout that
1913 \textit{falsify} is enabled.
1915 \opsmart{user\_axioms}{no\_user\_axioms}
1916 Specifies whether the user-defined axioms (specified using
1917 \textbf{axiomatization} and \textbf{axioms}) should be considered. If the option
1918 is set to \textit{smart}, Nitpick performs an ad hoc axiom selection based on
1919 the constants that occur in the formula to falsify. The option is implicitly set
1920 to \textit{true} for automatic runs.
1922 \textbf{Warning:} If the option is set to \textit{true}, Nitpick might
1923 nonetheless ignore some polymorphic axioms. Counterexamples generated under
1924 these conditions are tagged as ``quasi genuine.'' The \textit{debug}
1925 (\S\ref{output-format}) option can be used to find out which axioms were
1929 {\small See also \textit{assms} (\S\ref{mode-of-operation}) and \textit{debug}
1930 (\S\ref{output-format}).}
1932 \optrue{assms}{no\_assms}
1933 Specifies whether the relevant assumptions in structured proofs should be
1934 considered. The option is implicitly enabled for automatic runs.
1937 {\small See also \textit{user\_axioms} (\S\ref{mode-of-operation}).}
1939 \opfalse{overlord}{no\_overlord}
1940 Specifies whether Nitpick should put its temporary files in
1941 \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
1942 debugging Nitpick but also unsafe if several instances of the tool are run
1943 simultaneously. The files are identified by the extensions
1944 \texttt{.kki}, \texttt{.cnf}, \texttt{.out}, and
1945 \texttt{.err}; you may safely remove them after Nitpick has run.
1948 {\small See also \textit{debug} (\S\ref{output-format}).}
1951 \subsection{Scope of Search}
1952 \label{scope-of-search}
1955 \oparg{card}{type}{int\_seq}
1956 Specifies the sequence of cardinalities to use for a given type.
1957 For free types, and often also for \textbf{typedecl}'d types, it usually makes
1958 sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
1961 {\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
1962 (\S\ref{scope-of-search}).}
1964 \opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
1965 Specifies the default sequence of cardinalities to use. This can be overridden
1966 on a per-type basis using the \textit{card}~\qty{type} option described above.
1968 \oparg{max}{const}{int\_seq}
1969 Specifies the sequence of maximum multiplicities to use for a given
1970 (co)in\-duc\-tive datatype constructor. A constructor's multiplicity is the
1971 number of distinct values that it can construct. Nonsensical values (e.g.,
1972 \textit{max}~[]~$=$~2) are silently repaired. This option is only available for
1973 datatypes equipped with several constructors.
1975 \opnodefault{max}{int\_seq}
1976 Specifies the default sequence of maximum multiplicities to use for
1977 (co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor
1978 basis using the \textit{max}~\qty{const} option described above.
1980 \opsmart{binary\_ints}{unary\_ints}
1981 Specifies whether natural numbers and integers should be encoded using a unary
1982 or binary notation. In unary mode, the cardinality fully specifies the subset
1983 used to approximate the type. For example:
1985 $$\hbox{\begin{tabular}{@{}rll@{}}%
1986 \textit{card nat} = 4 & induces & $\{0,\, 1,\, 2,\, 3\}$ \\
1987 \textit{card int} = 4 & induces & $\{-1,\, 0,\, +1,\, +2\}$ \\
1988 \textit{card int} = 5 & induces & $\{-2,\, -1,\, 0,\, +1,\, +2\}.$%
1993 $$\hbox{\begin{tabular}{@{}rll@{}}%
1994 \textit{card nat} = $K$ & induces & $\{0,\, \ldots,\, K - 1\}$ \\
1995 \textit{card int} = $K$ & induces & $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor K/2 \rfloor\}.$%
1998 In binary mode, the cardinality specifies the number of distinct values that can
1999 be constructed. Each of these value is represented by a bit pattern whose length
2000 is specified by the \textit{bits} (\S\ref{scope-of-search}) option. By default,
2001 Nitpick attempts to choose the more appropriate encoding by inspecting the
2002 formula at hand, preferring the binary notation for problems involving
2003 multiplicative operators or large constants.
2005 \textbf{Warning:} For technical reasons, Nitpick always reverts to unary for
2006 problems that refer to the types \textit{rat} or \textit{real} or the constants
2007 \textit{Suc}, \textit{gcd}, or \textit{lcm}.
2009 {\small See also \textit{bits} (\S\ref{scope-of-search}) and
2010 \textit{show\_datatypes} (\S\ref{output-format}).}
2012 \opdefault{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$}
2013 Specifies the number of bits to use to represent natural numbers and integers in
2014 binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
2016 {\small See also \textit{binary\_ints} (\S\ref{scope-of-search}).}
2018 \opargboolorsmart{wf}{const}{non\_wf}
2019 Specifies whether the specified (co)in\-duc\-tively defined predicate is
2020 well-founded. The option can take the following values:
2023 \item[$\bullet$] \textbf{\textit{true}}: Tentatively treat the (co)in\-duc\-tive
2024 predicate as if it were well-founded. Since this is generally not sound when the
2025 predicate is not well-founded, the counterexamples are tagged as ``quasi
2028 \item[$\bullet$] \textbf{\textit{false}}: Treat the (co)in\-duc\-tive predicate
2029 as if it were not well-founded. The predicate is then unrolled as prescribed by
2030 the \textit{star\_linear\_preds}, \textit{iter}~\qty{const}, and \textit{iter}
2033 \item[$\bullet$] \textbf{\textit{smart}}: Try to prove that the inductive
2034 predicate is well-founded using Isabelle's \textit{lexicographic\_order} and
2035 \textit{size\_change} tactics. If this succeeds (or the predicate occurs with an
2036 appropriate polarity in the formula to falsify), use an efficient fixed point
2037 equation as specification of the predicate; otherwise, unroll the predicates
2038 according to the \textit{iter}~\qty{const} and \textit{iter} options.
2042 {\small See also \textit{iter} (\S\ref{scope-of-search}),
2043 \textit{star\_linear\_preds} (\S\ref{optimizations}), and \textit{tac\_timeout}
2044 (\S\ref{timeouts}).}
2046 \opsmart{wf}{non\_wf}
2047 Specifies the default wellfoundedness setting to use. This can be overridden on
2048 a per-predicate basis using the \textit{wf}~\qty{const} option above.
2050 \oparg{iter}{const}{int\_seq}
2051 Specifies the sequence of iteration counts to use when unrolling a given
2052 (co)in\-duc\-tive predicate. By default, unrolling is applied for inductive
2053 predicates that occur negatively and coinductive predicates that occur
2054 positively in the formula to falsify and that cannot be proved to be
2055 well-founded, but this behavior is influenced by the \textit{wf} option. The
2056 iteration counts are automatically bounded by the cardinality of the predicate's
2059 {\small See also \textit{wf} (\S\ref{scope-of-search}) and
2060 \textit{star\_linear\_preds} (\S\ref{optimizations}).}
2062 \opdefault{iter}{int\_seq}{$\mathbf{1{,}2{,}4{,}8{,}12{,}16{,}24{,}32}$}
2063 Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive
2064 predicates. This can be overridden on a per-predicate basis using the
2065 \textit{iter} \qty{const} option above.
2067 \opdefault{bisim\_depth}{int\_seq}{$\mathbf{7}$}
2068 Specifies the sequence of iteration counts to use when unrolling the
2069 bisimilarity predicate generated by Nitpick for coinductive datatypes. A value
2070 of $-1$ means that no predicate is generated, in which case Nitpick performs an
2071 after-the-fact check to see if the known coinductive datatype values are
2072 bidissimilar. If two values are found to be bisimilar, the counterexample is
2073 tagged as ``quasi genuine.'' The iteration counts are automatically bounded by
2074 the sum of the cardinalities of the coinductive datatypes occurring in the
2077 \opargboolorsmart{box}{type}{dont\_box}
2078 Specifies whether Nitpick should attempt to wrap (``box'') a given function or
2079 product type in an isomorphic datatype internally. Boxing is an effective mean
2080 to reduce the search space and speed up Nitpick, because the isomorphic datatype
2081 is approximated by a subset of the possible function or pair values.
2082 Like other drastic optimizations, it can also prevent the discovery of
2083 counterexamples. The option can take the following values:
2086 \item[$\bullet$] \textbf{\textit{true}}: Box the specified type whenever
2088 \item[$\bullet$] \textbf{\textit{false}}: Never box the type.
2089 \item[$\bullet$] \textbf{\textit{smart}}: Box the type only in contexts where it
2090 is likely to help. For example, $n$-tuples where $n > 2$ and arguments to
2091 higher-order functions are good candidates for boxing.
2095 {\small See also \textit{finitize} (\S\ref{scope-of-search}), \textit{verbose}
2096 (\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}).}
2098 \opsmart{box}{dont\_box}
2099 Specifies the default boxing setting to use. This can be overridden on a
2100 per-type basis using the \textit{box}~\qty{type} option described above.
2102 \opargboolorsmart{finitize}{type}{dont\_finitize}
2103 Specifies whether Nitpick should attempt to finitize a given type, which can be
2104 a function type or an infinite ``shallow datatype'' (an infinite datatype whose
2105 constructors don't appear in the problem).
2107 For function types, Nitpick performs a monotonicity analysis to detect functions
2108 that are constant at all but finitely many points (e.g., finite sets) and treats
2109 such occurrences specially, thereby increasing the precision. The option can
2110 then take the following values:
2113 \item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the type.
2114 \item[$\bullet$] \textbf{\textit{true}} or \textbf{\textit{smart}}: Finitize the
2115 type wherever possible.
2118 The semantics of the option is somewhat different for infinite shallow
2122 \item[$\bullet$] \textbf{\textit{true}}: Finitize the datatype. Since this is
2123 unsound, counterexamples generated under these conditions are tagged as ``quasi
2125 \item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the datatype.
2126 \item[$\bullet$] \textbf{\textit{smart}}: Perform a monotonicity analysis to
2127 detect whether the datatype can be safely finitized before finitizing it.
2130 Like other drastic optimizations, finitization can sometimes prevent the
2131 discovery of counterexamples.
2134 {\small See also \textit{box} (\S\ref{scope-of-search}), \textit{mono}
2135 (\S\ref{scope-of-search}), \textit{verbose} (\S\ref{output-format}), and
2136 \textit{debug} (\S\ref{output-format}).}
2138 \opsmart{finitize}{dont\_finitize}
2139 Specifies the default finitization setting to use. This can be overridden on a
2140 per-type basis using the \textit{finitize}~\qty{type} option described above.
2142 \opargboolorsmart{mono}{type}{non\_mono}
2143 Specifies whether the given type should be considered monotonic when enumerating
2144 scopes and finitizing types. If the option is set to \textit{smart}, Nitpick
2145 performs a monotonicity check on the type. Setting this option to \textit{true}
2146 can reduce the number of scopes tried, but it can also diminish the chance of
2147 finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}.
2150 {\small See also \textit{card} (\S\ref{scope-of-search}),
2151 \textit{finitize} (\S\ref{scope-of-search}),
2152 \textit{merge\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
2153 (\S\ref{output-format}).}
2155 \opsmart{mono}{non\_mono}
2156 Specifies the default monotonicity setting to use. This can be overridden on a
2157 per-type basis using the \textit{mono}~\qty{type} option described above.
2159 \opfalse{merge\_type\_vars}{dont\_merge\_type\_vars}
2160 Specifies whether type variables with the same sort constraints should be
2161 merged. Setting this option to \textit{true} can reduce the number of scopes
2162 tried and the size of the generated Kodkod formulas, but it also diminishes the
2163 theoretical chance of finding a counterexample.
2165 {\small See also \textit{mono} (\S\ref{scope-of-search}).}
2167 \opargbool{std}{type}{non\_std}
2168 Specifies whether the given (recursive) datatype should be given standard
2169 models. Nonstandard models are unsound but can help debug structural induction
2170 proofs, as explained in \S\ref{inductive-properties}.
2172 \optrue{std}{non\_std}
2173 Specifies the default standardness to use. This can be overridden on a per-type
2174 basis using the \textit{std}~\qty{type} option described above.
2177 \subsection{Output Format}
2178 \label{output-format}
2181 \opfalse{verbose}{quiet}
2182 Specifies whether the \textbf{nitpick} command should explain what it does. This
2183 option is useful to determine which scopes are tried or which SAT solver is
2184 used. This option is implicitly disabled for automatic runs.
2186 \opfalse{debug}{no\_debug}
2187 Specifies whether Nitpick should display additional debugging information beyond
2188 what \textit{verbose} already displays. Enabling \textit{debug} also enables
2189 \textit{verbose} and \textit{show\_all} behind the scenes. The \textit{debug}
2190 option is implicitly disabled for automatic runs.
2193 {\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
2194 \textit{batch\_size} (\S\ref{optimizations}).}
2196 \optrue{show\_skolems}{hide\_skolem}
2197 Specifies whether the values of Skolem constants should be displayed as part of
2198 counterexamples. Skolem constants correspond to bound variables in the original
2199 formula and usually help us to understand why the counterexample falsifies the
2203 {\small See also \textit{skolemize} (\S\ref{optimizations}).}
2205 \opfalse{show\_datatypes}{hide\_datatypes}
2206 Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
2207 be displayed as part of counterexamples. Such subsets are sometimes helpful when
2208 investigating whether a potential counterexample is genuine or spurious, but
2209 their potential for clutter is real.
2211 \opfalse{show\_consts}{hide\_consts}
2212 Specifies whether the values of constants occurring in the formula (including
2213 its axioms) should be displayed along with any counterexample. These values are
2214 sometimes helpful when investigating why a counterexample is
2215 genuine, but they can clutter the output.
2217 \opfalse{show\_all}{dont\_show\_all}
2218 Enabling this option effectively enables \textit{show\_skolems},
2219 \textit{show\_datatypes}, and \textit{show\_consts}.
2221 \opdefault{max\_potential}{int}{$\mathbf{1}$}
2222 Specifies the maximum number of potential counterexamples to display. Setting
2223 this option to 0 speeds up the search for a genuine counterexample. This option
2224 is implicitly set to 0 for automatic runs. If you set this option to a value
2225 greater than 1, you will need an incremental SAT solver, such as
2226 \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that many of
2227 the counterexamples may be identical.
2230 {\small See also \textit{check\_potential} (\S\ref{authentication}) and
2231 \textit{sat\_solver} (\S\ref{optimizations}).}
2233 \opdefault{max\_genuine}{int}{$\mathbf{1}$}
2234 Specifies the maximum number of genuine counterexamples to display. If you set
2235 this option to a value greater than 1, you will need an incremental SAT solver,
2236 such as \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that
2237 many of the counterexamples may be identical.
2240 {\small See also \textit{check\_genuine} (\S\ref{authentication}) and
2241 \textit{sat\_solver} (\S\ref{optimizations}).}
2243 \opnodefault{eval}{term\_list}
2244 Specifies the list of terms whose values should be displayed along with
2245 counterexamples. This option suffers from an ``observer effect'': Nitpick might
2246 find different counterexamples for different values of this option.
2248 \oparg{format}{term}{int\_seq}
2249 Specifies how to uncurry the value displayed for a variable or constant.
2250 Uncurrying sometimes increases the readability of the output for high-arity
2251 functions. For example, given the variable $y \mathbin{\Colon} {'a}\Rightarrow
2252 {'b}\Rightarrow {'c}\Rightarrow {'d}\Rightarrow {'e}\Rightarrow {'f}\Rightarrow
2253 {'g}$, setting \textit{format}~$y$ = 3 tells Nitpick to group the last three
2254 arguments, as if the type had been ${'a}\Rightarrow {'b}\Rightarrow
2255 {'c}\Rightarrow {'d}\times {'e}\times {'f}\Rightarrow {'g}$. In general, a list
2256 of values $n_1,\ldots,n_k$ tells Nitpick to show the last $n_k$ arguments as an
2257 $n_k$-tuple, the previous $n_{k-1}$ arguments as an $n_{k-1}$-tuple, and so on;
2258 arguments that are not accounted for are left alone, as if the specification had
2259 been $1,\ldots,1,n_1,\ldots,n_k$.
2262 {\small See also \textit{uncurry} (\S\ref{optimizations}).}
2264 \opdefault{format}{int\_seq}{$\mathbf{1}$}
2265 Specifies the default format to use. Irrespective of the default format, the
2266 extra arguments to a Skolem constant corresponding to the outer bound variables
2267 are kept separated from the remaining arguments, the \textbf{for} arguments of
2268 an inductive definitions are kept separated from the remaining arguments, and
2269 the iteration counter of an unrolled inductive definition is shown alone. The
2270 default format can be overridden on a per-variable or per-constant basis using
2271 the \textit{format}~\qty{term} option described above.
2274 \subsection{Authentication}
2275 \label{authentication}
2278 \opfalse{check\_potential}{trust\_potential}
2279 Specifies whether potential counterexamples should be given to Isabelle's
2280 \textit{auto} tactic to assess their validity. If a potential counterexample is
2281 shown to be genuine, Nitpick displays a message to this effect and terminates.
2284 {\small See also \textit{max\_potential} (\S\ref{output-format}).}
2286 \opfalse{check\_genuine}{trust\_genuine}
2287 Specifies whether genuine and quasi genuine counterexamples should be given to
2288 Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine''
2289 counterexample is shown to be spurious, the user is kindly asked to send a bug
2290 report to the author at
2291 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@in.tum.de}.
2294 {\small See also \textit{max\_genuine} (\S\ref{output-format}).}
2296 \opnodefault{expect}{string}
2297 Specifies the expected outcome, which must be one of the following:
2300 \item[$\bullet$] \textbf{\textit{genuine}}: Nitpick found a genuine counterexample.
2301 \item[$\bullet$] \textbf{\textit{quasi\_genuine}}: Nitpick found a ``quasi
2302 genuine'' counterexample (i.e., a counterexample that is genuine unless
2303 it contradicts a missing axiom or a dangerous option was used inappropriately).
2304 \item[$\bullet$] \textbf{\textit{potential}}: Nitpick found a potential counterexample.
2305 \item[$\bullet$] \textbf{\textit{none}}: Nitpick found no counterexample.
2306 \item[$\bullet$] \textbf{\textit{unknown}}: Nitpick encountered some problem (e.g.,
2307 Kodkod ran out of memory).
2310 Nitpick emits an error if the actual outcome differs from the expected outcome.
2311 This option is useful for regression testing.
2314 \subsection{Optimizations}
2315 \label{optimizations}
2317 \def\cpp{C\nobreak\raisebox{.1ex}{+}\nobreak\raisebox{.1ex}{+}}
2322 \opdefault{sat\_solver}{string}{smart}
2323 Specifies which SAT solver to use. SAT solvers implemented in C or \cpp{} tend
2324 to be faster than their Java counterparts, but they can be more difficult to
2325 install. Also, if you set the \textit{max\_potential} (\S\ref{output-format}) or
2326 \textit{max\_genuine} (\S\ref{output-format}) option to a value greater than 1,
2327 you will need an incremental SAT solver, such as \textit{MiniSat\_JNI}
2328 (recommended) or \textit{SAT4J}.
2330 The supported solvers are listed below:
2336 \item[$\bullet$] \textbf{\textit{MiniSat}}: MiniSat is an efficient solver
2337 written in \cpp{}. To use MiniSat, set the environment variable
2338 \texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
2340 \footnote{Important note for Cygwin users: The path must be specified using
2341 native Windows syntax. Make sure to escape backslashes properly.%
2342 \label{cygwin-paths}}
2343 The \cpp{} sources and executables for MiniSat are available at
2344 \url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
2345 and 2.0 beta (2007-07-21).
2347 \item[$\bullet$] \textbf{\textit{MiniSat\_JNI}}: The JNI (Java Native Interface)
2348 version of MiniSat is bundled with Kodkodi and is precompiled for the major
2349 platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
2350 which you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
2351 version of MiniSat, the JNI version can be used incrementally.
2353 \item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver
2354 written in C. You can install a standard version of
2355 PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
2356 that contains the \texttt{picosat} executable.%
2357 \footref{cygwin-paths}
2358 The C sources for PicoSAT are
2359 available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
2360 Nitpick has been tested with version 913.
2362 \item[$\bullet$] \textbf{\textit{zChaff}}: zChaff is an efficient solver written
2363 in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
2364 the directory that contains the \texttt{zchaff} executable.%
2365 \footref{cygwin-paths}
2366 The \cpp{} sources and executables for zChaff are available at
2367 \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
2368 versions 2004-05-13, 2004-11-15, and 2007-03-12.
2370 \item[$\bullet$] \textbf{\textit{zChaff\_JNI}}: The JNI version of zChaff is
2371 bundled with Kodkodi and is precompiled for the major
2372 platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
2373 which you will find on Kodkod's web site \cite{kodkod-2009}.
2375 \item[$\bullet$] \textbf{\textit{RSat}}: RSat is an efficient solver written in
2376 \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
2377 directory that contains the \texttt{rsat} executable.%
2378 \footref{cygwin-paths}
2379 The \cpp{} sources for RSat are available at
2380 \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been tested with version
2383 \item[$\bullet$] \textbf{\textit{BerkMin}}: BerkMin561 is an efficient solver
2384 written in C. To use BerkMin, set the environment variable
2385 \texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561}
2386 executable.\footref{cygwin-paths}
2387 The BerkMin executables are available at
2388 \url{http://eigold.tripod.com/BerkMin.html}.
2390 \item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}}: Variant of BerkMin that is
2391 included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
2392 version of BerkMin, set the environment variable
2393 \texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
2395 \footref{cygwin-paths}
2397 \item[$\bullet$] \textbf{\textit{Jerusat}}: Jerusat 1.3 is an efficient solver
2398 written in C. To use Jerusat, set the environment variable
2399 \texttt{JERUSAT\_HOME} to the directory that contains the \texttt{Jerusat1.3}
2401 \footref{cygwin-paths}
2402 The C sources for Jerusat are available at
2403 \url{http://www.cs.tau.ac.il/~ale1/Jerusat1.3.tgz}.
2405 \item[$\bullet$] \textbf{\textit{SAT4J}}: SAT4J is a reasonably efficient solver
2406 written in Java that can be used incrementally. It is bundled with Kodkodi and
2407 requires no further installation or configuration steps. Do not attempt to
2408 install the official SAT4J packages, because their API is incompatible with
2411 \item[$\bullet$] \textbf{\textit{SAT4J\_Light}}: Variant of SAT4J that is
2412 optimized for small problems. It can also be used incrementally.
2414 \item[$\bullet$] \textbf{\textit{HaifaSat}}: HaifaSat 1.0 beta is an
2415 experimental solver written in \cpp. To use HaifaSat, set the environment
2416 variable \texttt{HAIFASAT\_\allowbreak HOME} to the directory that contains the
2417 \texttt{HaifaSat} executable.%
2418 \footref{cygwin-paths}
2419 The \cpp{} sources for HaifaSat are available at
2420 \url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}.
2422 \item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
2423 \textit{smart}, Nitpick selects the first solver among MiniSat,
2424 PicoSAT, zChaff, RSat, BerkMin, BerkMin\_Alloy, Jerusat, MiniSat\_JNI, and zChaff\_JNI
2425 that is recognized by Isabelle. If none is found, it falls back on SAT4J, which
2426 should always be available. If \textit{verbose} (\S\ref{output-format}) is
2427 enabled, Nitpick displays which SAT solver was chosen.
2431 \opdefault{batch\_size}{int\_or\_smart}{smart}
2432 Specifies the maximum number of Kodkod problems that should be lumped together
2433 when invoking Kodkodi. Each problem corresponds to one scope. Lumping problems
2434 together ensures that Kodkodi is launched less often, but it makes the verbose
2435 output less readable and is sometimes detrimental to performance. If
2436 \textit{batch\_size} is set to \textit{smart}, the actual value used is 1 if
2437 \textit{debug} (\S\ref{output-format}) is set and 64 otherwise.
2439 \optrue{destroy\_constrs}{dont\_destroy\_constrs}
2440 Specifies whether formulas involving (co)in\-duc\-tive datatype constructors should
2441 be rewritten to use (automatically generated) discriminators and destructors.
2442 This optimization can drastically reduce the size of the Boolean formulas given
2446 {\small See also \textit{debug} (\S\ref{output-format}).}
2448 \optrue{specialize}{dont\_specialize}
2449 Specifies whether functions invoked with static arguments should be specialized.
2450 This optimization can drastically reduce the search space, especially for
2451 higher-order functions.
2454 {\small See also \textit{debug} (\S\ref{output-format}) and
2455 \textit{show\_consts} (\S\ref{output-format}).}
2457 \optrue{skolemize}{dont\_skolemize}
2458 Specifies whether the formula should be skolemized. For performance reasons,
2459 (positive) $\forall$-quanti\-fiers that occur in the scope of a higher-order
2460 (positive) $\exists$-quanti\-fier are left unchanged.
2463 {\small See also \textit{debug} (\S\ref{output-format}) and
2464 \textit{show\_skolems} (\S\ref{output-format}).}
2466 \optrue{star\_linear\_preds}{dont\_star\_linear\_preds}
2467 Specifies whether Nitpick should use Kodkod's transitive closure operator to
2468 encode non-well-founded ``linear inductive predicates,'' i.e., inductive
2469 predicates for which each the predicate occurs in at most one assumption of each
2470 introduction rule. Using the reflexive transitive closure is in principle
2471 equivalent to setting \textit{iter} to the cardinality of the predicate's
2472 domain, but it is usually more efficient.
2474 {\small See also \textit{wf} (\S\ref{scope-of-search}), \textit{debug}
2475 (\S\ref{output-format}), and \textit{iter} (\S\ref{scope-of-search}).}
2477 \optrue{uncurry}{dont\_uncurry}
2478 Specifies whether Nitpick should uncurry functions. Uncurrying has on its own no
2479 tangible effect on efficiency, but it creates opportunities for the boxing
2483 {\small See also \textit{box} (\S\ref{scope-of-search}), \textit{debug}
2484 (\S\ref{output-format}), and \textit{format} (\S\ref{output-format}).}
2486 \optrue{fast\_descrs}{full\_descrs}
2487 Specifies whether Nitpick should optimize the definite and indefinite
2488 description operators (THE and SOME). The optimized versions usually help
2489 Nitpick generate more counterexamples or at least find them faster, but only the
2490 unoptimized versions are complete when all types occurring in the formula are
2493 {\small See also \textit{debug} (\S\ref{output-format}).}
2495 \optrue{peephole\_optim}{no\_peephole\_optim}
2496 Specifies whether Nitpick should simplify the generated Kodkod formulas using a
2497 peephole optimizer. These optimizations can make a significant difference.
2498 Unless you are tracking down a bug in Nitpick or distrust the peephole
2499 optimizer, you should leave this option enabled.
2501 \opdefault{sym\_break}{int}{20}
2502 Specifies an upper bound on the number of relations for which Kodkod generates
2503 symmetry breaking predicates. According to the Kodkod documentation
2504 \cite{kodkod-2009-options}, ``in general, the higher this value, the more
2505 symmetries will be broken, and the faster the formula will be solved. But,
2506 setting the value too high may have the opposite effect and slow down the
2509 \opdefault{sharing\_depth}{int}{3}
2510 Specifies the depth to which Kodkod should check circuits for equivalence during
2511 the translation to SAT. The default of 3 is the same as in Alloy. The minimum
2512 allowed depth is 1. Increasing the sharing may result in a smaller SAT problem,
2513 but can also slow down Kodkod.
2515 \opfalse{flatten\_props}{dont\_flatten\_props}
2516 Specifies whether Kodkod should try to eliminate intermediate Boolean variables.
2517 Although this might sound like a good idea, in practice it can drastically slow
2520 \opdefault{max\_threads}{int}{0}
2521 Specifies the maximum number of threads to use in Kodkod. If this option is set
2522 to 0, Kodkod will compute an appropriate value based on the number of processor
2526 {\small See also \textit{batch\_size} (\S\ref{optimizations}) and
2527 \textit{timeout} (\S\ref{timeouts}).}
2530 \subsection{Timeouts}
2534 \opdefault{timeout}{time}{$\mathbf{30}$ s}
2535 Specifies the maximum amount of time that the \textbf{nitpick} command should
2536 spend looking for a counterexample. Nitpick tries to honor this constraint as
2537 well as it can but offers no guarantees. For automatic runs,
2538 \textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share
2539 a time slot whose length is specified by the ``Auto Counterexample Time
2540 Limit'' option in Proof General.
2543 {\small See also \textit{max\_threads} (\S\ref{optimizations}).}
2545 \opdefault{tac\_timeout}{time}{$\mathbf{500}$\,ms}
2546 Specifies the maximum amount of time that the \textit{auto} tactic should use
2547 when checking a counterexample, and similarly that \textit{lexicographic\_order}
2548 and \textit{size\_change} should use when checking whether a (co)in\-duc\-tive
2549 predicate is well-founded. Nitpick tries to honor this constraint as well as it
2550 can but offers no guarantees.
2553 {\small See also \textit{wf} (\S\ref{scope-of-search}),
2554 \textit{check\_potential} (\S\ref{authentication}),
2555 and \textit{check\_genuine} (\S\ref{authentication}).}
2558 \section{Attribute Reference}
2559 \label{attribute-reference}
2561 Nitpick needs to consider the definitions of all constants occurring in a
2562 formula in order to falsify it. For constants introduced using the
2563 \textbf{definition} command, the definition is simply the associated
2564 \textit{\_def} axiom. In contrast, instead of using the internal representation
2565 of functions synthesized by Isabelle's \textbf{primrec}, \textbf{function}, and
2566 \textbf{nominal\_primrec} packages, Nitpick relies on the more natural
2567 equational specification entered by the user.
2569 Behind the scenes, Isabelle's built-in packages and theories rely on the
2570 following attributes to affect Nitpick's behavior:
2573 \flushitem{\textit{nitpick\_def}}
2576 This attribute specifies an alternative definition of a constant. The
2577 alternative definition should be logically equivalent to the constant's actual
2578 axiomatic definition and should be of the form
2580 \qquad $c~{?}x_1~\ldots~{?}x_n \,\equiv\, t$,
2582 where ${?}x_1, \ldots, {?}x_n$ are distinct variables and $c$ does not occur in
2585 \flushitem{\textit{nitpick\_simp}}
2588 This attribute specifies the equations that constitute the specification of a
2589 constant. For functions defined using the \textbf{primrec}, \textbf{function},
2590 and \textbf{nominal\_\allowbreak primrec} packages, this corresponds to the
2591 \textit{simps} rules. The equations must be of the form
2593 \qquad $c~t_1~\ldots\ t_n \,=\, u.$
2595 \flushitem{\textit{nitpick\_psimp}}
2598 This attribute specifies the equations that constitute the partial specification
2599 of a constant. For functions defined using the \textbf{function} package, this
2600 corresponds to the \textit{psimps} rules. The conditional equations must be of
2603 \qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,=\, u$.
2605 \flushitem{\textit{nitpick\_intro}}
2608 This attribute specifies the introduction rules of a (co)in\-duc\-tive predicate.
2609 For predicates defined using the \textbf{inductive} or \textbf{coinductive}
2610 command, this corresponds to the \textit{intros} rules. The introduction rules
2613 \qquad $\lbrakk P_1;\> \ldots;\> P_m;\> M~(c\ t_{11}\ \ldots\ t_{1n});\>
2614 \ldots;\> M~(c\ t_{k1}\ \ldots\ t_{kn})\rbrakk \,\Longrightarrow\, c\ u_1\
2617 where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an
2618 optional monotonic operator. The order of the assumptions is irrelevant.
2620 \flushitem{\textit{nitpick\_choice\_spec}}
2623 This attribute specifies the (free-form) specification of a constant defined
2624 using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command.
2628 When faced with a constant, Nitpick proceeds as follows:
2631 \item[1.] If the \textit{nitpick\_simp} set associated with the constant
2632 is not empty, Nitpick uses these rules as the specification of the constant.
2634 \item[2.] Otherwise, if the \textit{nitpick\_psimp} set associated with
2635 the constant is not empty, it uses these rules as the specification of the
2638 \item[3.] Otherwise, if the constant was defined using the
2639 \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command and the
2640 \textit{nitpick\_choice\_spec} set associated with the constant is not empty, it
2641 uses these theorems as the specification of the constant.
2643 \item[4.] Otherwise, it looks up the definition of the constant:
2646 \item[1.] If the \textit{nitpick\_def} set associated with the constant
2647 is not empty, it uses the latest rule added to the set as the definition of the
2648 constant; otherwise it uses the actual definition axiom.
2649 \item[2.] If the definition is of the form
2651 \qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{lfp}~(\lambda f.\; t)$,
2653 then Nitpick assumes that the definition was made using an inductive package and
2654 based on the introduction rules marked with \textit{nitpick\_\allowbreak
2655 \allowbreak intros} tries to determine whether the definition is
2660 As an illustration, consider the inductive definition
2663 \textbf{inductive}~\textit{odd}~\textbf{where} \\
2664 ``\textit{odd}~1'' $\,\mid$ \\
2665 ``\textit{odd}~$n\,\Longrightarrow\, \textit{odd}~(\textit{Suc}~(\textit{Suc}~n))$''
2668 Isabelle automatically attaches the \textit{nitpick\_intro} attribute to
2669 the above rules. Nitpick then uses the \textit{lfp}-based definition in
2670 conjunction with these rules. To override this, we can specify an alternative
2671 definition as follows:
2674 \textbf{lemma} $\mathit{odd\_def}'$ [\textit{nitpick\_def}]:\kern.4em ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
2677 Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2
2678 = 1$. Alternatively, we can specify an equational specification of the constant:
2681 \textbf{lemma} $\mathit{odd\_simp}'$ [\textit{nitpick\_simp}]:\kern.4em ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
2684 Such tweaks should be done with great care, because Nitpick will assume that the
2685 constant is completely defined by its equational specification. For example, if
2686 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
2687 $\textit{odd}~n$ arbitrarily for even values of $n$. The \textit{debug}
2688 (\S\ref{output-format}) option is extremely useful to understand what is going
2689 on when experimenting with \textit{nitpick\_} attributes.
2691 \section{Standard ML Interface}
2692 \label{standard-ml-interface}
2694 Nitpick provides a rich Standard ML interface used mainly for internal purposes
2695 and debugging. Among the most interesting functions exported by Nitpick are
2696 those that let you invoke the tool programmatically and those that let you
2697 register and unregister custom coinductive datatypes as well as term
2700 \subsection{Invocation of Nitpick}
2701 \label{invocation-of-nitpick}
2703 The \textit{Nitpick} structure offers the following functions for invoking your
2704 favorite counterexample generator:
2707 $\textbf{val}\,~\textit{pick\_nits\_in\_term} : \\
2708 \hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{term~list} \rightarrow \textit{term} \\
2709 \hbox{}\quad{\rightarrow}\; \textit{string} * \textit{Proof.state}$ \\
2710 $\textbf{val}\,~\textit{pick\_nits\_in\_subgoal} : \\
2711 \hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{int} \rightarrow \textit{string} * \textit{Proof.state}$
2714 The return value is a new proof state paired with an outcome string
2715 (``genuine'', ``quasi\_genuine'', ``potential'', ``none'', or ``unknown''). The
2716 \textit{params} type is a large record that lets you set Nitpick's options. The
2717 current default options can be retrieved by calling the following function
2718 defined in the \textit{Nitpick\_Isar} structure:
2721 $\textbf{val}\,~\textit{default\_params} :\,
2722 \textit{theory} \rightarrow (\textit{string} * \textit{string})~\textit{list} \rightarrow \textit{params}$
2725 The second argument lets you override option values before they are parsed and
2726 put into a \textit{params} record. Here is an example:
2729 $\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout\/}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
2730 $\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t]
2731 & \textit{state}~\textit{params}~\textit{false} \\[-2pt]
2732 & \textit{subgoal}\end{aligned}$
2737 \subsection{Registration of Coinductive Datatypes}
2738 \label{registration-of-coinductive-datatypes}
2740 If you have defined a custom coinductive datatype, you can tell Nitpick about
2741 it, so that it can use an efficient Kodkod axiomatization similar to the one it
2742 uses for lazy lists. The interface for registering and unregistering coinductive
2743 datatypes consists of the following pair of functions defined in the
2744 \textit{Nitpick} structure:
2747 $\textbf{val}\,~\textit{register\_codatatype} :\,
2748 \textit{typ} \rightarrow \textit{string} \rightarrow \textit{styp~list} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\
2749 $\textbf{val}\,~\textit{unregister\_codatatype} :\,
2750 \textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$
2753 The type $'a~\textit{llist}$ of lazy lists is already registered; had it
2754 not been, you could have told Nitpick about it by adding the following line
2755 to your theory file:
2758 $\textbf{setup}~\,\{{*}\,~\!\begin{aligned}[t]
2759 & \textit{Nitpick.register\_codatatype} \\[-2pt]
2760 & \qquad @\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}~@\{\antiq{const\_name}~ \textit{llist\_case}\} \\[-2pt] %% TYPESETTING
2761 & \qquad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])\,\ {*}\}\end{aligned}$
2764 The \textit{register\_codatatype} function takes a coinductive type, its case
2765 function, and the list of its constructors. The case function must take its
2766 arguments in the order that the constructors are listed. If no case function
2767 with the correct signature is available, simply pass the empty string.
2769 On the other hand, if your goal is to cripple Nitpick, add the following line to
2770 your theory file and try to check a few conjectures about lazy lists:
2773 $\textbf{setup}~\,\{{*}\,~\textit{Nitpick.unregister\_codatatype}~@\{\antiq{typ}~``
2774 \kern1pt'a~\textit{list\/}\textrm{''}\}\ \,{*}\}$
2777 Inductive datatypes can be registered as coinductive datatypes, given
2778 appropriate coinductive constructors. However, doing so precludes
2779 the use of the inductive constructors---Nitpick will generate an error if they
2782 \subsection{Registration of Term Postprocessors}
2783 \label{registration-of-term-postprocessors}
2785 It is possible to change the output of any term that Nitpick considers a
2786 datatype by registering a term postprocessor. The interface for registering and
2787 unregistering postprocessors consists of the following pair of functions defined
2788 in the \textit{Nitpick} structure:
2791 $\textbf{type}\,~\textit{term\_postprocessor}\,~{=} {}$ \\
2792 $\hbox{}\quad\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \rightarrow \textit{term}$ \\
2793 $\textbf{val}\,~\textit{register\_term\_postprocessors} : {}$ \\
2794 $\hbox{}\quad\textit{typ} \rightarrow \textit{term\_postprocessor} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\
2795 $\textbf{val}\,~\textit{unregister\_term\_postprocessors} :\,
2796 \textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$
2799 \S\ref{typedefs-quotient-types-records-rationals-and-reals} and
2800 \texttt{src/HOL/Library/Multiset.thy} illustrate this feature in context.
2802 \section{Known Bugs and Limitations}
2803 \label{known-bugs-and-limitations}
2805 Here are the known bugs and limitations in Nitpick at the time of writing:
2808 \item[$\bullet$] Underspecified functions defined using the \textbf{primrec},
2809 \textbf{function}, or \textbf{nominal\_\allowbreak primrec} packages can lead
2810 Nitpick to generate spurious counterexamples for theorems that refer to values
2811 for which the function is not defined. For example:
2814 \textbf{primrec} \textit{prec} \textbf{where} \\
2815 ``$\textit{prec}~(\textit{Suc}~n) = n$'' \\[2\smallskipamount]
2816 \textbf{lemma} ``$\textit{prec}~0 = \undef$'' \\
2817 \textbf{nitpick} \\[2\smallskipamount]
2818 \quad{\slshape Nitpick found a counterexample for \textit{card nat}~= 2:
2820 \\[2\smallskipamount]
2821 \hbox{}\qquad Empty assignment} \nopagebreak\\[2\smallskipamount]
2822 \textbf{by}~(\textit{auto simp}:~\textit{prec\_def})
2825 Such theorems are considered bad style because they rely on the internal
2826 representation of functions synthesized by Isabelle, which is an implementation
2829 \item[$\bullet$] Axioms that restrict the possible values of the
2830 \textit{undefined} constant are in general ignored.
2832 \item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions,
2833 which can become invalid if you change the definition of an inductive predicate
2834 that is registered in the cache. To clear the cache,
2835 run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
2836 501$\,\textit{ms}$).
2838 \item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
2839 \textbf{guess} command in a structured proof.
2841 \item[$\bullet$] The \textit{nitpick\_} attributes and the
2842 \textit{Nitpick.register\_} functions can cause havoc if used improperly.
2844 \item[$\bullet$] Although this has never been observed, arbitrary theorem
2845 morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
2847 \item[$\bullet$] All constants, types, free variables, and schematic variables
2848 whose names start with \textit{Nitpick}{.} are reserved for internal use.
2852 \bibliography{../manual}{}
2853 \bibliographystyle{abbrv}