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