1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/Nitpick/nitpick.tex Thu Oct 22 14:45:20 2009 +0200
1.3 @@ -0,0 +1,2484 @@
1.4 +\documentclass[a4paper,12pt]{article}
1.5 +\usepackage[T1]{fontenc}
1.6 +\usepackage{amsmath}
1.7 +\usepackage{amssymb}
1.8 +\usepackage[french,english]{babel}
1.9 +\usepackage{color}
1.10 +\usepackage{graphicx}
1.11 +%\usepackage{mathpazo}
1.12 +\usepackage{multicol}
1.13 +\usepackage{stmaryrd}
1.14 +%\usepackage[scaled=.85]{beramono}
1.15 +\usepackage{../iman,../pdfsetup}
1.16 +
1.17 +%\oddsidemargin=4.6mm
1.18 +%\evensidemargin=4.6mm
1.19 +%\textwidth=150mm
1.20 +%\topmargin=4.6mm
1.21 +%\headheight=0mm
1.22 +%\headsep=0mm
1.23 +%\textheight=234mm
1.24 +
1.25 +\def\Colon{\mathord{:\mkern-1.5mu:}}
1.26 +%\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
1.27 +%\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
1.28 +\def\lparr{\mathopen{(\mkern-4mu\mid}}
1.29 +\def\rparr{\mathclose{\mid\mkern-4mu)}}
1.30 +
1.31 +\def\undef{\textit{undefined}}
1.32 +\def\unk{{?}}
1.33 +%\def\unr{\textit{others}}
1.34 +\def\unr{\ldots}
1.35 +\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
1.36 +\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
1.37 +
1.38 +\hyphenation{Mini-Sat size-change First-Steps grand-parent nit-pick
1.39 +counter-example counter-examples data-type data-types co-data-type
1.40 +co-data-types in-duc-tive co-in-duc-tive}
1.41 +
1.42 +\urlstyle{tt}
1.43 +
1.44 +\begin{document}
1.45 +
1.46 +\title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]
1.47 +Picking Nits \\[\smallskipamount]
1.48 +\Large A User's Guide to Nitpick for Isabelle/HOL 2010}
1.49 +\author{\hbox{} \\
1.50 +Jasmin Christian Blanchette \\
1.51 +{\normalsize Fakult\"at f\"ur Informatik, Technische Universit\"at M\"unchen} \\
1.52 +\hbox{}}
1.53 +
1.54 +\maketitle
1.55 +
1.56 +\tableofcontents
1.57 +
1.58 +\setlength{\parskip}{.7em plus .2em minus .1em}
1.59 +\setlength{\parindent}{0pt}
1.60 +\setlength{\abovedisplayskip}{\parskip}
1.61 +\setlength{\abovedisplayshortskip}{.9\parskip}
1.62 +\setlength{\belowdisplayskip}{\parskip}
1.63 +\setlength{\belowdisplayshortskip}{.9\parskip}
1.64 +
1.65 +% General-purpose enum environment with correct spacing
1.66 +\newenvironment{enum}%
1.67 + {\begin{list}{}{%
1.68 + \setlength{\topsep}{.1\parskip}%
1.69 + \setlength{\partopsep}{.1\parskip}%
1.70 + \setlength{\itemsep}{\parskip}%
1.71 + \advance\itemsep by-\parsep}}
1.72 + {\end{list}}
1.73 +
1.74 +\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
1.75 +\advance\rightskip by\leftmargin}
1.76 +\def\post{\vskip0pt plus1ex\endgroup}
1.77 +
1.78 +\def\prew{\pre\advance\rightskip by-\leftmargin}
1.79 +\def\postw{\post}
1.80 +
1.81 +\section{Introduction}
1.82 +\label{introduction}
1.83 +
1.84 +Nitpick \cite{blanchette-nipkow-2009} is a counterexample generator for
1.85 +Isabelle/HOL \cite{isa-tutorial} that is designed to handle formulas
1.86 +combining (co)in\-duc\-tive datatypes, (co)in\-duc\-tively defined predicates, and
1.87 +quantifiers. It builds on Kodkod \cite{torlak-jackson-2007}, a highly optimized
1.88 +first-order relational model finder developed by the Software Design Group at
1.89 +MIT. It is conceptually similar to Refute \cite{weber-2008}, from which it
1.90 +borrows many ideas and code fragments, but it benefits from Kodkod's
1.91 +optimizations and a new encoding scheme. The name Nitpick is shamelessly
1.92 +appropriated from a now retired Alloy precursor.
1.93 +
1.94 +Nitpick is easy to use---you simply enter \textbf{nitpick} after a putative
1.95 +theorem and wait a few seconds. Nonetheless, there are situations where knowing
1.96 +how it works under the hood and how it reacts to various options helps
1.97 +increase the test coverage. This manual also explains how to install the tool on
1.98 +your workstation. Should the motivation fail you, think of the many hours of
1.99 +hard work Nitpick will save you. Proving non-theorems is \textsl{hard work}.
1.100 +
1.101 +Another common use of Nitpick is to find out whether the axioms of a locale are
1.102 +satisfiable, while the locale is being developed. To check this, it suffices to
1.103 +write
1.104 +
1.105 +\prew
1.106 +\textbf{lemma}~``$\textit{False}$'' \\
1.107 +\textbf{nitpick}~[\textit{show\_all}]
1.108 +\postw
1.109 +
1.110 +after the locale's \textbf{begin} keyword. To falsify \textit{False}, Nitpick
1.111 +must find a model for the axioms. If it finds no model, we have an indication
1.112 +that the axioms might be unsatisfiable.
1.113 +
1.114 +\newbox\boxA
1.115 +\setbox\boxA=\hbox{\texttt{nospam}}
1.116 +
1.117 +The known bugs and limitations at the time of writing are listed in
1.118 +\S\ref{known-bugs-and-limitations}. Comments and bug reports concerning Nitpick
1.119 +or this manual should be directed to
1.120 +\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
1.121 +in.\allowbreak tum.\allowbreak de}.
1.122 +
1.123 +\vskip2.5\smallskipamount
1.124 +
1.125 +\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
1.126 +suggesting several textual improvements.
1.127 +% and Perry James for reporting a typo.
1.128 +
1.129 +\section{First Steps}
1.130 +\label{first-steps}
1.131 +
1.132 +This section introduces Nitpick by presenting small examples. If possible, you
1.133 +should try out the examples on your workstation. Your theory file should start
1.134 +the standard way:
1.135 +
1.136 +\prew
1.137 +\textbf{theory}~\textit{Scratch} \\
1.138 +\textbf{imports}~\textit{Main} \\
1.139 +\textbf{begin}
1.140 +\postw
1.141 +
1.142 +The results presented here were obtained using the JNI version of MiniSat and
1.143 +with multithreading disabled to reduce nondeterminism. This was done by adding
1.144 +the line
1.145 +
1.146 +\prew
1.147 +\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSatJNI}, \,\textit{max\_threads}~= 1]
1.148 +\postw
1.149 +
1.150 +after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
1.151 +Kodkodi and is precompiled for the major platforms. Other SAT solvers can also
1.152 +be installed, as explained in \S\ref{optimizations}. If you have already
1.153 +configured SAT solvers in Isabelle (e.g., for Refute), these will also be
1.154 +available to Nitpick.
1.155 +
1.156 +Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
1.157 +Nitpick also provides an automatic mode that can be enabled by specifying
1.158 +
1.159 +\prew
1.160 +\textbf{nitpick\_params} [\textit{auto}]
1.161 +\postw
1.162 +
1.163 +at the beginning of the theory file. In this mode, Nitpick is run for up to 5
1.164 +seconds (by default) on every newly entered theorem, much like Auto Quickcheck.
1.165 +
1.166 +\subsection{Propositional Logic}
1.167 +\label{propositional-logic}
1.168 +
1.169 +Let's start with a trivial example from propositional logic:
1.170 +
1.171 +\prew
1.172 +\textbf{lemma}~``$P \longleftrightarrow Q$'' \\
1.173 +\textbf{nitpick}
1.174 +\postw
1.175 +
1.176 +You should get the following output:
1.177 +
1.178 +\prew
1.179 +\slshape
1.180 +Nitpick found a counterexample: \\[2\smallskipamount]
1.181 +\hbox{}\qquad Free variables: \nopagebreak \\
1.182 +\hbox{}\qquad\qquad $P = \textit{True}$ \\
1.183 +\hbox{}\qquad\qquad $Q = \textit{False}$
1.184 +\postw
1.185 +
1.186 +Nitpick can also be invoked on individual subgoals, as in the example below:
1.187 +
1.188 +\prew
1.189 +\textbf{apply}~\textit{auto} \\[2\smallskipamount]
1.190 +{\slshape goal (2 subgoals): \\
1.191 +\ 1. $P\,\Longrightarrow\, Q$ \\
1.192 +\ 2. $Q\,\Longrightarrow\, P$} \\[2\smallskipamount]
1.193 +\textbf{nitpick}~1 \\[2\smallskipamount]
1.194 +{\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.195 +\hbox{}\qquad Free variables: \nopagebreak \\
1.196 +\hbox{}\qquad\qquad $P = \textit{True}$ \\
1.197 +\hbox{}\qquad\qquad $Q = \textit{False}$} \\[2\smallskipamount]
1.198 +\textbf{nitpick}~2 \\[2\smallskipamount]
1.199 +{\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.200 +\hbox{}\qquad Free variables: \nopagebreak \\
1.201 +\hbox{}\qquad\qquad $P = \textit{False}$ \\
1.202 +\hbox{}\qquad\qquad $Q = \textit{True}$} \\[2\smallskipamount]
1.203 +\textbf{oops}
1.204 +\postw
1.205 +
1.206 +\subsection{Type Variables}
1.207 +\label{type-variables}
1.208 +
1.209 +If you are left unimpressed by the previous example, don't worry. The next
1.210 +one is more mind- and computer-boggling:
1.211 +
1.212 +\prew
1.213 +\textbf{lemma} ``$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
1.214 +\postw
1.215 +\pagebreak[2] %% TYPESETTING
1.216 +
1.217 +The putative lemma involves the definite description operator, {THE}, presented
1.218 +in section 5.10.1 of the Isabelle tutorial \cite{isa-tutorial}. The
1.219 +operator is defined by the axiom $(\textrm{THE}~x.\; x = a) = a$. The putative
1.220 +lemma is merely asserting the indefinite description operator axiom with {THE}
1.221 +substituted for {SOME}.
1.222 +
1.223 +The free variable $x$ and the bound variable $y$ have type $'a$. For formulas
1.224 +containing type variables, Nitpick enumerates the possible domains for each type
1.225 +variable, up to a given cardinality (8 by default), looking for a finite
1.226 +countermodel:
1.227 +
1.228 +\prew
1.229 +\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
1.230 +\slshape
1.231 +Trying 8 scopes: \nopagebreak \\
1.232 +\hbox{}\qquad \textit{card}~$'a$~= 1; \\
1.233 +\hbox{}\qquad \textit{card}~$'a$~= 2; \\
1.234 +\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1.235 +\hbox{}\qquad \textit{card}~$'a$~= 8. \\[2\smallskipamount]
1.236 +Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
1.237 +\hbox{}\qquad Free variables: \nopagebreak \\
1.238 +\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
1.239 +\hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount]
1.240 +Total time: 580 ms.
1.241 +\postw
1.242 +
1.243 +Nitpick found a counterexample in which $'a$ has cardinality 3. (For
1.244 +cardinalities 1 and 2, the formula holds.) In the counterexample, the three
1.245 +values of type $'a$ are written $a_1$, $a_2$, and $a_3$.
1.246 +
1.247 +The message ``Trying $n$ scopes: {\ldots}''\ is shown only if the option
1.248 +\textit{verbose} is enabled. You can specify \textit{verbose} each time you
1.249 +invoke \textbf{nitpick}, or you can set it globally using the command
1.250 +
1.251 +\prew
1.252 +\textbf{nitpick\_params} [\textit{verbose}]
1.253 +\postw
1.254 +
1.255 +This command also displays the current default values for all of the options
1.256 +supported by Nitpick. The options are listed in \S\ref{option-reference}.
1.257 +
1.258 +\subsection{Constants}
1.259 +\label{constants}
1.260 +
1.261 +By just looking at Nitpick's output, it might not be clear why the
1.262 +counterexample in \S\ref{type-variables} is genuine. Let's invoke Nitpick again,
1.263 +this time telling it to show the values of the constants that occur in the
1.264 +formula:
1.265 +
1.266 +\prew
1.267 +\textbf{lemma}~``$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$'' \\
1.268 +\textbf{nitpick}~[\textit{show\_consts}] \\[2\smallskipamount]
1.269 +\slshape
1.270 +Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
1.271 +\hbox{}\qquad Free variables: \nopagebreak \\
1.272 +\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
1.273 +\hbox{}\qquad\qquad $x = a_3$ \\
1.274 +\hbox{}\qquad Constant: \nopagebreak \\
1.275 +\hbox{}\qquad\qquad $\textit{The}~\textsl{fallback} = a_1$
1.276 +\postw
1.277 +
1.278 +We can see more clearly now. Since the predicate $P$ isn't true for a unique
1.279 +value, $\textrm{THE}~y.\;P~y$ can denote any value of type $'a$, even
1.280 +$a_1$. Since $P~a_1$ is false, the entire formula is falsified.
1.281 +
1.282 +As an optimization, Nitpick's preprocessor introduced the special constant
1.283 +``\textit{The} fallback'' corresponding to $\textrm{THE}~y.\;P~y$ (i.e.,
1.284 +$\mathit{The}~(\lambda y.\;P~y)$) when there doesn't exist a unique $y$
1.285 +satisfying $P~y$. We disable this optimization by passing the
1.286 +\textit{full\_descrs} option:
1.287 +
1.288 +\prew
1.289 +\textbf{nitpick}~[\textit{full\_descrs},\, \textit{show\_consts}] \\[2\smallskipamount]
1.290 +\slshape
1.291 +Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
1.292 +\hbox{}\qquad Free variables: \nopagebreak \\
1.293 +\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
1.294 +\hbox{}\qquad\qquad $x = a_3$ \\
1.295 +\hbox{}\qquad Constant: \nopagebreak \\
1.296 +\hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$
1.297 +\postw
1.298 +
1.299 +As the result of another optimization, Nitpick directly assigned a value to the
1.300 +subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we
1.301 +disable this second optimization by using the command
1.302 +
1.303 +\prew
1.304 +\textbf{nitpick}~[\textit{dont\_specialize},\, \textit{full\_descrs},\,
1.305 +\textit{show\_consts}]
1.306 +\postw
1.307 +
1.308 +we finally get \textit{The}:
1.309 +
1.310 +\prew
1.311 +\slshape Constant: \nopagebreak \\
1.312 +\hbox{}\qquad $\mathit{The} = \undef{}
1.313 + (\!\begin{aligned}[t]%
1.314 + & \{\} := a_3,\> \{a_3\} := a_3,\> \{a_2\} := a_2, \\[-2pt] %% TYPESETTING
1.315 + & \{a_2, a_3\} := a_1,\> \{a_1\} := a_1,\> \{a_1, a_3\} := a_3, \\[-2pt]
1.316 + & \{a_1, a_2\} := a_3,\> \{a_1, a_2, a_3\} := a_3)\end{aligned}$
1.317 +\postw
1.318 +
1.319 +Notice that $\textit{The}~(\lambda y.\;P~y) = \textit{The}~\{a_2, a_3\} = a_1$,
1.320 +just like before.\footnote{The \undef{} symbol's presence is explained as
1.321 +follows: In higher-order logic, any function can be built from the undefined
1.322 +function using repeated applications of the function update operator $f(x :=
1.323 +y)$, just like any list can be built from the empty list using $x \mathbin{\#}
1.324 +xs$.}
1.325 +
1.326 +Our misadventures with THE suggest adding `$\exists!x{.}$' (``there exists a
1.327 +unique $x$ such that'') at the front of our putative lemma's assumption:
1.328 +
1.329 +\prew
1.330 +\textbf{lemma}~``$\exists {!}x.\; P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
1.331 +\postw
1.332 +
1.333 +The fix appears to work:
1.334 +
1.335 +\prew
1.336 +\textbf{nitpick} \\[2\smallskipamount]
1.337 +\slshape Nitpick found no counterexample.
1.338 +\postw
1.339 +
1.340 +We can further increase our confidence in the formula by exhausting all
1.341 +cardinalities up to 50:
1.342 +
1.343 +\prew
1.344 +\textbf{nitpick} [\textit{card} $'a$~= 1--50]\footnote{The symbol `--'
1.345 +can be entered as \texttt{-} (hyphen) or
1.346 +\texttt{\char`\\\char`\<midarrow\char`\>}.} \\[2\smallskipamount]
1.347 +\slshape Nitpick found no counterexample.
1.348 +\postw
1.349 +
1.350 +Let's see if Sledgehammer \cite{sledgehammer-2009} can find a proof:
1.351 +
1.352 +\prew
1.353 +\textbf{sledgehammer} \\[2\smallskipamount]
1.354 +{\slshape Sledgehammer: external prover ``$e$'' for subgoal 1: \\
1.355 +$\exists{!}x.\; P~x\,\Longrightarrow\, P~(\hbox{\slshape THE}~y.\; P~y)$ \\
1.356 +Try this command: \textrm{apply}~(\textit{metis~the\_equality})} \\[2\smallskipamount]
1.357 +\textbf{apply}~(\textit{metis~the\_equality\/}) \nopagebreak \\[2\smallskipamount]
1.358 +{\slshape No subgoals!}% \\[2\smallskipamount]
1.359 +%\textbf{done}
1.360 +\postw
1.361 +
1.362 +This must be our lucky day.
1.363 +
1.364 +\subsection{Skolemization}
1.365 +\label{skolemization}
1.366 +
1.367 +Are all invertible functions onto? Let's find out:
1.368 +
1.369 +\prew
1.370 +\textbf{lemma} ``$\exists g.\; \forall x.~g~(f~x) = x
1.371 + \,\Longrightarrow\, \forall y.\; \exists x.~y = f~x$'' \\
1.372 +\textbf{nitpick} \\[2\smallskipamount]
1.373 +\slshape
1.374 +Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\[2\smallskipamount]
1.375 +\hbox{}\qquad Free variable: \nopagebreak \\
1.376 +\hbox{}\qquad\qquad $f = \undef{}(b_1 := a_1)$ \\
1.377 +\hbox{}\qquad Skolem constants: \nopagebreak \\
1.378 +\hbox{}\qquad\qquad $g = \undef{}(a_1 := b_1,\> a_2 := b_1)$ \\
1.379 +\hbox{}\qquad\qquad $y = a_2$
1.380 +\postw
1.381 +
1.382 +Although $f$ is the only free variable occurring in the formula, Nitpick also
1.383 +displays values for the bound variables $g$ and $y$. These values are available
1.384 +to Nitpick because it performs skolemization as a preprocessing step.
1.385 +
1.386 +In the previous example, skolemization only affected the outermost quantifiers.
1.387 +This is not always the case, as illustrated below:
1.388 +
1.389 +\prew
1.390 +\textbf{lemma} ``$\exists x.\; \forall f.\; f~x = x$'' \\
1.391 +\textbf{nitpick} \\[2\smallskipamount]
1.392 +\slshape
1.393 +Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
1.394 +\hbox{}\qquad Skolem constant: \nopagebreak \\
1.395 +\hbox{}\qquad\qquad $\lambda x.\; f =
1.396 + \undef{}(\!\begin{aligned}[t]
1.397 + & a_1 := \undef{}(a_1 := a_2,\> a_2 := a_1), \\[-2pt]
1.398 + & a_2 := \undef{}(a_1 := a_1,\> a_2 := a_1))\end{aligned}$
1.399 +\postw
1.400 +
1.401 +The variable $f$ is bound within the scope of $x$; therefore, $f$ depends on
1.402 +$x$, as suggested by the notation $\lambda x.\,f$. If $x = a_1$, then $f$ is the
1.403 +function that maps $a_1$ to $a_2$ and vice versa; otherwise, $x = a_2$ and $f$
1.404 +maps both $a_1$ and $a_2$ to $a_1$. In both cases, $f~x \not= x$.
1.405 +
1.406 +The source of the Skolem constants is sometimes more obscure:
1.407 +
1.408 +\prew
1.409 +\textbf{lemma} ``$\mathit{refl}~r\,\Longrightarrow\, \mathit{sym}~r$'' \\
1.410 +\textbf{nitpick} \\[2\smallskipamount]
1.411 +\slshape
1.412 +Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
1.413 +\hbox{}\qquad Free variable: \nopagebreak \\
1.414 +\hbox{}\qquad\qquad $r = \{(a_1, a_1),\, (a_2, a_1),\, (a_2, a_2)\}$ \\
1.415 +\hbox{}\qquad Skolem constants: \nopagebreak \\
1.416 +\hbox{}\qquad\qquad $\mathit{sym}.x = a_2$ \\
1.417 +\hbox{}\qquad\qquad $\mathit{sym}.y = a_1$
1.418 +\postw
1.419 +
1.420 +What happened here is that Nitpick expanded the \textit{sym} constant to its
1.421 +definition:
1.422 +
1.423 +\prew
1.424 +$\mathit{sym}~r \,\equiv\,
1.425 + \forall x\> y.\,\> (x, y) \in r \longrightarrow (y, x) \in r.$
1.426 +\postw
1.427 +
1.428 +As their names suggest, the Skolem constants $\mathit{sym}.x$ and
1.429 +$\mathit{sym}.y$ are simply the bound variables $x$ and $y$
1.430 +from \textit{sym}'s definition.
1.431 +
1.432 +Although skolemization is a useful optimization, you can disable it by invoking
1.433 +Nitpick with \textit{dont\_skolemize}. See \S\ref{optimizations} for details.
1.434 +
1.435 +\subsection{Natural Numbers and Integers}
1.436 +\label{natural-numbers-and-integers}
1.437 +
1.438 +Because of the axiom of infinity, the type \textit{nat} does not admit any
1.439 +finite models. To deal with this, Nitpick considers prefixes $\{0,\, 1,\,
1.440 +\ldots,\, K - 1\}$ of \textit{nat} (where $K = \textit{card}~\textit{nat}$) and
1.441 +maps all other numbers to the undefined value ($\unk$). The type \textit{int} is
1.442 +handled in a similar way: If $K = \textit{card}~\textit{int}$, the subset of
1.443 +\textit{int} known to Nitpick is $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor
1.444 +K/2 \rfloor\}$. Undefined values lead to a three-valued logic.
1.445 +
1.446 +Here is an example involving \textit{int}:
1.447 +
1.448 +\prew
1.449 +\textbf{lemma} ``$\lbrakk i \le j;\> n \le (m{\Colon}\mathit{int})\rbrakk \,\Longrightarrow\, i * n + j * m \le i * m + j * n$'' \\
1.450 +\textbf{nitpick} \\[2\smallskipamount]
1.451 +\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.452 +\hbox{}\qquad Free variables: \nopagebreak \\
1.453 +\hbox{}\qquad\qquad $i = 0$ \\
1.454 +\hbox{}\qquad\qquad $j = 1$ \\
1.455 +\hbox{}\qquad\qquad $m = 1$ \\
1.456 +\hbox{}\qquad\qquad $n = 0$
1.457 +\postw
1.458 +
1.459 +With infinite types, we don't always have the luxury of a genuine counterexample
1.460 +and must often content ourselves with a potential one. The tedious task of
1.461 +finding out whether the potential counterexample is in fact genuine can be
1.462 +outsourced to \textit{auto} by passing the option \textit{check\_potential}. For
1.463 +example:
1.464 +
1.465 +\prew
1.466 +\textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
1.467 +\textbf{nitpick} [\textit{card~nat}~= 100,\, \textit{check\_potential}] \\[2\smallskipamount]
1.468 +\slshape Nitpick found a potential counterexample: \\[2\smallskipamount]
1.469 +\hbox{}\qquad Free variable: \nopagebreak \\
1.470 +\hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
1.471 +Confirmation by ``\textit{auto}'': The above counterexample is genuine.
1.472 +\postw
1.473 +
1.474 +You might wonder why the counterexample is first reported as potential. The root
1.475 +of the problem is that the bound variable in $\forall n.\; \textit{Suc}~n
1.476 +\mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds an $n$ such
1.477 +that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
1.478 +\textit{False}; but otherwise, it does not know anything about values of $n \ge
1.479 +\textit{card~nat}$ and must therefore evaluate the assumption to $\unk$, not
1.480 +\textit{True}. Since the assumption can never be satisfied, the putative lemma
1.481 +can never be falsified.
1.482 +
1.483 +Incidentally, if you distrust the so-called genuine counterexamples, you can
1.484 +enable \textit{check\_\allowbreak genuine} to verify them as well. However, be
1.485 +aware that \textit{auto} will often fail to prove that the counterexample is
1.486 +genuine or spurious.
1.487 +
1.488 +Some conjectures involving elementary number theory make Nitpick look like a
1.489 +giant with feet of clay:
1.490 +
1.491 +\prew
1.492 +\textbf{lemma} ``$P~\textit{Suc}$'' \\
1.493 +\textbf{nitpick} [\textit{card} = 1--6] \\[2\smallskipamount]
1.494 +\slshape
1.495 +Nitpick found no counterexample.
1.496 +\postw
1.497 +
1.498 +For any cardinality $k$, \textit{Suc} is the partial function $\{0 \mapsto 1,\,
1.499 +1 \mapsto 2,\, \ldots,\, k - 1 \mapsto \unk\}$, which evaluates to $\unk$ when
1.500 +it is passed as argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$.
1.501 +The next example is similar:
1.502 +
1.503 +\prew
1.504 +\textbf{lemma} ``$P~(\textit{op}~{+}\Colon
1.505 +\textit{nat}\mathbin{\Rightarrow}\textit{nat}\mathbin{\Rightarrow}\textit{nat})$'' \\
1.506 +\textbf{nitpick} [\textit{card nat} = 1] \\[2\smallskipamount]
1.507 +{\slshape Nitpick found a counterexample:} \\[2\smallskipamount]
1.508 +\hbox{}\qquad Free variable: \nopagebreak \\
1.509 +\hbox{}\qquad\qquad $P = \{\}$ \\[2\smallskipamount]
1.510 +\textbf{nitpick} [\textit{card nat} = 2] \\[2\smallskipamount]
1.511 +{\slshape Nitpick found no counterexample.}
1.512 +\postw
1.513 +
1.514 +The problem here is that \textit{op}~+ is total when \textit{nat} is taken to be
1.515 +$\{0\}$ but becomes partial as soon as we add $1$, because $1 + 1 \notin \{0,
1.516 +1\}$.
1.517 +
1.518 +Because numbers are infinite and are approximated using a three-valued logic,
1.519 +there is usually no need to systematically enumerate domain sizes. If Nitpick
1.520 +cannot find a genuine counterexample for \textit{card~nat}~= $k$, it is very
1.521 +unlikely that one could be found for smaller domains. (The $P~(\textit{op}~{+})$
1.522 +example above is an exception to this principle.) Nitpick nonetheless enumerates
1.523 +all cardinalities from 1 to 8 for \textit{nat}, mainly because smaller
1.524 +cardinalities are fast to handle and give rise to simpler counterexamples. This
1.525 +is explained in more detail in \S\ref{scope-monotonicity}.
1.526 +
1.527 +\subsection{Inductive Datatypes}
1.528 +\label{inductive-datatypes}
1.529 +
1.530 +Like natural numbers and integers, inductive datatypes with recursive
1.531 +constructors admit no finite models and must be approximated by a subterm-closed
1.532 +subset. For example, using a cardinality of 10 for ${'}a~\textit{list}$,
1.533 +Nitpick looks for all counterexamples that can be built using at most 10
1.534 +different lists.
1.535 +
1.536 +Let's see with an example involving \textit{hd} (which returns the first element
1.537 +of a list) and $@$ (which concatenates two lists):
1.538 +
1.539 +\prew
1.540 +\textbf{lemma} ``$\textit{hd}~(\textit{xs} \mathbin{@} [y, y]) = \textit{hd}~\textit{xs}$'' \\
1.541 +\textbf{nitpick} \\[2\smallskipamount]
1.542 +\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
1.543 +\hbox{}\qquad Free variables: \nopagebreak \\
1.544 +\hbox{}\qquad\qquad $\textit{xs} = []$ \\
1.545 +\hbox{}\qquad\qquad $\textit{y} = a_3$
1.546 +\postw
1.547 +
1.548 +To see why the counterexample is genuine, we enable \textit{show\_consts}
1.549 +and \textit{show\_\allowbreak datatypes}:
1.550 +
1.551 +\prew
1.552 +{\slshape Datatype:} \\
1.553 +\hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_3, a_3],\, [a_3],\, \unr\}$ \\
1.554 +{\slshape Constants:} \\
1.555 +\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_3, a_3],\> [a_3, a_3] := \unk,\> [a_3] := \unk)$ \\
1.556 +\hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_3, a_3] := a_3,\> [a_3] := a_3)$
1.557 +\postw
1.558 +
1.559 +Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value,
1.560 +including $a_2$.
1.561 +
1.562 +The second constant, $\lambda x_1.\; x_1 \mathbin{@} [y, y]$, is simply the
1.563 +append operator whose second argument is fixed to be $[y, y]$. Appending $[a_3,
1.564 +a_3]$ to $[a_3]$ would normally give $[a_3, a_3, a_3]$, but this value is not
1.565 +representable in the subset of $'a$~\textit{list} considered by Nitpick, which
1.566 +is shown under the ``Datatype'' heading; hence the result is $\unk$. Similarly,
1.567 +appending $[a_3, a_3]$ to itself gives $\unk$.
1.568 +
1.569 +Given \textit{card}~$'a = 3$ and \textit{card}~$'a~\textit{list} = 3$, Nitpick
1.570 +considers the following subsets:
1.571 +
1.572 +\kern-.5\smallskipamount %% TYPESETTING
1.573 +
1.574 +\prew
1.575 +\begin{multicols}{3}
1.576 +$\{[],\, [a_1],\, [a_2]\}$; \\
1.577 +$\{[],\, [a_1],\, [a_3]\}$; \\
1.578 +$\{[],\, [a_2],\, [a_3]\}$; \\
1.579 +$\{[],\, [a_1],\, [a_1, a_1]\}$; \\
1.580 +$\{[],\, [a_1],\, [a_2, a_1]\}$; \\
1.581 +$\{[],\, [a_1],\, [a_3, a_1]\}$; \\
1.582 +$\{[],\, [a_2],\, [a_1, a_2]\}$; \\
1.583 +$\{[],\, [a_2],\, [a_2, a_2]\}$; \\
1.584 +$\{[],\, [a_2],\, [a_3, a_2]\}$; \\
1.585 +$\{[],\, [a_3],\, [a_1, a_3]\}$; \\
1.586 +$\{[],\, [a_3],\, [a_2, a_3]\}$; \\
1.587 +$\{[],\, [a_3],\, [a_3, a_3]\}$.
1.588 +\end{multicols}
1.589 +\postw
1.590 +
1.591 +\kern-2\smallskipamount %% TYPESETTING
1.592 +
1.593 +All subterm-closed subsets of $'a~\textit{list}$ consisting of three values
1.594 +are listed and only those. As an example of a non-subterm-closed subset,
1.595 +consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_3]\}$, and observe
1.596 +that $[a_1, a_3]$ (i.e., $a_1 \mathbin{\#} [a_3]$) has $[a_3] \notin
1.597 +\mathcal{S}$ as a subterm.
1.598 +
1.599 +Here's another m\"ochtegern-lemma that Nitpick can refute without a blink:
1.600 +
1.601 +\prew
1.602 +\textbf{lemma} ``$\lbrakk \textit{length}~\textit{xs} = 1;\> \textit{length}~\textit{ys} = 1
1.603 +\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$''
1.604 +\\
1.605 +\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
1.606 +\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
1.607 +\hbox{}\qquad Free variables: \nopagebreak \\
1.608 +\hbox{}\qquad\qquad $\textit{xs} = [a_2]$ \\
1.609 +\hbox{}\qquad\qquad $\textit{ys} = [a_3]$ \\
1.610 +\hbox{}\qquad Datatypes: \\
1.611 +\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
1.612 +\hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_3],\, [a_2],\, \unr\}$
1.613 +\postw
1.614 +
1.615 +Because datatypes are approximated using a three-valued logic, there is usually
1.616 +no need to systematically enumerate cardinalities: If Nitpick cannot find a
1.617 +genuine counterexample for \textit{card}~$'a~\textit{list}$~= 10, it is very
1.618 +unlikely that one could be found for smaller cardinalities.
1.619 +
1.620 +\subsection{Typedefs, Records, Rationals, and Reals}
1.621 +\label{typedefs-records-rationals-and-reals}
1.622 +
1.623 +Nitpick generally treats types declared using \textbf{typedef} as datatypes
1.624 +whose single constructor is the corresponding \textit{Abs\_\kern.1ex} function.
1.625 +For example:
1.626 +
1.627 +\prew
1.628 +\textbf{typedef}~\textit{three} = ``$\{0\Colon\textit{nat},\, 1,\, 2\}$'' \\
1.629 +\textbf{by}~\textit{blast} \\[2\smallskipamount]
1.630 +\textbf{definition}~$A \mathbin{\Colon} \textit{three}$ \textbf{where} ``\kern-.1em$A \,\equiv\, \textit{Abs\_\allowbreak three}~0$'' \\
1.631 +\textbf{definition}~$B \mathbin{\Colon} \textit{three}$ \textbf{where} ``$B \,\equiv\, \textit{Abs\_three}~1$'' \\
1.632 +\textbf{definition}~$C \mathbin{\Colon} \textit{three}$ \textbf{where} ``$C \,\equiv\, \textit{Abs\_three}~2$'' \\[2\smallskipamount]
1.633 +\textbf{lemma} ``$\lbrakk P~A;\> P~B\rbrakk \,\Longrightarrow\, P~x$'' \\
1.634 +\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
1.635 +\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.636 +\hbox{}\qquad Free variables: \nopagebreak \\
1.637 +\hbox{}\qquad\qquad $P = \{\Abs{1},\, \Abs{0}\}$ \\
1.638 +\hbox{}\qquad\qquad $x = \Abs{2}$ \\
1.639 +\hbox{}\qquad Datatypes: \\
1.640 +\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
1.641 +\hbox{}\qquad\qquad $\textit{three} = \{\Abs{2},\, \Abs{1},\, \Abs{0},\, \unr\}$
1.642 +\postw
1.643 +
1.644 +%% MARK
1.645 +In the output above, $\Abs{n}$ abbreviates $\textit{Abs\_three}~n$.
1.646 +
1.647 +%% MARK
1.648 +Records, which are implemented as \textbf{typedef}s behind the scenes, are
1.649 +handled in much the same way:
1.650 +
1.651 +\prew
1.652 +\textbf{record} \textit{point} = \\
1.653 +\hbox{}\quad $\textit{Xcoord} \mathbin{\Colon} \textit{int}$ \\
1.654 +\hbox{}\quad $\textit{Ycoord} \mathbin{\Colon} \textit{int}$ \\[2\smallskipamount]
1.655 +\textbf{lemma} ``$\textit{Xcoord}~(p\Colon\textit{point}) = \textit{Xcoord}~(q\Colon\textit{point})$'' \\
1.656 +\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
1.657 +\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.658 +\hbox{}\qquad Free variables: \nopagebreak \\
1.659 +\hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
1.660 +\hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
1.661 +\hbox{}\qquad Datatypes: \\
1.662 +\hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, \unr\}$ \\
1.663 +\hbox{}\qquad\qquad $\textit{point} = \{\lparr\textit{Xcoord} = 1,\>
1.664 +\textit{Ycoord} = 1\rparr,\> \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr,\, \unr\}$\kern-1pt %% QUIET
1.665 +\postw
1.666 +
1.667 +Finally, Nitpick provides rudimentary support for rationals and reals using a
1.668 +similar approach:
1.669 +
1.670 +\prew
1.671 +\textbf{lemma} ``$4 * x + 3 * (y\Colon\textit{real}) \not= 1/2$'' \\
1.672 +\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
1.673 +\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.674 +\hbox{}\qquad Free variables: \nopagebreak \\
1.675 +\hbox{}\qquad\qquad $x = 1/2$ \\
1.676 +\hbox{}\qquad\qquad $y = -1/2$ \\
1.677 +\hbox{}\qquad Datatypes: \\
1.678 +\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, 3,\, 4,\, 5,\, 6,\, 7,\, \unr\}$ \\
1.679 +\hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, 2,\, 3,\, 4,\, -3,\, -2,\, -1,\, \unr\}$ \\
1.680 +\hbox{}\qquad\qquad $\textit{real} = \{1,\, 0,\, 4,\, -3/2,\, 3,\, 2,\, 1/2,\, -1/2,\, \unr\}$
1.681 +\postw
1.682 +
1.683 +\subsection{Inductive and Coinductive Predicates}
1.684 +\label{inductive-and-coinductive-predicates}
1.685 +
1.686 +Inductively defined predicates (and sets) are particularly problematic for
1.687 +counterexample generators. They can make Quickcheck~\cite{berghofer-nipkow-2004}
1.688 +loop forever and Refute~\cite{weber-2008} run out of resources. The crux of
1.689 +the problem is that they are defined using a least fixed point construction.
1.690 +
1.691 +Nitpick's philosophy is that not all inductive predicates are equal. Consider
1.692 +the \textit{even} predicate below:
1.693 +
1.694 +\prew
1.695 +\textbf{inductive}~\textit{even}~\textbf{where} \\
1.696 +``\textit{even}~0'' $\,\mid$ \\
1.697 +``\textit{even}~$n\,\Longrightarrow\, \textit{even}~(\textit{Suc}~(\textit{Suc}~n))$''
1.698 +\postw
1.699 +
1.700 +This predicate enjoys the desirable property of being well-founded, which means
1.701 +that the introduction rules don't give rise to infinite chains of the form
1.702 +
1.703 +\prew
1.704 +$\cdots\,\Longrightarrow\, \textit{even}~k''
1.705 + \,\Longrightarrow\, \textit{even}~k'
1.706 + \,\Longrightarrow\, \textit{even}~k.$
1.707 +\postw
1.708 +
1.709 +For \textit{even}, this is obvious: Any chain ending at $k$ will be of length
1.710 +$k/2 + 1$:
1.711 +
1.712 +\prew
1.713 +$\textit{even}~0\,\Longrightarrow\, \textit{even}~2\,\Longrightarrow\, \cdots
1.714 + \,\Longrightarrow\, \textit{even}~(k - 2)
1.715 + \,\Longrightarrow\, \textit{even}~k.$
1.716 +\postw
1.717 +
1.718 +Wellfoundedness is desirable because it enables Nitpick to use a very efficient
1.719 +fixed point computation.%
1.720 +\footnote{If an inductive predicate is
1.721 +well-founded, then it has exactly one fixed point, which is simultaneously the
1.722 +least and the greatest fixed point. In these circumstances, the computation of
1.723 +the least fixed point amounts to the computation of an arbitrary fixed point,
1.724 +which can be performed using a straightforward recursive equation.}
1.725 +Moreover, Nitpick can prove wellfoundedness of most well-founded predicates,
1.726 +just as Isabelle's \textbf{function} package usually discharges termination
1.727 +proof obligations automatically.
1.728 +
1.729 +Let's try an example:
1.730 +
1.731 +\prew
1.732 +\textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
1.733 +\textbf{nitpick}~[\textit{card nat}~= 100,\, \textit{verbose}] \\[2\smallskipamount]
1.734 +\slshape The inductive predicate ``\textit{even}'' was proved well-founded.
1.735 +Nitpick can compute it efficiently. \\[2\smallskipamount]
1.736 +Trying 1 scope: \\
1.737 +\hbox{}\qquad \textit{card nat}~= 100. \\[2\smallskipamount]
1.738 +Nitpick found a potential counterexample for \textit{card nat}~= 100: \\[2\smallskipamount]
1.739 +\hbox{}\qquad Empty assignment \\[2\smallskipamount]
1.740 +Nitpick could not find a better counterexample. \\[2\smallskipamount]
1.741 +Total time: 2274 ms.
1.742 +\postw
1.743 +
1.744 +No genuine counterexample is possible because Nitpick cannot rule out the
1.745 +existence of a natural number $n \ge 100$ such that both $\textit{even}~n$ and
1.746 +$\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the
1.747 +existential quantifier:
1.748 +
1.749 +\prew
1.750 +\textbf{lemma} ``$\exists n \mathbin{\le} 99.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
1.751 +\textbf{nitpick}~[\textit{card nat}~= 100] \\[2\smallskipamount]
1.752 +\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.753 +\hbox{}\qquad Empty assignment
1.754 +\postw
1.755 +
1.756 +So far we were blessed by the wellfoundedness of \textit{even}. What happens if
1.757 +we use the following definition instead?
1.758 +
1.759 +\prew
1.760 +\textbf{inductive} $\textit{even}'$ \textbf{where} \\
1.761 +``$\textit{even}'~(0{\Colon}\textit{nat})$'' $\,\mid$ \\
1.762 +``$\textit{even}'~2$'' $\,\mid$ \\
1.763 +``$\lbrakk\textit{even}'~m;\> \textit{even}'~n\rbrakk \,\Longrightarrow\, \textit{even}'~(m + n)$''
1.764 +\postw
1.765 +
1.766 +This definition is not well-founded: From $\textit{even}'~0$ and
1.767 +$\textit{even}'~0$, we can derive that $\textit{even}'~0$. Nonetheless, the
1.768 +predicates $\textit{even}$ and $\textit{even}'$ are equivalent.
1.769 +
1.770 +Let's check a property involving $\textit{even}'$. To make up for the
1.771 +foreseeable computational hurdles entailed by non-wellfoundedness, we decrease
1.772 +\textit{nat}'s cardinality to a mere 10:
1.773 +
1.774 +\prew
1.775 +\textbf{lemma}~``$\exists n \in \{0, 2, 4, 6, 8\}.\;
1.776 +\lnot\;\textit{even}'~n$'' \\
1.777 +\textbf{nitpick}~[\textit{card nat}~= 10,\, \textit{verbose},\, \textit{show\_consts}] \\[2\smallskipamount]
1.778 +\slshape
1.779 +The inductive predicate ``$\textit{even}'\!$'' could not be proved well-founded.
1.780 +Nitpick might need to unroll it. \\[2\smallskipamount]
1.781 +Trying 6 scopes: \\
1.782 +\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 0; \\
1.783 +\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 1; \\
1.784 +\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2; \\
1.785 +\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 4; \\
1.786 +\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 8; \\
1.787 +\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 9. \\[2\smallskipamount]
1.788 +Nitpick found a counterexample for \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2: \\[2\smallskipamount]
1.789 +\hbox{}\qquad Constant: \nopagebreak \\
1.790 +\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t]
1.791 +& 2 := \{0, 2, 4, 6, 8, 1^\Q, 3^\Q, 5^\Q, 7^\Q, 9^\Q\}, \\[-2pt]
1.792 +& 1 := \{0, 2, 4, 1^\Q, 3^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\}, \\[-2pt]
1.793 +& 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\[2\smallskipamount]
1.794 +Total time: 1140 ms.
1.795 +\postw
1.796 +
1.797 +Nitpick's output is very instructive. First, it tells us that the predicate is
1.798 +unrolled, meaning that it is computed iteratively from the empty set. Then it
1.799 +lists six scopes specifying different bounds on the numbers of iterations:\ 0,
1.800 +1, 2, 4, 8, and~9.
1.801 +
1.802 +The output also shows how each iteration contributes to $\textit{even}'$. The
1.803 +notation $\lambda i.\; \textit{even}'$ indicates that the value of the
1.804 +predicate depends on an iteration counter. Iteration 0 provides the basis
1.805 +elements, $0$ and $2$. Iteration 1 contributes $4$ ($= 2 + 2$). Iteration 2
1.806 +throws $6$ ($= 2 + 4 = 4 + 2$) and $8$ ($= 4 + 4$) into the mix. Further
1.807 +iterations would not contribute any new elements.
1.808 +
1.809 +Some values are marked with superscripted question
1.810 +marks~(`\lower.2ex\hbox{$^\Q$}'). These are the elements for which the
1.811 +predicate evaluates to $\unk$. Thus, $\textit{even}'$ evaluates to either
1.812 +\textit{True} or $\unk$, never \textit{False}.
1.813 +
1.814 +When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, and 24
1.815 +iterations. However, these numbers are bounded by the cardinality of the
1.816 +predicate's domain. With \textit{card~nat}~= 10, no more than 9 iterations are
1.817 +ever needed to compute the value of a \textit{nat} predicate. You can specify
1.818 +the number of iterations using the \textit{iter} option, as explained in
1.819 +\S\ref{scope-of-search}.
1.820 +
1.821 +In the next formula, $\textit{even}'$ occurs both positively and negatively:
1.822 +
1.823 +\prew
1.824 +\textbf{lemma} ``$\textit{even}'~(n - 2) \,\Longrightarrow\, \textit{even}'~n$'' \\
1.825 +\textbf{nitpick} [\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
1.826 +\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.827 +\hbox{}\qquad Free variable: \nopagebreak \\
1.828 +\hbox{}\qquad\qquad $n = 1$ \\
1.829 +\hbox{}\qquad Constants: \nopagebreak \\
1.830 +\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t]
1.831 +& 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\
1.832 +\hbox{}\qquad\qquad $\textit{even}' \subseteq \{0, 2, 4, 6, 8, \unr\}$
1.833 +\postw
1.834 +
1.835 +Notice the special constraint $\textit{even}' \subseteq \{0,\, 2,\, 4,\, 6,\,
1.836 +8,\, \unr\}$ in the output, whose right-hand side represents an arbitrary
1.837 +fixed point (not necessarily the least one). It is used to falsify
1.838 +$\textit{even}'~n$. In contrast, the unrolled predicate is used to satisfy
1.839 +$\textit{even}'~(n - 2)$.
1.840 +
1.841 +Coinductive predicates are handled dually. For example:
1.842 +
1.843 +\prew
1.844 +\textbf{coinductive} \textit{nats} \textbf{where} \\
1.845 +``$\textit{nats}~(x\Colon\textit{nat}) \,\Longrightarrow\, \textit{nats}~x$'' \\[2\smallskipamount]
1.846 +\textbf{lemma} ``$\textit{nats} = \{0, 1, 2, 3, 4\}$'' \\
1.847 +\textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
1.848 +\slshape Nitpick found a counterexample:
1.849 +\\[2\smallskipamount]
1.850 +\hbox{}\qquad Constants: \nopagebreak \\
1.851 +\hbox{}\qquad\qquad $\lambda i.\; \textit{nats} = \undef(0 := \{\!\begin{aligned}[t]
1.852 +& 0^\Q, 1^\Q, 2^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q, \\[-2pt]
1.853 +& \unr\})\end{aligned}$ \\
1.854 +\hbox{}\qquad\qquad $nats \supseteq \{9, 5^\Q, 6^\Q, 7^\Q, 8^\Q, \unr\}$
1.855 +\postw
1.856 +
1.857 +As a special case, Nitpick uses Kodkod's transitive closure operator to encode
1.858 +negative occurrences of non-well-founded ``linear inductive predicates,'' i.e.,
1.859 +inductive predicates for which each the predicate occurs in at most one
1.860 +assumption of each introduction rule. For example:
1.861 +
1.862 +\prew
1.863 +\textbf{inductive} \textit{odd} \textbf{where} \\
1.864 +``$\textit{odd}~1$'' $\,\mid$ \\
1.865 +``$\lbrakk \textit{odd}~m;\>\, \textit{even}~n\rbrakk \,\Longrightarrow\, \textit{odd}~(m + n)$'' \\[2\smallskipamount]
1.866 +\textbf{lemma}~``$\textit{odd}~n \,\Longrightarrow\, \textit{odd}~(n - 2)$'' \\
1.867 +\textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
1.868 +\slshape Nitpick found a counterexample:
1.869 +\\[2\smallskipamount]
1.870 +\hbox{}\qquad Free variable: \nopagebreak \\
1.871 +\hbox{}\qquad\qquad $n = 1$ \\
1.872 +\hbox{}\qquad Constants: \nopagebreak \\
1.873 +\hbox{}\qquad\qquad $\textit{even} = \{0, 2, 4, 6, 8, \unr\}$ \\
1.874 +\hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = \{1, \unr\}$ \\
1.875 +\hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \!
1.876 +\!\begin{aligned}[t]
1.877 + & \{(0, 0), (0, 2), (0, 4), (0, 6), (0, 8), (1, 1), (1, 3), (1, 5), \\[-2pt]
1.878 + & \phantom{\{} (1, 7), (1, 9), (2, 2), (2, 4), (2, 6), (2, 8), (3, 3),
1.879 + (3, 5), \\[-2pt]
1.880 + & \phantom{\{} (3, 7), (3, 9), (4, 4), (4, 6), (4, 8), (5, 5), (5, 7), (5, 9), \\[-2pt]
1.881 + & \phantom{\{} (6, 6), (6, 8), (7, 7), (7, 9), (8, 8), (9, 9), \unr\}\end{aligned}$ \\
1.882 +\hbox{}\qquad\qquad $\textit{odd} \subseteq \{1, 3, 5, 7, 9, 8^\Q, \unr\}$
1.883 +\postw
1.884 +
1.885 +\noindent
1.886 +In the output, $\textit{odd}_{\textrm{base}}$ represents the base elements and
1.887 +$\textit{odd}_{\textrm{step}}$ is a transition relation that computes new
1.888 +elements from known ones. The set $\textit{odd}$ consists of all the values
1.889 +reachable through the reflexive transitive closure of
1.890 +$\textit{odd}_{\textrm{step}}$ starting with any element from
1.891 +$\textit{odd}_{\textrm{base}}$, namely 1, 3, 5, 7, and 9. Using Kodkod's
1.892 +transitive closure to encode linear predicates is normally either more thorough
1.893 +or more efficient than unrolling (depending on the value of \textit{iter}), but
1.894 +for those cases where it isn't you can disable it by passing the
1.895 +\textit{dont\_star\_linear\_preds} option.
1.896 +
1.897 +\subsection{Coinductive Datatypes}
1.898 +\label{coinductive-datatypes}
1.899 +
1.900 +While Isabelle regrettably lacks a high-level mechanism for defining coinductive
1.901 +datatypes, the \textit{Coinductive\_List} theory provides a coinductive ``lazy
1.902 +list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick supports
1.903 +these lazy lists seamlessly and provides a hook, described in
1.904 +\S\ref{registration-of-coinductive-datatypes}, to register custom coinductive
1.905 +datatypes.
1.906 +
1.907 +(Co)intuitively, a coinductive datatype is similar to an inductive datatype but
1.908 +allows infinite objects. Thus, the infinite lists $\textit{ps}$ $=$ $[a, a, a,
1.909 +\ldots]$, $\textit{qs}$ $=$ $[a, b, a, b, \ldots]$, and $\textit{rs}$ $=$ $[0,
1.910 +1, 2, 3, \ldots]$ can be defined as lazy lists using the
1.911 +$\textit{LNil}\mathbin{\Colon}{'}a~\textit{llist}$ and
1.912 +$\textit{LCons}\mathbin{\Colon}{'}a \mathbin{\Rightarrow} {'}a~\textit{llist}
1.913 +\mathbin{\Rightarrow} {'}a~\textit{llist}$ constructors.
1.914 +
1.915 +Although it is otherwise no friend of infinity, Nitpick can find counterexamples
1.916 +involving cyclic lists such as \textit{ps} and \textit{qs} above as well as
1.917 +finite lists:
1.918 +
1.919 +\prew
1.920 +\textbf{lemma} ``$\textit{xs} \not= \textit{LCons}~a~\textit{xs}$'' \\
1.921 +\textbf{nitpick} \\[2\smallskipamount]
1.922 +\slshape Nitpick found a counterexample for {\itshape card}~$'a$ = 1: \\[2\smallskipamount]
1.923 +\hbox{}\qquad Free variables: \nopagebreak \\
1.924 +\hbox{}\qquad\qquad $\textit{a} = a_1$ \\
1.925 +\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$
1.926 +\postw
1.927 +
1.928 +The notation $\textrm{THE}~\omega.\; \omega = t(\omega)$ stands
1.929 +for the infinite term $t(t(t(\ldots)))$. Hence, \textit{xs} is simply the
1.930 +infinite list $[a_1, a_1, a_1, \ldots]$.
1.931 +
1.932 +The next example is more interesting:
1.933 +
1.934 +\prew
1.935 +\textbf{lemma}~``$\lbrakk\textit{xs} = \textit{LCons}~a~\textit{xs};\>\,
1.936 +\textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
1.937 +\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
1.938 +\slshape The type ``\kern1pt$'a$'' passed the monotonicity test. Nitpick might be able to skip
1.939 +some scopes. \\[2\smallskipamount]
1.940 +Trying 8 scopes: \\
1.941 +\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list}$''~= 1,
1.942 +and \textit{bisim\_depth}~= 0. \\
1.943 +\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1.944 +\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} ``\kern1pt$'a~\textit{list}$''~= 8,
1.945 +and \textit{bisim\_depth}~= 7. \\[2\smallskipamount]
1.946 +Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
1.947 +\textit{card}~``\kern1pt$'a~\textit{list}$''~= 2, and \textit{bisim\_\allowbreak
1.948 +depth}~= 1:
1.949 +\\[2\smallskipamount]
1.950 +\hbox{}\qquad Free variables: \nopagebreak \\
1.951 +\hbox{}\qquad\qquad $\textit{a} = a_2$ \\
1.952 +\hbox{}\qquad\qquad $\textit{b} = a_1$ \\
1.953 +\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega$ \\
1.954 +\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_1~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega)$ \\[2\smallskipamount]
1.955 +Total time: 726 ms.
1.956 +\postw
1.957 +
1.958 +The lazy list $\textit{xs}$ is simply $[a_2, a_2, a_2, \ldots]$, whereas
1.959 +$\textit{ys}$ is $[a_1, a_2, a_2, a_2, \ldots]$, i.e., a lasso-shaped list with
1.960 +$[a_1]$ as its stem and $[a_2]$ as its cycle. In general, the list segment
1.961 +within the scope of the {THE} binder corresponds to the lasso's cycle, whereas
1.962 +the segment leading to the binder is the stem.
1.963 +
1.964 +A salient property of coinductive datatypes is that two objects are considered
1.965 +equal if and only if they lead to the same observations. For example, the lazy
1.966 +lists $\textrm{THE}~\omega.\; \omega =
1.967 +\textit{LCons}~a~(\textit{LCons}~b~\omega)$ and
1.968 +$\textit{LCons}~a~(\textrm{THE}~\omega.\; \omega =
1.969 +\textit{LCons}~b~(\textit{LCons}~a~\omega))$ are identical, because both lead
1.970 +to the sequence of observations $a$, $b$, $a$, $b$, \hbox{\ldots} (or,
1.971 +equivalently, both encode the infinite list $[a, b, a, b, \ldots]$). This
1.972 +concept of equality for coinductive datatypes is called bisimulation and is
1.973 +defined coinductively.
1.974 +
1.975 +Internally, Nitpick encodes the coinductive bisimilarity predicate as part of
1.976 +the Kodkod problem to ensure that distinct objects lead to different
1.977 +observations. This precaution is somewhat expensive and often unnecessary, so it
1.978 +can be disabled by setting the \textit{bisim\_depth} option to $-1$. The
1.979 +bisimilarity check is then performed \textsl{after} the counterexample has been
1.980 +found to ensure correctness. If this after-the-fact check fails, the
1.981 +counterexample is tagged as ``likely genuine'' and Nitpick recommends to try
1.982 +again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the
1.983 +check for the previous example saves approximately 150~milli\-seconds; the speed
1.984 +gains can be more significant for larger scopes.
1.985 +
1.986 +The next formula illustrates the need for bisimilarity (either as a Kodkod
1.987 +predicate or as an after-the-fact check) to prevent spurious counterexamples:
1.988 +
1.989 +\prew
1.990 +\textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
1.991 +\,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
1.992 +\textbf{nitpick} [\textit{bisim\_depth} = $-1$,\, \textit{show\_datatypes}] \\[2\smallskipamount]
1.993 +\slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
1.994 +\hbox{}\qquad Free variables: \nopagebreak \\
1.995 +\hbox{}\qquad\qquad $a = a_2$ \\
1.996 +\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
1.997 +\textit{LCons}~a_2~\omega$ \\
1.998 +\hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega$ \\
1.999 +\hbox{}\qquad Codatatype:\strut \nopagebreak \\
1.1000 +\hbox{}\qquad\qquad $'a~\textit{llist} =
1.1001 +\{\!\begin{aligned}[t]
1.1002 + & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega, \\[-2pt]
1.1003 + & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega,\> \unr\}\end{aligned}$
1.1004 +\\[2\smallskipamount]
1.1005 +Try again with ``\textit{bisim\_depth}'' set to a nonnegative value to confirm
1.1006 +that the counterexample is genuine. \\[2\smallskipamount]
1.1007 +{\upshape\textbf{nitpick}} \\[2\smallskipamount]
1.1008 +\slshape Nitpick found no counterexample.
1.1009 +\postw
1.1010 +
1.1011 +In the first \textbf{nitpick} invocation, the after-the-fact check discovered
1.1012 +that the two known elements of type $'a~\textit{llist}$ are bisimilar.
1.1013 +
1.1014 +A compromise between leaving out the bisimilarity predicate from the Kodkod
1.1015 +problem and performing the after-the-fact check is to specify a lower
1.1016 +nonnegative \textit{bisim\_depth} value than the default one provided by
1.1017 +Nitpick. In general, a value of $K$ means that Nitpick will require all lists to
1.1018 +be distinguished from each other by their prefixes of length $K$. Be aware that
1.1019 +setting $K$ to a too low value can overconstrain Nitpick, preventing it from
1.1020 +finding any counterexamples.
1.1021 +
1.1022 +\subsection{Boxing}
1.1023 +\label{boxing}
1.1024 +
1.1025 +Nitpick normally maps function and product types directly to the corresponding
1.1026 +Kodkod concepts. As a consequence, if $'a$ has cardinality 3 and $'b$ has
1.1027 +cardinality 4, then $'a \times {'}b$ has cardinality 12 ($= 4 \times 3$) and $'a
1.1028 +\Rightarrow {'}b$ has cardinality 64 ($= 4^3$). In some circumstances, it pays
1.1029 +off to treat these types in the same way as plain datatypes, by approximating
1.1030 +them by a subset of a given cardinality. This technique is called ``boxing'' and
1.1031 +is particularly useful for functions passed as arguments to other functions, for
1.1032 +high-arity functions, and for large tuples. Under the hood, boxing involves
1.1033 +wrapping occurrences of the types $'a \times {'}b$ and $'a \Rightarrow {'}b$ in
1.1034 +isomorphic datatypes, as can be seen by enabling the \textit{debug} option.
1.1035 +
1.1036 +To illustrate boxing, we consider a formalization of $\lambda$-terms represented
1.1037 +using de Bruijn's notation:
1.1038 +
1.1039 +\prew
1.1040 +\textbf{datatype} \textit{tm} = \textit{Var}~\textit{nat}~$\mid$~\textit{Lam}~\textit{tm} $\mid$ \textit{App~tm~tm}
1.1041 +\postw
1.1042 +
1.1043 +The $\textit{lift}~t~k$ function increments all variables with indices greater
1.1044 +than or equal to $k$ by one:
1.1045 +
1.1046 +\prew
1.1047 +\textbf{primrec} \textit{lift} \textbf{where} \\
1.1048 +``$\textit{lift}~(\textit{Var}~j)~k = \textit{Var}~(\textrm{if}~j < k~\textrm{then}~j~\textrm{else}~j + 1)$'' $\mid$ \\
1.1049 +``$\textit{lift}~(\textit{Lam}~t)~k = \textit{Lam}~(\textit{lift}~t~(k + 1))$'' $\mid$ \\
1.1050 +``$\textit{lift}~(\textit{App}~t~u)~k = \textit{App}~(\textit{lift}~t~k)~(\textit{lift}~u~k)$''
1.1051 +\postw
1.1052 +
1.1053 +The $\textit{loose}~t~k$ predicate returns \textit{True} if and only if
1.1054 +term $t$ has a loose variable with index $k$ or more:
1.1055 +
1.1056 +\prew
1.1057 +\textbf{primrec}~\textit{loose} \textbf{where} \\
1.1058 +``$\textit{loose}~(\textit{Var}~j)~k = (j \ge k)$'' $\mid$ \\
1.1059 +``$\textit{loose}~(\textit{Lam}~t)~k = \textit{loose}~t~(\textit{Suc}~k)$'' $\mid$ \\
1.1060 +``$\textit{loose}~(\textit{App}~t~u)~k = (\textit{loose}~t~k \mathrel{\lor} \textit{loose}~u~k)$''
1.1061 +\postw
1.1062 +
1.1063 +Next, the $\textit{subst}~\sigma~t$ function applies the substitution $\sigma$
1.1064 +on $t$:
1.1065 +
1.1066 +\prew
1.1067 +\textbf{primrec}~\textit{subst} \textbf{where} \\
1.1068 +``$\textit{subst}~\sigma~(\textit{Var}~j) = \sigma~j$'' $\mid$ \\
1.1069 +``$\textit{subst}~\sigma~(\textit{Lam}~t) = {}$\phantom{''} \\
1.1070 +\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$ \\
1.1071 +``$\textit{subst}~\sigma~(\textit{App}~t~u) = \textit{App}~(\textit{subst}~\sigma~t)~(\textit{subst}~\sigma~u)$''
1.1072 +\postw
1.1073 +
1.1074 +A substitution is a function that maps variable indices to terms. Observe that
1.1075 +$\sigma$ is a function passed as argument and that Nitpick can't optimize it
1.1076 +away, because the recursive call for the \textit{Lam} case involves an altered
1.1077 +version. Also notice the \textit{lift} call, which increments the variable
1.1078 +indices when moving under a \textit{Lam}.
1.1079 +
1.1080 +A reasonable property to expect of substitution is that it should leave closed
1.1081 +terms unchanged. Alas, even this simple property does not hold:
1.1082 +
1.1083 +\pre
1.1084 +\textbf{lemma}~``$\lnot\,\textit{loose}~t~0 \,\Longrightarrow\, \textit{subst}~\sigma~t = t$'' \\
1.1085 +\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
1.1086 +\slshape
1.1087 +Trying 8 scopes: \nopagebreak \\
1.1088 +\hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 1; \\
1.1089 +\hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 2; \\
1.1090 +\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1.1091 +\hbox{}\qquad \textit{card~nat}~= 8, \textit{card tm}~= 8, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 8. \\[2\smallskipamount]
1.1092 +Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6,
1.1093 +and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm}$''~= 6: \\[2\smallskipamount]
1.1094 +\hbox{}\qquad Free variables: \nopagebreak \\
1.1095 +\hbox{}\qquad\qquad $\sigma = \undef(\!\begin{aligned}[t]
1.1096 +& 0 := \textit{Var}~0,\>
1.1097 + 1 := \textit{Var}~0,\>
1.1098 + 2 := \textit{Var}~0, \\[-2pt]
1.1099 +& 3 := \textit{Var}~0,\>
1.1100 + 4 := \textit{Var}~0,\>
1.1101 + 5 := \textit{Var}~0)\end{aligned}$ \\
1.1102 +\hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount]
1.1103 +Total time: $4679$ ms.
1.1104 +\postw
1.1105 +
1.1106 +Using \textit{eval}, we find out that $\textit{subst}~\sigma~t =
1.1107 +\textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional
1.1108 +$\lambda$-term notation, $t$~is
1.1109 +$\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is $\lambda x\, y.\> y$.
1.1110 +The bug is in \textit{subst}: The $\textit{lift}~(\sigma~m)~1$ call should be
1.1111 +replaced with $\textit{lift}~(\sigma~m)~0$.
1.1112 +
1.1113 +An interesting aspect of Nitpick's verbose output is that it assigned inceasing
1.1114 +cardinalities from 1 to 8 to the type $\textit{nat} \Rightarrow \textit{tm}$.
1.1115 +For the formula of interest, knowing 6 values of that type was enough to find
1.1116 +the counterexample. Without boxing, $46\,656$ ($= 6^6$) values must be
1.1117 +considered, a hopeless undertaking:
1.1118 +
1.1119 +\prew
1.1120 +\textbf{nitpick} [\textit{dont\_box}] \\[2\smallskipamount]
1.1121 +{\slshape Nitpick ran out of time after checking 4 of 8 scopes.}
1.1122 +\postw
1.1123 +
1.1124 +{\looseness=-1
1.1125 +Boxing can be enabled or disabled globally or on a per-type basis using the
1.1126 +\textit{box} option. Moreover, setting the cardinality of a function or
1.1127 +product type implicitly enables boxing for that type. Nitpick usually performs
1.1128 +reasonable choices about which types should be boxed, but option tweaking
1.1129 +sometimes helps.
1.1130 +
1.1131 +}
1.1132 +
1.1133 +\subsection{Scope Monotonicity}
1.1134 +\label{scope-monotonicity}
1.1135 +
1.1136 +The \textit{card} option (together with \textit{iter}, \textit{bisim\_depth},
1.1137 +and \textit{max}) controls which scopes are actually tested. In general, to
1.1138 +exhaust all models below a certain cardinality bound, the number of scopes that
1.1139 +Nitpick must consider increases exponentially with the number of type variables
1.1140 +(and \textbf{typedecl}'d types) occurring in the formula. Given the default
1.1141 +cardinality specification of 1--8, no fewer than $8^4 = 4096$ scopes must be
1.1142 +considered for a formula involving $'a$, $'b$, $'c$, and $'d$.
1.1143 +
1.1144 +Fortunately, many formulas exhibit a property called \textsl{scope
1.1145 +monotonicity}, meaning that if the formula is falsifiable for a given scope,
1.1146 +it is also falsifiable for all larger scopes \cite[p.~165]{jackson-2006}.
1.1147 +
1.1148 +Consider the formula
1.1149 +
1.1150 +\prew
1.1151 +\textbf{lemma}~``$\textit{length~xs} = \textit{length~ys} \,\Longrightarrow\, \textit{rev}~(\textit{zip~xs~ys}) = \textit{zip~xs}~(\textit{rev~ys})$''
1.1152 +\postw
1.1153 +
1.1154 +where \textit{xs} is of type $'a~\textit{list}$ and \textit{ys} is of type
1.1155 +$'b~\textit{list}$. A priori, Nitpick would need to consider 512 scopes to
1.1156 +exhaust the specification \textit{card}~= 1--8. However, our intuition tells us
1.1157 +that any counterexample found with a small scope would still be a counterexample
1.1158 +in a larger scope---by simply ignoring the fresh $'a$ and $'b$ values provided
1.1159 +by the larger scope. Nitpick comes to the same conclusion after a careful
1.1160 +inspection of the formula and the relevant definitions:
1.1161 +
1.1162 +\prew
1.1163 +\textbf{nitpick}~[\textit{verbose}] \\[2\smallskipamount]
1.1164 +\slshape
1.1165 +The types ``\kern1pt$'a$'' and ``\kern1pt$'b$'' passed the monotonicity test.
1.1166 +Nitpick might be able to skip some scopes.
1.1167 + \\[2\smallskipamount]
1.1168 +Trying 8 scopes: \\
1.1169 +\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1,
1.1170 +\textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$
1.1171 +\textit{list}''~= 1, \\
1.1172 +\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 1, and
1.1173 +\textit{card} ``\kern1pt$'b$ \textit{list}''~= 1. \\
1.1174 +\hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2,
1.1175 +\textit{card} \textit{nat}~= 2, \textit{card} ``$('a \times {'}b)$
1.1176 +\textit{list}''~= 2, \\
1.1177 +\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 2, and
1.1178 +\textit{card} ``\kern1pt$'b$ \textit{list}''~= 2. \\
1.1179 +\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1.1180 +\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} $'b$~= 8,
1.1181 +\textit{card} \textit{nat}~= 8, \textit{card} ``$('a \times {'}b)$
1.1182 +\textit{list}''~= 8, \\
1.1183 +\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 8, and
1.1184 +\textit{card} ``\kern1pt$'b$ \textit{list}''~= 8.
1.1185 +\\[2\smallskipamount]
1.1186 +Nitpick found a counterexample for
1.1187 +\textit{card} $'a$~= 5, \textit{card} $'b$~= 5,
1.1188 +\textit{card} \textit{nat}~= 5, \textit{card} ``$('a \times {'}b)$
1.1189 +\textit{list}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list}''~= 5, and
1.1190 +\textit{card} ``\kern1pt$'b$ \textit{list}''~= 5:
1.1191 +\\[2\smallskipamount]
1.1192 +\hbox{}\qquad Free variables: \nopagebreak \\
1.1193 +\hbox{}\qquad\qquad $\textit{xs} = [a_4, a_5]$ \\
1.1194 +\hbox{}\qquad\qquad $\textit{ys} = [b_3, b_3]$ \\[2\smallskipamount]
1.1195 +Total time: 1636 ms.
1.1196 +\postw
1.1197 +
1.1198 +In theory, it should be sufficient to test a single scope:
1.1199 +
1.1200 +\prew
1.1201 +\textbf{nitpick}~[\textit{card}~= 8]
1.1202 +\postw
1.1203 +
1.1204 +However, this is often less efficient in practice and may lead to overly complex
1.1205 +counterexamples.
1.1206 +
1.1207 +If the monotonicity check fails but we believe that the formula is monotonic (or
1.1208 +we don't mind missing some counterexamples), we can pass the
1.1209 +\textit{mono} option. To convince yourself that this option is risky,
1.1210 +simply consider this example from \S\ref{skolemization}:
1.1211 +
1.1212 +\prew
1.1213 +\textbf{lemma} ``$\exists g.\; \forall x\Colon 'b.~g~(f~x) = x
1.1214 + \,\Longrightarrow\, \forall y\Colon {'}a.\; \exists x.~y = f~x$'' \\
1.1215 +\textbf{nitpick} [\textit{mono}] \\[2\smallskipamount]
1.1216 +{\slshape Nitpick found no counterexample.} \\[2\smallskipamount]
1.1217 +\textbf{nitpick} \\[2\smallskipamount]
1.1218 +\slshape
1.1219 +Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\
1.1220 +\hbox{}\qquad $\vdots$
1.1221 +\postw
1.1222 +
1.1223 +(It turns out the formula holds if and only if $\textit{card}~'a \le
1.1224 +\textit{card}~'b$.) Although this is rarely advisable, the automatic
1.1225 +monotonicity checks can be disabled by passing \textit{non\_mono}
1.1226 +(\S\ref{optimizations}).
1.1227 +
1.1228 +As insinuated in \S\ref{natural-numbers-and-integers} and
1.1229 +\S\ref{inductive-datatypes}, \textit{nat}, \textit{int}, and inductive datatypes
1.1230 +are normally monotonic and treated as such. The same is true for record types,
1.1231 +\textit{rat}, \textit{real}, and some \textbf{typedef}'d types. Thus, given the
1.1232 +cardinality specification 1--8, a formula involving \textit{nat}, \textit{int},
1.1233 +\textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
1.1234 +consider only 8~scopes instead of $32\,768$.
1.1235 +
1.1236 +\section{Case Studies}
1.1237 +\label{case-studies}
1.1238 +
1.1239 +As a didactic device, the previous section focused mostly on toy formulas whose
1.1240 +validity can easily be assessed just by looking at the formula. We will now
1.1241 +review two somewhat more realistic case studies that are within Nitpick's
1.1242 +reach:\ a context-free grammar modeled by mutually inductive sets and a
1.1243 +functional implementation of AA trees. The results presented in this
1.1244 +section were produced with the following settings:
1.1245 +
1.1246 +\prew
1.1247 +\textbf{nitpick\_params} [\textit{max\_potential}~= 0,\, \textit{max\_threads} = 2]
1.1248 +\postw
1.1249 +
1.1250 +\subsection{A Context-Free Grammar}
1.1251 +\label{a-context-free-grammar}
1.1252 +
1.1253 +Our first case study is taken from section 7.4 in the Isabelle tutorial
1.1254 +\cite{isa-tutorial}. The following grammar, originally due to Hopcroft and
1.1255 +Ullman, produces all strings with an equal number of $a$'s and $b$'s:
1.1256 +
1.1257 +\prew
1.1258 +\begin{tabular}{@{}r@{$\;\,$}c@{$\;\,$}l@{}}
1.1259 +$S$ & $::=$ & $\epsilon \mid bA \mid aB$ \\
1.1260 +$A$ & $::=$ & $aS \mid bAA$ \\
1.1261 +$B$ & $::=$ & $bS \mid aBB$
1.1262 +\end{tabular}
1.1263 +\postw
1.1264 +
1.1265 +The intuition behind the grammar is that $A$ generates all string with one more
1.1266 +$a$ than $b$'s and $B$ generates all strings with one more $b$ than $a$'s.
1.1267 +
1.1268 +The alphabet consists exclusively of $a$'s and $b$'s:
1.1269 +
1.1270 +\prew
1.1271 +\textbf{datatype} \textit{alphabet}~= $a$ $\mid$ $b$
1.1272 +\postw
1.1273 +
1.1274 +Strings over the alphabet are represented by \textit{alphabet list}s.
1.1275 +Nonterminals in the grammar become sets of strings. The production rules
1.1276 +presented above can be expressed as a mutually inductive definition:
1.1277 +
1.1278 +\prew
1.1279 +\textbf{inductive\_set} $S$ \textbf{and} $A$ \textbf{and} $B$ \textbf{where} \\
1.1280 +\textit{R1}:\kern.4em ``$[] \in S$'' $\,\mid$ \\
1.1281 +\textit{R2}:\kern.4em ``$w \in A\,\Longrightarrow\, b \mathbin{\#} w \in S$'' $\,\mid$ \\
1.1282 +\textit{R3}:\kern.4em ``$w \in B\,\Longrightarrow\, a \mathbin{\#} w \in S$'' $\,\mid$ \\
1.1283 +\textit{R4}:\kern.4em ``$w \in S\,\Longrightarrow\, a \mathbin{\#} w \in A$'' $\,\mid$ \\
1.1284 +\textit{R5}:\kern.4em ``$w \in S\,\Longrightarrow\, b \mathbin{\#} w \in S$'' $\,\mid$ \\
1.1285 +\textit{R6}:\kern.4em ``$\lbrakk v \in B;\> v \in B\rbrakk \,\Longrightarrow\, a \mathbin{\#} v \mathbin{@} w \in B$''
1.1286 +\postw
1.1287 +
1.1288 +The conversion of the grammar into the inductive definition was done manually by
1.1289 +Joe Blow, an underpaid undergraduate student. As a result, some errors might
1.1290 +have sneaked in.
1.1291 +
1.1292 +Debugging faulty specifications is at the heart of Nitpick's \textsl{raison
1.1293 +d'\^etre}. A good approach is to state desirable properties of the specification
1.1294 +(here, that $S$ is exactly the set of strings over $\{a, b\}$ with as many $a$'s
1.1295 +as $b$'s) and check them with Nitpick. If the properties are correctly stated,
1.1296 +counterexamples will point to bugs in the specification. For our grammar
1.1297 +example, we will proceed in two steps, separating the soundness and the
1.1298 +completeness of the set $S$. First, soundness:
1.1299 +
1.1300 +\prew
1.1301 +\textbf{theorem}~\textit{S\_sound}: \\
1.1302 +``$w \in S \longrightarrow \textit{length}~[x\mathbin{\leftarrow} w.\; x = a] =
1.1303 + \textit{length}~[x\mathbin{\leftarrow} w.\; x = b]$'' \\
1.1304 +\textbf{nitpick} \\[2\smallskipamount]
1.1305 +\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.1306 +\hbox{}\qquad Free variable: \nopagebreak \\
1.1307 +\hbox{}\qquad\qquad $w = [b]$
1.1308 +\postw
1.1309 +
1.1310 +It would seem that $[b] \in S$. How could this be? An inspection of the
1.1311 +introduction rules reveals that the only rule with a right-hand side of the form
1.1312 +$b \mathbin{\#} {\ldots} \in S$ that could have introduced $[b]$ into $S$ is
1.1313 +\textit{R5}:
1.1314 +
1.1315 +\prew
1.1316 +``$w \in S\,\Longrightarrow\, b \mathbin{\#} w \in S$''
1.1317 +\postw
1.1318 +
1.1319 +On closer inspection, we can see that this rule is wrong. To match the
1.1320 +production $B ::= bS$, the second $S$ should be a $B$. We fix the typo and try
1.1321 +again:
1.1322 +
1.1323 +\prew
1.1324 +\textbf{nitpick} \\[2\smallskipamount]
1.1325 +\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.1326 +\hbox{}\qquad Free variable: \nopagebreak \\
1.1327 +\hbox{}\qquad\qquad $w = [a, a, b]$
1.1328 +\postw
1.1329 +
1.1330 +Some detective work is necessary to find out what went wrong here. To get $[a,
1.1331 +a, b] \in S$, we need $[a, b] \in B$ by \textit{R3}, which in turn can only come
1.1332 +from \textit{R6}:
1.1333 +
1.1334 +\prew
1.1335 +``$\lbrakk v \in B;\> v \in B\rbrakk \,\Longrightarrow\, a \mathbin{\#} v \mathbin{@} w \in B$''
1.1336 +\postw
1.1337 +
1.1338 +Now, this formula must be wrong: The same assumption occurs twice, and the
1.1339 +variable $w$ is unconstrained. Clearly, one of the two occurrences of $v$ in
1.1340 +the assumptions should have been a $w$.
1.1341 +
1.1342 +With the correction made, we don't get any counterexample from Nitpick. Let's
1.1343 +move on and check completeness:
1.1344 +
1.1345 +\prew
1.1346 +\textbf{theorem}~\textit{S\_complete}: \\
1.1347 +``$\textit{length}~[x\mathbin{\leftarrow} w.\; x = a] =
1.1348 + \textit{length}~[x\mathbin{\leftarrow} w.\; x = b]
1.1349 + \longrightarrow w \in S$'' \\
1.1350 +\textbf{nitpick} \\[2\smallskipamount]
1.1351 +\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.1352 +\hbox{}\qquad Free variable: \nopagebreak \\
1.1353 +\hbox{}\qquad\qquad $w = [b, b, a, a]$
1.1354 +\postw
1.1355 +
1.1356 +Apparently, $[b, b, a, a] \notin S$, even though it has the same numbers of
1.1357 +$a$'s and $b$'s. But since our inductive definition passed the soundness check,
1.1358 +the introduction rules we have are probably correct. Perhaps we simply lack an
1.1359 +introduction rule. Comparing the grammar with the inductive definition, our
1.1360 +suspicion is confirmed: Joe Blow simply forgot the production $A ::= bAA$,
1.1361 +without which the grammar cannot generate two or more $b$'s in a row. So we add
1.1362 +the rule
1.1363 +
1.1364 +\prew
1.1365 +``$\lbrakk v \in A;\> w \in A\rbrakk \,\Longrightarrow\, b \mathbin{\#} v \mathbin{@} w \in A$''
1.1366 +\postw
1.1367 +
1.1368 +With this last change, we don't get any counterexamples from Nitpick for either
1.1369 +soundness or completeness. We can even generalize our result to cover $A$ and
1.1370 +$B$ as well:
1.1371 +
1.1372 +\prew
1.1373 +\textbf{theorem} \textit{S\_A\_B\_sound\_and\_complete}: \\
1.1374 +``$w \in S \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b]$'' \\
1.1375 +``$w \in A \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] + 1$'' \\
1.1376 +``$w \in B \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] + 1$'' \\
1.1377 +\textbf{nitpick} \\[2\smallskipamount]
1.1378 +\slshape Nitpick found no counterexample.
1.1379 +\postw
1.1380 +
1.1381 +\subsection{AA Trees}
1.1382 +\label{aa-trees}
1.1383 +
1.1384 +AA trees are a kind of balanced trees discovered by Arne Andersson that provide
1.1385 +similar performance to red-black trees, but with a simpler implementation
1.1386 +\cite{andersson-1993}. They can be used to store sets of elements equipped with
1.1387 +a total order $<$. We start by defining the datatype and some basic extractor
1.1388 +functions:
1.1389 +
1.1390 +\prew
1.1391 +\textbf{datatype} $'a$~\textit{tree} = $\Lambda$ $\mid$ $N$ ``\kern1pt$'a\Colon \textit{linorder}$'' \textit{nat} ``\kern1pt$'a$ \textit{tree}'' ``\kern1pt$'a$ \textit{tree}'' \\[2\smallskipamount]
1.1392 +\textbf{primrec} \textit{data} \textbf{where} \\
1.1393 +``$\textit{data}~\Lambda = \undef$'' $\,\mid$ \\
1.1394 +``$\textit{data}~(N~x~\_~\_~\_) = x$'' \\[2\smallskipamount]
1.1395 +\textbf{primrec} \textit{dataset} \textbf{where} \\
1.1396 +``$\textit{dataset}~\Lambda = \{\}$'' $\,\mid$ \\
1.1397 +``$\textit{dataset}~(N~x~\_~t~u) = \{x\} \cup \textit{dataset}~t \mathrel{\cup} \textit{dataset}~u$'' \\[2\smallskipamount]
1.1398 +\textbf{primrec} \textit{level} \textbf{where} \\
1.1399 +``$\textit{level}~\Lambda = 0$'' $\,\mid$ \\
1.1400 +``$\textit{level}~(N~\_~k~\_~\_) = k$'' \\[2\smallskipamount]
1.1401 +\textbf{primrec} \textit{left} \textbf{where} \\
1.1402 +``$\textit{left}~\Lambda = \Lambda$'' $\,\mid$ \\
1.1403 +``$\textit{left}~(N~\_~\_~t~\_) = t$'' \\[2\smallskipamount]
1.1404 +\textbf{primrec} \textit{right} \textbf{where} \\
1.1405 +``$\textit{right}~\Lambda = \Lambda$'' $\,\mid$ \\
1.1406 +``$\textit{right}~(N~\_~\_~\_~u) = u$''
1.1407 +\postw
1.1408 +
1.1409 +The wellformedness criterion for AA trees is fairly complex. Wikipedia states it
1.1410 +as follows \cite{wikipedia-2009-aa-trees}:
1.1411 +
1.1412 +\kern.2\parskip %% TYPESETTING
1.1413 +
1.1414 +\pre
1.1415 +Each node has a level field, and the following invariants must remain true for
1.1416 +the tree to be valid:
1.1417 +
1.1418 +\raggedright
1.1419 +
1.1420 +\kern-.4\parskip %% TYPESETTING
1.1421 +
1.1422 +\begin{enum}
1.1423 +\item[]
1.1424 +\begin{enum}
1.1425 +\item[1.] The level of a leaf node is one.
1.1426 +\item[2.] The level of a left child is strictly less than that of its parent.
1.1427 +\item[3.] The level of a right child is less than or equal to that of its parent.
1.1428 +\item[4.] The level of a right grandchild is strictly less than that of its grandparent.
1.1429 +\item[5.] Every node of level greater than one must have two children.
1.1430 +\end{enum}
1.1431 +\end{enum}
1.1432 +\post
1.1433 +
1.1434 +\kern.4\parskip %% TYPESETTING
1.1435 +
1.1436 +The \textit{wf} predicate formalizes this description:
1.1437 +
1.1438 +\prew
1.1439 +\textbf{primrec} \textit{wf} \textbf{where} \\
1.1440 +``$\textit{wf}~\Lambda = \textit{True}$'' $\,\mid$ \\
1.1441 +``$\textit{wf}~(N~\_~k~t~u) =$ \\
1.1442 +\phantom{``}$(\textrm{if}~t = \Lambda~\textrm{then}$ \\
1.1443 +\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))$ \\
1.1444 +\phantom{``$($}$\textrm{else}$ \\
1.1445 +\hbox{\phantom{``$(\quad$}$\textit{wf}~t \mathrel{\land} \textit{wf}~u
1.1446 +\mathrel{\land} u \not= \Lambda \mathrel{\land} \textit{level}~t < k
1.1447 +\mathrel{\land} \textit{level}~u \le k \mathrel{\land}
1.1448 +\textit{level}~(\textit{right}~u) < k)$''}\kern-200mm
1.1449 +\postw
1.1450 +
1.1451 +Rebalancing the tree upon insertion and removal of elements is performed by two
1.1452 +auxiliary functions called \textit{skew} and \textit{split}, defined below:
1.1453 +
1.1454 +\prew
1.1455 +\textbf{primrec} \textit{skew} \textbf{where} \\
1.1456 +``$\textit{skew}~\Lambda = \Lambda$'' $\,\mid$ \\
1.1457 +``$\textit{skew}~(N~x~k~t~u) = {}$ \\
1.1458 +\phantom{``}$(\textrm{if}~t \not= \Lambda \mathrel{\land} k =
1.1459 +\textit{level}~t~\textrm{then}$ \\
1.1460 +\phantom{``(\quad}$N~(\textit{data}~t)~k~(\textit{left}~t)~(N~x~k~
1.1461 +(\textit{right}~t)~u)$ \\
1.1462 +\phantom{``(}$\textrm{else}$ \\
1.1463 +\phantom{``(\quad}$N~x~k~t~u)$''
1.1464 +\postw
1.1465 +
1.1466 +\prew
1.1467 +\textbf{primrec} \textit{split} \textbf{where} \\
1.1468 +``$\textit{split}~\Lambda = \Lambda$'' $\,\mid$ \\
1.1469 +``$\textit{split}~(N~x~k~t~u) = {}$ \\
1.1470 +\phantom{``}$(\textrm{if}~u \not= \Lambda \mathrel{\land} k =
1.1471 +\textit{level}~(\textit{right}~u)~\textrm{then}$ \\
1.1472 +\phantom{``(\quad}$N~(\textit{data}~u)~(\textit{Suc}~k)~
1.1473 +(N~x~k~t~(\textit{left}~u))~(\textit{right}~u)$ \\
1.1474 +\phantom{``(}$\textrm{else}$ \\
1.1475 +\phantom{``(\quad}$N~x~k~t~u)$''
1.1476 +\postw
1.1477 +
1.1478 +Performing a \textit{skew} or a \textit{split} should have no impact on the set
1.1479 +of elements stored in the tree:
1.1480 +
1.1481 +\prew
1.1482 +\textbf{theorem}~\textit{dataset\_skew\_split}:\\
1.1483 +``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
1.1484 +``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
1.1485 +\textbf{nitpick} \\[2\smallskipamount]
1.1486 +{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
1.1487 +\postw
1.1488 +
1.1489 +Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
1.1490 +should not alter the tree:
1.1491 +
1.1492 +\prew
1.1493 +\textbf{theorem}~\textit{wf\_skew\_split}:\\
1.1494 +``$\textit{wf}~t\,\Longrightarrow\, \textit{skew}~t = t$'' \\
1.1495 +``$\textit{wf}~t\,\Longrightarrow\, \textit{split}~t = t$'' \\
1.1496 +\textbf{nitpick} \\[2\smallskipamount]
1.1497 +{\slshape Nitpick found no counterexample.}
1.1498 +\postw
1.1499 +
1.1500 +Insertion is implemented recursively. It preserves the sort order:
1.1501 +
1.1502 +\prew
1.1503 +\textbf{primrec}~\textit{insort} \textbf{where} \\
1.1504 +``$\textit{insort}~\Lambda~x = N~x~1~\Lambda~\Lambda$'' $\,\mid$ \\
1.1505 +``$\textit{insort}~(N~y~k~t~u)~x =$ \\
1.1506 +\phantom{``}$({*}~(\textit{split} \circ \textit{skew})~{*})~(N~y~k~(\textrm{if}~x < y~\textrm{then}~\textit{insort}~t~x~\textrm{else}~t)$ \\
1.1507 +\phantom{``$({*}~(\textit{split} \circ \textit{skew})~{*})~(N~y~k~$}$(\textrm{if}~x > y~\textrm{then}~\textit{insort}~u~x~\textrm{else}~u))$''
1.1508 +\postw
1.1509 +
1.1510 +Notice that we deliberately commented out the application of \textit{skew} and
1.1511 +\textit{split}. Let's see if this causes any problems:
1.1512 +
1.1513 +\prew
1.1514 +\textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
1.1515 +\textbf{nitpick} \\[2\smallskipamount]
1.1516 +\slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
1.1517 +\hbox{}\qquad Free variables: \nopagebreak \\
1.1518 +\hbox{}\qquad\qquad $t = N~a_3~1~\Lambda~\Lambda$ \\
1.1519 +\hbox{}\qquad\qquad $x = a_4$ \\[2\smallskipamount]
1.1520 +Hint: Maybe you forgot a type constraint?
1.1521 +\postw
1.1522 +
1.1523 +It's hard to see why this is a counterexample. The hint is of no help here. To
1.1524 +improve readability, we will restrict the theorem to \textit{nat}, so that we
1.1525 +don't need to look up the value of the $\textit{op}~{<}$ constant to find out
1.1526 +which element is smaller than the other. In addition, we will tell Nitpick to
1.1527 +display the value of $\textit{insort}~t~x$ using the \textit{eval} option. This
1.1528 +gives
1.1529 +
1.1530 +\prew
1.1531 +\textbf{theorem} \textit{wf\_insort\_nat}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\
1.1532 +\textbf{nitpick} [\textit{eval} = ``$\textit{insort}~t~x$''] \\[2\smallskipamount]
1.1533 +\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.1534 +\hbox{}\qquad Free variables: \nopagebreak \\
1.1535 +\hbox{}\qquad\qquad $t = N~1~1~\Lambda~\Lambda$ \\
1.1536 +\hbox{}\qquad\qquad $x = 0$ \\
1.1537 +\hbox{}\qquad Evaluated term: \\
1.1538 +\hbox{}\qquad\qquad $\textit{insort}~t~x = N~1~1~(N~0~1~\Lambda~\Lambda)~\Lambda$
1.1539 +\postw
1.1540 +
1.1541 +Nitpick's output reveals that the element $0$ was added as a left child of $1$,
1.1542 +where both have a level of 1. This violates the second AA tree invariant, which
1.1543 +states that a left child's level must be less than its parent's. This shouldn't
1.1544 +come as a surprise, considering that we commented out the tree rebalancing code.
1.1545 +Reintroducing the code seems to solve the problem:
1.1546 +
1.1547 +\prew
1.1548 +\textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
1.1549 +\textbf{nitpick} \\[2\smallskipamount]
1.1550 +{\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
1.1551 +\postw
1.1552 +
1.1553 +Insertion should transform the set of elements represented by the tree in the
1.1554 +obvious way:
1.1555 +
1.1556 +\prew
1.1557 +\textbf{theorem} \textit{dataset\_insort}:\kern.4em
1.1558 +``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
1.1559 +\textbf{nitpick} \\[2\smallskipamount]
1.1560 +{\slshape Nitpick ran out of time after checking 5 of 8 scopes.}
1.1561 +\postw
1.1562 +
1.1563 +We could continue like this and sketch a complete theory of AA trees without
1.1564 +performing a single proof. Once the definitions and main theorems are in place
1.1565 +and have been thoroughly tested using Nitpick, we could start working on the
1.1566 +proofs. Developing theories this way usually saves time, because faulty theorems
1.1567 +and definitions are discovered much earlier in the process.
1.1568 +
1.1569 +\section{Option Reference}
1.1570 +\label{option-reference}
1.1571 +
1.1572 +\def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
1.1573 +\def\qty#1{$\left<\textit{#1}\right>$}
1.1574 +\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
1.1575 +\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1.1576 +\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1.1577 +\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1.1578 +\def\ops#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
1.1579 +\def\opt#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
1.1580 +\def\opu#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
1.1581 +\def\opusmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
1.1582 +
1.1583 +Nitpick's behavior can be influenced by various options, which can be specified
1.1584 +in brackets after the \textbf{nitpick} command. Default values can be set
1.1585 +using \textbf{nitpick\_\allowbreak params}. For example:
1.1586 +
1.1587 +\prew
1.1588 +\textbf{nitpick\_params} [\textit{verbose}, \,\textit{timeout} = 60$\,s$]
1.1589 +\postw
1.1590 +
1.1591 +The options are categorized as follows:\ mode of operation
1.1592 +(\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output
1.1593 +format (\S\ref{output-format}), automatic counterexample checks
1.1594 +(\S\ref{authentication}), optimizations
1.1595 +(\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
1.1596 +
1.1597 +The number of options can be overwhelming at first glance. Do not let that worry
1.1598 +you: Nitpick's defaults have been chosen so that it almost always does the right
1.1599 +thing, and the most important options have been covered in context in
1.1600 +\S\ref{first-steps}.
1.1601 +
1.1602 +The descriptions below refer to the following syntactic quantities:
1.1603 +
1.1604 +\begin{enum}
1.1605 +\item[$\bullet$] \qtybf{string}: A string.
1.1606 +\item[$\bullet$] \qtybf{bool}: \textit{true} or \textit{false}.
1.1607 +\item[$\bullet$] \qtybf{bool\_or\_smart}: \textit{true}, \textit{false}, or \textit{smart}.
1.1608 +\item[$\bullet$] \qtybf{int}: An integer. Negative integers are prefixed with a hyphen.
1.1609 +\item[$\bullet$] \qtybf{int\_or\_smart}: An integer or \textit{smart}.
1.1610 +\item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
1.1611 +of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<midarrow\char`\>}.
1.1612 +
1.1613 +\item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
1.1614 +\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
1.1615 +(milliseconds), or the keyword \textit{none} ($\infty$ years).
1.1616 +\item[$\bullet$] \qtybf{const}: The name of a HOL constant.
1.1617 +\item[$\bullet$] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
1.1618 +\item[$\bullet$] \qtybf{term\_list}: A space-separated list of HOL terms (e.g.,
1.1619 +``$f~x$''~``$g~y$'').
1.1620 +\item[$\bullet$] \qtybf{type}: A HOL type.
1.1621 +\end{enum}
1.1622 +
1.1623 +Default values are indicated in square brackets. Boolean options have a negated
1.1624 +counterpart (e.g., \textit{auto} vs.\ \textit{no\_auto}). When setting Boolean
1.1625 +options, ``= \textit{true}'' may be omitted.
1.1626 +
1.1627 +\subsection{Mode of Operation}
1.1628 +\label{mode-of-operation}
1.1629 +
1.1630 +\begin{enum}
1.1631 +\opfalse{auto}{no\_auto}
1.1632 +Specifies whether Nitpick should be run automatically on newly entered theorems.
1.1633 +For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}) and
1.1634 +\textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
1.1635 +\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
1.1636 +(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
1.1637 +disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
1.1638 +\textit{auto\_timeout} (\S\ref{timeouts}) is used as the time limit instead of
1.1639 +\textit{timeout} (\S\ref{timeouts}). The output is also more concise.
1.1640 +
1.1641 +\nopagebreak
1.1642 +{\small See also \textit{auto\_timeout} (\S\ref{timeouts}).}
1.1643 +
1.1644 +\optrue{blocking}{non\_blocking}
1.1645 +Specifies whether the \textbf{nitpick} command should operate synchronously.
1.1646 +The asynchronous (non-blocking) mode lets the user start proving the putative
1.1647 +theorem while Nitpick looks for a counterexample, but it can also be more
1.1648 +confusing. For technical reasons, automatic runs currently always block.
1.1649 +
1.1650 +\nopagebreak
1.1651 +{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
1.1652 +
1.1653 +\optrue{falsify}{satisfy}
1.1654 +Specifies whether Nitpick should look for falsifying examples (countermodels) or
1.1655 +satisfying examples (models). This manual assumes throughout that
1.1656 +\textit{falsify} is enabled.
1.1657 +
1.1658 +\opsmart{user\_axioms}{no\_user\_axioms}
1.1659 +Specifies whether the user-defined axioms (specified using
1.1660 +\textbf{axiomatization} and \textbf{axioms}) should be considered. If the option
1.1661 +is set to \textit{smart}, Nitpick performs an ad hoc axiom selection based on
1.1662 +the constants that occur in the formula to falsify. The option is implicitly set
1.1663 +to \textit{true} for automatic runs.
1.1664 +
1.1665 +\textbf{Warning:} If the option is set to \textit{true}, Nitpick might
1.1666 +nonetheless ignore some polymorphic axioms. Counterexamples generated under
1.1667 +these conditions are tagged as ``likely genuine.'' The \textit{debug}
1.1668 +(\S\ref{output-format}) option can be used to find out which axioms were
1.1669 +considered.
1.1670 +
1.1671 +\nopagebreak
1.1672 +{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{assms}
1.1673 +(\S\ref{mode-of-operation}), and \textit{debug} (\S\ref{output-format}).}
1.1674 +
1.1675 +\optrue{assms}{no\_assms}
1.1676 +Specifies whether the relevant assumptions in structured proof should be
1.1677 +considered. The option is implicitly enabled for automatic runs.
1.1678 +
1.1679 +\nopagebreak
1.1680 +{\small See also \textit{auto} (\S\ref{mode-of-operation})
1.1681 +and \textit{user\_axioms} (\S\ref{mode-of-operation}).}
1.1682 +
1.1683 +\opfalse{overlord}{no\_overlord}
1.1684 +Specifies whether Nitpick should put its temporary files in
1.1685 +\texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
1.1686 +debugging Nitpick but also unsafe if several instances of the tool are run
1.1687 +simultaneously. This option is disabled by default unless your home directory
1.1688 +ends with \texttt{blanchet} or \texttt{blanchette}.
1.1689 +%``I thought there was only one overlord.'' --- Tobias Nipkow
1.1690 +
1.1691 +\nopagebreak
1.1692 +{\small See also \textit{debug} (\S\ref{output-format}).}
1.1693 +\end{enum}
1.1694 +
1.1695 +\subsection{Scope of Search}
1.1696 +\label{scope-of-search}
1.1697 +
1.1698 +\begin{enum}
1.1699 +\opu{card}{type}{int\_seq}
1.1700 +Specifies the sequence of cardinalities to use for a given type. For
1.1701 +\textit{nat} and \textit{int}, the cardinality fully specifies the subset used
1.1702 +to approximate the type. For example:
1.1703 +%
1.1704 +$$\hbox{\begin{tabular}{@{}rll@{}}%
1.1705 +\textit{card nat} = 4 & induces & $\{0,\, 1,\, 2,\, 3\}$ \\
1.1706 +\textit{card int} = 4 & induces & $\{-1,\, 0,\, +1,\, +2\}$ \\
1.1707 +\textit{card int} = 5 & induces & $\{-2,\, -1,\, 0,\, +1,\, +2\}.$%
1.1708 +\end{tabular}}$$
1.1709 +%
1.1710 +In general:
1.1711 +%
1.1712 +$$\hbox{\begin{tabular}{@{}rll@{}}%
1.1713 +\textit{card nat} = $K$ & induces & $\{0,\, \ldots,\, K - 1\}$ \\
1.1714 +\textit{card int} = $K$ & induces & $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor K/2 \rfloor\}.$%
1.1715 +\end{tabular}}$$
1.1716 +%
1.1717 +For free types, and often also for \textbf{typedecl}'d types, it usually makes
1.1718 +sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
1.1719 +Although function and product types are normally mapped directly to the
1.1720 +corresponding Kodkod concepts, setting
1.1721 +the cardinality of such types is also allowed and implicitly enables ``boxing''
1.1722 +for them, as explained in the description of the \textit{box}~\qty{type}
1.1723 +and \textit{box} (\S\ref{scope-of-search}) options.
1.1724 +
1.1725 +\nopagebreak
1.1726 +{\small See also \textit{mono} (\S\ref{scope-of-search}).}
1.1727 +
1.1728 +\opt{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
1.1729 +Specifies the default sequence of cardinalities to use. This can be overridden
1.1730 +on a per-type basis using the \textit{card}~\qty{type} option described above.
1.1731 +
1.1732 +\opu{max}{const}{int\_seq}
1.1733 +Specifies the sequence of maximum multiplicities to use for a given
1.1734 +(co)in\-duc\-tive datatype constructor. A constructor's multiplicity is the
1.1735 +number of distinct values that it can construct. Nonsensical values (e.g.,
1.1736 +\textit{max}~[]~$=$~2) are silently repaired. This option is only available for
1.1737 +datatypes equipped with several constructors.
1.1738 +
1.1739 +\ops{max}{int\_seq}
1.1740 +Specifies the default sequence of maximum multiplicities to use for
1.1741 +(co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor
1.1742 +basis using the \textit{max}~\qty{const} option described above.
1.1743 +
1.1744 +\opusmart{wf}{const}{non\_wf}
1.1745 +Specifies whether the specified (co)in\-duc\-tively defined predicate is
1.1746 +well-founded. The option can take the following values:
1.1747 +
1.1748 +\begin{enum}
1.1749 +\item[$\bullet$] \textbf{\textit{true}}: Tentatively treat the (co)in\-duc\-tive
1.1750 +predicate as if it were well-founded. Since this is generally not sound when the
1.1751 +predicate is not well-founded, the counterexamples are tagged as ``likely
1.1752 +genuine.''
1.1753 +
1.1754 +\item[$\bullet$] \textbf{\textit{false}}: Treat the (co)in\-duc\-tive predicate
1.1755 +as if it were not well-founded. The predicate is then unrolled as prescribed by
1.1756 +the \textit{star\_linear\_preds}, \textit{iter}~\qty{const}, and \textit{iter}
1.1757 +options.
1.1758 +
1.1759 +\item[$\bullet$] \textbf{\textit{smart}}: Try to prove that the inductive
1.1760 +predicate is well-founded using Isabelle's \textit{lexicographic\_order} and
1.1761 +\textit{sizechange} tactics. If this succeeds (or the predicate occurs with an
1.1762 +appropriate polarity in the formula to falsify), use an efficient fixed point
1.1763 +equation as specification of the predicate; otherwise, unroll the predicates
1.1764 +according to the \textit{iter}~\qty{const} and \textit{iter} options.
1.1765 +\end{enum}
1.1766 +
1.1767 +\nopagebreak
1.1768 +{\small See also \textit{iter} (\S\ref{scope-of-search}),
1.1769 +\textit{star\_linear\_preds} (\S\ref{optimizations}), and \textit{tac\_timeout}
1.1770 +(\S\ref{timeouts}).}
1.1771 +
1.1772 +\opsmart{wf}{non\_wf}
1.1773 +Specifies the default wellfoundedness setting to use. This can be overridden on
1.1774 +a per-predicate basis using the \textit{wf}~\qty{const} option above.
1.1775 +
1.1776 +\opu{iter}{const}{int\_seq}
1.1777 +Specifies the sequence of iteration counts to use when unrolling a given
1.1778 +(co)in\-duc\-tive predicate. By default, unrolling is applied for inductive
1.1779 +predicates that occur negatively and coinductive predicates that occur
1.1780 +positively in the formula to falsify and that cannot be proved to be
1.1781 +well-founded, but this behavior is influenced by the \textit{wf} option. The
1.1782 +iteration counts are automatically bounded by the cardinality of the predicate's
1.1783 +domain.
1.1784 +
1.1785 +{\small See also \textit{wf} (\S\ref{scope-of-search}) and
1.1786 +\textit{star\_linear\_preds} (\S\ref{optimizations}).}
1.1787 +
1.1788 +\opt{iter}{int\_seq}{$\mathbf{1{,}2{,}4{,}8{,}12{,}16{,}24{,}32}$}
1.1789 +Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive
1.1790 +predicates. This can be overridden on a per-predicate basis using the
1.1791 +\textit{iter} \qty{const} option above.
1.1792 +
1.1793 +\opt{bisim\_depth}{int\_seq}{$\mathbf{7}$}
1.1794 +Specifies the sequence of iteration counts to use when unrolling the
1.1795 +bisimilarity predicate generated by Nitpick for coinductive datatypes. A value
1.1796 +of $-1$ means that no predicate is generated, in which case Nitpick performs an
1.1797 +after-the-fact check to see if the known coinductive datatype values are
1.1798 +bidissimilar. If two values are found to be bisimilar, the counterexample is
1.1799 +tagged as ``likely genuine.'' The iteration counts are automatically bounded by
1.1800 +the sum of the cardinalities of the coinductive datatypes occurring in the
1.1801 +formula to falsify.
1.1802 +
1.1803 +\opusmart{box}{type}{dont\_box}
1.1804 +Specifies whether Nitpick should attempt to wrap (``box'') a given function or
1.1805 +product type in an isomorphic datatype internally. Boxing is an effective mean
1.1806 +to reduce the search space and speed up Nitpick, because the isomorphic datatype
1.1807 +is approximated by a subset of the possible function or pair values;
1.1808 +like other drastic optimizations, it can also prevent the discovery of
1.1809 +counterexamples. The option can take the following values:
1.1810 +
1.1811 +\begin{enum}
1.1812 +\item[$\bullet$] \textbf{\textit{true}}: Box the specified type whenever
1.1813 +practicable.
1.1814 +\item[$\bullet$] \textbf{\textit{false}}: Never box the type.
1.1815 +\item[$\bullet$] \textbf{\textit{smart}}: Box the type only in contexts where it
1.1816 +is likely to help. For example, $n$-tuples where $n > 2$ and arguments to
1.1817 +higher-order functions are good candidates for boxing.
1.1818 +\end{enum}
1.1819 +
1.1820 +Setting the \textit{card}~\qty{type} option for a function or product type
1.1821 +implicitly enables boxing for that type.
1.1822 +
1.1823 +\nopagebreak
1.1824 +{\small See also \textit{verbose} (\S\ref{output-format})
1.1825 +and \textit{debug} (\S\ref{output-format}).}
1.1826 +
1.1827 +\opsmart{box}{dont\_box}
1.1828 +Specifies the default boxing setting to use. This can be overridden on a
1.1829 +per-type basis using the \textit{box}~\qty{type} option described above.
1.1830 +
1.1831 +\opusmart{mono}{type}{non\_mono}
1.1832 +Specifies whether the specified type should be considered monotonic when
1.1833 +enumerating scopes. If the option is set to \textit{smart}, Nitpick performs a
1.1834 +monotonicity check on the type. Setting this option to \textit{true} can reduce
1.1835 +the number of scopes tried, but it also diminishes the theoretical chance of
1.1836 +finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}.
1.1837 +
1.1838 +\nopagebreak
1.1839 +{\small See also \textit{card} (\S\ref{scope-of-search}),
1.1840 +\textit{coalesce\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
1.1841 +(\S\ref{output-format}).}
1.1842 +
1.1843 +\opsmart{mono}{non\_box}
1.1844 +Specifies the default monotonicity setting to use. This can be overridden on a
1.1845 +per-type basis using the \textit{mono}~\qty{type} option described above.
1.1846 +
1.1847 +\opfalse{coalesce\_type\_vars}{dont\_coalesce\_type\_vars}
1.1848 +Specifies whether type variables with the same sort constraints should be
1.1849 +merged. Setting this option to \textit{true} can reduce the number of scopes
1.1850 +tried and the size of the generated Kodkod formulas, but it also diminishes the
1.1851 +theoretical chance of finding a counterexample.
1.1852 +
1.1853 +{\small See also \textit{mono} (\S\ref{scope-of-search}).}
1.1854 +\end{enum}
1.1855 +
1.1856 +\subsection{Output Format}
1.1857 +\label{output-format}
1.1858 +
1.1859 +\begin{enum}
1.1860 +\opfalse{verbose}{quiet}
1.1861 +Specifies whether the \textbf{nitpick} command should explain what it does. This
1.1862 +option is useful to determine which scopes are tried or which SAT solver is
1.1863 +used. This option is implicitly disabled for automatic runs.
1.1864 +
1.1865 +\nopagebreak
1.1866 +{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
1.1867 +
1.1868 +\opfalse{debug}{no\_debug}
1.1869 +Specifies whether Nitpick should display additional debugging information beyond
1.1870 +what \textit{verbose} already displays. Enabling \textit{debug} also enables
1.1871 +\textit{verbose} and \textit{show\_all} behind the scenes. The \textit{debug}
1.1872 +option is implicitly disabled for automatic runs.
1.1873 +
1.1874 +\nopagebreak
1.1875 +{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{overlord}
1.1876 +(\S\ref{mode-of-operation}), and \textit{batch\_size} (\S\ref{optimizations}).}
1.1877 +
1.1878 +\optrue{show\_skolems}{hide\_skolem}
1.1879 +Specifies whether the values of Skolem constants should be displayed as part of
1.1880 +counterexamples. Skolem constants correspond to bound variables in the original
1.1881 +formula and usually help us to understand why the counterexample falsifies the
1.1882 +formula.
1.1883 +
1.1884 +\nopagebreak
1.1885 +{\small See also \textit{skolemize} (\S\ref{optimizations}).}
1.1886 +
1.1887 +\opfalse{show\_datatypes}{hide\_datatypes}
1.1888 +Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
1.1889 +be displayed as part of counterexamples. Such subsets are sometimes helpful when
1.1890 +investigating whether a potential counterexample is genuine or spurious, but
1.1891 +their potential for clutter is real.
1.1892 +
1.1893 +\opfalse{show\_consts}{hide\_consts}
1.1894 +Specifies whether the values of constants occurring in the formula (including
1.1895 +its axioms) should be displayed along with any counterexample. These values are
1.1896 +sometimes helpful when investigating why a counterexample is
1.1897 +genuine, but they can clutter the output.
1.1898 +
1.1899 +\opfalse{show\_all}{dont\_show\_all}
1.1900 +Enabling this option effectively enables \textit{show\_skolems},
1.1901 +\textit{show\_datatypes}, and \textit{show\_consts}.
1.1902 +
1.1903 +\opt{max\_potential}{int}{$\mathbf{1}$}
1.1904 +Specifies the maximum number of potential counterexamples to display. Setting
1.1905 +this option to 0 speeds up the search for a genuine counterexample. This option
1.1906 +is implicitly set to 0 for automatic runs. If you set this option to a value
1.1907 +greater than 1, you will need an incremental SAT solver: For efficiency, it is
1.1908 +recommended to install the JNI version of MiniSat and set \textit{sat\_solver} =
1.1909 +\textit{MiniSatJNI}. Also be aware that many of the counterexamples may look
1.1910 +identical, unless the \textit{show\_all} (\S\ref{output-format}) option is
1.1911 +enabled.
1.1912 +
1.1913 +\nopagebreak
1.1914 +{\small See also \textit{auto} (\S\ref{mode-of-operation}),
1.1915 +\textit{check\_potential} (\S\ref{authentication}), and
1.1916 +\textit{sat\_solver} (\S\ref{optimizations}).}
1.1917 +
1.1918 +\opt{max\_genuine}{int}{$\mathbf{1}$}
1.1919 +Specifies the maximum number of genuine counterexamples to display. If you set
1.1920 +this option to a value greater than 1, you will need an incremental SAT solver:
1.1921 +For efficiency, it is recommended to install the JNI version of MiniSat and set
1.1922 +\textit{sat\_solver} = \textit{MiniSatJNI}. Also be aware that many of the
1.1923 +counterexamples may look identical, unless the \textit{show\_all}
1.1924 +(\S\ref{output-format}) option is enabled.
1.1925 +
1.1926 +\nopagebreak
1.1927 +{\small See also \textit{check\_genuine} (\S\ref{authentication}) and
1.1928 +\textit{sat\_solver} (\S\ref{optimizations}).}
1.1929 +
1.1930 +\ops{eval}{term\_list}
1.1931 +Specifies the list of terms whose values should be displayed along with
1.1932 +counterexamples. This option suffers from an ``observer effect'': Nitpick might
1.1933 +find different counterexamples for different values of this option.
1.1934 +
1.1935 +\opu{format}{term}{int\_seq}
1.1936 +Specifies how to uncurry the value displayed for a variable or constant.
1.1937 +Uncurrying sometimes increases the readability of the output for high-arity
1.1938 +functions. For example, given the variable $y \mathbin{\Colon} {'a}\Rightarrow
1.1939 +{'b}\Rightarrow {'c}\Rightarrow {'d}\Rightarrow {'e}\Rightarrow {'f}\Rightarrow
1.1940 +{'g}$, setting \textit{format}~$y$ = 3 tells Nitpick to group the last three
1.1941 +arguments, as if the type had been ${'a}\Rightarrow {'b}\Rightarrow
1.1942 +{'c}\Rightarrow {'d}\times {'e}\times {'f}\Rightarrow {'g}$. In general, a list
1.1943 +of values $n_1,\ldots,n_k$ tells Nitpick to show the last $n_k$ arguments as an
1.1944 +$n_k$-tuple, the previous $n_{k-1}$ arguments as an $n_{k-1}$-tuple, and so on;
1.1945 +arguments that are not accounted for are left alone, as if the specification had
1.1946 +been $1,\ldots,1,n_1,\ldots,n_k$.
1.1947 +
1.1948 +\nopagebreak
1.1949 +{\small See also \textit{uncurry} (\S\ref{optimizations}).}
1.1950 +
1.1951 +\opt{format}{int\_seq}{$\mathbf{1}$}
1.1952 +Specifies the default format to use. Irrespective of the default format, the
1.1953 +extra arguments to a Skolem constant corresponding to the outer bound variables
1.1954 +are kept separated from the remaining arguments, the \textbf{for} arguments of
1.1955 +an inductive definitions are kept separated from the remaining arguments, and
1.1956 +the iteration counter of an unrolled inductive definition is shown alone. The
1.1957 +default format can be overridden on a per-variable or per-constant basis using
1.1958 +the \textit{format}~\qty{term} option described above.
1.1959 +\end{enum}
1.1960 +
1.1961 +%% MARK: Authentication
1.1962 +\subsection{Authentication}
1.1963 +\label{authentication}
1.1964 +
1.1965 +\begin{enum}
1.1966 +\opfalse{check\_potential}{trust\_potential}
1.1967 +Specifies whether potential counterexamples should be given to Isabelle's
1.1968 +\textit{auto} tactic to assess their validity. If a potential counterexample is
1.1969 +shown to be genuine, Nitpick displays a message to this effect and terminates.
1.1970 +
1.1971 +\nopagebreak
1.1972 +{\small See also \textit{max\_potential} (\S\ref{output-format}) and
1.1973 +\textit{auto\_timeout} (\S\ref{timeouts}).}
1.1974 +
1.1975 +\opfalse{check\_genuine}{trust\_genuine}
1.1976 +Specifies whether genuine and likely genuine counterexamples should be given to
1.1977 +Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine''
1.1978 +counterexample is shown to be spurious, the user is kindly asked to send a bug
1.1979 +report to the author at
1.1980 +\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@in.tum.de}.
1.1981 +
1.1982 +\nopagebreak
1.1983 +{\small See also \textit{max\_genuine} (\S\ref{output-format}) and
1.1984 +\textit{auto\_timeout} (\S\ref{timeouts}).}
1.1985 +
1.1986 +\ops{expect}{string}
1.1987 +Specifies the expected outcome, which must be one of the following:
1.1988 +
1.1989 +\begin{enum}
1.1990 +\item[$\bullet$] \textbf{\textit{genuine}}: Nitpick found a genuine counterexample.
1.1991 +\item[$\bullet$] \textbf{\textit{likely\_genuine}}: Nitpick found a ``likely
1.1992 +genuine'' counterexample (i.e., a counterexample that is genuine unless
1.1993 +it contradicts a missing axiom or a dangerous option was used inappropriately).
1.1994 +\item[$\bullet$] \textbf{\textit{potential}}: Nitpick found a potential counterexample.
1.1995 +\item[$\bullet$] \textbf{\textit{none}}: Nitpick found no counterexample.
1.1996 +\item[$\bullet$] \textbf{\textit{unknown}}: Nitpick encountered some problem (e.g.,
1.1997 +Kodkod ran out of memory).
1.1998 +\end{enum}
1.1999 +
1.2000 +Nitpick emits an error if the actual outcome differs from the expected outcome.
1.2001 +This option is useful for regression testing.
1.2002 +\end{enum}
1.2003 +
1.2004 +\subsection{Optimizations}
1.2005 +\label{optimizations}
1.2006 +
1.2007 +\def\cpp{C\nobreak\raisebox{.1ex}{+}\nobreak\raisebox{.1ex}{+}}
1.2008 +
1.2009 +\sloppy
1.2010 +
1.2011 +\begin{enum}
1.2012 +\opt{sat\_solver}{string}{smart}
1.2013 +Specifies which SAT solver to use. SAT solvers implemented in C or \cpp{} tend
1.2014 +to be faster than their Java counterparts, but they can be more difficult to
1.2015 +install. Also, if you set the \textit{max\_potential} (\S\ref{output-format}) or
1.2016 +\textit{max\_genuine} (\S\ref{output-format}) option to a value greater than 1,
1.2017 +you will need an incremental SAT solver, such as \textit{MiniSatJNI}
1.2018 +(recommended) or \textit{SAT4J}.
1.2019 +
1.2020 +The supported solvers are listed below:
1.2021 +
1.2022 +\begin{enum}
1.2023 +
1.2024 +\item[$\bullet$] \textbf{\textit{MiniSat}}: MiniSat is an efficient solver
1.2025 +written in \cpp{}. To use MiniSat, set the environment variable
1.2026 +\texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
1.2027 +executable. The \cpp{} sources and executables for MiniSat are available at
1.2028 +\url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
1.2029 +and 2.0 beta (2007-07-21).
1.2030 +
1.2031 +\item[$\bullet$] \textbf{\textit{MiniSatJNI}}: The JNI (Java Native Interface)
1.2032 +version of MiniSat is bundled in \texttt{nativesolver.\allowbreak tgz}, which
1.2033 +you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
1.2034 +version of MiniSat, the JNI version can be used incrementally.
1.2035 +
1.2036 +\item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver
1.2037 +written in C. It is bundled with Kodkodi and requires no further installation or
1.2038 +configuration steps. Alternatively, you can install a standard version of
1.2039 +PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
1.2040 +that contains the \texttt{picosat} executable. The C sources for PicoSAT are
1.2041 +available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
1.2042 +Nitpick has been tested with version 913.
1.2043 +
1.2044 +\item[$\bullet$] \textbf{\textit{zChaff}}: zChaff is an efficient solver written
1.2045 +in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
1.2046 +the directory that contains the \texttt{zchaff} executable. The \cpp{} sources
1.2047 +and executables for zChaff are available at
1.2048 +\url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
1.2049 +versions 2004-05-13, 2004-11-15, and 2007-03-12.
1.2050 +
1.2051 +\item[$\bullet$] \textbf{\textit{zChaffJNI}}: The JNI version of zChaff is
1.2052 +bundled in \texttt{native\-solver.\allowbreak tgz}, which you will find on
1.2053 +Kodkod's web site \cite{kodkod-2009}.
1.2054 +
1.2055 +\item[$\bullet$] \textbf{\textit{RSat}}: RSat is an efficient solver written in
1.2056 +\cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
1.2057 +directory that contains the \texttt{rsat} executable. The \cpp{} sources for
1.2058 +RSat are available at \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been
1.2059 +tested with version 2.01.
1.2060 +
1.2061 +\item[$\bullet$] \textbf{\textit{BerkMin}}: BerkMin561 is an efficient solver
1.2062 +written in C. To use BerkMin, set the environment variable
1.2063 +\texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561}
1.2064 +executable. The BerkMin executables are available at
1.2065 +\url{http://eigold.tripod.com/BerkMin.html}.
1.2066 +
1.2067 +\item[$\bullet$] \textbf{\textit{BerkMinAlloy}}: Variant of BerkMin that is
1.2068 +included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
1.2069 +version of BerkMin, set the environment variable
1.2070 +\texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
1.2071 +executable.
1.2072 +
1.2073 +\item[$\bullet$] \textbf{\textit{Jerusat}}: Jerusat 1.3 is an efficient solver
1.2074 +written in C. To use Jerusat, set the environment variable
1.2075 +\texttt{JERUSAT\_HOME} to the directory that contains the \texttt{Jerusat1.3}
1.2076 +executable. The C sources for Jerusat are available at
1.2077 +\url{http://www.cs.tau.ac.il/~ale1/Jerusat1.3.tgz}.
1.2078 +
1.2079 +\item[$\bullet$] \textbf{\textit{SAT4J}}: SAT4J is a reasonably efficient solver
1.2080 +written in Java that can be used incrementally. It is bundled with Kodkodi and
1.2081 +requires no further installation or configuration steps. Do not attempt to
1.2082 +install the official SAT4J packages, because their API is incompatible with
1.2083 +Kodkod.
1.2084 +
1.2085 +\item[$\bullet$] \textbf{\textit{SAT4JLight}}: Variant of SAT4J that is
1.2086 +optimized for small problems. It can also be used incrementally.
1.2087 +
1.2088 +\item[$\bullet$] \textbf{\textit{HaifaSat}}: HaifaSat 1.0 beta is an
1.2089 +experimental solver written in \cpp. To use HaifaSat, set the environment
1.2090 +variable \texttt{HAIFASAT\_\allowbreak HOME} to the directory that contains the
1.2091 +\texttt{HaifaSat} executable. The \cpp{} sources for HaifaSat are available at
1.2092 +\url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}.
1.2093 +
1.2094 +\item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
1.2095 +\textit{smart}, Nitpick selects the first solver among MiniSat, PicoSAT, zChaff,
1.2096 +RSat, BerkMin, BerkMinAlloy, and Jerusat that is recognized by Isabelle. If none
1.2097 +is found, it falls back on SAT4J, which should always be available. If
1.2098 +\textit{verbose} is enabled, Nitpick displays which SAT solver was chosen.
1.2099 +
1.2100 +\end{enum}
1.2101 +\fussy
1.2102 +
1.2103 +\opt{batch\_size}{int\_or\_smart}{smart}
1.2104 +Specifies the maximum number of Kodkod problems that should be lumped together
1.2105 +when invoking Kodkodi. Each problem corresponds to one scope. Lumping problems
1.2106 +together ensures that Kodkodi is launched less often, but it makes the verbose
1.2107 +output less readable and is sometimes detrimental to performance. If
1.2108 +\textit{batch\_size} is set to \textit{smart}, the actual value used is 1 if
1.2109 +\textit{debug} (\S\ref{output-format}) is set and 64 otherwise.
1.2110 +
1.2111 +\optrue{destroy\_constrs}{dont\_destroy\_constrs}
1.2112 +Specifies whether formulas involving (co)in\-duc\-tive datatype constructors should
1.2113 +be rewritten to use (automatically generated) discriminators and destructors.
1.2114 +This optimization can drastically reduce the size of the Boolean formulas given
1.2115 +to the SAT solver.
1.2116 +
1.2117 +\nopagebreak
1.2118 +{\small See also \textit{debug} (\S\ref{output-format}).}
1.2119 +
1.2120 +\optrue{specialize}{dont\_specialize}
1.2121 +Specifies whether functions invoked with static arguments should be specialized.
1.2122 +This optimization can drastically reduce the search space, especially for
1.2123 +higher-order functions.
1.2124 +
1.2125 +\nopagebreak
1.2126 +{\small See also \textit{debug} (\S\ref{output-format}) and
1.2127 +\textit{show\_consts} (\S\ref{output-format}).}
1.2128 +
1.2129 +\optrue{skolemize}{dont\_skolemize}
1.2130 +Specifies whether the formula should be skolemized. For performance reasons,
1.2131 +(positive) $\forall$-quanti\-fiers that occur in the scope of a higher-order
1.2132 +(positive) $\exists$-quanti\-fier are left unchanged.
1.2133 +
1.2134 +\nopagebreak
1.2135 +{\small See also \textit{debug} (\S\ref{output-format}) and
1.2136 +\textit{show\_skolems} (\S\ref{output-format}).}
1.2137 +
1.2138 +\optrue{star\_linear\_preds}{dont\_star\_linear\_preds}
1.2139 +Specifies whether Nitpick should use Kodkod's transitive closure operator to
1.2140 +encode non-well-founded ``linear inductive predicates,'' i.e., inductive
1.2141 +predicates for which each the predicate occurs in at most one assumption of each
1.2142 +introduction rule. Using the reflexive transitive closure is in principle
1.2143 +equivalent to setting \textit{iter} to the cardinality of the predicate's
1.2144 +domain, but it is usually more efficient.
1.2145 +
1.2146 +{\small See also \textit{wf} (\S\ref{scope-of-search}), \textit{debug}
1.2147 +(\S\ref{output-format}), and \textit{iter} (\S\ref{scope-of-search}).}
1.2148 +
1.2149 +\optrue{uncurry}{dont\_uncurry}
1.2150 +Specifies whether Nitpick should uncurry functions. Uncurrying has on its own no
1.2151 +tangible effect on efficiency, but it creates opportunities for the boxing
1.2152 +optimization.
1.2153 +
1.2154 +\nopagebreak
1.2155 +{\small See also \textit{box} (\S\ref{scope-of-search}), \textit{debug}
1.2156 +(\S\ref{output-format}), and \textit{format} (\S\ref{output-format}).}
1.2157 +
1.2158 +\optrue{fast\_descrs}{full\_descrs}
1.2159 +Specifies whether Nitpick should optimize the definite and indefinite
1.2160 +description operators (THE and SOME). The optimized versions usually help
1.2161 +Nitpick generate more counterexamples or at least find them faster, but only the
1.2162 +unoptimized versions are complete when all types occurring in the formula are
1.2163 +finite.
1.2164 +
1.2165 +{\small See also \textit{debug} (\S\ref{output-format}).}
1.2166 +
1.2167 +\optrue{peephole\_optim}{no\_peephole\_optim}
1.2168 +Specifies whether Nitpick should simplify the generated Kodkod formulas using a
1.2169 +peephole optimizer. These optimizations can make a significant difference.
1.2170 +Unless you are tracking down a bug in Nitpick or distrust the peephole
1.2171 +optimizer, you should leave this option enabled.
1.2172 +
1.2173 +\opt{sym\_break}{int}{20}
1.2174 +Specifies an upper bound on the number of relations for which Kodkod generates
1.2175 +symmetry breaking predicates. According to the Kodkod documentation
1.2176 +\cite{kodkod-2009-options}, ``in general, the higher this value, the more
1.2177 +symmetries will be broken, and the faster the formula will be solved. But,
1.2178 +setting the value too high may have the opposite effect and slow down the
1.2179 +solving.''
1.2180 +
1.2181 +\opt{sharing\_depth}{int}{3}
1.2182 +Specifies the depth to which Kodkod should check circuits for equivalence during
1.2183 +the translation to SAT. The default of 3 is the same as in Alloy. The minimum
1.2184 +allowed depth is 1. Increasing the sharing may result in a smaller SAT problem,
1.2185 +but can also slow down Kodkod.
1.2186 +
1.2187 +\opfalse{flatten\_props}{dont\_flatten\_props}
1.2188 +Specifies whether Kodkod should try to eliminate intermediate Boolean variables.
1.2189 +Although this might sound like a good idea, in practice it can drastically slow
1.2190 +down Kodkod.
1.2191 +
1.2192 +\opt{max\_threads}{int}{0}
1.2193 +Specifies the maximum number of threads to use in Kodkod. If this option is set
1.2194 +to 0, Kodkod will compute an appropriate value based on the number of processor
1.2195 +cores available.
1.2196 +
1.2197 +\nopagebreak
1.2198 +{\small See also \textit{batch\_size} (\S\ref{optimizations}) and
1.2199 +\textit{timeout} (\S\ref{timeouts}).}
1.2200 +\end{enum}
1.2201 +
1.2202 +\subsection{Timeouts}
1.2203 +\label{timeouts}
1.2204 +
1.2205 +\begin{enum}
1.2206 +\opt{timeout}{time}{$\mathbf{30}$ s}
1.2207 +Specifies the maximum amount of time that the \textbf{nitpick} command should
1.2208 +spend looking for a counterexample. Nitpick tries to honor this constraint as
1.2209 +well as it can but offers no guarantees. For automatic runs,
1.2210 +\textit{auto\_timeout} is used instead.
1.2211 +
1.2212 +\nopagebreak
1.2213 +{\small See also \textit{auto} (\S\ref{mode-of-operation})
1.2214 +and \textit{max\_threads} (\S\ref{optimizations}).}
1.2215 +
1.2216 +\opt{auto\_timeout}{time}{$\mathbf{5}$ s}
1.2217 +Specifies the maximum amount of time that Nitpick should use to find a
1.2218 +counterexample when running automatically. Nitpick tries to honor this
1.2219 +constraint as well as it can but offers no guarantees.
1.2220 +
1.2221 +\nopagebreak
1.2222 +{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
1.2223 +
1.2224 +\opt{tac\_timeout}{time}{$\mathbf{500}$ ms}
1.2225 +Specifies the maximum amount of time that the \textit{auto} tactic should use
1.2226 +when checking a counterexample, and similarly that \textit{lexicographic\_order}
1.2227 +and \textit{sizechange} should use when checking whether a (co)in\-duc\-tive
1.2228 +predicate is well-founded. Nitpick tries to honor this constraint as well as it
1.2229 +can but offers no guarantees.
1.2230 +
1.2231 +\nopagebreak
1.2232 +{\small See also \textit{wf} (\S\ref{scope-of-search}),
1.2233 +\textit{check\_potential} (\S\ref{authentication}),
1.2234 +and \textit{check\_genuine} (\S\ref{authentication}).}
1.2235 +\end{enum}
1.2236 +
1.2237 +\section{Attribute Reference}
1.2238 +\label{attribute-reference}
1.2239 +
1.2240 +Nitpick needs to consider the definitions of all constants occurring in a
1.2241 +formula in order to falsify it. For constants introduced using the
1.2242 +\textbf{definition} command, the definition is simply the associated
1.2243 +\textit{\_def} axiom. In contrast, instead of using the internal representation
1.2244 +of functions synthesized by Isabelle's \textbf{primrec}, \textbf{function}, and
1.2245 +\textbf{nominal\_primrec} packages, Nitpick relies on the more natural
1.2246 +equational specification entered by the user.
1.2247 +
1.2248 +Behind the scenes, Isabelle's built-in packages and theories rely on the
1.2249 +following attributes to affect Nitpick's behavior:
1.2250 +
1.2251 +\begin{itemize}
1.2252 +\flushitem{\textit{nitpick\_def}}
1.2253 +
1.2254 +\nopagebreak
1.2255 +This attribute specifies an alternative definition of a constant. The
1.2256 +alternative definition should be logically equivalent to the constant's actual
1.2257 +axiomatic definition and should be of the form
1.2258 +
1.2259 +\qquad $c~{?}x_1~\ldots~{?}x_n \,\equiv\, t$,
1.2260 +
1.2261 +where ${?}x_1, \ldots, {?}x_n$ are distinct variables and $c$ does not occur in
1.2262 +$t$.
1.2263 +
1.2264 +\flushitem{\textit{nitpick\_simp}}
1.2265 +
1.2266 +\nopagebreak
1.2267 +This attribute specifies the equations that constitute the specification of a
1.2268 +constant. For functions defined using the \textbf{primrec}, \textbf{function},
1.2269 +and \textbf{nominal\_\allowbreak primrec} packages, this corresponds to the
1.2270 +\textit{simps} rules. The equations must be of the form
1.2271 +
1.2272 +\qquad $c~t_1~\ldots\ t_n \,=\, u.$
1.2273 +
1.2274 +\flushitem{\textit{nitpick\_psimp}}
1.2275 +
1.2276 +\nopagebreak
1.2277 +This attribute specifies the equations that constitute the partial specification
1.2278 +of a constant. For functions defined using the \textbf{function} package, this
1.2279 +corresponds to the \textit{psimps} rules. The conditional equations must be of
1.2280 +the form
1.2281 +
1.2282 +\qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,=\, u$.
1.2283 +
1.2284 +\flushitem{\textit{nitpick\_intro}}
1.2285 +
1.2286 +\nopagebreak
1.2287 +This attribute specifies the introduction rules of a (co)in\-duc\-tive predicate.
1.2288 +For predicates defined using the \textbf{inductive} or \textbf{coinductive}
1.2289 +command, this corresponds to the \textit{intros} rules. The introduction rules
1.2290 +must be of the form
1.2291 +
1.2292 +\qquad $\lbrakk P_1;\> \ldots;\> P_m;\> M~(c\ t_{11}\ \ldots\ t_{1n});\>
1.2293 +\ldots;\> M~(c\ t_{k1}\ \ldots\ t_{kn})\rbrakk \,\Longrightarrow\, c\ u_1\
1.2294 +\ldots\ u_n$,
1.2295 +
1.2296 +where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an
1.2297 +optional monotonic operator. The order of the assumptions is irrelevant.
1.2298 +
1.2299 +\end{itemize}
1.2300 +
1.2301 +When faced with a constant, Nitpick proceeds as follows:
1.2302 +
1.2303 +\begin{enum}
1.2304 +\item[1.] If the \textit{nitpick\_simp} set associated with the constant
1.2305 +is not empty, Nitpick uses these rules as the specification of the constant.
1.2306 +
1.2307 +\item[2.] Otherwise, if the \textit{nitpick\_psimp} set associated with
1.2308 +the constant is not empty, it uses these rules as the specification of the
1.2309 +constant.
1.2310 +
1.2311 +\item[3.] Otherwise, it looks up the definition of the constant:
1.2312 +
1.2313 +\begin{enum}
1.2314 +\item[1.] If the \textit{nitpick\_def} set associated with the constant
1.2315 +is not empty, it uses the latest rule added to the set as the definition of the
1.2316 +constant; otherwise it uses the actual definition axiom.
1.2317 +\item[2.] If the definition is of the form
1.2318 +
1.2319 +\qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{lfp}~(\lambda f.\; t)$,
1.2320 +
1.2321 +then Nitpick assumes that the definition was made using an inductive package and
1.2322 +based on the introduction rules marked with \textit{nitpick\_\allowbreak
1.2323 +ind\_\allowbreak intros} tries to determine whether the definition is
1.2324 +well-founded.
1.2325 +\end{enum}
1.2326 +\end{enum}
1.2327 +
1.2328 +As an illustration, consider the inductive definition
1.2329 +
1.2330 +\prew
1.2331 +\textbf{inductive}~\textit{odd}~\textbf{where} \\
1.2332 +``\textit{odd}~1'' $\,\mid$ \\
1.2333 +``\textit{odd}~$n\,\Longrightarrow\, \textit{odd}~(\textit{Suc}~(\textit{Suc}~n))$''
1.2334 +\postw
1.2335 +
1.2336 +Isabelle automatically attaches the \textit{nitpick\_intro} attribute to
1.2337 +the above rules. Nitpick then uses the \textit{lfp}-based definition in
1.2338 +conjunction with these rules. To override this, we can specify an alternative
1.2339 +definition as follows:
1.2340 +
1.2341 +\prew
1.2342 +\textbf{lemma} $\mathit{odd\_def}'$ [\textit{nitpick\_def}]: ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
1.2343 +\postw
1.2344 +
1.2345 +Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2
1.2346 += 1$. Alternatively, we can specify an equational specification of the constant:
1.2347 +
1.2348 +\prew
1.2349 +\textbf{lemma} $\mathit{odd\_simp}'$ [\textit{nitpick\_simp}]: ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
1.2350 +\postw
1.2351 +
1.2352 +Such tweaks should be done with great care, because Nitpick will assume that the
1.2353 +constant is completely defined by its equational specification. For example, if
1.2354 +you make ``$\textit{odd}~(2 * k + 1)$'' a \textit{nitpick\_simp} rule and neglect to provide rules to handle the $2 * k$ case, Nitpick will define
1.2355 +$\textit{odd}~n$ arbitrarily for even values of $n$. The \textit{debug}
1.2356 +(\S\ref{output-format}) option is extremely useful to understand what is going
1.2357 +on when experimenting with \textit{nitpick\_} attributes.
1.2358 +
1.2359 +\section{Standard ML Interface}
1.2360 +\label{standard-ml-interface}
1.2361 +
1.2362 +Nitpick provides a rich Standard ML interface used mainly for internal purposes
1.2363 +and debugging. Among the most interesting functions exported by Nitpick are
1.2364 +those that let you invoke the tool programmatically and those that let you
1.2365 +register and unregister custom coinductive datatypes.
1.2366 +
1.2367 +\subsection{Invocation of Nitpick}
1.2368 +\label{invocation-of-nitpick}
1.2369 +
1.2370 +The \textit{Nitpick} structure offers the following functions for invoking your
1.2371 +favorite counterexample generator:
1.2372 +
1.2373 +\prew
1.2374 +$\textbf{val}\,~\textit{pick\_nits\_in\_term} : \\
1.2375 +\hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{term~list} \rightarrow \textit{term} \\
1.2376 +\hbox{}\quad{\rightarrow}\; \textit{string} * \textit{Proof.state}$ \\
1.2377 +$\textbf{val}\,~\textit{pick\_nits\_in\_subgoal} : \\
1.2378 +\hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{int} \rightarrow \textit{string} * \textit{Proof.state}$
1.2379 +\postw
1.2380 +
1.2381 +The return value is a new proof state paired with an outcome string
1.2382 +(``genuine'', ``likely\_genuine'', ``potential'', ``none'', or ``unknown''). The
1.2383 +\textit{params} type is a large record that lets you set Nitpick's options. The
1.2384 +current default options can be retrieved by calling the following function
1.2385 +defined in the \textit{NitpickIsar} structure:
1.2386 +
1.2387 +\prew
1.2388 +$\textbf{val}\,~\textit{default\_params} :\,
1.2389 +\textit{theory} \rightarrow (\textit{string} * \textit{string})~\textit{list} \rightarrow \textit{params}$
1.2390 +\postw
1.2391 +
1.2392 +The second argument lets you override option values before they are parsed and
1.2393 +put into a \textit{params} record. Here is an example:
1.2394 +
1.2395 +\prew
1.2396 +$\textbf{val}\,~\textit{params} = \textit{NitpickIsar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
1.2397 +$\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t]
1.2398 +& \textit{state}~\textit{params}~\textit{false} \\[-2pt]
1.2399 +& \textit{subgoal}\end{aligned}$
1.2400 +\postw
1.2401 +
1.2402 +\subsection{Registration of Coinductive Datatypes}
1.2403 +\label{registration-of-coinductive-datatypes}
1.2404 +
1.2405 +\let\antiq=\textrm
1.2406 +
1.2407 +If you have defined a custom coinductive datatype, you can tell Nitpick about
1.2408 +it, so that it can use an efficient Kodkod axiomatization similar to the one it
1.2409 +uses for lazy lists. The interface for registering and unregistering coinductive
1.2410 +datatypes consists of the following pair of functions defined in the
1.2411 +\textit{Nitpick} structure:
1.2412 +
1.2413 +\prew
1.2414 +$\textbf{val}\,~\textit{register\_codatatype} :\,
1.2415 +\textit{typ} \rightarrow \textit{string} \rightarrow \textit{styp~list} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\
1.2416 +$\textbf{val}\,~\textit{unregister\_codatatype} :\,
1.2417 +\textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$
1.2418 +\postw
1.2419 +
1.2420 +The type $'a~\textit{llist}$ of lazy lists is already registered; had it
1.2421 +not been, you could have told Nitpick about it by adding the following line
1.2422 +to your theory file:
1.2423 +
1.2424 +\prew
1.2425 +$\textbf{setup}~\,\{{*}\,~\!\begin{aligned}[t]
1.2426 +& \textit{Nitpick.register\_codatatype} \\[-2pt]
1.2427 +& \qquad @\{\antiq{typ}~``\kern1pt'a~\textit{llist}\textrm{''}\}~@\{\antiq{const\_name}~ \textit{llist\_case}\} \\[-2pt] %% TYPESETTING
1.2428 +& \qquad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])\,\ {*}\}\end{aligned}$
1.2429 +\postw
1.2430 +
1.2431 +The \textit{register\_codatatype} function takes a coinductive type, its case
1.2432 +function, and the list of its constructors. The case function must take its
1.2433 +arguments in the order that the constructors are listed. If no case function
1.2434 +with the correct signature is available, simply pass the empty string.
1.2435 +
1.2436 +On the other hand, if your goal is to cripple Nitpick, add the following line to
1.2437 +your theory file and try to check a few conjectures about lazy lists:
1.2438 +
1.2439 +\prew
1.2440 +$\textbf{setup}~\,\{{*}\,~\textit{Nitpick.unregister\_codatatype}~@\{\antiq{typ}~``
1.2441 +\kern1pt'a~\textit{list}\textrm{''}\}\ \,{*}\}$
1.2442 +\postw
1.2443 +
1.2444 +\section{Known Bugs and Limitations}
1.2445 +\label{known-bugs-and-limitations}
1.2446 +
1.2447 +Here are the known bugs and limitations in Nitpick at the time of writing:
1.2448 +
1.2449 +\begin{enum}
1.2450 +\item[$\bullet$] Underspecified functions defined using the \textbf{primrec},
1.2451 +\textbf{function}, or \textbf{nominal\_\allowbreak primrec} packages can lead
1.2452 +Nitpick to generate spurious counterexamples for theorems that refer to values
1.2453 +for which the function is not defined. For example:
1.2454 +
1.2455 +\prew
1.2456 +\textbf{primrec} \textit{prec} \textbf{where} \\
1.2457 +``$\textit{prec}~(\textit{Suc}~n) = n$'' \\[2\smallskipamount]
1.2458 +\textbf{lemma} ``$\textit{prec}~0 = \undef$'' \\
1.2459 +\textbf{nitpick} \\[2\smallskipamount]
1.2460 +\quad{\slshape Nitpick found a counterexample for \textit{card nat}~= 2:
1.2461 +\nopagebreak
1.2462 +\\[2\smallskipamount]
1.2463 +\hbox{}\qquad Empty assignment} \nopagebreak\\[2\smallskipamount]
1.2464 +\textbf{by}~(\textit{auto simp}: \textit{prec\_def})
1.2465 +\postw
1.2466 +
1.2467 +Such theorems are considered bad style because they rely on the internal
1.2468 +representation of functions synthesized by Isabelle, which is an implementation
1.2469 +detail.
1.2470 +
1.2471 +\item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
1.2472 +\textbf{guess} command in a structured proof.
1.2473 +
1.2474 +\item[$\bullet$] The \textit{nitpick\_} attributes and the
1.2475 +\textit{Nitpick.register\_} functions can cause havoc if used improperly.
1.2476 +
1.2477 +\item[$\bullet$] Local definitions are not supported and result in an error.
1.2478 +
1.2479 +\item[$\bullet$] All constants and types whose names start with
1.2480 +\textit{Nitpick}{.} or \textit{NitpickDefs}{.} are reserved for internal use.
1.2481 +\end{enum}
1.2482 +
1.2483 +\let\em=\sl
1.2484 +\bibliography{../manual}{}
1.2485 +\bibliographystyle{abbrv}
1.2486 +
1.2487 +\end{document}