src/Doc/Nitpick/document/root.tex
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 55902 39cc8409373f
child 57040 fc96f394c7e5
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
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}
53091
d2afb0eb82e2 removed french option to manuals
blanchet
parents: 50488
diff changeset
     5
\usepackage[english]{babel}
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
     6
\usepackage{color}
35695
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35665
diff changeset
     7
\usepackage{footmisc}
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
     8
\usepackage{graphicx}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
     9
%\usepackage{mathpazo}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    10
\usepackage{multicol}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    11
\usepackage{stmaryrd}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    12
%\usepackage[scaled=.85]{beramono}
48963
f11d88bfa934 more standard document preparation within session context;
wenzelm
parents: 47717
diff changeset
    13
\usepackage{isabelle,iman,pdfsetup}
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    14
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    15
%\oddsidemargin=4.6mm
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    16
%\evensidemargin=4.6mm
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    17
%\textwidth=150mm
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    18
%\topmargin=4.6mm
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    19
%\headheight=0mm
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    20
%\headsep=0mm
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    21
%\textheight=234mm
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    22
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    23
\def\Colon{\mathord{:\mkern-1.5mu:}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    24
%\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    25
%\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    26
\def\lparr{\mathopen{(\mkern-4mu\mid}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    27
\def\rparr{\mathclose{\mid\mkern-4mu)}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    28
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    29
\def\unk{{?}}
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
    30
\def\unkef{(\lambda x.\; \unk)}
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
    31
\def\undef{(\lambda x.\; \_)}
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    32
%\def\unr{\textit{others}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    33
\def\unr{\ldots}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    34
\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    35
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    36
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    37
\hyphenation{Mini-Sat size-change First-Steps grand-parent nit-pick
45083
014342144091 put CryptoMiniSat first and remove warning about unsoundness now that it has been fixed in Kodkod
blanchet
parents: 45080
diff changeset
    38
counter-example counter-examples data-type data-types co-data-type
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    39
co-data-types in-duc-tive co-in-duc-tive}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    40
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    41
\urlstyle{tt}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    42
55290
3951ced4156c searchable underscores
blanchet
parents: 55081
diff changeset
    43
\renewcommand\_{\hbox{\textunderscore\kern-.05ex}}
3951ced4156c searchable underscores
blanchet
parents: 55081
diff changeset
    44
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    45
\begin{document}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    46
45515
9fa58cacf95d nicer bullets
blanchet
parents: 45084
diff changeset
    47
%%% TYPESETTING
9fa58cacf95d nicer bullets
blanchet
parents: 45084
diff changeset
    48
%\renewcommand\labelitemi{$\bullet$}
9fa58cacf95d nicer bullets
blanchet
parents: 45084
diff changeset
    49
\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}}
9fa58cacf95d nicer bullets
blanchet
parents: 45084
diff changeset
    50
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    51
\title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    52
Picking Nits \\[\smallskipamount]
33887
d9d0faf8d511 remove version number from Nitpick manual
blanchet
parents: 33731
diff changeset
    53
\Large A User's Guide to Nitpick for Isabelle/HOL}
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    54
\author{\hbox{} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    55
Jasmin Christian Blanchette \\
33887
d9d0faf8d511 remove version number from Nitpick manual
blanchet
parents: 33731
diff changeset
    56
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    57
\hbox{}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    58
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    59
\maketitle
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    60
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    61
\tableofcontents
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    62
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    63
\setlength{\parskip}{.7em plus .2em minus .1em}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    64
\setlength{\parindent}{0pt}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    65
\setlength{\abovedisplayskip}{\parskip}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    66
\setlength{\abovedisplayshortskip}{.9\parskip}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    67
\setlength{\belowdisplayskip}{\parskip}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    68
\setlength{\belowdisplayshortskip}{.9\parskip}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    69
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    70
% General-purpose enum environment with correct spacing
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    71
\newenvironment{enum}%
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    72
    {\begin{list}{}{%
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    73
        \setlength{\topsep}{.1\parskip}%
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    74
        \setlength{\partopsep}{.1\parskip}%
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    75
        \setlength{\itemsep}{\parskip}%
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    76
        \advance\itemsep by-\parsep}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    77
    {\end{list}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    78
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    79
\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    80
\advance\rightskip by\leftmargin}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    81
\def\post{\vskip0pt plus1ex\endgroup}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    82
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    83
\def\prew{\pre\advance\rightskip by-\leftmargin}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    84
\def\postw{\post}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    85
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    86
\section{Introduction}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    87
\label{introduction}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    88
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents: 36390
diff changeset
    89
Nitpick \cite{blanchette-nipkow-2010} is a counterexample generator for
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    90
Isabelle/HOL \cite{isa-tutorial} that is designed to handle formulas
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    91
combining (co)in\-duc\-tive datatypes, (co)in\-duc\-tively defined predicates, and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    92
quantifiers. It builds on Kodkod \cite{torlak-jackson-2007}, a highly optimized
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    93
first-order relational model finder developed by the Software Design Group at
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    94
MIT. It is conceptually similar to Refute \cite{weber-2008}, from which it
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    95
borrows many ideas and code fragments, but it benefits from Kodkod's
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    96
optimizations and a new encoding scheme. The name Nitpick is shamelessly
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    97
appropriated from a now retired Alloy precursor.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    98
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
    99
Nitpick is easy to use---you simply enter \textbf{nitpick} after a putative
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   100
theorem and wait a few seconds. Nonetheless, there are situations where knowing
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   101
how it works under the hood and how it reacts to various options helps
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   102
increase the test coverage. This manual also explains how to install the tool on
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   103
your workstation. Should the motivation fail you, think of the many hours of
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   104
hard work Nitpick will save you. Proving non-theorems is \textsl{hard work}.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   105
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   106
Another common use of Nitpick is to find out whether the axioms of a locale are
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   107
satisfiable, while the locale is being developed. To check this, it suffices to
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   108
write
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   109
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   110
\prew
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   111
\textbf{lemma}~``$\textit{False\/}$'' \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   112
\textbf{nitpick}~[\textit{show\_all}]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   113
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   114
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   115
after the locale's \textbf{begin} keyword. To falsify \textit{False}, Nitpick
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   116
must find a model for the axioms. If it finds no model, we have an indication
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   117
that the axioms might be unsatisfiable.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   118
53760
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53091
diff changeset
   119
For Isabelle/jEdit users, Nitpick provides an automatic mode that can be enabled
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53091
diff changeset
   120
via the ``Auto Nitpick'' option under ``Plugins > Plugin Options > Isabelle >
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53091
diff changeset
   121
General.'' In this mode, Nitpick is run on every newly entered theorem.
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents: 33559
diff changeset
   122
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   123
\newbox\boxA
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   124
\setbox\boxA=\hbox{\texttt{nospam}}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   125
46242
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   126
\newcommand\authoremail{\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   127
in.\allowbreak tum.\allowbreak de}}
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   128
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   129
To run Nitpick, you must also make sure that the theory \textit{Nitpick} is
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   130
imported---this is rarely a problem in practice since it is part of
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   131
\textit{Main}. The examples presented in this manual can be found
55290
3951ced4156c searchable underscores
blanchet
parents: 55081
diff changeset
   132
in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_\allowbreak Examples/\allowbreak Manual\_Nits.thy} theory.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   133
The known bugs and limitations at the time of writing are listed in
46242
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   134
\S\ref{known-bugs-and-limitations}. Comments and bug reports concerning either
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   135
the tool or the manual should be directed to the author at \authoremail.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   136
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   137
\vskip2.5\smallskipamount
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   138
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   139
\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   140
suggesting several textual improvements.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   141
% and Perry James for reporting a typo.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   142
46242
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   143
\section{Installation}
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   144
\label{installation}
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   145
53760
cf37f4b84824 moved focus to Isabell/jEdit and away from Proof General
blanchet
parents: 53091
diff changeset
   146
Nitpick is part of Isabelle, so you don't need to install it. However, it
46242
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   147
relies on a third-party Kodkod front-end called Kodkodi as well as a Java
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   148
virtual machine called \texttt{java} (version 1.5 or above).
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   149
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   150
There are two main ways of installing Kodkodi:
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   151
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   152
\begin{enum}
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   153
\item[\labelitemi] If you installed an official Isabelle package,
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   154
it should already include a properly setup version of Kodkodi.
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   155
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   156
\item[\labelitemi] If you use a repository or snapshot version of Isabelle, you
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   157
an official Isabelle package, you can download the Isabelle-aware Kodkodi package
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   158
from \url{http://www21.in.tum.de/~blanchet/\#software}. Extract the archive, then add a
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   159
line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}%
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   160
\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   161
startup. Its value can be retrieved by executing \texttt{isabelle}
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   162
\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   163
file with the absolute path to Kodkodi. For example, if the
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   164
\texttt{components} file does not exist yet and you extracted Kodkodi to
50488
1b3eb579e08b use modern SAT solvers with modern Kodkod versions
blanchet
parents: 49618
diff changeset
   165
\texttt{/usr/local/kodkodi-1.5.2}, create it with the single line
46242
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   166
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   167
\prew
50488
1b3eb579e08b use modern SAT solvers with modern Kodkod versions
blanchet
parents: 49618
diff changeset
   168
\texttt{/usr/local/kodkodi-1.5.2}
46242
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   169
\postw
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   170
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   171
(including an invisible newline character) in it.
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   172
\end{enum}
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   173
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   174
To check whether Kodkodi is successfully installed, you can try out the example
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   175
in \S\ref{propositional-logic}.
36926
90bb12cf8e36 added Sledgehammer manual;
blanchet
parents: 36390
diff changeset
   176
35712
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   177
\section{First Steps}
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   178
\label{first-steps}
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   179
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   180
This section introduces Nitpick by presenting small examples. If possible, you
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   181
should try out the examples on your workstation. Your theory file should start
35284
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   182
as follows:
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   183
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   184
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   185
\textbf{theory}~\textit{Scratch} \\
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   186
\textbf{imports}~\textit{Main~Quotient\_Product~RealDef} \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   187
\textbf{begin}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   188
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   189
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35695
diff changeset
   190
The results presented here were obtained using the JNI (Java Native Interface)
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35695
diff changeset
   191
version of MiniSat and with multithreading disabled to reduce nondeterminism.
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35695
diff changeset
   192
This was done by adding the line
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   193
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   194
\prew
35710
58acd48904bc made "Manual_Nits" tests more robust
blanchet
parents: 35695
diff changeset
   195
\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   196
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   197
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   198
after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
45080
b4f1beba1897 clarify platforms
blanchet
parents: 45079
diff changeset
   199
Kodkodi and is precompiled for Linux, Mac~OS~X, and Windows (Cygwin). Other SAT
50488
1b3eb579e08b use modern SAT solvers with modern Kodkod versions
blanchet
parents: 49618
diff changeset
   200
solvers can also be used, as explained in \S\ref{optimizations}. If you
45080
b4f1beba1897 clarify platforms
blanchet
parents: 45079
diff changeset
   201
have already configured SAT solvers in Isabelle (e.g., for Refute), these will
b4f1beba1897 clarify platforms
blanchet
parents: 45079
diff changeset
   202
also be available to Nitpick.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   203
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   204
\subsection{Propositional Logic}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   205
\label{propositional-logic}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   206
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   207
Let's start with a trivial example from propositional logic:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   208
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   209
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   210
\textbf{lemma}~``$P \longleftrightarrow Q$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   211
\textbf{nitpick}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   212
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   213
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   214
You should get the following output:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   215
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   216
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   217
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   218
Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   219
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   220
\hbox{}\qquad\qquad $P = \textit{True}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   221
\hbox{}\qquad\qquad $Q = \textit{False}$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   222
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   223
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   224
Nitpick can also be invoked on individual subgoals, as in the example below:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   225
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   226
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   227
\textbf{apply}~\textit{auto} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   228
{\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
   229
\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
   230
\phantom{0}2. $Q\,\Longrightarrow\, P$} \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   231
\textbf{nitpick}~1 \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   232
{\slshape Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   233
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   234
\hbox{}\qquad\qquad $P = \textit{True}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   235
\hbox{}\qquad\qquad $Q = \textit{False}$} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   236
\textbf{nitpick}~2 \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   237
{\slshape Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   238
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   239
\hbox{}\qquad\qquad $P = \textit{False}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   240
\hbox{}\qquad\qquad $Q = \textit{True}$} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   241
\textbf{oops}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   242
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   243
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   244
\subsection{Type Variables}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   245
\label{type-variables}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   246
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   247
If you are left unimpressed by the previous example, don't worry. The next
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   248
one is more mind- and computer-boggling:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   249
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   250
\prew
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   251
\textbf{lemma} ``$x \in A\,\Longrightarrow\, (\textrm{THE}~y.\;y \in A) \in A$''
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   252
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   253
\pagebreak[2] %% TYPESETTING
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   254
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   255
The putative lemma involves the definite description operator, {THE}, presented
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   256
in section 5.10.1 of the Isabelle tutorial \cite{isa-tutorial}. The
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   257
operator is defined by the axiom $(\textrm{THE}~x.\; x = a) = a$. The putative
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   258
lemma is merely asserting the indefinite description operator axiom with {THE}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   259
substituted for {SOME}.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   260
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   261
The free variable $x$ and the bound variable $y$ have type $'a$. For formulas
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   262
containing type variables, Nitpick enumerates the possible domains for each type
38181
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
   263
variable, up to a given cardinality (10 by default), looking for a finite
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   264
countermodel:
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{nitpick} [\textit{verbose}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   268
\slshape
38181
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
   269
Trying 10 scopes: \nopagebreak \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   270
\hbox{}\qquad \textit{card}~$'a$~= 1; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   271
\hbox{}\qquad \textit{card}~$'a$~= 2; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   272
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
38181
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
   273
\hbox{}\qquad \textit{card}~$'a$~= 10. \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   274
Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   275
\hbox{}\qquad Free variables: \nopagebreak \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   276
\hbox{}\qquad\qquad $A = \{a_2,\, a_3\}$ \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   277
\hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount]
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   278
Total time: 963 ms.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   279
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   280
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   281
Nitpick found a counterexample in which $'a$ has cardinality 3. (For
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   282
cardinalities 1 and 2, the formula holds.) In the counterexample, the three
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   283
values of type $'a$ are written $a_1$, $a_2$, and $a_3$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   284
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   285
The message ``Trying $n$ scopes: {\ldots}''\ is shown only if the option
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   286
\textit{verbose} is enabled. You can specify \textit{verbose} each time you
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   287
invoke \textbf{nitpick}, or you can set it globally using the command
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   288
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   289
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   290
\textbf{nitpick\_params} [\textit{verbose}]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   291
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   292
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   293
This command also displays the current default values for all of the options
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   294
supported by Nitpick. The options are listed in \S\ref{option-reference}.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   295
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   296
\subsection{Constants}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   297
\label{constants}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   298
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   299
By just looking at Nitpick's output, it might not be clear why the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   300
counterexample in \S\ref{type-variables} is genuine. Let's invoke Nitpick again,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   301
this time telling it to show the values of the constants that occur in the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   302
formula:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   303
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   304
\prew
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   305
\textbf{lemma} ``$x \in A\,\Longrightarrow\, (\textrm{THE}~y.\;y \in A) \in A$'' \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   306
\textbf{nitpick}~[\textit{show\_consts}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   307
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   308
Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   309
\hbox{}\qquad Free variables: \nopagebreak \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   310
\hbox{}\qquad\qquad $A = \{a_2,\, a_3\}$ \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   311
\hbox{}\qquad\qquad $x = a_3$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   312
\hbox{}\qquad Constant: \nopagebreak \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   313
\hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;y \in A = a_1$
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   314
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   315
39359
6f49c7fbb1b1 remove "fast_descs" option from Nitpick;
blanchet
parents: 39317
diff changeset
   316
As the result of an optimization, Nitpick directly assigned a value to the
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   317
subterm $\textrm{THE}~y.\;y \in A$, rather than to the \textit{The} constant. We
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   318
can disable this optimization by using the command
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   319
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   320
\prew
39359
6f49c7fbb1b1 remove "fast_descs" option from Nitpick;
blanchet
parents: 39317
diff changeset
   321
\textbf{nitpick}~[\textit{dont\_specialize},\, \textit{show\_consts}]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   322
\postw
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
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   328
\textbf{lemma} ``$\exists {!}x.\; x \in A\,\Longrightarrow\, (\textrm{THE}~y.\;y \in A) \in A$''
33191
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
42959
ee829022381d use \<emdash> rather than \<midarrow>
blanchet
parents: 42511
diff changeset
   344
\texttt{\char`\\\char`\<emdash\char`\>}.} \\[2\smallskipamount]
33191
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
38181
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
   348
Let's see if Sledgehammer can find a proof:
33191
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]
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   352
{\slshape Sledgehammer: ``$e$'' on goal \\
46242
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   353
Try this: \textbf{by}~(\textit{metis~theI}) (42 ms).} \\
99a2a541c125 improve installation instructions
blanchet
parents: 46110
diff changeset
   354
\hbox{}\qquad\vdots \\[2\smallskipamount]
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   355
\textbf{by}~(\textit{metis~theI\/})
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   356
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   357
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   358
This must be our lucky day.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   359
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   360
\subsection{Skolemization}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   361
\label{skolemization}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   362
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   363
Are all invertible functions onto? Let's find out:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   364
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   365
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   366
\textbf{lemma} ``$\exists g.\; \forall x.~g~(f~x) = x
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   367
 \,\Longrightarrow\, \forall y.\; \exists x.~y = f~x$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   368
\textbf{nitpick} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   369
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   370
Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   371
\hbox{}\qquad Free variable: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   372
\hbox{}\qquad\qquad $f = \undef{}(b_1 := a_1)$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   373
\hbox{}\qquad Skolem constants: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   374
\hbox{}\qquad\qquad $g = \undef{}(a_1 := b_1,\> a_2 := b_1)$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   375
\hbox{}\qquad\qquad $y = a_2$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   376
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   377
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   378
(The Isabelle/HOL notation $f(x := y)$ denotes the function that maps $x$ to $y$
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   379
and that otherwise behaves like $f$.)
33191
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
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   418
What happened here is that Nitpick expanded \textit{sym} to its definition:
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   419
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   420
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   421
$\mathit{sym}~r \,\equiv\,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   422
 \forall x\> y.\,\> (x, y) \in r \longrightarrow (y, x) \in r.$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   423
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   424
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   425
As their names suggest, the Skolem constants $\mathit{sym}.x$ and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   426
$\mathit{sym}.y$ are simply the bound variables $x$ and $y$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   427
from \textit{sym}'s definition.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   428
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   429
\subsection{Natural Numbers and Integers}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   430
\label{natural-numbers-and-integers}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   431
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   432
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
   433
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
   434
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
   435
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
   436
Internally, undefined values lead to a three-valued logic.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   437
35284
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   438
Here is an example involving \textit{int\/}:
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   439
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   440
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   441
\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
   442
\textbf{nitpick} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   443
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   444
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   445
\hbox{}\qquad\qquad $i = 0$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   446
\hbox{}\qquad\qquad $j = 1$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   447
\hbox{}\qquad\qquad $m = 1$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   448
\hbox{}\qquad\qquad $n = 0$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   449
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   450
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34038
diff changeset
   451
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
   452
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
   453
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
   454
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
   455
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
   456
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
   457
the \textit{bits} option. For example:
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34038
diff changeset
   458
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34038
diff changeset
   459
\prew
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34038
diff changeset
   460
\textbf{nitpick} [\textit{binary\_ints}, \textit{bits}${} = 16$]
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34038
diff changeset
   461
\postw
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34038
diff changeset
   462
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   463
With infinite types, we don't always have the luxury of a genuine counterexample
41992
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   464
and must often content ourselves with a potentially spurious one. The tedious
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   465
task of finding out whether the potentially spurious counterexample is in fact
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   466
genuine can be delegated to \textit{auto} by passing \textit{check\_potential}.
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   467
For example:
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   468
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   469
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   470
\textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
35712
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   471
\textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[2\smallskipamount]
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35335
diff changeset
   472
\slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
41992
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   473
fragment. Only potentially spurious counterexamples may be found. \\[2\smallskipamount]
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   474
Nitpick found a potentially spurious counterexample: \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   475
\hbox{}\qquad Free variable: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   476
\hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   477
Confirmation by ``\textit{auto}'': The above counterexample is genuine.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   478
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   479
41992
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   480
You might wonder why the counterexample is first reported as potentially
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   481
spurious. The root of the problem is that the bound variable in $\forall n.\;
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   482
\textit{Suc}~n \mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   483
an $n$ such that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   484
\textit{False}; but otherwise, it does not know anything about values of $n \ge
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   485
\textit{card~nat}$ and must therefore evaluate the assumption to~$\unk$, not
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   486
\textit{True}. Since the assumption can never be satisfied, the putative lemma
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   487
can never be falsified.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   488
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   489
Incidentally, if you distrust the so-called genuine counterexamples, you can
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   490
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
   491
aware that \textit{auto} will usually fail to prove that the counterexample is
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   492
genuine or spurious.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   493
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   494
Some conjectures involving elementary number theory make Nitpick look like a
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   495
giant with feet of clay:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   496
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   497
\prew
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   498
\textbf{lemma} ``$P~\textit{Suc\/}$'' \\
35309
997aa3a3e4bb catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents: 35284
diff changeset
   499
\textbf{nitpick} \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   500
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   501
Nitpick found no counterexample.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   502
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   503
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34038
diff changeset
   504
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
   505
\{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
   506
\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
   507
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
   508
example is similar:
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   509
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   510
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   511
\textbf{lemma} ``$P~(\textit{op}~{+}\Colon
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   512
\textit{nat}\mathbin{\Rightarrow}\textit{nat}\mathbin{\Rightarrow}\textit{nat})$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   513
\textbf{nitpick} [\textit{card nat} = 1] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   514
{\slshape Nitpick found a counterexample:} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   515
\hbox{}\qquad Free variable: \nopagebreak \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   516
\hbox{}\qquad\qquad $P = \unkef(\unkef(0 := \unkef(0 := 0)) := \mathit{False})$ \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   517
\textbf{nitpick} [\textit{card nat} = 2] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   518
{\slshape Nitpick found no counterexample.}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   519
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   520
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   521
The problem here is that \textit{op}~+ is total when \textit{nat} is taken to be
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   522
$\{0\}$ but becomes partial as soon as we add $1$, because
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   523
$1 + 1 \notin \{0, 1\}$.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   524
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   525
Because numbers are infinite and are approximated using a three-valued logic,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   526
there is usually no need to systematically enumerate domain sizes. If Nitpick
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   527
cannot find a genuine counterexample for \textit{card~nat}~= $k$, it is very
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   528
unlikely that one could be found for smaller domains. (The $P~(\textit{op}~{+})$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   529
example above is an exception to this principle.) Nitpick nonetheless enumerates
38181
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
   530
all cardinalities from 1 to 10 for \textit{nat}, mainly because smaller
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   531
cardinalities are fast to handle and give rise to simpler counterexamples. This
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   532
is explained in more detail in \S\ref{scope-monotonicity}.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   533
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   534
\subsection{Inductive Datatypes}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   535
\label{inductive-datatypes}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   536
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   537
Like natural numbers and integers, inductive datatypes with recursive
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   538
constructors admit no finite models and must be approximated by a subterm-closed
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   539
subset. For example, using a cardinality of 10 for ${'}a~\textit{list}$,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   540
Nitpick looks for all counterexamples that can be built using at most 10
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   541
different lists.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   542
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   543
Let's see with an example involving \textit{hd} (which returns the first element
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   544
of a list) and $@$ (which concatenates two lists):
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   545
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   546
\prew
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   547
\textbf{lemma} ``$\textit{hd}~(\textit{xs} \mathbin{@} [y, y]) = \textit{hd}~\textit{xs\/}$'' \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   548
\textbf{nitpick} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   549
\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   550
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   551
\hbox{}\qquad\qquad $\textit{xs} = []$ \\
35078
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
   552
\hbox{}\qquad\qquad $\textit{y} = a_1$
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   553
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   554
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   555
To see why the counterexample is genuine, we enable \textit{show\_consts}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   556
and \textit{show\_\allowbreak datatypes}:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   557
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   558
\prew
55892
6fba7f6c532a updated docs
blanchet
parents: 55889
diff changeset
   559
{\slshape Type:} \\
35078
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
   560
\hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_1],\, [a_1, a_1],\, \unr\}$ \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   561
{\slshape Constants:} \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   562
\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \unkef([] := [a_1, a_1])$ \\
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   563
\hbox{}\qquad $\textit{hd} = \unkef([] := a_2,\> [a_1] := a_1,\> [a_1, a_1] := a_1)$
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   564
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   565
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   566
Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   567
including $a_2$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   568
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   569
The second constant, $\lambda x_1.\; x_1 \mathbin{@} [y, y]$, is simply the
35078
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
   570
append operator whose second argument is fixed to be $[y, y]$. Appending $[a_1,
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
   571
a_1]$ to $[a_1]$ would normally give $[a_1, a_1, a_1]$, but this value is not
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   572
representable in the subset of $'a$~\textit{list} considered by Nitpick, which
55892
6fba7f6c532a updated docs
blanchet
parents: 55889
diff changeset
   573
is shown under the ``Type'' heading; hence the result is $\unk$. Similarly,
35078
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
   574
appending $[a_1, a_1]$ to itself gives $\unk$.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   575
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   576
Given \textit{card}~$'a = 3$ and \textit{card}~$'a~\textit{list} = 3$, Nitpick
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   577
considers the following subsets:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   578
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   579
\kern-.5\smallskipamount %% TYPESETTING
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   580
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   581
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   582
\begin{multicols}{3}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   583
$\{[],\, [a_1],\, [a_2]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   584
$\{[],\, [a_1],\, [a_3]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   585
$\{[],\, [a_2],\, [a_3]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   586
$\{[],\, [a_1],\, [a_1, a_1]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   587
$\{[],\, [a_1],\, [a_2, a_1]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   588
$\{[],\, [a_1],\, [a_3, a_1]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   589
$\{[],\, [a_2],\, [a_1, a_2]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   590
$\{[],\, [a_2],\, [a_2, a_2]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   591
$\{[],\, [a_2],\, [a_3, a_2]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   592
$\{[],\, [a_3],\, [a_1, a_3]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   593
$\{[],\, [a_3],\, [a_2, a_3]\}$; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   594
$\{[],\, [a_3],\, [a_3, a_3]\}$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   595
\end{multicols}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   596
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   597
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   598
\kern-2\smallskipamount %% TYPESETTING
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   599
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   600
All subterm-closed subsets of $'a~\textit{list}$ consisting of three values
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   601
are listed and only those. As an example of a non-subterm-closed subset,
35078
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
   602
consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_2]\}$, and observe
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
   603
that $[a_1, a_2]$ (i.e., $a_1 \mathbin{\#} [a_2]$) has $[a_2] \notin
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   604
\mathcal{S}$ as a subterm.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   605
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   606
Here's another m\"ochtegern-lemma that Nitpick can refute without a blink:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   607
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   608
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   609
\textbf{lemma} ``$\lbrakk \textit{length}~\textit{xs} = 1;\> \textit{length}~\textit{ys} = 1
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   610
\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys\/}$''
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   611
\\
55889
6bfbec3dff62 tuned code
blanchet
parents: 55888
diff changeset
   612
\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   613
\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   614
\hbox{}\qquad Free variables: \nopagebreak \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   615
\hbox{}\qquad\qquad $\textit{xs} = [a_2]$ \\
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   616
\hbox{}\qquad\qquad $\textit{ys} = [a_1]$ \\
55892
6fba7f6c532a updated docs
blanchet
parents: 55889
diff changeset
   617
\hbox{}\qquad Types: \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   618
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
35078
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
   619
\hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_1],\, [a_2],\, \unr\}$
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   620
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   621
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   622
Because datatypes are approximated using a three-valued logic, there is usually
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   623
no need to systematically enumerate cardinalities: If Nitpick cannot find a
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   624
genuine counterexample for \textit{card}~$'a~\textit{list}$~= 10, it is very
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   625
unlikely that one could be found for smaller cardinalities.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   626
35284
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   627
\subsection{Typedefs, Quotient Types, Records, Rationals, and Reals}
35712
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   628
\label{typedefs-quotient-types-records-rationals-and-reals}
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   629
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   630
Nitpick generally treats types declared using \textbf{typedef} as datatypes
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   631
whose single constructor is the corresponding \textit{Abs\_\kern.1ex} function.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   632
For example:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   633
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   634
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   635
\textbf{typedef}~\textit{three} = ``$\{0\Colon\textit{nat},\, 1,\, 2\}$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   636
\textbf{by}~\textit{blast} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   637
\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
   638
\textbf{definition}~$B \mathbin{\Colon} \textit{three}$ \textbf{where} ``$B \,\equiv\, \textit{Abs\_three}~1$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   639
\textbf{definition}~$C \mathbin{\Colon} \textit{three}$ \textbf{where} ``$C \,\equiv\, \textit{Abs\_three}~2$'' \\[2\smallskipamount]
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   640
\textbf{lemma} ``$\lbrakk A \in X;\> B \in X\rbrakk \,\Longrightarrow\, c \in X$'' \\
55889
6bfbec3dff62 tuned code
blanchet
parents: 55888
diff changeset
   641
\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   642
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   643
\hbox{}\qquad Free variables: \nopagebreak \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   644
\hbox{}\qquad\qquad $X = \{\Abs{0},\, \Abs{1}\}$ \\
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   645
\hbox{}\qquad\qquad $c = \Abs{2}$ \\
55892
6fba7f6c532a updated docs
blanchet
parents: 55889
diff changeset
   646
\hbox{}\qquad Types: \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   647
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
35078
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
   648
\hbox{}\qquad\qquad $\textit{three} = \{\Abs{0},\, \Abs{1},\, \Abs{2},\, \unr\}$
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   649
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   650
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   651
In the output above, $\Abs{n}$ abbreviates $\textit{Abs\_three}~n$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   652
35284
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   653
Quotient types are handled in much the same way. The following fragment defines
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   654
the integer type \textit{my\_int} by encoding the integer $x$ by a pair of
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   655
natural numbers $(m, n)$ such that $x + n = m$:
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   656
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   657
\prew
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   658
\textbf{fun} \textit{my\_int\_rel} \textbf{where} \\
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   659
``$\textit{my\_int\_rel}~(x,\, y)~(u,\, v) = (x + v = u + y)$'' \\[2\smallskipamount]
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   660
%
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   661
\textbf{quotient\_type}~\textit{my\_int} = ``$\textit{nat} \times \textit{nat\/}$''$\;{/}\;$\textit{my\_int\_rel} \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   662
\textbf{by}~(\textit{auto simp add\/}:\ \textit{equivp\_def fun\_eq\_iff}) \\[2\smallskipamount]
35284
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   663
%
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   664
\textbf{definition}~\textit{add\_raw}~\textbf{where} \\
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   665
``$\textit{add\_raw} \,\equiv\, \lambda(x,\, y)~(u,\, v).\; (x + (u\Colon\textit{nat}), y + (v\Colon\textit{nat}))$'' \\[2\smallskipamount]
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   666
%
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   667
\textbf{quotient\_definition} ``$\textit{add\/}\Colon\textit{my\_int} \Rightarrow \textit{my\_int} \Rightarrow \textit{my\_int\/}$'' \textbf{is} \textit{add\_raw} \\[2\smallskipamount]
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   668
%
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   669
\textbf{lemma} ``$\textit{add}~x~y = \textit{add}~x~x$'' \\
55889
6bfbec3dff62 tuned code
blanchet
parents: 55888
diff changeset
   670
\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
35284
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   671
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   672
\hbox{}\qquad Free variables: \nopagebreak \\
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   673
\hbox{}\qquad\qquad $x = \Abs{(0,\, 0)}$ \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   674
\hbox{}\qquad\qquad $y = \Abs{(0,\, 1)}$ \\
55892
6fba7f6c532a updated docs
blanchet
parents: 55889
diff changeset
   675
\hbox{}\qquad Types: \\
35284
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   676
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, \unr\}$ \\
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
   677
\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat}~[\textsl{boxed\/}] = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   678
\hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(0,\, 1)},\> \unr\}$
35284
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   679
\postw
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   680
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   681
The values $\Abs{(0,\, 0)}$ and $\Abs{(0,\, 1)}$ represent the
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   682
integers $0$ and $-1$, respectively. Other representants would have been
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   683
possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(11,\, 12)}$. If we are going to
35712
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   684
use \textit{my\_int} extensively, it pays off to install a term postprocessor
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   685
that converts the pair notation to the standard mathematical notation:
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   686
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   687
\prew
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   688
$\textbf{ML}~\,\{{*} \\
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   689
\!\begin{aligned}[t]
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   690
%& ({*}~\,\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \\[-2pt]
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   691
%& \phantom{(*}~\,{\rightarrow}\;\textit{term}~\,{*}) \\[-2pt]
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   692
& \textbf{fun}\,~\textit{my\_int\_postproc}~\_~\_~\_~T~(\textit{Const}~\_~\$~(\textit{Const}~\_~\$~\textit{t1}~\$~\textit{t2\/})) = {} \\[-2pt]
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   693
& \phantom{fun}\,~\textit{HOLogic.mk\_number}~T~(\textit{snd}~(\textit{HOLogic.dest\_number~t1}) \\[-2pt]
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   694
& \phantom{fun\,~\textit{HOLogic.mk\_number}~T~(}{-}~\textit{snd}~(\textit{HOLogic.dest\_number~t2\/})) \\[-2pt]
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   695
& \phantom{fun}\!{\mid}\,~\textit{my\_int\_postproc}~\_~\_~\_~\_~t = t \\[-2pt]
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   696
{*}\}\end{aligned}$ \\[2\smallskipamount]
38284
9f98107ad8b4 use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents: 38274
diff changeset
   697
$\textbf{declaration}~\,\{{*} \\
35712
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   698
\!\begin{aligned}[t]
38284
9f98107ad8b4 use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents: 38274
diff changeset
   699
& \textit{Nitpick\_Model.register\_term\_postprocessor}~\!\begin{aligned}[t]
38241
842057125043 document the non-legacy interfaces
blanchet
parents: 38213
diff changeset
   700
  & @\{\textrm{typ}~\textit{my\_int}\} \\[-2pt]
842057125043 document the non-legacy interfaces
blanchet
parents: 38213
diff changeset
   701
  & \textit{my\_int\_postproc}\end{aligned} \\[-2pt]
35712
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   702
{*}\}\end{aligned}$
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   703
\postw
35284
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   704
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   705
Records are handled as datatypes with a single constructor:
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   706
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   707
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   708
\textbf{record} \textit{point} = \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   709
\hbox{}\quad $\textit{Xcoord} \mathbin{\Colon} \textit{int}$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   710
\hbox{}\quad $\textit{Ycoord} \mathbin{\Colon} \textit{int}$ \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   711
\textbf{lemma} ``$\textit{Xcoord}~(p\Colon\textit{point}) = \textit{Xcoord}~(q\Colon\textit{point})$'' \\
55889
6bfbec3dff62 tuned code
blanchet
parents: 55888
diff changeset
   712
\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   713
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   714
\hbox{}\qquad Free variables: \nopagebreak \\
35078
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
   715
\hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
   716
\hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
55892
6fba7f6c532a updated docs
blanchet
parents: 55889
diff changeset
   717
\hbox{}\qquad Types: \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   718
\hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, \unr\}$ \\
35078
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
   719
\hbox{}\qquad\qquad $\textit{point} = \{\!\begin{aligned}[t]
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
   720
& \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr, \\[-2pt] %% TYPESETTING
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
   721
& \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   722
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   723
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   724
Finally, Nitpick provides rudimentary support for rationals and reals using a
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   725
similar approach:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   726
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   727
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   728
\textbf{lemma} ``$4 * x + 3 * (y\Colon\textit{real}) \not= 1/2$'' \\
55889
6bfbec3dff62 tuned code
blanchet
parents: 55888
diff changeset
   729
\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   730
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   731
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   732
\hbox{}\qquad\qquad $x = 1/2$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   733
\hbox{}\qquad\qquad $y = -1/2$ \\
55892
6fba7f6c532a updated docs
blanchet
parents: 55889
diff changeset
   734
\hbox{}\qquad Types: \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   735
\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, 3,\, 4,\, 5,\, 6,\, 7,\, \unr\}$ \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   736
\hbox{}\qquad\qquad $\textit{int} = \{-3,\, -2,\, -1,\, 0,\, 1,\, 2,\, 3,\, 4,\, \unr\}$ \\
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   737
\hbox{}\qquad\qquad $\textit{real} = \{-3/2,\, -1/2,\, 0,\, 1/2,\, 1,\, 2,\, 3,\, 4,\, \unr\}$
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   738
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   739
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   740
\subsection{Inductive and Coinductive Predicates}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   741
\label{inductive-and-coinductive-predicates}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   742
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   743
Inductively defined predicates (and sets) are particularly problematic for
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   744
counterexample generators. They can make Quickcheck~\cite{berghofer-nipkow-2004}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   745
loop forever and Refute~\cite{weber-2008} run out of resources. The crux of
38176
bc2f9383fd59 clarify attribute documentation
blanchet
parents: 38175
diff changeset
   746
the problem is that they are defined using a least fixed-point construction.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   747
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   748
Nitpick's philosophy is that not all inductive predicates are equal. Consider
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   749
the \textit{even} predicate below:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   750
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   751
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   752
\textbf{inductive}~\textit{even}~\textbf{where} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   753
``\textit{even}~0'' $\,\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   754
``\textit{even}~$n\,\Longrightarrow\, \textit{even}~(\textit{Suc}~(\textit{Suc}~n))$''
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   755
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   756
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   757
This predicate enjoys the desirable property of being well-founded, which means
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   758
that the introduction rules don't give rise to infinite chains of the form
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   759
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   760
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   761
$\cdots\,\Longrightarrow\, \textit{even}~k''
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   762
       \,\Longrightarrow\, \textit{even}~k'
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   763
       \,\Longrightarrow\, \textit{even}~k.$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   764
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   765
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   766
For \textit{even}, this is obvious: Any chain ending at $k$ will be of length
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   767
$k/2 + 1$:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   768
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   769
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   770
$\textit{even}~0\,\Longrightarrow\, \textit{even}~2\,\Longrightarrow\, \cdots
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   771
       \,\Longrightarrow\, \textit{even}~(k - 2)
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   772
       \,\Longrightarrow\, \textit{even}~k.$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   773
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   774
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   775
Wellfoundedness is desirable because it enables Nitpick to use a very efficient
38176
bc2f9383fd59 clarify attribute documentation
blanchet
parents: 38175
diff changeset
   776
fixed-point computation.%
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   777
\footnote{If an inductive predicate is
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   778
well-founded, then it has exactly one fixed point, which is simultaneously the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   779
least and the greatest fixed point. In these circumstances, the computation of
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   780
the least fixed point amounts to the computation of an arbitrary fixed point,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   781
which can be performed using a straightforward recursive equation.}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   782
Moreover, Nitpick can prove wellfoundedness of most well-founded predicates,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   783
just as Isabelle's \textbf{function} package usually discharges termination
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   784
proof obligations automatically.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   785
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   786
Let's try an example:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   787
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   788
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   789
\textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
35712
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   790
\textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   791
\slshape The inductive predicate ``\textit{even}'' was proved well-founded.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   792
Nitpick can compute it efficiently. \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   793
Trying 1 scope: \\
35712
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   794
\hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   795
Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported fragment. Only
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   796
potentially spurious counterexamples may be found. \\[2\smallskipamount]
41992
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   797
Nitpick found a potentially spurious counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   798
\hbox{}\qquad Empty assignment \\[2\smallskipamount]
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   799
Nitpick could not find a better counterexample. It checked 1 of 1 scope. \\[2\smallskipamount]
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   800
Total time: 1.62 s.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   801
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   802
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   803
No genuine counterexample is possible because Nitpick cannot rule out the
35712
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   804
existence of a natural number $n \ge 50$ such that both $\textit{even}~n$ and
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   805
$\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   806
existential quantifier:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   807
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   808
\prew
35712
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   809
\textbf{lemma} ``$\exists n \mathbin{\le} 49.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
   810
\textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}] \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   811
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   812
\hbox{}\qquad Empty assignment
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   813
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   814
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   815
So far we were blessed by the wellfoundedness of \textit{even}. What happens if
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   816
we use the following definition instead?
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   817
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   818
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   819
\textbf{inductive} $\textit{even}'$ \textbf{where} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   820
``$\textit{even}'~(0{\Colon}\textit{nat})$'' $\,\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   821
``$\textit{even}'~2$'' $\,\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   822
``$\lbrakk\textit{even}'~m;\> \textit{even}'~n\rbrakk \,\Longrightarrow\, \textit{even}'~(m + n)$''
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   823
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   824
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   825
This definition is not well-founded: From $\textit{even}'~0$ and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   826
$\textit{even}'~0$, we can derive that $\textit{even}'~0$. Nonetheless, the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   827
predicates $\textit{even}$ and $\textit{even}'$ are equivalent.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   828
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   829
Let's check a property involving $\textit{even}'$. To make up for the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   830
foreseeable computational hurdles entailed by non-wellfoundedness, we decrease
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   831
\textit{nat}'s cardinality to a mere 10:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   832
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   833
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   834
\textbf{lemma}~``$\exists n \in \{0, 2, 4, 6, 8\}.\;
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   835
\lnot\;\textit{even}'~n$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   836
\textbf{nitpick}~[\textit{card nat}~= 10,\, \textit{verbose},\, \textit{show\_consts}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   837
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   838
The inductive predicate ``$\textit{even}'\!$'' could not be proved well-founded.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   839
Nitpick might need to unroll it. \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   840
Trying 6 scopes: \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   841
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 0; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   842
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 1; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   843
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   844
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 4; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   845
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 8; \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   846
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 9. \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   847
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
   848
\hbox{}\qquad Constant: \nopagebreak \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   849
\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\unkef(\!\begin{aligned}[t]
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   850
& 0 := \unkef(0 := \textit{True},\, 2 := \textit{True}),\, \\[-2pt]
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   851
& 1 := \unkef(0 := \textit{True},\, 2 := \textit{True},\, 4 := \textit{True}),\, \\[-2pt]
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   852
& 2 := \unkef(0 := \textit{True},\, 2 := \textit{True},\, 4 := \textit{True},\, \\[-2pt]
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   853
& \phantom{2 := \unkef(}6 := \textit{True},\, 8 := \textit{True}))\end{aligned}$ \\[2\smallskipamount]
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   854
Total time: 1.87 s.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   855
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   856
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   857
Nitpick's output is very instructive. First, it tells us that the predicate is
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   858
unrolled, meaning that it is computed iteratively from the empty set. Then it
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   859
lists six scopes specifying different bounds on the numbers of iterations:\ 0,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   860
1, 2, 4, 8, and~9.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   861
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   862
The output also shows how each iteration contributes to $\textit{even}'$. The
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   863
notation $\lambda i.\; \textit{even}'$ indicates that the value of the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   864
predicate depends on an iteration counter. Iteration 0 provides the basis
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   865
elements, $0$ and $2$. Iteration 1 contributes $4$ ($= 2 + 2$). Iteration 2
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   866
throws $6$ ($= 2 + 4 = 4 + 2$) and $8$ ($= 4 + 4$) into the mix. Further
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   867
iterations would not contribute any new elements.
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   868
The predicate $\textit{even}'$ evaluates to either \textit{True} or $\unk$,
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   869
never \textit{False}.
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   870
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   871
%Some values are marked with superscripted question
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   872
%marks~(`\lower.2ex\hbox{$^\Q$}'). These are the elements for which the
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   873
%predicate evaluates to $\unk$.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   874
38181
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
   875
When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, 20, 24, and 28
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   876
iterations. However, these numbers are bounded by the cardinality of the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   877
predicate's domain. With \textit{card~nat}~= 10, no more than 9 iterations are
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   878
ever needed to compute the value of a \textit{nat} predicate. You can specify
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   879
the number of iterations using the \textit{iter} option, as explained in
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   880
\S\ref{scope-of-search}.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   881
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   882
In the next formula, $\textit{even}'$ occurs both positively and negatively:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   883
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   884
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   885
\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
   886
\textbf{nitpick} [\textit{card nat} = 10, \textit{show\_consts}] \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   887
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   888
\hbox{}\qquad Free variable: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   889
\hbox{}\qquad\qquad $n = 1$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   890
\hbox{}\qquad Constants: \nopagebreak \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   891
\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\unkef(\!\begin{aligned}[t]
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   892
& 0 := \unkef(0 := \mathit{True},\, 2 := \mathit{True}))\end{aligned}$  \\
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   893
\hbox{}\qquad\qquad $\textit{even}' \leq \unkef(\!\begin{aligned}[t]
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   894
& 0 := \mathit{True},\, 1 := \mathit{False},\, 2 := \mathit{True},\, \\[-2pt]
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   895
& 4 := \mathit{True},\, 6 := \mathit{True},\, 8 := \mathit{True})\end{aligned}$
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   896
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   897
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   898
Notice the special constraint $\textit{even}' \leq \ldots$ in the output, whose
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   899
right-hand side represents an arbitrary fixed point (not necessarily the least
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   900
one). It is used to falsify $\textit{even}'~n$. In contrast, the unrolled
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   901
predicate is used to satisfy $\textit{even}'~(n - 2)$.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   902
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   903
Coinductive predicates are handled dually. For example:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   904
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   905
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   906
\textbf{coinductive} \textit{nats} \textbf{where} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   907
``$\textit{nats}~(x\Colon\textit{nat}) \,\Longrightarrow\, \textit{nats}~x$'' \\[2\smallskipamount]
46074
3ab55dfd2400 update docs to reflect "Manual_Nits"
blanchet
parents: 45571
diff changeset
   908
\textbf{lemma} ``$\textit{nats} = (\lambda n.\; n \mathbin\in \{0, 1, 2, 3, 4\})$'' \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   909
\textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   910
\slshape Nitpick found a counterexample:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   911
\\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   912
\hbox{}\qquad Constants: \nopagebreak \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   913
\hbox{}\qquad\qquad $\lambda i.\; \textit{nats} = \unkef(0 := \unkef,\, 1 := \unkef,\, 2 := \unkef)$ \\
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   914
\hbox{}\qquad\qquad $\textit{nats} \geq \unkef(3 := \textit{True},\, 4 := \textit{False},\, 5 := \textit{True})$
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   915
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   916
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   917
As a special case, Nitpick uses Kodkod's transitive closure operator to encode
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   918
negative occurrences of non-well-founded ``linear inductive predicates,'' i.e.,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   919
inductive predicates for which each the predicate occurs in at most one
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   920
assumption of each introduction rule. For example:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   921
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   922
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   923
\textbf{inductive} \textit{odd} \textbf{where} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   924
``$\textit{odd}~1$'' $\,\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   925
``$\lbrakk \textit{odd}~m;\>\, \textit{even}~n\rbrakk \,\Longrightarrow\, \textit{odd}~(m + n)$'' \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   926
\textbf{lemma}~``$\textit{odd}~n \,\Longrightarrow\, \textit{odd}~(n - 2)$'' \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   927
\textbf{nitpick}~[\textit{card nat} = 4,\, \textit{show\_consts}] \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   928
\slshape Nitpick found a counterexample:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   929
\\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   930
\hbox{}\qquad Free variable: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   931
\hbox{}\qquad\qquad $n = 1$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   932
\hbox{}\qquad Constants: \nopagebreak \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   933
\hbox{}\qquad\qquad $\textit{even} = (λx. ?)(0 := True, 1 := False, 2 := True, 3 := False)$ \\
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   934
\hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = {}$ \\
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   935
\hbox{}\qquad\qquad\quad $\unkef(0 := \textit{False},\, 1 := \textit{True},\, 2 := \textit{False},\, 3 := \textit{False})$ \\
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   936
\hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \unkef$\\
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   937
\hbox{}\qquad\qquad\quad $(
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   938
\!\begin{aligned}[t]
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   939
& 0 := \unkef(0 := \textit{True},\, 1 := \textit{False},\, 2 := \textit{True},\, 3 := \textit{False}), \\[-2pt]
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   940
& 1 := \unkef(0 := \textit{False},\, 1 := \textit{True},\, 2 := \textit{False},\, 3 := \textit{True}), \\[-2pt]
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   941
& 2 := \unkef(0 := \textit{False},\, 1 := \textit{False},\, 2 := \textit{True},\, 3 := \textit{False}), \\[-2pt]
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   942
& 3 := \unkef(0 := \textit{False},\, 1 := \textit{False},\, 2 := \textit{False},\, 3 := \textit{True}))
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   943
\end{aligned}$ \\
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   944
\hbox{}\qquad\qquad $\textit{odd} \leq \unkef(0 := \textit{False},\, 1 := \textit{True},\, 2 := \textit{False},\, 3 := \textit{True})$
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   945
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   946
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   947
\noindent
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   948
In the output, $\textit{odd}_{\textrm{base}}$ represents the base elements and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   949
$\textit{odd}_{\textrm{step}}$ is a transition relation that computes new
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   950
elements from known ones. The set $\textit{odd}$ consists of all the values
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   951
reachable through the reflexive transitive closure of
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   952
$\textit{odd}_{\textrm{step}}$ starting with any element from
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   953
$\textit{odd}_{\textrm{base}}$, namely 1 and 3. Using Kodkod's
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   954
transitive closure to encode linear predicates is normally either more thorough
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   955
or more efficient than unrolling (depending on the value of \textit{iter}), but
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   956
you can disable it by passing the \textit{dont\_star\_linear\_preds} option.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   957
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   958
\subsection{Coinductive Datatypes}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   959
\label{coinductive-datatypes}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   960
53808
b3e2022530e3 register codatatypes with Nitpick
blanchet
parents: 53803
diff changeset
   961
A coinductive datatype is similar to an inductive datatype but
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   962
allows infinite objects. Thus, the infinite lists $\textit{ps}$ $=$ $[a, a, a,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   963
\ldots]$, $\textit{qs}$ $=$ $[a, b, a, b, \ldots]$, and $\textit{rs}$ $=$ $[0,
53809
2c0e45bb2f05 tuned docs
blanchet
parents: 53808
diff changeset
   964
1, 2, 3, \ldots]$ can be defined as coinductive lists, or ``lazy lists,'' using the
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   965
$\textit{LNil}\mathbin{\Colon}{'}a~\textit{llist}$ and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   966
$\textit{LCons}\mathbin{\Colon}{'}a \mathbin{\Rightarrow} {'}a~\textit{llist}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   967
\mathbin{\Rightarrow} {'}a~\textit{llist}$ constructors.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   968
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   969
Although it is otherwise no friend of infinity, Nitpick can find counterexamples
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   970
involving cyclic lists such as \textit{ps} and \textit{qs} above as well as
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   971
finite lists:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   972
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   973
\prew
53808
b3e2022530e3 register codatatypes with Nitpick
blanchet
parents: 53803
diff changeset
   974
\textbf{codatatype} $'a$ \textit{llist} = \textit{LNil}~$\mid$~\textit{LCons}~$'a$~``$'a\;\textit{llist}$'' \\[2\smallskipamount]
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   975
\textbf{lemma} ``$\textit{xs} \not= \textit{LCons}~a~\textit{xs\/}$'' \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   976
\textbf{nitpick} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   977
\slshape Nitpick found a counterexample for {\itshape card}~$'a$ = 1: \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   978
\hbox{}\qquad Free variables: \nopagebreak \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   979
\hbox{}\qquad\qquad $\textit{a} = a_1$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   980
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   981
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   982
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   983
The notation $\textrm{THE}~\omega.\; \omega = t(\omega)$ stands
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   984
for the infinite term $t(t(t(\ldots)))$. Hence, \textit{xs} is simply the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   985
infinite list $[a_1, a_1, a_1, \ldots]$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   986
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   987
The next example is more interesting:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   988
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   989
\prew
53812
369537953d05 use forthcoming "primcorec" command
blanchet
parents: 53809
diff changeset
   990
\textbf{primcorec}~$\textit{iterates}$~\textbf{where} \\
369537953d05 use forthcoming "primcorec" command
blanchet
parents: 53809
diff changeset
   991
``$\textit{iterates}~f\>a = \textit{LCons}~a~(\textit{iterates}~f\>(f\>a))$'' \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   992
\textbf{lemma}~``$\lbrakk\textit{xs} = \textit{LCons}~a~\textit{xs};\>\,
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   993
\textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys\/}$'' \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   994
\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
   995
\slshape The type $'a$ passed the monotonicity test. Nitpick might be able to skip
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   996
some scopes. \\[2\smallskipamount]
38181
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
   997
Trying 10 scopes: \\
35284
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
   998
\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 1,
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
   999
and \textit{bisim\_depth}~= 0. \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1000
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
38181
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
  1001
\hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 10,
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
  1002
and \textit{bisim\_depth}~= 9. \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1003
Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
  1004
\textit{card}~``\kern1pt$'a~\textit{llist\/}$''~= 2, and \textit{bisim\_\allowbreak
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1005
depth}~= 1:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1006
\\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1007
\hbox{}\qquad Free variables: \nopagebreak \\
35078
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
  1008
\hbox{}\qquad\qquad $\textit{a} = a_1$ \\
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
  1009
\hbox{}\qquad\qquad $\textit{b} = a_2$ \\
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
  1010
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
  1011
\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount]
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
  1012
Total time: 1.11 s.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1013
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1014
35078
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
  1015
The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
  1016
$\textit{ys}$ is $[a_2, a_1, a_1, a_1, \ldots]$, i.e., a lasso-shaped list with
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
  1017
$[a_2]$ as its stem and $[a_1]$ as its cycle. In general, the list segment
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1018
within the scope of the {THE} binder corresponds to the lasso's cycle, whereas
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1019
the segment leading to the binder is the stem.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1020
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1021
A salient property of coinductive datatypes is that two objects are considered
46110
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1022
equal if and only if they lead to the same observations. For example, the two
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1023
lazy lists
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1024
%
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1025
\begin{gather*}
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1026
\textrm{THE}~\omega.\; \omega = \textit{LCons}~a~(\textit{LCons}~b~\omega) \\
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1027
\textit{LCons}~a~(\textrm{THE}~\omega.\; \omega = \textit{LCons}~b~(\textit{LCons}~a~\omega))
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1028
\end{gather*}
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1029
%
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1030
are identical, because both lead
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1031
to the sequence of observations $a$, $b$, $a$, $b$, \hbox{\ldots} (or,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1032
equivalently, both encode the infinite list $[a, b, a, b, \ldots]$). This
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1033
concept of equality for coinductive datatypes is called bisimulation and is
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1034
defined coinductively.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1035
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1036
Internally, Nitpick encodes the coinductive bisimilarity predicate as part of
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1037
the Kodkod problem to ensure that distinct objects lead to different
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1038
observations. This precaution is somewhat expensive and often unnecessary, so it
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1039
can be disabled by setting the \textit{bisim\_depth} option to $-1$. The
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1040
bisimilarity check is then performed \textsl{after} the counterexample has been
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1041
found to ensure correctness. If this after-the-fact check fails, the
35695
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35665
diff changeset
  1042
counterexample is tagged as ``quasi genuine'' and Nitpick recommends to try
46110
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1043
again with \textit{bisim\_depth} set to a nonnegative integer.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1044
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1045
The next formula illustrates the need for bisimilarity (either as a Kodkod
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1046
predicate or as an after-the-fact check) to prevent spurious counterexamples:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1047
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1048
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1049
\textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
  1050
\,\Longrightarrow\, \textit{xs} = \textit{ys\/}$'' \\
55889
6bfbec3dff62 tuned code
blanchet
parents: 55888
diff changeset
  1051
\textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_types}] \\[2\smallskipamount]
35695
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35665
diff changeset
  1052
\slshape Nitpick found a quasi genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1053
\hbox{}\qquad Free variables: \nopagebreak \\
35078
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
  1054
\hbox{}\qquad\qquad $a = a_1$ \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1055
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
35078
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
  1056
\textit{LCons}~a_1~\omega$ \\
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
  1057
\hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
55892
6fba7f6c532a updated docs
blanchet
parents: 55889
diff changeset
  1058
\hbox{}\qquad Type:\strut \nopagebreak \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1059
\hbox{}\qquad\qquad $'a~\textit{llist} =
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1060
\{\!\begin{aligned}[t]
35078
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
  1061
  & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega, \\[-2pt]
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
  1062
  & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega,\> \unr\}\end{aligned}$
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1063
\\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1064
Try again with ``\textit{bisim\_depth}'' set to a nonnegative value to confirm
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1065
that the counterexample is genuine. \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1066
{\upshape\textbf{nitpick}} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1067
\slshape Nitpick found no counterexample.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1068
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1069
45083
014342144091 put CryptoMiniSat first and remove warning about unsoundness now that it has been fixed in Kodkod
blanchet
parents: 45080
diff changeset
  1070
In the first \textbf{nitpick} invocation, the after-the-fact check discovered
46110
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1071
that the two known elements of type $'a~\textit{llist}$ are bisimilar, prompting
53808
b3e2022530e3 register codatatypes with Nitpick
blanchet
parents: 53803
diff changeset
  1072
Nitpick to label the example as only ``quasi genuine.''
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1073
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1074
A compromise between leaving out the bisimilarity predicate from the Kodkod
53808
b3e2022530e3 register codatatypes with Nitpick
blanchet
parents: 53803
diff changeset
  1075
problem and performing the after-the-fact check is to specify a low
b3e2022530e3 register codatatypes with Nitpick
blanchet
parents: 53803
diff changeset
  1076
nonnegative \textit{bisim\_depth} value. In general, a value of $K$ means that
b3e2022530e3 register codatatypes with Nitpick
blanchet
parents: 53803
diff changeset
  1077
Nitpick will require all lists to be distinguished from each other by their
b3e2022530e3 register codatatypes with Nitpick
blanchet
parents: 53803
diff changeset
  1078
prefixes of length $K$. However, setting $K$ to a too low value can
b3e2022530e3 register codatatypes with Nitpick
blanchet
parents: 53803
diff changeset
  1079
overconstrain Nitpick, preventing it from finding any counterexamples.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1080
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1081
\subsection{Boxing}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1082
\label{boxing}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1083
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1084
Nitpick normally maps function and product types directly to the corresponding
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1085
Kodkod concepts. As a consequence, if $'a$ has cardinality 3 and $'b$ has
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1086
cardinality 4, then $'a \times {'}b$ has cardinality 12 ($= 4 \times 3$) and $'a
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1087
\Rightarrow {'}b$ has cardinality 64 ($= 4^3$). In some circumstances, it pays
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1088
off to treat these types in the same way as plain datatypes, by approximating
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1089
them by a subset of a given cardinality. This technique is called ``boxing'' and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1090
is particularly useful for functions passed as arguments to other functions, for
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1091
high-arity functions, and for large tuples. Under the hood, boxing involves
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1092
wrapping occurrences of the types $'a \times {'}b$ and $'a \Rightarrow {'}b$ in
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1093
isomorphic datatypes, as can be seen by enabling the \textit{debug} option.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1094
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1095
To illustrate boxing, we consider a formalization of $\lambda$-terms represented
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1096
using de Bruijn's notation:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1097
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1098
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1099
\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
  1100
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1101
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1102
The $\textit{lift}~t~k$ function increments all variables with indices greater
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1103
than or equal to $k$ by one:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1104
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1105
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1106
\textbf{primrec} \textit{lift} \textbf{where} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1107
``$\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
  1108
``$\textit{lift}~(\textit{Lam}~t)~k = \textit{Lam}~(\textit{lift}~t~(k + 1))$'' $\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1109
``$\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
  1110
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1111
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1112
The $\textit{loose}~t~k$ predicate returns \textit{True} if and only if
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1113
term $t$ has a loose variable with index $k$ or more:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1114
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1115
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1116
\textbf{primrec}~\textit{loose} \textbf{where} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1117
``$\textit{loose}~(\textit{Var}~j)~k = (j \ge k)$'' $\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1118
``$\textit{loose}~(\textit{Lam}~t)~k = \textit{loose}~t~(\textit{Suc}~k)$'' $\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1119
``$\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
  1120
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1121
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1122
Next, the $\textit{subst}~\sigma~t$ function applies the substitution $\sigma$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1123
on $t$:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1124
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1125
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1126
\textbf{primrec}~\textit{subst} \textbf{where} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1127
``$\textit{subst}~\sigma~(\textit{Var}~j) = \sigma~j$'' $\mid$ \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1128
``$\textit{subst}~\sigma~(\textit{Lam}~t) = {}$\phantom{''} \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1129
\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
  1130
``$\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
  1131
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1132
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1133
A substitution is a function that maps variable indices to terms. Observe that
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1134
$\sigma$ is a function passed as argument and that Nitpick can't optimize it
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1135
away, because the recursive call for the \textit{Lam} case involves an altered
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1136
version. Also notice the \textit{lift} call, which increments the variable
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1137
indices when moving under a \textit{Lam}.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1138
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1139
A reasonable property to expect of substitution is that it should leave closed
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1140
terms unchanged. Alas, even this simple property does not hold:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1141
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1142
\pre
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1143
\textbf{lemma}~``$\lnot\,\textit{loose}~t~0 \,\Longrightarrow\, \textit{subst}~\sigma~t = t$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1144
\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1145
\slshape
38181
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
  1146
Trying 10 scopes: \nopagebreak \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
  1147
\hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm\/}$'' = 1; \\
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
  1148
\hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm\/}$'' = 2; \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1149
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
  1150
\hbox{}\qquad \textit{card~nat}~= 10, \textit{card tm}~= 10, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm\/}$'' = 10. \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1151
Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6,
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
  1152
and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm\/}$''~= 6: \\[2\smallskipamount]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1153
\hbox{}\qquad Free variables: \nopagebreak \\
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
  1154
\hbox{}\qquad\qquad $\sigma = \unkef(\!\begin{aligned}[t]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1155
& 0 := \textit{Var}~0,\>
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1156
  1 := \textit{Var}~0,\>
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1157
  2 := \textit{Var}~0, \\[-2pt]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1158
& 3 := \textit{Var}~0,\>
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1159
  4 := \textit{Var}~0,\>
46110
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1160
  5 := \textit{Lam}~(\textit{Lam}~(\textit{Var}~0)))\end{aligned}$ \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1161
\hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount]
46110
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1162
Total time: 3.08 s.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1163
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1164
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1165
Using \textit{eval}, we find out that $\textit{subst}~\sigma~t =
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1166
\textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional
46110
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1167
$\lambda$-calculus notation, $t$ is
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1168
$\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is (wrongly) $\lambda x\, y.\> y$.
35284
9edc2bd6d2bd enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents: 35220
diff changeset
  1169
The bug is in \textit{subst\/}: The $\textit{lift}~(\sigma~m)~1$ call should be
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1170
replaced with $\textit{lift}~(\sigma~m)~0$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1171
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1172
An interesting aspect of Nitpick's verbose output is that it assigned inceasing
46110
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1173
cardinalities from 1 to 10 to the type $\textit{nat} \Rightarrow \textit{tm}$
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1174
of the higher-order argument $\sigma$ of \textit{subst}.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1175
For the formula of interest, knowing 6 values of that type was enough to find
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
  1176
the counterexample. Without boxing, $6^6 = 46\,656$ values must be
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1177
considered, a hopeless undertaking:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1178
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1179
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1180
\textbf{nitpick} [\textit{dont\_box}] \\[2\smallskipamount]
38183
e3bb14be0931 updated example timings
blanchet
parents: 38181
diff changeset
  1181
{\slshape Nitpick ran out of time after checking 3 of 10 scopes.}
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1182
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1183
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1184
Boxing can be enabled or disabled globally or on a per-type basis using the
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35386
diff changeset
  1185
\textit{box} option. Nitpick usually performs reasonable choices about which
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
  1186
types should be boxed, but option tweaking sometimes helps.
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
  1187
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
  1188
%A related optimization,
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
  1189
%``finitization,'' attempts to wrap functions that are constant at all but finitely
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
  1190
%many points (e.g., finite sets); see the documentation for the \textit{finitize}
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
  1191
%option in \S\ref{scope-of-search} for details.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1192
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1193
\subsection{Scope Monotonicity}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1194
\label{scope-monotonicity}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1195
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1196
The \textit{card} option (together with \textit{iter}, \textit{bisim\_depth},
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1197
and \textit{max}) controls which scopes are actually tested. In general, to
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1198
exhaust all models below a certain cardinality bound, the number of scopes that
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1199
Nitpick must consider increases exponentially with the number of type variables
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1200
(and \textbf{typedecl}'d types) occurring in the formula. Given the default
38181
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
  1201
cardinality specification of 1--10, no fewer than $10^4 = 10\,000$ scopes must be
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1202
considered for a formula involving $'a$, $'b$, $'c$, and $'d$.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1203
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1204
Fortunately, many formulas exhibit a property called \textsl{scope
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1205
monotonicity}, meaning that if the formula is falsifiable for a given scope,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1206
it is also falsifiable for all larger scopes \cite[p.~165]{jackson-2006}.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1207
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1208
Consider the formula
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1209
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1210
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1211
\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
  1212
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1213
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1214
where \textit{xs} is of type $'a~\textit{list}$ and \textit{ys} is of type
38181
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
  1215
$'b~\textit{list}$. A priori, Nitpick would need to consider $1\,000$ scopes to
38274
8672d106623c minor doc changes
blanchet
parents: 38241
diff changeset
  1216
exhaust the specification \textit{card}~= 1--10 (10 cardinalies for $'a$
8672d106623c minor doc changes
blanchet
parents: 38241
diff changeset
  1217
$\times$ 10 cardinalities for $'b$ $\times$ 10 cardinalities for the datatypes).
8672d106623c minor doc changes
blanchet
parents: 38241
diff changeset
  1218
However, our intuition tells us that any counterexample found with a small scope
8672d106623c minor doc changes
blanchet
parents: 38241
diff changeset
  1219
would still be a counterexample in a larger scope---by simply ignoring the fresh
8672d106623c minor doc changes
blanchet
parents: 38241
diff changeset
  1220
$'a$ and $'b$ values provided by the larger scope. Nitpick comes to the same
8672d106623c minor doc changes
blanchet
parents: 38241
diff changeset
  1221
conclusion after a careful inspection of the formula and the relevant
8672d106623c minor doc changes
blanchet
parents: 38241
diff changeset
  1222
definitions:
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1223
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1224
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1225
\textbf{nitpick}~[\textit{verbose}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1226
\slshape
46105
9abb756352a6 updated Nitpick docs after "set" reintroduction
blanchet
parents: 46074
diff changeset
  1227
The types $'a$ and $'b$ passed the monotonicity test.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1228
Nitpick might be able to skip some scopes.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1229
 \\[2\smallskipamount]
38181
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
  1230
Trying 10 scopes: \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1231
\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1232
\textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$
35712
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
  1233
\textit{list\/}''~= 1, \\
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
  1234
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 1, and
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
  1235
\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 1. \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1236
\hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1237
\textit{card} \textit{nat}~= 2, \textit{card} ``$('a \times {'}b)$
35712
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
  1238
\textit{list\/}''~= 2, \\
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
  1239
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 2, and
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
  1240
\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 2. \\
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1241
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
38181
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
  1242
\hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} $'b$~= 10,
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
  1243
\textit{card} \textit{nat}~= 10, \textit{card} ``$('a \times {'}b)$
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
  1244
\textit{list\/}''~= 10, \\
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
  1245
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 10, and
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
  1246
\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 10.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1247
\\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1248
Nitpick found a counterexample for
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1249
\textit{card} $'a$~= 5, \textit{card} $'b$~= 5,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1250
\textit{card} \textit{nat}~= 5, \textit{card} ``$('a \times {'}b)$
35712
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
  1251
\textit{list\/}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 5, and
77aa29bf14ee added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents: 35710
diff changeset
  1252
\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 5:
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1253
\\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1254
\hbox{}\qquad Free variables: \nopagebreak \\
35078
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
  1255
\hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\
6fd1052fe463 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents: 35072
diff changeset
  1256
\hbox{}\qquad\qquad $\textit{ys} = [b_1, b_1]$ \\[2\smallskipamount]
40341
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 40147
diff changeset
  1257
Total time: 1.63 s.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1258
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1259
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1260
In theory, it should be sufficient to test a single scope:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1261
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1262
\prew
38181
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
  1263
\textbf{nitpick}~[\textit{card}~= 10]
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1264
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1265
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1266
However, this is often less efficient in practice and may lead to overly complex
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1267
counterexamples.
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1268
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1269
If the monotonicity check fails but we believe that the formula is monotonic (or
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1270
we don't mind missing some counterexamples), we can pass the
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1271
\textit{mono} option. To convince yourself that this option is risky,
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1272
simply consider this example from \S\ref{skolemization}:
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1273
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1274
\prew
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1275
\textbf{lemma} ``$\exists g.\; \forall x\Colon 'b.~g~(f~x) = x
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1276
 \,\Longrightarrow\, \forall y\Colon {'}a.\; \exists x.~y = f~x$'' \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1277
\textbf{nitpick} [\textit{mono}] \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1278
{\slshape Nitpick found no counterexample.} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1279
\textbf{nitpick} \\[2\smallskipamount]
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1280
\slshape
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1281
Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1282
\hbox{}\qquad $\vdots$
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1283
\postw
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1284
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1285
(It turns out the formula holds if and only if $\textit{card}~'a \le
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1286
\textit{card}~'b$.) Although this is rarely advisable, the automatic
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1287
monotonicity checks can be disabled by passing \textit{non\_mono}
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1288
(\S\ref{optimizations}).
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1289
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1290
As insinuated in \S\ref{natural-numbers-and-integers} and
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1291
\S\ref{inductive-datatypes}, \textit{nat}, \textit{int}, and inductive datatypes
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1292
are normally monotonic and treated as such. The same is true for record types,
38274
8672d106623c minor doc changes
blanchet
parents: 38241
diff changeset
  1293
\textit{rat}, and \textit{real}. Thus, given the
38181
6f9f80afaf4f also mention gfp
blanchet
parents: 38178
diff changeset
  1294
cardinality specification 1--10, a formula involving \textit{nat}, \textit{int},
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1295
\textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
46110
22294c79cea6 more Nitpick doc updates
blanchet
parents: 46105
diff changeset
  1296
consider only 10~scopes instead of $10^4 = 10\,000$. On the other hand,
38274
8672d106623c minor doc changes
blanchet
parents: 38241
diff changeset
  1297
\textbf{typedef}s and quotient types are generally nonmonotonic.
33191
fe3c65d9c577 Added Nitpick manual.
blanchet
parents:
diff changeset
  1298
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
  1299
\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
  1300
\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
  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
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
  1303
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
  1304
%
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
\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
  1306
\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
  1307
\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
  1308
\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
  1309
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
  1310
\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
  1311
%
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
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
  1313
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
  1314
%
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
\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
  1316
\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
  1317
\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
  1318
\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
  1319
\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
  1320
%
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
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
  1322
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
  1323
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
  1324
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
  1325
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
  1326
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
\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
  1328
\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
  1329
``$(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
  1330
``$\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
  1331
``$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
  1332
\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
  1333
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
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
  1335
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
\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
  1337
\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
  1338
\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
  1339
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
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
  1341
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
  1342
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
\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
  1344
\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
  1345
\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
  1346
\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
  1347
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
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
  1349
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
\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
  1351
{\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
  1352
\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
  1353
\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
  1354
}
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
\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
  1356
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
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
  1358
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
  1359
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
  1360
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
  1361
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
  1362
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
\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
  1364
\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
  1365
\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
  1366
\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
  1367
\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
  1368
\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
  1369
\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
  1370
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
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
  1372
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
  1373
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
\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
  1375
\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
  1376
\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