1.1 --- a/doc-src/Nitpick/nitpick.tex Tue Jan 03 18:33:18 2012 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Tue Jan 03 23:03:49 2012 +0100
1.3 @@ -27,7 +27,8 @@
1.4 \def\rparr{\mathclose{\mid\mkern-4mu)}}
1.5
1.6 \def\unk{{?}}
1.7 -\def\undef{(\lambda x.\; \unk)}
1.8 +\def\unkef{(\lambda x.\; \unk)}
1.9 +\def\undef{(\lambda x.\; \_)}
1.10 %\def\unr{\textit{others}}
1.11 \def\unr{\ldots}
1.12 \def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
1.13 @@ -107,7 +108,7 @@
1.14 write
1.15
1.16 \prew
1.17 -\textbf{lemma}~``$\textit{False}$'' \\
1.18 +\textbf{lemma}~``$\textit{False\/}$'' \\
1.19 \textbf{nitpick}~[\textit{show\_all}]
1.20 \postw
1.21
1.22 @@ -241,7 +242,7 @@
1.23 one is more mind- and computer-boggling:
1.24
1.25 \prew
1.26 -\textbf{lemma} ``$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
1.27 +\textbf{lemma} ``$x \in A\,\Longrightarrow\, (\textrm{THE}~y.\;y \in A) \in A$''
1.28 \postw
1.29 \pagebreak[2] %% TYPESETTING
1.30
1.31 @@ -266,9 +267,9 @@
1.32 \hbox{}\qquad \textit{card}~$'a$~= 10. \\[2\smallskipamount]
1.33 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
1.34 \hbox{}\qquad Free variables: \nopagebreak \\
1.35 -\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
1.36 +\hbox{}\qquad\qquad $A = \{a_2,\, a_3\}$ \\
1.37 \hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount]
1.38 -Total time: 0.76 s.
1.39 +Total time: 963 ms.
1.40 \postw
1.41
1.42 Nitpick found a counterexample in which $'a$ has cardinality 3. (For
1.43 @@ -295,46 +296,30 @@
1.44 formula:
1.45
1.46 \prew
1.47 -\textbf{lemma}~``$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$'' \\
1.48 +\textbf{lemma} ``$x \in A\,\Longrightarrow\, (\textrm{THE}~y.\;y \in A) \in A$'' \\
1.49 \textbf{nitpick}~[\textit{show\_consts}] \\[2\smallskipamount]
1.50 \slshape
1.51 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
1.52 \hbox{}\qquad Free variables: \nopagebreak \\
1.53 -\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
1.54 +\hbox{}\qquad\qquad $A = \{a_2,\, a_3\}$ \\
1.55 \hbox{}\qquad\qquad $x = a_3$ \\
1.56 \hbox{}\qquad Constant: \nopagebreak \\
1.57 -\hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$
1.58 +\hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;y \in A = a_1$
1.59 \postw
1.60
1.61 As the result of an optimization, Nitpick directly assigned a value to the
1.62 -subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we
1.63 -disable this optimization by using the command
1.64 +subterm $\textrm{THE}~y.\;y \in A$, rather than to the \textit{The} constant. We
1.65 +can disable this optimization by using the command
1.66
1.67 \prew
1.68 \textbf{nitpick}~[\textit{dont\_specialize},\, \textit{show\_consts}]
1.69 \postw
1.70
1.71 -we get \textit{The}:
1.72 -
1.73 -\prew
1.74 -\slshape Constant: \nopagebreak \\
1.75 -\hbox{}\qquad $\mathit{The} = \undef{}
1.76 - (\!\begin{aligned}[t]%
1.77 - & \{a_1, a_2, a_3\} := a_3,\> \{a_1, a_2\} := a_3,\> \{a_1, a_3\} := a_3, \\[-2pt] %% TYPESETTING
1.78 - & \{a_1\} := a_1,\> \{a_2, a_3\} := a_1,\> \{a_2\} := a_2, \\[-2pt]
1.79 - & \{a_3\} := a_3,\> \{\} := a_3)\end{aligned}$
1.80 -\postw
1.81 -
1.82 -Notice that $\textit{The}~(\lambda y.\;P~y) = \textit{The}~\{a_2, a_3\} = a_1$,
1.83 -just like before.\footnote{The Isabelle/HOL notation $f(x :=
1.84 -y)$ denotes the function that maps $x$ to $y$ and that otherwise behaves like
1.85 -$f$.}
1.86 -
1.87 Our misadventures with THE suggest adding `$\exists!x{.}$' (``there exists a
1.88 unique $x$ such that'') at the front of our putative lemma's assumption:
1.89
1.90 \prew
1.91 -\textbf{lemma}~``$\exists {!}x.\; P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
1.92 +\textbf{lemma} ``$\exists {!}x.\; x \in A\,\Longrightarrow\, (\textrm{THE}~y.\;y \in A) \in A$''
1.93 \postw
1.94
1.95 The fix appears to work:
1.96 @@ -358,12 +343,9 @@
1.97
1.98 \prew
1.99 \textbf{sledgehammer} \\[2\smallskipamount]
1.100 -{\slshape Sledgehammer: ``$e$'' on goal: \\
1.101 -$\exists{!}x.\; P~x\,\Longrightarrow\, P~(\hbox{\slshape THE}~y.\; P~y)$ \\
1.102 -Try this: \textrm{apply}~(\textit{metis~theI}) (21 ms).} \\[2\smallskipamount]
1.103 -\textbf{by}~(\textit{metis~theI\/}) \nopagebreak \\[2\smallskipamount]
1.104 -{\slshape No subgoals!}% \\[2\smallskipamount]
1.105 -%\textbf{done}
1.106 +{\slshape Sledgehammer: ``$e$'' on goal \\
1.107 +Try this: \textrm{by}~(\textit{metis~theI}) (42 ms).} \\[2\smallskipamount]
1.108 +\textbf{by}~(\textit{metis~theI\/})
1.109 \postw
1.110
1.111 This must be our lucky day.
1.112 @@ -386,6 +368,8 @@
1.113 \hbox{}\qquad\qquad $y = a_2$
1.114 \postw
1.115
1.116 +(The Isabelle/HOL notation $f(x := y)$ denotes the function that maps $x$ to $y$
1.117 +and that otherwise behaves like $f$.)
1.118 Although $f$ is the only free variable occurring in the formula, Nitpick also
1.119 displays values for the bound variables $g$ and $y$. These values are available
1.120 to Nitpick because it performs skolemization as a preprocessing step.
1.121 @@ -424,8 +408,7 @@
1.122 \hbox{}\qquad\qquad $\mathit{sym}.y = a_1$
1.123 \postw
1.124
1.125 -What happened here is that Nitpick expanded the \textit{sym} constant to its
1.126 -definition:
1.127 +What happened here is that Nitpick expanded \textit{sym} to its definition:
1.128
1.129 \prew
1.130 $\mathit{sym}~r \,\equiv\,
1.131 @@ -492,7 +475,7 @@
1.132 \textit{Suc}~n \mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds
1.133 an $n$ such that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
1.134 \textit{False}; but otherwise, it does not know anything about values of $n \ge
1.135 -\textit{card~nat}$ and must therefore evaluate the assumption to $\unk$, not
1.136 +\textit{card~nat}$ and must therefore evaluate the assumption to~$\unk$, not
1.137 \textit{True}. Since the assumption can never be satisfied, the putative lemma
1.138 can never be falsified.
1.139
1.140 @@ -505,7 +488,7 @@
1.141 giant with feet of clay:
1.142
1.143 \prew
1.144 -\textbf{lemma} ``$P~\textit{Suc}$'' \\
1.145 +\textbf{lemma} ``$P~\textit{Suc\/}$'' \\
1.146 \textbf{nitpick} \\[2\smallskipamount]
1.147 \slshape
1.148 Nitpick found no counterexample.
1.149 @@ -523,14 +506,14 @@
1.150 \textbf{nitpick} [\textit{card nat} = 1] \\[2\smallskipamount]
1.151 {\slshape Nitpick found a counterexample:} \\[2\smallskipamount]
1.152 \hbox{}\qquad Free variable: \nopagebreak \\
1.153 -\hbox{}\qquad\qquad $P = \{\}$ \\[2\smallskipamount]
1.154 +\hbox{}\qquad\qquad $P = \unkef(\unkef(0 := \unkef(0 := 0)) := \mathit{False})$ \\[2\smallskipamount]
1.155 \textbf{nitpick} [\textit{card nat} = 2] \\[2\smallskipamount]
1.156 {\slshape Nitpick found no counterexample.}
1.157 \postw
1.158
1.159 The problem here is that \textit{op}~+ is total when \textit{nat} is taken to be
1.160 -$\{0\}$ but becomes partial as soon as we add $1$, because $1 + 1 \notin \{0,
1.161 -1\}$.
1.162 +$\{0\}$ but becomes partial as soon as we add $1$, because
1.163 +$1 + 1 \notin \{0, 1\}$.
1.164
1.165 Because numbers are infinite and are approximated using a three-valued logic,
1.166 there is usually no need to systematically enumerate domain sizes. If Nitpick
1.167 @@ -554,7 +537,7 @@
1.168 of a list) and $@$ (which concatenates two lists):
1.169
1.170 \prew
1.171 -\textbf{lemma} ``$\textit{hd}~(\textit{xs} \mathbin{@} [y, y]) = \textit{hd}~\textit{xs}$'' \\
1.172 +\textbf{lemma} ``$\textit{hd}~(\textit{xs} \mathbin{@} [y, y]) = \textit{hd}~\textit{xs\/}$'' \\
1.173 \textbf{nitpick} \\[2\smallskipamount]
1.174 \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
1.175 \hbox{}\qquad Free variables: \nopagebreak \\
1.176 @@ -569,8 +552,8 @@
1.177 {\slshape Datatype:} \\
1.178 \hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_1],\, [a_1, a_1],\, \unr\}$ \\
1.179 {\slshape Constants:} \\
1.180 -\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_1, a_1])$ \\
1.181 -\hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_1] := a_1,\> [a_1, a_1] := a_1)$
1.182 +\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \unkef([] := [a_1, a_1])$ \\
1.183 +\hbox{}\qquad $\textit{hd} = \unkef([] := a_2,\> [a_1] := a_1,\> [a_1, a_1] := a_1)$
1.184 \postw
1.185
1.186 Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value,
1.187 @@ -617,13 +600,13 @@
1.188
1.189 \prew
1.190 \textbf{lemma} ``$\lbrakk \textit{length}~\textit{xs} = 1;\> \textit{length}~\textit{ys} = 1
1.191 -\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$''
1.192 +\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys\/}$''
1.193 \\
1.194 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
1.195 \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
1.196 \hbox{}\qquad Free variables: \nopagebreak \\
1.197 -\hbox{}\qquad\qquad $\textit{xs} = [a_1]$ \\
1.198 -\hbox{}\qquad\qquad $\textit{ys} = [a_2]$ \\
1.199 +\hbox{}\qquad\qquad $\textit{xs} = [a_2]$ \\
1.200 +\hbox{}\qquad\qquad $\textit{ys} = [a_1]$ \\
1.201 \hbox{}\qquad Datatypes: \\
1.202 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
1.203 \hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_1],\, [a_2],\, \unr\}$
1.204 @@ -647,12 +630,12 @@
1.205 \textbf{definition}~$A \mathbin{\Colon} \textit{three}$ \textbf{where} ``\kern-.1em$A \,\equiv\, \textit{Abs\_\allowbreak three}~0$'' \\
1.206 \textbf{definition}~$B \mathbin{\Colon} \textit{three}$ \textbf{where} ``$B \,\equiv\, \textit{Abs\_three}~1$'' \\
1.207 \textbf{definition}~$C \mathbin{\Colon} \textit{three}$ \textbf{where} ``$C \,\equiv\, \textit{Abs\_three}~2$'' \\[2\smallskipamount]
1.208 -\textbf{lemma} ``$\lbrakk P~A;\> P~B\rbrakk \,\Longrightarrow\, P~x$'' \\
1.209 +\textbf{lemma} ``$\lbrakk A \in X;\> B \in X\rbrakk \,\Longrightarrow\, c \in X$'' \\
1.210 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
1.211 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.212 \hbox{}\qquad Free variables: \nopagebreak \\
1.213 -\hbox{}\qquad\qquad $P = \{\Abs{0},\, \Abs{1}\}$ \\
1.214 -\hbox{}\qquad\qquad $x = \Abs{2}$ \\
1.215 +\hbox{}\qquad\qquad $X = \{\Abs{0},\, \Abs{1}\}$ \\
1.216 +\hbox{}\qquad\qquad $c = \Abs{2}$ \\
1.217 \hbox{}\qquad Datatypes: \\
1.218 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
1.219 \hbox{}\qquad\qquad $\textit{three} = \{\Abs{0},\, \Abs{1},\, \Abs{2},\, \unr\}$
1.220 @@ -669,7 +652,7 @@
1.221 ``$\textit{my\_int\_rel}~(x,\, y)~(u,\, v) = (x + v = u + y)$'' \\[2\smallskipamount]
1.222 %
1.223 \textbf{quotient\_type}~\textit{my\_int} = ``$\textit{nat} \times \textit{nat\/}$''$\;{/}\;$\textit{my\_int\_rel} \\
1.224 -\textbf{by}~(\textit{auto simp add\/}:\ \textit{equivp\_def expand\_fun\_eq}) \\[2\smallskipamount]
1.225 +\textbf{by}~(\textit{auto simp add\/}:\ \textit{equivp\_def fun\_eq\_iff}) \\[2\smallskipamount]
1.226 %
1.227 \textbf{definition}~\textit{add\_raw}~\textbf{where} \\
1.228 ``$\textit{add\_raw} \,\equiv\, \lambda(x,\, y)~(u,\, v).\; (x + (u\Colon\textit{nat}), y + (v\Colon\textit{nat}))$'' \\[2\smallskipamount]
1.229 @@ -681,16 +664,16 @@
1.230 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.231 \hbox{}\qquad Free variables: \nopagebreak \\
1.232 \hbox{}\qquad\qquad $x = \Abs{(0,\, 0)}$ \\
1.233 -\hbox{}\qquad\qquad $y = \Abs{(1,\, 0)}$ \\
1.234 +\hbox{}\qquad\qquad $y = \Abs{(0,\, 1)}$ \\
1.235 \hbox{}\qquad Datatypes: \\
1.236 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, \unr\}$ \\
1.237 \hbox{}\qquad\qquad $\textit{nat} \times \textit{nat}~[\textsl{boxed\/}] = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
1.238 -\hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(1,\, 0)},\> \unr\}$
1.239 +\hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(0,\, 1)},\> \unr\}$
1.240 \postw
1.241
1.242 -In the counterexample, $\Abs{(0,\, 0)}$ and $\Abs{(1,\, 0)}$ represent the
1.243 -integers $0$ and $1$, respectively. Other representants would have been
1.244 -possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$. If we are going to
1.245 +The values $\Abs{(0,\, 0)}$ and $\Abs{(0,\, 1)}$ represent the
1.246 +integers $0$ and $-1$, respectively. Other representants would have been
1.247 +possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(11,\, 12)}$. If we are going to
1.248 use \textit{my\_int} extensively, it pays off to install a term postprocessor
1.249 that converts the pair notation to the standard mathematical notation:
1.250
1.251 @@ -712,7 +695,7 @@
1.252 {*}\}\end{aligned}$
1.253 \postw
1.254
1.255 -Records are also handled as datatypes with a single constructor:
1.256 +Records are handled as datatypes with a single constructor:
1.257
1.258 \prew
1.259 \textbf{record} \textit{point} = \\
1.260 @@ -743,8 +726,8 @@
1.261 \hbox{}\qquad\qquad $y = -1/2$ \\
1.262 \hbox{}\qquad Datatypes: \\
1.263 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, 3,\, 4,\, 5,\, 6,\, 7,\, \unr\}$ \\
1.264 -\hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, 2,\, 3,\, 4,\, -3,\, -2,\, -1,\, \unr\}$ \\
1.265 -\hbox{}\qquad\qquad $\textit{real} = \{1,\, 0,\, 4,\, -3/2,\, 3,\, 2,\, 1/2,\, -1/2,\, \unr\}$
1.266 +\hbox{}\qquad\qquad $\textit{int} = \{-3,\, -2,\, -1,\, 0,\, 1,\, 2,\, 3,\, 4,\, \unr\}$ \\
1.267 +\hbox{}\qquad\qquad $\textit{real} = \{-3/2,\, -1/2,\, 0,\, 1/2,\, 1,\, 2,\, 3,\, 4,\, \unr\}$
1.268 \postw
1.269
1.270 \subsection{Inductive and Coinductive Predicates}
1.271 @@ -802,10 +785,12 @@
1.272 Nitpick can compute it efficiently. \\[2\smallskipamount]
1.273 Trying 1 scope: \\
1.274 \hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
1.275 +Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported fragment. Only
1.276 +potentially spurious counterexamples may be found. \\[2\smallskipamount]
1.277 Nitpick found a potentially spurious counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
1.278 \hbox{}\qquad Empty assignment \\[2\smallskipamount]
1.279 -Nitpick could not find a better counterexample. \\[2\smallskipamount]
1.280 -Total time: 1.43 s.
1.281 +Nitpick could not find a better counterexample. It checked 1 of 1 scope. \\[2\smallskipamount]
1.282 +Total time: 1.62 s.
1.283 \postw
1.284
1.285 No genuine counterexample is possible because Nitpick cannot rule out the
1.286 @@ -854,11 +839,12 @@
1.287 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 9. \\[2\smallskipamount]
1.288 Nitpick found a counterexample for \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2: \\[2\smallskipamount]
1.289 \hbox{}\qquad Constant: \nopagebreak \\
1.290 -\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t]
1.291 -& 2 := \{0, 2, 4, 6, 8, 1^\Q, 3^\Q, 5^\Q, 7^\Q, 9^\Q\}, \\[-2pt]
1.292 -& 1 := \{0, 2, 4, 1^\Q, 3^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\}, \\[-2pt]
1.293 -& 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\[2\smallskipamount]
1.294 -Total time: 2.42 s.
1.295 +\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\unkef(\!\begin{aligned}[t]
1.296 +& 0 := \unkef(0 := \textit{True},\, 2 := \textit{True}),\, \\[-2pt]
1.297 +& 1 := \unkef(0 := \textit{True},\, 2 := \textit{True},\, 4 := \textit{True}),\, \\[-2pt]
1.298 +& 2 := \unkef(0 := \textit{True},\, 2 := \textit{True},\, 4 := \textit{True},\, \\[-2pt]
1.299 +& \phantom{2 := \unkef(}6 := \textit{True},\, 8 := \textit{True}))\end{aligned}$ \\[2\smallskipamount]
1.300 +Total time: 1.87 s.
1.301 \postw
1.302
1.303 Nitpick's output is very instructive. First, it tells us that the predicate is
1.304 @@ -872,11 +858,12 @@
1.305 elements, $0$ and $2$. Iteration 1 contributes $4$ ($= 2 + 2$). Iteration 2
1.306 throws $6$ ($= 2 + 4 = 4 + 2$) and $8$ ($= 4 + 4$) into the mix. Further
1.307 iterations would not contribute any new elements.
1.308 -
1.309 -Some values are marked with superscripted question
1.310 -marks~(`\lower.2ex\hbox{$^\Q$}'). These are the elements for which the
1.311 -predicate evaluates to $\unk$. Thus, $\textit{even}'$ evaluates to either
1.312 -\textit{True} or $\unk$, never \textit{False}.
1.313 +The predicate $\textit{even}'$ evaluates to either \textit{True} or $\unk$,
1.314 +never \textit{False}.
1.315 +
1.316 +%Some values are marked with superscripted question
1.317 +%marks~(`\lower.2ex\hbox{$^\Q$}'). These are the elements for which the
1.318 +%predicate evaluates to $\unk$.
1.319
1.320 When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, 20, 24, and 28
1.321 iterations. However, these numbers are bounded by the cardinality of the
1.322 @@ -894,16 +881,17 @@
1.323 \hbox{}\qquad Free variable: \nopagebreak \\
1.324 \hbox{}\qquad\qquad $n = 1$ \\
1.325 \hbox{}\qquad Constants: \nopagebreak \\
1.326 -\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t]
1.327 -& 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\
1.328 -\hbox{}\qquad\qquad $\textit{even}' \subseteq \{0, 2, 4, 6, 8, \unr\}$
1.329 +\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\unkef(\!\begin{aligned}[t]
1.330 +& 0 := \unkef(0 := \mathit{True},\, 2 := \mathit{True}))\end{aligned}$ \\
1.331 +\hbox{}\qquad\qquad $\textit{even}' \leq \unkef(\!\begin{aligned}[t]
1.332 +& 0 := \mathit{True},\, 1 := \mathit{False},\, 2 := \mathit{True},\, \\[-2pt]
1.333 +& 4 := \mathit{True},\, 6 := \mathit{True},\, 8 := \mathit{True})\end{aligned}$
1.334 \postw
1.335
1.336 -Notice the special constraint $\textit{even}' \subseteq \{0,\, 2,\, 4,\, 6,\,
1.337 -8,\, \unr\}$ in the output, whose right-hand side represents an arbitrary
1.338 -fixed point (not necessarily the least one). It is used to falsify
1.339 -$\textit{even}'~n$. In contrast, the unrolled predicate is used to satisfy
1.340 -$\textit{even}'~(n - 2)$.
1.341 +Notice the special constraint $\textit{even}' \leq \ldots$ in the output, whose
1.342 +right-hand side represents an arbitrary fixed point (not necessarily the least
1.343 +one). It is used to falsify $\textit{even}'~n$. In contrast, the unrolled
1.344 +predicate is used to satisfy $\textit{even}'~(n - 2)$.
1.345
1.346 Coinductive predicates are handled dually. For example:
1.347
1.348 @@ -915,10 +903,8 @@
1.349 \slshape Nitpick found a counterexample:
1.350 \\[2\smallskipamount]
1.351 \hbox{}\qquad Constants: \nopagebreak \\
1.352 -\hbox{}\qquad\qquad $\lambda i.\; \textit{nats} = \undef(0 := \{\!\begin{aligned}[t]
1.353 -& 0^\Q, 1^\Q, 2^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q, \\[-2pt]
1.354 -& \unr\})\end{aligned}$ \\
1.355 -\hbox{}\qquad\qquad $nats \supseteq \{9, 5^\Q, 6^\Q, 7^\Q, 8^\Q, \unr\}$
1.356 +\hbox{}\qquad\qquad $\lambda i.\; \textit{nats} = \unkef(0 := \unkef,\, 1 := \unkef,\, 2 := \unkef)$ \\
1.357 +\hbox{}\qquad\qquad $\textit{nats} \geq \unkef(3 := \textit{True},\, 4 := \textit{False},\, 5 := \textit{True})$
1.358 \postw
1.359
1.360 As a special case, Nitpick uses Kodkod's transitive closure operator to encode
1.361 @@ -931,22 +917,24 @@
1.362 ``$\textit{odd}~1$'' $\,\mid$ \\
1.363 ``$\lbrakk \textit{odd}~m;\>\, \textit{even}~n\rbrakk \,\Longrightarrow\, \textit{odd}~(m + n)$'' \\[2\smallskipamount]
1.364 \textbf{lemma}~``$\textit{odd}~n \,\Longrightarrow\, \textit{odd}~(n - 2)$'' \\
1.365 -\textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
1.366 +\textbf{nitpick}~[\textit{card nat} = 4,\, \textit{show\_consts}] \\[2\smallskipamount]
1.367 \slshape Nitpick found a counterexample:
1.368 \\[2\smallskipamount]
1.369 \hbox{}\qquad Free variable: \nopagebreak \\
1.370 \hbox{}\qquad\qquad $n = 1$ \\
1.371 \hbox{}\qquad Constants: \nopagebreak \\
1.372 -\hbox{}\qquad\qquad $\textit{even} = \{0, 2, 4, 6, 8, \unr\}$ \\
1.373 -\hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = \{1, \unr\}$ \\
1.374 -\hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \!
1.375 +\hbox{}\qquad\qquad $\textit{even} = (λx. ?)(0 := True, 1 := False, 2 := True, 3 := False)$ \\
1.376 +\hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = {}$ \\
1.377 +\hbox{}\qquad\qquad\quad $\unkef(0 := \textit{False},\, 1 := \textit{True},\, 2 := \textit{False},\, 3 := \textit{False})$ \\
1.378 +\hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \unkef$\\
1.379 +\hbox{}\qquad\qquad\quad $(
1.380 \!\begin{aligned}[t]
1.381 - & \{(0, 0), (0, 2), (0, 4), (0, 6), (0, 8), (1, 1), (1, 3), (1, 5), \\[-2pt]
1.382 - & \phantom{\{} (1, 7), (1, 9), (2, 2), (2, 4), (2, 6), (2, 8), (3, 3),
1.383 - (3, 5), \\[-2pt]
1.384 - & \phantom{\{} (3, 7), (3, 9), (4, 4), (4, 6), (4, 8), (5, 5), (5, 7), (5, 9), \\[-2pt]
1.385 - & \phantom{\{} (6, 6), (6, 8), (7, 7), (7, 9), (8, 8), (9, 9), \unr\}\end{aligned}$ \\
1.386 -\hbox{}\qquad\qquad $\textit{odd} \subseteq \{1, 3, 5, 7, 9, 8^\Q, \unr\}$
1.387 +& 0 := \unkef(0 := \textit{True},\, 1 := \textit{False},\, 2 := \textit{True},\, 3 := \textit{False}), \\[-2pt]
1.388 +& 1 := \unkef(0 := \textit{False},\, 1 := \textit{True},\, 2 := \textit{False},\, 3 := \textit{True}), \\[-2pt]
1.389 +& 2 := \unkef(0 := \textit{False},\, 1 := \textit{False},\, 2 := \textit{True},\, 3 := \textit{False}), \\[-2pt]
1.390 +& 3 := \unkef(0 := \textit{False},\, 1 := \textit{False},\, 2 := \textit{False},\, 3 := \textit{True}))
1.391 +\end{aligned}$ \\
1.392 +\hbox{}\qquad\qquad $\textit{odd} \leq \unkef(0 := \textit{False},\, 1 := \textit{True},\, 2 := \textit{False},\, 3 := \textit{True})$
1.393 \postw
1.394
1.395 \noindent
1.396 @@ -955,11 +943,10 @@
1.397 elements from known ones. The set $\textit{odd}$ consists of all the values
1.398 reachable through the reflexive transitive closure of
1.399 $\textit{odd}_{\textrm{step}}$ starting with any element from
1.400 -$\textit{odd}_{\textrm{base}}$, namely 1, 3, 5, 7, and 9. Using Kodkod's
1.401 +$\textit{odd}_{\textrm{base}}$, namely 1 and 3. Using Kodkod's
1.402 transitive closure to encode linear predicates is normally either more thorough
1.403 or more efficient than unrolling (depending on the value of \textit{iter}), but
1.404 -for those cases where it isn't you can disable it by passing the
1.405 -\textit{dont\_star\_linear\_preds} option.
1.406 +you can disable it by passing the \textit{dont\_star\_linear\_preds} option.
1.407
1.408 \subsection{Coinductive Datatypes}
1.409 \label{coinductive-datatypes}
1.410 @@ -985,7 +972,7 @@
1.411 finite lists:
1.412
1.413 \prew
1.414 -\textbf{lemma} ``$\textit{xs} \not= \textit{LCons}~a~\textit{xs}$'' \\
1.415 +\textbf{lemma} ``$\textit{xs} \not= \textit{LCons}~a~\textit{xs\/}$'' \\
1.416 \textbf{nitpick} \\[2\smallskipamount]
1.417 \slshape Nitpick found a counterexample for {\itshape card}~$'a$ = 1: \\[2\smallskipamount]
1.418 \hbox{}\qquad Free variables: \nopagebreak \\
1.419 @@ -1001,9 +988,9 @@
1.420
1.421 \prew
1.422 \textbf{lemma}~``$\lbrakk\textit{xs} = \textit{LCons}~a~\textit{xs};\>\,
1.423 -\textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
1.424 +\textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys\/}$'' \\
1.425 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
1.426 -\slshape The type ``\kern1pt$'a$'' passed the monotonicity test. Nitpick might be able to skip
1.427 +\slshape The type $'a$ passed the monotonicity test. Nitpick might be able to skip
1.428 some scopes. \\[2\smallskipamount]
1.429 Trying 10 scopes: \\
1.430 \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 1,
1.431 @@ -1011,8 +998,11 @@
1.432 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1.433 \hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 10,
1.434 and \textit{bisim\_depth}~= 9. \\[2\smallskipamount]
1.435 +Limit reached: arity 11 of Kodkod relation associated with
1.436 +``\textit{Set.insert\/}'' too large for universe of cardinality 9. Skipping scope.
1.437 +\\[2\smallskipamount]
1.438 Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
1.439 -\textit{card}~``\kern1pt$'a~\textit{list\/}$''~= 2, and \textit{bisim\_\allowbreak
1.440 +\textit{card}~``\kern1pt$'a~\textit{llist\/}$''~= 2, and \textit{bisim\_\allowbreak
1.441 depth}~= 1:
1.442 \\[2\smallskipamount]
1.443 \hbox{}\qquad Free variables: \nopagebreak \\
1.444 @@ -1020,7 +1010,7 @@
1.445 \hbox{}\qquad\qquad $\textit{b} = a_2$ \\
1.446 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
1.447 \hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount]
1.448 -Total time: 1.02 s.
1.449 +Total time: 1.11 s.
1.450 \postw
1.451
1.452 The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas
1.453 @@ -1056,7 +1046,7 @@
1.454
1.455 \prew
1.456 \textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
1.457 -\,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
1.458 +\,\Longrightarrow\, \textit{xs} = \textit{ys\/}$'' \\
1.459 \textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
1.460 \slshape Nitpick found a quasi genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
1.461 \hbox{}\qquad Free variables: \nopagebreak \\
1.462 @@ -1153,14 +1143,14 @@
1.463 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
1.464 \slshape
1.465 Trying 10 scopes: \nopagebreak \\
1.466 -\hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 1; \\
1.467 -\hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 2; \\
1.468 +\hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm\/}$'' = 1; \\
1.469 +\hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm\/}$'' = 2; \\
1.470 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1.471 -\hbox{}\qquad \textit{card~nat}~= 10, \textit{card tm}~= 10, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 10. \\[2\smallskipamount]
1.472 +\hbox{}\qquad \textit{card~nat}~= 10, \textit{card tm}~= 10, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm\/}$'' = 10. \\[2\smallskipamount]
1.473 Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6,
1.474 -and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm}$''~= 6: \\[2\smallskipamount]
1.475 +and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm\/}$''~= 6: \\[2\smallskipamount]
1.476 \hbox{}\qquad Free variables: \nopagebreak \\
1.477 -\hbox{}\qquad\qquad $\sigma = \undef(\!\begin{aligned}[t]
1.478 +\hbox{}\qquad\qquad $\sigma = \unkef(\!\begin{aligned}[t]
1.479 & 0 := \textit{Var}~0,\>
1.480 1 := \textit{Var}~0,\>
1.481 2 := \textit{Var}~0, \\[-2pt]
1.482 @@ -1181,7 +1171,7 @@
1.483 An interesting aspect of Nitpick's verbose output is that it assigned inceasing
1.484 cardinalities from 1 to 10 to the type $\textit{nat} \Rightarrow \textit{tm}$.
1.485 For the formula of interest, knowing 6 values of that type was enough to find
1.486 -the counterexample. Without boxing, $46\,656$ ($= 6^6$) values must be
1.487 +the counterexample. Without boxing, $6^6 = 46\,656$ values must be
1.488 considered, a hopeless undertaking:
1.489
1.490 \prew
1.491 @@ -1189,15 +1179,14 @@
1.492 {\slshape Nitpick ran out of time after checking 3 of 10 scopes.}
1.493 \postw
1.494
1.495 -{\looseness=-1
1.496 Boxing can be enabled or disabled globally or on a per-type basis using the
1.497 \textit{box} option. Nitpick usually performs reasonable choices about which
1.498 -types should be boxed, but option tweaking sometimes helps. A related optimization,
1.499 -``finalization,'' attempts to wrap functions that constant at all but finitely
1.500 -many points (e.g., finite sets); see the documentation for the \textit{finalize}
1.501 -option in \S\ref{scope-of-search} for details.
1.502 -
1.503 -}
1.504 +types should be boxed, but option tweaking sometimes helps.
1.505 +
1.506 +%A related optimization,
1.507 +%``finitization,'' attempts to wrap functions that are constant at all but finitely
1.508 +%many points (e.g., finite sets); see the documentation for the \textit{finitize}
1.509 +%option in \S\ref{scope-of-search} for details.
1.510
1.511 \subsection{Scope Monotonicity}
1.512 \label{scope-monotonicity}
1.513 @@ -1233,7 +1222,7 @@
1.514 \prew
1.515 \textbf{nitpick}~[\textit{verbose}] \\[2\smallskipamount]
1.516 \slshape
1.517 -The types ``\kern1pt$'a$'' and ``\kern1pt$'b$'' passed the monotonicity test.
1.518 +The types $'a$ and $'b$ passed the monotonicity test.
1.519 Nitpick might be able to skip some scopes.
1.520 \\[2\smallskipamount]
1.521 Trying 10 scopes: \\
1.522 @@ -1447,11 +1436,11 @@
1.523 \hbox{}\qquad Datatype: \nopagebreak \\
1.524 \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\}$ \\
1.525 \hbox{}\qquad {\slshape Constants:} \nopagebreak \\
1.526 -\hbox{}\qquad\qquad $\textit{labels} = \undef
1.527 +\hbox{}\qquad\qquad $\textit{labels} = \unkef
1.528 (\!\begin{aligned}[t]%
1.529 & \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[-2pt]
1.530 & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\
1.531 -\hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
1.532 +\hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \unkef
1.533 (\!\begin{aligned}[t]%
1.534 & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
1.535 & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
1.536 @@ -1661,9 +1650,9 @@
1.537
1.538 \prew
1.539 \textbf{datatype} $'a$~\textit{aa\_tree} = \\
1.540 -\hbox{}\quad $\Lambda$ $\mid$ $N$ ``\kern1pt$'a\Colon \textit{linorder}$'' \textit{nat} ``\kern1pt$'a$ \textit{aa\_tree}'' ``\kern1pt$'a$ \textit{aa\_tree}'' \\[2\smallskipamount]
1.541 +\hbox{}\quad $\Lambda$ $\mid$ $N$ ``\kern1pt$'a\Colon \textit{linorder\/}$'' \textit{nat} ``\kern1pt$'a$ \textit{aa\_tree}'' ``\kern1pt$'a$ \textit{aa\_tree}'' \\[2\smallskipamount]
1.542 \textbf{primrec} \textit{data} \textbf{where} \\
1.543 -``$\textit{data}~\Lambda = \undef$'' $\,\mid$ \\
1.544 +``$\textit{data}~\Lambda = \unkef$'' $\,\mid$ \\
1.545 ``$\textit{data}~(N~x~\_~\_~\_) = x$'' \\[2\smallskipamount]
1.546 \textbf{primrec} \textit{dataset} \textbf{where} \\
1.547 ``$\textit{dataset}~\Lambda = \{\}$'' $\,\mid$ \\
1.548 @@ -1710,7 +1699,7 @@
1.549
1.550 \prew
1.551 \textbf{primrec} \textit{wf} \textbf{where} \\
1.552 -``$\textit{wf}~\Lambda = \textit{True}$'' $\,\mid$ \\
1.553 +``$\textit{wf}~\Lambda = \textit{True\/}$'' $\,\mid$ \\
1.554 ``$\textit{wf}~(N~\_~k~t~u) =$ \\
1.555 \phantom{``}$(\textrm{if}~t = \Lambda~\textrm{then}$ \\
1.556 \phantom{``$(\quad$}$k = 1 \mathrel{\land} (u = \Lambda \mathrel{\lor} (\textit{level}~u = 1 \mathrel{\land} \textit{left}~u = \Lambda \mathrel{\land} \textit{right}~u = \Lambda))$ \\
1.557 @@ -2849,7 +2838,7 @@
1.558 \prew
1.559 \textbf{primrec} \textit{prec} \textbf{where} \\
1.560 ``$\textit{prec}~(\textit{Suc}~n) = n$'' \\[2\smallskipamount]
1.561 -\textbf{lemma} ``$\textit{prec}~0 = \undef$'' \\
1.562 +\textbf{lemma} ``$\textit{prec}~0 = \textit{undefined\/}$'' \\
1.563 \textbf{nitpick} \\[2\smallskipamount]
1.564 \quad{\slshape Nitpick found a counterexample for \textit{card nat}~= 2:
1.565 \nopagebreak