author  blanchet 
Mon, 22 Feb 2010 19:31:00 +0100  
changeset 35284  9edc2bd6d2bd 
parent 35220  2bcdae5f4fdb 
child 35309  997aa3a3e4bb 
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} 
7 
\usepackage{graphicx} 

8 
%\usepackage{mathpazo} 

9 
\usepackage{multicol} 

10 
\usepackage{stmaryrd} 

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

12 
\usepackage{../iman,../pdfsetup} 

13 

14 
%\oddsidemargin=4.6mm 

15 
%\evensidemargin=4.6mm 

16 
%\textwidth=150mm 

17 
%\topmargin=4.6mm 

18 
%\headheight=0mm 

19 
%\headsep=0mm 

20 
%\textheight=234mm 

21 

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

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

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

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

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

27 

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

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

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

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

34 

35 
\hyphenation{MiniSat sizechange FirstSteps grandparent nitpick 

36 
counterexample counterexamples datatype datatypes codatatype 

37 
codatatypes inductive coinductive} 

38 

39 
\urlstyle{tt} 

40 

41 
\begin{document} 

42 

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

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

44 

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

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

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

53 
\maketitle 

54 

55 
\tableofcontents 

56 

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

58 
\setlength{\parindent}{0pt} 

59 
\setlength{\abovedisplayskip}{\parskip} 

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

61 
\setlength{\belowdisplayskip}{\parskip} 

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

63 

64 
% Generalpurpose enum environment with correct spacing 

65 
\newenvironment{enum}% 

66 
{\begin{list}{}{% 

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

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

69 
\setlength{\itemsep}{\parskip}% 

70 
\advance\itemsep by\parsep}} 

71 
{\end{list}} 

72 

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

74 
\advance\rightskip by\leftmargin} 

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

76 

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

78 
\def\postw{\post} 

79 

80 
\section{Introduction} 

81 
\label{introduction} 

82 

83 
Nitpick \cite{blanchettenipkow2009} is a counterexample generator for 

84 
Isabelle/HOL \cite{isatutorial} that is designed to handle formulas 

85 
combining (co)in\duc\tive datatypes, (co)in\duc\tively defined predicates, and 

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

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

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

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

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

91 
appropriated from a now retired Alloy precursor. 

92 

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

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

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

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

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

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

99 

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

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

102 
write 

103 

104 
\prew 

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

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

107 
\postw 

108 

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

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

111 
that the axioms might be unsatisfiable. 

112 

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

113 
Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.5 virtual 
0efe26262e73
updated Nitpick manual to reflect the latest Stand der Dinge
blanchet
parents:
33193
diff
changeset

114 
machine called \texttt{java}. The examples presented in this manual can be found 
0efe26262e73
updated Nitpick manual to reflect the latest Stand der Dinge
blanchet
parents:
33193
diff
changeset

115 
in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory. 
0efe26262e73
updated Nitpick manual to reflect the latest Stand der Dinge
blanchet
parents:
33193
diff
changeset

116 

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

117 
Throughout this manual, we will explicitly invoke the \textbf{nitpick} command. 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33559
diff
changeset

118 
Nitpick also provides an automatic mode that can be enabled using the 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33559
diff
changeset

119 
``Auto Nitpick'' option from the ``Isabelle'' menu in Proof General. In this 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33559
diff
changeset

120 
mode, Nitpick is run on every newly entered theorem, much like Auto Quickcheck. 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33559
diff
changeset

121 
The collective time limit for Auto Nitpick and Auto Quickcheck can be set using 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33559
diff
changeset

122 
the ``Auto Counterexample Time Limit'' option. 
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33559
diff
changeset

123 

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

126 

127 
The known bugs and limitations at the time of writing are listed in 

128 
\S\ref{knownbugsandlimitations}. Comments and bug reports concerning Nitpick 

129 
or this manual should be directed to 

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

131 
in.\allowbreak tum.\allowbreak de}. 

132 

133 
\vskip2.5\smallskipamount 

134 

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

136 
suggesting several textual improvements. 

137 
% and Perry James for reporting a typo. 

138 

139 
\section{First Steps} 

140 
\label{firststeps} 

141 

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

143 
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

144 
as follows: 
33191  145 

146 
\prew 

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

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

148 
\textbf{imports}~\textit{Main~Coinductive\_List~Quotient\_Product~RealDef} \\ 
33191  149 
\textbf{begin} 
150 
\postw 

151 

152 
The results presented here were obtained using the JNI version of MiniSat and 

153 
with multithreading disabled to reduce nondeterminism. This was done by adding 

154 
the line 

155 

156 
\prew 

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

157 
\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1] 
33191  158 
\postw 
159 

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

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

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

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

164 
available to Nitpick. 

165 

166 
\subsection{Propositional Logic} 

167 
\label{propositionallogic} 

168 

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

170 

171 
\prew 

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

173 
\textbf{nitpick} 

174 
\postw 

175 

176 
You should get the following output: 

177 

178 
\prew 

179 
\slshape 

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

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

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

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

184 
\postw 

185 

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

187 

188 
\prew 

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

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

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

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

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

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

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

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

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

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

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

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

203 
\textbf{oops} 

204 
\postw 

205 

206 
\subsection{Type Variables} 

207 
\label{typevariables} 

208 

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

210 
one is more mind and computerboggling: 

211 

212 
\prew 

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

214 
\postw 

215 
\pagebreak[2] %% TYPESETTING 

216 

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

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

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

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

221 
substituted for {SOME}. 

222 

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

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

225 
variable, up to a given cardinality (8 by default), looking for a finite 

226 
countermodel: 

227 

228 
\prew 

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

230 
\slshape 

231 
Trying 8 scopes: \nopagebreak \\ 

232 
\hbox{}\qquad \textit{card}~$'a$~= 1; \\ 

233 
\hbox{}\qquad \textit{card}~$'a$~= 2; \\ 

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

235 
\hbox{}\qquad \textit{card}~$'a$~= 8. \\[2\smallskipamount] 

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

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

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

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

240 
Total time: 580 ms. 

241 
\postw 

242 

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

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

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

246 

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

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

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

250 

251 
\prew 

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

253 
\postw 

254 

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

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

257 

258 
\subsection{Constants} 

259 
\label{constants} 

260 

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

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

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

264 
formula: 

265 

266 
\prew 

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

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

269 
\slshape 

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

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

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

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

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

275 
\hbox{}\qquad\qquad $\textit{The}~\textsl{fallback} = a_1$ 

276 
\postw 

277 

278 
We can see more clearly now. Since the predicate $P$ isn't true for a unique 

279 
value, $\textrm{THE}~y.\;P~y$ can denote any value of type $'a$, even 

280 
$a_1$. Since $P~a_1$ is false, the entire formula is falsified. 

281 

282 
As an optimization, Nitpick's preprocessor introduced the special constant 

283 
``\textit{The} fallback'' corresponding to $\textrm{THE}~y.\;P~y$ (i.e., 

284 
$\mathit{The}~(\lambda y.\;P~y)$) when there doesn't exist a unique $y$ 

285 
satisfying $P~y$. We disable this optimization by passing the 

286 
\textit{full\_descrs} option: 

287 

288 
\prew 

289 
\textbf{nitpick}~[\textit{full\_descrs},\, \textit{show\_consts}] \\[2\smallskipamount] 

290 
\slshape 

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

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

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

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

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

296 
\hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$ 

297 
\postw 

298 

299 
As the result of another optimization, Nitpick directly assigned a value to the 

300 
subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we 

301 
disable this second optimization by using the command 

302 

303 
\prew 

304 
\textbf{nitpick}~[\textit{dont\_specialize},\, \textit{full\_descrs},\, 

305 
\textit{show\_consts}] 

306 
\postw 

307 

308 
we finally get \textit{The}: 

309 

310 
\prew 

311 
\slshape Constant: \nopagebreak \\ 

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

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

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

314 
& \{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

315 
& \{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

316 
& \{a_3\} := a_3,\> \{\} := a_3)\end{aligned}$ 
33191  317 
\postw 
318 

319 
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

320 
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

321 
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

322 
$f$.} 
33191  323 

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

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

326 

327 
\prew 

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

329 
\postw 

330 

331 
The fix appears to work: 

332 

333 
\prew 

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

335 
\slshape Nitpick found no counterexample. 

336 
\postw 

337 

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

339 
cardinalities up to 50: 

340 

341 
\prew 

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

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

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

345 
\slshape Nitpick found no counterexample. 

346 
\postw 

347 

348 
Let's see if Sledgehammer \cite{sledgehammer2009} can find a proof: 

349 

350 
\prew 

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

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

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

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

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

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

357 
%\textbf{done} 

358 
\postw 

359 

360 
This must be our lucky day. 

361 

362 
\subsection{Skolemization} 

363 
\label{skolemization} 

364 

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

366 

367 
\prew 

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

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

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

371 
\slshape 

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

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

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

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

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

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

378 
\postw 

379 

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

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

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

383 

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

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

386 

387 
\prew 

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

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

390 
\slshape 

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

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

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

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

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

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

397 
\postw 

398 

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

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

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

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

403 

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

405 

406 
\prew 

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

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

409 
\slshape 

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

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

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

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

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

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

416 
\postw 

417 

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

419 
definition: 

420 

421 
\prew 

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

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

424 
\postw 

425 

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

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

428 
from \textit{sym}'s definition. 

429 

430 
Although skolemization is a useful optimization, you can disable it by invoking 

431 
Nitpick with \textit{dont\_skolemize}. See \S\ref{optimizations} for details. 

432 

433 
\subsection{Natural Numbers and Integers} 

434 
\label{naturalnumbersandintegers} 

435 

436 
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

437 
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

438 
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

439 
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

440 
Internally, undefined values lead to a threevalued logic. 
33191  441 

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

442 
Here is an example involving \textit{int\/}: 
33191  443 

444 
\prew 

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

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

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

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

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

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

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

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

453 
\postw 

454 

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

455 
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

456 
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

457 
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

458 
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

459 
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

460 
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

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

462 

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

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

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

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

466 

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

469 
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

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

472 
\prew 

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

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

474 
\textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount] 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35189
diff
changeset

475 
\slshape Warning: The conjecture either trivially holds for the given scopes or (more likely) 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

476 
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

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

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

481 
\postw 

482 

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

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

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

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

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

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

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

490 
can never be falsified. 

491 

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

493 
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

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

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

498 
giant with feet of clay: 

499 

500 
\prew 

501 
\textbf{lemma} ``$P~\textit{Suc}$'' \\ 

502 
\textbf{nitpick} [\textit{card} = 16] \\[2\smallskipamount] 

503 
\slshape 

504 
Nitpick found no counterexample. 

505 
\postw 

506 

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

507 
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

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

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

510 
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

511 
example is similar: 
33191  512 

513 
\prew 

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

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

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

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

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

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

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

521 
{\slshape Nitpick found no counterexample.} 

522 
\postw 

523 

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

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

526 
1\}$. 

527 

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

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

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

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

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

533 
all cardinalities from 1 to 8 for \textit{nat}, mainly because smaller 

534 
cardinalities are fast to handle and give rise to simpler counterexamples. This 

535 
is explained in more detail in \S\ref{scopemonotonicity}. 

536 

537 
\subsection{Inductive Datatypes} 

538 
\label{inductivedatatypes} 

539 

540 
Like natural numbers and integers, inductive datatypes with recursive 

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

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

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

544 
different lists. 

545 

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

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

548 

549 
\prew 

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

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

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

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

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

555 
\hbox{}\qquad\qquad $\textit{y} = a_1$ 
33191  556 
\postw 
557 

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

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

560 

561 
\prew 

562 
{\slshape Datatype:} \\ 

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

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

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

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

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

570 
including $a_2$. 

571 

572 
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

573 
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

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

577 
appending $[a_1, a_1]$ to itself gives $\unk$. 
33191  578 

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

580 
considers the following subsets: 

581 

582 
\kern.5\smallskipamount %% TYPESETTING 

583 

584 
\prew 

585 
\begin{multicols}{3} 

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

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

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

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

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

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

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

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

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

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

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

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

598 
\end{multicols} 

599 
\postw 

600 

601 
\kern2\smallskipamount %% TYPESETTING 

602 

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

604 
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

605 
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

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

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

610 

611 
\prew 

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

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

614 
\\ 

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

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

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

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

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

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

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

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

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

628 
unlikely that one could be found for smaller cardinalities. 

629 

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

630 
\subsection{Typedefs, Quotient Types, Records, Rationals, and Reals} 
33191  631 
\label{typedefsrecordsrationalsandreals} 
632 

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

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

635 
For example: 

636 

637 
\prew 

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

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

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

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

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

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

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

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

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

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

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

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

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

655 

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

656 
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

657 
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

658 
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

659 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

683 

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

684 
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

685 
integers $0$ and $1$, respectively. Other representants would have been 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

686 
possiblee.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$. 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35220
diff
changeset

687 

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

688 
Records are also handled as datatypes with a single constructor: 
33191  689 

690 
\prew 

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

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

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

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

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

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

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

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

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

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

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

704 
& \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$ 
33191  705 
\postw 
706 

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

707 

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

708 

33191  709 
Finally, Nitpick provides rudimentary support for rationals and reals using a 
710 
similar approach: 

711 

712 
\prew 

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

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

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

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

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

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

719 
\hbox{}\qquad Datatypes: \\ 

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

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

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

723 
\postw 

724 

725 
\subsection{Inductive and Coinductive Predicates} 

726 
\label{inductiveandcoinductivepredicates} 

727 

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

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

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

731 
the problem is that they are defined using a least fixed point construction. 

732 

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

734 
the \textit{even} predicate below: 

735 

736 
\prew 

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

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

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

740 
\postw 

741 

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

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

744 

745 
\prew 

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

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

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

749 
\postw 

750 

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

752 
$k/2 + 1$: 

753 

754 
\prew 

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

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

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

758 
\postw 

759 

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

761 
fixed point computation.% 

762 
\footnote{If an inductive predicate is 

763 
wellfounded, then it has exactly one fixed point, which is simultaneously the 

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

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

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

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

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

769 
proof obligations automatically. 

770 

771 
Let's try an example: 

772 

773 
\prew 

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

34126  775 
\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount] 
33191  776 
\slshape The inductive predicate ``\textit{even}'' was proved wellfounded. 
777 
Nitpick can compute it efficiently. \\[2\smallskipamount] 

778 
Trying 1 scope: \\ 

779 
\hbox{}\qquad \textit{card nat}~= 100. \\[2\smallskipamount] 

780 
Nitpick found a potential counterexample for \textit{card nat}~= 100: \\[2\smallskipamount] 

781 
\hbox{}\qquad Empty assignment \\[2\smallskipamount] 

782 
Nitpick could not find a better counterexample. \\[2\smallskipamount] 

783 
Total time: 2274 ms. 

784 
\postw 

785 

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

787 
existence of a natural number $n \ge 100$ such that both $\textit{even}~n$ and 

788 
$\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the 

789 
existential quantifier: 

790 

791 
\prew 

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

34126  793 
\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}] \\[2\smallskipamount] 
33191  794 
\slshape Nitpick found a counterexample: \\[2\smallskipamount] 
795 
\hbox{}\qquad Empty assignment 

796 
\postw 

797 

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

799 
we use the following definition instead? 

800 

801 
\prew 

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

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

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

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

806 
\postw 

807 

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

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

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

811 

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

813 
foreseeable computational hurdles entailed by nonwellfoundedness, we decrease 

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

815 

816 
\prew 

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

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

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

820 
\slshape 

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

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

823 
Trying 6 scopes: \\ 

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

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

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

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

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

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

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

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

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

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

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

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

836 
Total time: 1140 ms. 

837 
\postw 

838 

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

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

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

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

843 

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

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

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

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

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

849 
iterations would not contribute any new elements. 

850 

851 
Some values are marked with superscripted question 

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

853 
predicate evaluates to $\unk$. Thus, $\textit{even}'$ evaluates to either 

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

855 

856 
When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, and 24 

857 
iterations. However, these numbers are bounded by the cardinality of the 

858 
predicate's domain. With \textit{card~nat}~= 10, no more than 9 iterations are 

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

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

861 
\S\ref{scopeofsearch}. 

862 

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

864 

865 
\prew 

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

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

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

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

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

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

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

875 
\postw 

876 

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

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

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

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

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

882 

883 
Coinductive predicates are handled dually. For example: 

884 

885 
\prew 

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

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

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

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

890 
\slshape Nitpick found a counterexample: 

891 
\\[2\smallskipamount] 

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

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

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

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

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

897 
\postw 

898 

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

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

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

902 
assumption of each introduction rule. For example: 

903 

904 
\prew 

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

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

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

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

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

910 
\slshape Nitpick found a counterexample: 

911 
\\[2\smallskipamount] 

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

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

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

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

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

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

918 
\!\begin{aligned}[t] 

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

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

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

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

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

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

925 
\postw 

926 

927 
\noindent 

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

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

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

931 
reachable through the reflexive transitive closure of 

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

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

934 
transitive closure to encode linear predicates is normally either more thorough 

935 
or more efficient than unrolling (depending on the value of \textit{iter}), but 

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

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

938 

939 
\subsection{Coinductive Datatypes} 

940 
\label{coinductivedatatypes} 

941 

942 
While Isabelle regrettably lacks a highlevel mechanism for defining coinductive 

943 
datatypes, the \textit{Coinductive\_List} theory provides a coinductive ``lazy 

944 
list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick supports 

945 
these lazy lists seamlessly and provides a hook, described in 

946 
\S\ref{registrationofcoinductivedatatypes}, to register custom coinductive 

947 
datatypes. 

948 

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

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

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

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

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

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

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

956 

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

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

959 
finite lists: 

960 

961 
\prew 

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

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

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

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

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

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

968 
\postw 

969 

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

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

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

973 

974 
The next example is more interesting: 

975 

976 
\prew 

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

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

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

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

981 
some scopes. \\[2\smallskipamount] 

982 
Trying 8 scopes: \\ 

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

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

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

986 
\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 8, 
33191  987 
and \textit{bisim\_depth}~= 7. \\[2\smallskipamount] 
988 
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

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

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

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

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

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

996 
\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount] 
33191  997 
Total time: 726 ms. 
998 
\postw 

999 

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

1000 
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

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

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

1005 

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

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

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

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

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

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

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

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

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

1015 
defined coinductively. 

1016 

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

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

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

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

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

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

1023 
counterexample is tagged as ``likely genuine'' and Nitpick recommends to try 

1024 
again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the 

1025 
check for the previous example saves approximately 150~milli\seconds; the speed 

1026 
gains can be more significant for larger scopes. 

1027 

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

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

1030 

1031 
\prew 

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

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

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

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

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

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

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

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

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

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

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

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

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

1050 
\slshape Nitpick found no counterexample. 

1051 
\postw 

1052 

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

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

1055 

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

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

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

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

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

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

1062 
finding any counterexamples. 

1063 

1064 
\subsection{Boxing} 

1065 
\label{boxing} 

1066 

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

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

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

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

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

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

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

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

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

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

1077 

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

1079 
using de Bruijn's notation: 

1080 

1081 
\prew 

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

1083 
\postw 

1084 

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

1086 
than or equal to $k$ by one: 

1087 

1088 
\prew 

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

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

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

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

1093 
\postw 

1094 

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

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

1097 

1098 
\prew 

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

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

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

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

1103 
\postw 

1104 

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

1106 
on $t$: 

1107 

1108 
\prew 

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

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

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

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

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

1114 
\postw 

1115 

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

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

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

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

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

1121 

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

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

1124 

1125 
\pre 

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

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

1128 
\slshape 

1129 
Trying 8 scopes: \nopagebreak \\ 

1130 
\hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 1; \\ 

1131 
\hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 2; \\ 

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

1133 
\hbox{}\qquad \textit{card~nat}~= 8, \textit{card tm}~= 8, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 8. \\[2\smallskipamount] 

1134 
Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6, 

1135 
and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm}$''~= 6: \\[2\smallskipamount] 

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

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

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

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

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

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

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

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

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

1145 
Total time: $4679$ ms. 

1146 
\postw 

1147 

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

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

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

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

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

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

1156 
cardinalities from 1 to 8 to the type $\textit{nat} \Rightarrow \textit{tm}$. 

1157 
For the formula of interest, knowing 6 values of that type was enough to find 

1158 
the counterexample. Without boxing, $46\,656$ ($= 6^6$) values must be 

1159 
considered, a hopeless undertaking: 

1160 

1161 
\prew 

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

1163 
{\slshape Nitpick ran out of time after checking 4 of 8 scopes.} 

1164 
\postw 

1165 

1166 
{\looseness=1 

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

1168 
\textit{box} option. Moreover, setting the cardinality of a function or 

1169 
product type implicitly enables boxing for that type. Nitpick usually performs 

1170 
reasonable choices about which types should be boxed, but option tweaking 

1171 
sometimes helps. 

1172 

1173 
} 

1174 

1175 
\subsection{Scope Monotonicity} 

1176 
\label{scopemonotonicity} 

1177 

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

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

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

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

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

1183 
cardinality specification of 18, no fewer than $8^4 = 4096$ scopes must be 

1184 
considered for a formula involving $'a$, $'b$, $'c$, and $'d$. 

1185 

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

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

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

1189 

1190 
Consider the formula 

1191 

1192 
\prew 

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

1194 
\postw 

1195 

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

1197 
$'b~\textit{list}$. A priori, Nitpick would need to consider 512 scopes to 

1198 
exhaust the specification \textit{card}~= 18. However, our intuition tells us 

1199 
that any counterexample found with a small scope would still be a counterexample 

1200 
in a larger scopeby simply ignoring the fresh $'a$ and $'b$ values provided 

1201 
by the larger scope. Nitpick comes to the same conclusion after a careful 

1202 
inspection of the formula and the relevant definitions: 

1203 

1204 
\prew 

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

1206 
\slshape 

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

1208 
Nitpick might be able to skip some scopes. 

1209 
\\[2\smallskipamount] 

1210 
Trying 8 scopes: \\ 

1211 
\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1, 

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

1213 
\textit{list}''~= 1, \\ 

1214 
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 1, and 

1215 
\textit{card} ``\kern1pt$'b$ \textit{list}''~= 1. \\ 

1216 
\hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2, 

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

1218 
\textit{list}''~= 2, \\ 

1219 
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 2, and 

1220 
\textit{card} ``\kern1pt$'b$ \textit{list}''~= 2. \\ 

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

1222 
\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} $'b$~= 8, 

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

1224 
\textit{list}''~= 8, \\ 

1225 
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 8, and 

1226 
\textit{card} ``\kern1pt$'b$ \textit{list}''~= 8. 

1227 
\\[2\smallskipamount] 

1228 
Nitpick found a counterexample for 

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

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

1231 
\textit{list}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list}''~= 5, and 

1232 
\textit{card} ``\kern1pt$'b$ \textit{list}''~= 5: 

1233 
\\[2\smallskipamount] 

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

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

1236 
\hbox{}\qquad\qquad $\textit{ys} = [b_1, b_1]$ \\[2\smallskipamount] 
33191  1237 
Total time: 1636 ms. 
1238 
\postw 

1239 

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

1241 

1242 
\prew 

1243 
\textbf{nitpick}~[\textit{card}~= 8] 

1244 
\postw 

1245 

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

1247 
counterexamples. 

1248 

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

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

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

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

1253 

1254 
\prew 

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

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

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

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

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

1260 
\slshape 

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

1262 
\hbox{}\qquad $\vdots$ 

1263 
\postw 

1264 

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

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

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

1268 
(\S\ref{optimizations}). 

1269 

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

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

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

1273 
\textit{rat}, \textit{real}, and some \textbf{typedef}'d types. Thus, given the 

1274 
cardinality specification 18, a formula involving \textit{nat}, \textit{int}, 

1275 
\textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to 

1276 
consider only 8~scopes instead of $32\,768$. 

1277 

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

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

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

1280 

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

1281 
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

1282 
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

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

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

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

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

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

1288 
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

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

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

1291 
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

1292 
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

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

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

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

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

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

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

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

1300 
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

1301 
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

1302 
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

1303 
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

1304 
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

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

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

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

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

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

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

1312 

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

1314 

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

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

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

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

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

1320 
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

1321 

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

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

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

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

1326 

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

1327 
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

1328 

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

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

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

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

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

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

1335 

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

1336 
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

1337 
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

1338 
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

1339 
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

1340 
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

1341 

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

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

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

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

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

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

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

1349 

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

1350 
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

1351 
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

1352 

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

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

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

1356 

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

1357 
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

1358 
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

1359 

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

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

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

1363 

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

1365 

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

1367 
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

1368 

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

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

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

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

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

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

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

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

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

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

1379 

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

1381 
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

1382 
labels $a$ and $b$ occur in a tree $t$, they should also occur in the tree 
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 
obtained by swapping $a$ and $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

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 
35180
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35178
diff
changeset

1386 
\textbf{lemma} $``\{a, b\} \subseteq \textit{labels}~t \,\Longrightarrow\, \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$'' 
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

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 
Nitpick can't find any counterexample, so we proceed with 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

1390 
(this time favoring a more structured style): 
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 

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

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

1393 
\textbf{proof}~(\textit{induct}~$t$) \\ 
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 
\hbox{}\quad \textbf{case}~\textit{Leaf}~\textbf{thus}~\textit{?case}~\textbf{by}~\textit{simp} \\ 
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{next} \\ 
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 
\hbox{}\quad \textbf{case}~$(\textit{Branch}~t~u)$~\textbf{thus} \textit{?case} 
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 
\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

1398 

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 
Nitpick can't find any counterexample at this point either, but it makes the 
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 
following suggestion: 
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 

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

1403 
\slshape 
35178  1404 
Hint: To check that the induction hypothesis is general enough, try this command: 
35183
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35180
diff
changeset

1405 
\textbf{nitpick}~[\textit{non\_std}, \textit{show\_all}]. 
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

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

1407 

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

1408 
If we follow the hint, we get a ``nonstandard'' counterexample for the 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

1409 

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

1410 
\prew 
35180
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35178
diff
changeset

1411 
\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 3: \\[2\smallskipamount] 
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

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

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

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

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

1416 
\hbox{}\qquad\qquad $u = \xi_2$ \\ 
35180
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35178
diff
changeset

1417 
\hbox{}\qquad Datatype: \nopagebreak \\ 
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35178
diff
changeset

1418 
\hbox{}\qquad\qquad $\alpha~\textit{btree} = \{\xi_1 \mathbin{=} \textit{Branch}~\xi_1~\xi_1,\> \xi_2 \mathbin{=} \textit{Branch}~\xi_2~\xi_2,\> \textit{Branch}~\xi_1~\xi_2\}$ \\ 
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

1419 
\hbox{}\qquad {\slshape Constants:} \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

1420 
\hbox{}\qquad\qquad $\textit{labels} = \undef 
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

1421 
(\!\begin{aligned}[t]% 
35180
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35178
diff
changeset

1422 
& \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[2pt] 
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35178
diff
changeset

1423 
& \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\ 
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

1424 
\hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef 
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

1425 
(\!\begin{aligned}[t]% 
35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35072
diff
changeset

1426 
& \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[2pt] 
35180
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35178
diff
changeset

1427 
& \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount] 
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

1428 
The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanch&# 