doc-src/Nitpick/nitpick.tex
author blanchet
Tue, 02 Feb 2010 11:38:38 +0100
changeset 34982 7b8c366e34a2
parent 34126 8a2c5d7aff51
child 34998 5e492a862b34
permissions -rw-r--r--
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
     1
\documentclass[a4paper,12pt]{article}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
     2
\usepackage[T1]{fontenc}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
     3
\usepackage{amsmath}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
     4
\usepackage{amssymb}
33564
75ce0f60617a fixed minor problems with Nitpick's documentation
blanchet
parents: 33561
diff changeset
     5
\usepackage[english,french]{babel}
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
     6
\usepackage{color}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
     7
\usepackage{graphicx}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
     8
%\usepackage{mathpazo}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
     9
\usepackage{multicol}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    10
\usepackage{stmaryrd}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    11
%\usepackage[scaled=.85]{beramono}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    12
\usepackage{../iman,../pdfsetup}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    13
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    14
%\oddsidemargin=4.6mm
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    15
%\evensidemargin=4.6mm
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    16
%\textwidth=150mm
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    17
%\topmargin=4.6mm
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    18
%\headheight=0mm
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    19
%\headsep=0mm
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    20
%\textheight=234mm
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    21
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    22
\def\Colon{\mathord{:\mkern-1.5mu:}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    23
%\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    24
%\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    25
\def\lparr{\mathopen{(\mkern-4mu\mid}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    26
\def\rparr{\mathclose{\mid\mkern-4mu)}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    27
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    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
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    30
%\def\unr{\textit{others}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    31
\def\unr{\ldots}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    32
\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    33
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    34
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    35
\hyphenation{Mini-Sat size-change First-Steps grand-parent nit-pick
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    36
counter-example counter-examples data-type data-types co-data-type 
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    37
co-data-types in-duc-tive co-in-duc-tive}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    38
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    39
\urlstyle{tt}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    40
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    41
\begin{document}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    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
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    45
\title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    46
Picking Nits \\[\smallskipamount]
33887
d9d0faf8d511 remove version number from Nitpick manual
blanchet
parents: 33731
diff changeset
    47
\Large A User's Guide to Nitpick for Isabelle/HOL}
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    48
\author{\hbox{} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    49
Jasmin Christian Blanchette \\
33887
d9d0faf8d511 remove version number from Nitpick manual
blanchet
parents: 33731
diff changeset
    50
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    51
\hbox{}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    52
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    53
\maketitle
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    54
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    55
\tableofcontents
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    56
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    57
\setlength{\parskip}{.7em plus .2em minus .1em}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    58
\setlength{\parindent}{0pt}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    59
\setlength{\abovedisplayskip}{\parskip}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    60
\setlength{\abovedisplayshortskip}{.9\parskip}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    61
\setlength{\belowdisplayskip}{\parskip}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    62
\setlength{\belowdisplayshortskip}{.9\parskip}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    63
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    64
% General-purpose enum environment with correct spacing
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    65
\newenvironment{enum}%
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    66
    {\begin{list}{}{%
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    67
        \setlength{\topsep}{.1\parskip}%
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    68
        \setlength{\partopsep}{.1\parskip}%
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    69
        \setlength{\itemsep}{\parskip}%
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    70
        \advance\itemsep by-\parsep}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    71
    {\end{list}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    72
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    73
\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    74
\advance\rightskip by\leftmargin}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    75
\def\post{\vskip0pt plus1ex\endgroup}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    76
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    77
\def\prew{\pre\advance\rightskip by-\leftmargin}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    78
\def\postw{\post}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    79
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    80
\section{Introduction}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    81
\label{introduction}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    82
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    83
Nitpick \cite{blanchette-nipkow-2009} is a counterexample generator for
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    84
Isabelle/HOL \cite{isa-tutorial} that is designed to handle formulas
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    85
combining (co)in\-duc\-tive datatypes, (co)in\-duc\-tively defined predicates, and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    86
quantifiers. It builds on Kodkod \cite{torlak-jackson-2007}, a highly optimized
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    87
first-order relational model finder developed by the Software Design Group at
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    88
MIT. It is conceptually similar to Refute \cite{weber-2008}, from which it
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    89
borrows many ideas and code fragments, but it benefits from Kodkod's
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    90
optimizations and a new encoding scheme. The name Nitpick is shamelessly
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    91
appropriated from a now retired Alloy precursor.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    92
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    93
Nitpick is easy to use---you simply enter \textbf{nitpick} after a putative
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    94
theorem and wait a few seconds. Nonetheless, there are situations where knowing
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    95
how it works under the hood and how it reacts to various options helps
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    96
increase the test coverage. This manual also explains how to install the tool on
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    97
your workstation. Should the motivation fail you, think of the many hours of
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    98
hard work Nitpick will save you. Proving non-theorems is \textsl{hard work}.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    99
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   100
Another common use of Nitpick is to find out whether the axioms of a locale are
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   101
satisfiable, while the locale is being developed. To check this, it suffices to
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   102
write
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   103
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   104
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   105
\textbf{lemma}~``$\textit{False}$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   106
\textbf{nitpick}~[\textit{show\_all}]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   107
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   108
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   109
after the locale's \textbf{begin} keyword. To falsify \textit{False}, Nitpick
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   110
must find a model for the axioms. If it finds no model, we have an indication
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   111
that the axioms might be unsatisfiable.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   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
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   124
\newbox\boxA
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   125
\setbox\boxA=\hbox{\texttt{nospam}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   126
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   127
The known bugs and limitations at the time of writing are listed in
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   128
\S\ref{known-bugs-and-limitations}. Comments and bug reports concerning Nitpick
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   129
or this manual should be directed to
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   130
\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   131
in.\allowbreak tum.\allowbreak de}.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   132
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   133
\vskip2.5\smallskipamount
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   134
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   135
\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   136
suggesting several textual improvements.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   137
% and Perry James for reporting a typo.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   138
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   139
\section{First Steps}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   140
\label{first-steps}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   141
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   142
This section introduces Nitpick by presenting small examples. If possible, you
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   143
should try out the examples on your workstation. Your theory file should start
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   144
the standard way:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   145
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   146
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   147
\textbf{theory}~\textit{Scratch} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   148
\textbf{imports}~\textit{Main} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   149
\textbf{begin}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   150
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   151
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   152
The results presented here were obtained using the JNI version of MiniSat and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   153
with multithreading disabled to reduce nondeterminism. This was done by adding
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   154
the line
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   155
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   156
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   157
\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSatJNI}, \,\textit{max\_threads}~= 1]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   158
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   159
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   160
after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   161
Kodkodi and is precompiled for the major platforms. Other SAT solvers can also
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   162
be installed, as explained in \S\ref{optimizations}. If you have already
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   163
configured SAT solvers in Isabelle (e.g., for Refute), these will also be
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   164
available to Nitpick.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   165
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   166
\subsection{Propositional Logic}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   167
\label{propositional-logic}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   168
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   169
Let's start with a trivial example from propositional logic:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   170
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   171
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   172
\textbf{lemma}~``$P \longleftrightarrow Q$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   173
\textbf{nitpick}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   174
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   175
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   176
You should get the following output:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   177
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   178
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   179
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   180
Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   181
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   182
\hbox{}\qquad\qquad $P = \textit{True}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   183
\hbox{}\qquad\qquad $Q = \textit{False}$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   184
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   185
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   186
Nitpick can also be invoked on individual subgoals, as in the example below:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   187
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   188
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   189
\textbf{apply}~\textit{auto} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   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
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   193
\textbf{nitpick}~1 \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   194
{\slshape Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   195
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   196
\hbox{}\qquad\qquad $P = \textit{True}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   197
\hbox{}\qquad\qquad $Q = \textit{False}$} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   198
\textbf{nitpick}~2 \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   199
{\slshape Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   200
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   201
\hbox{}\qquad\qquad $P = \textit{False}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   202
\hbox{}\qquad\qquad $Q = \textit{True}$} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   203
\textbf{oops}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   204
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   205
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   206
\subsection{Type Variables}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   207
\label{type-variables}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   208
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   209
If you are left unimpressed by the previous example, don't worry. The next
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   210
one is more mind- and computer-boggling:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   211
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   212
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   213
\textbf{lemma} ``$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   214
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   215
\pagebreak[2] %% TYPESETTING
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   216
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   217
The putative lemma involves the definite description operator, {THE}, presented
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   218
in section 5.10.1 of the Isabelle tutorial \cite{isa-tutorial}. The
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   219
operator is defined by the axiom $(\textrm{THE}~x.\; x = a) = a$. The putative
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   220
lemma is merely asserting the indefinite description operator axiom with {THE}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   221
substituted for {SOME}.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   222
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   223
The free variable $x$ and the bound variable $y$ have type $'a$. For formulas
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   224
containing type variables, Nitpick enumerates the possible domains for each type
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   225
variable, up to a given cardinality (8 by default), looking for a finite
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   226
countermodel:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   227
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   228
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   229
\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   230
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   231
Trying 8 scopes: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   232
\hbox{}\qquad \textit{card}~$'a$~= 1; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   233
\hbox{}\qquad \textit{card}~$'a$~= 2; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   234
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   235
\hbox{}\qquad \textit{card}~$'a$~= 8. \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   236
Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   237
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   238
\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   239
\hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   240
Total time: 580 ms.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   241
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   242
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   243
Nitpick found a counterexample in which $'a$ has cardinality 3. (For
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   244
cardinalities 1 and 2, the formula holds.) In the counterexample, the three
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   245
values of type $'a$ are written $a_1$, $a_2$, and $a_3$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   246
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   247
The message ``Trying $n$ scopes: {\ldots}''\ is shown only if the option
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   248
\textit{verbose} is enabled. You can specify \textit{verbose} each time you
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   249
invoke \textbf{nitpick}, or you can set it globally using the command
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   250
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   251
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   252
\textbf{nitpick\_params} [\textit{verbose}]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   253
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   254
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   255
This command also displays the current default values for all of the options
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   256
supported by Nitpick. The options are listed in \S\ref{option-reference}.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   257
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   258
\subsection{Constants}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   259
\label{constants}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   260
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   261
By just looking at Nitpick's output, it might not be clear why the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   262
counterexample in \S\ref{type-variables} is genuine. Let's invoke Nitpick again,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   263
this time telling it to show the values of the constants that occur in the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   264
formula:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   265
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   266
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   267
\textbf{lemma}~``$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   268
\textbf{nitpick}~[\textit{show\_consts}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   269
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   270
Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   271
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   272
\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   273
\hbox{}\qquad\qquad $x = a_3$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   274
\hbox{}\qquad Constant: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   275
\hbox{}\qquad\qquad $\textit{The}~\textsl{fallback} = a_1$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   276
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   277
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   278
We can see more clearly now. Since the predicate $P$ isn't true for a unique
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   279
value, $\textrm{THE}~y.\;P~y$ can denote any value of type $'a$, even
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   280
$a_1$. Since $P~a_1$ is false, the entire formula is falsified.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   281
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   282
As an optimization, Nitpick's preprocessor introduced the special constant
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   283
``\textit{The} fallback'' corresponding to $\textrm{THE}~y.\;P~y$ (i.e.,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   284
$\mathit{The}~(\lambda y.\;P~y)$) when there doesn't exist a unique $y$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   285
satisfying $P~y$. We disable this optimization by passing the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   286
\textit{full\_descrs} option:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   287
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   288
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   289
\textbf{nitpick}~[\textit{full\_descrs},\, \textit{show\_consts}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   290
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   291
Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   292
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   293
\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   294
\hbox{}\qquad\qquad $x = a_3$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   295
\hbox{}\qquad Constant: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   296
\hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   297
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   298
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   299
As the result of another optimization, Nitpick directly assigned a value to the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   300
subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   301
disable this second optimization by using the command
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   302
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   303
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   304
\textbf{nitpick}~[\textit{dont\_specialize},\, \textit{full\_descrs},\,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   305
\textit{show\_consts}]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   306
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   307
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   308
we finally get \textit{The}:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   309
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   310
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   311
\slshape Constant: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   312
\hbox{}\qquad $\mathit{The} = \undef{}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   313
    (\!\begin{aligned}[t]%
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   314
    & \{\} := a_3,\> \{a_3\} := a_3,\> \{a_2\} := a_2, \\[-2pt] %% TYPESETTING
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   315
    & \{a_2, a_3\} := a_1,\> \{a_1\} := a_1,\> \{a_1, a_3\} := a_3, \\[-2pt]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   316
    & \{a_1, a_2\} := a_3,\> \{a_1, a_2, a_3\} := a_3)\end{aligned}$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   317
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   318
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   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
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   323
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   324
Our misadventures with THE suggest adding `$\exists!x{.}$' (``there exists a
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   325
unique $x$ such that'') at the front of our putative lemma's assumption:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   326
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   327
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   328
\textbf{lemma}~``$\exists {!}x.\; P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   329
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   330
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   331
The fix appears to work:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   332
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   333
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   334
\textbf{nitpick} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   335
\slshape Nitpick found no counterexample.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   336
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   337
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   338
We can further increase our confidence in the formula by exhausting all
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   339
cardinalities up to 50:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   340
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   341
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   342
\textbf{nitpick} [\textit{card} $'a$~= 1--50]\footnote{The symbol `--'
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   343
can be entered as \texttt{-} (hyphen) or
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   344
\texttt{\char`\\\char`\<midarrow\char`\>}.} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   345
\slshape Nitpick found no counterexample.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   346
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   347
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   348
Let's see if Sledgehammer \cite{sledgehammer-2009} can find a proof:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   349
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   350
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   351
\textbf{sledgehammer} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   352
{\slshape Sledgehammer: external prover ``$e$'' for subgoal 1: \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   353
$\exists{!}x.\; P~x\,\Longrightarrow\, P~(\hbox{\slshape THE}~y.\; P~y)$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   354
Try this command: \textrm{apply}~(\textit{metis~the\_equality})} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   355
\textbf{apply}~(\textit{metis~the\_equality\/}) \nopagebreak \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   356
{\slshape No subgoals!}% \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   357
%\textbf{done}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   358
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   359
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   360
This must be our lucky day.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   361
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   362
\subsection{Skolemization}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   363
\label{skolemization}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   364
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   365
Are all invertible functions onto? Let's find out:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   366
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   367
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   368
\textbf{lemma} ``$\exists g.\; \forall x.~g~(f~x) = x
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   369
 \,\Longrightarrow\, \forall y.\; \exists x.~y = f~x$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   370
\textbf{nitpick} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   371
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   372
Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   373
\hbox{}\qquad Free variable: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   374
\hbox{}\qquad\qquad $f = \undef{}(b_1 := a_1)$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   375
\hbox{}\qquad Skolem constants: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   376
\hbox{}\qquad\qquad $g = \undef{}(a_1 := b_1,\> a_2 := b_1)$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   377
\hbox{}\qquad\qquad $y = a_2$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   378
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   379
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   380
Although $f$ is the only free variable occurring in the formula, Nitpick also
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   381
displays values for the bound variables $g$ and $y$. These values are available
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   382
to Nitpick because it performs skolemization as a preprocessing step.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   383
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   384
In the previous example, skolemization only affected the outermost quantifiers.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   385
This is not always the case, as illustrated below:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   386
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   387
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   388
\textbf{lemma} ``$\exists x.\; \forall f.\; f~x = x$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   389
\textbf{nitpick} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   390
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   391
Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   392
\hbox{}\qquad Skolem constant: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   393
\hbox{}\qquad\qquad $\lambda x.\; f =
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   394
    \undef{}(\!\begin{aligned}[t]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   395
    & a_1 := \undef{}(a_1 := a_2,\> a_2 := a_1), \\[-2pt]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   396
    & a_2 := \undef{}(a_1 := a_1,\> a_2 := a_1))\end{aligned}$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   397
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   398
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   399
The variable $f$ is bound within the scope of $x$; therefore, $f$ depends on
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   400
$x$, as suggested by the notation $\lambda x.\,f$. If $x = a_1$, then $f$ is the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   401
function that maps $a_1$ to $a_2$ and vice versa; otherwise, $x = a_2$ and $f$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   402
maps both $a_1$ and $a_2$ to $a_1$. In both cases, $f~x \not= x$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   403
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   404
The source of the Skolem constants is sometimes more obscure:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   405
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   406
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   407
\textbf{lemma} ``$\mathit{refl}~r\,\Longrightarrow\, \mathit{sym}~r$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   408
\textbf{nitpick} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   409
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   410
Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   411
\hbox{}\qquad Free variable: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   412
\hbox{}\qquad\qquad $r = \{(a_1, a_1),\, (a_2, a_1),\, (a_2, a_2)\}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   413
\hbox{}\qquad Skolem constants: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   414
\hbox{}\qquad\qquad $\mathit{sym}.x = a_2$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   415
\hbox{}\qquad\qquad $\mathit{sym}.y = a_1$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   416
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   417
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   418
What happened here is that Nitpick expanded the \textit{sym} constant to its
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   419
definition:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   420
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   421
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   422
$\mathit{sym}~r \,\equiv\,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   423
 \forall x\> y.\,\> (x, y) \in r \longrightarrow (y, x) \in r.$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   424
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   425
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   426
As their names suggest, the Skolem constants $\mathit{sym}.x$ and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   427
$\mathit{sym}.y$ are simply the bound variables $x$ and $y$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   428
from \textit{sym}'s definition.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   429
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   430
Although skolemization is a useful optimization, you can disable it by invoking
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   431
Nitpick with \textit{dont\_skolemize}. See \S\ref{optimizations} for details.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   432
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   433
\subsection{Natural Numbers and Integers}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   434
\label{natural-numbers-and-integers}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   435
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   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 three-valued logic.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   441
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   442
Here is an example involving \textit{int}:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   443
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   444
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   445
\textbf{lemma} ``$\lbrakk i \le j;\> n \le (m{\Colon}\mathit{int})\rbrakk \,\Longrightarrow\, i * n + j * m \le i * m + j * n$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   446
\textbf{nitpick} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   447
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   448
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   449
\hbox{}\qquad\qquad $i = 0$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   450
\hbox{}\qquad\qquad $j = 1$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   451
\hbox{}\qquad\qquad $m = 1$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   452
\hbox{}\qquad\qquad $n = 0$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   453
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   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
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   467
With infinite types, we don't always have the luxury of a genuine counterexample
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   468
and must often content ourselves with a potential one. The tedious task of
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   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
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   471
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   472
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   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]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   475
\slshape Nitpick found a potential counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   476
\hbox{}\qquad Free variable: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   477
\hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   478
Confirmation by ``\textit{auto}'': The above counterexample is genuine.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   479
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   480
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   481
You might wonder why the counterexample is first reported as potential. The root
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   482
of the problem is that the bound variable in $\forall n.\; \textit{Suc}~n
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   483
\mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds an $n$ such
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   484
that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   485
\textit{False}; but otherwise, it does not know anything about values of $n \ge
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   486
\textit{card~nat}$ and must therefore evaluate the assumption to $\unk$, not
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   487
\textit{True}. Since the assumption can never be satisfied, the putative lemma
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   488
can never be falsified.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   489
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   490
Incidentally, if you distrust the so-called genuine counterexamples, you can
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   491
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
   492
aware that \textit{auto} will usually fail to prove that the counterexample is
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   493
genuine or spurious.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   494
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   495
Some conjectures involving elementary number theory make Nitpick look like a
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   496
giant with feet of clay:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   497
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   498
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   499
\textbf{lemma} ``$P~\textit{Suc}$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   500
\textbf{nitpick} [\textit{card} = 1--6] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   501
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   502
Nitpick found no counterexample.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   503
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   504
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34038
diff changeset
   505
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
   506
\{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
   507
\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
   508
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
   509
example is similar:
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   510
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   511
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   512
\textbf{lemma} ``$P~(\textit{op}~{+}\Colon
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   513
\textit{nat}\mathbin{\Rightarrow}\textit{nat}\mathbin{\Rightarrow}\textit{nat})$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   514
\textbf{nitpick} [\textit{card nat} = 1] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   515
{\slshape Nitpick found a counterexample:} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   516
\hbox{}\qquad Free variable: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   517
\hbox{}\qquad\qquad $P = \{\}$ \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   518
\textbf{nitpick} [\textit{card nat} = 2] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   519
{\slshape Nitpick found no counterexample.}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   520
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   521
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   522
The problem here is that \textit{op}~+ is total when \textit{nat} is taken to be
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   523
$\{0\}$ but becomes partial as soon as we add $1$, because $1 + 1 \notin \{0,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   524
1\}$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   525
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   526
Because numbers are infinite and are approximated using a three-valued logic,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   527
there is usually no need to systematically enumerate domain sizes. If Nitpick
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   528
cannot find a genuine counterexample for \textit{card~nat}~= $k$, it is very
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   529
unlikely that one could be found for smaller domains. (The $P~(\textit{op}~{+})$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   530
example above is an exception to this principle.) Nitpick nonetheless enumerates
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   531
all cardinalities from 1 to 8 for \textit{nat}, mainly because smaller
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   532
cardinalities are fast to handle and give rise to simpler counterexamples. This
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   533
is explained in more detail in \S\ref{scope-monotonicity}.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   534
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   535
\subsection{Inductive Datatypes}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   536
\label{inductive-datatypes}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   537
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   538
Like natural numbers and integers, inductive datatypes with recursive
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   539
constructors admit no finite models and must be approximated by a subterm-closed
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   540
subset. For example, using a cardinality of 10 for ${'}a~\textit{list}$,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   541
Nitpick looks for all counterexamples that can be built using at most 10
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   542
different lists.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   543
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   544
Let's see with an example involving \textit{hd} (which returns the first element
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   545
of a list) and $@$ (which concatenates two lists):
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   546
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   547
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   548
\textbf{lemma} ``$\textit{hd}~(\textit{xs} \mathbin{@} [y, y]) = \textit{hd}~\textit{xs}$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   549
\textbf{nitpick} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   550
\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   551
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   552
\hbox{}\qquad\qquad $\textit{xs} = []$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   553
\hbox{}\qquad\qquad $\textit{y} = a_3$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   554
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   555
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   556
To see why the counterexample is genuine, we enable \textit{show\_consts}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   557
and \textit{show\_\allowbreak datatypes}:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   558
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   559
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   560
{\slshape Datatype:} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   561
\hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_3, a_3],\, [a_3],\, \unr\}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   562
{\slshape Constants:} \\
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
   563
\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_3, a_3])$ \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   564
\hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_3, a_3] := a_3,\> [a_3] := a_3)$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   565
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   566
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   567
Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   568
including $a_2$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   569
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   570
The second constant, $\lambda x_1.\; x_1 \mathbin{@} [y, y]$, is simply the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   571
append operator whose second argument is fixed to be $[y, y]$. Appending $[a_3,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   572
a_3]$ to $[a_3]$ would normally give $[a_3, a_3, a_3]$, but this value is not
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   573
representable in the subset of $'a$~\textit{list} considered by Nitpick, which
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   574
is shown under the ``Datatype'' heading; hence the result is $\unk$. Similarly,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   575
appending $[a_3, a_3]$ to itself gives $\unk$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   576
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   577
Given \textit{card}~$'a = 3$ and \textit{card}~$'a~\textit{list} = 3$, Nitpick
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   578
considers the following subsets:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   579
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   580
\kern-.5\smallskipamount %% TYPESETTING
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   581
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   582
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   583
\begin{multicols}{3}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   584
$\{[],\, [a_1],\, [a_2]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   585
$\{[],\, [a_1],\, [a_3]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   586
$\{[],\, [a_2],\, [a_3]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   587
$\{[],\, [a_1],\, [a_1, a_1]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   588
$\{[],\, [a_1],\, [a_2, a_1]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   589
$\{[],\, [a_1],\, [a_3, a_1]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   590
$\{[],\, [a_2],\, [a_1, a_2]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   591
$\{[],\, [a_2],\, [a_2, a_2]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   592
$\{[],\, [a_2],\, [a_3, a_2]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   593
$\{[],\, [a_3],\, [a_1, a_3]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   594
$\{[],\, [a_3],\, [a_2, a_3]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   595
$\{[],\, [a_3],\, [a_3, a_3]\}$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   596
\end{multicols}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   597
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   598
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   599
\kern-2\smallskipamount %% TYPESETTING
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   600
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   601
All subterm-closed subsets of $'a~\textit{list}$ consisting of three values
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   602
are listed and only those. As an example of a non-subterm-closed subset,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   603
consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_3]\}$, and observe
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   604
that $[a_1, a_3]$ (i.e., $a_1 \mathbin{\#} [a_3]$) has $[a_3] \notin
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   605
\mathcal{S}$ as a subterm.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   606
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   607
Here's another m\"ochtegern-lemma that Nitpick can refute without a blink:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   608
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   609
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   610
\textbf{lemma} ``$\lbrakk \textit{length}~\textit{xs} = 1;\> \textit{length}~\textit{ys} = 1
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   611
\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$''
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   612
\\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   613
\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   614
\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   615
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   616
\hbox{}\qquad\qquad $\textit{xs} = [a_2]$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   617
\hbox{}\qquad\qquad $\textit{ys} = [a_3]$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   618
\hbox{}\qquad Datatypes: \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   619
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   620
\hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_3],\, [a_2],\, \unr\}$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   621
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   622
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   623
Because datatypes are approximated using a three-valued logic, there is usually
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   624
no need to systematically enumerate cardinalities: If Nitpick cannot find a
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   625
genuine counterexample for \textit{card}~$'a~\textit{list}$~= 10, it is very
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   626
unlikely that one could be found for smaller cardinalities.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   627
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   628
\subsection{Typedefs, Records, Rationals, and Reals}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   629
\label{typedefs-records-rationals-and-reals}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   630
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   631
Nitpick generally treats types declared using \textbf{typedef} as datatypes
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   632
whose single constructor is the corresponding \textit{Abs\_\kern.1ex} function.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   633
For example:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   634
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   635
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   636
\textbf{typedef}~\textit{three} = ``$\{0\Colon\textit{nat},\, 1,\, 2\}$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   637
\textbf{by}~\textit{blast} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   638
\textbf{definition}~$A \mathbin{\Colon} \textit{three}$ \textbf{where} ``\kern-.1em$A \,\equiv\, \textit{Abs\_\allowbreak three}~0$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   639
\textbf{definition}~$B \mathbin{\Colon} \textit{three}$ \textbf{where} ``$B \,\equiv\, \textit{Abs\_three}~1$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   640
\textbf{definition}~$C \mathbin{\Colon} \textit{three}$ \textbf{where} ``$C \,\equiv\, \textit{Abs\_three}~2$'' \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   641
\textbf{lemma} ``$\lbrakk P~A;\> P~B\rbrakk \,\Longrightarrow\, P~x$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   642
\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   643
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   644
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   645
\hbox{}\qquad\qquad $P = \{\Abs{1},\, \Abs{0}\}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   646
\hbox{}\qquad\qquad $x = \Abs{2}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   647
\hbox{}\qquad Datatypes: \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   648
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   649
\hbox{}\qquad\qquad $\textit{three} = \{\Abs{2},\, \Abs{1},\, \Abs{0},\, \unr\}$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   650
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   651
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   652
%% MARK
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   653
In the output above, $\Abs{n}$ abbreviates $\textit{Abs\_three}~n$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   654
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   655
%% MARK
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   656
Records, which are implemented as \textbf{typedef}s behind the scenes, are
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   657
handled in much the same way:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   658
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   659
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   660
\textbf{record} \textit{point} = \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   661
\hbox{}\quad $\textit{Xcoord} \mathbin{\Colon} \textit{int}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   662
\hbox{}\quad $\textit{Ycoord} \mathbin{\Colon} \textit{int}$ \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   663
\textbf{lemma} ``$\textit{Xcoord}~(p\Colon\textit{point}) = \textit{Xcoord}~(q\Colon\textit{point})$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   664
\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   665
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   666
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   667
\hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   668
\hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   669
\hbox{}\qquad Datatypes: \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   670
\hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, \unr\}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   671
\hbox{}\qquad\qquad $\textit{point} = \{\lparr\textit{Xcoord} = 1,\>
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   672
\textit{Ycoord} = 1\rparr,\> \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr,\, \unr\}$\kern-1pt %% QUIET
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   673
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   674
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   675
Finally, Nitpick provides rudimentary support for rationals and reals using a
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   676
similar approach:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   677
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   678
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   679
\textbf{lemma} ``$4 * x + 3 * (y\Colon\textit{real}) \not= 1/2$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   680
\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   681
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   682
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   683
\hbox{}\qquad\qquad $x = 1/2$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   684
\hbox{}\qquad\qquad $y = -1/2$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   685
\hbox{}\qquad Datatypes: \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   686
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, 3,\, 4,\, 5,\, 6,\, 7,\, \unr\}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   687
\hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, 2,\, 3,\, 4,\, -3,\, -2,\, -1,\, \unr\}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   688
\hbox{}\qquad\qquad $\textit{real} = \{1,\, 0,\, 4,\, -3/2,\, 3,\, 2,\, 1/2,\, -1/2,\, \unr\}$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   689
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   690
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   691
\subsection{Inductive and Coinductive Predicates}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   692
\label{inductive-and-coinductive-predicates}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   693
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   694
Inductively defined predicates (and sets) are particularly problematic for
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   695
counterexample generators. They can make Quickcheck~\cite{berghofer-nipkow-2004}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   696
loop forever and Refute~\cite{weber-2008} run out of resources. The crux of
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   697
the problem is that they are defined using a least fixed point construction.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   698
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   699
Nitpick's philosophy is that not all inductive predicates are equal. Consider
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   700
the \textit{even} predicate below:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   701
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   702
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   703
\textbf{inductive}~\textit{even}~\textbf{where} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   704
``\textit{even}~0'' $\,\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   705
``\textit{even}~$n\,\Longrightarrow\, \textit{even}~(\textit{Suc}~(\textit{Suc}~n))$''
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   706
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   707
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   708
This predicate enjoys the desirable property of being well-founded, which means
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   709
that the introduction rules don't give rise to infinite chains of the form
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   710
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   711
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   712
$\cdots\,\Longrightarrow\, \textit{even}~k''
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   713
       \,\Longrightarrow\, \textit{even}~k'
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   714
       \,\Longrightarrow\, \textit{even}~k.$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   715
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   716
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   717
For \textit{even}, this is obvious: Any chain ending at $k$ will be of length
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   718
$k/2 + 1$:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   719
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   720
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   721
$\textit{even}~0\,\Longrightarrow\, \textit{even}~2\,\Longrightarrow\, \cdots
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   722
       \,\Longrightarrow\, \textit{even}~(k - 2)
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   723
       \,\Longrightarrow\, \textit{even}~k.$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   724
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   725
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   726
Wellfoundedness is desirable because it enables Nitpick to use a very efficient
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   727
fixed point computation.%
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   728
\footnote{If an inductive predicate is
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   729
well-founded, then it has exactly one fixed point, which is simultaneously the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   730
least and the greatest fixed point. In these circumstances, the computation of
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   731
the least fixed point amounts to the computation of an arbitrary fixed point,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   732
which can be performed using a straightforward recursive equation.}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   733
Moreover, Nitpick can prove wellfoundedness of most well-founded predicates,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   734
just as Isabelle's \textbf{function} package usually discharges termination
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   735
proof obligations automatically.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   736
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   737
Let's try an example:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   738
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   739
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   740
\textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   741
\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   742
\slshape The inductive predicate ``\textit{even}'' was proved well-founded.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   743
Nitpick can compute it efficiently. \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   744
Trying 1 scope: \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   745
\hbox{}\qquad \textit{card nat}~= 100. \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   746
Nitpick found a potential counterexample for \textit{card nat}~= 100: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   747
\hbox{}\qquad Empty assignment \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   748
Nitpick could not find a better counterexample. \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   749
Total time: 2274 ms.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   750
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   751
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   752
No genuine counterexample is possible because Nitpick cannot rule out the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   753
existence of a natural number $n \ge 100$ such that both $\textit{even}~n$ and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   754
$\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   755
existential quantifier:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   756
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   757
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   758
\textbf{lemma} ``$\exists n \mathbin{\le} 99.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   759
\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}] \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   760
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   761
\hbox{}\qquad Empty assignment
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   762
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   763
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   764
So far we were blessed by the wellfoundedness of \textit{even}. What happens if
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   765
we use the following definition instead?
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   766
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   767
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   768
\textbf{inductive} $\textit{even}'$ \textbf{where} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   769
``$\textit{even}'~(0{\Colon}\textit{nat})$'' $\,\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   770
``$\textit{even}'~2$'' $\,\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   771
``$\lbrakk\textit{even}'~m;\> \textit{even}'~n\rbrakk \,\Longrightarrow\, \textit{even}'~(m + n)$''
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   772
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   773
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   774
This definition is not well-founded: From $\textit{even}'~0$ and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   775
$\textit{even}'~0$, we can derive that $\textit{even}'~0$. Nonetheless, the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   776
predicates $\textit{even}$ and $\textit{even}'$ are equivalent.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   777
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   778
Let's check a property involving $\textit{even}'$. To make up for the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   779
foreseeable computational hurdles entailed by non-wellfoundedness, we decrease
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   780
\textit{nat}'s cardinality to a mere 10:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   781
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   782
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   783
\textbf{lemma}~``$\exists n \in \{0, 2, 4, 6, 8\}.\;
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   784
\lnot\;\textit{even}'~n$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   785
\textbf{nitpick}~[\textit{card nat}~= 10,\, \textit{verbose},\, \textit{show\_consts}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   786
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   787
The inductive predicate ``$\textit{even}'\!$'' could not be proved well-founded.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   788
Nitpick might need to unroll it. \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   789
Trying 6 scopes: \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   790
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 0; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   791
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 1; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   792
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   793
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 4; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   794
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 8; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   795
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 9. \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   796
Nitpick found a counterexample for \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   797
\hbox{}\qquad Constant: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   798
\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   799
& 2 := \{0, 2, 4, 6, 8, 1^\Q, 3^\Q, 5^\Q, 7^\Q, 9^\Q\}, \\[-2pt]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   800
& 1 := \{0, 2, 4, 1^\Q, 3^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\}, \\[-2pt]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   801
& 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   802
Total time: 1140 ms.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   803
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   804
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   805
Nitpick's output is very instructive. First, it tells us that the predicate is
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   806
unrolled, meaning that it is computed iteratively from the empty set. Then it
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   807
lists six scopes specifying different bounds on the numbers of iterations:\ 0,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   808
1, 2, 4, 8, and~9.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   809
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   810
The output also shows how each iteration contributes to $\textit{even}'$. The
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   811
notation $\lambda i.\; \textit{even}'$ indicates that the value of the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   812
predicate depends on an iteration counter. Iteration 0 provides the basis
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   813
elements, $0$ and $2$. Iteration 1 contributes $4$ ($= 2 + 2$). Iteration 2
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   814
throws $6$ ($= 2 + 4 = 4 + 2$) and $8$ ($= 4 + 4$) into the mix. Further
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   815
iterations would not contribute any new elements.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   816
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   817
Some values are marked with superscripted question
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   818
marks~(`\lower.2ex\hbox{$^\Q$}'). These are the elements for which the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   819
predicate evaluates to $\unk$. Thus, $\textit{even}'$ evaluates to either
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   820
\textit{True} or $\unk$, never \textit{False}.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   821
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   822
When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, and 24
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   823
iterations. However, these numbers are bounded by the cardinality of the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   824
predicate's domain. With \textit{card~nat}~= 10, no more than 9 iterations are
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   825
ever needed to compute the value of a \textit{nat} predicate. You can specify
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   826
the number of iterations using the \textit{iter} option, as explained in
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   827
\S\ref{scope-of-search}.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   828
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   829
In the next formula, $\textit{even}'$ occurs both positively and negatively:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   830
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   831
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   832
\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
   833
\textbf{nitpick} [\textit{card nat} = 10, \textit{show\_consts}] \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   834
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   835
\hbox{}\qquad Free variable: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   836
\hbox{}\qquad\qquad $n = 1$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   837
\hbox{}\qquad Constants: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   838
\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   839
& 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$  \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   840
\hbox{}\qquad\qquad $\textit{even}' \subseteq \{0, 2, 4, 6, 8, \unr\}$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   841
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   842
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   843
Notice the special constraint $\textit{even}' \subseteq \{0,\, 2,\, 4,\, 6,\,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   844
8,\, \unr\}$ in the output, whose right-hand side represents an arbitrary
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   845
fixed point (not necessarily the least one). It is used to falsify
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   846
$\textit{even}'~n$. In contrast, the unrolled predicate is used to satisfy
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   847
$\textit{even}'~(n - 2)$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   848
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   849
Coinductive predicates are handled dually. For example:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   850
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   851
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   852
\textbf{coinductive} \textit{nats} \textbf{where} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   853
``$\textit{nats}~(x\Colon\textit{nat}) \,\Longrightarrow\, \textit{nats}~x$'' \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   854
\textbf{lemma} ``$\textit{nats} = \{0, 1, 2, 3, 4\}$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   855
\textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   856
\slshape Nitpick found a counterexample:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   857
\\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   858
\hbox{}\qquad Constants: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   859
\hbox{}\qquad\qquad $\lambda i.\; \textit{nats} = \undef(0 := \{\!\begin{aligned}[t]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   860
& 0^\Q, 1^\Q, 2^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q, \\[-2pt]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   861
& \unr\})\end{aligned}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   862
\hbox{}\qquad\qquad $nats \supseteq \{9, 5^\Q, 6^\Q, 7^\Q, 8^\Q, \unr\}$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   863
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   864
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   865
As a special case, Nitpick uses Kodkod's transitive closure operator to encode
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   866
negative occurrences of non-well-founded ``linear inductive predicates,'' i.e.,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   867
inductive predicates for which each the predicate occurs in at most one
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   868
assumption of each introduction rule. For example:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   869
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   870
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   871
\textbf{inductive} \textit{odd} \textbf{where} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   872
``$\textit{odd}~1$'' $\,\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   873
``$\lbrakk \textit{odd}~m;\>\, \textit{even}~n\rbrakk \,\Longrightarrow\, \textit{odd}~(m + n)$'' \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   874
\textbf{lemma}~``$\textit{odd}~n \,\Longrightarrow\, \textit{odd}~(n - 2)$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   875
\textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   876
\slshape Nitpick found a counterexample:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   877
\\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   878
\hbox{}\qquad Free variable: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   879
\hbox{}\qquad\qquad $n = 1$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   880
\hbox{}\qquad Constants: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   881
\hbox{}\qquad\qquad $\textit{even} = \{0, 2, 4, 6, 8, \unr\}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   882
\hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = \{1, \unr\}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   883
\hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \!
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   884
\!\begin{aligned}[t]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   885
  & \{(0, 0), (0, 2), (0, 4), (0, 6), (0, 8), (1, 1), (1, 3), (1, 5), \\[-2pt]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   886
  & \phantom{\{} (1, 7), (1, 9), (2, 2), (2, 4), (2, 6), (2, 8), (3, 3),
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   887
       (3, 5), \\[-2pt]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   888
  & \phantom{\{} (3, 7), (3, 9), (4, 4), (4, 6), (4, 8), (5, 5), (5, 7), (5, 9), \\[-2pt]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   889
  & \phantom{\{} (6, 6), (6, 8), (7, 7), (7, 9), (8, 8), (9, 9), \unr\}\end{aligned}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   890
\hbox{}\qquad\qquad $\textit{odd} \subseteq \{1, 3, 5, 7, 9, 8^\Q, \unr\}$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   891
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   892
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   893
\noindent
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   894
In the output, $\textit{odd}_{\textrm{base}}$ represents the base elements and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   895
$\textit{odd}_{\textrm{step}}$ is a transition relation that computes new
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   896
elements from known ones. The set $\textit{odd}$ consists of all the values
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   897
reachable through the reflexive transitive closure of
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   898
$\textit{odd}_{\textrm{step}}$ starting with any element from
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   899
$\textit{odd}_{\textrm{base}}$, namely 1, 3, 5, 7, and 9. Using Kodkod's
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   900
transitive closure to encode linear predicates is normally either more thorough
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   901
or more efficient than unrolling (depending on the value of \textit{iter}), but
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   902
for those cases where it isn't you can disable it by passing the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   903
\textit{dont\_star\_linear\_preds} option.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   904
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   905
\subsection{Coinductive Datatypes}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   906
\label{coinductive-datatypes}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   907
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   908
While Isabelle regrettably lacks a high-level mechanism for defining coinductive
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   909
datatypes, the \textit{Coinductive\_List} theory provides a coinductive ``lazy
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   910
list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick supports
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   911
these lazy lists seamlessly and provides a hook, described in
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   912
\S\ref{registration-of-coinductive-datatypes}, to register custom coinductive
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   913
datatypes.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   914
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   915
(Co)intuitively, a coinductive datatype is similar to an inductive datatype but
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   916
allows infinite objects. Thus, the infinite lists $\textit{ps}$ $=$ $[a, a, a,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   917
\ldots]$, $\textit{qs}$ $=$ $[a, b, a, b, \ldots]$, and $\textit{rs}$ $=$ $[0,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   918
1, 2, 3, \ldots]$ can be defined as lazy lists using the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   919
$\textit{LNil}\mathbin{\Colon}{'}a~\textit{llist}$ and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   920
$\textit{LCons}\mathbin{\Colon}{'}a \mathbin{\Rightarrow} {'}a~\textit{llist}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   921
\mathbin{\Rightarrow} {'}a~\textit{llist}$ constructors.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   922
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   923
Although it is otherwise no friend of infinity, Nitpick can find counterexamples
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   924
involving cyclic lists such as \textit{ps} and \textit{qs} above as well as
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   925
finite lists:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   926
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   927
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   928
\textbf{lemma} ``$\textit{xs} \not= \textit{LCons}~a~\textit{xs}$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   929
\textbf{nitpick} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   930
\slshape Nitpick found a counterexample for {\itshape card}~$'a$ = 1: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   931
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   932
\hbox{}\qquad\qquad $\textit{a} = a_1$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   933
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   934
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   935
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   936
The notation $\textrm{THE}~\omega.\; \omega = t(\omega)$ stands
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   937
for the infinite term $t(t(t(\ldots)))$. Hence, \textit{xs} is simply the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   938
infinite list $[a_1, a_1, a_1, \ldots]$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   939
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   940
The next example is more interesting:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   941
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   942
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   943
\textbf{lemma}~``$\lbrakk\textit{xs} = \textit{LCons}~a~\textit{xs};\>\,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   944
\textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   945
\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   946
\slshape The type ``\kern1pt$'a$'' passed the monotonicity test. Nitpick might be able to skip
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   947
some scopes. \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   948
Trying 8 scopes: \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   949
\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list}$''~= 1,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   950
and \textit{bisim\_depth}~= 0. \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   951
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   952
\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} ``\kern1pt$'a~\textit{list}$''~= 8,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   953
and \textit{bisim\_depth}~= 7. \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   954
Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   955
\textit{card}~``\kern1pt$'a~\textit{list}$''~= 2, and \textit{bisim\_\allowbreak
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   956
depth}~= 1:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   957
\\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   958
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   959
\hbox{}\qquad\qquad $\textit{a} = a_2$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   960
\hbox{}\qquad\qquad $\textit{b} = a_1$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   961
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   962
\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_1~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega)$ \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   963
Total time: 726 ms.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   964
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   965
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   966
The lazy list $\textit{xs}$ is simply $[a_2, a_2, a_2, \ldots]$, whereas
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   967
$\textit{ys}$ is $[a_1, a_2, a_2, a_2, \ldots]$, i.e., a lasso-shaped list with
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   968
$[a_1]$ as its stem and $[a_2]$ as its cycle. In general, the list segment
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   969
within the scope of the {THE} binder corresponds to the lasso's cycle, whereas
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   970
the segment leading to the binder is the stem.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   971
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   972
A salient property of coinductive datatypes is that two objects are considered
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   973
equal if and only if they lead to the same observations. For example, the lazy
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   974
lists $\textrm{THE}~\omega.\; \omega =
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   975
\textit{LCons}~a~(\textit{LCons}~b~\omega)$ and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   976
$\textit{LCons}~a~(\textrm{THE}~\omega.\; \omega =
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   977
\textit{LCons}~b~(\textit{LCons}~a~\omega))$ are identical, because both lead
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   978
to the sequence of observations $a$, $b$, $a$, $b$, \hbox{\ldots} (or,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   979
equivalently, both encode the infinite list $[a, b, a, b, \ldots]$). This
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   980
concept of equality for coinductive datatypes is called bisimulation and is
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   981
defined coinductively.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   982
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   983
Internally, Nitpick encodes the coinductive bisimilarity predicate as part of
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   984
the Kodkod problem to ensure that distinct objects lead to different
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   985
observations. This precaution is somewhat expensive and often unnecessary, so it
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   986
can be disabled by setting the \textit{bisim\_depth} option to $-1$. The
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   987
bisimilarity check is then performed \textsl{after} the counterexample has been
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   988
found to ensure correctness. If this after-the-fact check fails, the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   989
counterexample is tagged as ``likely genuine'' and Nitpick recommends to try
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   990
again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   991
check for the previous example saves approximately 150~milli\-seconds; the speed
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   992
gains can be more significant for larger scopes.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   993
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   994
The next formula illustrates the need for bisimilarity (either as a Kodkod
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   995
predicate or as an after-the-fact check) to prevent spurious counterexamples:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   996
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   997
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   998
\textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   999
\,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34038
diff changeset
  1000
\textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1001
\slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1002
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1003
\hbox{}\qquad\qquad $a = a_2$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1004
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1005
\textit{LCons}~a_2~\omega$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1006
\hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1007
\hbox{}\qquad Codatatype:\strut \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1008
\hbox{}\qquad\qquad $'a~\textit{llist} =
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1009
\{\!\begin{aligned}[t]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1010
  & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega, \\[-2pt]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1011
  & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega,\> \unr\}\end{aligned}$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1012
\\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1013
Try again with ``\textit{bisim\_depth}'' set to a nonnegative value to confirm
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1014
that the counterexample is genuine. \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1015
{\upshape\textbf{nitpick}} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1016
\slshape Nitpick found no counterexample.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1017
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1018
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1019
In the first \textbf{nitpick} invocation, the after-the-fact check discovered 
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1020
that the two known elements of type $'a~\textit{llist}$ are bisimilar.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1021
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1022
A compromise between leaving out the bisimilarity predicate from the Kodkod
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1023
problem and performing the after-the-fact check is to specify a lower
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1024
nonnegative \textit{bisim\_depth} value than the default one provided by
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1025
Nitpick. In general, a value of $K$ means that Nitpick will require all lists to
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1026
be distinguished from each other by their prefixes of length $K$. Be aware that
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1027
setting $K$ to a too low value can overconstrain Nitpick, preventing it from
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1028
finding any counterexamples.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1029
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1030
\subsection{Boxing}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1031
\label{boxing}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1032
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1033
Nitpick normally maps function and product types directly to the corresponding
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1034
Kodkod concepts. As a consequence, if $'a$ has cardinality 3 and $'b$ has
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1035
cardinality 4, then $'a \times {'}b$ has cardinality 12 ($= 4 \times 3$) and $'a
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1036
\Rightarrow {'}b$ has cardinality 64 ($= 4^3$). In some circumstances, it pays
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1037
off to treat these types in the same way as plain datatypes, by approximating
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1038
them by a subset of a given cardinality. This technique is called ``boxing'' and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1039
is particularly useful for functions passed as arguments to other functions, for
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1040
high-arity functions, and for large tuples. Under the hood, boxing involves
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1041
wrapping occurrences of the types $'a \times {'}b$ and $'a \Rightarrow {'}b$ in
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1042
isomorphic datatypes, as can be seen by enabling the \textit{debug} option.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1043
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1044
To illustrate boxing, we consider a formalization of $\lambda$-terms represented
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1045
using de Bruijn's notation:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1046
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1047
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1048
\textbf{datatype} \textit{tm} = \textit{Var}~\textit{nat}~$\mid$~\textit{Lam}~\textit{tm} $\mid$ \textit{App~tm~tm}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1049
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1050
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1051
The $\textit{lift}~t~k$ function increments all variables with indices greater
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1052
than or equal to $k$ by one:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1053
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1054
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1055
\textbf{primrec} \textit{lift} \textbf{where} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1056
``$\textit{lift}~(\textit{Var}~j)~k = \textit{Var}~(\textrm{if}~j < k~\textrm{then}~j~\textrm{else}~j + 1)$'' $\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1057
``$\textit{lift}~(\textit{Lam}~t)~k = \textit{Lam}~(\textit{lift}~t~(k + 1))$'' $\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1058
``$\textit{lift}~(\textit{App}~t~u)~k = \textit{App}~(\textit{lift}~t~k)~(\textit{lift}~u~k)$''
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1059
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1060
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1061
The $\textit{loose}~t~k$ predicate returns \textit{True} if and only if
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1062
term $t$ has a loose variable with index $k$ or more:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1063
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1064
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1065
\textbf{primrec}~\textit{loose} \textbf{where} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1066
``$\textit{loose}~(\textit{Var}~j)~k = (j \ge k)$'' $\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1067
``$\textit{loose}~(\textit{Lam}~t)~k = \textit{loose}~t~(\textit{Suc}~k)$'' $\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1068
``$\textit{loose}~(\textit{App}~t~u)~k = (\textit{loose}~t~k \mathrel{\lor} \textit{loose}~u~k)$''
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1069
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1070
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1071
Next, the $\textit{subst}~\sigma~t$ function applies the substitution $\sigma$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1072
on $t$:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1073
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1074
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1075
\textbf{primrec}~\textit{subst} \textbf{where} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1076
``$\textit{subst}~\sigma~(\textit{Var}~j) = \sigma~j$'' $\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1077
``$\textit{subst}~\sigma~(\textit{Lam}~t) = {}$\phantom{''} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1078
\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$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1079
``$\textit{subst}~\sigma~(\textit{App}~t~u) = \textit{App}~(\textit{subst}~\sigma~t)~(\textit{subst}~\sigma~u)$''
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1080
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1081
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1082
A substitution is a function that maps variable indices to terms. Observe that
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1083
$\sigma$ is a function passed as argument and that Nitpick can't optimize it
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1084
away, because the recursive call for the \textit{Lam} case involves an altered
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1085
version. Also notice the \textit{lift} call, which increments the variable
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1086
indices when moving under a \textit{Lam}.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1087
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1088
A reasonable property to expect of substitution is that it should leave closed
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1089
terms unchanged. Alas, even this simple property does not hold:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1090
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1091
\pre
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1092
\textbf{lemma}~``$\lnot\,\textit{loose}~t~0 \,\Longrightarrow\, \textit{subst}~\sigma~t = t$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1093
\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1094
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1095
Trying 8 scopes: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1096
\hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 1; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1097
\hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 2; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1098
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1099
\hbox{}\qquad \textit{card~nat}~= 8, \textit{card tm}~= 8, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 8. \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1100
Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1101
and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm}$''~= 6: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1102
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1103
\hbox{}\qquad\qquad $\sigma = \undef(\!\begin{aligned}[t]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1104
& 0 := \textit{Var}~0,\>
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1105
  1 := \textit{Var}~0,\>
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1106
  2 := \textit{Var}~0, \\[-2pt]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1107
& 3 := \textit{Var}~0,\>
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1108
  4 := \textit{Var}~0,\>
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1109
  5 := \textit{Var}~0)\end{aligned}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1110
\hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1111
Total time: $4679$ ms.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1112
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1113
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1114
Using \textit{eval}, we find out that $\textit{subst}~\sigma~t =
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1115
\textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1116
$\lambda$-term notation, $t$~is
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1117
$\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is $\lambda x\, y.\> y$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1118
The bug is in \textit{subst}: The $\textit{lift}~(\sigma~m)~1$ call should be
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1119
replaced with $\textit{lift}~(\sigma~m)~0$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1120
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1121
An interesting aspect of Nitpick's verbose output is that it assigned inceasing
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1122
cardinalities from 1 to 8 to the type $\textit{nat} \Rightarrow \textit{tm}$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1123
For the formula of interest, knowing 6 values of that type was enough to find
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1124
the counterexample. Without boxing, $46\,656$ ($= 6^6$) values must be
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1125
considered, a hopeless undertaking:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1126
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1127
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1128
\textbf{nitpick} [\textit{dont\_box}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1129
{\slshape Nitpick ran out of time after checking 4 of 8 scopes.}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1130
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1131
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1132
{\looseness=-1
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1133
Boxing can be enabled or disabled globally or on a per-type basis using the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1134
\textit{box} option. Moreover, setting the cardinality of a function or
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1135
product type implicitly enables boxing for that type. Nitpick usually performs
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1136
reasonable choices about which types should be boxed, but option tweaking
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1137
sometimes helps.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1138
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1139
}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1140
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1141
\subsection{Scope Monotonicity}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1142
\label{scope-monotonicity}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1143
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1144
The \textit{card} option (together with \textit{iter}, \textit{bisim\_depth},
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1145
and \textit{max}) controls which scopes are actually tested. In general, to
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1146
exhaust all models below a certain cardinality bound, the number of scopes that
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1147
Nitpick must consider increases exponentially with the number of type variables
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1148
(and \textbf{typedecl}'d types) occurring in the formula. Given the default
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1149
cardinality specification of 1--8, no fewer than $8^4 = 4096$ scopes must be
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1150
considered for a formula involving $'a$, $'b$, $'c$, and $'d$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1151
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1152
Fortunately, many formulas exhibit a property called \textsl{scope
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1153
monotonicity}, meaning that if the formula is falsifiable for a given scope,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1154
it is also falsifiable for all larger scopes \cite[p.~165]{jackson-2006}.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1155
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1156
Consider the formula
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1157
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1158
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1159
\textbf{lemma}~``$\textit{length~xs} = \textit{length~ys} \,\Longrightarrow\, \textit{rev}~(\textit{zip~xs~ys}) = \textit{zip~xs}~(\textit{rev~ys})$''
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1160
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1161
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1162
where \textit{xs} is of type $'a~\textit{list}$ and \textit{ys} is of type
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1163
$'b~\textit{list}$. A priori, Nitpick would need to consider 512 scopes to
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1164
exhaust the specification \textit{card}~= 1--8. However, our intuition tells us
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1165
that any counterexample found with a small scope would still be a counterexample
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1166
in a larger scope---by simply ignoring the fresh $'a$ and $'b$ values provided
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1167
by the larger scope. Nitpick comes to the same conclusion after a careful
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1168
inspection of the formula and the relevant definitions:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1169
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1170
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1171
\textbf{nitpick}~[\textit{verbose}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1172
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1173
The types ``\kern1pt$'a$'' and ``\kern1pt$'b$'' passed the monotonicity test.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1174
Nitpick might be able to skip some scopes.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1175
 \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1176
Trying 8 scopes: \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1177
\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1178
\textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1179
\textit{list}''~= 1, \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1180
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 1, and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1181
\textit{card} ``\kern1pt$'b$ \textit{list}''~= 1. \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1182
\hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1183
\textit{card} \textit{nat}~= 2, \textit{card} ``$('a \times {'}b)$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1184
\textit{list}''~= 2, \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1185
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 2, and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1186
\textit{card} ``\kern1pt$'b$ \textit{list}''~= 2. \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1187
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1188
\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} $'b$~= 8,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1189
\textit{card} \textit{nat}~= 8, \textit{card} ``$('a \times {'}b)$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1190
\textit{list}''~= 8, \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1191
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 8, and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1192
\textit{card} ``\kern1pt$'b$ \textit{list}''~= 8.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1193
\\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1194
Nitpick found a counterexample for
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1195
\textit{card} $'a$~= 5, \textit{card} $'b$~= 5,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1196
\textit{card} \textit{nat}~= 5, \textit{card} ``$('a \times {'}b)$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1197
\textit{list}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list}''~= 5, and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1198
\textit{card} ``\kern1pt$'b$ \textit{list}''~= 5:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1199
\\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1200
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1201
\hbox{}\qquad\qquad $\textit{xs} = [a_4, a_5]$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1202
\hbox{}\qquad\qquad $\textit{ys} = [b_3, b_3]$ \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1203
Total time: 1636 ms.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1204
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1205
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1206
In theory, it should be sufficient to test a single scope:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1207
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1208
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1209
\textbf{nitpick}~[\textit{card}~= 8]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1210
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1211
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1212
However, this is often less efficient in practice and may lead to overly complex
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1213
counterexamples.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1214
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1215
If the monotonicity check fails but we believe that the formula is monotonic (or
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1216
we don't mind missing some counterexamples), we can pass the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1217
\textit{mono} option. To convince yourself that this option is risky,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1218
simply consider this example from \S\ref{skolemization}:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1219
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1220
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1221
\textbf{lemma} ``$\exists g.\; \forall x\Colon 'b.~g~(f~x) = x
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1222
 \,\Longrightarrow\, \forall y\Colon {'}a.\; \exists x.~y = f~x$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1223
\textbf{nitpick} [\textit{mono}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1224
{\slshape Nitpick found no counterexample.} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1225
\textbf{nitpick} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1226
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1227
Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1228
\hbox{}\qquad $\vdots$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1229
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1230
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1231
(It turns out the formula holds if and only if $\textit{card}~'a \le
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1232
\textit{card}~'b$.) Although this is rarely advisable, the automatic
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1233
monotonicity checks can be disabled by passing \textit{non\_mono}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1234
(\S\ref{optimizations}).
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1235
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1236
As insinuated in \S\ref{natural-numbers-and-integers} and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1237
\S\ref{inductive-datatypes}, \textit{nat}, \textit{int}, and inductive datatypes
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1238
are normally monotonic and treated as such. The same is true for record types,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1239
\textit{rat}, \textit{real}, and some \textbf{typedef}'d types. Thus, given the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1240
cardinality specification 1--8, a formula involving \textit{nat}, \textit{int},
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1241
\textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1242
consider only 8~scopes instead of $32\,768$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1243
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
  1244
\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
  1245
\label{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
  1246
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
  1247
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
  1248
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
  1249
%
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
  1250
\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
  1251
\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
  1252
\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
  1253
\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
  1254
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
  1255
\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
  1256
%
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
  1257
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
  1258
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
  1259
%
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
  1260
\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
  1261
\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
  1262
\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
  1263
\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
  1264
\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
  1265
%
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
  1266
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
  1267
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
  1268
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
  1269
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
  1270
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
  1271
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
  1272
\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
  1273
\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
  1274
``$(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
  1275
``$\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
  1276
``$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
  1277
\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
  1278
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
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
  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
\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
  1282
\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
  1283
\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
  1284
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
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
  1286
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
  1287
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
\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
  1289
\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
  1290
\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
  1291
\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
  1292
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
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
  1294
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
\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
  1296
{\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
  1297
\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
  1298
\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
  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
\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
  1301
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
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
  1303
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
  1304
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
  1305
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
  1306
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
  1307
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
\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
  1309
\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
  1310
\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
  1311
\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
  1312
\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
  1313
\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
  1314
\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
  1315
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
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
  1317
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
  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
\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
  1320
\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
  1321
\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
  1322
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
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
  1324
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
  1325
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
\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
  1327
\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
  1328
\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
  1329
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
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
  1331
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
A similar technique can be employed for structural induction. 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
  1333
following mini-formalization of full binary trees will serve as illustration:
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
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
\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
  1336
\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
  1337
\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
  1338
``$\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
  1339
``$\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
  1340
\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
  1341
``$\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
  1342
\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
  1343
``$\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
  1344
\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
  1345
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
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
  1347
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
  1348
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
  1349
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
  1350
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
\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
  1352
\textbf{lemma} $``\lbrakk a \in \textit{labels}~t;\, b \in \textit{labels}~t;\, a \not= b\rbrakk {}$ \\
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
\phantom{\textbf{lemma} ``}$\,{\Longrightarrow}{\;\,} \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~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
  1354
\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
  1355
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
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
  1357
(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
  1358
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
\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
  1360
\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
  1361
\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
  1362
\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
  1363
\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
  1364
\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
  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
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
  1367
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
  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
\slshape
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
Hint: To check that the induction hypothesis is general enough, try the following command:
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
\textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_consts}].
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
\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
  1374
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
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
  1376
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
\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
  1378
\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 4: \\[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
  1379
\hbox{}\qquad Free variables: \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
  1380
\hbox{}\qquad\qquad $a = a_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
  1381
\hbox{}\qquad\qquad $b = a_3$ \\
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
\hbox{}\qquad\qquad $t = \xi_3$ \\
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
\hbox{}\qquad\qquad $u = \xi_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
  1384
\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
  1385
\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
  1386
    (\!\begin{aligned}[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
  1387
    & \xi_3 := \{a_4\},\> \xi_4 := \{a_1, a_3\}, \\[-2pt] %% TYPESETTING
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
    & \textit{Branch}~\xi_3~\xi_3 := \{a_4\}, \\[-2pt]
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
    & \textit{Branch}~\xi_3~\xi_4 := \{a_1, a_3, a_4\})\end{aligned}$ \\
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
\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
  1391
    (\!\begin{aligned}[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
  1392
    & \xi_3 := \xi_3,\> \xi_4 := \xi_3, \\[-2pt]
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
    & \textit{Branch}~\xi_3~\xi_3 := \textit{Branch}~\xi_3~\xi_3, \\[-2pt]
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
    & \textit{Branch}~\xi_4~\xi_3 := \textit{Branch}~\xi_3~\xi_3)\end{aligned}$ \\[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
  1395
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
blanchet
parents: 34126
diff changeset
  1396
even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
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
Reading the Nitpick manual is a most excellent idea.
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
But what's going on? The \textit{non\_std} ``${\kern1pt'a}~\textit{bin\_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
  1401
option told the tool to look for nonstandard models of binary trees, 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
  1402
means that new ``nonstandard'' trees $\xi_1, \xi_2, \ldots$, are now allowed in
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
addition to the standard trees generated by the \textit{Leaf} and
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
  1404
\textit{Branch} constructors.%
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
  1405
\footnote{Notice the similarity between allowing nonstandard trees here and
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
allowing unreachable states in the preceding example (by removing the ``$n \in
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
\textit{reach\/}$'' assumption). In both cases, we effectively enlarge 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
  1408
set of objects over which the induction is performed while doing 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
so as to test the induction hypothesis's strength.}
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
The new trees are so nonstandard that we know nothing about them, except what
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
  1411
the induction hypothesis states and what can be proved about all trees without
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
relying on induction or case distinction. The key observation is,
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
  1413
%
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
  1414
\begin{quote}
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
  1415
\textsl{If the 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
  1416
hypothesis is strong enough, the induction step will hold even for nonstandard
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
  1417
objects, and Nitpick won't find any nonstandard 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
  1418
\end{quote}
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
%
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
But here, Nitpick did find some nonstandard trees $t = \xi_3$
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
and $u = \xi_4$ such that $a \in \textit{labels}~t$, $b \notin
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
  1422
\textit{labels}~t$, $a \notin \textit{labels}~u$, and $b \in \textit{labels}~u$.
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
  1423
Because neither tree contains both $a$ and $b$, the induction hypothesis tells
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
us nothing about the labels of $\textit{swap}~t~a~b$ and $\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
  1425
and as a result we know nothing about the labels of 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
  1426
$\textit{swap}~(\textit{Branch}~t~u)~a~b$, which by definition equals
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
  1427
$\textit{Branch}$ $(\textit{swap}~t~a~b)$ $(\textit{swap}~u~a~b)$, whose
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
labels are $\textit{labels}$ $(\textit{swap}~t~a~b) \mathrel{\cup}
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
  1429
\textit{labels}$ $(\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
  1430
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
  1431
The solution is to ensure that we always know what the labels of the subtrees
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
  1432
are in the inductive step, by covering the cases where $a$ and/or~$b$ is not in
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
  1433
$t$ in the statement of 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
  1434
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
  1435
\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
  1436
\textbf{lemma} ``$\textit{labels}~(\textit{swap}~t~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
  1437
\phantom{\textbf{lemma} ``}$(\textrm{if}~a \in \textit{labels}~t~\textrm{then}$ \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
  1438
\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\}$ \\
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
  1439
\phantom{\textbf{lemma} ``(}$\textrm{else}$ \\
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
  1440
\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)$''
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
  1441
\postw
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and d