author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 55902  39cc8409373f 
child 57040  fc96f394c7e5 
permissions  rwrr 
33191  1 
\documentclass[a4paper,12pt]{article} 
2 
\usepackage[T1]{fontenc} 

3 
\usepackage{amsmath} 

4 
\usepackage{amssymb} 

53091  5 
\usepackage[english]{babel} 
33191  6 
\usepackage{color} 
35695  7 
\usepackage{footmisc} 
33191  8 
\usepackage{graphicx} 
9 
%\usepackage{mathpazo} 

10 
\usepackage{multicol} 

11 
\usepackage{stmaryrd} 

12 
%\usepackage[scaled=.85]{beramono} 

48963
f11d88bfa934
more standard document preparation within session context;
wenzelm
parents:
47717
diff
changeset

13 
\usepackage{isabelle,iman,pdfsetup} 
33191  14 

15 
%\oddsidemargin=4.6mm 

16 
%\evensidemargin=4.6mm 

17 
%\textwidth=150mm 

18 
%\topmargin=4.6mm 

19 
%\headheight=0mm 

20 
%\headsep=0mm 

21 
%\textheight=234mm 

22 

23 
\def\Colon{\mathord{:\mkern1.5mu:}} 

24 
%\def\lbrakk{\mathopen{\lbrack\mkern3.25mu\lbrack}} 

25 
%\def\rbrakk{\mathclose{\rbrack\mkern3.255mu\rbrack}} 

26 
\def\lparr{\mathopen{(\mkern4mu\mid}} 

27 
\def\rparr{\mathclose{\mid\mkern4mu)}} 

28 

29 
\def\unk{{?}} 

46105  30 
\def\unkef{(\lambda x.\; \unk)} 
31 
\def\undef{(\lambda x.\; \_)} 

33191  32 
%\def\unr{\textit{others}} 
33 
\def\unr{\ldots} 

34 
\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}} 

35 
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}} 

36 

37 
\hyphenation{MiniSat sizechange FirstSteps grandparent nitpick 

45083
014342144091
put CryptoMiniSat first and remove warning about unsoundness now that it has been fixed in Kodkod
blanchet
parents:
45080
diff
changeset

38 
counterexample counterexamples datatype datatypes codatatype 
33191  39 
codatatypes inductive coinductive} 
40 

41 
\urlstyle{tt} 

42 

55290  43 
\renewcommand\_{\hbox{\textunderscore\kern.05ex}} 
44 

33191  45 
\begin{document} 
46 

45515  47 
%%% TYPESETTING 
48 
%\renewcommand\labelitemi{$\bullet$} 

49 
\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}} 

50 

33191  51 
\title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex] 
52 
Picking Nits \\[\smallskipamount] 

33887  53 
\Large A User's Guide to Nitpick for Isabelle/HOL} 
33191  54 
\author{\hbox{} \\ 
55 
Jasmin Christian Blanchette \\ 

33887  56 
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\ 
33191  57 
\hbox{}} 
58 

59 
\maketitle 

60 

61 
\tableofcontents 

62 

63 
\setlength{\parskip}{.7em plus .2em minus .1em} 

64 
\setlength{\parindent}{0pt} 

65 
\setlength{\abovedisplayskip}{\parskip} 

66 
\setlength{\abovedisplayshortskip}{.9\parskip} 

67 
\setlength{\belowdisplayskip}{\parskip} 

68 
\setlength{\belowdisplayshortskip}{.9\parskip} 

69 

70 
% Generalpurpose enum environment with correct spacing 

71 
\newenvironment{enum}% 

72 
{\begin{list}{}{% 

73 
\setlength{\topsep}{.1\parskip}% 

74 
\setlength{\partopsep}{.1\parskip}% 

75 
\setlength{\itemsep}{\parskip}% 

76 
\advance\itemsep by\parsep}} 

77 
{\end{list}} 

78 

79 
\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin 

80 
\advance\rightskip by\leftmargin} 

81 
\def\post{\vskip0pt plus1ex\endgroup} 

82 

83 
\def\prew{\pre\advance\rightskip by\leftmargin} 

84 
\def\postw{\post} 

85 

86 
\section{Introduction} 

87 
\label{introduction} 

88 

36926  89 
Nitpick \cite{blanchettenipkow2010} is a counterexample generator for 
33191  90 
Isabelle/HOL \cite{isatutorial} that is designed to handle formulas 
91 
combining (co)in\duc\tive datatypes, (co)in\duc\tively defined predicates, and 

92 
quantifiers. It builds on Kodkod \cite{torlakjackson2007}, a highly optimized 

93 
firstorder relational model finder developed by the Software Design Group at 

94 
MIT. It is conceptually similar to Refute \cite{weber2008}, from which it 

95 
borrows many ideas and code fragments, but it benefits from Kodkod's 

96 
optimizations and a new encoding scheme. The name Nitpick is shamelessly 

97 
appropriated from a now retired Alloy precursor. 

98 

99 
Nitpick is easy to useyou simply enter \textbf{nitpick} after a putative 

100 
theorem and wait a few seconds. Nonetheless, there are situations where knowing 

101 
how it works under the hood and how it reacts to various options helps 

102 
increase the test coverage. This manual also explains how to install the tool on 

103 
your workstation. Should the motivation fail you, think of the many hours of 

104 
hard work Nitpick will save you. Proving nontheorems is \textsl{hard work}. 

105 

106 
Another common use of Nitpick is to find out whether the axioms of a locale are 

107 
satisfiable, while the locale is being developed. To check this, it suffices to 

108 
write 

109 

110 
\prew 

46105  111 
\textbf{lemma}~``$\textit{False\/}$'' \\ 
33191  112 
\textbf{nitpick}~[\textit{show\_all}] 
113 
\postw 

114 

115 
after the locale's \textbf{begin} keyword. To falsify \textit{False}, Nitpick 

116 
must find a model for the axioms. If it finds no model, we have an indication 

117 
that the axioms might be unsatisfiable. 

118 

53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53091
diff
changeset

119 
For Isabelle/jEdit users, Nitpick provides an automatic mode that can be enabled 
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53091
diff
changeset

120 
via the ``Auto Nitpick'' option under ``Plugins > Plugin Options > Isabelle > 
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53091
diff
changeset

121 
General.'' In this mode, Nitpick is run on every newly entered theorem. 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33559
diff
changeset

122 

33191  123 
\newbox\boxA 
124 
\setbox\boxA=\hbox{\texttt{nospam}} 

125 

46242  126 
\newcommand\authoremail{\texttt{blan{\color{white}nospam}\kern\wd\boxA{}chette@\allowbreak 
127 
in.\allowbreak tum.\allowbreak de}} 

128 

129 
To run Nitpick, you must also make sure that the theory \textit{Nitpick} is 

130 
importedthis is rarely a problem in practice since it is part of 

131 
\textit{Main}. The examples presented in this manual can be found 

55290  132 
in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_\allowbreak Examples/\allowbreak Manual\_Nits.thy} theory. 
33191  133 
The known bugs and limitations at the time of writing are listed in 
46242  134 
\S\ref{knownbugsandlimitations}. Comments and bug reports concerning either 
135 
the tool or the manual should be directed to the author at \authoremail. 

33191  136 

137 
\vskip2.5\smallskipamount 

138 

139 
\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for 

140 
suggesting several textual improvements. 

141 
% and Perry James for reporting a typo. 

142 

46242  143 
\section{Installation} 
144 
\label{installation} 

145 

53760
cf37f4b84824
moved focus to Isabell/jEdit and away from Proof General
blanchet
parents:
53091
diff
changeset

146 
Nitpick is part of Isabelle, so you don't need to install it. However, it 
46242  147 
relies on a thirdparty Kodkod frontend called Kodkodi as well as a Java 
148 
virtual machine called \texttt{java} (version 1.5 or above). 

149 

150 
There are two main ways of installing Kodkodi: 

151 

152 
\begin{enum} 

153 
\item[\labelitemi] If you installed an official Isabelle package, 

154 
it should already include a properly setup version of Kodkodi. 

155 

156 
\item[\labelitemi] If you use a repository or snapshot version of Isabelle, you 

157 
an official Isabelle package, you can download the Isabelleaware Kodkodi package 

158 
from \url{http://www21.in.tum.de/~blanchet/\#software}. Extract the archive, then add a 

159 
line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}% 

160 
\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at 

161 
startup. Its value can be retrieved by executing \texttt{isabelle} 

162 
\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.} 

163 
file with the absolute path to Kodkodi. For example, if the 

164 
\texttt{components} file does not exist yet and you extracted Kodkodi to 

50488
1b3eb579e08b
use modern SAT solvers with modern Kodkod versions
blanchet
parents:
49618
diff
changeset

165 
\texttt{/usr/local/kodkodi1.5.2}, create it with the single line 
46242  166 

167 
\prew 

50488
1b3eb579e08b
use modern SAT solvers with modern Kodkod versions
blanchet
parents:
49618
diff
changeset

168 
\texttt{/usr/local/kodkodi1.5.2} 
46242  169 
\postw 
170 

171 
(including an invisible newline character) in it. 

172 
\end{enum} 

173 

174 
To check whether Kodkodi is successfully installed, you can try out the example 

175 
in \S\ref{propositionallogic}. 

36926  176 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

177 
\section{First Steps} 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

178 
\label{firststeps} 
33191  179 

180 
This section introduces Nitpick by presenting small examples. If possible, you 

181 
should try out the examples on your workstation. Your theory file should start 

35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

182 
as follows: 
33191  183 

184 
\prew 

185 
\textbf{theory}~\textit{Scratch} \\ 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

186 
\textbf{imports}~\textit{Main~Quotient\_Product~RealDef} \\ 
33191  187 
\textbf{begin} 
188 
\postw 

189 

35710  190 
The results presented here were obtained using the JNI (Java Native Interface) 
191 
version of MiniSat and with multithreading disabled to reduce nondeterminism. 

192 
This was done by adding the line 

33191  193 

194 
\prew 

35710  195 
\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1] 
33191  196 
\postw 
197 

198 
after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with 

45080  199 
Kodkodi and is precompiled for Linux, Mac~OS~X, and Windows (Cygwin). Other SAT 
50488
1b3eb579e08b
use modern SAT solvers with modern Kodkod versions
blanchet
parents:
49618
diff
changeset

200 
solvers can also be used, as explained in \S\ref{optimizations}. If you 
45080  201 
have already configured SAT solvers in Isabelle (e.g., for Refute), these will 
202 
also be available to Nitpick. 

33191  203 

204 
\subsection{Propositional Logic} 

205 
\label{propositionallogic} 

206 

207 
Let's start with a trivial example from propositional logic: 

208 

209 
\prew 

210 
\textbf{lemma}~``$P \longleftrightarrow Q$'' \\ 

211 
\textbf{nitpick} 

212 
\postw 

213 

214 
You should get the following output: 

215 

216 
\prew 

217 
\slshape 

218 
Nitpick found a counterexample: \\[2\smallskipamount] 

219 
\hbox{}\qquad Free variables: \nopagebreak \\ 

220 
\hbox{}\qquad\qquad $P = \textit{True}$ \\ 

221 
\hbox{}\qquad\qquad $Q = \textit{False}$ 

222 
\postw 

223 

224 
Nitpick can also be invoked on individual subgoals, as in the example below: 

225 

226 
\prew 

227 
\textbf{apply}~\textit{auto} \\[2\smallskipamount] 

228 
{\slshape goal (2 subgoals): \\ 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

229 
\phantom{0}1. $P\,\Longrightarrow\, Q$ \\ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

230 
\phantom{0}2. $Q\,\Longrightarrow\, P$} \\[2\smallskipamount] 
33191  231 
\textbf{nitpick}~1 \\[2\smallskipamount] 
232 
{\slshape Nitpick found a counterexample: \\[2\smallskipamount] 

233 
\hbox{}\qquad Free variables: \nopagebreak \\ 

234 
\hbox{}\qquad\qquad $P = \textit{True}$ \\ 

235 
\hbox{}\qquad\qquad $Q = \textit{False}$} \\[2\smallskipamount] 

236 
\textbf{nitpick}~2 \\[2\smallskipamount] 

237 
{\slshape Nitpick found a counterexample: \\[2\smallskipamount] 

238 
\hbox{}\qquad Free variables: \nopagebreak \\ 

239 
\hbox{}\qquad\qquad $P = \textit{False}$ \\ 

240 
\hbox{}\qquad\qquad $Q = \textit{True}$} \\[2\smallskipamount] 

241 
\textbf{oops} 

242 
\postw 

243 

244 
\subsection{Type Variables} 

245 
\label{typevariables} 

246 

247 
If you are left unimpressed by the previous example, don't worry. The next 

248 
one is more mind and computerboggling: 

249 

250 
\prew 

46105  251 
\textbf{lemma} ``$x \in A\,\Longrightarrow\, (\textrm{THE}~y.\;y \in A) \in A$'' 
33191  252 
\postw 
253 
\pagebreak[2] %% TYPESETTING 

254 

255 
The putative lemma involves the definite description operator, {THE}, presented 

256 
in section 5.10.1 of the Isabelle tutorial \cite{isatutorial}. The 

257 
operator is defined by the axiom $(\textrm{THE}~x.\; x = a) = a$. The putative 

258 
lemma is merely asserting the indefinite description operator axiom with {THE} 

259 
substituted for {SOME}. 

260 

261 
The free variable $x$ and the bound variable $y$ have type $'a$. For formulas 

262 
containing type variables, Nitpick enumerates the possible domains for each type 

38181  263 
variable, up to a given cardinality (10 by default), looking for a finite 
33191  264 
countermodel: 
265 

266 
\prew 

267 
\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount] 

268 
\slshape 

38181  269 
Trying 10 scopes: \nopagebreak \\ 
33191  270 
\hbox{}\qquad \textit{card}~$'a$~= 1; \\ 
271 
\hbox{}\qquad \textit{card}~$'a$~= 2; \\ 

272 
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount] 

38181  273 
\hbox{}\qquad \textit{card}~$'a$~= 10. \\[2\smallskipamount] 
33191  274 
Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount] 
275 
\hbox{}\qquad Free variables: \nopagebreak \\ 

46105  276 
\hbox{}\qquad\qquad $A = \{a_2,\, a_3\}$ \\ 
33191  277 
\hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount] 
46105  278 
Total time: 963 ms. 
33191  279 
\postw 
280 

281 
Nitpick found a counterexample in which $'a$ has cardinality 3. (For 

282 
cardinalities 1 and 2, the formula holds.) In the counterexample, the three 

283 
values of type $'a$ are written $a_1$, $a_2$, and $a_3$. 

284 

285 
The message ``Trying $n$ scopes: {\ldots}''\ is shown only if the option 

286 
\textit{verbose} is enabled. You can specify \textit{verbose} each time you 

287 
invoke \textbf{nitpick}, or you can set it globally using the command 

288 

289 
\prew 

290 
\textbf{nitpick\_params} [\textit{verbose}] 

291 
\postw 

292 

293 
This command also displays the current default values for all of the options 

294 
supported by Nitpick. The options are listed in \S\ref{optionreference}. 

295 

296 
\subsection{Constants} 

297 
\label{constants} 

298 

299 
By just looking at Nitpick's output, it might not be clear why the 

300 
counterexample in \S\ref{typevariables} is genuine. Let's invoke Nitpick again, 

301 
this time telling it to show the values of the constants that occur in the 

302 
formula: 

303 

304 
\prew 

46105  305 
\textbf{lemma} ``$x \in A\,\Longrightarrow\, (\textrm{THE}~y.\;y \in A) \in A$'' \\ 
33191  306 
\textbf{nitpick}~[\textit{show\_consts}] \\[2\smallskipamount] 
307 
\slshape 

308 
Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount] 

309 
\hbox{}\qquad Free variables: \nopagebreak \\ 

46105  310 
\hbox{}\qquad\qquad $A = \{a_2,\, a_3\}$ \\ 
33191  311 
\hbox{}\qquad\qquad $x = a_3$ \\ 
312 
\hbox{}\qquad Constant: \nopagebreak \\ 

46105  313 
\hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;y \in A = a_1$ 
33191  314 
\postw 
315 

39359  316 
As the result of an optimization, Nitpick directly assigned a value to the 
46105  317 
subterm $\textrm{THE}~y.\;y \in A$, rather than to the \textit{The} constant. We 
318 
can disable this optimization by using the command 

33191  319 

320 
\prew 

39359  321 
\textbf{nitpick}~[\textit{dont\_specialize},\, \textit{show\_consts}] 
33191  322 
\postw 
323 

324 
Our misadventures with THE suggest adding `$\exists!x{.}$' (``there exists a 

325 
unique $x$ such that'') at the front of our putative lemma's assumption: 

326 

327 
\prew 

46105  328 
\textbf{lemma} ``$\exists {!}x.\; x \in A\,\Longrightarrow\, (\textrm{THE}~y.\;y \in A) \in A$'' 
33191  329 
\postw 
330 

331 
The fix appears to work: 

332 

333 
\prew 

334 
\textbf{nitpick} \\[2\smallskipamount] 

335 
\slshape Nitpick found no counterexample. 

336 
\postw 

337 

338 
We can further increase our confidence in the formula by exhausting all 

339 
cardinalities up to 50: 

340 

341 
\prew 

342 
\textbf{nitpick} [\textit{card} $'a$~= 150]\footnote{The symbol `' 

343 
can be entered as \texttt{} (hyphen) or 

42959  344 
\texttt{\char`\\\char`\<emdash\char`\>}.} \\[2\smallskipamount] 
33191  345 
\slshape Nitpick found no counterexample. 
346 
\postw 

347 

38181  348 
Let's see if Sledgehammer can find a proof: 
33191  349 

350 
\prew 

351 
\textbf{sledgehammer} \\[2\smallskipamount] 

46105  352 
{\slshape Sledgehammer: ``$e$'' on goal \\ 
46242  353 
Try this: \textbf{by}~(\textit{metis~theI}) (42 ms).} \\ 
354 
\hbox{}\qquad\vdots \\[2\smallskipamount] 

46105  355 
\textbf{by}~(\textit{metis~theI\/}) 
33191  356 
\postw 
357 

358 
This must be our lucky day. 

359 

360 
\subsection{Skolemization} 

361 
\label{skolemization} 

362 

363 
Are all invertible functions onto? Let's find out: 

364 

365 
\prew 

366 
\textbf{lemma} ``$\exists g.\; \forall x.~g~(f~x) = x 

367 
\,\Longrightarrow\, \forall y.\; \exists x.~y = f~x$'' \\ 

368 
\textbf{nitpick} \\[2\smallskipamount] 

369 
\slshape 

370 
Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\[2\smallskipamount] 

371 
\hbox{}\qquad Free variable: \nopagebreak \\ 

372 
\hbox{}\qquad\qquad $f = \undef{}(b_1 := a_1)$ \\ 

373 
\hbox{}\qquad Skolem constants: \nopagebreak \\ 

374 
\hbox{}\qquad\qquad $g = \undef{}(a_1 := b_1,\> a_2 := b_1)$ \\ 

375 
\hbox{}\qquad\qquad $y = a_2$ 

376 
\postw 

377 

46105  378 
(The Isabelle/HOL notation $f(x := y)$ denotes the function that maps $x$ to $y$ 
379 
and that otherwise behaves like $f$.) 

33191  380 
Although $f$ is the only free variable occurring in the formula, Nitpick also 
381 
displays values for the bound variables $g$ and $y$. These values are available 

382 
to Nitpick because it performs skolemization as a preprocessing step. 

383 

384 
In the previous example, skolemization only affected the outermost quantifiers. 

385 
This is not always the case, as illustrated below: 

386 

387 
\prew 

388 
\textbf{lemma} ``$\exists x.\; \forall f.\; f~x = x$'' \\ 

389 
\textbf{nitpick} \\[2\smallskipamount] 

390 
\slshape 

391 
Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount] 

392 
\hbox{}\qquad Skolem constant: \nopagebreak \\ 

393 
\hbox{}\qquad\qquad $\lambda x.\; f = 

394 
\undef{}(\!\begin{aligned}[t] 

395 
& a_1 := \undef{}(a_1 := a_2,\> a_2 := a_1), \\[2pt] 

396 
& a_2 := \undef{}(a_1 := a_1,\> a_2 := a_1))\end{aligned}$ 

397 
\postw 

398 

399 
The variable $f$ is bound within the scope of $x$; therefore, $f$ depends on 

400 
$x$, as suggested by the notation $\lambda x.\,f$. If $x = a_1$, then $f$ is the 

401 
function that maps $a_1$ to $a_2$ and vice versa; otherwise, $x = a_2$ and $f$ 

402 
maps both $a_1$ and $a_2$ to $a_1$. In both cases, $f~x \not= x$. 

403 

404 
The source of the Skolem constants is sometimes more obscure: 

405 

406 
\prew 

407 
\textbf{lemma} ``$\mathit{refl}~r\,\Longrightarrow\, \mathit{sym}~r$'' \\ 

408 
\textbf{nitpick} \\[2\smallskipamount] 

409 
\slshape 

410 
Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount] 

411 
\hbox{}\qquad Free variable: \nopagebreak \\ 

412 
\hbox{}\qquad\qquad $r = \{(a_1, a_1),\, (a_2, a_1),\, (a_2, a_2)\}$ \\ 

413 
\hbox{}\qquad Skolem constants: \nopagebreak \\ 

414 
\hbox{}\qquad\qquad $\mathit{sym}.x = a_2$ \\ 

415 
\hbox{}\qquad\qquad $\mathit{sym}.y = a_1$ 

416 
\postw 

417 

46105  418 
What happened here is that Nitpick expanded \textit{sym} to its definition: 
33191  419 

420 
\prew 

421 
$\mathit{sym}~r \,\equiv\, 

422 
\forall x\> y.\,\> (x, y) \in r \longrightarrow (y, x) \in r.$ 

423 
\postw 

424 

425 
As their names suggest, the Skolem constants $\mathit{sym}.x$ and 

426 
$\mathit{sym}.y$ are simply the bound variables $x$ and $y$ 

427 
from \textit{sym}'s definition. 

428 

429 
\subsection{Natural Numbers and Integers} 

430 
\label{naturalnumbersandintegers} 

431 

432 
Because of the axiom of infinity, the type \textit{nat} does not admit any 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

433 
finite models. To deal with this, Nitpick's approach is to consider finite 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

434 
subsets $N$ of \textit{nat} and maps all numbers $\notin N$ to the undefined 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

435 
value (displayed as `$\unk$'). The type \textit{int} is handled similarly. 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

436 
Internally, undefined values lead to a threevalued logic. 
33191  437 

35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

438 
Here is an example involving \textit{int\/}: 
33191  439 

440 
\prew 

441 
\textbf{lemma} ``$\lbrakk i \le j;\> n \le (m{\Colon}\mathit{int})\rbrakk \,\Longrightarrow\, i * n + j * m \le i * m + j * n$'' \\ 

442 
\textbf{nitpick} \\[2\smallskipamount] 

443 
\slshape Nitpick found a counterexample: \\[2\smallskipamount] 

444 
\hbox{}\qquad Free variables: \nopagebreak \\ 

445 
\hbox{}\qquad\qquad $i = 0$ \\ 

446 
\hbox{}\qquad\qquad $j = 1$ \\ 

447 
\hbox{}\qquad\qquad $m = 1$ \\ 

448 
\hbox{}\qquad\qquad $n = 0$ 

449 
\postw 

450 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

451 
Internally, Nitpick uses either a unary or a binary representation of numbers. 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

452 
The unary representation is more efficient but only suitable for numbers very 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

453 
close to zero. By default, Nitpick attempts to choose the more appropriate 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

454 
encoding by inspecting the formula at hand. This behavior can be overridden by 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

455 
passing either \textit{unary\_ints} or \textit{binary\_ints} as option. For 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

456 
binary notation, the number of bits to use can be specified using 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

457 
the \textit{bits} option. For example: 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

458 

c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

459 
\prew 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

460 
\textbf{nitpick} [\textit{binary\_ints}, \textit{bits}${} = 16$] 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

461 
\postw 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

462 

33191  463 
With infinite types, we don't always have the luxury of a genuine counterexample 
41992
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

464 
and must often content ourselves with a potentially spurious one. The tedious 
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

465 
task of finding out whether the potentially spurious counterexample is in fact 
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

466 
genuine can be delegated to \textit{auto} by passing \textit{check\_potential}. 
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

467 
For example: 
33191  468 

469 
\prew 

470 
\textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\ 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

471 
\textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[2\smallskipamount] 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35335
diff
changeset

472 
\slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported 
41992
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

473 
fragment. Only potentially spurious counterexamples may be found. \\[2\smallskipamount] 
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

474 
Nitpick found a potentially spurious counterexample: \\[2\smallskipamount] 
33191  475 
\hbox{}\qquad Free variable: \nopagebreak \\ 
476 
\hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount] 

477 
Confirmation by ``\textit{auto}'': The above counterexample is genuine. 

478 
\postw 

479 

41992
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

480 
You might wonder why the counterexample is first reported as potentially 
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

481 
spurious. The root of the problem is that the bound variable in $\forall n.\; 
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

482 
\textit{Suc}~n \mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds 
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

483 
an $n$ such that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to 
33191  484 
\textit{False}; but otherwise, it does not know anything about values of $n \ge 
46105  485 
\textit{card~nat}$ and must therefore evaluate the assumption to~$\unk$, not 
33191  486 
\textit{True}. Since the assumption can never be satisfied, the putative lemma 
487 
can never be falsified. 

488 

489 
Incidentally, if you distrust the socalled genuine counterexamples, you can 

490 
enable \textit{check\_\allowbreak genuine} to verify them as well. However, be 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

491 
aware that \textit{auto} will usually fail to prove that the counterexample is 
33191  492 
genuine or spurious. 
493 

494 
Some conjectures involving elementary number theory make Nitpick look like a 

495 
giant with feet of clay: 

496 

497 
\prew 

46105  498 
\textbf{lemma} ``$P~\textit{Suc\/}$'' \\ 
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35284
diff
changeset

499 
\textbf{nitpick} \\[2\smallskipamount] 
33191  500 
\slshape 
501 
Nitpick found no counterexample. 

502 
\postw 

503 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

504 
On any finite set $N$, \textit{Suc} is a partial function; for example, if $N = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

505 
\{0, 1, \ldots, k\}$, then \textit{Suc} is $\{0 \mapsto 1,\, 1 \mapsto 2,\, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

506 
\ldots,\, k \mapsto \unk\}$, which evaluates to $\unk$ when passed as 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

507 
argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$. The next 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

508 
example is similar: 
33191  509 

510 
\prew 

511 
\textbf{lemma} ``$P~(\textit{op}~{+}\Colon 

512 
\textit{nat}\mathbin{\Rightarrow}\textit{nat}\mathbin{\Rightarrow}\textit{nat})$'' \\ 

513 
\textbf{nitpick} [\textit{card nat} = 1] \\[2\smallskipamount] 

514 
{\slshape Nitpick found a counterexample:} \\[2\smallskipamount] 

515 
\hbox{}\qquad Free variable: \nopagebreak \\ 

46105  516 
\hbox{}\qquad\qquad $P = \unkef(\unkef(0 := \unkef(0 := 0)) := \mathit{False})$ \\[2\smallskipamount] 
33191  517 
\textbf{nitpick} [\textit{card nat} = 2] \\[2\smallskipamount] 
518 
{\slshape Nitpick found no counterexample.} 

519 
\postw 

520 

521 
The problem here is that \textit{op}~+ is total when \textit{nat} is taken to be 

46105  522 
$\{0\}$ but becomes partial as soon as we add $1$, because 
523 
$1 + 1 \notin \{0, 1\}$. 

33191  524 

525 
Because numbers are infinite and are approximated using a threevalued logic, 

526 
there is usually no need to systematically enumerate domain sizes. If Nitpick 

527 
cannot find a genuine counterexample for \textit{card~nat}~= $k$, it is very 

528 
unlikely that one could be found for smaller domains. (The $P~(\textit{op}~{+})$ 

529 
example above is an exception to this principle.) Nitpick nonetheless enumerates 

38181  530 
all cardinalities from 1 to 10 for \textit{nat}, mainly because smaller 
33191  531 
cardinalities are fast to handle and give rise to simpler counterexamples. This 
532 
is explained in more detail in \S\ref{scopemonotonicity}. 

533 

534 
\subsection{Inductive Datatypes} 

535 
\label{inductivedatatypes} 

536 

537 
Like natural numbers and integers, inductive datatypes with recursive 

538 
constructors admit no finite models and must be approximated by a subtermclosed 

539 
subset. For example, using a cardinality of 10 for ${'}a~\textit{list}$, 

540 
Nitpick looks for all counterexamples that can be built using at most 10 

541 
different lists. 

542 

543 
Let's see with an example involving \textit{hd} (which returns the first element 

544 
of a list) and $@$ (which concatenates two lists): 

545 

546 
\prew 

46105  547 
\textbf{lemma} ``$\textit{hd}~(\textit{xs} \mathbin{@} [y, y]) = \textit{hd}~\textit{xs\/}$'' \\ 
33191  548 
\textbf{nitpick} \\[2\smallskipamount] 
549 
\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount] 

550 
\hbox{}\qquad Free variables: \nopagebreak \\ 

551 
\hbox{}\qquad\qquad $\textit{xs} = []$ \\ 

35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

552 
\hbox{}\qquad\qquad $\textit{y} = a_1$ 
33191  553 
\postw 
554 

555 
To see why the counterexample is genuine, we enable \textit{show\_consts} 

556 
and \textit{show\_\allowbreak datatypes}: 

557 

558 
\prew 

55892  559 
{\slshape Type:} \\ 
35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

560 
\hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_1],\, [a_1, a_1],\, \unr\}$ \\ 
33191  561 
{\slshape Constants:} \\ 
46105  562 
\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \unkef([] := [a_1, a_1])$ \\ 
563 
\hbox{}\qquad $\textit{hd} = \unkef([] := a_2,\> [a_1] := a_1,\> [a_1, a_1] := a_1)$ 

33191  564 
\postw 
565 

566 
Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value, 

567 
including $a_2$. 

568 

569 
The second constant, $\lambda x_1.\; x_1 \mathbin{@} [y, y]$, is simply the 

35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

570 
append operator whose second argument is fixed to be $[y, y]$. Appending $[a_1, 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

571 
a_1]$ to $[a_1]$ would normally give $[a_1, a_1, a_1]$, but this value is not 
33191  572 
representable in the subset of $'a$~\textit{list} considered by Nitpick, which 
55892  573 
is shown under the ``Type'' heading; hence the result is $\unk$. Similarly, 
35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

574 
appending $[a_1, a_1]$ to itself gives $\unk$. 
33191  575 

576 
Given \textit{card}~$'a = 3$ and \textit{card}~$'a~\textit{list} = 3$, Nitpick 

577 
considers the following subsets: 

578 

579 
\kern.5\smallskipamount %% TYPESETTING 

580 

581 
\prew 

582 
\begin{multicols}{3} 

583 
$\{[],\, [a_1],\, [a_2]\}$; \\ 

584 
$\{[],\, [a_1],\, [a_3]\}$; \\ 

585 
$\{[],\, [a_2],\, [a_3]\}$; \\ 

586 
$\{[],\, [a_1],\, [a_1, a_1]\}$; \\ 

587 
$\{[],\, [a_1],\, [a_2, a_1]\}$; \\ 

588 
$\{[],\, [a_1],\, [a_3, a_1]\}$; \\ 

589 
$\{[],\, [a_2],\, [a_1, a_2]\}$; \\ 

590 
$\{[],\, [a_2],\, [a_2, a_2]\}$; \\ 

591 
$\{[],\, [a_2],\, [a_3, a_2]\}$; \\ 

592 
$\{[],\, [a_3],\, [a_1, a_3]\}$; \\ 

593 
$\{[],\, [a_3],\, [a_2, a_3]\}$; \\ 

594 
$\{[],\, [a_3],\, [a_3, a_3]\}$. 

595 
\end{multicols} 

596 
\postw 

597 

598 
\kern2\smallskipamount %% TYPESETTING 

599 

600 
All subtermclosed subsets of $'a~\textit{list}$ consisting of three values 

601 
are listed and only those. As an example of a nonsubtermclosed subset, 

35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

602 
consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_2]\}$, and observe 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

603 
that $[a_1, a_2]$ (i.e., $a_1 \mathbin{\#} [a_2]$) has $[a_2] \notin 
33191  604 
\mathcal{S}$ as a subterm. 
605 

606 
Here's another m\"ochtegernlemma that Nitpick can refute without a blink: 

607 

608 
\prew 

609 
\textbf{lemma} ``$\lbrakk \textit{length}~\textit{xs} = 1;\> \textit{length}~\textit{ys} = 1 

46105  610 
\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys\/}$'' 
33191  611 
\\ 
55889  612 
\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount] 
33191  613 
\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount] 
614 
\hbox{}\qquad Free variables: \nopagebreak \\ 

46105  615 
\hbox{}\qquad\qquad $\textit{xs} = [a_2]$ \\ 
616 
\hbox{}\qquad\qquad $\textit{ys} = [a_1]$ \\ 

55892  617 
\hbox{}\qquad Types: \\ 
33191  618 
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\ 
35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

619 
\hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_1],\, [a_2],\, \unr\}$ 
33191  620 
\postw 
621 

622 
Because datatypes are approximated using a threevalued logic, there is usually 

623 
no need to systematically enumerate cardinalities: If Nitpick cannot find a 

624 
genuine counterexample for \textit{card}~$'a~\textit{list}$~= 10, it is very 

625 
unlikely that one could be found for smaller cardinalities. 

626 

35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

627 
\subsection{Typedefs, Quotient Types, Records, Rationals, and Reals} 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

628 
\label{typedefsquotienttypesrecordsrationalsandreals} 
33191  629 

630 
Nitpick generally treats types declared using \textbf{typedef} as datatypes 

631 
whose single constructor is the corresponding \textit{Abs\_\kern.1ex} function. 

632 
For example: 

633 

634 
\prew 

635 
\textbf{typedef}~\textit{three} = ``$\{0\Colon\textit{nat},\, 1,\, 2\}$'' \\ 

636 
\textbf{by}~\textit{blast} \\[2\smallskipamount] 

637 
\textbf{definition}~$A \mathbin{\Colon} \textit{three}$ \textbf{where} ``\kern.1em$A \,\equiv\, \textit{Abs\_\allowbreak three}~0$'' \\ 

638 
\textbf{definition}~$B \mathbin{\Colon} \textit{three}$ \textbf{where} ``$B \,\equiv\, \textit{Abs\_three}~1$'' \\ 

639 
\textbf{definition}~$C \mathbin{\Colon} \textit{three}$ \textbf{where} ``$C \,\equiv\, \textit{Abs\_three}~2$'' \\[2\smallskipamount] 

46105  640 
\textbf{lemma} ``$\lbrakk A \in X;\> B \in X\rbrakk \,\Longrightarrow\, c \in X$'' \\ 
55889  641 
\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount] 
33191  642 
\slshape Nitpick found a counterexample: \\[2\smallskipamount] 
643 
\hbox{}\qquad Free variables: \nopagebreak \\ 

46105  644 
\hbox{}\qquad\qquad $X = \{\Abs{0},\, \Abs{1}\}$ \\ 
645 
\hbox{}\qquad\qquad $c = \Abs{2}$ \\ 

55892  646 
\hbox{}\qquad Types: \\ 
33191  647 
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\ 
35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

648 
\hbox{}\qquad\qquad $\textit{three} = \{\Abs{0},\, \Abs{1},\, \Abs{2},\, \unr\}$ 
33191  649 
\postw 
650 

651 
In the output above, $\Abs{n}$ abbreviates $\textit{Abs\_three}~n$. 

652 

35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

653 
Quotient types are handled in much the same way. The following fragment defines 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

654 
the integer type \textit{my\_int} by encoding the integer $x$ by a pair of 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

655 
natural numbers $(m, n)$ such that $x + n = m$: 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

656 

9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

657 
\prew 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

658 
\textbf{fun} \textit{my\_int\_rel} \textbf{where} \\ 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

659 
``$\textit{my\_int\_rel}~(x,\, y)~(u,\, v) = (x + v = u + y)$'' \\[2\smallskipamount] 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

660 
% 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

661 
\textbf{quotient\_type}~\textit{my\_int} = ``$\textit{nat} \times \textit{nat\/}$''$\;{/}\;$\textit{my\_int\_rel} \\ 
46105  662 
\textbf{by}~(\textit{auto simp add\/}:\ \textit{equivp\_def fun\_eq\_iff}) \\[2\smallskipamount] 
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

663 
% 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

664 
\textbf{definition}~\textit{add\_raw}~\textbf{where} \\ 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

665 
``$\textit{add\_raw} \,\equiv\, \lambda(x,\, y)~(u,\, v).\; (x + (u\Colon\textit{nat}), y + (v\Colon\textit{nat}))$'' \\[2\smallskipamount] 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

666 
% 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

667 
\textbf{quotient\_definition} ``$\textit{add\/}\Colon\textit{my\_int} \Rightarrow \textit{my\_int} \Rightarrow \textit{my\_int\/}$'' \textbf{is} \textit{add\_raw} \\[2\smallskipamount] 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

668 
% 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

669 
\textbf{lemma} ``$\textit{add}~x~y = \textit{add}~x~x$'' \\ 
55889  670 
\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount] 
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

671 
\slshape Nitpick found a counterexample: \\[2\smallskipamount] 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

672 
\hbox{}\qquad Free variables: \nopagebreak \\ 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

673 
\hbox{}\qquad\qquad $x = \Abs{(0,\, 0)}$ \\ 
46105  674 
\hbox{}\qquad\qquad $y = \Abs{(0,\, 1)}$ \\ 
55892  675 
\hbox{}\qquad Types: \\ 
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

676 
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, \unr\}$ \\ 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

677 
\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat}~[\textsl{boxed\/}] = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\ 
46105  678 
\hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(0,\, 1)},\> \unr\}$ 
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

679 
\postw 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

680 

46105  681 
The values $\Abs{(0,\, 0)}$ and $\Abs{(0,\, 1)}$ represent the 
682 
integers $0$ and $1$, respectively. Other representants would have been 

683 
possiblee.g., $\Abs{(5,\, 5)}$ and $\Abs{(11,\, 12)}$. If we are going to 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

684 
use \textit{my\_int} extensively, it pays off to install a term postprocessor 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

685 
that converts the pair notation to the standard mathematical notation: 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

686 

77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

687 
\prew 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

688 
$\textbf{ML}~\,\{{*} \\ 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

689 
\!\begin{aligned}[t] 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

690 
%& ({*}~\,\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \\[2pt] 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

691 
%& \phantom{(*}~\,{\rightarrow}\;\textit{term}~\,{*}) \\[2pt] 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

692 
& \textbf{fun}\,~\textit{my\_int\_postproc}~\_~\_~\_~T~(\textit{Const}~\_~\$~(\textit{Const}~\_~\$~\textit{t1}~\$~\textit{t2\/})) = {} \\[2pt] 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

693 
& \phantom{fun}\,~\textit{HOLogic.mk\_number}~T~(\textit{snd}~(\textit{HOLogic.dest\_number~t1}) \\[2pt] 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

694 
& \phantom{fun\,~\textit{HOLogic.mk\_number}~T~(}{}~\textit{snd}~(\textit{HOLogic.dest\_number~t2\/})) \\[2pt] 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

695 
& \phantom{fun}\!{\mid}\,~\textit{my\_int\_postproc}~\_~\_~\_~\_~t = t \\[2pt] 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

696 
{*}\}\end{aligned}$ \\[2\smallskipamount] 
38284
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38274
diff
changeset

697 
$\textbf{declaration}~\,\{{*} \\ 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

698 
\!\begin{aligned}[t] 
38284
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38274
diff
changeset

699 
& \textit{Nitpick\_Model.register\_term\_postprocessor}~\!\begin{aligned}[t] 
38241  700 
& @\{\textrm{typ}~\textit{my\_int}\} \\[2pt] 
701 
& \textit{my\_int\_postproc}\end{aligned} \\[2pt] 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

702 
{*}\}\end{aligned}$ 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

703 
\postw 
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

704 

46105  705 
Records are handled as datatypes with a single constructor: 
33191  706 

707 
\prew 

708 
\textbf{record} \textit{point} = \\ 

709 
\hbox{}\quad $\textit{Xcoord} \mathbin{\Colon} \textit{int}$ \\ 

710 
\hbox{}\quad $\textit{Ycoord} \mathbin{\Colon} \textit{int}$ \\[2\smallskipamount] 

711 
\textbf{lemma} ``$\textit{Xcoord}~(p\Colon\textit{point}) = \textit{Xcoord}~(q\Colon\textit{point})$'' \\ 

55889  712 
\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount] 
33191  713 
\slshape Nitpick found a counterexample: \\[2\smallskipamount] 
714 
\hbox{}\qquad Free variables: \nopagebreak \\ 

35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

715 
\hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\ 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

716 
\hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\ 
55892  717 
\hbox{}\qquad Types: \\ 
33191  718 
\hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, \unr\}$ \\ 
35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

719 
\hbox{}\qquad\qquad $\textit{point} = \{\!\begin{aligned}[t] 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

720 
& \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr, \\[2pt] %% TYPESETTING 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

721 
& \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$ 
33191  722 
\postw 
723 

724 
Finally, Nitpick provides rudimentary support for rationals and reals using a 

725 
similar approach: 

726 

727 
\prew 

728 
\textbf{lemma} ``$4 * x + 3 * (y\Colon\textit{real}) \not= 1/2$'' \\ 

55889  729 
\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount] 
33191  730 
\slshape Nitpick found a counterexample: \\[2\smallskipamount] 
731 
\hbox{}\qquad Free variables: \nopagebreak \\ 

732 
\hbox{}\qquad\qquad $x = 1/2$ \\ 

733 
\hbox{}\qquad\qquad $y = 1/2$ \\ 

55892  734 
\hbox{}\qquad Types: \\ 
33191  735 
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, 3,\, 4,\, 5,\, 6,\, 7,\, \unr\}$ \\ 
46105  736 
\hbox{}\qquad\qquad $\textit{int} = \{3,\, 2,\, 1,\, 0,\, 1,\, 2,\, 3,\, 4,\, \unr\}$ \\ 
737 
\hbox{}\qquad\qquad $\textit{real} = \{3/2,\, 1/2,\, 0,\, 1/2,\, 1,\, 2,\, 3,\, 4,\, \unr\}$ 

33191  738 
\postw 
739 

740 
\subsection{Inductive and Coinductive Predicates} 

741 
\label{inductiveandcoinductivepredicates} 

742 

743 
Inductively defined predicates (and sets) are particularly problematic for 

744 
counterexample generators. They can make Quickcheck~\cite{berghofernipkow2004} 

745 
loop forever and Refute~\cite{weber2008} run out of resources. The crux of 

38176  746 
the problem is that they are defined using a least fixedpoint construction. 
33191  747 

748 
Nitpick's philosophy is that not all inductive predicates are equal. Consider 

749 
the \textit{even} predicate below: 

750 

751 
\prew 

752 
\textbf{inductive}~\textit{even}~\textbf{where} \\ 

753 
``\textit{even}~0'' $\,\mid$ \\ 

754 
``\textit{even}~$n\,\Longrightarrow\, \textit{even}~(\textit{Suc}~(\textit{Suc}~n))$'' 

755 
\postw 

756 

757 
This predicate enjoys the desirable property of being wellfounded, which means 

758 
that the introduction rules don't give rise to infinite chains of the form 

759 

760 
\prew 

761 
$\cdots\,\Longrightarrow\, \textit{even}~k'' 

762 
\,\Longrightarrow\, \textit{even}~k' 

763 
\,\Longrightarrow\, \textit{even}~k.$ 

764 
\postw 

765 

766 
For \textit{even}, this is obvious: Any chain ending at $k$ will be of length 

767 
$k/2 + 1$: 

768 

769 
\prew 

770 
$\textit{even}~0\,\Longrightarrow\, \textit{even}~2\,\Longrightarrow\, \cdots 

771 
\,\Longrightarrow\, \textit{even}~(k  2) 

772 
\,\Longrightarrow\, \textit{even}~k.$ 

773 
\postw 

774 

775 
Wellfoundedness is desirable because it enables Nitpick to use a very efficient 

38176  776 
fixedpoint computation.% 
33191  777 
\footnote{If an inductive predicate is 
778 
wellfounded, then it has exactly one fixed point, which is simultaneously the 

779 
least and the greatest fixed point. In these circumstances, the computation of 

780 
the least fixed point amounts to the computation of an arbitrary fixed point, 

781 
which can be performed using a straightforward recursive equation.} 

782 
Moreover, Nitpick can prove wellfoundedness of most wellfounded predicates, 

783 
just as Isabelle's \textbf{function} package usually discharges termination 

784 
proof obligations automatically. 

785 

786 
Let's try an example: 

787 

788 
\prew 

789 
\textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\ 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

790 
\textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount] 
33191  791 
\slshape The inductive predicate ``\textit{even}'' was proved wellfounded. 
792 
Nitpick can compute it efficiently. \\[2\smallskipamount] 

793 
Trying 1 scope: \\ 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

794 
\hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount] 
46105  795 
Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported fragment. Only 
796 
potentially spurious counterexamples may be found. \\[2\smallskipamount] 

41992
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

797 
Nitpick found a potentially spurious counterexample for \textit{card nat}~= 50: \\[2\smallskipamount] 
33191  798 
\hbox{}\qquad Empty assignment \\[2\smallskipamount] 
46105  799 
Nitpick could not find a better counterexample. It checked 1 of 1 scope. \\[2\smallskipamount] 
800 
Total time: 1.62 s. 

33191  801 
\postw 
802 

803 
No genuine counterexample is possible because Nitpick cannot rule out the 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

804 
existence of a natural number $n \ge 50$ such that both $\textit{even}~n$ and 
33191  805 
$\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the 
806 
existential quantifier: 

807 

808 
\prew 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

809 
\textbf{lemma} ``$\exists n \mathbin{\le} 49.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\ 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

810 
\textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}] \\[2\smallskipamount] 
33191  811 
\slshape Nitpick found a counterexample: \\[2\smallskipamount] 
812 
\hbox{}\qquad Empty assignment 

813 
\postw 

814 

815 
So far we were blessed by the wellfoundedness of \textit{even}. What happens if 

816 
we use the following definition instead? 

817 

818 
\prew 

819 
\textbf{inductive} $\textit{even}'$ \textbf{where} \\ 

820 
``$\textit{even}'~(0{\Colon}\textit{nat})$'' $\,\mid$ \\ 

821 
``$\textit{even}'~2$'' $\,\mid$ \\ 

822 
``$\lbrakk\textit{even}'~m;\> \textit{even}'~n\rbrakk \,\Longrightarrow\, \textit{even}'~(m + n)$'' 

823 
\postw 

824 

825 
This definition is not wellfounded: From $\textit{even}'~0$ and 

826 
$\textit{even}'~0$, we can derive that $\textit{even}'~0$. Nonetheless, the 

827 
predicates $\textit{even}$ and $\textit{even}'$ are equivalent. 

828 

829 
Let's check a property involving $\textit{even}'$. To make up for the 

830 
foreseeable computational hurdles entailed by nonwellfoundedness, we decrease 

831 
\textit{nat}'s cardinality to a mere 10: 

832 

833 
\prew 

834 
\textbf{lemma}~``$\exists n \in \{0, 2, 4, 6, 8\}.\; 

835 
\lnot\;\textit{even}'~n$'' \\ 

836 
\textbf{nitpick}~[\textit{card nat}~= 10,\, \textit{verbose},\, \textit{show\_consts}] \\[2\smallskipamount] 

837 
\slshape 

838 
The inductive predicate ``$\textit{even}'\!$'' could not be proved wellfounded. 

839 
Nitpick might need to unroll it. \\[2\smallskipamount] 

840 
Trying 6 scopes: \\ 

841 
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 0; \\ 

842 
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 1; \\ 

843 
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2; \\ 

844 
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 4; \\ 

845 
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 8; \\ 

846 
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 9. \\[2\smallskipamount] 

847 
Nitpick found a counterexample for \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2: \\[2\smallskipamount] 

848 
\hbox{}\qquad Constant: \nopagebreak \\ 

46105  849 
\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\unkef(\!\begin{aligned}[t] 
850 
& 0 := \unkef(0 := \textit{True},\, 2 := \textit{True}),\, \\[2pt] 

851 
& 1 := \unkef(0 := \textit{True},\, 2 := \textit{True},\, 4 := \textit{True}),\, \\[2pt] 

852 
& 2 := \unkef(0 := \textit{True},\, 2 := \textit{True},\, 4 := \textit{True},\, \\[2pt] 

853 
& \phantom{2 := \unkef(}6 := \textit{True},\, 8 := \textit{True}))\end{aligned}$ \\[2\smallskipamount] 

854 
Total time: 1.87 s. 

33191  855 
\postw 
856 

857 
Nitpick's output is very instructive. First, it tells us that the predicate is 

858 
unrolled, meaning that it is computed iteratively from the empty set. Then it 

859 
lists six scopes specifying different bounds on the numbers of iterations:\ 0, 

860 
1, 2, 4, 8, and~9. 

861 

862 
The output also shows how each iteration contributes to $\textit{even}'$. The 

863 
notation $\lambda i.\; \textit{even}'$ indicates that the value of the 

864 
predicate depends on an iteration counter. Iteration 0 provides the basis 

865 
elements, $0$ and $2$. Iteration 1 contributes $4$ ($= 2 + 2$). Iteration 2 

866 
throws $6$ ($= 2 + 4 = 4 + 2$) and $8$ ($= 4 + 4$) into the mix. Further 

867 
iterations would not contribute any new elements. 

46105  868 
The predicate $\textit{even}'$ evaluates to either \textit{True} or $\unk$, 
869 
never \textit{False}. 

870 

871 
%Some values are marked with superscripted question 

872 
%marks~(`\lower.2ex\hbox{$^\Q$}'). These are the elements for which the 

873 
%predicate evaluates to $\unk$. 

33191  874 

38181  875 
When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, 20, 24, and 28 
33191  876 
iterations. However, these numbers are bounded by the cardinality of the 
877 
predicate's domain. With \textit{card~nat}~= 10, no more than 9 iterations are 

878 
ever needed to compute the value of a \textit{nat} predicate. You can specify 

879 
the number of iterations using the \textit{iter} option, as explained in 

880 
\S\ref{scopeofsearch}. 

881 

882 
In the next formula, $\textit{even}'$ occurs both positively and negatively: 

883 

884 
\prew 

885 
\textbf{lemma} ``$\textit{even}'~(n  2) \,\Longrightarrow\, \textit{even}'~n$'' \\ 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34038
diff
changeset

886 
\textbf{nitpick} [\textit{card nat} = 10, \textit{show\_consts}] \\[2\smallskipamount] 
33191  887 
\slshape Nitpick found a counterexample: \\[2\smallskipamount] 
888 
\hbox{}\qquad Free variable: \nopagebreak \\ 

889 
\hbox{}\qquad\qquad $n = 1$ \\ 

890 
\hbox{}\qquad Constants: \nopagebreak \\ 

46105  891 
\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\unkef(\!\begin{aligned}[t] 
892 
& 0 := \unkef(0 := \mathit{True},\, 2 := \mathit{True}))\end{aligned}$ \\ 

893 
\hbox{}\qquad\qquad $\textit{even}' \leq \unkef(\!\begin{aligned}[t] 

894 
& 0 := \mathit{True},\, 1 := \mathit{False},\, 2 := \mathit{True},\, \\[2pt] 

895 
& 4 := \mathit{True},\, 6 := \mathit{True},\, 8 := \mathit{True})\end{aligned}$ 

33191  896 
\postw 
897 

46105  898 
Notice the special constraint $\textit{even}' \leq \ldots$ in the output, whose 
899 
righthand side represents an arbitrary fixed point (not necessarily the least 

900 
one). It is used to falsify $\textit{even}'~n$. In contrast, the unrolled 

901 
predicate is used to satisfy $\textit{even}'~(n  2)$. 

33191  902 

903 
Coinductive predicates are handled dually. For example: 

904 

905 
\prew 

906 
\textbf{coinductive} \textit{nats} \textbf{where} \\ 

907 
``$\textit{nats}~(x\Colon\textit{nat}) \,\Longrightarrow\, \textit{nats}~x$'' \\[2\smallskipamount] 

46074  908 
\textbf{lemma} ``$\textit{nats} = (\lambda n.\; n \mathbin\in \{0, 1, 2, 3, 4\})$'' \\ 
33191  909 
\textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount] 
910 
\slshape Nitpick found a counterexample: 

911 
\\[2\smallskipamount] 

912 
\hbox{}\qquad Constants: \nopagebreak \\ 

46105  913 
\hbox{}\qquad\qquad $\lambda i.\; \textit{nats} = \unkef(0 := \unkef,\, 1 := \unkef,\, 2 := \unkef)$ \\ 
914 
\hbox{}\qquad\qquad $\textit{nats} \geq \unkef(3 := \textit{True},\, 4 := \textit{False},\, 5 := \textit{True})$ 

33191  915 
\postw 
916 

917 
As a special case, Nitpick uses Kodkod's transitive closure operator to encode 

918 
negative occurrences of nonwellfounded ``linear inductive predicates,'' i.e., 

919 
inductive predicates for which each the predicate occurs in at most one 

920 
assumption of each introduction rule. For example: 

921 

922 
\prew 

923 
\textbf{inductive} \textit{odd} \textbf{where} \\ 

924 
``$\textit{odd}~1$'' $\,\mid$ \\ 

925 
``$\lbrakk \textit{odd}~m;\>\, \textit{even}~n\rbrakk \,\Longrightarrow\, \textit{odd}~(m + n)$'' \\[2\smallskipamount] 

926 
\textbf{lemma}~``$\textit{odd}~n \,\Longrightarrow\, \textit{odd}~(n  2)$'' \\ 

46105  927 
\textbf{nitpick}~[\textit{card nat} = 4,\, \textit{show\_consts}] \\[2\smallskipamount] 
33191  928 
\slshape Nitpick found a counterexample: 
929 
\\[2\smallskipamount] 

930 
\hbox{}\qquad Free variable: \nopagebreak \\ 

931 
\hbox{}\qquad\qquad $n = 1$ \\ 

932 
\hbox{}\qquad Constants: \nopagebreak \\ 

46105  933 
\hbox{}\qquad\qquad $\textit{even} = (Î»x. ?)(0 := True, 1 := False, 2 := True, 3 := False)$ \\ 
934 
\hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = {}$ \\ 

935 
\hbox{}\qquad\qquad\quad $\unkef(0 := \textit{False},\, 1 := \textit{True},\, 2 := \textit{False},\, 3 := \textit{False})$ \\ 

936 
\hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \unkef$\\ 

937 
\hbox{}\qquad\qquad\quad $( 

33191  938 
\!\begin{aligned}[t] 
46105  939 
& 0 := \unkef(0 := \textit{True},\, 1 := \textit{False},\, 2 := \textit{True},\, 3 := \textit{False}), \\[2pt] 
940 
& 1 := \unkef(0 := \textit{False},\, 1 := \textit{True},\, 2 := \textit{False},\, 3 := \textit{True}), \\[2pt] 

941 
& 2 := \unkef(0 := \textit{False},\, 1 := \textit{False},\, 2 := \textit{True},\, 3 := \textit{False}), \\[2pt] 

942 
& 3 := \unkef(0 := \textit{False},\, 1 := \textit{False},\, 2 := \textit{False},\, 3 := \textit{True})) 

943 
\end{aligned}$ \\ 

944 
\hbox{}\qquad\qquad $\textit{odd} \leq \unkef(0 := \textit{False},\, 1 := \textit{True},\, 2 := \textit{False},\, 3 := \textit{True})$ 

33191  945 
\postw 
946 

947 
\noindent 

948 
In the output, $\textit{odd}_{\textrm{base}}$ represents the base elements and 

949 
$\textit{odd}_{\textrm{step}}$ is a transition relation that computes new 

950 
elements from known ones. The set $\textit{odd}$ consists of all the values 

951 
reachable through the reflexive transitive closure of 

952 
$\textit{odd}_{\textrm{step}}$ starting with any element from 

46105  953 
$\textit{odd}_{\textrm{base}}$, namely 1 and 3. Using Kodkod's 
33191  954 
transitive closure to encode linear predicates is normally either more thorough 
955 
or more efficient than unrolling (depending on the value of \textit{iter}), but 

46105  956 
you can disable it by passing the \textit{dont\_star\_linear\_preds} option. 
33191  957 

958 
\subsection{Coinductive Datatypes} 

959 
\label{coinductivedatatypes} 

960 

53808  961 
A coinductive datatype is similar to an inductive datatype but 
33191  962 
allows infinite objects. Thus, the infinite lists $\textit{ps}$ $=$ $[a, a, a, 
963 
\ldots]$, $\textit{qs}$ $=$ $[a, b, a, b, \ldots]$, and $\textit{rs}$ $=$ $[0, 

53809  964 
1, 2, 3, \ldots]$ can be defined as coinductive lists, or ``lazy lists,'' using the 
33191  965 
$\textit{LNil}\mathbin{\Colon}{'}a~\textit{llist}$ and 
966 
$\textit{LCons}\mathbin{\Colon}{'}a \mathbin{\Rightarrow} {'}a~\textit{llist} 

967 
\mathbin{\Rightarrow} {'}a~\textit{llist}$ constructors. 

968 

969 
Although it is otherwise no friend of infinity, Nitpick can find counterexamples 

970 
involving cyclic lists such as \textit{ps} and \textit{qs} above as well as 

971 
finite lists: 

972 

973 
\prew 

53808  974 
\textbf{codatatype} $'a$ \textit{llist} = \textit{LNil}~$\mid$~\textit{LCons}~$'a$~``$'a\;\textit{llist}$'' \\[2\smallskipamount] 
46105  975 
\textbf{lemma} ``$\textit{xs} \not= \textit{LCons}~a~\textit{xs\/}$'' \\ 
33191  976 
\textbf{nitpick} \\[2\smallskipamount] 
977 
\slshape Nitpick found a counterexample for {\itshape card}~$'a$ = 1: \\[2\smallskipamount] 

978 
\hbox{}\qquad Free variables: \nopagebreak \\ 

979 
\hbox{}\qquad\qquad $\textit{a} = a_1$ \\ 

980 
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ 

981 
\postw 

982 

983 
The notation $\textrm{THE}~\omega.\; \omega = t(\omega)$ stands 

984 
for the infinite term $t(t(t(\ldots)))$. Hence, \textit{xs} is simply the 

985 
infinite list $[a_1, a_1, a_1, \ldots]$. 

986 

987 
The next example is more interesting: 

988 

989 
\prew 

53812  990 
\textbf{primcorec}~$\textit{iterates}$~\textbf{where} \\ 
991 
``$\textit{iterates}~f\>a = \textit{LCons}~a~(\textit{iterates}~f\>(f\>a))$'' \\[2\smallskipamount] 

33191  992 
\textbf{lemma}~``$\lbrakk\textit{xs} = \textit{LCons}~a~\textit{xs};\>\, 
46105  993 
\textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys\/}$'' \\ 
33191  994 
\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount] 
46105  995 
\slshape The type $'a$ passed the monotonicity test. Nitpick might be able to skip 
33191  996 
some scopes. \\[2\smallskipamount] 
38181  997 
Trying 10 scopes: \\ 
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

998 
\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 1, 
33191  999 
and \textit{bisim\_depth}~= 0. \\ 
1000 
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount] 

38181  1001 
\hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 10, 
1002 
and \textit{bisim\_depth}~= 9. \\[2\smallskipamount] 

33191  1003 
Nitpick found a counterexample for {\itshape card}~$'a$ = 2, 
46105  1004 
\textit{card}~``\kern1pt$'a~\textit{llist\/}$''~= 2, and \textit{bisim\_\allowbreak 
33191  1005 
depth}~= 1: 
1006 
\\[2\smallskipamount] 

1007 
\hbox{}\qquad Free variables: \nopagebreak \\ 

35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

1008 
\hbox{}\qquad\qquad $\textit{a} = a_1$ \\ 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

1009 
\hbox{}\qquad\qquad $\textit{b} = a_2$ \\ 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

1010 
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\ 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

1011 
\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount] 
46105  1012 
Total time: 1.11 s. 
33191  1013 
\postw 
1014 

35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

1015 
The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

1016 
$\textit{ys}$ is $[a_2, a_1, a_1, a_1, \ldots]$, i.e., a lassoshaped list with 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

1017 
$[a_2]$ as its stem and $[a_1]$ as its cycle. In general, the list segment 
33191  1018 
within the scope of the {THE} binder corresponds to the lasso's cycle, whereas 
1019 
the segment leading to the binder is the stem. 

1020 

1021 
A salient property of coinductive datatypes is that two objects are considered 

46110  1022 
equal if and only if they lead to the same observations. For example, the two 
1023 
lazy lists 

1024 
% 

1025 
\begin{gather*} 

1026 
\textrm{THE}~\omega.\; \omega = \textit{LCons}~a~(\textit{LCons}~b~\omega) \\ 

1027 
\textit{LCons}~a~(\textrm{THE}~\omega.\; \omega = \textit{LCons}~b~(\textit{LCons}~a~\omega)) 

1028 
\end{gather*} 

1029 
% 

1030 
are identical, because both lead 

33191  1031 
to the sequence of observations $a$, $b$, $a$, $b$, \hbox{\ldots} (or, 
1032 
equivalently, both encode the infinite list $[a, b, a, b, \ldots]$). This 

1033 
concept of equality for coinductive datatypes is called bisimulation and is 

1034 
defined coinductively. 

1035 

1036 
Internally, Nitpick encodes the coinductive bisimilarity predicate as part of 

1037 
the Kodkod problem to ensure that distinct objects lead to different 

1038 
observations. This precaution is somewhat expensive and often unnecessary, so it 

1039 
can be disabled by setting the \textit{bisim\_depth} option to $1$. The 

1040 
bisimilarity check is then performed \textsl{after} the counterexample has been 

1041 
found to ensure correctness. If this afterthefact check fails, the 

35695  1042 
counterexample is tagged as ``quasi genuine'' and Nitpick recommends to try 
46110  1043 
again with \textit{bisim\_depth} set to a nonnegative integer. 
33191  1044 

1045 
The next formula illustrates the need for bisimilarity (either as a Kodkod 

1046 
predicate or as an afterthefact check) to prevent spurious counterexamples: 

1047 

1048 
\prew 

1049 
\textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk 

46105  1050 
\,\Longrightarrow\, \textit{xs} = \textit{ys\/}$'' \\ 
55889  1051 
\textbf{nitpick} [\textit{bisim\_depth} = $1$, \textit{show\_types}] \\[2\smallskipamount] 
35695  1052 
\slshape Nitpick found a quasi genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount] 
33191  1053 
\hbox{}\qquad Free variables: \nopagebreak \\ 
35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

1054 
\hbox{}\qquad\qquad $a = a_1$ \\ 
33191  1055 
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = 
35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

1056 
\textit{LCons}~a_1~\omega$ \\ 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

1057 
\hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\ 
55892  1058 
\hbox{}\qquad Type:\strut \nopagebreak \\ 
33191  1059 
\hbox{}\qquad\qquad $'a~\textit{llist} = 
1060 
\{\!\begin{aligned}[t] 

35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

1061 
& \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega, \\[2pt] 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

1062 
& \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega,\> \unr\}\end{aligned}$ 
33191  1063 
\\[2\smallskipamount] 
1064 
Try again with ``\textit{bisim\_depth}'' set to a nonnegative value to confirm 

1065 
that the counterexample is genuine. \\[2\smallskipamount] 

1066 
{\upshape\textbf{nitpick}} \\[2\smallskipamount] 

1067 
\slshape Nitpick found no counterexample. 

1068 
\postw 

1069 

45083
014342144091
put CryptoMiniSat first and remove warning about unsoundness now that it has been fixed in Kodkod
blanchet
parents:
45080
diff
changeset

1070 
In the first \textbf{nitpick} invocation, the afterthefact check discovered 
46110  1071 
that the two known elements of type $'a~\textit{llist}$ are bisimilar, prompting 
53808  1072 
Nitpick to label the example as only ``quasi genuine.'' 
33191  1073 

1074 
A compromise between leaving out the bisimilarity predicate from the Kodkod 

53808  1075 
problem and performing the afterthefact check is to specify a low 
1076 
nonnegative \textit{bisim\_depth} value. In general, a value of $K$ means that 

1077 
Nitpick will require all lists to be distinguished from each other by their 

1078 
prefixes of length $K$. However, setting $K$ to a too low value can 

1079 
overconstrain Nitpick, preventing it from finding any counterexamples. 

33191  1080 

1081 
\subsection{Boxing} 

1082 
\label{boxing} 

1083 

1084 
Nitpick normally maps function and product types directly to the corresponding 

1085 
Kodkod concepts. As a consequence, if $'a$ has cardinality 3 and $'b$ has 

1086 
cardinality 4, then $'a \times {'}b$ has cardinality 12 ($= 4 \times 3$) and $'a 

1087 
\Rightarrow {'}b$ has cardinality 64 ($= 4^3$). In some circumstances, it pays 

1088 
off to treat these types in the same way as plain datatypes, by approximating 

1089 
them by a subset of a given cardinality. This technique is called ``boxing'' and 

1090 
is particularly useful for functions passed as arguments to other functions, for 

1091 
higharity functions, and for large tuples. Under the hood, boxing involves 

1092 
wrapping occurrences of the types $'a \times {'}b$ and $'a \Rightarrow {'}b$ in 

1093 
isomorphic datatypes, as can be seen by enabling the \textit{debug} option. 

1094 

1095 
To illustrate boxing, we consider a formalization of $\lambda$terms represented 

1096 
using de Bruijn's notation: 

1097 

1098 
\prew 

1099 
\textbf{datatype} \textit{tm} = \textit{Var}~\textit{nat}~$\mid$~\textit{Lam}~\textit{tm} $\mid$ \textit{App~tm~tm} 

1100 
\postw 

1101 

1102 
The $\textit{lift}~t~k$ function increments all variables with indices greater 

1103 
than or equal to $k$ by one: 

1104 

1105 
\prew 

1106 
\textbf{primrec} \textit{lift} \textbf{where} \\ 

1107 
``$\textit{lift}~(\textit{Var}~j)~k = \textit{Var}~(\textrm{if}~j < k~\textrm{then}~j~\textrm{else}~j + 1)$'' $\mid$ \\ 

1108 
``$\textit{lift}~(\textit{Lam}~t)~k = \textit{Lam}~(\textit{lift}~t~(k + 1))$'' $\mid$ \\ 

1109 
``$\textit{lift}~(\textit{App}~t~u)~k = \textit{App}~(\textit{lift}~t~k)~(\textit{lift}~u~k)$'' 

1110 
\postw 

1111 

1112 
The $\textit{loose}~t~k$ predicate returns \textit{True} if and only if 

1113 
term $t$ has a loose variable with index $k$ or more: 

1114 

1115 
\prew 

1116 
\textbf{primrec}~\textit{loose} \textbf{where} \\ 

1117 
``$\textit{loose}~(\textit{Var}~j)~k = (j \ge k)$'' $\mid$ \\ 

1118 
``$\textit{loose}~(\textit{Lam}~t)~k = \textit{loose}~t~(\textit{Suc}~k)$'' $\mid$ \\ 

1119 
``$\textit{loose}~(\textit{App}~t~u)~k = (\textit{loose}~t~k \mathrel{\lor} \textit{loose}~u~k)$'' 

1120 
\postw 

1121 

1122 
Next, the $\textit{subst}~\sigma~t$ function applies the substitution $\sigma$ 

1123 
on $t$: 

1124 

1125 
\prew 

1126 
\textbf{primrec}~\textit{subst} \textbf{where} \\ 

1127 
``$\textit{subst}~\sigma~(\textit{Var}~j) = \sigma~j$'' $\mid$ \\ 

1128 
``$\textit{subst}~\sigma~(\textit{Lam}~t) = {}$\phantom{''} \\ 

1129 
\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$ \\ 

1130 
``$\textit{subst}~\sigma~(\textit{App}~t~u) = \textit{App}~(\textit{subst}~\sigma~t)~(\textit{subst}~\sigma~u)$'' 

1131 
\postw 

1132 

1133 
A substitution is a function that maps variable indices to terms. Observe that 

1134 
$\sigma$ is a function passed as argument and that Nitpick can't optimize it 

1135 
away, because the recursive call for the \textit{Lam} case involves an altered 

1136 
version. Also notice the \textit{lift} call, which increments the variable 

1137 
indices when moving under a \textit{Lam}. 

1138 

1139 
A reasonable property to expect of substitution is that it should leave closed 

1140 
terms unchanged. Alas, even this simple property does not hold: 

1141 

1142 
\pre 

1143 
\textbf{lemma}~``$\lnot\,\textit{loose}~t~0 \,\Longrightarrow\, \textit{subst}~\sigma~t = t$'' \\ 

1144 
\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount] 

1145 
\slshape 

38181  1146 
Trying 10 scopes: \nopagebreak \\ 
46105  1147 
\hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm\/}$'' = 1; \\ 
1148 
\hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm\/}$'' = 2; \\ 

33191  1149 
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount] 
46105  1150 
\hbox{}\qquad \textit{card~nat}~= 10, \textit{card tm}~= 10, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm\/}$'' = 10. \\[2\smallskipamount] 
33191  1151 
Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6, 
46105  1152 
and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm\/}$''~= 6: \\[2\smallskipamount] 
33191  1153 
\hbox{}\qquad Free variables: \nopagebreak \\ 
46105  1154 
\hbox{}\qquad\qquad $\sigma = \unkef(\!\begin{aligned}[t] 
33191  1155 
& 0 := \textit{Var}~0,\> 
1156 
1 := \textit{Var}~0,\> 

1157 
2 := \textit{Var}~0, \\[2pt] 

1158 
& 3 := \textit{Var}~0,\> 

1159 
4 := \textit{Var}~0,\> 

46110  1160 
5 := \textit{Lam}~(\textit{Lam}~(\textit{Var}~0)))\end{aligned}$ \\ 
33191  1161 
\hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount] 
46110  1162 
Total time: 3.08 s. 
33191  1163 
\postw 
1164 

1165 
Using \textit{eval}, we find out that $\textit{subst}~\sigma~t = 

1166 
\textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional 

46110  1167 
$\lambda$calculus notation, $t$ is 
1168 
$\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is (wrongly) $\lambda x\, y.\> y$. 

35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

1169 
The bug is in \textit{subst\/}: The $\textit{lift}~(\sigma~m)~1$ call should be 
33191  1170 
replaced with $\textit{lift}~(\sigma~m)~0$. 
1171 

1172 
An interesting aspect of Nitpick's verbose output is that it assigned inceasing 

46110  1173 
cardinalities from 1 to 10 to the type $\textit{nat} \Rightarrow \textit{tm}$ 
1174 
of the higherorder argument $\sigma$ of \textit{subst}. 

33191  1175 
For the formula of interest, knowing 6 values of that type was enough to find 
46105  1176 
the counterexample. Without boxing, $6^6 = 46\,656$ values must be 
33191  1177 
considered, a hopeless undertaking: 
1178 

1179 
\prew 

1180 
\textbf{nitpick} [\textit{dont\_box}] \\[2\smallskipamount] 

38183  1181 
{\slshape Nitpick ran out of time after checking 3 of 10 scopes.} 
33191  1182 
\postw 
1183 

1184 
Boxing can be enabled or disabled globally or on a pertype basis using the 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1185 
\textit{box} option. Nitpick usually performs reasonable choices about which 
46105  1186 
types should be boxed, but option tweaking sometimes helps. 
1187 

1188 
%A related optimization, 

1189 
%``finitization,'' attempts to wrap functions that are constant at all but finitely 

1190 
%many points (e.g., finite sets); see the documentation for the \textit{finitize} 

1191 
%option in \S\ref{scopeofsearch} for details. 

33191  1192 

1193 
\subsection{Scope Monotonicity} 

1194 
\label{scopemonotonicity} 

1195 

1196 
The \textit{card} option (together with \textit{iter}, \textit{bisim\_depth}, 

1197 
and \textit{max}) controls which scopes are actually tested. In general, to 

1198 
exhaust all models below a certain cardinality bound, the number of scopes that 

1199 
Nitpick must consider increases exponentially with the number of type variables 

1200 
(and \textbf{typedecl}'d types) occurring in the formula. Given the default 

38181  1201 
cardinality specification of 110, no fewer than $10^4 = 10\,000$ scopes must be 
33191  1202 
considered for a formula involving $'a$, $'b$, $'c$, and $'d$. 
1203 

1204 
Fortunately, many formulas exhibit a property called \textsl{scope 

1205 
monotonicity}, meaning that if the formula is falsifiable for a given scope, 

1206 
it is also falsifiable for all larger scopes \cite[p.~165]{jackson2006}. 

1207 

1208 
Consider the formula 

1209 

1210 
\prew 

1211 
\textbf{lemma}~``$\textit{length~xs} = \textit{length~ys} \,\Longrightarrow\, \textit{rev}~(\textit{zip~xs~ys}) = \textit{zip~xs}~(\textit{rev~ys})$'' 

1212 
\postw 

1213 

1214 
where \textit{xs} is of type $'a~\textit{list}$ and \textit{ys} is of type 

38181  1215 
$'b~\textit{list}$. A priori, Nitpick would need to consider $1\,000$ scopes to 
38274  1216 
exhaust the specification \textit{card}~= 110 (10 cardinalies for $'a$ 
1217 
$\times$ 10 cardinalities for $'b$ $\times$ 10 cardinalities for the datatypes). 

1218 
However, our intuition tells us that any counterexample found with a small scope 

1219 
would still be a counterexample in a larger scopeby simply ignoring the fresh 

1220 
$'a$ and $'b$ values provided by the larger scope. Nitpick comes to the same 

1221 
conclusion after a careful inspection of the formula and the relevant 

1222 
definitions: 

33191  1223 

1224 
\prew 

1225 
\textbf{nitpick}~[\textit{verbose}] \\[2\smallskipamount] 

1226 
\slshape 

46105  1227 
The types $'a$ and $'b$ passed the monotonicity test. 
33191  1228 
Nitpick might be able to skip some scopes. 
1229 
\\[2\smallskipamount] 

38181  1230 
Trying 10 scopes: \\ 
33191  1231 
\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1, 
1232 
\textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$ 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

1233 
\textit{list\/}''~= 1, \\ 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

1234 
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 1, and 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

1235 
\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 1. \\ 
33191  1236 
\hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2, 
1237 
\textit{card} \textit{nat}~= 2, \textit{card} ``$('a \times {'}b)$ 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

1238 
\textit{list\/}''~= 2, \\ 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

1239 
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 2, and 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

1240 
\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 2. \\ 
33191  1241 
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount] 
38181  1242 
\hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} $'b$~= 10, 
1243 
\textit{card} \textit{nat}~= 10, \textit{card} ``$('a \times {'}b)$ 

1244 
\textit{list\/}''~= 10, \\ 

1245 
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 10, and 

1246 
\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 10. 

33191  1247 
\\[2\smallskipamount] 
1248 
Nitpick found a counterexample for 

1249 
\textit{card} $'a$~= 5, \textit{card} $'b$~= 5, 

1250 
\textit{card} \textit{nat}~= 5, \textit{card} ``$('a \times {'}b)$ 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

1251 
\textit{list\/}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 5, and 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

1252 
\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 5: 
33191  1253 
\\[2\smallskipamount] 
1254 
\hbox{}\qquad Free variables: \nopagebreak \\ 

35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

1255 
\hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\ 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

1256 
\hbox{}\qquad\qquad $\textit{ys} = [b_1, b_1]$ \\[2\smallskipamount] 
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40147
diff
changeset

1257 
Total time: 1.63 s. 
33191  1258 
\postw 
1259 

1260 
In theory, it should be sufficient to test a single scope: 

1261 

1262 
\prew 

38181  1263 
\textbf{nitpick}~[\textit{card}~= 10] 
33191  1264 
\postw 
1265 

1266 
However, this is often less efficient in practice and may lead to overly complex 

1267 
counterexamples. 

1268 

1269 
If the monotonicity check fails but we believe that the formula is monotonic (or 

1270 
we don't mind missing some counterexamples), we can pass the 

1271 
\textit{mono} option. To convince yourself that this option is risky, 

1272 
simply consider this example from \S\ref{skolemization}: 

1273 

1274 
\prew 

1275 
\textbf{lemma} ``$\exists g.\; \forall x\Colon 'b.~g~(f~x) = x 

1276 
\,\Longrightarrow\, \forall y\Colon {'}a.\; \exists x.~y = f~x$'' \\ 

1277 
\textbf{nitpick} [\textit{mono}] \\[2\smallskipamount] 

1278 
{\slshape Nitpick found no counterexample.} \\[2\smallskipamount] 

1279 
\textbf{nitpick} \\[2\smallskipamount] 

1280 
\slshape 

1281 
Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\ 

1282 
\hbox{}\qquad $\vdots$ 

1283 
\postw 

1284 

1285 
(It turns out the formula holds if and only if $\textit{card}~'a \le 

1286 
\textit{card}~'b$.) Although this is rarely advisable, the automatic 

1287 
monotonicity checks can be disabled by passing \textit{non\_mono} 

1288 
(\S\ref{optimizations}). 

1289 

1290 
As insinuated in \S\ref{naturalnumbersandintegers} and 

1291 
\S\ref{inductivedatatypes}, \textit{nat}, \textit{int}, and inductive datatypes 

1292 
are normally monotonic and treated as such. The same is true for record types, 

38274  1293 
\textit{rat}, and \textit{real}. Thus, given the 
38181  1294 
cardinality specification 110, a formula involving \textit{nat}, \textit{int}, 
33191  1295 
\textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to 
46110  1296 
consider only 10~scopes instead of $10^4 = 10\,000$. On the other hand, 
38274  1297 
\textbf{typedef}s and quotient types are generally nonmonotonic. 
33191  1298 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1299 
\subsection{Inductive Properties} 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1300 
\label{inductiveproperties} 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1301 

7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1302 
Inductive properties are a particular pain to prove, because the failure to 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1303 
establish an induction step can mean several things: 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1304 
% 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1305 
\begin{enumerate} 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1306 
\item The property is invalid. 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1307 
\item The property is valid but is too weak to support the induction step. 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1308 
\item The property is valid and strong enough; it's just that we haven't found 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1309 
the proof yet. 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1310 
\end{enumerate} 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1311 
% 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1312 
Depending on which scenario applies, we would take the appropriate course of 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1313 
action: 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1314 
% 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1315 
\begin{enumerate} 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1316 
\item Repair the statement of the property so that it becomes valid. 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1317 
\item Generalize the property and/or prove auxiliary properties. 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1318 
\item Work harder on a proof. 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1319 
\end{enumerate} 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1320 
% 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1321 
How can we distinguish between the three scenarios? Nitpick's normal mode of 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1322 
operation can often detect scenario 1, and Isabelle's automatic tactics help with 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1323 
scenario 3. Using appropriate techniques, it is also often possible to use 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1324 
Nitpick to identify scenario 2. Consider the following transition system, 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1325 
in which natural numbers represent states: 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1326 

7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1327 
\prew 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1328 
\textbf{inductive\_set}~\textit{reach}~\textbf{where} \\ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1329 
``$(4\Colon\textit{nat}) \in \textit{reach\/}$'' $\mid$ \\ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1330 
``$\lbrakk n < 4;\> n \in \textit{reach\/}\rbrakk \,\Longrightarrow\, 3 * n + 1 \in \textit{reach\/}$'' $\mid$ \\ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1331 
``$n \in \textit{reach} \,\Longrightarrow n + 2 \in \textit{reach\/}$'' 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1332 
\postw 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1333 

7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1334 
We will try to prove that only even numbers are reachable: 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1335 

7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1336 
\prew 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1337 
\textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n$'' 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1338 
\postw 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1339 

7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1340 
Does this property hold? Nitpick cannot find a counterexample within 30 seconds, 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1341 
so let's attempt a proof by induction: 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1342 

7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1343 
\prew 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1344 
\textbf{apply}~(\textit{induct~set}{:}~\textit{reach\/}) \\ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1345 
\textbf{apply}~\textit{auto} 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1346 
\postw 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1347 

7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1348 
This leaves us in the following proof state: 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1349 

7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1350 
\prew 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1351 
{\slshape goal (2 subgoals): \\ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1352 
\phantom{0}1. ${\bigwedge}n.\;\, \lbrakk n \in \textit{reach\/};\, n < 4;\, 2~\textsl{dvd}~n\rbrakk \,\Longrightarrow\, 2~\textsl{dvd}~\textit{Suc}~(3 * n)$ \\ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1353 
\phantom{0}2. ${\bigwedge}n.\;\, \lbrakk n \in \textit{reach\/};\, 2~\textsl{dvd}~n\rbrakk \,\Longrightarrow\, 2~\textsl{dvd}~\textit{Suc}~(\textit{Suc}~n)$ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1354 
} 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1355 
\postw 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1356 

7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1357 
If we run Nitpick on the first subgoal, it still won't find any 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1358 
counterexample; and yet, \textit{auto} fails to go further, and \textit{arith} 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1359 
is helpless. However, notice the $n \in \textit{reach}$ assumption, which 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1360 
strengthens the induction hypothesis but is not immediately usable in the proof. 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1361 
If we remove it and invoke Nitpick, this time we get a counterexample: 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1362 

7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1363 
\prew 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1364 
\textbf{apply}~(\textit{thin\_tac}~``$n \in \textit{reach\/}$'') \\ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1365 
\textbf{nitpick} \\[2\smallskipamount] 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1366 
\slshape Nitpick found a counterexample: \\[2\smallskipamount] 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1367 
\hbox{}\qquad Skolem constant: \nopagebreak \\ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1368 
\hbox{}\qquad\qquad $n = 0$ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1369 
\postw 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1370 

7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1371 
Indeed, 0 < 4, 2 divides 0, but 2 does not divide 1. We can use this information 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1372 
to strength the lemma: 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1373 

7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1374 
\prew 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1375 
\textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \not= 0$'' 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
diff
changeset

1376 
\postw 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34126
