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