--- a/src/Doc/Nitpick/document/root.tex Fri May 29 17:17:50 2015 +0200
+++ b/src/Doc/Nitpick/document/root.tex Fri May 29 17:56:43 2015 +0200
@@ -463,35 +463,26 @@
\postw
With infinite types, we don't always have the luxury of a genuine counterexample
-and must often content ourselves with a potentially spurious one. The tedious
-task of finding out whether the potentially spurious counterexample is in fact
-genuine can be delegated to \textit{auto} by passing \textit{check\_potential}.
+and must often content ourselves with a potentially spurious one.
For example:
\prew
\textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
-\textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[2\smallskipamount]
+\textbf{nitpick} [\textit{card~nat}~= 50] \\[2\smallskipamount]
\slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
fragment. Only potentially spurious counterexamples may be found. \\[2\smallskipamount]
Nitpick found a potentially spurious counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variable: \nopagebreak \\
-\hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
-Confirmation by ``\textit{auto}'': The above counterexample is genuine.
+\hbox{}\qquad\qquad $P = \textit{False}$
\postw
-You might wonder why the counterexample is first reported as potentially
-spurious. The root of the problem is that the bound variable in $\forall n.\;
+The issue is that the bound variable in $\forall n.\;
\textit{Suc}~n \mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds
an $n$ such that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
\textit{False}; but otherwise, it does not know anything about values of $n \ge
\textit{card~nat}$ and must therefore evaluate the assumption to~$\unk$, not
-\textit{True}. Since the assumption can never be satisfied, the putative lemma
-can never be falsified.
-
-Incidentally, if you distrust the so-called genuine counterexamples, you can
-enable \textit{check\_\allowbreak genuine} to verify them as well. However, be
-aware that \textit{auto} will usually fail to prove that the counterexample is
-genuine or spurious.
+\textit{True}. Since the assumption can never be fully satisfied by Nitpick,
+the putative lemma can never be falsified.
Some conjectures involving elementary number theory make Nitpick look like a
giant with feet of clay:
@@ -1746,8 +1737,7 @@
The options are categorized as follows:\ mode of operation
(\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output
-format (\S\ref{output-format}), automatic counterexample checks
-(\S\ref{authentication}), regression testing (\S\ref{regression-testing}),
+format (\S\ref{output-format}), regression testing (\S\ref{regression-testing}),
optimizations (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
If you use Isabelle/jEdit, Nitpick also provides an automatic mode that can
@@ -1757,9 +1747,9 @@
\textit{assms} (\S\ref{mode-of-operation}), and \textit{mono}
(\S\ref{scope-of-search}) are implicitly enabled, \textit{blocking}
(\S\ref{mode-of-operation}), \textit{verbose} (\S\ref{output-format}), and
-\textit{debug} (\S\ref{output-format}) are disabled, \textit{max\_threads}
-(\S\ref{optimizations}) is taken to be 1, \textit{max\_potential}
-(\S\ref{output-format}) is taken to be 0, and \textit{timeout}
+\textit{debug} (\S\ref{output-format}) are disabled, \textit{max\_potential}
+(\S\ref{output-format}) is taken to be 0, \textit{max\_threads}
+(\S\ref{optimizations}) is taken to be 1, and \textit{timeout}
(\S\ref{timeouts}) is superseded by the ``Auto Time Limit'' in jEdit. Nitpick's
output is also more concise.
@@ -2112,8 +2102,7 @@
the counterexamples may be identical.
\nopagebreak
-{\small See also \textit{check\_potential} (\S\ref{authentication}) and
-\textit{sat\_solver} (\S\ref{optimizations}).}
+{\small See also \textit{sat\_solver} (\S\ref{optimizations}).}
\opdefault{max\_genuine}{int}{\upshape 1}
Specifies the maximum number of genuine counterexamples to display. If you set
@@ -2122,8 +2111,7 @@
many of the counterexamples may be identical.
\nopagebreak
-{\small See also \textit{check\_genuine} (\S\ref{authentication}) and
-\textit{sat\_solver} (\S\ref{optimizations}).}
+{\small See also \textit{sat\_solver} (\S\ref{optimizations}).}
\opnodefault{eval}{term\_list}
Specifies the list of terms whose values should be displayed along with
@@ -2166,31 +2154,10 @@
the \textit{format}~\qty{term} option described above.
\end{enum}
-\subsection{Authentication}
-\label{authentication}
+\subsection{Regression Testing}
+\label{regression-testing}
\begin{enum}
-\opfalse{check\_potential}{trust\_potential}
-Specifies whether potentially spurious counterexamples should be given to
-Isabelle's \textit{auto} tactic to assess their validity. If a potentially
-spurious counterexample is shown to be genuine, Nitpick displays a message to
-this effect and terminates.
-
-\nopagebreak
-{\small See also \textit{max\_potential} (\S\ref{output-format}).}
-
-\opfalse{check\_genuine}{trust\_genuine}
-Specifies whether genuine and quasi genuine counterexamples should be given to
-Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine''
-counterexample is shown to be spurious, the user is kindly asked to send a bug
-report to the author at \authoremail.
-
-\nopagebreak
-{\small See also \textit{max\_genuine} (\S\ref{output-format}).}
-
-\subsection{Regression Testing}
-\label{regression-testing}
-
\opnodefault{expect}{string}
Specifies the expected outcome, which must be one of the following:
@@ -2426,15 +2393,12 @@
\opdefault{tac\_timeout}{float}{\upshape 0.5}
Specifies the maximum number of seconds that should be used by internal
tactics---\textit{lexicographic\_order} and \textit{size\_change} when checking
-whether a (co)in\-duc\-tive predicate is well-founded, \textit{auto} tactic when
-checking a counterexample, or the monotonicity inference. Nitpick tries to honor
-this constraint but offers no guarantees.
+whether a (co)in\-duc\-tive predicate is well-founded or the monotonicity
+inference. Nitpick tries to honor this constraint but offers no guarantees.
\nopagebreak
-{\small See also \textit{wf} (\S\ref{scope-of-search}),
-\textit{mono} (\S\ref{scope-of-search}),
-\textit{check\_potential} (\S\ref{authentication}),
-and \textit{check\_genuine} (\S\ref{authentication}).}
+{\small See also \textit{wf} (\S\ref{scope-of-search}) and
+\textit{mono} (\S\ref{scope-of-search}).}
\end{enum}
\section{Attribute Reference}
@@ -2501,7 +2465,7 @@
\nopagebreak
This attribute specifies the (free-form) specification of a constant defined
-using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command.
+using the \textbf{specification} command.
\end{enum}
When faced with a constant, Nitpick proceeds as follows:
@@ -2515,7 +2479,7 @@
constant.
\item[3.] Otherwise, if the constant was defined using the
-\hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command and the
+\allowbreak\textbf{specification} command and the
\textit{nitpick\_choice\_spec} set associated with the constant is not empty, it
uses these theorems as the specification of the constant.