1 \documentclass[a4paper,12pt]{article}
2 \usepackage[T1]{fontenc}
5 \usepackage[english,french]{babel}
12 %\usepackage[scaled=.85]{beramono}
13 \usepackage{../../lib/texinputs/isabelle,../iman,../pdfsetup}
16 %\evensidemargin=4.6mm
23 \def\Colon{\mathord{:\mkern-1.5mu:}}
24 %\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
25 %\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
26 \def\lparr{\mathopen{(\mkern-4mu\mid}}
27 \def\rparr{\mathclose{\mid\mkern-4mu)}}
30 \def\undef{(\lambda x.\; \unk)}
31 %\def\unr{\textit{others}}
33 \def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
34 \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
36 \hyphenation{Mini-Sat size-change First-Steps grand-parent nit-pick
37 counter-example counter-examples data-type data-types co-data-type
38 co-data-types in-duc-tive co-in-duc-tive}
44 \selectlanguage{english}
46 \title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]
47 Picking Nits \\[\smallskipamount]
48 \Large A User's Guide to Nitpick for Isabelle/HOL}
50 Jasmin Christian Blanchette \\
51 {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
58 \setlength{\parskip}{.7em plus .2em minus .1em}
59 \setlength{\parindent}{0pt}
60 \setlength{\abovedisplayskip}{\parskip}
61 \setlength{\abovedisplayshortskip}{.9\parskip}
62 \setlength{\belowdisplayskip}{\parskip}
63 \setlength{\belowdisplayshortskip}{.9\parskip}
65 % General-purpose enum environment with correct spacing
66 \newenvironment{enum}%
68 \setlength{\topsep}{.1\parskip}%
69 \setlength{\partopsep}{.1\parskip}%
70 \setlength{\itemsep}{\parskip}%
71 \advance\itemsep by-\parsep}}
74 \def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
75 \advance\rightskip by\leftmargin}
76 \def\post{\vskip0pt plus1ex\endgroup}
78 \def\prew{\pre\advance\rightskip by-\leftmargin}
81 \section{Introduction}
84 Nitpick \cite{blanchette-nipkow-2010} is a counterexample generator for
85 Isabelle/HOL \cite{isa-tutorial} that is designed to handle formulas
86 combining (co)in\-duc\-tive datatypes, (co)in\-duc\-tively defined predicates, and
87 quantifiers. It builds on Kodkod \cite{torlak-jackson-2007}, a highly optimized
88 first-order relational model finder developed by the Software Design Group at
89 MIT. It is conceptually similar to Refute \cite{weber-2008}, from which it
90 borrows many ideas and code fragments, but it benefits from Kodkod's
91 optimizations and a new encoding scheme. The name Nitpick is shamelessly
92 appropriated from a now retired Alloy precursor.
94 Nitpick is easy to use---you simply enter \textbf{nitpick} after a putative
95 theorem and wait a few seconds. Nonetheless, there are situations where knowing
96 how it works under the hood and how it reacts to various options helps
97 increase the test coverage. This manual also explains how to install the tool on
98 your workstation. Should the motivation fail you, think of the many hours of
99 hard work Nitpick will save you. Proving non-theorems is \textsl{hard work}.
101 Another common use of Nitpick is to find out whether the axioms of a locale are
102 satisfiable, while the locale is being developed. To check this, it suffices to
106 \textbf{lemma}~``$\textit{False}$'' \\
107 \textbf{nitpick}~[\textit{show\_all}]
110 after the locale's \textbf{begin} keyword. To falsify \textit{False}, Nitpick
111 must find a model for the axioms. If it finds no model, we have an indication
112 that the axioms might be unsatisfiable.
114 You can also invoke Nitpick from the ``Commands'' submenu of the
115 ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c C-a
116 C-n. This is equivalent to entering the \textbf{nitpick} command with no
117 arguments in the theory text.
119 Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.5 virtual
120 machine called \texttt{java}. To run Nitpick, you must also make sure that the
121 theory \textit{Nitpick} is imported---this is rarely a problem in practice
122 since it is part of \textit{Main}.
124 Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
125 Nitpick also provides an automatic mode that can be enabled via the ``Auto
126 Nitpick'' option from the ``Isabelle'' menu in Proof General. In this mode,
127 Nitpick is run on every newly entered theorem. The time limit for Auto Nitpick
128 and other automatic tools can be set using the ``Auto Tools Time Limit'' option.
131 \setbox\boxA=\hbox{\texttt{nospam}}
133 The examples presented in this manual can be found
134 in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_Examples/Manual\_Nits.thy} theory.
135 The known bugs and limitations at the time of writing are listed in
136 \S\ref{known-bugs-and-limitations}. Comments and bug reports concerning Nitpick
137 or this manual should be directed to
138 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
139 in.\allowbreak tum.\allowbreak de}.
141 \vskip2.5\smallskipamount
143 \textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
144 suggesting several textual improvements.
145 % and Perry James for reporting a typo.
147 %\section{Installation}
148 %\label{installation}
152 % * Nitpick is part of Isabelle/HOL
153 % * but it relies on an external tool called Kodkodi (Kodkod wrapper)
155 % * if you use a prebuilt Isabelle package, Kodkodi is automatically there
156 % * if you work from sources, the latest Kodkodi can be obtained from ...
157 % download it, install it in some directory of your choice (e.g.,
158 % $ISABELLE_HOME/contrib/kodkodi), and add the absolute path to Kodkodi
159 % in your .isabelle/etc/components file
161 % * If you're not sure, just try the example in the next section
163 \section{First Steps}
166 This section introduces Nitpick by presenting small examples. If possible, you
167 should try out the examples on your workstation. Your theory file should start
171 \textbf{theory}~\textit{Scratch} \\
172 \textbf{imports}~\textit{Main~Quotient\_Product~RealDef} \\
176 The results presented here were obtained using the JNI (Java Native Interface)
177 version of MiniSat and with multithreading disabled to reduce nondeterminism.
178 This was done by adding the line
181 \textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1]
184 after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
185 Kodkodi and is precompiled for the major platforms. Other SAT solvers can also
186 be installed, as explained in \S\ref{optimizations}. If you have already
187 configured SAT solvers in Isabelle (e.g., for Refute), these will also be
188 available to Nitpick.
190 \subsection{Propositional Logic}
191 \label{propositional-logic}
193 Let's start with a trivial example from propositional logic:
196 \textbf{lemma}~``$P \longleftrightarrow Q$'' \\
200 You should get the following output:
204 Nitpick found a counterexample: \\[2\smallskipamount]
205 \hbox{}\qquad Free variables: \nopagebreak \\
206 \hbox{}\qquad\qquad $P = \textit{True}$ \\
207 \hbox{}\qquad\qquad $Q = \textit{False}$
210 %FIXME: If you get the output:...
211 %Then do such-and-such.
213 Nitpick can also be invoked on individual subgoals, as in the example below:
216 \textbf{apply}~\textit{auto} \\[2\smallskipamount]
217 {\slshape goal (2 subgoals): \\
218 \phantom{0}1. $P\,\Longrightarrow\, Q$ \\
219 \phantom{0}2. $Q\,\Longrightarrow\, P$} \\[2\smallskipamount]
220 \textbf{nitpick}~1 \\[2\smallskipamount]
221 {\slshape Nitpick found a counterexample: \\[2\smallskipamount]
222 \hbox{}\qquad Free variables: \nopagebreak \\
223 \hbox{}\qquad\qquad $P = \textit{True}$ \\
224 \hbox{}\qquad\qquad $Q = \textit{False}$} \\[2\smallskipamount]
225 \textbf{nitpick}~2 \\[2\smallskipamount]
226 {\slshape Nitpick found a counterexample: \\[2\smallskipamount]
227 \hbox{}\qquad Free variables: \nopagebreak \\
228 \hbox{}\qquad\qquad $P = \textit{False}$ \\
229 \hbox{}\qquad\qquad $Q = \textit{True}$} \\[2\smallskipamount]
233 \subsection{Type Variables}
234 \label{type-variables}
236 If you are left unimpressed by the previous example, don't worry. The next
237 one is more mind- and computer-boggling:
240 \textbf{lemma} ``$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
242 \pagebreak[2] %% TYPESETTING
244 The putative lemma involves the definite description operator, {THE}, presented
245 in section 5.10.1 of the Isabelle tutorial \cite{isa-tutorial}. The
246 operator is defined by the axiom $(\textrm{THE}~x.\; x = a) = a$. The putative
247 lemma is merely asserting the indefinite description operator axiom with {THE}
248 substituted for {SOME}.
250 The free variable $x$ and the bound variable $y$ have type $'a$. For formulas
251 containing type variables, Nitpick enumerates the possible domains for each type
252 variable, up to a given cardinality (10 by default), looking for a finite
256 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
258 Trying 10 scopes: \nopagebreak \\
259 \hbox{}\qquad \textit{card}~$'a$~= 1; \\
260 \hbox{}\qquad \textit{card}~$'a$~= 2; \\
261 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
262 \hbox{}\qquad \textit{card}~$'a$~= 10. \\[2\smallskipamount]
263 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
264 \hbox{}\qquad Free variables: \nopagebreak \\
265 \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
266 \hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount]
270 Nitpick found a counterexample in which $'a$ has cardinality 3. (For
271 cardinalities 1 and 2, the formula holds.) In the counterexample, the three
272 values of type $'a$ are written $a_1$, $a_2$, and $a_3$.
274 The message ``Trying $n$ scopes: {\ldots}''\ is shown only if the option
275 \textit{verbose} is enabled. You can specify \textit{verbose} each time you
276 invoke \textbf{nitpick}, or you can set it globally using the command
279 \textbf{nitpick\_params} [\textit{verbose}]
282 This command also displays the current default values for all of the options
283 supported by Nitpick. The options are listed in \S\ref{option-reference}.
285 \subsection{Constants}
288 By just looking at Nitpick's output, it might not be clear why the
289 counterexample in \S\ref{type-variables} is genuine. Let's invoke Nitpick again,
290 this time telling it to show the values of the constants that occur in the
294 \textbf{lemma}~``$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$'' \\
295 \textbf{nitpick}~[\textit{show\_consts}] \\[2\smallskipamount]
297 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
298 \hbox{}\qquad Free variables: \nopagebreak \\
299 \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
300 \hbox{}\qquad\qquad $x = a_3$ \\
301 \hbox{}\qquad Constant: \nopagebreak \\
302 \hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$
305 As the result of an optimization, Nitpick directly assigned a value to the
306 subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we
307 disable this optimization by using the command
310 \textbf{nitpick}~[\textit{dont\_specialize},\, \textit{show\_consts}]
316 \slshape Constant: \nopagebreak \\
317 \hbox{}\qquad $\mathit{The} = \undef{}
318 (\!\begin{aligned}[t]%
319 & \{a_1, a_2, a_3\} := a_3,\> \{a_1, a_2\} := a_3,\> \{a_1, a_3\} := a_3, \\[-2pt] %% TYPESETTING
320 & \{a_1\} := a_1,\> \{a_2, a_3\} := a_1,\> \{a_2\} := a_2, \\[-2pt]
321 & \{a_3\} := a_3,\> \{\} := a_3)\end{aligned}$
324 Notice that $\textit{The}~(\lambda y.\;P~y) = \textit{The}~\{a_2, a_3\} = a_1$,
325 just like before.\footnote{The Isabelle/HOL notation $f(x :=
326 y)$ denotes the function that maps $x$ to $y$ and that otherwise behaves like
329 Our misadventures with THE suggest adding `$\exists!x{.}$' (``there exists a
330 unique $x$ such that'') at the front of our putative lemma's assumption:
333 \textbf{lemma}~``$\exists {!}x.\; P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
336 The fix appears to work:
339 \textbf{nitpick} \\[2\smallskipamount]
340 \slshape Nitpick found no counterexample.
343 We can further increase our confidence in the formula by exhausting all
344 cardinalities up to 50:
347 \textbf{nitpick} [\textit{card} $'a$~= 1--50]\footnote{The symbol `--'
348 can be entered as \texttt{-} (hyphen) or
349 \texttt{\char`\\\char`\<emdash\char`\>}.} \\[2\smallskipamount]
350 \slshape Nitpick found no counterexample.
353 Let's see if Sledgehammer can find a proof:
356 \textbf{sledgehammer} \\[2\smallskipamount]
357 {\slshape Sledgehammer: external prover ``$e$'' for subgoal 1: \\
358 $\exists{!}x.\; P~x\,\Longrightarrow\, P~(\hbox{\slshape THE}~y.\; P~y)$ \\
359 Try this command: \textrm{apply}~(\textit{metis~the\_equality})} \\[2\smallskipamount]
360 \textbf{apply}~(\textit{metis~the\_equality\/}) \nopagebreak \\[2\smallskipamount]
361 {\slshape No subgoals!}% \\[2\smallskipamount]
365 This must be our lucky day.
367 \subsection{Skolemization}
368 \label{skolemization}
370 Are all invertible functions onto? Let's find out:
373 \textbf{lemma} ``$\exists g.\; \forall x.~g~(f~x) = x
374 \,\Longrightarrow\, \forall y.\; \exists x.~y = f~x$'' \\
375 \textbf{nitpick} \\[2\smallskipamount]
377 Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\[2\smallskipamount]
378 \hbox{}\qquad Free variable: \nopagebreak \\
379 \hbox{}\qquad\qquad $f = \undef{}(b_1 := a_1)$ \\
380 \hbox{}\qquad Skolem constants: \nopagebreak \\
381 \hbox{}\qquad\qquad $g = \undef{}(a_1 := b_1,\> a_2 := b_1)$ \\
382 \hbox{}\qquad\qquad $y = a_2$
385 Although $f$ is the only free variable occurring in the formula, Nitpick also
386 displays values for the bound variables $g$ and $y$. These values are available
387 to Nitpick because it performs skolemization as a preprocessing step.
389 In the previous example, skolemization only affected the outermost quantifiers.
390 This is not always the case, as illustrated below:
393 \textbf{lemma} ``$\exists x.\; \forall f.\; f~x = x$'' \\
394 \textbf{nitpick} \\[2\smallskipamount]
396 Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
397 \hbox{}\qquad Skolem constant: \nopagebreak \\
398 \hbox{}\qquad\qquad $\lambda x.\; f =
399 \undef{}(\!\begin{aligned}[t]
400 & a_1 := \undef{}(a_1 := a_2,\> a_2 := a_1), \\[-2pt]
401 & a_2 := \undef{}(a_1 := a_1,\> a_2 := a_1))\end{aligned}$
404 The variable $f$ is bound within the scope of $x$; therefore, $f$ depends on
405 $x$, as suggested by the notation $\lambda x.\,f$. If $x = a_1$, then $f$ is the
406 function that maps $a_1$ to $a_2$ and vice versa; otherwise, $x = a_2$ and $f$
407 maps both $a_1$ and $a_2$ to $a_1$. In both cases, $f~x \not= x$.
409 The source of the Skolem constants is sometimes more obscure:
412 \textbf{lemma} ``$\mathit{refl}~r\,\Longrightarrow\, \mathit{sym}~r$'' \\
413 \textbf{nitpick} \\[2\smallskipamount]
415 Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
416 \hbox{}\qquad Free variable: \nopagebreak \\
417 \hbox{}\qquad\qquad $r = \{(a_1, a_1),\, (a_2, a_1),\, (a_2, a_2)\}$ \\
418 \hbox{}\qquad Skolem constants: \nopagebreak \\
419 \hbox{}\qquad\qquad $\mathit{sym}.x = a_2$ \\
420 \hbox{}\qquad\qquad $\mathit{sym}.y = a_1$
423 What happened here is that Nitpick expanded the \textit{sym} constant to its
427 $\mathit{sym}~r \,\equiv\,
428 \forall x\> y.\,\> (x, y) \in r \longrightarrow (y, x) \in r.$
431 As their names suggest, the Skolem constants $\mathit{sym}.x$ and
432 $\mathit{sym}.y$ are simply the bound variables $x$ and $y$
433 from \textit{sym}'s definition.
435 \subsection{Natural Numbers and Integers}
436 \label{natural-numbers-and-integers}
438 Because of the axiom of infinity, the type \textit{nat} does not admit any
439 finite models. To deal with this, Nitpick's approach is to consider finite
440 subsets $N$ of \textit{nat} and maps all numbers $\notin N$ to the undefined
441 value (displayed as `$\unk$'). The type \textit{int} is handled similarly.
442 Internally, undefined values lead to a three-valued logic.
444 Here is an example involving \textit{int\/}:
447 \textbf{lemma} ``$\lbrakk i \le j;\> n \le (m{\Colon}\mathit{int})\rbrakk \,\Longrightarrow\, i * n + j * m \le i * m + j * n$'' \\
448 \textbf{nitpick} \\[2\smallskipamount]
449 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
450 \hbox{}\qquad Free variables: \nopagebreak \\
451 \hbox{}\qquad\qquad $i = 0$ \\
452 \hbox{}\qquad\qquad $j = 1$ \\
453 \hbox{}\qquad\qquad $m = 1$ \\
454 \hbox{}\qquad\qquad $n = 0$
457 Internally, Nitpick uses either a unary or a binary representation of numbers.
458 The unary representation is more efficient but only suitable for numbers very
459 close to zero. By default, Nitpick attempts to choose the more appropriate
460 encoding by inspecting the formula at hand. This behavior can be overridden by
461 passing either \textit{unary\_ints} or \textit{binary\_ints} as option. For
462 binary notation, the number of bits to use can be specified using
463 the \textit{bits} option. For example:
466 \textbf{nitpick} [\textit{binary\_ints}, \textit{bits}${} = 16$]
469 With infinite types, we don't always have the luxury of a genuine counterexample
470 and must often content ourselves with a potentially spurious one. The tedious
471 task of finding out whether the potentially spurious counterexample is in fact
472 genuine can be delegated to \textit{auto} by passing \textit{check\_potential}.
476 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
477 \textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[2\smallskipamount]
478 \slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
479 fragment. Only potentially spurious counterexamples may be found. \\[2\smallskipamount]
480 Nitpick found a potentially spurious counterexample: \\[2\smallskipamount]
481 \hbox{}\qquad Free variable: \nopagebreak \\
482 \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
483 Confirmation by ``\textit{auto}'': The above counterexample is genuine.
486 You might wonder why the counterexample is first reported as potentially
487 spurious. The root of the problem is that the bound variable in $\forall n.\;
488 \textit{Suc}~n \mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds
489 an $n$ such that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
490 \textit{False}; but otherwise, it does not know anything about values of $n \ge
491 \textit{card~nat}$ and must therefore evaluate the assumption to $\unk$, not
492 \textit{True}. Since the assumption can never be satisfied, the putative lemma
493 can never be falsified.
495 Incidentally, if you distrust the so-called genuine counterexamples, you can
496 enable \textit{check\_\allowbreak genuine} to verify them as well. However, be
497 aware that \textit{auto} will usually fail to prove that the counterexample is
500 Some conjectures involving elementary number theory make Nitpick look like a
501 giant with feet of clay:
504 \textbf{lemma} ``$P~\textit{Suc}$'' \\
505 \textbf{nitpick} \\[2\smallskipamount]
507 Nitpick found no counterexample.
510 On any finite set $N$, \textit{Suc} is a partial function; for example, if $N =
511 \{0, 1, \ldots, k\}$, then \textit{Suc} is $\{0 \mapsto 1,\, 1 \mapsto 2,\,
512 \ldots,\, k \mapsto \unk\}$, which evaluates to $\unk$ when passed as
513 argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$. The next
517 \textbf{lemma} ``$P~(\textit{op}~{+}\Colon
518 \textit{nat}\mathbin{\Rightarrow}\textit{nat}\mathbin{\Rightarrow}\textit{nat})$'' \\
519 \textbf{nitpick} [\textit{card nat} = 1] \\[2\smallskipamount]
520 {\slshape Nitpick found a counterexample:} \\[2\smallskipamount]
521 \hbox{}\qquad Free variable: \nopagebreak \\
522 \hbox{}\qquad\qquad $P = \{\}$ \\[2\smallskipamount]
523 \textbf{nitpick} [\textit{card nat} = 2] \\[2\smallskipamount]
524 {\slshape Nitpick found no counterexample.}
527 The problem here is that \textit{op}~+ is total when \textit{nat} is taken to be
528 $\{0\}$ but becomes partial as soon as we add $1$, because $1 + 1 \notin \{0,
531 Because numbers are infinite and are approximated using a three-valued logic,
532 there is usually no need to systematically enumerate domain sizes. If Nitpick
533 cannot find a genuine counterexample for \textit{card~nat}~= $k$, it is very
534 unlikely that one could be found for smaller domains. (The $P~(\textit{op}~{+})$
535 example above is an exception to this principle.) Nitpick nonetheless enumerates
536 all cardinalities from 1 to 10 for \textit{nat}, mainly because smaller
537 cardinalities are fast to handle and give rise to simpler counterexamples. This
538 is explained in more detail in \S\ref{scope-monotonicity}.
540 \subsection{Inductive Datatypes}
541 \label{inductive-datatypes}
543 Like natural numbers and integers, inductive datatypes with recursive
544 constructors admit no finite models and must be approximated by a subterm-closed
545 subset. For example, using a cardinality of 10 for ${'}a~\textit{list}$,
546 Nitpick looks for all counterexamples that can be built using at most 10
549 Let's see with an example involving \textit{hd} (which returns the first element
550 of a list) and $@$ (which concatenates two lists):
553 \textbf{lemma} ``$\textit{hd}~(\textit{xs} \mathbin{@} [y, y]) = \textit{hd}~\textit{xs}$'' \\
554 \textbf{nitpick} \\[2\smallskipamount]
555 \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
556 \hbox{}\qquad Free variables: \nopagebreak \\
557 \hbox{}\qquad\qquad $\textit{xs} = []$ \\
558 \hbox{}\qquad\qquad $\textit{y} = a_1$
561 To see why the counterexample is genuine, we enable \textit{show\_consts}
562 and \textit{show\_\allowbreak datatypes}:
565 {\slshape Datatype:} \\
566 \hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_1],\, [a_1, a_1],\, \unr\}$ \\
567 {\slshape Constants:} \\
568 \hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_1, a_1])$ \\
569 \hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_1] := a_1,\> [a_1, a_1] := a_1)$
572 Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value,
575 The second constant, $\lambda x_1.\; x_1 \mathbin{@} [y, y]$, is simply the
576 append operator whose second argument is fixed to be $[y, y]$. Appending $[a_1,
577 a_1]$ to $[a_1]$ would normally give $[a_1, a_1, a_1]$, but this value is not
578 representable in the subset of $'a$~\textit{list} considered by Nitpick, which
579 is shown under the ``Datatype'' heading; hence the result is $\unk$. Similarly,
580 appending $[a_1, a_1]$ to itself gives $\unk$.
582 Given \textit{card}~$'a = 3$ and \textit{card}~$'a~\textit{list} = 3$, Nitpick
583 considers the following subsets:
585 \kern-.5\smallskipamount %% TYPESETTING
589 $\{[],\, [a_1],\, [a_2]\}$; \\
590 $\{[],\, [a_1],\, [a_3]\}$; \\
591 $\{[],\, [a_2],\, [a_3]\}$; \\
592 $\{[],\, [a_1],\, [a_1, a_1]\}$; \\
593 $\{[],\, [a_1],\, [a_2, a_1]\}$; \\
594 $\{[],\, [a_1],\, [a_3, a_1]\}$; \\
595 $\{[],\, [a_2],\, [a_1, a_2]\}$; \\
596 $\{[],\, [a_2],\, [a_2, a_2]\}$; \\
597 $\{[],\, [a_2],\, [a_3, a_2]\}$; \\
598 $\{[],\, [a_3],\, [a_1, a_3]\}$; \\
599 $\{[],\, [a_3],\, [a_2, a_3]\}$; \\
600 $\{[],\, [a_3],\, [a_3, a_3]\}$.
604 \kern-2\smallskipamount %% TYPESETTING
606 All subterm-closed subsets of $'a~\textit{list}$ consisting of three values
607 are listed and only those. As an example of a non-subterm-closed subset,
608 consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_2]\}$, and observe
609 that $[a_1, a_2]$ (i.e., $a_1 \mathbin{\#} [a_2]$) has $[a_2] \notin
610 \mathcal{S}$ as a subterm.
612 Here's another m\"ochtegern-lemma that Nitpick can refute without a blink:
615 \textbf{lemma} ``$\lbrakk \textit{length}~\textit{xs} = 1;\> \textit{length}~\textit{ys} = 1
616 \rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$''
618 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
619 \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
620 \hbox{}\qquad Free variables: \nopagebreak \\
621 \hbox{}\qquad\qquad $\textit{xs} = [a_1]$ \\
622 \hbox{}\qquad\qquad $\textit{ys} = [a_2]$ \\
623 \hbox{}\qquad Datatypes: \\
624 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
625 \hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_1],\, [a_2],\, \unr\}$
628 Because datatypes are approximated using a three-valued logic, there is usually
629 no need to systematically enumerate cardinalities: If Nitpick cannot find a
630 genuine counterexample for \textit{card}~$'a~\textit{list}$~= 10, it is very
631 unlikely that one could be found for smaller cardinalities.
633 \subsection{Typedefs, Quotient Types, Records, Rationals, and Reals}
634 \label{typedefs-quotient-types-records-rationals-and-reals}
636 Nitpick generally treats types declared using \textbf{typedef} as datatypes
637 whose single constructor is the corresponding \textit{Abs\_\kern.1ex} function.
641 \textbf{typedef}~\textit{three} = ``$\{0\Colon\textit{nat},\, 1,\, 2\}$'' \\
642 \textbf{by}~\textit{blast} \\[2\smallskipamount]
643 \textbf{definition}~$A \mathbin{\Colon} \textit{three}$ \textbf{where} ``\kern-.1em$A \,\equiv\, \textit{Abs\_\allowbreak three}~0$'' \\
644 \textbf{definition}~$B \mathbin{\Colon} \textit{three}$ \textbf{where} ``$B \,\equiv\, \textit{Abs\_three}~1$'' \\
645 \textbf{definition}~$C \mathbin{\Colon} \textit{three}$ \textbf{where} ``$C \,\equiv\, \textit{Abs\_three}~2$'' \\[2\smallskipamount]
646 \textbf{lemma} ``$\lbrakk P~A;\> P~B\rbrakk \,\Longrightarrow\, P~x$'' \\
647 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
648 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
649 \hbox{}\qquad Free variables: \nopagebreak \\
650 \hbox{}\qquad\qquad $P = \{\Abs{0},\, \Abs{1}\}$ \\
651 \hbox{}\qquad\qquad $x = \Abs{2}$ \\
652 \hbox{}\qquad Datatypes: \\
653 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
654 \hbox{}\qquad\qquad $\textit{three} = \{\Abs{0},\, \Abs{1},\, \Abs{2},\, \unr\}$
657 In the output above, $\Abs{n}$ abbreviates $\textit{Abs\_three}~n$.
659 Quotient types are handled in much the same way. The following fragment defines
660 the integer type \textit{my\_int} by encoding the integer $x$ by a pair of
661 natural numbers $(m, n)$ such that $x + n = m$:
664 \textbf{fun} \textit{my\_int\_rel} \textbf{where} \\
665 ``$\textit{my\_int\_rel}~(x,\, y)~(u,\, v) = (x + v = u + y)$'' \\[2\smallskipamount]
667 \textbf{quotient\_type}~\textit{my\_int} = ``$\textit{nat} \times \textit{nat\/}$''$\;{/}\;$\textit{my\_int\_rel} \\
668 \textbf{by}~(\textit{auto simp add\/}:\ \textit{equivp\_def expand\_fun\_eq}) \\[2\smallskipamount]
670 \textbf{definition}~\textit{add\_raw}~\textbf{where} \\
671 ``$\textit{add\_raw} \,\equiv\, \lambda(x,\, y)~(u,\, v).\; (x + (u\Colon\textit{nat}), y + (v\Colon\textit{nat}))$'' \\[2\smallskipamount]
673 \textbf{quotient\_definition} ``$\textit{add\/}\Colon\textit{my\_int} \Rightarrow \textit{my\_int} \Rightarrow \textit{my\_int\/}$'' \textbf{is} \textit{add\_raw} \\[2\smallskipamount]
675 \textbf{lemma} ``$\textit{add}~x~y = \textit{add}~x~x$'' \\
676 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
677 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
678 \hbox{}\qquad Free variables: \nopagebreak \\
679 \hbox{}\qquad\qquad $x = \Abs{(0,\, 0)}$ \\
680 \hbox{}\qquad\qquad $y = \Abs{(1,\, 0)}$ \\
681 \hbox{}\qquad Datatypes: \\
682 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, \unr\}$ \\
683 \hbox{}\qquad\qquad $\textit{nat} \times \textit{nat}~[\textsl{boxed\/}] = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
684 \hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(1,\, 0)},\> \unr\}$
687 In the counterexample, $\Abs{(0,\, 0)}$ and $\Abs{(1,\, 0)}$ represent the
688 integers $0$ and $1$, respectively. Other representants would have been
689 possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$. If we are going to
690 use \textit{my\_int} extensively, it pays off to install a term postprocessor
691 that converts the pair notation to the standard mathematical notation:
694 $\textbf{ML}~\,\{{*} \\
696 %& ({*}~\,\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \\[-2pt]
697 %& \phantom{(*}~\,{\rightarrow}\;\textit{term}~\,{*}) \\[-2pt]
698 & \textbf{fun}\,~\textit{my\_int\_postproc}~\_~\_~\_~T~(\textit{Const}~\_~\$~(\textit{Const}~\_~\$~\textit{t1}~\$~\textit{t2\/})) = {} \\[-2pt]
699 & \phantom{fun}\,~\textit{HOLogic.mk\_number}~T~(\textit{snd}~(\textit{HOLogic.dest\_number~t1}) \\[-2pt]
700 & \phantom{fun\,~\textit{HOLogic.mk\_number}~T~(}{-}~\textit{snd}~(\textit{HOLogic.dest\_number~t2\/})) \\[-2pt]
701 & \phantom{fun}\!{\mid}\,~\textit{my\_int\_postproc}~\_~\_~\_~\_~t = t \\[-2pt]
702 {*}\}\end{aligned}$ \\[2\smallskipamount]
703 $\textbf{declaration}~\,\{{*} \\
705 & \textit{Nitpick\_Model.register\_term\_postprocessor}~\!\begin{aligned}[t]
706 & @\{\textrm{typ}~\textit{my\_int}\} \\[-2pt]
707 & \textit{my\_int\_postproc}\end{aligned} \\[-2pt]
711 Records are also handled as datatypes with a single constructor:
714 \textbf{record} \textit{point} = \\
715 \hbox{}\quad $\textit{Xcoord} \mathbin{\Colon} \textit{int}$ \\
716 \hbox{}\quad $\textit{Ycoord} \mathbin{\Colon} \textit{int}$ \\[2\smallskipamount]
717 \textbf{lemma} ``$\textit{Xcoord}~(p\Colon\textit{point}) = \textit{Xcoord}~(q\Colon\textit{point})$'' \\
718 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
719 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
720 \hbox{}\qquad Free variables: \nopagebreak \\
721 \hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
722 \hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
723 \hbox{}\qquad Datatypes: \\
724 \hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, \unr\}$ \\
725 \hbox{}\qquad\qquad $\textit{point} = \{\!\begin{aligned}[t]
726 & \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr, \\[-2pt] %% TYPESETTING
727 & \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
730 Finally, Nitpick provides rudimentary support for rationals and reals using a
734 \textbf{lemma} ``$4 * x + 3 * (y\Colon\textit{real}) \not= 1/2$'' \\
735 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
736 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
737 \hbox{}\qquad Free variables: \nopagebreak \\
738 \hbox{}\qquad\qquad $x = 1/2$ \\
739 \hbox{}\qquad\qquad $y = -1/2$ \\
740 \hbox{}\qquad Datatypes: \\
741 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, 3,\, 4,\, 5,\, 6,\, 7,\, \unr\}$ \\
742 \hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, 2,\, 3,\, 4,\, -3,\, -2,\, -1,\, \unr\}$ \\
743 \hbox{}\qquad\qquad $\textit{real} = \{1,\, 0,\, 4,\, -3/2,\, 3,\, 2,\, 1/2,\, -1/2,\, \unr\}$
746 \subsection{Inductive and Coinductive Predicates}
747 \label{inductive-and-coinductive-predicates}
749 Inductively defined predicates (and sets) are particularly problematic for
750 counterexample generators. They can make Quickcheck~\cite{berghofer-nipkow-2004}
751 loop forever and Refute~\cite{weber-2008} run out of resources. The crux of
752 the problem is that they are defined using a least fixed-point construction.
754 Nitpick's philosophy is that not all inductive predicates are equal. Consider
755 the \textit{even} predicate below:
758 \textbf{inductive}~\textit{even}~\textbf{where} \\
759 ``\textit{even}~0'' $\,\mid$ \\
760 ``\textit{even}~$n\,\Longrightarrow\, \textit{even}~(\textit{Suc}~(\textit{Suc}~n))$''
763 This predicate enjoys the desirable property of being well-founded, which means
764 that the introduction rules don't give rise to infinite chains of the form
767 $\cdots\,\Longrightarrow\, \textit{even}~k''
768 \,\Longrightarrow\, \textit{even}~k'
769 \,\Longrightarrow\, \textit{even}~k.$
772 For \textit{even}, this is obvious: Any chain ending at $k$ will be of length
776 $\textit{even}~0\,\Longrightarrow\, \textit{even}~2\,\Longrightarrow\, \cdots
777 \,\Longrightarrow\, \textit{even}~(k - 2)
778 \,\Longrightarrow\, \textit{even}~k.$
781 Wellfoundedness is desirable because it enables Nitpick to use a very efficient
782 fixed-point computation.%
783 \footnote{If an inductive predicate is
784 well-founded, then it has exactly one fixed point, which is simultaneously the
785 least and the greatest fixed point. In these circumstances, the computation of
786 the least fixed point amounts to the computation of an arbitrary fixed point,
787 which can be performed using a straightforward recursive equation.}
788 Moreover, Nitpick can prove wellfoundedness of most well-founded predicates,
789 just as Isabelle's \textbf{function} package usually discharges termination
790 proof obligations automatically.
792 Let's try an example:
795 \textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
796 \textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
797 \slshape The inductive predicate ``\textit{even}'' was proved well-founded.
798 Nitpick can compute it efficiently. \\[2\smallskipamount]
800 \hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
801 Nitpick found a potentially spurious counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
802 \hbox{}\qquad Empty assignment \\[2\smallskipamount]
803 Nitpick could not find a better counterexample. \\[2\smallskipamount]
807 No genuine counterexample is possible because Nitpick cannot rule out the
808 existence of a natural number $n \ge 50$ such that both $\textit{even}~n$ and
809 $\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the
810 existential quantifier:
813 \textbf{lemma} ``$\exists n \mathbin{\le} 49.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
814 \textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}] \\[2\smallskipamount]
815 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
816 \hbox{}\qquad Empty assignment
819 So far we were blessed by the wellfoundedness of \textit{even}. What happens if
820 we use the following definition instead?
823 \textbf{inductive} $\textit{even}'$ \textbf{where} \\
824 ``$\textit{even}'~(0{\Colon}\textit{nat})$'' $\,\mid$ \\
825 ``$\textit{even}'~2$'' $\,\mid$ \\
826 ``$\lbrakk\textit{even}'~m;\> \textit{even}'~n\rbrakk \,\Longrightarrow\, \textit{even}'~(m + n)$''
829 This definition is not well-founded: From $\textit{even}'~0$ and
830 $\textit{even}'~0$, we can derive that $\textit{even}'~0$. Nonetheless, the
831 predicates $\textit{even}$ and $\textit{even}'$ are equivalent.
833 Let's check a property involving $\textit{even}'$. To make up for the
834 foreseeable computational hurdles entailed by non-wellfoundedness, we decrease
835 \textit{nat}'s cardinality to a mere 10:
838 \textbf{lemma}~``$\exists n \in \{0, 2, 4, 6, 8\}.\;
839 \lnot\;\textit{even}'~n$'' \\
840 \textbf{nitpick}~[\textit{card nat}~= 10,\, \textit{verbose},\, \textit{show\_consts}] \\[2\smallskipamount]
842 The inductive predicate ``$\textit{even}'\!$'' could not be proved well-founded.
843 Nitpick might need to unroll it. \\[2\smallskipamount]
845 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 0; \\
846 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 1; \\
847 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2; \\
848 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 4; \\
849 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 8; \\
850 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 9. \\[2\smallskipamount]
851 Nitpick found a counterexample for \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2: \\[2\smallskipamount]
852 \hbox{}\qquad Constant: \nopagebreak \\
853 \hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t]
854 & 2 := \{0, 2, 4, 6, 8, 1^\Q, 3^\Q, 5^\Q, 7^\Q, 9^\Q\}, \\[-2pt]
855 & 1 := \{0, 2, 4, 1^\Q, 3^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\}, \\[-2pt]
856 & 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\[2\smallskipamount]
860 Nitpick's output is very instructive. First, it tells us that the predicate is
861 unrolled, meaning that it is computed iteratively from the empty set. Then it
862 lists six scopes specifying different bounds on the numbers of iterations:\ 0,
865 The output also shows how each iteration contributes to $\textit{even}'$. The
866 notation $\lambda i.\; \textit{even}'$ indicates that the value of the
867 predicate depends on an iteration counter. Iteration 0 provides the basis
868 elements, $0$ and $2$. Iteration 1 contributes $4$ ($= 2 + 2$). Iteration 2
869 throws $6$ ($= 2 + 4 = 4 + 2$) and $8$ ($= 4 + 4$) into the mix. Further
870 iterations would not contribute any new elements.
872 Some values are marked with superscripted question
873 marks~(`\lower.2ex\hbox{$^\Q$}'). These are the elements for which the
874 predicate evaluates to $\unk$. Thus, $\textit{even}'$ evaluates to either
875 \textit{True} or $\unk$, never \textit{False}.
877 When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, 20, 24, and 28
878 iterations. However, these numbers are bounded by the cardinality of the
879 predicate's domain. With \textit{card~nat}~= 10, no more than 9 iterations are
880 ever needed to compute the value of a \textit{nat} predicate. You can specify
881 the number of iterations using the \textit{iter} option, as explained in
882 \S\ref{scope-of-search}.
884 In the next formula, $\textit{even}'$ occurs both positively and negatively:
887 \textbf{lemma} ``$\textit{even}'~(n - 2) \,\Longrightarrow\, \textit{even}'~n$'' \\
888 \textbf{nitpick} [\textit{card nat} = 10, \textit{show\_consts}] \\[2\smallskipamount]
889 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
890 \hbox{}\qquad Free variable: \nopagebreak \\
891 \hbox{}\qquad\qquad $n = 1$ \\
892 \hbox{}\qquad Constants: \nopagebreak \\
893 \hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t]
894 & 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\
895 \hbox{}\qquad\qquad $\textit{even}' \subseteq \{0, 2, 4, 6, 8, \unr\}$
898 Notice the special constraint $\textit{even}' \subseteq \{0,\, 2,\, 4,\, 6,\,
899 8,\, \unr\}$ in the output, whose right-hand side represents an arbitrary
900 fixed point (not necessarily the least one). It is used to falsify
901 $\textit{even}'~n$. In contrast, the unrolled predicate is used to satisfy
902 $\textit{even}'~(n - 2)$.
904 Coinductive predicates are handled dually. For example:
907 \textbf{coinductive} \textit{nats} \textbf{where} \\
908 ``$\textit{nats}~(x\Colon\textit{nat}) \,\Longrightarrow\, \textit{nats}~x$'' \\[2\smallskipamount]
909 \textbf{lemma} ``$\textit{nats} = \{0, 1, 2, 3, 4\}$'' \\
910 \textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
911 \slshape Nitpick found a counterexample:
912 \\[2\smallskipamount]
913 \hbox{}\qquad Constants: \nopagebreak \\
914 \hbox{}\qquad\qquad $\lambda i.\; \textit{nats} = \undef(0 := \{\!\begin{aligned}[t]
915 & 0^\Q, 1^\Q, 2^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q, \\[-2pt]
916 & \unr\})\end{aligned}$ \\
917 \hbox{}\qquad\qquad $nats \supseteq \{9, 5^\Q, 6^\Q, 7^\Q, 8^\Q, \unr\}$
920 As a special case, Nitpick uses Kodkod's transitive closure operator to encode
921 negative occurrences of non-well-founded ``linear inductive predicates,'' i.e.,
922 inductive predicates for which each the predicate occurs in at most one
923 assumption of each introduction rule. For example:
926 \textbf{inductive} \textit{odd} \textbf{where} \\
927 ``$\textit{odd}~1$'' $\,\mid$ \\
928 ``$\lbrakk \textit{odd}~m;\>\, \textit{even}~n\rbrakk \,\Longrightarrow\, \textit{odd}~(m + n)$'' \\[2\smallskipamount]
929 \textbf{lemma}~``$\textit{odd}~n \,\Longrightarrow\, \textit{odd}~(n - 2)$'' \\
930 \textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
931 \slshape Nitpick found a counterexample:
932 \\[2\smallskipamount]
933 \hbox{}\qquad Free variable: \nopagebreak \\
934 \hbox{}\qquad\qquad $n = 1$ \\
935 \hbox{}\qquad Constants: \nopagebreak \\
936 \hbox{}\qquad\qquad $\textit{even} = \{0, 2, 4, 6, 8, \unr\}$ \\
937 \hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = \{1, \unr\}$ \\
938 \hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \!
940 & \{(0, 0), (0, 2), (0, 4), (0, 6), (0, 8), (1, 1), (1, 3), (1, 5), \\[-2pt]
941 & \phantom{\{} (1, 7), (1, 9), (2, 2), (2, 4), (2, 6), (2, 8), (3, 3),
943 & \phantom{\{} (3, 7), (3, 9), (4, 4), (4, 6), (4, 8), (5, 5), (5, 7), (5, 9), \\[-2pt]
944 & \phantom{\{} (6, 6), (6, 8), (7, 7), (7, 9), (8, 8), (9, 9), \unr\}\end{aligned}$ \\
945 \hbox{}\qquad\qquad $\textit{odd} \subseteq \{1, 3, 5, 7, 9, 8^\Q, \unr\}$
949 In the output, $\textit{odd}_{\textrm{base}}$ represents the base elements and
950 $\textit{odd}_{\textrm{step}}$ is a transition relation that computes new
951 elements from known ones. The set $\textit{odd}$ consists of all the values
952 reachable through the reflexive transitive closure of
953 $\textit{odd}_{\textrm{step}}$ starting with any element from
954 $\textit{odd}_{\textrm{base}}$, namely 1, 3, 5, 7, and 9. Using Kodkod's
955 transitive closure to encode linear predicates is normally either more thorough
956 or more efficient than unrolling (depending on the value of \textit{iter}), but
957 for those cases where it isn't you can disable it by passing the
958 \textit{dont\_star\_linear\_preds} option.
960 \subsection{Coinductive Datatypes}
961 \label{coinductive-datatypes}
963 While Isabelle regrettably lacks a high-level mechanism for defining coinductive
964 datatypes, the \textit{Coinductive\_List} theory from Andreas Lochbihler's
965 \textit{Coinductive} AFP entry \cite{lochbihler-2010} provides a coinductive
966 ``lazy list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick
967 supports these lazy lists seamlessly and provides a hook, described in
968 \S\ref{registration-of-coinductive-datatypes}, to register custom coinductive
971 (Co)intuitively, a coinductive datatype is similar to an inductive datatype but
972 allows infinite objects. Thus, the infinite lists $\textit{ps}$ $=$ $[a, a, a,
973 \ldots]$, $\textit{qs}$ $=$ $[a, b, a, b, \ldots]$, and $\textit{rs}$ $=$ $[0,
974 1, 2, 3, \ldots]$ can be defined as lazy lists using the
975 $\textit{LNil}\mathbin{\Colon}{'}a~\textit{llist}$ and
976 $\textit{LCons}\mathbin{\Colon}{'}a \mathbin{\Rightarrow} {'}a~\textit{llist}
977 \mathbin{\Rightarrow} {'}a~\textit{llist}$ constructors.
979 Although it is otherwise no friend of infinity, Nitpick can find counterexamples
980 involving cyclic lists such as \textit{ps} and \textit{qs} above as well as
984 \textbf{lemma} ``$\textit{xs} \not= \textit{LCons}~a~\textit{xs}$'' \\
985 \textbf{nitpick} \\[2\smallskipamount]
986 \slshape Nitpick found a counterexample for {\itshape card}~$'a$ = 1: \\[2\smallskipamount]
987 \hbox{}\qquad Free variables: \nopagebreak \\
988 \hbox{}\qquad\qquad $\textit{a} = a_1$ \\
989 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$
992 The notation $\textrm{THE}~\omega.\; \omega = t(\omega)$ stands
993 for the infinite term $t(t(t(\ldots)))$. Hence, \textit{xs} is simply the
994 infinite list $[a_1, a_1, a_1, \ldots]$.
996 The next example is more interesting:
999 \textbf{lemma}~``$\lbrakk\textit{xs} = \textit{LCons}~a~\textit{xs};\>\,
1000 \textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
1001 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
1002 \slshape The type ``\kern1pt$'a$'' passed the monotonicity test. Nitpick might be able to skip
1003 some scopes. \\[2\smallskipamount]
1004 Trying 10 scopes: \\
1005 \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 1,
1006 and \textit{bisim\_depth}~= 0. \\
1007 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1008 \hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 10,
1009 and \textit{bisim\_depth}~= 9. \\[2\smallskipamount]
1010 Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
1011 \textit{card}~``\kern1pt$'a~\textit{list\/}$''~= 2, and \textit{bisim\_\allowbreak
1013 \\[2\smallskipamount]
1014 \hbox{}\qquad Free variables: \nopagebreak \\
1015 \hbox{}\qquad\qquad $\textit{a} = a_1$ \\
1016 \hbox{}\qquad\qquad $\textit{b} = a_2$ \\
1017 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
1018 \hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount]
1022 The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas
1023 $\textit{ys}$ is $[a_2, a_1, a_1, a_1, \ldots]$, i.e., a lasso-shaped list with
1024 $[a_2]$ as its stem and $[a_1]$ as its cycle. In general, the list segment
1025 within the scope of the {THE} binder corresponds to the lasso's cycle, whereas
1026 the segment leading to the binder is the stem.
1028 A salient property of coinductive datatypes is that two objects are considered
1029 equal if and only if they lead to the same observations. For example, the lazy
1030 lists $\textrm{THE}~\omega.\; \omega =
1031 \textit{LCons}~a~(\textit{LCons}~b~\omega)$ and
1032 $\textit{LCons}~a~(\textrm{THE}~\omega.\; \omega =
1033 \textit{LCons}~b~(\textit{LCons}~a~\omega))$ are identical, because both lead
1034 to the sequence of observations $a$, $b$, $a$, $b$, \hbox{\ldots} (or,
1035 equivalently, both encode the infinite list $[a, b, a, b, \ldots]$). This
1036 concept of equality for coinductive datatypes is called bisimulation and is
1037 defined coinductively.
1039 Internally, Nitpick encodes the coinductive bisimilarity predicate as part of
1040 the Kodkod problem to ensure that distinct objects lead to different
1041 observations. This precaution is somewhat expensive and often unnecessary, so it
1042 can be disabled by setting the \textit{bisim\_depth} option to $-1$. The
1043 bisimilarity check is then performed \textsl{after} the counterexample has been
1044 found to ensure correctness. If this after-the-fact check fails, the
1045 counterexample is tagged as ``quasi genuine'' and Nitpick recommends to try
1046 again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the
1047 check for the previous example saves approximately 150~milli\-seconds; the speed
1048 gains can be more significant for larger scopes.
1050 The next formula illustrates the need for bisimilarity (either as a Kodkod
1051 predicate or as an after-the-fact check) to prevent spurious counterexamples:
1054 \textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
1055 \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
1056 \textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
1057 \slshape Nitpick found a quasi genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
1058 \hbox{}\qquad Free variables: \nopagebreak \\
1059 \hbox{}\qquad\qquad $a = a_1$ \\
1060 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
1061 \textit{LCons}~a_1~\omega$ \\
1062 \hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
1063 \hbox{}\qquad Codatatype:\strut \nopagebreak \\
1064 \hbox{}\qquad\qquad $'a~\textit{llist} =
1065 \{\!\begin{aligned}[t]
1066 & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega, \\[-2pt]
1067 & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega,\> \unr\}\end{aligned}$
1068 \\[2\smallskipamount]
1069 Try again with ``\textit{bisim\_depth}'' set to a nonnegative value to confirm
1070 that the counterexample is genuine. \\[2\smallskipamount]
1071 {\upshape\textbf{nitpick}} \\[2\smallskipamount]
1072 \slshape Nitpick found no counterexample.
1075 In the first \textbf{nitpick} invocation, the after-the-fact check discovered
1076 that the two known elements of type $'a~\textit{llist}$ are bisimilar.
1078 A compromise between leaving out the bisimilarity predicate from the Kodkod
1079 problem and performing the after-the-fact check is to specify a lower
1080 nonnegative \textit{bisim\_depth} value than the default one provided by
1081 Nitpick. In general, a value of $K$ means that Nitpick will require all lists to
1082 be distinguished from each other by their prefixes of length $K$. Be aware that
1083 setting $K$ to a too low value can overconstrain Nitpick, preventing it from
1084 finding any counterexamples.
1089 Nitpick normally maps function and product types directly to the corresponding
1090 Kodkod concepts. As a consequence, if $'a$ has cardinality 3 and $'b$ has
1091 cardinality 4, then $'a \times {'}b$ has cardinality 12 ($= 4 \times 3$) and $'a
1092 \Rightarrow {'}b$ has cardinality 64 ($= 4^3$). In some circumstances, it pays
1093 off to treat these types in the same way as plain datatypes, by approximating
1094 them by a subset of a given cardinality. This technique is called ``boxing'' and
1095 is particularly useful for functions passed as arguments to other functions, for
1096 high-arity functions, and for large tuples. Under the hood, boxing involves
1097 wrapping occurrences of the types $'a \times {'}b$ and $'a \Rightarrow {'}b$ in
1098 isomorphic datatypes, as can be seen by enabling the \textit{debug} option.
1100 To illustrate boxing, we consider a formalization of $\lambda$-terms represented
1101 using de Bruijn's notation:
1104 \textbf{datatype} \textit{tm} = \textit{Var}~\textit{nat}~$\mid$~\textit{Lam}~\textit{tm} $\mid$ \textit{App~tm~tm}
1107 The $\textit{lift}~t~k$ function increments all variables with indices greater
1108 than or equal to $k$ by one:
1111 \textbf{primrec} \textit{lift} \textbf{where} \\
1112 ``$\textit{lift}~(\textit{Var}~j)~k = \textit{Var}~(\textrm{if}~j < k~\textrm{then}~j~\textrm{else}~j + 1)$'' $\mid$ \\
1113 ``$\textit{lift}~(\textit{Lam}~t)~k = \textit{Lam}~(\textit{lift}~t~(k + 1))$'' $\mid$ \\
1114 ``$\textit{lift}~(\textit{App}~t~u)~k = \textit{App}~(\textit{lift}~t~k)~(\textit{lift}~u~k)$''
1117 The $\textit{loose}~t~k$ predicate returns \textit{True} if and only if
1118 term $t$ has a loose variable with index $k$ or more:
1121 \textbf{primrec}~\textit{loose} \textbf{where} \\
1122 ``$\textit{loose}~(\textit{Var}~j)~k = (j \ge k)$'' $\mid$ \\
1123 ``$\textit{loose}~(\textit{Lam}~t)~k = \textit{loose}~t~(\textit{Suc}~k)$'' $\mid$ \\
1124 ``$\textit{loose}~(\textit{App}~t~u)~k = (\textit{loose}~t~k \mathrel{\lor} \textit{loose}~u~k)$''
1127 Next, the $\textit{subst}~\sigma~t$ function applies the substitution $\sigma$
1131 \textbf{primrec}~\textit{subst} \textbf{where} \\
1132 ``$\textit{subst}~\sigma~(\textit{Var}~j) = \sigma~j$'' $\mid$ \\
1133 ``$\textit{subst}~\sigma~(\textit{Lam}~t) = {}$\phantom{''} \\
1134 \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$ \\
1135 ``$\textit{subst}~\sigma~(\textit{App}~t~u) = \textit{App}~(\textit{subst}~\sigma~t)~(\textit{subst}~\sigma~u)$''
1138 A substitution is a function that maps variable indices to terms. Observe that
1139 $\sigma$ is a function passed as argument and that Nitpick can't optimize it
1140 away, because the recursive call for the \textit{Lam} case involves an altered
1141 version. Also notice the \textit{lift} call, which increments the variable
1142 indices when moving under a \textit{Lam}.
1144 A reasonable property to expect of substitution is that it should leave closed
1145 terms unchanged. Alas, even this simple property does not hold:
1148 \textbf{lemma}~``$\lnot\,\textit{loose}~t~0 \,\Longrightarrow\, \textit{subst}~\sigma~t = t$'' \\
1149 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
1151 Trying 10 scopes: \nopagebreak \\
1152 \hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 1; \\
1153 \hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 2; \\
1154 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1155 \hbox{}\qquad \textit{card~nat}~= 10, \textit{card tm}~= 10, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 10. \\[2\smallskipamount]
1156 Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6,
1157 and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm}$''~= 6: \\[2\smallskipamount]
1158 \hbox{}\qquad Free variables: \nopagebreak \\
1159 \hbox{}\qquad\qquad $\sigma = \undef(\!\begin{aligned}[t]
1160 & 0 := \textit{Var}~0,\>
1161 1 := \textit{Var}~0,\>
1162 2 := \textit{Var}~0, \\[-2pt]
1163 & 3 := \textit{Var}~0,\>
1164 4 := \textit{Var}~0,\>
1165 5 := \textit{Var}~0)\end{aligned}$ \\
1166 \hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount]
1170 Using \textit{eval}, we find out that $\textit{subst}~\sigma~t =
1171 \textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional
1172 $\lambda$-term notation, $t$~is
1173 $\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is $\lambda x\, y.\> y$.
1174 The bug is in \textit{subst\/}: The $\textit{lift}~(\sigma~m)~1$ call should be
1175 replaced with $\textit{lift}~(\sigma~m)~0$.
1177 An interesting aspect of Nitpick's verbose output is that it assigned inceasing
1178 cardinalities from 1 to 10 to the type $\textit{nat} \Rightarrow \textit{tm}$.
1179 For the formula of interest, knowing 6 values of that type was enough to find
1180 the counterexample. Without boxing, $46\,656$ ($= 6^6$) values must be
1181 considered, a hopeless undertaking:
1184 \textbf{nitpick} [\textit{dont\_box}] \\[2\smallskipamount]
1185 {\slshape Nitpick ran out of time after checking 3 of 10 scopes.}
1189 Boxing can be enabled or disabled globally or on a per-type basis using the
1190 \textit{box} option. Nitpick usually performs reasonable choices about which
1191 types should be boxed, but option tweaking sometimes helps. A related optimization,
1192 ``finalization,'' attempts to wrap functions that constant at all but finitely
1193 many points (e.g., finite sets); see the documentation for the \textit{finalize}
1194 option in \S\ref{scope-of-search} for details.
1198 \subsection{Scope Monotonicity}
1199 \label{scope-monotonicity}
1201 The \textit{card} option (together with \textit{iter}, \textit{bisim\_depth},
1202 and \textit{max}) controls which scopes are actually tested. In general, to
1203 exhaust all models below a certain cardinality bound, the number of scopes that
1204 Nitpick must consider increases exponentially with the number of type variables
1205 (and \textbf{typedecl}'d types) occurring in the formula. Given the default
1206 cardinality specification of 1--10, no fewer than $10^4 = 10\,000$ scopes must be
1207 considered for a formula involving $'a$, $'b$, $'c$, and $'d$.
1209 Fortunately, many formulas exhibit a property called \textsl{scope
1210 monotonicity}, meaning that if the formula is falsifiable for a given scope,
1211 it is also falsifiable for all larger scopes \cite[p.~165]{jackson-2006}.
1213 Consider the formula
1216 \textbf{lemma}~``$\textit{length~xs} = \textit{length~ys} \,\Longrightarrow\, \textit{rev}~(\textit{zip~xs~ys}) = \textit{zip~xs}~(\textit{rev~ys})$''
1219 where \textit{xs} is of type $'a~\textit{list}$ and \textit{ys} is of type
1220 $'b~\textit{list}$. A priori, Nitpick would need to consider $1\,000$ scopes to
1221 exhaust the specification \textit{card}~= 1--10 (10 cardinalies for $'a$
1222 $\times$ 10 cardinalities for $'b$ $\times$ 10 cardinalities for the datatypes).
1223 However, our intuition tells us that any counterexample found with a small scope
1224 would still be a counterexample in a larger scope---by simply ignoring the fresh
1225 $'a$ and $'b$ values provided by the larger scope. Nitpick comes to the same
1226 conclusion after a careful inspection of the formula and the relevant
1230 \textbf{nitpick}~[\textit{verbose}] \\[2\smallskipamount]
1232 The types ``\kern1pt$'a$'' and ``\kern1pt$'b$'' passed the monotonicity test.
1233 Nitpick might be able to skip some scopes.
1234 \\[2\smallskipamount]
1235 Trying 10 scopes: \\
1236 \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1,
1237 \textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$
1238 \textit{list\/}''~= 1, \\
1239 \hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 1, and
1240 \textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 1. \\
1241 \hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2,
1242 \textit{card} \textit{nat}~= 2, \textit{card} ``$('a \times {'}b)$
1243 \textit{list\/}''~= 2, \\
1244 \hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 2, and
1245 \textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 2. \\
1246 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1247 \hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} $'b$~= 10,
1248 \textit{card} \textit{nat}~= 10, \textit{card} ``$('a \times {'}b)$
1249 \textit{list\/}''~= 10, \\
1250 \hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 10, and
1251 \textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 10.
1252 \\[2\smallskipamount]
1253 Nitpick found a counterexample for
1254 \textit{card} $'a$~= 5, \textit{card} $'b$~= 5,
1255 \textit{card} \textit{nat}~= 5, \textit{card} ``$('a \times {'}b)$
1256 \textit{list\/}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 5, and
1257 \textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 5:
1258 \\[2\smallskipamount]
1259 \hbox{}\qquad Free variables: \nopagebreak \\
1260 \hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\
1261 \hbox{}\qquad\qquad $\textit{ys} = [b_1, b_1]$ \\[2\smallskipamount]
1265 In theory, it should be sufficient to test a single scope:
1268 \textbf{nitpick}~[\textit{card}~= 10]
1271 However, this is often less efficient in practice and may lead to overly complex
1274 If the monotonicity check fails but we believe that the formula is monotonic (or
1275 we don't mind missing some counterexamples), we can pass the
1276 \textit{mono} option. To convince yourself that this option is risky,
1277 simply consider this example from \S\ref{skolemization}:
1280 \textbf{lemma} ``$\exists g.\; \forall x\Colon 'b.~g~(f~x) = x
1281 \,\Longrightarrow\, \forall y\Colon {'}a.\; \exists x.~y = f~x$'' \\
1282 \textbf{nitpick} [\textit{mono}] \\[2\smallskipamount]
1283 {\slshape Nitpick found no counterexample.} \\[2\smallskipamount]
1284 \textbf{nitpick} \\[2\smallskipamount]
1286 Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\
1287 \hbox{}\qquad $\vdots$
1290 (It turns out the formula holds if and only if $\textit{card}~'a \le
1291 \textit{card}~'b$.) Although this is rarely advisable, the automatic
1292 monotonicity checks can be disabled by passing \textit{non\_mono}
1293 (\S\ref{optimizations}).
1295 As insinuated in \S\ref{natural-numbers-and-integers} and
1296 \S\ref{inductive-datatypes}, \textit{nat}, \textit{int}, and inductive datatypes
1297 are normally monotonic and treated as such. The same is true for record types,
1298 \textit{rat}, and \textit{real}. Thus, given the
1299 cardinality specification 1--10, a formula involving \textit{nat}, \textit{int},
1300 \textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
1301 consider only 10~scopes instead of $10\,000$. On the other hand,
1302 \textbf{typedef}s and quotient types are generally nonmonotonic.
1304 \subsection{Inductive Properties}
1305 \label{inductive-properties}
1307 Inductive properties are a particular pain to prove, because the failure to
1308 establish an induction step can mean several things:
1311 \item The property is invalid.
1312 \item The property is valid but is too weak to support the induction step.
1313 \item The property is valid and strong enough; it's just that we haven't found
1317 Depending on which scenario applies, we would take the appropriate course of
1321 \item Repair the statement of the property so that it becomes valid.
1322 \item Generalize the property and/or prove auxiliary properties.
1323 \item Work harder on a proof.
1326 How can we distinguish between the three scenarios? Nitpick's normal mode of
1327 operation can often detect scenario 1, and Isabelle's automatic tactics help with
1328 scenario 3. Using appropriate techniques, it is also often possible to use
1329 Nitpick to identify scenario 2. Consider the following transition system,
1330 in which natural numbers represent states:
1333 \textbf{inductive\_set}~\textit{reach}~\textbf{where} \\
1334 ``$(4\Colon\textit{nat}) \in \textit{reach\/}$'' $\mid$ \\
1335 ``$\lbrakk n < 4;\> n \in \textit{reach\/}\rbrakk \,\Longrightarrow\, 3 * n + 1 \in \textit{reach\/}$'' $\mid$ \\
1336 ``$n \in \textit{reach} \,\Longrightarrow n + 2 \in \textit{reach\/}$''
1339 We will try to prove that only even numbers are reachable:
1342 \textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n$''
1345 Does this property hold? Nitpick cannot find a counterexample within 30 seconds,
1346 so let's attempt a proof by induction:
1349 \textbf{apply}~(\textit{induct~set}{:}~\textit{reach\/}) \\
1350 \textbf{apply}~\textit{auto}
1353 This leaves us in the following proof state:
1356 {\slshape goal (2 subgoals): \\
1357 \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)$ \\
1358 \phantom{0}2. ${\bigwedge}n.\;\, \lbrakk n \in \textit{reach\/};\, 2~\textsl{dvd}~n\rbrakk \,\Longrightarrow\, 2~\textsl{dvd}~\textit{Suc}~(\textit{Suc}~n)$
1362 If we run Nitpick on the first subgoal, it still won't find any
1363 counterexample; and yet, \textit{auto} fails to go further, and \textit{arith}
1364 is helpless. However, notice the $n \in \textit{reach}$ assumption, which
1365 strengthens the induction hypothesis but is not immediately usable in the proof.
1366 If we remove it and invoke Nitpick, this time we get a counterexample:
1369 \textbf{apply}~(\textit{thin\_tac}~``$n \in \textit{reach\/}$'') \\
1370 \textbf{nitpick} \\[2\smallskipamount]
1371 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1372 \hbox{}\qquad Skolem constant: \nopagebreak \\
1373 \hbox{}\qquad\qquad $n = 0$
1376 Indeed, 0 < 4, 2 divides 0, but 2 does not divide 1. We can use this information
1377 to strength the lemma:
1380 \textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \not= 0$''
1383 Unfortunately, the proof by induction still gets stuck, except that Nitpick now
1384 finds the counterexample $n = 2$. We generalize the lemma further to
1387 \textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \ge 4$''
1390 and this time \textit{arith} can finish off the subgoals.
1392 A similar technique can be employed for structural induction. The
1393 following mini formalization of full binary trees will serve as illustration:
1396 \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]
1397 \textbf{primrec}~\textit{labels}~\textbf{where} \\
1398 ``$\textit{labels}~(\textit{Leaf}~a) = \{a\}$'' $\mid$ \\
1399 ``$\textit{labels}~(\textit{Branch}~t~u) = \textit{labels}~t \mathrel{\cup} \textit{labels}~u$'' \\[2\smallskipamount]
1400 \textbf{primrec}~\textit{swap}~\textbf{where} \\
1401 ``$\textit{swap}~(\textit{Leaf}~c)~a~b =$ \\
1402 \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$ \\
1403 ``$\textit{swap}~(\textit{Branch}~t~u)~a~b = \textit{Branch}~(\textit{swap}~t~a~b)~(\textit{swap}~u~a~b)$''
1406 The \textit{labels} function returns the set of labels occurring on leaves of a
1407 tree, and \textit{swap} exchanges two labels. Intuitively, if two distinct
1408 labels $a$ and $b$ occur in a tree $t$, they should also occur in the tree
1409 obtained by swapping $a$ and $b$:
1412 \textbf{lemma} $``\{a, b\} \subseteq \textit{labels}~t \,\Longrightarrow\, \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
1415 Nitpick can't find any counterexample, so we proceed with induction
1416 (this time favoring a more structured style):
1419 \textbf{proof}~(\textit{induct}~$t$) \\
1420 \hbox{}\quad \textbf{case}~\textit{Leaf}~\textbf{thus}~\textit{?case}~\textbf{by}~\textit{simp} \\
1422 \hbox{}\quad \textbf{case}~$(\textit{Branch}~t~u)$~\textbf{thus} \textit{?case}
1425 Nitpick can't find any counterexample at this point either, but it makes the
1426 following suggestion:
1430 Hint: To check that the induction hypothesis is general enough, try this command:
1431 \textbf{nitpick}~[\textit{non\_std}, \textit{show\_all}].
1434 If we follow the hint, we get a ``nonstandard'' counterexample for the step:
1437 \slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 3: \\[2\smallskipamount]
1438 \hbox{}\qquad Free variables: \nopagebreak \\
1439 \hbox{}\qquad\qquad $a = a_1$ \\
1440 \hbox{}\qquad\qquad $b = a_2$ \\
1441 \hbox{}\qquad\qquad $t = \xi_1$ \\
1442 \hbox{}\qquad\qquad $u = \xi_2$ \\
1443 \hbox{}\qquad Datatype: \nopagebreak \\
1444 \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\}$ \\
1445 \hbox{}\qquad {\slshape Constants:} \nopagebreak \\
1446 \hbox{}\qquad\qquad $\textit{labels} = \undef
1447 (\!\begin{aligned}[t]%
1448 & \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[-2pt]
1449 & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\
1450 \hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
1451 (\!\begin{aligned}[t]%
1452 & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
1453 & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
1454 The existence of a nonstandard model suggests that the induction hypothesis is not general enough or may even
1455 be wrong. See the Nitpick manual's ``Inductive Properties'' section for details (``\textit{isabelle doc nitpick}'').
1458 Reading the Nitpick manual is a most excellent idea.
1459 But what's going on? The \textit{non\_std} option told the tool to look for
1460 nonstandard models of binary trees, which means that new ``nonstandard'' trees
1461 $\xi_1, \xi_2, \ldots$, are now allowed in addition to the standard trees
1462 generated by the \textit{Leaf} and \textit{Branch} constructors.%
1463 \footnote{Notice the similarity between allowing nonstandard trees here and
1464 allowing unreachable states in the preceding example (by removing the ``$n \in
1465 \textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
1466 set of objects over which the induction is performed while doing the step
1467 in order to test the induction hypothesis's strength.}
1468 Unlike standard trees, these new trees contain cycles. We will see later that
1469 every property of acyclic trees that can be proved without using induction also
1470 holds for cyclic trees. Hence,
1473 \textsl{If the induction
1474 hypothesis is strong enough, the induction step will hold even for nonstandard
1475 objects, and Nitpick won't find any nonstandard counterexample.}
1478 But here the tool find some nonstandard trees $t = \xi_1$
1479 and $u = \xi_2$ such that $a \notin \textit{labels}~t$, $b \in
1480 \textit{labels}~t$, $a \in \textit{labels}~u$, and $b \notin \textit{labels}~u$.
1481 Because neither tree contains both $a$ and $b$, the induction hypothesis tells
1482 us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
1483 and as a result we know nothing about the labels of the tree
1484 $\textit{swap}~(\textit{Branch}~t~u)~a~b$, which by definition equals
1485 $\textit{Branch}$ $(\textit{swap}~t~a~b)$ $(\textit{swap}~u~a~b)$, whose
1486 labels are $\textit{labels}$ $(\textit{swap}~t~a~b) \mathrel{\cup}
1487 \textit{labels}$ $(\textit{swap}~u~a~b)$.
1489 The solution is to ensure that we always know what the labels of the subtrees
1490 are in the inductive step, by covering the cases where $a$ and/or~$b$ is not in
1491 $t$ in the statement of the lemma:
1494 \textbf{lemma} ``$\textit{labels}~(\textit{swap}~t~a~b) = {}$ \\
1495 \phantom{\textbf{lemma} ``}$(\textrm{if}~a \in \textit{labels}~t~\textrm{then}$ \nopagebreak \\
1496 \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\}$ \\
1497 \phantom{\textbf{lemma} ``(}$\textrm{else}$ \\
1498 \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)$''
1501 This time, Nitpick won't find any nonstandard counterexample, and we can perform
1502 the induction step using \textit{auto}.
1504 \section{Case Studies}
1505 \label{case-studies}
1507 As a didactic device, the previous section focused mostly on toy formulas whose
1508 validity can easily be assessed just by looking at the formula. We will now
1509 review two somewhat more realistic case studies that are within Nitpick's
1510 reach:\ a context-free grammar modeled by mutually inductive sets and a
1511 functional implementation of AA trees. The results presented in this
1512 section were produced with the following settings:
1515 \textbf{nitpick\_params} [\textit{max\_potential}~= 0]
1518 \subsection{A Context-Free Grammar}
1519 \label{a-context-free-grammar}
1521 Our first case study is taken from section 7.4 in the Isabelle tutorial
1522 \cite{isa-tutorial}. The following grammar, originally due to Hopcroft and
1523 Ullman, produces all strings with an equal number of $a$'s and $b$'s:
1526 \begin{tabular}{@{}r@{$\;\,$}c@{$\;\,$}l@{}}
1527 $S$ & $::=$ & $\epsilon \mid bA \mid aB$ \\
1528 $A$ & $::=$ & $aS \mid bAA$ \\
1529 $B$ & $::=$ & $bS \mid aBB$
1533 The intuition behind the grammar is that $A$ generates all string with one more
1534 $a$ than $b$'s and $B$ generates all strings with one more $b$ than $a$'s.
1536 The alphabet consists exclusively of $a$'s and $b$'s:
1539 \textbf{datatype} \textit{alphabet}~= $a$ $\mid$ $b$
1542 Strings over the alphabet are represented by \textit{alphabet list}s.
1543 Nonterminals in the grammar become sets of strings. The production rules
1544 presented above can be expressed as a mutually inductive definition:
1547 \textbf{inductive\_set} $S$ \textbf{and} $A$ \textbf{and} $B$ \textbf{where} \\
1548 \textit{R1}:\kern.4em ``$[] \in S$'' $\,\mid$ \\
1549 \textit{R2}:\kern.4em ``$w \in A\,\Longrightarrow\, b \mathbin{\#} w \in S$'' $\,\mid$ \\
1550 \textit{R3}:\kern.4em ``$w \in B\,\Longrightarrow\, a \mathbin{\#} w \in S$'' $\,\mid$ \\
1551 \textit{R4}:\kern.4em ``$w \in S\,\Longrightarrow\, a \mathbin{\#} w \in A$'' $\,\mid$ \\
1552 \textit{R5}:\kern.4em ``$w \in S\,\Longrightarrow\, b \mathbin{\#} w \in S$'' $\,\mid$ \\
1553 \textit{R6}:\kern.4em ``$\lbrakk v \in B;\> v \in B\rbrakk \,\Longrightarrow\, a \mathbin{\#} v \mathbin{@} w \in B$''
1556 The conversion of the grammar into the inductive definition was done manually by
1557 Joe Blow, an underpaid undergraduate student. As a result, some errors might
1560 Debugging faulty specifications is at the heart of Nitpick's \textsl{raison
1561 d'\^etre}. A good approach is to state desirable properties of the specification
1562 (here, that $S$ is exactly the set of strings over $\{a, b\}$ with as many $a$'s
1563 as $b$'s) and check them with Nitpick. If the properties are correctly stated,
1564 counterexamples will point to bugs in the specification. For our grammar
1565 example, we will proceed in two steps, separating the soundness and the
1566 completeness of the set $S$. First, soundness:
1569 \textbf{theorem}~\textit{S\_sound\/}: \\
1570 ``$w \in S \longrightarrow \textit{length}~[x\mathbin{\leftarrow} w.\; x = a] =
1571 \textit{length}~[x\mathbin{\leftarrow} w.\; x = b]$'' \\
1572 \textbf{nitpick} \\[2\smallskipamount]
1573 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1574 \hbox{}\qquad Free variable: \nopagebreak \\
1575 \hbox{}\qquad\qquad $w = [b]$
1578 It would seem that $[b] \in S$. How could this be? An inspection of the
1579 introduction rules reveals that the only rule with a right-hand side of the form
1580 $b \mathbin{\#} {\ldots} \in S$ that could have introduced $[b]$ into $S$ is
1584 ``$w \in S\,\Longrightarrow\, b \mathbin{\#} w \in S$''
1587 On closer inspection, we can see that this rule is wrong. To match the
1588 production $B ::= bS$, the second $S$ should be a $B$. We fix the typo and try
1592 \textbf{nitpick} \\[2\smallskipamount]
1593 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1594 \hbox{}\qquad Free variable: \nopagebreak \\
1595 \hbox{}\qquad\qquad $w = [a, a, b]$
1598 Some detective work is necessary to find out what went wrong here. To get $[a,
1599 a, b] \in S$, we need $[a, b] \in B$ by \textit{R3}, which in turn can only come
1603 ``$\lbrakk v \in B;\> v \in B\rbrakk \,\Longrightarrow\, a \mathbin{\#} v \mathbin{@} w \in B$''
1606 Now, this formula must be wrong: The same assumption occurs twice, and the
1607 variable $w$ is unconstrained. Clearly, one of the two occurrences of $v$ in
1608 the assumptions should have been a $w$.
1610 With the correction made, we don't get any counterexample from Nitpick. Let's
1611 move on and check completeness:
1614 \textbf{theorem}~\textit{S\_complete}: \\
1615 ``$\textit{length}~[x\mathbin{\leftarrow} w.\; x = a] =
1616 \textit{length}~[x\mathbin{\leftarrow} w.\; x = b]
1617 \longrightarrow w \in S$'' \\
1618 \textbf{nitpick} \\[2\smallskipamount]
1619 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1620 \hbox{}\qquad Free variable: \nopagebreak \\
1621 \hbox{}\qquad\qquad $w = [b, b, a, a]$
1624 Apparently, $[b, b, a, a] \notin S$, even though it has the same numbers of
1625 $a$'s and $b$'s. But since our inductive definition passed the soundness check,
1626 the introduction rules we have are probably correct. Perhaps we simply lack an
1627 introduction rule. Comparing the grammar with the inductive definition, our
1628 suspicion is confirmed: Joe Blow simply forgot the production $A ::= bAA$,
1629 without which the grammar cannot generate two or more $b$'s in a row. So we add
1633 ``$\lbrakk v \in A;\> w \in A\rbrakk \,\Longrightarrow\, b \mathbin{\#} v \mathbin{@} w \in A$''
1636 With this last change, we don't get any counterexamples from Nitpick for either
1637 soundness or completeness. We can even generalize our result to cover $A$ and
1641 \textbf{theorem} \textit{S\_A\_B\_sound\_and\_complete}: \\
1642 ``$w \in S \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b]$'' \\
1643 ``$w \in A \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] + 1$'' \\
1644 ``$w \in B \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] + 1$'' \\
1645 \textbf{nitpick} \\[2\smallskipamount]
1646 \slshape Nitpick found no counterexample.
1649 \subsection{AA Trees}
1652 AA trees are a kind of balanced trees discovered by Arne Andersson that provide
1653 similar performance to red-black trees, but with a simpler implementation
1654 \cite{andersson-1993}. They can be used to store sets of elements equipped with
1655 a total order $<$. We start by defining the datatype and some basic extractor
1659 \textbf{datatype} $'a$~\textit{aa\_tree} = \\
1660 \hbox{}\quad $\Lambda$ $\mid$ $N$ ``\kern1pt$'a\Colon \textit{linorder}$'' \textit{nat} ``\kern1pt$'a$ \textit{aa\_tree}'' ``\kern1pt$'a$ \textit{aa\_tree}'' \\[2\smallskipamount]
1661 \textbf{primrec} \textit{data} \textbf{where} \\
1662 ``$\textit{data}~\Lambda = \undef$'' $\,\mid$ \\
1663 ``$\textit{data}~(N~x~\_~\_~\_) = x$'' \\[2\smallskipamount]
1664 \textbf{primrec} \textit{dataset} \textbf{where} \\
1665 ``$\textit{dataset}~\Lambda = \{\}$'' $\,\mid$ \\
1666 ``$\textit{dataset}~(N~x~\_~t~u) = \{x\} \cup \textit{dataset}~t \mathrel{\cup} \textit{dataset}~u$'' \\[2\smallskipamount]
1667 \textbf{primrec} \textit{level} \textbf{where} \\
1668 ``$\textit{level}~\Lambda = 0$'' $\,\mid$ \\
1669 ``$\textit{level}~(N~\_~k~\_~\_) = k$'' \\[2\smallskipamount]
1670 \textbf{primrec} \textit{left} \textbf{where} \\
1671 ``$\textit{left}~\Lambda = \Lambda$'' $\,\mid$ \\
1672 ``$\textit{left}~(N~\_~\_~t~\_) = t$'' \\[2\smallskipamount]
1673 \textbf{primrec} \textit{right} \textbf{where} \\
1674 ``$\textit{right}~\Lambda = \Lambda$'' $\,\mid$ \\
1675 ``$\textit{right}~(N~\_~\_~\_~u) = u$''
1678 The wellformedness criterion for AA trees is fairly complex. Wikipedia states it
1679 as follows \cite{wikipedia-2009-aa-trees}:
1681 \kern.2\parskip %% TYPESETTING
1684 Each node has a level field, and the following invariants must remain true for
1685 the tree to be valid:
1689 \kern-.4\parskip %% TYPESETTING
1694 \item[1.] The level of a leaf node is one.
1695 \item[2.] The level of a left child is strictly less than that of its parent.
1696 \item[3.] The level of a right child is less than or equal to that of its parent.
1697 \item[4.] The level of a right grandchild is strictly less than that of its grandparent.
1698 \item[5.] Every node of level greater than one must have two children.
1703 \kern.4\parskip %% TYPESETTING
1705 The \textit{wf} predicate formalizes this description:
1708 \textbf{primrec} \textit{wf} \textbf{where} \\
1709 ``$\textit{wf}~\Lambda = \textit{True}$'' $\,\mid$ \\
1710 ``$\textit{wf}~(N~\_~k~t~u) =$ \\
1711 \phantom{``}$(\textrm{if}~t = \Lambda~\textrm{then}$ \\
1712 \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))$ \\
1713 \phantom{``$($}$\textrm{else}$ \\
1714 \hbox{}\phantom{``$(\quad$}$\textit{wf}~t \mathrel{\land} \textit{wf}~u
1715 \mathrel{\land} u \not= \Lambda \mathrel{\land} \textit{level}~t < k
1716 \mathrel{\land} \textit{level}~u \le k$ \\
1717 \hbox{}\phantom{``$(\quad$}${\land}\; \textit{level}~(\textit{right}~u) < k)$''
1720 Rebalancing the tree upon insertion and removal of elements is performed by two
1721 auxiliary functions called \textit{skew} and \textit{split}, defined below:
1724 \textbf{primrec} \textit{skew} \textbf{where} \\
1725 ``$\textit{skew}~\Lambda = \Lambda$'' $\,\mid$ \\
1726 ``$\textit{skew}~(N~x~k~t~u) = {}$ \\
1727 \phantom{``}$(\textrm{if}~t \not= \Lambda \mathrel{\land} k =
1728 \textit{level}~t~\textrm{then}$ \\
1729 \phantom{``(\quad}$N~(\textit{data}~t)~k~(\textit{left}~t)~(N~x~k~
1730 (\textit{right}~t)~u)$ \\
1731 \phantom{``(}$\textrm{else}$ \\
1732 \phantom{``(\quad}$N~x~k~t~u)$''
1736 \textbf{primrec} \textit{split} \textbf{where} \\
1737 ``$\textit{split}~\Lambda = \Lambda$'' $\,\mid$ \\
1738 ``$\textit{split}~(N~x~k~t~u) = {}$ \\
1739 \phantom{``}$(\textrm{if}~u \not= \Lambda \mathrel{\land} k =
1740 \textit{level}~(\textit{right}~u)~\textrm{then}$ \\
1741 \phantom{``(\quad}$N~(\textit{data}~u)~(\textit{Suc}~k)~
1742 (N~x~k~t~(\textit{left}~u))~(\textit{right}~u)$ \\
1743 \phantom{``(}$\textrm{else}$ \\
1744 \phantom{``(\quad}$N~x~k~t~u)$''
1747 Performing a \textit{skew} or a \textit{split} should have no impact on the set
1748 of elements stored in the tree:
1751 \textbf{theorem}~\textit{dataset\_skew\_split\/}:\\
1752 ``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
1753 ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
1754 \textbf{nitpick} \\[2\smallskipamount]
1755 {\slshape Nitpick ran out of time after checking 9 of 10 scopes.}
1758 Furthermore, applying \textit{skew} or \textit{split} on a well-formed tree
1759 should not alter the tree:
1762 \textbf{theorem}~\textit{wf\_skew\_split\/}:\\
1763 ``$\textit{wf}~t\,\Longrightarrow\, \textit{skew}~t = t$'' \\
1764 ``$\textit{wf}~t\,\Longrightarrow\, \textit{split}~t = t$'' \\
1765 \textbf{nitpick} \\[2\smallskipamount]
1766 {\slshape Nitpick found no counterexample.}
1769 Insertion is implemented recursively. It preserves the sort order:
1772 \textbf{primrec}~\textit{insort} \textbf{where} \\
1773 ``$\textit{insort}~\Lambda~x = N~x~1~\Lambda~\Lambda$'' $\,\mid$ \\
1774 ``$\textit{insort}~(N~y~k~t~u)~x =$ \\
1775 \phantom{``}$({*}~(\textit{split} \circ \textit{skew})~{*})~(N~y~k~(\textrm{if}~x < y~\textrm{then}~\textit{insort}~t~x~\textrm{else}~t)$ \\
1776 \phantom{``$({*}~(\textit{split} \circ \textit{skew})~{*})~(N~y~k~$}$(\textrm{if}~x > y~\textrm{then}~\textit{insort}~u~x~\textrm{else}~u))$''
1779 Notice that we deliberately commented out the application of \textit{skew} and
1780 \textit{split}. Let's see if this causes any problems:
1783 \textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
1784 \textbf{nitpick} \\[2\smallskipamount]
1785 \slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
1786 \hbox{}\qquad Free variables: \nopagebreak \\
1787 \hbox{}\qquad\qquad $t = N~a_1~1~\Lambda~\Lambda$ \\
1788 \hbox{}\qquad\qquad $x = a_2$
1791 It's hard to see why this is a counterexample. To improve readability, we will
1792 restrict the theorem to \textit{nat}, so that we don't need to look up the value
1793 of the $\textit{op}~{<}$ constant to find out which element is smaller than the
1794 other. In addition, we will tell Nitpick to display the value of
1795 $\textit{insort}~t~x$ using the \textit{eval} option. This gives
1798 \textbf{theorem} \textit{wf\_insort\_nat\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\
1799 \textbf{nitpick} [\textit{eval} = ``$\textit{insort}~t~x$''] \\[2\smallskipamount]
1800 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1801 \hbox{}\qquad Free variables: \nopagebreak \\
1802 \hbox{}\qquad\qquad $t = N~1~1~\Lambda~\Lambda$ \\
1803 \hbox{}\qquad\qquad $x = 0$ \\
1804 \hbox{}\qquad Evaluated term: \\
1805 \hbox{}\qquad\qquad $\textit{insort}~t~x = N~1~1~(N~0~1~\Lambda~\Lambda)~\Lambda$
1808 Nitpick's output reveals that the element $0$ was added as a left child of $1$,
1809 where both nodes have a level of 1. This violates the second AA tree invariant,
1810 which states that a left child's level must be less than its parent's. This
1811 shouldn't come as a surprise, considering that we commented out the tree
1812 rebalancing code. Reintroducing the code seems to solve the problem:
1815 \textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
1816 \textbf{nitpick} \\[2\smallskipamount]
1817 {\slshape Nitpick ran out of time after checking 8 of 10 scopes.}
1820 Insertion should transform the set of elements represented by the tree in the
1824 \textbf{theorem} \textit{dataset\_insort\/}:\kern.4em
1825 ``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
1826 \textbf{nitpick} \\[2\smallskipamount]
1827 {\slshape Nitpick ran out of time after checking 7 of 10 scopes.}
1830 We could continue like this and sketch a complete theory of AA trees. Once the
1831 definitions and main theorems are in place and have been thoroughly tested using
1832 Nitpick, we could start working on the proofs. Developing theories this way
1833 usually saves time, because faulty theorems and definitions are discovered much
1834 earlier in the process.
1836 \section{Option Reference}
1837 \label{option-reference}
1842 \def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
1843 \def\qty#1{$\left<\textit{#1}\right>$}
1844 \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
1845 \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1846 \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1847 \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1848 \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
1849 \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]}
1850 \def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
1851 \def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
1852 \def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
1854 Nitpick's behavior can be influenced by various options, which can be specified
1855 in brackets after the \textbf{nitpick} command. Default values can be set
1856 using \textbf{nitpick\_\allowbreak params}. For example:
1859 \textbf{nitpick\_params} [\textit{verbose}, \,\textit{timeout} = 60]
1862 The options are categorized as follows:\ mode of operation
1863 (\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output
1864 format (\S\ref{output-format}), automatic counterexample checks
1865 (\S\ref{authentication}), optimizations
1866 (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
1868 You can instruct Nitpick to run automatically on newly entered theorems by
1869 enabling the ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof
1870 General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}),
1871 \textit{assms} (\S\ref{mode-of-operation}), and \textit{mono}
1872 (\S\ref{scope-of-search}) are implicitly enabled, \textit{blocking}
1873 (\S\ref{mode-of-operation}), \textit{verbose} (\S\ref{output-format}), and
1874 \textit{debug} (\S\ref{output-format}) are disabled, \textit{max\_threads}
1875 (\S\ref{optimizations}) is taken to be 1, \textit{max\_potential}
1876 (\S\ref{output-format}) is taken to be 0, and \textit{timeout}
1877 (\S\ref{timeouts}) is superseded by the ``Auto Tools Time Limit'' in
1878 Proof General's ``Isabelle'' menu. Nitpick's output is also more concise.
1880 The number of options can be overwhelming at first glance. Do not let that worry
1881 you: Nitpick's defaults have been chosen so that it almost always does the right
1882 thing, and the most important options have been covered in context in
1883 \S\ref{first-steps}.
1885 The descriptions below refer to the following syntactic quantities:
1888 \item[$\bullet$] \qtybf{string}: A string.
1889 \item[$\bullet$] \qtybf{string\_list\/}: A space-separated list of strings
1890 (e.g., ``\textit{ichi ni san}'').
1891 \item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
1892 \item[$\bullet$] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or \textit{smart}.
1893 \item[$\bullet$] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
1894 \item[$\bullet$] \qtybf{smart\_int\/}: An integer or \textit{smart}.
1895 \item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
1896 of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<emdash\char`\>}.
1897 \item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
1898 \item[$\bullet$] \qtybf{float\_or\_none}: An integer (e.g., 60) or floating-point number
1899 (e.g., 0.5) expressing a number of seconds, or the keyword \textit{none}
1901 \item[$\bullet$] \qtybf{const\/}: The name of a HOL constant.
1902 \item[$\bullet$] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
1903 \item[$\bullet$] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g.,
1904 ``$f~x$''~``$g~y$'').
1905 \item[$\bullet$] \qtybf{type}: A HOL type.
1908 Default values are indicated in square brackets. Boolean options have a negated
1909 counterpart (e.g., \textit{blocking} vs.\ \textit{non\_blocking}). When setting
1910 Boolean options, ``= \textit{true}'' may be omitted.
1912 \subsection{Mode of Operation}
1913 \label{mode-of-operation}
1916 \optrue{blocking}{non\_blocking}
1917 Specifies whether the \textbf{nitpick} command should operate synchronously.
1918 The asynchronous (non-blocking) mode lets the user start proving the putative
1919 theorem while Nitpick looks for a counterexample, but it can also be more
1920 confusing. For technical reasons, automatic runs currently always block.
1922 \optrue{falsify}{satisfy}
1923 Specifies whether Nitpick should look for falsifying examples (countermodels) or
1924 satisfying examples (models). This manual assumes throughout that
1925 \textit{falsify} is enabled.
1927 \opsmart{user\_axioms}{no\_user\_axioms}
1928 Specifies whether the user-defined axioms (specified using
1929 \textbf{axiomatization} and \textbf{axioms}) should be considered. If the option
1930 is set to \textit{smart}, Nitpick performs an ad hoc axiom selection based on
1931 the constants that occur in the formula to falsify. The option is implicitly set
1932 to \textit{true} for automatic runs.
1934 \textbf{Warning:} If the option is set to \textit{true}, Nitpick might
1935 nonetheless ignore some polymorphic axioms. Counterexamples generated under
1936 these conditions are tagged as ``quasi genuine.'' The \textit{debug}
1937 (\S\ref{output-format}) option can be used to find out which axioms were
1941 {\small See also \textit{assms} (\S\ref{mode-of-operation}) and \textit{debug}
1942 (\S\ref{output-format}).}
1944 \optrue{assms}{no\_assms}
1945 Specifies whether the relevant assumptions in structured proofs should be
1946 considered. The option is implicitly enabled for automatic runs.
1949 {\small See also \textit{user\_axioms} (\S\ref{mode-of-operation}).}
1951 \opfalse{overlord}{no\_overlord}
1952 Specifies whether Nitpick should put its temporary files in
1953 \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
1954 debugging Nitpick but also unsafe if several instances of the tool are run
1955 simultaneously. The files are identified by the extensions
1956 \texttt{.kki}, \texttt{.cnf}, \texttt{.out}, and
1957 \texttt{.err}; you may safely remove them after Nitpick has run.
1960 {\small See also \textit{debug} (\S\ref{output-format}).}
1963 \subsection{Scope of Search}
1964 \label{scope-of-search}
1967 \oparg{card}{type}{int\_seq}
1968 Specifies the sequence of cardinalities to use for a given type.
1969 For free types, and often also for \textbf{typedecl}'d types, it usually makes
1970 sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
1973 {\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
1974 (\S\ref{scope-of-search}).}
1976 \opdefault{card}{int\_seq}{\upshape 1--10}
1977 Specifies the default sequence of cardinalities to use. This can be overridden
1978 on a per-type basis using the \textit{card}~\qty{type} option described above.
1980 \oparg{max}{const}{int\_seq}
1981 Specifies the sequence of maximum multiplicities to use for a given
1982 (co)in\-duc\-tive datatype constructor. A constructor's multiplicity is the
1983 number of distinct values that it can construct. Nonsensical values (e.g.,
1984 \textit{max}~[]~$=$~2) are silently repaired. This option is only available for
1985 datatypes equipped with several constructors.
1987 \opnodefault{max}{int\_seq}
1988 Specifies the default sequence of maximum multiplicities to use for
1989 (co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor
1990 basis using the \textit{max}~\qty{const} option described above.
1992 \opsmart{binary\_ints}{unary\_ints}
1993 Specifies whether natural numbers and integers should be encoded using a unary
1994 or binary notation. In unary mode, the cardinality fully specifies the subset
1995 used to approximate the type. For example:
1997 $$\hbox{\begin{tabular}{@{}rll@{}}%
1998 \textit{card nat} = 4 & induces & $\{0,\, 1,\, 2,\, 3\}$ \\
1999 \textit{card int} = 4 & induces & $\{-1,\, 0,\, +1,\, +2\}$ \\
2000 \textit{card int} = 5 & induces & $\{-2,\, -1,\, 0,\, +1,\, +2\}.$%
2005 $$\hbox{\begin{tabular}{@{}rll@{}}%
2006 \textit{card nat} = $K$ & induces & $\{0,\, \ldots,\, K - 1\}$ \\
2007 \textit{card int} = $K$ & induces & $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor K/2 \rfloor\}.$%
2010 In binary mode, the cardinality specifies the number of distinct values that can
2011 be constructed. Each of these value is represented by a bit pattern whose length
2012 is specified by the \textit{bits} (\S\ref{scope-of-search}) option. By default,
2013 Nitpick attempts to choose the more appropriate encoding by inspecting the
2014 formula at hand, preferring the binary notation for problems involving
2015 multiplicative operators or large constants.
2017 \textbf{Warning:} For technical reasons, Nitpick always reverts to unary for
2018 problems that refer to the types \textit{rat} or \textit{real} or the constants
2019 \textit{Suc}, \textit{gcd}, or \textit{lcm}.
2021 {\small See also \textit{bits} (\S\ref{scope-of-search}) and
2022 \textit{show\_datatypes} (\S\ref{output-format}).}
2024 \opdefault{bits}{int\_seq}{\upshape 1,2,3,4,6,8,10,12,14,16}
2025 Specifies the number of bits to use to represent natural numbers and integers in
2026 binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
2028 {\small See also \textit{binary\_ints} (\S\ref{scope-of-search}).}
2030 \opargboolorsmart{wf}{const}{non\_wf}
2031 Specifies whether the specified (co)in\-duc\-tively defined predicate is
2032 well-founded. The option can take the following values:
2035 \item[$\bullet$] \textbf{\textit{true}:} Tentatively treat the (co)in\-duc\-tive
2036 predicate as if it were well-founded. Since this is generally not sound when the
2037 predicate is not well-founded, the counterexamples are tagged as ``quasi
2040 \item[$\bullet$] \textbf{\textit{false}:} Treat the (co)in\-duc\-tive predicate
2041 as if it were not well-founded. The predicate is then unrolled as prescribed by
2042 the \textit{star\_linear\_preds}, \textit{iter}~\qty{const}, and \textit{iter}
2045 \item[$\bullet$] \textbf{\textit{smart}:} Try to prove that the inductive
2046 predicate is well-founded using Isabelle's \textit{lexicographic\_order} and
2047 \textit{size\_change} tactics. If this succeeds (or the predicate occurs with an
2048 appropriate polarity in the formula to falsify), use an efficient fixed-point
2049 equation as specification of the predicate; otherwise, unroll the predicates
2050 according to the \textit{iter}~\qty{const} and \textit{iter} options.
2054 {\small See also \textit{iter} (\S\ref{scope-of-search}),
2055 \textit{star\_linear\_preds} (\S\ref{optimizations}), and \textit{tac\_timeout}
2056 (\S\ref{timeouts}).}
2058 \opsmart{wf}{non\_wf}
2059 Specifies the default wellfoundedness setting to use. This can be overridden on
2060 a per-predicate basis using the \textit{wf}~\qty{const} option above.
2062 \oparg{iter}{const}{int\_seq}
2063 Specifies the sequence of iteration counts to use when unrolling a given
2064 (co)in\-duc\-tive predicate. By default, unrolling is applied for inductive
2065 predicates that occur negatively and coinductive predicates that occur
2066 positively in the formula to falsify and that cannot be proved to be
2067 well-founded, but this behavior is influenced by the \textit{wf} option. The
2068 iteration counts are automatically bounded by the cardinality of the predicate's
2071 {\small See also \textit{wf} (\S\ref{scope-of-search}) and
2072 \textit{star\_linear\_preds} (\S\ref{optimizations}).}
2074 \opdefault{iter}{int\_seq}{\upshape 0{,}1{,}2{,}4{,}8{,}12{,}16{,}20{,}24{,}28}
2075 Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive
2076 predicates. This can be overridden on a per-predicate basis using the
2077 \textit{iter} \qty{const} option above.
2079 \opdefault{bisim\_depth}{int\_seq}{\upshape 9}
2080 Specifies the sequence of iteration counts to use when unrolling the
2081 bisimilarity predicate generated by Nitpick for coinductive datatypes. A value
2082 of $-1$ means that no predicate is generated, in which case Nitpick performs an
2083 after-the-fact check to see if the known coinductive datatype values are
2084 bidissimilar. If two values are found to be bisimilar, the counterexample is
2085 tagged as ``quasi genuine.'' The iteration counts are automatically bounded by
2086 the sum of the cardinalities of the coinductive datatypes occurring in the
2089 \opargboolorsmart{box}{type}{dont\_box}
2090 Specifies whether Nitpick should attempt to wrap (``box'') a given function or
2091 product type in an isomorphic datatype internally. Boxing is an effective mean
2092 to reduce the search space and speed up Nitpick, because the isomorphic datatype
2093 is approximated by a subset of the possible function or pair values.
2094 Like other drastic optimizations, it can also prevent the discovery of
2095 counterexamples. The option can take the following values:
2098 \item[$\bullet$] \textbf{\textit{true}:} Box the specified type whenever
2100 \item[$\bullet$] \textbf{\textit{false}:} Never box the type.
2101 \item[$\bullet$] \textbf{\textit{smart}:} Box the type only in contexts where it
2102 is likely to help. For example, $n$-tuples where $n > 2$ and arguments to
2103 higher-order functions are good candidates for boxing.
2107 {\small See also \textit{finitize} (\S\ref{scope-of-search}), \textit{verbose}
2108 (\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}).}
2110 \opsmart{box}{dont\_box}
2111 Specifies the default boxing setting to use. This can be overridden on a
2112 per-type basis using the \textit{box}~\qty{type} option described above.
2114 \opargboolorsmart{finitize}{type}{dont\_finitize}
2115 Specifies whether Nitpick should attempt to finitize an infinite datatype. The
2116 option can then take the following values:
2119 \item[$\bullet$] \textbf{\textit{true}:} Finitize the datatype. Since this is
2120 unsound, counterexamples generated under these conditions are tagged as ``quasi
2122 \item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the datatype.
2123 \item[$\bullet$] \textbf{\textit{smart}:}
2124 If the datatype's constructors don't appear in the problem, perform a
2125 monotonicity analysis to detect whether the datatype can be soundly finitized;
2126 otherwise, don't finitize it.
2130 {\small See also \textit{box} (\S\ref{scope-of-search}), \textit{mono}
2131 (\S\ref{scope-of-search}), \textit{verbose} (\S\ref{output-format}), and
2132 \textit{debug} (\S\ref{output-format}).}
2134 \opsmart{finitize}{dont\_finitize}
2135 Specifies the default finitization setting to use. This can be overridden on a
2136 per-type basis using the \textit{finitize}~\qty{type} option described above.
2138 \opargboolorsmart{mono}{type}{non\_mono}
2139 Specifies whether the given type should be considered monotonic when enumerating
2140 scopes and finitizing types. If the option is set to \textit{smart}, Nitpick
2141 performs a monotonicity check on the type. Setting this option to \textit{true}
2142 can reduce the number of scopes tried, but it can also diminish the chance of
2143 finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}. The
2144 option is implicitly set to \textit{true} for automatic runs.
2147 {\small See also \textit{card} (\S\ref{scope-of-search}),
2148 \textit{finitize} (\S\ref{scope-of-search}),
2149 \textit{merge\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
2150 (\S\ref{output-format}).}
2152 \opsmart{mono}{non\_mono}
2153 Specifies the default monotonicity setting to use. This can be overridden on a
2154 per-type basis using the \textit{mono}~\qty{type} option described above.
2156 \opfalse{merge\_type\_vars}{dont\_merge\_type\_vars}
2157 Specifies whether type variables with the same sort constraints should be
2158 merged. Setting this option to \textit{true} can reduce the number of scopes
2159 tried and the size of the generated Kodkod formulas, but it also diminishes the
2160 theoretical chance of finding a counterexample.
2162 {\small See also \textit{mono} (\S\ref{scope-of-search}).}
2164 \opargbool{std}{type}{non\_std}
2165 Specifies whether the given (recursive) datatype should be given standard
2166 models. Nonstandard models are unsound but can help debug structural induction
2167 proofs, as explained in \S\ref{inductive-properties}.
2169 \optrue{std}{non\_std}
2170 Specifies the default standardness to use. This can be overridden on a per-type
2171 basis using the \textit{std}~\qty{type} option described above.
2174 \subsection{Output Format}
2175 \label{output-format}
2178 \opfalse{verbose}{quiet}
2179 Specifies whether the \textbf{nitpick} command should explain what it does. This
2180 option is useful to determine which scopes are tried or which SAT solver is
2181 used. This option is implicitly disabled for automatic runs.
2183 \opfalse{debug}{no\_debug}
2184 Specifies whether Nitpick should display additional debugging information beyond
2185 what \textit{verbose} already displays. Enabling \textit{debug} also enables
2186 \textit{verbose} and \textit{show\_all} behind the scenes. The \textit{debug}
2187 option is implicitly disabled for automatic runs.
2190 {\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
2191 \textit{batch\_size} (\S\ref{optimizations}).}
2193 \opfalse{show\_datatypes}{hide\_datatypes}
2194 Specifies whether the subsets used to approximate (co)in\-duc\-tive data\-types should
2195 be displayed as part of counterexamples. Such subsets are sometimes helpful when
2196 investigating whether a potentially spurious counterexample is genuine, but
2197 their potential for clutter is real.
2199 \optrue{show\_skolems}{hide\_skolem}
2200 Specifies whether the values of Skolem constants should be displayed as part of
2201 counterexamples. Skolem constants correspond to bound variables in the original
2202 formula and usually help us to understand why the counterexample falsifies the
2205 \opfalse{show\_consts}{hide\_consts}
2206 Specifies whether the values of constants occurring in the formula (including
2207 its axioms) should be displayed along with any counterexample. These values are
2208 sometimes helpful when investigating why a counterexample is
2209 genuine, but they can clutter the output.
2211 \opnodefault{show\_all}{bool}
2212 Abbreviation for \textit{show\_datatypes}, \textit{show\_skolems}, and
2213 \textit{show\_consts}.
2215 \opdefault{max\_potential}{int}{\upshape 1}
2216 Specifies the maximum number of potentially spurious counterexamples to display.
2217 Setting this option to 0 speeds up the search for a genuine counterexample. This
2218 option is implicitly set to 0 for automatic runs. If you set this option to a
2219 value greater than 1, you will need an incremental SAT solver, such as
2220 \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that many of
2221 the counterexamples may be identical.
2224 {\small See also \textit{check\_potential} (\S\ref{authentication}) and
2225 \textit{sat\_solver} (\S\ref{optimizations}).}
2227 \opdefault{max\_genuine}{int}{\upshape 1}
2228 Specifies the maximum number of genuine counterexamples to display. If you set
2229 this option to a value greater than 1, you will need an incremental SAT solver,
2230 such as \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that
2231 many of the counterexamples may be identical.
2234 {\small See also \textit{check\_genuine} (\S\ref{authentication}) and
2235 \textit{sat\_solver} (\S\ref{optimizations}).}
2237 \opnodefault{eval}{term\_list}
2238 Specifies the list of terms whose values should be displayed along with
2239 counterexamples. This option suffers from an ``observer effect'': Nitpick might
2240 find different counterexamples for different values of this option.
2242 \oparg{atoms}{type}{string\_list}
2243 Specifies the names to use to refer to the atoms of the given type. By default,
2244 Nitpick generates names of the form $a_1, \ldots, a_n$, where $a$ is the first
2245 letter of the type's name.
2247 \opnodefault{atoms}{string\_list}
2248 Specifies the default names to use to refer to atoms of any type. For example,
2249 to call the three atoms of type ${'}a$ \textit{ichi}, \textit{ni}, and
2250 \textit{san} instead of $a_1$, $a_2$, $a_3$, specify the option
2251 ``\textit{atoms}~${'}a$ = \textit{ichi~ni~san}''. The default names can be
2252 overridden on a per-type basis using the \textit{atoms}~\qty{type} option
2255 \oparg{format}{term}{int\_seq}
2256 Specifies how to uncurry the value displayed for a variable or constant.
2257 Uncurrying sometimes increases the readability of the output for high-arity
2258 functions. For example, given the variable $y \mathbin{\Colon} {'a}\Rightarrow
2259 {'b}\Rightarrow {'c}\Rightarrow {'d}\Rightarrow {'e}\Rightarrow {'f}\Rightarrow
2260 {'g}$, setting \textit{format}~$y$ = 3 tells Nitpick to group the last three
2261 arguments, as if the type had been ${'a}\Rightarrow {'b}\Rightarrow
2262 {'c}\Rightarrow {'d}\times {'e}\times {'f}\Rightarrow {'g}$. In general, a list
2263 of values $n_1,\ldots,n_k$ tells Nitpick to show the last $n_k$ arguments as an
2264 $n_k$-tuple, the previous $n_{k-1}$ arguments as an $n_{k-1}$-tuple, and so on;
2265 arguments that are not accounted for are left alone, as if the specification had
2266 been $1,\ldots,1,n_1,\ldots,n_k$.
2268 \opdefault{format}{int\_seq}{\upshape 1}
2269 Specifies the default format to use. Irrespective of the default format, the
2270 extra arguments to a Skolem constant corresponding to the outer bound variables
2271 are kept separated from the remaining arguments, the \textbf{for} arguments of
2272 an inductive definitions are kept separated from the remaining arguments, and
2273 the iteration counter of an unrolled inductive definition is shown alone. The
2274 default format can be overridden on a per-variable or per-constant basis using
2275 the \textit{format}~\qty{term} option described above.
2278 \subsection{Authentication}
2279 \label{authentication}
2282 \opfalse{check\_potential}{trust\_potential}
2283 Specifies whether potentially spurious counterexamples should be given to
2284 Isabelle's \textit{auto} tactic to assess their validity. If a potentially
2285 spurious counterexample is shown to be genuine, Nitpick displays a message to
2286 this effect and terminates.
2289 {\small See also \textit{max\_potential} (\S\ref{output-format}).}
2291 \opfalse{check\_genuine}{trust\_genuine}
2292 Specifies whether genuine and quasi genuine counterexamples should be given to
2293 Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine''
2294 counterexample is shown to be spurious, the user is kindly asked to send a bug
2295 report to the author at
2296 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@in.tum.de}.
2299 {\small See also \textit{max\_genuine} (\S\ref{output-format}).}
2301 \opnodefault{expect}{string}
2302 Specifies the expected outcome, which must be one of the following:
2305 \item[$\bullet$] \textbf{\textit{genuine}:} Nitpick found a genuine counterexample.
2306 \item[$\bullet$] \textbf{\textit{quasi\_genuine}:} Nitpick found a ``quasi
2307 genuine'' counterexample (i.e., a counterexample that is genuine unless
2308 it contradicts a missing axiom or a dangerous option was used inappropriately).
2309 \item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potentially
2310 spurious counterexample.
2311 \item[$\bullet$] \textbf{\textit{none}:} Nitpick found no counterexample.
2312 \item[$\bullet$] \textbf{\textit{unknown}:} Nitpick encountered some problem (e.g.,
2313 Kodkod ran out of memory).
2316 Nitpick emits an error if the actual outcome differs from the expected outcome.
2317 This option is useful for regression testing.
2320 \subsection{Optimizations}
2321 \label{optimizations}
2323 \def\cpp{C\nobreak\raisebox{.1ex}{+}\nobreak\raisebox{.1ex}{+}}
2328 \opdefault{sat\_solver}{string}{smart}
2329 Specifies which SAT solver to use. SAT solvers implemented in C or \cpp{} tend
2330 to be faster than their Java counterparts, but they can be more difficult to
2331 install. Also, if you set the \textit{max\_potential} (\S\ref{output-format}) or
2332 \textit{max\_genuine} (\S\ref{output-format}) option to a value greater than 1,
2333 you will need an incremental SAT solver, such as \textit{MiniSat\_JNI}
2334 (recommended) or \textit{SAT4J}.
2336 The supported solvers are listed below:
2340 \item[$\bullet$] \textbf{\textit{MiniSat}:} MiniSat is an efficient solver
2341 written in \cpp{}. To use MiniSat, set the environment variable
2342 \texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
2344 \footnote{Important note for Cygwin users: The path must be specified using
2345 native Windows syntax. Make sure to escape backslashes properly.%
2346 \label{cygwin-paths}}
2347 The \cpp{} sources and executables for MiniSat are available at
2348 \url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
2349 and 2.0 beta (2007-07-21).
2351 \item[$\bullet$] \textbf{\textit{MiniSat\_JNI}:} The JNI (Java Native Interface)
2352 version of MiniSat is bundled with Kodkodi and is precompiled for the major
2353 platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
2354 which you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
2355 version of MiniSat, the JNI version can be used incrementally.
2357 \item[$\bullet$] \textbf{\textit{CryptoMiniSat}:} CryptoMiniSat is the winner of
2358 the 2010 SAT Race. To use CryptoMiniSat, set the environment variable
2359 \texttt{CRYPTO\-MINISAT\_}\discretionary{}{}{}\texttt{HOME} to the directory that contains the \texttt{crypto\-minisat}
2361 \footref{cygwin-paths}
2362 The \cpp{} sources and executables for Crypto\-Mini\-Sat are available at
2363 \url{http://planete.inrialpes.fr/~soos/}\allowbreak\url{CryptoMiniSat2/index.php}.
2364 Nitpick has been tested with version 2.51.
2366 \item[$\bullet$] \textbf{\textit{PicoSAT}:} PicoSAT is an efficient solver
2367 written in C. You can install a standard version of
2368 PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
2369 that contains the \texttt{picosat} executable.%
2370 \footref{cygwin-paths}
2371 The C sources for PicoSAT are
2372 available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
2373 Nitpick has been tested with version 913.
2375 \item[$\bullet$] \textbf{\textit{zChaff}:} zChaff is an efficient solver written
2376 in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
2377 the directory that contains the \texttt{zchaff} executable.%
2378 \footref{cygwin-paths}
2379 The \cpp{} sources and executables for zChaff are available at
2380 \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
2381 versions 2004-05-13, 2004-11-15, and 2007-03-12.
2383 \item[$\bullet$] \textbf{\textit{zChaff\_JNI}:} The JNI version of zChaff is
2384 bundled with Kodkodi and is precompiled for the major
2385 platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
2386 which you will find on Kodkod's web site \cite{kodkod-2009}.
2388 \item[$\bullet$] \textbf{\textit{RSat}:} RSat is an efficient solver written in
2389 \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
2390 directory that contains the \texttt{rsat} executable.%
2391 \footref{cygwin-paths}
2392 The \cpp{} sources for RSat are available at
2393 \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been tested with version
2396 \item[$\bullet$] \textbf{\textit{BerkMin}:} BerkMin561 is an efficient solver
2397 written in C. To use BerkMin, set the environment variable
2398 \texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561}
2399 executable.\footref{cygwin-paths}
2400 The BerkMin executables are available at
2401 \url{http://eigold.tripod.com/BerkMin.html}.
2403 \item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}:} Variant of BerkMin that is
2404 included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
2405 version of BerkMin, set the environment variable
2406 \texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
2408 \footref{cygwin-paths}
2410 \item[$\bullet$] \textbf{\textit{Jerusat}:} Jerusat 1.3 is an efficient solver
2411 written in C. To use Jerusat, set the environment variable
2412 \texttt{JERUSAT\_HOME} to the directory that contains the \texttt{Jerusat1.3}
2414 \footref{cygwin-paths}
2415 The C sources for Jerusat are available at
2416 \url{http://www.cs.tau.ac.il/~ale1/Jerusat1.3.tgz}.
2418 \item[$\bullet$] \textbf{\textit{SAT4J}:} SAT4J is a reasonably efficient solver
2419 written in Java that can be used incrementally. It is bundled with Kodkodi and
2420 requires no further installation or configuration steps. Do not attempt to
2421 install the official SAT4J packages, because their API is incompatible with
2424 \item[$\bullet$] \textbf{\textit{SAT4J\_Light}:} Variant of SAT4J that is
2425 optimized for small problems. It can also be used incrementally.
2427 \item[$\bullet$] \textbf{\textit{smart}:} If \textit{sat\_solver} is set to
2428 \textit{smart}, Nitpick selects the first solver among the above that is
2429 recognized by Isabelle. If \textit{verbose} (\S\ref{output-format}) is enabled,
2430 Nitpick displays which SAT solver was chosen.
2434 \opdefault{batch\_size}{smart\_int}{smart}
2435 Specifies the maximum number of Kodkod problems that should be lumped together
2436 when invoking Kodkodi. Each problem corresponds to one scope. Lumping problems
2437 together ensures that Kodkodi is launched less often, but it makes the verbose
2438 output less readable and is sometimes detrimental to performance. If
2439 \textit{batch\_size} is set to \textit{smart}, the actual value used is 1 if
2440 \textit{debug} (\S\ref{output-format}) is set and 50 otherwise.
2442 \optrue{destroy\_constrs}{dont\_destroy\_constrs}
2443 Specifies whether formulas involving (co)in\-duc\-tive datatype constructors should
2444 be rewritten to use (automatically generated) discriminators and destructors.
2445 This optimization can drastically reduce the size of the Boolean formulas given
2449 {\small See also \textit{debug} (\S\ref{output-format}).}
2451 \optrue{specialize}{dont\_specialize}
2452 Specifies whether functions invoked with static arguments should be specialized.
2453 This optimization can drastically reduce the search space, especially for
2454 higher-order functions.
2457 {\small See also \textit{debug} (\S\ref{output-format}) and
2458 \textit{show\_consts} (\S\ref{output-format}).}
2460 \optrue{star\_linear\_preds}{dont\_star\_linear\_preds}
2461 Specifies whether Nitpick should use Kodkod's transitive closure operator to
2462 encode non-well-founded ``linear inductive predicates,'' i.e., inductive
2463 predicates for which each the predicate occurs in at most one assumption of each
2464 introduction rule. Using the reflexive transitive closure is in principle
2465 equivalent to setting \textit{iter} to the cardinality of the predicate's
2466 domain, but it is usually more efficient.
2468 {\small See also \textit{wf} (\S\ref{scope-of-search}), \textit{debug}
2469 (\S\ref{output-format}), and \textit{iter} (\S\ref{scope-of-search}).}
2471 \opnodefault{whack}{term\_list}
2472 Specifies a list of atomic terms (usually constants, but also free and schematic
2473 variables) that should be taken as being $\unk$ (unknown). This can be useful to
2474 reduce the size of the Kodkod problem if you can guess in advance that a
2475 constant might not be needed to find a countermodel.
2477 {\small See also \textit{debug} (\S\ref{output-format}).}
2479 \opnodefault{need}{term\_list}
2480 Specifies a list of datatype values (normally ground constructor terms) that
2481 should be part of the subterm-closed subsets used to approximate datatypes. If
2482 you know that a value must necessarily belong to the subset of representable
2483 values that approximates a datatype, specifying it can speed up the search,
2484 especially for high cardinalities.
2485 %By default, Nitpick inspects the conjecture to infer needed datatype values.
2487 \opsmart{total\_consts}{partial\_consts}
2488 Specifies whether constants occurring in the problem other than constructors can
2489 be assumed to be considered total for the representable values that approximate
2490 a datatype. This option is highly incomplete; it should be used only for
2491 problems that do not construct datatype values explicitly. Since this option is
2492 (in rare cases) unsound, counterexamples generated under these conditions are
2493 tagged as ``quasi genuine.''
2495 \opdefault{datatype\_sym\_break}{int}{\upshape 5}
2496 Specifies an upper bound on the number of datatypes for which Nitpick generates
2497 symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
2498 considerably, especially for unsatisfiable problems, but too much of it can slow
2501 \opdefault{kodkod\_sym\_break}{int}{\upshape 15}
2502 Specifies an upper bound on the number of relations for which Kodkod generates
2503 symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
2504 considerably, especially for unsatisfiable problems, but too much of it can slow
2507 \optrue{peephole\_optim}{no\_peephole\_optim}
2508 Specifies whether Nitpick should simplify the generated Kodkod formulas using a
2509 peephole optimizer. These optimizations can make a significant difference.
2510 Unless you are tracking down a bug in Nitpick or distrust the peephole
2511 optimizer, you should leave this option enabled.
2513 \opdefault{max\_threads}{int}{\upshape 0}
2514 Specifies the maximum number of threads to use in Kodkod. If this option is set
2515 to 0, Kodkod will compute an appropriate value based on the number of processor
2516 cores available. The option is implicitly set to 1 for automatic runs.
2519 {\small See also \textit{batch\_size} (\S\ref{optimizations}) and
2520 \textit{timeout} (\S\ref{timeouts}).}
2523 \subsection{Timeouts}
2527 \opdefault{timeout}{float\_or\_none}{\upshape 30}
2528 Specifies the maximum number of seconds that the \textbf{nitpick} command should
2529 spend looking for a counterexample. Nitpick tries to honor this constraint as
2530 well as it can but offers no guarantees. For automatic runs,
2531 \textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share
2532 a time slot whose length is specified by the ``Auto Counterexample Time
2533 Limit'' option in Proof General.
2536 {\small See also \textit{max\_threads} (\S\ref{optimizations}).}
2538 \opdefault{tac\_timeout}{float\_or\_none}{\upshape 0.5}
2539 Specifies the maximum number of seconds that the \textit{auto} tactic should use
2540 when checking a counterexample, and similarly that \textit{lexicographic\_order}
2541 and \textit{size\_change} should use when checking whether a (co)in\-duc\-tive
2542 predicate is well-founded. Nitpick tries to honor this constraint as well as it
2543 can but offers no guarantees.
2546 {\small See also \textit{wf} (\S\ref{scope-of-search}),
2547 \textit{check\_potential} (\S\ref{authentication}),
2548 and \textit{check\_genuine} (\S\ref{authentication}).}
2551 \section{Attribute Reference}
2552 \label{attribute-reference}
2554 Nitpick needs to consider the definitions of all constants occurring in a
2555 formula in order to falsify it. For constants introduced using the
2556 \textbf{definition} command, the definition is simply the associated
2557 \textit{\_def} axiom. In contrast, instead of using the internal representation
2558 of functions synthesized by Isabelle's \textbf{primrec}, \textbf{function}, and
2559 \textbf{nominal\_primrec} packages, Nitpick relies on the more natural
2560 equational specification entered by the user.
2562 Behind the scenes, Isabelle's built-in packages and theories rely on the
2563 following attributes to affect Nitpick's behavior:
2566 \flushitem{\textit{nitpick\_unfold}}
2569 This attribute specifies an equation that Nitpick should use to expand a
2570 constant. The equation should be logically equivalent to the constant's actual
2571 definition and should be of the form
2573 \qquad $c~{?}x_1~\ldots~{?}x_n \,=\, t$,
2577 \qquad $c~{?}x_1~\ldots~{?}x_n \,\equiv\, t$,
2579 where ${?}x_1, \ldots, {?}x_n$ are distinct variables and $c$ does not occur in
2580 $t$. Each occurrence of $c$ in the problem is expanded to $\lambda x_1\,\ldots
2583 \flushitem{\textit{nitpick\_simp}}
2586 This attribute specifies the equations that constitute the specification of a
2587 constant. The \textbf{primrec}, \textbf{function}, and
2588 \textbf{nominal\_\allowbreak primrec} packages automatically attach this
2589 attribute to their \textit{simps} rules. The equations must be of the form
2591 \qquad $c~t_1~\ldots\ t_n \;\bigl[{=}\; u\bigr]$
2595 \qquad $c~t_1~\ldots\ t_n \,\equiv\, u.$
2597 \flushitem{\textit{nitpick\_psimp}}
2600 This attribute specifies the equations that constitute the partial specification
2601 of a constant. The \textbf{function} package automatically attaches this
2602 attribute to its \textit{psimps} rules. The conditional equations must be of the
2605 \qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \;\bigl[{=}\; u\bigr]$
2609 \qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,\equiv\, u$.
2611 \flushitem{\textit{nitpick\_choice\_spec}}
2614 This attribute specifies the (free-form) specification of a constant defined
2615 using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command.
2618 When faced with a constant, Nitpick proceeds as follows:
2621 \item[1.] If the \textit{nitpick\_simp} set associated with the constant
2622 is not empty, Nitpick uses these rules as the specification of the constant.
2624 \item[2.] Otherwise, if the \textit{nitpick\_psimp} set associated with
2625 the constant is not empty, it uses these rules as the specification of the
2628 \item[3.] Otherwise, if the constant was defined using the
2629 \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command and the
2630 \textit{nitpick\_choice\_spec} set associated with the constant is not empty, it
2631 uses these theorems as the specification of the constant.
2633 \item[4.] Otherwise, it looks up the definition of the constant. If the
2634 \textit{nitpick\_unfold} set associated with the constant is not empty, it uses
2635 the latest rule added to the set as the definition of the constant; otherwise it
2636 uses the actual definition axiom.
2639 \item[1.] If the definition is of the form
2641 \qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{lfp}~(\lambda f.\; t)$
2645 \qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{gfp}~(\lambda f.\; t).$
2647 Nitpick assumes that the definition was made using a (co)inductive package
2648 based on the user-specified introduction rules registered in Isabelle's internal
2649 \textit{Spec\_Rules} table. The tool uses the introduction rules to ascertain
2650 whether the definition is well-founded and the definition to generate a
2651 fixed-point equation or an unrolled equation.
2653 \item[2.] If the definition is compact enough, the constant is \textsl{unfolded}
2654 wherever it appears; otherwise, it is defined equationally, as with
2655 the \textit{nitpick\_simp} attribute.
2659 As an illustration, consider the inductive definition
2662 \textbf{inductive}~\textit{odd}~\textbf{where} \\
2663 ``\textit{odd}~1'' $\,\mid$ \\
2664 ``\textit{odd}~$n\,\Longrightarrow\, \textit{odd}~(\textit{Suc}~(\textit{Suc}~n))$''
2667 By default, Nitpick uses the \textit{lfp}-based definition in conjunction with
2668 the introduction rules. To override this, you can specify an alternative
2669 definition as follows:
2672 \textbf{lemma} $\mathit{odd\_alt\_unfold}$ [\textit{nitpick\_unfold}]:\kern.4em ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
2675 Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2
2676 = 1$. Alternatively, you can specify an equational specification of the constant:
2679 \textbf{lemma} $\mathit{odd\_simp}$ [\textit{nitpick\_simp}]:\kern.4em ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
2682 Such tweaks should be done with great care, because Nitpick will assume that the
2683 constant is completely defined by its equational specification. For example, if
2684 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
2685 $\textit{odd}~n$ arbitrarily for even values of $n$. The \textit{debug}
2686 (\S\ref{output-format}) option is extremely useful to understand what is going
2687 on when experimenting with \textit{nitpick\_} attributes.
2689 Because of its internal three-valued logic, Nitpick tends to lose a
2690 lot of precision in the presence of partially specified constants. For example,
2693 \textbf{lemma} \textit{odd\_simp} [\textit{nitpick\_simp}]:\kern.4em ``$\textit{odd~x} = \lnot\, \textit{even}~x$''
2699 \textbf{lemma} \textit{odd\_psimps} [\textit{nitpick\_simp}]: \\
2700 ``$\textit{even~x} \,\Longrightarrow\, \textit{odd~x} = \textit{False\/}$'' \\
2701 ``$\lnot\, \textit{even~x} \,\Longrightarrow\, \textit{odd~x} = \textit{True\/}$''
2704 Because Nitpick sometimes unfolds definitions but never simplification rules,
2705 you can ensure that a constant is defined explicitly using the
2706 \textit{nitpick\_simp}. For example:
2709 \textbf{definition}~\textit{optimum} \textbf{where} [\textit{nitpick\_simp}]: \\
2710 ``$\textit{optimum}~t =
2711 (\forall u.\; \textit{consistent}~u \mathrel{\land} \textit{alphabet}~t = \textit{alphabet}~u$ \\
2712 \phantom{``$\textit{optimum}~t = (\forall u.\;$}${\mathrel{\land}}\; \textit{freq}~t = \textit{freq}~u \longrightarrow
2713 \textit{cost}~t \le \textit{cost}~u)$''
2716 In some rare occasions, you might want to provide an inductive or coinductive
2717 view on top of an existing constant $c$. The easiest way to achieve this is to
2718 define a new constant $c'$ (co)inductively. Then prove that $c$ equals $c'$
2719 and let Nitpick know about it:
2722 \textbf{lemma} \textit{c\_alt\_unfold} [\textit{nitpick\_unfold}]:\kern.4em ``$c \equiv c'$\kern2pt ''
2725 This ensures that Nitpick will substitute $c'$ for $c$ and use the (co)inductive
2728 \section{Standard ML Interface}
2729 \label{standard-ml-interface}
2731 Nitpick provides a rich Standard ML interface used mainly for internal purposes
2732 and debugging. Among the most interesting functions exported by Nitpick are
2733 those that let you invoke the tool programmatically and those that let you
2734 register and unregister custom coinductive datatypes as well as term
2737 \subsection{Invocation of Nitpick}
2738 \label{invocation-of-nitpick}
2740 The \textit{Nitpick} structure offers the following functions for invoking your
2741 favorite counterexample generator:
2744 $\textbf{val}\,~\textit{pick\_nits\_in\_term} : \\
2745 \hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{mode}
2746 \rightarrow \textit{int} \rightarrow \textit{int} \rightarrow \textit{int}$ \\
2747 $\hbox{}\quad{\rightarrow}\; (\textit{term} * \textit{term})~\textit{list}
2748 \rightarrow \textit{term~list} \rightarrow \textit{term} \rightarrow \textit{string} * \textit{Proof.state}$ \\
2749 $\textbf{val}\,~\textit{pick\_nits\_in\_subgoal} : \\
2750 \hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{mode} \rightarrow \textit{int} \rightarrow \textit{int} \rightarrow \textit{string} * \textit{Proof.state}$
2753 The return value is a new proof state paired with an outcome string
2754 (``genuine'', ``quasi\_genuine'', ``potential'', ``none'', or ``unknown''). The
2755 \textit{params} type is a large record that lets you set Nitpick's options. The
2756 current default options can be retrieved by calling the following function
2757 defined in the \textit{Nitpick\_Isar} structure:
2760 $\textbf{val}\,~\textit{default\_params} :\,
2761 \textit{theory} \rightarrow (\textit{string} * \textit{string})~\textit{list} \rightarrow \textit{params}$
2764 The second argument lets you override option values before they are parsed and
2765 put into a \textit{params} record. Here is an example where Nitpick is invoked
2766 on subgoal $i$ of $n$ with no time limit:
2769 $\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout\/}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
2770 $\textbf{val}\,~(\textit{outcome},\, \textit{state}') = {}$ \\
2771 $\hbox{}\quad\textit{Nitpick.pick\_nits\_in\_subgoal}~\textit{state}~\textit{params}~\textit{Nitpick.Normal}~\textit{i}~\textit{n}$
2776 \subsection{Registration of Coinductive Datatypes}
2777 \label{registration-of-coinductive-datatypes}
2779 If you have defined a custom coinductive datatype, you can tell Nitpick about
2780 it, so that it can use an efficient Kodkod axiomatization similar to the one it
2781 uses for lazy lists. The interface for registering and unregistering coinductive
2782 datatypes consists of the following pair of functions defined in the
2783 \textit{Nitpick\_HOL} structure:
2786 $\textbf{val}\,~\textit{register\_codatatype\/} : {}$ \\
2787 $\hbox{}\quad\textit{morphism} \rightarrow \textit{typ} \rightarrow \textit{string} \rightarrow (\textit{string} \times \textit{typ})\;\textit{list} \rightarrow \textit{Context.generic} {}$ \\
2788 $\hbox{}\quad{\rightarrow}\; \textit{Context.generic}$ \\
2789 $\textbf{val}\,~\textit{unregister\_codatatype\/} : {}$ \\
2790 $\hbox{}\quad\textit{morphism} \rightarrow \textit{typ} \rightarrow \textit{Context.generic} \rightarrow \textit{Context.generic} {}$
2793 The type $'a~\textit{llist}$ of lazy lists is already registered; had it
2794 not been, you could have told Nitpick about it by adding the following line
2795 to your theory file:
2798 $\textbf{declaration}~\,\{{*}$ \\
2799 $\hbox{}\quad\textit{Nitpick\_HOL.register\_codatatype}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
2800 $\hbox{}\qquad\quad @\{\antiq{const\_name}~ \textit{llist\_case}\}$ \\
2801 $\hbox{}\qquad\quad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])$ \\
2805 The \textit{register\_codatatype} function takes a coinductive datatype, its
2806 case function, and the list of its constructors (in addition to the current
2807 morphism and generic proof context). The case function must take its arguments
2808 in the order that the constructors are listed. If no case function with the
2809 correct signature is available, simply pass the empty string.
2811 On the other hand, if your goal is to cripple Nitpick, add the following line to
2812 your theory file and try to check a few conjectures about lazy lists:
2815 $\textbf{declaration}~\,\{{*}$ \\
2816 $\hbox{}\quad\textit{Nitpick\_HOL.unregister\_codatatype}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
2820 Inductive datatypes can be registered as coinductive datatypes, given
2821 appropriate coinductive constructors. However, doing so precludes
2822 the use of the inductive constructors---Nitpick will generate an error if they
2825 \subsection{Registration of Term Postprocessors}
2826 \label{registration-of-term-postprocessors}
2828 It is possible to change the output of any term that Nitpick considers a
2829 datatype by registering a term postprocessor. The interface for registering and
2830 unregistering postprocessors consists of the following pair of functions defined
2831 in the \textit{Nitpick\_Model} structure:
2834 $\textbf{type}\,~\textit{term\_postprocessor}\,~{=} {}$ \\
2835 $\hbox{}\quad\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \rightarrow \textit{term}$ \\
2836 $\textbf{val}\,~\textit{register\_term\_postprocessor} : {}$ \\
2837 $\hbox{}\quad\textit{typ} \rightarrow \textit{term\_postprocessor} \rightarrow \textit{morphism} \rightarrow \textit{Context.generic}$ \\
2838 $\hbox{}\quad{\rightarrow}\; \textit{Context.generic}$ \\
2839 $\textbf{val}\,~\textit{unregister\_term\_postprocessor} : {}$ \\
2840 $\hbox{}\quad\textit{typ} \rightarrow \textit{morphism} \rightarrow \textit{Context.generic} \rightarrow \textit{Context.generic}$
2843 \S\ref{typedefs-quotient-types-records-rationals-and-reals} and
2844 \texttt{src/HOL/Library/Multiset.thy} illustrate this feature in context.
2846 \section{Known Bugs and Limitations}
2847 \label{known-bugs-and-limitations}
2849 Here are the known bugs and limitations in Nitpick at the time of writing:
2852 \item[$\bullet$] Underspecified functions defined using the \textbf{primrec},
2853 \textbf{function}, or \textbf{nominal\_\allowbreak primrec} packages can lead
2854 Nitpick to generate spurious counterexamples for theorems that refer to values
2855 for which the function is not defined. For example:
2858 \textbf{primrec} \textit{prec} \textbf{where} \\
2859 ``$\textit{prec}~(\textit{Suc}~n) = n$'' \\[2\smallskipamount]
2860 \textbf{lemma} ``$\textit{prec}~0 = \undef$'' \\
2861 \textbf{nitpick} \\[2\smallskipamount]
2862 \quad{\slshape Nitpick found a counterexample for \textit{card nat}~= 2:
2864 \\[2\smallskipamount]
2865 \hbox{}\qquad Empty assignment} \nopagebreak\\[2\smallskipamount]
2866 \textbf{by}~(\textit{auto simp}:~\textit{prec\_def})
2869 Such theorems are generally considered bad style because they rely on the
2870 internal representation of functions synthesized by Isabelle, an implementation
2873 \item[$\bullet$] Similarly, Nitpick might find spurious counterexamples for
2874 theorems that rely on the use of the indefinite description operator internally
2875 by \textbf{specification} and \textbf{quot\_type}.
2877 \item[$\bullet$] Axioms or definitions that restrict the possible values of the
2878 \textit{undefined} constant or other partially specified built-in Isabelle
2879 constants (e.g., \textit{Abs\_} and \textit{Rep\_} constants) are in general
2880 ignored. Again, such nonconservative extensions are generally considered bad
2883 \item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions,
2884 which can become invalid if you change the definition of an inductive predicate
2885 that is registered in the cache. To clear the cache,
2886 run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
2889 \item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
2890 \textbf{guess} command in a structured proof.
2892 \item[$\bullet$] The \textit{nitpick\_xxx} attributes and the
2893 \textit{Nitpick\_xxx.register\_yyy} functions can cause havoc if used
2896 \item[$\bullet$] Although this has never been observed, arbitrary theorem
2897 morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
2899 \item[$\bullet$] All constants, types, free variables, and schematic variables
2900 whose names start with \textit{Nitpick}{.} are reserved for internal use.
2904 \bibliography{../manual}{}
2905 \bibliographystyle{abbrv}