# HG changeset patch # User blanchet # Date 1300369433 -3600 # Node ID 0e4716fa330a7f24a8d03c6af3b6774ceb3ae184 # Parent ea02b9ee30854b73c27ef8dc3c066d5009bc676c reword Nitpick's wording concerning potential counterexamples diff -r ea02b9ee3085 -r 0e4716fa330a doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Thu Mar 17 14:43:51 2011 +0100 +++ b/doc-src/Nitpick/nitpick.tex Thu Mar 17 14:43:53 2011 +0100 @@ -467,25 +467,26 @@ \postw With infinite types, we don't always have the luxury of a genuine counterexample -and must often content ourselves with a potential one. The tedious task of -finding out whether the potential counterexample is in fact genuine can be -outsourced to \textit{auto} by passing \textit{check\_potential}. For example: +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}. +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] \slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported -fragment. Only potential counterexamples may be found. \\[2\smallskipamount] -Nitpick found a potential counterexample: \\[2\smallskipamount] +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. \postw -You might wonder why the counterexample is first reported as potential. The root -of the problem 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 +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.\; +\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 @@ -797,9 +798,9 @@ Nitpick can compute it efficiently. \\[2\smallskipamount] Trying 1 scope: \\ \hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount] -Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount] +Nitpick found a potentially spurious counterexample for \textit{card nat}~= 50: \\[2\smallskipamount] \hbox{}\qquad Empty assignment \\[2\smallskipamount] -Nitpick could not find a better counterexample. It checked 0 of 1 scope. \\[2\smallskipamount] +Nitpick could not find a better counterexample. \\[2\smallskipamount] Total time: 1.43 s. \postw @@ -2189,7 +2190,7 @@ \opfalse{show\_datatypes}{hide\_datatypes} Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should be displayed as part of counterexamples. Such subsets are sometimes helpful when -investigating whether a potential counterexample is genuine or spurious, but +investigating whether a potentially spurious counterexample is genuine, but their potential for clutter is real. \opfalse{show\_consts}{hide\_consts} @@ -2202,10 +2203,10 @@ Abbreviation for \textit{show\_datatypes} and \textit{show\_consts}. \opdefault{max\_potential}{int}{\upshape 1} -Specifies the maximum number of potential counterexamples to display. Setting -this option to 0 speeds up the search for a genuine counterexample. This option -is implicitly set to 0 for automatic runs. If you set this option to a value -greater than 1, you will need an incremental SAT solver, such as +Specifies the maximum number of potentially spurious counterexamples to display. +Setting this option to 0 speeds up the search for a genuine counterexample. This +option is implicitly set to 0 for automatic runs. If you set this option to a +value greater than 1, you will need an incremental SAT solver, such as \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that many of the counterexamples may be identical. @@ -2269,9 +2270,10 @@ \begin{enum} \opfalse{check\_potential}{trust\_potential} -Specifies whether potential counterexamples should be given to Isabelle's -\textit{auto} tactic to assess their validity. If a potential counterexample is -shown to be genuine, Nitpick displays a message to this effect and terminates. +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}).} @@ -2294,7 +2296,8 @@ \item[$\bullet$] \textbf{\textit{quasi\_genuine}:} Nitpick found a ``quasi genuine'' counterexample (i.e., a counterexample that is genuine unless it contradicts a missing axiom or a dangerous option was used inappropriately). -\item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potential counterexample. +\item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potentially +spurious counterexample. \item[$\bullet$] \textbf{\textit{none}:} Nitpick found no counterexample. \item[$\bullet$] \textbf{\textit{unknown}:} Nitpick encountered some problem (e.g., Kodkod ran out of memory). diff -r ea02b9ee3085 -r 0e4716fa330a src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 17 14:43:51 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 17 14:43:53 2011 +0100 @@ -605,16 +605,16 @@ NONE else (Unsynchronized.change too_big_scopes (cons scope); - print_v (fn () => ("Limit reached: " ^ msg ^ - ". Skipping " ^ (if unsound then "potential" - else "genuine") ^ - " component of scope.")); + print_v (fn () => + "Limit reached: " ^ msg ^ ". Skipping " ^ + (if unsound then "potential component of " else "") ^ + "scope."); NONE) | TOO_SMALL (_, msg) => - (print_v (fn () => ("Limit reached: " ^ msg ^ - ". Skipping " ^ (if unsound then "potential" - else "genuine") ^ - " component of scope.")); + (print_v (fn () => + "Limit reached: " ^ msg ^ ". Skipping " ^ + (if unsound then "potential component of " else "") ^ + "scope."); NONE) val das_wort_model = @@ -651,7 +651,7 @@ (pprint (Pretty.chunks [Pretty.blk (0, (pstrs ((if auto then "Auto " else "") ^ "Nitpick found a" ^ - (if not genuine then " potential " + (if not genuine then " potentially spurious " else if genuine_means_genuine then " " else " quasi genuine ") ^ das_wort_model) @ (case pretties_for_scope scope verbose of @@ -908,7 +908,8 @@ \fragment." ^ (if exists (not o KK.is_problem_trivially_false o fst) unsound_problems then - " Only potential " ^ das_wort_model ^ "s may be found." + " Only potentially spurious " ^ das_wort_model ^ + "s may be found." else "")) else