1.1 --- a/doc-src/Nitpick/nitpick.tex Mon Feb 01 14:12:12 2010 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Tue Feb 02 11:38:38 2010 +0100
1.3 @@ -25,8 +25,8 @@
1.4 \def\lparr{\mathopen{(\mkern-4mu\mid}}
1.5 \def\rparr{\mathclose{\mid\mkern-4mu)}}
1.6
1.7 -\def\undef{\textit{undefined}}
1.8 \def\unk{{?}}
1.9 +\def\undef{(\lambda x.\; \unk)}
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 @@ -188,8 +188,8 @@
1.14 \prew
1.15 \textbf{apply}~\textit{auto} \\[2\smallskipamount]
1.16 {\slshape goal (2 subgoals): \\
1.17 -\ 1. $P\,\Longrightarrow\, Q$ \\
1.18 -\ 2. $Q\,\Longrightarrow\, P$} \\[2\smallskipamount]
1.19 +\phantom{0}1. $P\,\Longrightarrow\, Q$ \\
1.20 +\phantom{0}2. $Q\,\Longrightarrow\, P$} \\[2\smallskipamount]
1.21 \textbf{nitpick}~1 \\[2\smallskipamount]
1.22 {\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.23 \hbox{}\qquad Free variables: \nopagebreak \\
1.24 @@ -317,11 +317,9 @@
1.25 \postw
1.26
1.27 Notice that $\textit{The}~(\lambda y.\;P~y) = \textit{The}~\{a_2, a_3\} = a_1$,
1.28 -just like before.\footnote{The \undef{} symbol's presence is explained as
1.29 -follows: In higher-order logic, any function can be built from the undefined
1.30 -function using repeated applications of the function update operator $f(x :=
1.31 -y)$, just like any list can be built from the empty list using $x \mathbin{\#}
1.32 -xs$.}
1.33 +just like before.\footnote{The Isabelle/HOL notation $f(x :=
1.34 +y)$ denotes the function that maps $x$ to $y$ and that otherwise behaves like
1.35 +$f$.}
1.36
1.37 Our misadventures with THE suggest adding `$\exists!x{.}$' (``there exists a
1.38 unique $x$ such that'') at the front of our putative lemma's assumption:
1.39 @@ -562,7 +560,7 @@
1.40 {\slshape Datatype:} \\
1.41 \hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_3, a_3],\, [a_3],\, \unr\}$ \\
1.42 {\slshape Constants:} \\
1.43 -\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_3, a_3],\> [a_3, a_3] := \unk,\> [a_3] := \unk)$ \\
1.44 +\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_3, a_3])$ \\
1.45 \hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_3, a_3] := a_3,\> [a_3] := a_3)$
1.46 \postw
1.47
1.48 @@ -1243,6 +1241,208 @@
1.49 \textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
1.50 consider only 8~scopes instead of $32\,768$.
1.51
1.52 +\subsection{Inductive Properties}
1.53 +\label{inductive-properties}
1.54 +
1.55 +Inductive properties are a particular pain to prove, because the failure to
1.56 +establish an induction step can mean several things:
1.57 +%
1.58 +\begin{enumerate}
1.59 +\item The property is invalid.
1.60 +\item The property is valid but is too weak to support the induction step.
1.61 +\item The property is valid and strong enough; it's just that we haven't found
1.62 +the proof yet.
1.63 +\end{enumerate}
1.64 +%
1.65 +Depending on which scenario applies, we would take the appropriate course of
1.66 +action:
1.67 +%
1.68 +\begin{enumerate}
1.69 +\item Repair the statement of the property so that it becomes valid.
1.70 +\item Generalize the property and/or prove auxiliary properties.
1.71 +\item Work harder on a proof.
1.72 +\end{enumerate}
1.73 +%
1.74 +How can we distinguish between the three scenarios? Nitpick's normal mode of
1.75 +operation can often detect scenario 1, and Isabelle's automatic tactics help with
1.76 +scenario 3. Using appropriate techniques, it is also often possible to use
1.77 +Nitpick to identify scenario 2. Consider the following transition system,
1.78 +in which natural numbers represent states:
1.79 +
1.80 +\prew
1.81 +\textbf{inductive\_set}~\textit{reach}~\textbf{where} \\
1.82 +``$(4\Colon\textit{nat}) \in \textit{reach\/}$'' $\mid$ \\
1.83 +``$\lbrakk n < 4;\> n \in \textit{reach\/}\rbrakk \,\Longrightarrow\, 3 * n + 1 \in \textit{reach\/}$'' $\mid$ \\
1.84 +``$n \in \textit{reach} \,\Longrightarrow n + 2 \in \textit{reach\/}$''
1.85 +\postw
1.86 +
1.87 +We will try to prove that only even numbers are reachable:
1.88 +
1.89 +\prew
1.90 +\textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n$''
1.91 +\postw
1.92 +
1.93 +Does this property hold? Nitpick cannot find a counterexample within 30 seconds,
1.94 +so let's attempt a proof by induction:
1.95 +
1.96 +\prew
1.97 +\textbf{apply}~(\textit{induct~set}{:}~\textit{reach\/}) \\
1.98 +\textbf{apply}~\textit{auto}
1.99 +\postw
1.100 +
1.101 +This leaves us in the following proof state:
1.102 +
1.103 +\prew
1.104 +{\slshape goal (2 subgoals): \\
1.105 +\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)$ \\
1.106 +\phantom{0}2. ${\bigwedge}n.\;\, \lbrakk n \in \textit{reach\/};\, 2~\textsl{dvd}~n\rbrakk \,\Longrightarrow\, 2~\textsl{dvd}~\textit{Suc}~(\textit{Suc}~n)$
1.107 +}
1.108 +\postw
1.109 +
1.110 +If we run Nitpick on the first subgoal, it still won't find any
1.111 +counterexample; and yet, \textit{auto} fails to go further, and \textit{arith}
1.112 +is helpless. However, notice the $n \in \textit{reach}$ assumption, which
1.113 +strengthens the induction hypothesis but is not immediately usable in the proof.
1.114 +If we remove it and invoke Nitpick, this time we get a counterexample:
1.115 +
1.116 +\prew
1.117 +\textbf{apply}~(\textit{thin\_tac}~``$n \in \textit{reach\/}$'') \\
1.118 +\textbf{nitpick} \\[2\smallskipamount]
1.119 +\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.120 +\hbox{}\qquad Skolem constant: \nopagebreak \\
1.121 +\hbox{}\qquad\qquad $n = 0$
1.122 +\postw
1.123 +
1.124 +Indeed, 0 < 4, 2 divides 0, but 2 does not divide 1. We can use this information
1.125 +to strength the lemma:
1.126 +
1.127 +\prew
1.128 +\textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \not= 0$''
1.129 +\postw
1.130 +
1.131 +Unfortunately, the proof by induction still gets stuck, except that Nitpick now
1.132 +finds the counterexample $n = 2$. We generalize the lemma further to
1.133 +
1.134 +\prew
1.135 +\textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \ge 4$''
1.136 +\postw
1.137 +
1.138 +and this time \textit{arith} can finish off the subgoals.
1.139 +
1.140 +A similar technique can be employed for structural induction. The
1.141 +following mini-formalization of full binary trees will serve as illustration:
1.142 +
1.143 +\prew
1.144 +\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]
1.145 +\textbf{primrec}~\textit{labels}~\textbf{where} \\
1.146 +``$\textit{labels}~(\textit{Leaf}~a) = \{a\}$'' $\mid$ \\
1.147 +``$\textit{labels}~(\textit{Branch}~t~u) = \textit{labels}~t \mathrel{\cup} \textit{labels}~u$'' \\[2\smallskipamount]
1.148 +\textbf{primrec}~\textit{swap}~\textbf{where} \\
1.149 +``$\textit{swap}~(\textit{Leaf}~c)~a~b =$ \\
1.150 +\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$ \\
1.151 +``$\textit{swap}~(\textit{Branch}~t~u)~a~b = \textit{Branch}~(\textit{swap}~t~a~b)~(\textit{swap}~u~a~b)$''
1.152 +\postw
1.153 +
1.154 +The \textit{labels} function returns the set of labels occurring on leaves of a
1.155 +tree, and \textit{swap} exchanges two labels. Intuitively, if two distinct
1.156 +labels $a$ and $b$ occur in a tree $t$, they should also occur in the tree
1.157 +obtained by swapping $a$ and $b$:
1.158 +
1.159 +\prew
1.160 +\textbf{lemma} $``\lbrakk a \in \textit{labels}~t;\, b \in \textit{labels}~t;\, a \not= b\rbrakk {}$ \\
1.161 +\phantom{\textbf{lemma} ``}$\,{\Longrightarrow}{\;\,} \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
1.162 +\postw
1.163 +
1.164 +Nitpick can't find any counterexample, so we proceed with induction
1.165 +(this time favoring a more structured style):
1.166 +
1.167 +\prew
1.168 +\textbf{proof}~(\textit{induct}~$t$) \\
1.169 +\hbox{}\quad \textbf{case}~\textit{Leaf}~\textbf{thus}~\textit{?case}~\textbf{by}~\textit{simp} \\
1.170 +\textbf{next} \\
1.171 +\hbox{}\quad \textbf{case}~$(\textit{Branch}~t~u)$~\textbf{thus} \textit{?case}
1.172 +\postw
1.173 +
1.174 +Nitpick can't find any counterexample at this point either, but it makes the
1.175 +following suggestion:
1.176 +
1.177 +\prew
1.178 +\slshape
1.179 +Hint: To check that the induction hypothesis is general enough, try the following command:
1.180 +\textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_consts}].
1.181 +\postw
1.182 +
1.183 +If we follow the hint, we get a ``nonstandard'' counterexample for the step:
1.184 +
1.185 +\prew
1.186 +\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
1.187 +\hbox{}\qquad Free variables: \nopagebreak \\
1.188 +\hbox{}\qquad\qquad $a = a_4$ \\
1.189 +\hbox{}\qquad\qquad $b = a_3$ \\
1.190 +\hbox{}\qquad\qquad $t = \xi_3$ \\
1.191 +\hbox{}\qquad\qquad $u = \xi_4$ \\
1.192 +\hbox{}\qquad {\slshape Constants:} \nopagebreak \\
1.193 +\hbox{}\qquad\qquad $\textit{labels} = \undef
1.194 + (\!\begin{aligned}[t]%
1.195 + & \xi_3 := \{a_4\},\> \xi_4 := \{a_1, a_3\}, \\[-2pt] %% TYPESETTING
1.196 + & \textit{Branch}~\xi_3~\xi_3 := \{a_4\}, \\[-2pt]
1.197 + & \textit{Branch}~\xi_3~\xi_4 := \{a_1, a_3, a_4\})\end{aligned}$ \\
1.198 +\hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
1.199 + (\!\begin{aligned}[t]%
1.200 + & \xi_3 := \xi_3,\> \xi_4 := \xi_3, \\[-2pt]
1.201 + & \textit{Branch}~\xi_3~\xi_3 := \textit{Branch}~\xi_3~\xi_3, \\[-2pt]
1.202 + & \textit{Branch}~\xi_4~\xi_3 := \textit{Branch}~\xi_3~\xi_3)\end{aligned}$ \\[2\smallskipamount]
1.203 +The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
1.204 +even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
1.205 +\postw
1.206 +
1.207 +Reading the Nitpick manual is a most excellent idea.
1.208 +But what's going on? The \textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$''
1.209 +option told the tool to look for nonstandard models of binary trees, which
1.210 +means that new ``nonstandard'' trees $\xi_1, \xi_2, \ldots$, are now allowed in
1.211 +addition to the standard trees generated by the \textit{Leaf} and
1.212 +\textit{Branch} constructors.%
1.213 +\footnote{Notice the similarity between allowing nonstandard trees here and
1.214 +allowing unreachable states in the preceding example (by removing the ``$n \in
1.215 +\textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
1.216 +set of objects over which the induction is performed while doing the step
1.217 +so as to test the induction hypothesis's strength.}
1.218 +The new trees are so nonstandard that we know nothing about them, except what
1.219 +the induction hypothesis states and what can be proved about all trees without
1.220 +relying on induction or case distinction. The key observation is,
1.221 +%
1.222 +\begin{quote}
1.223 +\textsl{If the induction
1.224 +hypothesis is strong enough, the induction step will hold even for nonstandard
1.225 +objects, and Nitpick won't find any nonstandard counterexample.}
1.226 +\end{quote}
1.227 +%
1.228 +But here, Nitpick did find some nonstandard trees $t = \xi_3$
1.229 +and $u = \xi_4$ such that $a \in \textit{labels}~t$, $b \notin
1.230 +\textit{labels}~t$, $a \notin \textit{labels}~u$, and $b \in \textit{labels}~u$.
1.231 +Because neither tree contains both $a$ and $b$, the induction hypothesis tells
1.232 +us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
1.233 +and as a result we know nothing about the labels of the tree
1.234 +$\textit{swap}~(\textit{Branch}~t~u)~a~b$, which by definition equals
1.235 +$\textit{Branch}$ $(\textit{swap}~t~a~b)$ $(\textit{swap}~u~a~b)$, whose
1.236 +labels are $\textit{labels}$ $(\textit{swap}~t~a~b) \mathrel{\cup}
1.237 +\textit{labels}$ $(\textit{swap}~u~a~b)$.
1.238 +
1.239 +The solution is to ensure that we always know what the labels of the subtrees
1.240 +are in the inductive step, by covering the cases where $a$ and/or~$b$ is not in
1.241 +$t$ in the statement of the lemma:
1.242 +
1.243 +\prew
1.244 +\textbf{lemma} ``$\textit{labels}~(\textit{swap}~t~a~b) = {}$ \\
1.245 +\phantom{\textbf{lemma} ``}$(\textrm{if}~a \in \textit{labels}~t~\textrm{then}$ \nopagebreak \\
1.246 +\phantom{\textbf{lemma} ``(\quad}$\textrm{if}~b \in \textit{labels}~t~\textrm{then}~\textit{labels}~t~\textrm{else}~(\textit{labels}~t - \{a\}) \mathrel{\cup} \{b\}$ \\
1.247 +\phantom{\textbf{lemma} ``(}$\textrm{else}$ \\
1.248 +\phantom{\textbf{lemma} ``(\quad}$\textrm{if}~b \in \textit{labels}~t~\textrm{then}~(\textit{labels}~t - \{b\}) \mathrel{\cup} \{a\}~\textrm{else}~\textit{labels}~t)$''
1.249 +\postw
1.250 +
1.251 +This time, Nitpick won't find any nonstandard counterexample, and we can perform
1.252 +the induction step using \textbf{auto}.
1.253 +
1.254 \section{Case Studies}
1.255 \label{case-studies}
1.256
1.257 @@ -1398,7 +1598,8 @@
1.258 functions:
1.259
1.260 \prew
1.261 -\textbf{datatype} $'a$~\textit{tree} = $\Lambda$ $\mid$ $N$ ``\kern1pt$'a\Colon \textit{linorder}$'' \textit{nat} ``\kern1pt$'a$ \textit{tree}'' ``\kern1pt$'a$ \textit{tree}'' \\[2\smallskipamount]
1.262 +\textbf{datatype} $'a$~\textit{aa\_tree} = \\
1.263 +\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.264 \textbf{primrec} \textit{data} \textbf{where} \\
1.265 ``$\textit{data}~\Lambda = \undef$'' $\,\mid$ \\
1.266 ``$\textit{data}~(N~x~\_~\_~\_) = x$'' \\[2\smallskipamount]
1.267 @@ -1526,7 +1727,7 @@
1.268 \slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
1.269 \hbox{}\qquad Free variables: \nopagebreak \\
1.270 \hbox{}\qquad\qquad $t = N~a_3~1~\Lambda~\Lambda$ \\
1.271 -\hbox{}\qquad\qquad $x = a_4$ \\[2\smallskipamount]
1.272 +\hbox{}\qquad\qquad $x = a_4$
1.273 \postw
1.274
1.275 It's hard to see why this is a counterexample. To improve readability, we will
1.276 @@ -1583,10 +1784,11 @@
1.277 \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1.278 \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1.279 \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1.280 -\def\ops#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
1.281 -\def\opt#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
1.282 -\def\opu#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
1.283 -\def\opusmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
1.284 +\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
1.285 +\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
1.286 +\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
1.287 +\def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
1.288 +\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
1.289
1.290 Nitpick's behavior can be influenced by various options, which can be specified
1.291 in brackets after the \textbf{nitpick} command. Default values can be set
1.292 @@ -1696,7 +1898,7 @@
1.293 \label{scope-of-search}
1.294
1.295 \begin{enum}
1.296 -\opu{card}{type}{int\_seq}
1.297 +\oparg{card}{type}{int\_seq}
1.298 Specifies the sequence of cardinalities to use for a given type.
1.299 For free types, and often also for \textbf{typedecl}'d types, it usually makes
1.300 sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
1.301 @@ -1709,18 +1911,18 @@
1.302 \nopagebreak
1.303 {\small See also \textit{mono} (\S\ref{scope-of-search}).}
1.304
1.305 -\opt{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
1.306 +\opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
1.307 Specifies the default sequence of cardinalities to use. This can be overridden
1.308 on a per-type basis using the \textit{card}~\qty{type} option described above.
1.309
1.310 -\opu{max}{const}{int\_seq}
1.311 +\oparg{max}{const}{int\_seq}
1.312 Specifies the sequence of maximum multiplicities to use for a given
1.313 (co)in\-duc\-tive datatype constructor. A constructor's multiplicity is the
1.314 number of distinct values that it can construct. Nonsensical values (e.g.,
1.315 \textit{max}~[]~$=$~2) are silently repaired. This option is only available for
1.316 datatypes equipped with several constructors.
1.317
1.318 -\ops{max}{int\_seq}
1.319 +\opnodefault{max}{int\_seq}
1.320 Specifies the default sequence of maximum multiplicities to use for
1.321 (co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor
1.322 basis using the \textit{max}~\qty{const} option described above.
1.323 @@ -1757,13 +1959,13 @@
1.324 {\small See also \textit{bits} (\S\ref{scope-of-search}) and
1.325 \textit{show\_datatypes} (\S\ref{output-format}).}
1.326
1.327 -\opt{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$}
1.328 +\opdefault{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$}
1.329 Specifies the number of bits to use to represent natural numbers and integers in
1.330 binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
1.331
1.332 {\small See also \textit{binary\_ints} (\S\ref{scope-of-search}).}
1.333
1.334 -\opusmart{wf}{const}{non\_wf}
1.335 +\opargboolorsmart{wf}{const}{non\_wf}
1.336 Specifies whether the specified (co)in\-duc\-tively defined predicate is
1.337 well-founded. The option can take the following values:
1.338
1.339 @@ -1780,7 +1982,7 @@
1.340
1.341 \item[$\bullet$] \textbf{\textit{smart}}: Try to prove that the inductive
1.342 predicate is well-founded using Isabelle's \textit{lexicographic\_order} and
1.343 -\textit{sizechange} tactics. If this succeeds (or the predicate occurs with an
1.344 +\textit{size\_change} tactics. If this succeeds (or the predicate occurs with an
1.345 appropriate polarity in the formula to falsify), use an efficient fixed point
1.346 equation as specification of the predicate; otherwise, unroll the predicates
1.347 according to the \textit{iter}~\qty{const} and \textit{iter} options.
1.348 @@ -1795,7 +1997,7 @@
1.349 Specifies the default wellfoundedness setting to use. This can be overridden on
1.350 a per-predicate basis using the \textit{wf}~\qty{const} option above.
1.351
1.352 -\opu{iter}{const}{int\_seq}
1.353 +\oparg{iter}{const}{int\_seq}
1.354 Specifies the sequence of iteration counts to use when unrolling a given
1.355 (co)in\-duc\-tive predicate. By default, unrolling is applied for inductive
1.356 predicates that occur negatively and coinductive predicates that occur
1.357 @@ -1807,12 +2009,12 @@
1.358 {\small See also \textit{wf} (\S\ref{scope-of-search}) and
1.359 \textit{star\_linear\_preds} (\S\ref{optimizations}).}
1.360
1.361 -\opt{iter}{int\_seq}{$\mathbf{1{,}2{,}4{,}8{,}12{,}16{,}24{,}32}$}
1.362 +\opdefault{iter}{int\_seq}{$\mathbf{1{,}2{,}4{,}8{,}12{,}16{,}24{,}32}$}
1.363 Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive
1.364 predicates. This can be overridden on a per-predicate basis using the
1.365 \textit{iter} \qty{const} option above.
1.366
1.367 -\opt{bisim\_depth}{int\_seq}{$\mathbf{7}$}
1.368 +\opdefault{bisim\_depth}{int\_seq}{$\mathbf{7}$}
1.369 Specifies the sequence of iteration counts to use when unrolling the
1.370 bisimilarity predicate generated by Nitpick for coinductive datatypes. A value
1.371 of $-1$ means that no predicate is generated, in which case Nitpick performs an
1.372 @@ -1822,7 +2024,7 @@
1.373 the sum of the cardinalities of the coinductive datatypes occurring in the
1.374 formula to falsify.
1.375
1.376 -\opusmart{box}{type}{dont\_box}
1.377 +\opargboolorsmart{box}{type}{dont\_box}
1.378 Specifies whether Nitpick should attempt to wrap (``box'') a given function or
1.379 product type in an isomorphic datatype internally. Boxing is an effective mean
1.380 to reduce the search space and speed up Nitpick, because the isomorphic datatype
1.381 @@ -1850,8 +2052,8 @@
1.382 Specifies the default boxing setting to use. This can be overridden on a
1.383 per-type basis using the \textit{box}~\qty{type} option described above.
1.384
1.385 -\opusmart{mono}{type}{non\_mono}
1.386 -Specifies whether the specified type should be considered monotonic when
1.387 +\opargboolorsmart{mono}{type}{non\_mono}
1.388 +Specifies whether the given type should be considered monotonic when
1.389 enumerating scopes. If the option is set to \textit{smart}, Nitpick performs a
1.390 monotonicity check on the type. Setting this option to \textit{true} can reduce
1.391 the number of scopes tried, but it also diminishes the theoretical chance of
1.392 @@ -1873,6 +2075,15 @@
1.393 theoretical chance of finding a counterexample.
1.394
1.395 {\small See also \textit{mono} (\S\ref{scope-of-search}).}
1.396 +
1.397 +\opargbool{std}{type}{non\_std}
1.398 +Specifies whether the given type should be given standard models.
1.399 +Nonstandard models are unsound but can help debug inductive arguments,
1.400 +as explained in \S\ref{inductive-properties}.
1.401 +
1.402 +\optrue{std}{non\_std}
1.403 +Specifies the default standardness to use. This can be overridden on a per-type
1.404 +basis using the \textit{std}~\qty{type} option described above.
1.405 \end{enum}
1.406
1.407 \subsection{Output Format}
1.408 @@ -1919,7 +2130,7 @@
1.409 Enabling this option effectively enables \textit{show\_skolems},
1.410 \textit{show\_datatypes}, and \textit{show\_consts}.
1.411
1.412 -\opt{max\_potential}{int}{$\mathbf{1}$}
1.413 +\opdefault{max\_potential}{int}{$\mathbf{1}$}
1.414 Specifies the maximum number of potential counterexamples to display. Setting
1.415 this option to 0 speeds up the search for a genuine counterexample. This option
1.416 is implicitly set to 0 for automatic runs. If you set this option to a value
1.417 @@ -1933,7 +2144,7 @@
1.418 {\small See also \textit{check\_potential} (\S\ref{authentication}) and
1.419 \textit{sat\_solver} (\S\ref{optimizations}).}
1.420
1.421 -\opt{max\_genuine}{int}{$\mathbf{1}$}
1.422 +\opdefault{max\_genuine}{int}{$\mathbf{1}$}
1.423 Specifies the maximum number of genuine counterexamples to display. If you set
1.424 this option to a value greater than 1, you will need an incremental SAT solver:
1.425 For efficiency, it is recommended to install the JNI version of MiniSat and set
1.426 @@ -1945,12 +2156,12 @@
1.427 {\small See also \textit{check\_genuine} (\S\ref{authentication}) and
1.428 \textit{sat\_solver} (\S\ref{optimizations}).}
1.429
1.430 -\ops{eval}{term\_list}
1.431 +\opnodefault{eval}{term\_list}
1.432 Specifies the list of terms whose values should be displayed along with
1.433 counterexamples. This option suffers from an ``observer effect'': Nitpick might
1.434 find different counterexamples for different values of this option.
1.435
1.436 -\opu{format}{term}{int\_seq}
1.437 +\oparg{format}{term}{int\_seq}
1.438 Specifies how to uncurry the value displayed for a variable or constant.
1.439 Uncurrying sometimes increases the readability of the output for high-arity
1.440 functions. For example, given the variable $y \mathbin{\Colon} {'a}\Rightarrow
1.441 @@ -1966,7 +2177,7 @@
1.442 \nopagebreak
1.443 {\small See also \textit{uncurry} (\S\ref{optimizations}).}
1.444
1.445 -\opt{format}{int\_seq}{$\mathbf{1}$}
1.446 +\opdefault{format}{int\_seq}{$\mathbf{1}$}
1.447 Specifies the default format to use. Irrespective of the default format, the
1.448 extra arguments to a Skolem constant corresponding to the outer bound variables
1.449 are kept separated from the remaining arguments, the \textbf{for} arguments of
1.450 @@ -1999,7 +2210,7 @@
1.451 \nopagebreak
1.452 {\small See also \textit{max\_genuine} (\S\ref{output-format}).}
1.453
1.454 -\ops{expect}{string}
1.455 +\opnodefault{expect}{string}
1.456 Specifies the expected outcome, which must be one of the following:
1.457
1.458 \begin{enum}
1.459 @@ -2025,7 +2236,7 @@
1.460 \sloppy
1.461
1.462 \begin{enum}
1.463 -\opt{sat\_solver}{string}{smart}
1.464 +\opdefault{sat\_solver}{string}{smart}
1.465 Specifies which SAT solver to use. SAT solvers implemented in C or \cpp{} tend
1.466 to be faster than their Java counterparts, but they can be more difficult to
1.467 install. Also, if you set the \textit{max\_potential} (\S\ref{output-format}) or
1.468 @@ -2118,7 +2329,7 @@
1.469 \end{enum}
1.470 \fussy
1.471
1.472 -\opt{batch\_size}{int\_or\_smart}{smart}
1.473 +\opdefault{batch\_size}{int\_or\_smart}{smart}
1.474 Specifies the maximum number of Kodkod problems that should be lumped together
1.475 when invoking Kodkodi. Each problem corresponds to one scope. Lumping problems
1.476 together ensures that Kodkodi is launched less often, but it makes the verbose
1.477 @@ -2188,7 +2399,7 @@
1.478 Unless you are tracking down a bug in Nitpick or distrust the peephole
1.479 optimizer, you should leave this option enabled.
1.480
1.481 -\opt{sym\_break}{int}{20}
1.482 +\opdefault{sym\_break}{int}{20}
1.483 Specifies an upper bound on the number of relations for which Kodkod generates
1.484 symmetry breaking predicates. According to the Kodkod documentation
1.485 \cite{kodkod-2009-options}, ``in general, the higher this value, the more
1.486 @@ -2196,7 +2407,7 @@
1.487 setting the value too high may have the opposite effect and slow down the
1.488 solving.''
1.489
1.490 -\opt{sharing\_depth}{int}{3}
1.491 +\opdefault{sharing\_depth}{int}{3}
1.492 Specifies the depth to which Kodkod should check circuits for equivalence during
1.493 the translation to SAT. The default of 3 is the same as in Alloy. The minimum
1.494 allowed depth is 1. Increasing the sharing may result in a smaller SAT problem,
1.495 @@ -2207,7 +2418,7 @@
1.496 Although this might sound like a good idea, in practice it can drastically slow
1.497 down Kodkod.
1.498
1.499 -\opt{max\_threads}{int}{0}
1.500 +\opdefault{max\_threads}{int}{0}
1.501 Specifies the maximum number of threads to use in Kodkod. If this option is set
1.502 to 0, Kodkod will compute an appropriate value based on the number of processor
1.503 cores available.
1.504 @@ -2221,7 +2432,7 @@
1.505 \label{timeouts}
1.506
1.507 \begin{enum}
1.508 -\opt{timeout}{time}{$\mathbf{30}$ s}
1.509 +\opdefault{timeout}{time}{$\mathbf{30}$ s}
1.510 Specifies the maximum amount of time that the \textbf{nitpick} command should
1.511 spend looking for a counterexample. Nitpick tries to honor this constraint as
1.512 well as it can but offers no guarantees. For automatic runs,
1.513 @@ -2232,10 +2443,10 @@
1.514 \nopagebreak
1.515 {\small See also \textit{max\_threads} (\S\ref{optimizations}).}
1.516
1.517 -\opt{tac\_timeout}{time}{$\mathbf{500}$\,ms}
1.518 +\opdefault{tac\_timeout}{time}{$\mathbf{500}$\,ms}
1.519 Specifies the maximum amount of time that the \textit{auto} tactic should use
1.520 when checking a counterexample, and similarly that \textit{lexicographic\_order}
1.521 -and \textit{sizechange} should use when checking whether a (co)in\-duc\-tive
1.522 +and \textit{size\_change} should use when checking whether a (co)in\-duc\-tive
1.523 predicate is well-founded. Nitpick tries to honor this constraint as well as it
1.524 can but offers no guarantees.
1.525
1.526 @@ -2477,7 +2688,7 @@
1.527 \nopagebreak
1.528 \\[2\smallskipamount]
1.529 \hbox{}\qquad Empty assignment} \nopagebreak\\[2\smallskipamount]
1.530 -\textbf{by}~(\textit{auto simp}: \textit{prec\_def})
1.531 +\textbf{by}~(\textit{auto simp}:~\textit{prec\_def})
1.532 \postw
1.533
1.534 Such theorems are considered bad style because they rely on the internal