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