author  blanchet 
Mon, 28 Feb 2011 17:53:10 +0100  
changeset 41857  07573743208f 
parent 41804  90dd5291afd8 
child 41875  e3cd0dce9b1a 
permissions  rwrr 
33191  1 
\documentclass[a4paper,12pt]{article} 
2 
\usepackage[T1]{fontenc} 

3 
\usepackage{amsmath} 

4 
\usepackage{amssymb} 

33564
75ce0f60617a
fixed minor problems with Nitpick's documentation
blanchet
parents:
33561
diff
changeset

5 
\usepackage[english,french]{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} 

40689  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{{?}} 

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

30 
\def\undef{(\lambda x.\; \unk)} 
33191  31 
%\def\unr{\textit{others}} 
32 
\def\unr{\ldots} 

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

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

35 

36 
\hyphenation{MiniSat sizechange FirstSteps grandparent nitpick 

37 
counterexample counterexamples datatype datatypes codatatype 

38 
codatatypes inductive coinductive} 

39 

40 
\urlstyle{tt} 

41 

42 
\begin{document} 

43 

33564
75ce0f60617a
fixed minor problems with Nitpick's documentation
blanchet
parents:
33561
diff
changeset

44 
\selectlanguage{english} 
75ce0f60617a
fixed minor problems with Nitpick's documentation
blanchet
parents:
33561
diff
changeset

45 

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

33887  48 
\Large A User's Guide to Nitpick for Isabelle/HOL} 
33191  49 
\author{\hbox{} \\ 
50 
Jasmin Christian Blanchette \\ 

33887  51 
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\ 
33191  52 
\hbox{}} 
53 

54 
\maketitle 

55 

56 
\tableofcontents 

57 

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

59 
\setlength{\parindent}{0pt} 

60 
\setlength{\abovedisplayskip}{\parskip} 

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

62 
\setlength{\belowdisplayskip}{\parskip} 

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

64 

65 
% Generalpurpose enum environment with correct spacing 

66 
\newenvironment{enum}% 

67 
{\begin{list}{}{% 

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

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

70 
\setlength{\itemsep}{\parskip}% 

71 
\advance\itemsep by\parsep}} 

72 
{\end{list}} 

73 

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

75 
\advance\rightskip by\leftmargin} 

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

77 

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

79 
\def\postw{\post} 

80 

81 
\section{Introduction} 

82 
\label{introduction} 

83 

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

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

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

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

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

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

92 
appropriated from a now retired Alloy precursor. 

93 

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

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

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

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

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

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

100 

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

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

103 
write 

104 

105 
\prew 

106 
\textbf{lemma}~``$\textit{False}$'' \\ 

107 
\textbf{nitpick}~[\textit{show\_all}] 

108 
\postw 

109 

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

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

112 
that the axioms might be unsatisfiable. 

113 

36926  114 
You can also invoke Nitpick from the ``Commands'' submenu of the 
115 
``Isabelle'' menu in Proof General or by pressing the Emacs key sequence Cc Ca 

116 
Cn. This is equivalent to entering the \textbf{nitpick} command with no 

117 
arguments in the theory text. 

118 

38517  119 
Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.5 virtual 
40689  120 
machine called \texttt{java}. To run Nitpick, you must also make sure that the 
121 
theory \textit{Nitpick} is importedthis is rarely a problem in practice 

122 
since it is part of \textit{Main}. 

33195
0efe26262e73
updated Nitpick manual to reflect the latest Stand der Dinge
blanchet
parents:
33193
diff
changeset

123 

33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33559
diff
changeset

124 
Throughout this manual, we will explicitly invoke the \textbf{nitpick} command. 
39317  125 
Nitpick also provides an automatic mode that can be enabled via the ``Auto 
126 
Nitpick'' option from the ``Isabelle'' menu in Proof General. In this mode, 

127 
Nitpick is run on every newly entered theorem. The time limit for Auto Nitpick 

128 
and other automatic tools can be set using the ``Auto Tools Time Limit'' option. 

33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33559
diff
changeset

129 

33191  130 
\newbox\boxA 
131 
\setbox\boxA=\hbox{\texttt{nospam}} 

132 

40689  133 
The examples presented in this manual can be found 
134 
in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_Examples/Manual\_Nits.thy} theory. 

33191  135 
The known bugs and limitations at the time of writing are listed in 
136 
\S\ref{knownbugsandlimitations}. Comments and bug reports concerning Nitpick 

137 
or this manual should be directed to 

138 
\texttt{blan{\color{white}nospam}\kern\wd\boxA{}chette@\allowbreak 

139 
in.\allowbreak tum.\allowbreak de}. 

140 

141 
\vskip2.5\smallskipamount 

142 

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

144 
suggesting several textual improvements. 

145 
% and Perry James for reporting a typo. 

146 

36926  147 
%\section{Installation} 
148 
%\label{installation} 

149 
% 

150 
%MISSING: 

151 
% 

152 
% * Nitpick is part of Isabelle/HOL 

153 
% * but it relies on an external tool called Kodkodi (Kodkod wrapper) 

154 
% * Two options: 

155 
% * if you use a prebuilt Isabelle package, Kodkodi is automatically there 

156 
% * if you work from sources, the latest Kodkodi can be obtained from ... 

157 
% download it, install it in some directory of your choice (e.g., 

158 
% $ISABELLE_HOME/contrib/kodkodi), and add the absolute path to Kodkodi 

159 
% in your .isabelle/etc/components file 

160 
% 

161 
% * If you're not sure, just try the example in the next section 

162 

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

163 
\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

164 
\label{firststeps} 
33191  165 

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

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

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

168 
as follows: 
33191  169 

170 
\prew 

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

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

172 
\textbf{imports}~\textit{Main~Quotient\_Product~RealDef} \\ 
33191  173 
\textbf{begin} 
174 
\postw 

175 

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

178 
This was done by adding the line 

33191  179 

180 
\prew 

35710  181 
\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1] 
33191  182 
\postw 
183 

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

185 
Kodkodi and is precompiled for the major platforms. Other SAT solvers can also 

186 
be installed, as explained in \S\ref{optimizations}. If you have already 

187 
configured SAT solvers in Isabelle (e.g., for Refute), these will also be 

188 
available to Nitpick. 

189 

190 
\subsection{Propositional Logic} 

191 
\label{propositionallogic} 

192 

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

194 

195 
\prew 

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

197 
\textbf{nitpick} 

198 
\postw 

199 

200 
You should get the following output: 

201 

202 
\prew 

203 
\slshape 

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

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

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

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

208 
\postw 

209 

36926  210 
%FIXME: If you get the output:... 
211 
%Then do suchandsuch. 

212 

33191  213 
Nitpick can also be invoked on individual subgoals, as in the example below: 
214 

215 
\prew 

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

217 
{\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

218 
\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

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

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

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

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

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

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

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

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

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

230 
\textbf{oops} 

231 
\postw 

232 

233 
\subsection{Type Variables} 

234 
\label{typevariables} 

235 

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

237 
one is more mind and computerboggling: 

238 

239 
\prew 

240 
\textbf{lemma} ``$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$'' 

241 
\postw 

242 
\pagebreak[2] %% TYPESETTING 

243 

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

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

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

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

248 
substituted for {SOME}. 

249 

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

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

38181  252 
variable, up to a given cardinality (10 by default), looking for a finite 
33191  253 
countermodel: 
254 

255 
\prew 

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

257 
\slshape 

38181  258 
Trying 10 scopes: \nopagebreak \\ 
33191  259 
\hbox{}\qquad \textit{card}~$'a$~= 1; \\ 
260 
\hbox{}\qquad \textit{card}~$'a$~= 2; \\ 

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

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

265 
\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\ 

266 
\hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount] 

40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40147
diff
changeset

267 
Total time: 0.76 s. 
33191  268 
\postw 
269 

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

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

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

273 

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

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

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

277 

278 
\prew 

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

280 
\postw 

281 

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

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

284 

285 
\subsection{Constants} 

286 
\label{constants} 

287 

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

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

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

291 
formula: 

292 

293 
\prew 

294 
\textbf{lemma}~``$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$'' \\ 

295 
\textbf{nitpick}~[\textit{show\_consts}] \\[2\smallskipamount] 

296 
\slshape 

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

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

299 
\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\ 

300 
\hbox{}\qquad\qquad $x = a_3$ \\ 

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

39359  302 
\hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$ 
33191  303 
\postw 
304 

39359  305 
As the result of an optimization, Nitpick directly assigned a value to the 
306 
subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we 

307 
disable this optimization by using the command 

33191  308 

309 
\prew 

39359  310 
\textbf{nitpick}~[\textit{dont\_specialize},\, \textit{show\_consts}] 
33191  311 
\postw 
312 

39359  313 
we get \textit{The}: 
33191  314 

315 
\prew 

316 
\slshape Constant: \nopagebreak \\ 

317 
\hbox{}\qquad $\mathit{The} = \undef{} 

318 
(\!\begin{aligned}[t]% 

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

319 
& \{a_1, a_2, a_3\} := a_3,\> \{a_1, a_2\} := a_3,\> \{a_1, a_3\} := a_3, \\[2pt] %% TYPESETTING 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

320 
& \{a_1\} := a_1,\> \{a_2, a_3\} := a_1,\> \{a_2\} := a_2, \\[2pt] 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

321 
& \{a_3\} := a_3,\> \{\} := a_3)\end{aligned}$ 
33191  322 
\postw 
323 

324 
Notice that $\textit{The}~(\lambda y.\;P~y) = \textit{The}~\{a_2, a_3\} = a_1$, 

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

325 
just like before.\footnote{The Isabelle/HOL notation $f(x := 
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

326 
y)$ denotes the function that maps $x$ to $y$ and that otherwise behaves like 
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

327 
$f$.} 
33191  328 

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

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

331 

332 
\prew 

333 
\textbf{lemma}~``$\exists {!}x.\; P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$'' 

334 
\postw 

335 

336 
The fix appears to work: 

337 

338 
\prew 

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

340 
\slshape Nitpick found no counterexample. 

341 
\postw 

342 

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

344 
cardinalities up to 50: 

345 

346 
\prew 

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

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

349 
\texttt{\char`\\\char`\<midarrow\char`\>}.} \\[2\smallskipamount] 

350 
\slshape Nitpick found no counterexample. 

351 
\postw 

352 

38181  353 
Let's see if Sledgehammer can find a proof: 
33191  354 

355 
\prew 

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

357 
{\slshape Sledgehammer: external prover ``$e$'' for subgoal 1: \\ 

358 
$\exists{!}x.\; P~x\,\Longrightarrow\, P~(\hbox{\slshape THE}~y.\; P~y)$ \\ 

359 
Try this command: \textrm{apply}~(\textit{metis~the\_equality})} \\[2\smallskipamount] 

360 
\textbf{apply}~(\textit{metis~the\_equality\/}) \nopagebreak \\[2\smallskipamount] 

361 
{\slshape No subgoals!}% \\[2\smallskipamount] 

362 
%\textbf{done} 

363 
\postw 

364 

365 
This must be our lucky day. 

366 

367 
\subsection{Skolemization} 

368 
\label{skolemization} 

369 

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

371 

372 
\prew 

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

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

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

376 
\slshape 

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

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

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

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

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

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

383 
\postw 

384 

385 
Although $f$ is the only free variable occurring in the formula, Nitpick also 

386 
displays values for the bound variables $g$ and $y$. These values are available 

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

388 

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

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

391 

392 
\prew 

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

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

395 
\slshape 

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

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

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

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

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

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

402 
\postw 

403 

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

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

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

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

408 

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

410 

411 
\prew 

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

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

414 
\slshape 

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

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

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

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

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

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

421 
\postw 

422 

423 
What happened here is that Nitpick expanded the \textit{sym} constant to its 

424 
definition: 

425 

426 
\prew 

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

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

429 
\postw 

430 

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

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

433 
from \textit{sym}'s definition. 

434 

435 
\subsection{Natural Numbers and Integers} 

436 
\label{naturalnumbersandintegers} 

437 

438 
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

439 
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

440 
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

441 
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

442 
Internally, undefined values lead to a threevalued logic. 
33191  443 

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

444 
Here is an example involving \textit{int\/}: 
33191  445 

446 
\prew 

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

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

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

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

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

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

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

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

455 
\postw 

456 

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

457 
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

458 
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

459 
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

460 
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

461 
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

462 
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

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

464 

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

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

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

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

468 

33191  469 
With infinite types, we don't always have the luxury of a genuine counterexample 
470 
and must often content ourselves with a potential one. The tedious task of 

471 
finding out whether the potential counterexample is in fact genuine can be 

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

472 
outsourced to \textit{auto} by passing \textit{check\_potential}. For example: 
33191  473 

474 
\prew 

475 
\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

476 
\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

477 
\slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

478 
fragment. Only potential counterexamples may be found. \\[2\smallskipamount] 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

479 
Nitpick found a potential counterexample: \\[2\smallskipamount] 
33191  480 
\hbox{}\qquad Free variable: \nopagebreak \\ 
481 
\hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount] 

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

483 
\postw 

484 

485 
You might wonder why the counterexample is first reported as potential. The root 

486 
of the problem is that the bound variable in $\forall n.\; \textit{Suc}~n 

487 
\mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds an $n$ such 

488 
that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to 

489 
\textit{False}; but otherwise, it does not know anything about values of $n \ge 

490 
\textit{card~nat}$ and must therefore evaluate the assumption to $\unk$, not 

491 
\textit{True}. Since the assumption can never be satisfied, the putative lemma 

492 
can never be falsified. 

493 

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

495 
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

496 
aware that \textit{auto} will usually fail to prove that the counterexample is 
33191  497 
genuine or spurious. 
498 

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

500 
giant with feet of clay: 

501 

502 
\prew 

503 
\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

504 
\textbf{nitpick} \\[2\smallskipamount] 
33191  505 
\slshape 
506 
Nitpick found no counterexample. 

507 
\postw 

508 

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

509 
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

510 
\{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

511 
\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

512 
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

513 
example is similar: 
33191  514 

515 
\prew 

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

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

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

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

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

521 
\hbox{}\qquad\qquad $P = \{\}$ \\[2\smallskipamount] 

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

523 
{\slshape Nitpick found no counterexample.} 

524 
\postw 

525 

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

527 
$\{0\}$ but becomes partial as soon as we add $1$, because $1 + 1 \notin \{0, 

528 
1\}$. 

529 

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

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

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

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

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

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

538 

539 
\subsection{Inductive Datatypes} 

540 
\label{inductivedatatypes} 

541 

542 
Like natural numbers and integers, inductive datatypes with recursive 

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

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

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

546 
different lists. 

547 

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

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

550 

551 
\prew 

552 
\textbf{lemma} ``$\textit{hd}~(\textit{xs} \mathbin{@} [y, y]) = \textit{hd}~\textit{xs}$'' \\ 

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

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

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

556 
\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

557 
\hbox{}\qquad\qquad $\textit{y} = a_1$ 
33191  558 
\postw 
559 

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

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

562 

563 
\prew 

564 
{\slshape Datatype:} \\ 

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

565 
\hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_1],\, [a_1, a_1],\, \unr\}$ \\ 
33191  566 
{\slshape Constants:} \\ 
35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

567 
\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_1, a_1])$ \\ 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

568 
\hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_1] := a_1,\> [a_1, a_1] := a_1)$ 
33191  569 
\postw 
570 

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

572 
including $a_2$. 

573 

574 
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

575 
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

576 
a_1]$ to $[a_1]$ would normally give $[a_1, a_1, a_1]$, but this value is not 
33191  577 
representable in the subset of $'a$~\textit{list} considered by Nitpick, which 
578 
is shown under the ``Datatype'' 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

579 
appending $[a_1, a_1]$ to itself gives $\unk$. 
33191  580 

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

582 
considers the following subsets: 

583 

584 
\kern.5\smallskipamount %% TYPESETTING 

585 

586 
\prew 

587 
\begin{multicols}{3} 

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

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

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

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

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

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

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

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

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

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

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

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

600 
\end{multicols} 

601 
\postw 

602 

603 
\kern2\smallskipamount %% TYPESETTING 

604 

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

606 
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

607 
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

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

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

612 

613 
\prew 

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

615 
\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' 

616 
\\ 

617 
\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount] 

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

619 
\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

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

621 
\hbox{}\qquad\qquad $\textit{ys} = [a_2]$ \\ 
33191  622 
\hbox{}\qquad Datatypes: \\ 
623 
\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

624 
\hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_1],\, [a_2],\, \unr\}$ 
33191  625 
\postw 
626 

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

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

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

630 
unlikely that one could be found for smaller cardinalities. 

631 

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

632 
\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

633 
\label{typedefsquotienttypesrecordsrationalsandreals} 
33191  634 

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

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

637 
For example: 

638 

639 
\prew 

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

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

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

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

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

645 
\textbf{lemma} ``$\lbrakk P~A;\> P~B\rbrakk \,\Longrightarrow\, P~x$'' \\ 

646 
\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount] 

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

648 
\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

649 
\hbox{}\qquad\qquad $P = \{\Abs{0},\, \Abs{1}\}$ \\ 
33191  650 
\hbox{}\qquad\qquad $x = \Abs{2}$ \\ 
651 
\hbox{}\qquad Datatypes: \\ 

652 
\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

653 
\hbox{}\qquad\qquad $\textit{three} = \{\Abs{0},\, \Abs{1},\, \Abs{2},\, \unr\}$ 
33191  654 
\postw 
655 

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

657 

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

658 
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

659 
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

660 
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

661 

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

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

663 
\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

664 
``$\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

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

666 
\textbf{quotient\_type}~\textit{my\_int} = ``$\textit{nat} \times \textit{nat\/}$''$\;{/}\;$\textit{my\_int\_rel} \\ 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

667 
\textbf{by}~(\textit{auto simp add\/}:\ \textit{equivp\_def expand\_fun\_eq}) \\[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{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

670 
``$\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

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

672 
\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

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

674 
\textbf{lemma} ``$\textit{add}~x~y = \textit{add}~x~x$'' \\ 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

675 
\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount] 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

676 
\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

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

678 
\hbox{}\qquad\qquad $x = \Abs{(0,\, 0)}$ \\ 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

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

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

681 
\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

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

683 
\hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(1,\, 0)},\> \unr\}$ 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

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

685 

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

686 
In the counterexample, $\Abs{(0,\, 0)}$ and $\Abs{(1,\, 0)}$ represent the 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

687 
integers $0$ and $1$, respectively. Other representants would have been 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

688 
possiblee.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$. If we are going to 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

689 
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

690 
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

691 

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

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

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

694 
\!\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

695 
%& ({*}~\,\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

696 
%& \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

697 
& \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

698 
& \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

699 
& \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

700 
& \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

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

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

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

704 
& \textit{Nitpick\_Model.register\_term\_postprocessor}~\!\begin{aligned}[t] 
38241  705 
& @\{\textrm{typ}~\textit{my\_int}\} \\[2pt] 
706 
& \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

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

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

709 

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

710 
Records are also handled as datatypes with a single constructor: 
33191  711 

712 
\prew 

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

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

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

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

717 
\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount] 

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

719 
\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

720 
\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

721 
\hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\ 
33191  722 
\hbox{}\qquad Datatypes: \\ 
723 
\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

724 
\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

725 
& \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

726 
& \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$ 
33191  727 
\postw 
728 

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

730 
similar approach: 

731 

732 
\prew 

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

734 
\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount] 

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

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

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

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

739 
\hbox{}\qquad Datatypes: \\ 

740 
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, 3,\, 4,\, 5,\, 6,\, 7,\, \unr\}$ \\ 

741 
\hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, 2,\, 3,\, 4,\, 3,\, 2,\, 1,\, \unr\}$ \\ 

742 
\hbox{}\qquad\qquad $\textit{real} = \{1,\, 0,\, 4,\, 3/2,\, 3,\, 2,\, 1/2,\, 1/2,\, \unr\}$ 

743 
\postw 

744 

745 
\subsection{Inductive and Coinductive Predicates} 

746 
\label{inductiveandcoinductivepredicates} 

747 

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

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

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

38176  751 
the problem is that they are defined using a least fixedpoint construction. 
33191  752 

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

754 
the \textit{even} predicate below: 

755 

756 
\prew 

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

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

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

760 
\postw 

761 

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

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

764 

765 
\prew 

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

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

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

769 
\postw 

770 

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

772 
$k/2 + 1$: 

773 

774 
\prew 

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

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

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

778 
\postw 

779 

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

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

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

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

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

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

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

789 
proof obligations automatically. 

790 

791 
Let's try an example: 

792 

793 
\prew 

794 
\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

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

798 
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

799 
\hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount] 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35710
diff
changeset

800 
Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount] 
33191  801 
\hbox{}\qquad Empty assignment \\[2\smallskipamount] 
38183  802 
Nitpick could not find a better counterexample. It checked 0 of 1 scope. \\[2\smallskipamount] 
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40147
diff
changeset

803 
Total time: 1.43 s. 
33191  804 
\postw 
805 

806 
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

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

810 

811 
\prew 

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

812 
\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

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

816 
\postw 

817 

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

819 
we use the following definition instead? 

820 

821 
\prew 

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

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

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

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

826 
\postw 

827 

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

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

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

831 

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

833 
foreseeable computational hurdles entailed by nonwellfoundedness, we decrease 

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

835 

836 
\prew 

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

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

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

840 
\slshape 

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

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

843 
Trying 6 scopes: \\ 

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

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

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

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

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

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

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

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

852 
\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t] 

853 
& 2 := \{0, 2, 4, 6, 8, 1^\Q, 3^\Q, 5^\Q, 7^\Q, 9^\Q\}, \\[2pt] 

854 
& 1 := \{0, 2, 4, 1^\Q, 3^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\}, \\[2pt] 

855 
& 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\[2\smallskipamount] 

40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40147
diff
changeset

856 
Total time: 2.42 s. 
33191  857 
\postw 
858 

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

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

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

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

863 

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

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

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

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

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

869 
iterations would not contribute any new elements. 

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$. Thus, $\textit{even}'$ evaluates to either 

874 
\textit{True} or $\unk$, never \textit{False}. 

875 

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

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

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

881 
\S\ref{scopeofsearch}. 

882 

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

884 

885 
\prew 

886 
\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

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

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

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

892 
\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t] 

893 
& 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\ 

894 
\hbox{}\qquad\qquad $\textit{even}' \subseteq \{0, 2, 4, 6, 8, \unr\}$ 

895 
\postw 

896 

897 
Notice the special constraint $\textit{even}' \subseteq \{0,\, 2,\, 4,\, 6,\, 

898 
8,\, \unr\}$ in the output, whose righthand side represents an arbitrary 

899 
fixed point (not necessarily the least one). It is used to falsify 

900 
$\textit{even}'~n$. In contrast, the unrolled predicate is used to satisfy 

901 
$\textit{even}'~(n  2)$. 

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] 

908 
\textbf{lemma} ``$\textit{nats} = \{0, 1, 2, 3, 4\}$'' \\ 

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

913 
\hbox{}\qquad\qquad $\lambda i.\; \textit{nats} = \undef(0 := \{\!\begin{aligned}[t] 

914 
& 0^\Q, 1^\Q, 2^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q, \\[2pt] 

915 
& \unr\})\end{aligned}$ \\ 

916 
\hbox{}\qquad\qquad $nats \supseteq \{9, 5^\Q, 6^\Q, 7^\Q, 8^\Q, \unr\}$ 

917 
\postw 

918 

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

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

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

922 
assumption of each introduction rule. For example: 

923 

924 
\prew 

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

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

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

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

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

930 
\slshape Nitpick found a counterexample: 

931 
\\[2\smallskipamount] 

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

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

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

935 
\hbox{}\qquad\qquad $\textit{even} = \{0, 2, 4, 6, 8, \unr\}$ \\ 

936 
\hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = \{1, \unr\}$ \\ 

937 
\hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \! 

938 
\!\begin{aligned}[t] 

939 
& \{(0, 0), (0, 2), (0, 4), (0, 6), (0, 8), (1, 1), (1, 3), (1, 5), \\[2pt] 

940 
& \phantom{\{} (1, 7), (1, 9), (2, 2), (2, 4), (2, 6), (2, 8), (3, 3), 

941 
(3, 5), \\[2pt] 

942 
& \phantom{\{} (3, 7), (3, 9), (4, 4), (4, 6), (4, 8), (5, 5), (5, 7), (5, 9), \\[2pt] 

943 
& \phantom{\{} (6, 6), (6, 8), (7, 7), (7, 9), (8, 8), (9, 9), \unr\}\end{aligned}$ \\ 

944 
\hbox{}\qquad\qquad $\textit{odd} \subseteq \{1, 3, 5, 7, 9, 8^\Q, \unr\}$ 

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 

953 
$\textit{odd}_{\textrm{base}}$, namely 1, 3, 5, 7, and 9. Using Kodkod's 

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 

956 
for those cases where it isn't you can disable it by passing the 

957 
\textit{dont\_star\_linear\_preds} option. 

958 

959 
\subsection{Coinductive Datatypes} 

960 
\label{coinductivedatatypes} 

961 

962 
While Isabelle regrettably lacks a highlevel mechanism for defining coinductive 

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

963 
datatypes, the \textit{Coinductive\_List} theory from Andreas Lochbihler's 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

964 
\textit{Coinductive} AFP entry \cite{lochbihler2010} provides a coinductive 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

965 
``lazy list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

966 
supports these lazy lists seamlessly and provides a hook, described in 
33191  967 
\S\ref{registrationofcoinductivedatatypes}, to register custom coinductive 
968 
datatypes. 

969 

970 
(Co)intuitively, a coinductive datatype is similar to an inductive datatype but 

971 
allows infinite objects. Thus, the infinite lists $\textit{ps}$ $=$ $[a, a, a, 

972 
\ldots]$, $\textit{qs}$ $=$ $[a, b, a, b, \ldots]$, and $\textit{rs}$ $=$ $[0, 

973 
1, 2, 3, \ldots]$ can be defined as lazy lists using the 

974 
$\textit{LNil}\mathbin{\Colon}{'}a~\textit{llist}$ and 

975 
$\textit{LCons}\mathbin{\Colon}{'}a \mathbin{\Rightarrow} {'}a~\textit{llist} 

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

977 

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

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

980 
finite lists: 

981 

982 
\prew 

983 
\textbf{lemma} ``$\textit{xs} \not= \textit{LCons}~a~\textit{xs}$'' \\ 

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

985 
\slshape Nitpick found a counterexample for {\itshape card}~$'a$ = 1: \\[2\smallskipamount] 

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

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

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

989 
\postw 

990 

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

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

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

994 

995 
The next example is more interesting: 

996 

997 
\prew 

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

999 
\textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\ 

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

1001 
\slshape The type ``\kern1pt$'a$'' passed the monotonicity test. Nitpick might be able to skip 

1002 
some scopes. \\[2\smallskipamount] 

38181  1003 
Trying 10 scopes: \\ 
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

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

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

33191  1009 
Nitpick found a counterexample for {\itshape card}~$'a$ = 2, 
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

1010 
\textit{card}~``\kern1pt$'a~\textit{list\/}$''~= 2, and \textit{bisim\_\allowbreak 
33191  1011 
depth}~= 1: 
1012 
\\[2\smallskipamount] 

1013 
\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

1014 
\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

1015 
\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

1016 
\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

1017 
\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount] 
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40147
diff
changeset

1018 
Total time: 1.02 s. 
33191  1019 
\postw 
1020 

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

1021 
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

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

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

1026 

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

1028 
equal if and only if they lead to the same observations. For example, the lazy 

1029 
lists $\textrm{THE}~\omega.\; \omega = 

1030 
\textit{LCons}~a~(\textit{LCons}~b~\omega)$ and 

1031 
$\textit{LCons}~a~(\textrm{THE}~\omega.\; \omega = 

1032 
\textit{LCons}~b~(\textit{LCons}~a~\omega))$ are identical, because both lead 

1033 
to the sequence of observations $a$, $b$, $a$, $b$, \hbox{\ldots} (or, 

1034 
equivalently, both encode the infinite list $[a, b, a, b, \ldots]$). This 

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

1036 
defined coinductively. 

1037 

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

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

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

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

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

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

35695  1044 
counterexample is tagged as ``quasi genuine'' and Nitpick recommends to try 
33191  1045 
again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the 
1046 
check for the previous example saves approximately 150~milli\seconds; the speed 

1047 
gains can be more significant for larger scopes. 

1048 

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

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

1051 

1052 
\prew 

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

1054 
\,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\ 

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

1055 
\textbf{nitpick} [\textit{bisim\_depth} = $1$, \textit{show\_datatypes}] \\[2\smallskipamount] 
35695  1056 
\slshape Nitpick found a quasi genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount] 
33191  1057 
\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

1058 
\hbox{}\qquad\qquad $a = a_1$ \\ 
33191  1059 
\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

1060 
\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

1061 
\hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\ 
33191  1062 
\hbox{}\qquad Codatatype:\strut \nopagebreak \\ 
1063 
\hbox{}\qquad\qquad $'a~\textit{llist} = 

1064 
\{\!\begin{aligned}[t] 

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

1065 
& \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

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

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

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

1071 
\slshape Nitpick found no counterexample. 

1072 
\postw 

1073 

1074 
In the first \textbf{nitpick} invocation, the afterthefact check discovered 

1075 
that the two known elements of type $'a~\textit{llist}$ are bisimilar. 

1076 

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

1078 
problem and performing the afterthefact check is to specify a lower 

1079 
nonnegative \textit{bisim\_depth} value than the default one provided by 

1080 
Nitpick. In general, a value of $K$ means that Nitpick will require all lists to 

1081 
be distinguished from each other by their prefixes of length $K$. Be aware that 

1082 
setting $K$ to a too low value can overconstrain Nitpick, preventing it from 

1083 
finding any counterexamples. 

1084 

1085 
\subsection{Boxing} 

1086 
\label{boxing} 

1087 

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

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

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

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

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

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

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

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

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

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

1098 

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

1100 
using de Bruijn's notation: 

1101 

1102 
\prew 

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

1104 
\postw 

1105 

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

1107 
than or equal to $k$ by one: 

1108 

1109 
\prew 

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

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

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

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

1114 
\postw 

1115 

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

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

1118 

1119 
\prew 

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

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

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

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

1124 
\postw 

1125 

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

1127 
on $t$: 

1128 

1129 
\prew 

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

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

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

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

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

1135 
\postw 

1136 

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

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

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

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

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

1142 

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

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

1145 

1146 
\pre 

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

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

1149 
\slshape 

38181  1150 
Trying 10 scopes: \nopagebreak \\ 
33191  1151 
\hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 1; \\ 
1152 
\hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 2; \\ 

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

38181  1154 
\hbox{}\qquad \textit{card~nat}~= 10, \textit{card tm}~= 10, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 10. \\[2\smallskipamount] 
33191  1155 
Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6, 
1156 
and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm}$''~= 6: \\[2\smallskipamount] 

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

1158 
\hbox{}\qquad\qquad $\sigma = \undef(\!\begin{aligned}[t] 

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

1160 
1 := \textit{Var}~0,\> 

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

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

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

1164 
5 := \textit{Var}~0)\end{aligned}$ \\ 

1165 
\hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount] 

40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40147
diff
changeset

1166 
Total time: 3.56 s. 
33191  1167 
\postw 
1168 

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

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

1171 
$\lambda$term notation, $t$~is 

1172 
$\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is $\lambda x\, y.\> y$. 

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

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

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

38181  1177 
cardinalities from 1 to 10 to the type $\textit{nat} \Rightarrow \textit{tm}$. 
33191  1178 
For the formula of interest, knowing 6 values of that type was enough to find 
1179 
the counterexample. Without boxing, $46\,656$ ($= 6^6$) values must be 

1180 
considered, a hopeless undertaking: 

1181 

1182 
\prew 

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

38183  1184 
{\slshape Nitpick ran out of time after checking 3 of 10 scopes.} 
33191  1185 
\postw 
1186 

1187 
{\looseness=1 

1188 
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

1189 
\textit{box} option. Nitpick usually performs reasonable choices about which 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1190 
types should be boxed, but option tweaking sometimes helps. A related optimization, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1191 
``finalization,'' attempts to wrap functions that constant at all but finitely 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1192 
many points (e.g., finite sets); see the documentation for the \textit{finalize} 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35386
diff
changeset

1193 
option in \S\ref{scopeofsearch} for details. 
33191  1194 

1195 
} 

1196 

1197 
\subsection{Scope Monotonicity} 

1198 
\label{scopemonotonicity} 

1199 

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

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

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

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

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

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

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

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

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

1211 

1212 
Consider the formula 

1213 

1214 
\prew 

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

1216 
\postw 

1217 

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

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

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

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

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

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

1226 
definitions: 

33191  1227 

1228 
\prew 

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

1230 
\slshape 

1231 
The types ``\kern1pt$'a$'' and ``\kern1pt$'b$'' passed the monotonicity test. 

1232 
Nitpick might be able to skip some scopes. 

1233 
\\[2\smallskipamount] 

38181  1234 
Trying 10 scopes: \\ 
33191  1235 
\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1, 
1236 
\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

1237 
\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

1238 
\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

1239 
\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 1. \\ 
33191  1240 
\hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2, 
1241 
\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

1242 
\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

1243 
\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

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

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

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

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

33191  1251 
\\[2\smallskipamount] 
1252 
Nitpick found a counterexample for 

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

1254 
\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

1255 
\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

1256 
\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 5: 
33191  1257 
\\[2\smallskipamount] 
1258 
\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

1259 
\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

1260 
\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

1261 
Total time: 1.63 s. 
33191  1262 
\postw 
1263 

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

1265 

1266 
\prew 

38181  1267 
\textbf{nitpick}~[\textit{card}~= 10] 
33191  1268 
\postw 
1269 

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

1271 
counterexamples. 

1272 

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

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

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

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

1277 

1278 
\prew 

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

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

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

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

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

1284 
\slshape 

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

1286 
\hbox{}\qquad $\vdots$ 

1287 
\postw 

1288 

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

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

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

1292 
(\S\ref{optimizations}). 

1293 

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

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

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

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

33191  1302 

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

1303 
\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

1304 
\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

1305 

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 
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

1307 
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

1308 
% 
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 
\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

1310 
\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

1311 
\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

1312 
\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

1313 
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

1314 
\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

1315 
% 
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 
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

1317 
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

1318 
% 
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 
\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

1320 
\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

1321 
\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

1322 
\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

1323 
\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

1324 
% 
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 
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

1326 
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

1327 
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

1328 
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

1329 
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

1330 

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

1332 
\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

1333 
``$(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

1334 
``$\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

1335 
``$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

1336 
\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

1337 

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 
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

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

1341 
\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

1342 
\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

1343 

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 
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

1345 
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

1346 

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

1348 
\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

1349 
\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

1350 
\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

1351 

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 
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

1353 

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

1355 
{\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

1356 
\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

1357 
\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

1358 
} 
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 
\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

1360 

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 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

1362 
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

1363 
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

1364 
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

1365 
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

1366 

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

1368 
\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

1369 
\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

1370 
\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

1371 
\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

1372 
\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

1373 
\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

1374 

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 
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

1376 
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

1377 

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

1378 
\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

1379 
\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

1380 
\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

1381 

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

1382 
Unfortunately, the proof by induction still gets stuck, except that Nitpick now 
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

1383 
finds the counterexample $n = 2$. We generalize the lemma further 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

1384 

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

1385 
\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

1386 
\textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \ge 4$'' 
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

1387 
\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

1388 

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

1389 
and this time \textit{arith} can finish off the 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

1390 

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

1391 
A similar technique can be employed for structural induction. The 
35180
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35178
diff
changeset

1392 
following mini formalization of full binary trees will serve as illustration: 
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

1393 

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

1394 
\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

1395 
\textbf{datatype} $\kern1pt'a$~\textit{bin\_tree} = $\textit{Leaf}~{\kern1pt'a}$ $\mid$ $\textit{Branch}$ ``\kern1pt$'a$ \textit{bin\_tree}'' ``\kern1pt$'a$ \textit{bin\_tree}'' \\[2\smallskipamount] 
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

1396 
\textbf{primrec}~\textit{labels}~\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

1397 
``$\textit{labels}~(\textit{Leaf}~a) = \{a\}$'' $\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

1398 
``$\textit{labels}~(\textit{Branch}~t~u) = \textit{labels}~t \mathrel{\cup} \textit{labels}~u$'' \\[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

1399 
\textbf{primrec}~\textit{swap}~\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

1400 
``$\textit{swap}~(\textit{Leaf}~c)~a~b =$ \\ 
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

1401 
\phantom{``}$(\textrm{if}~c = a~\textrm{then}~\textit{Leaf}~b~\textrm{else~if}~c = b~\textrm{then}~\textit{Leaf}~a~\textrm{else}~\textit{Leaf}~c)$'' $\mid$ \\ 
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

1402 
``$\textit{swap}~(\textit{Branch}~t~u)~a~b = \textit{Branch}~(\textit{swap}~t~a~b)~(\textit{swap}~u~a~b)$'' 
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

1403 
\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

1404 

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

1405 
The \textit{labels} function returns the set of labels occurring on leaves of a 
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

1406 
tree, and \textit{swap} exchanges two labels. Intuitively, if two distinct 
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

1407 
labels $a$ and $b$ occur in a tree $t$, they should also occur in the tree 