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