1\documentclass[a4paper,12pt,DIV=12,oneside]{scrbook} 2 3\usepackage{amsthm} 4\usepackage{palatino} 5\usepackage{amssymb} 6\usepackage{amsmath} 7\usepackage[sort&compress]{natbib} 8\usepackage{hyperref} 9\usepackage{lmodern} 10\usepackage{tabularx} 11\usepackage{booktabs} 12\newcommand{\tablehead}[1]{\addlinespace\multicolumn{2}{l}{\textit{#1}}\\} 13 14\let\vec\relax 15\DeclareMathAccent{\vec}{\mathord}{letters}{"7E} 16 17\usepackage{accents} 18 19\newcommand{\HOL}{{HOL}} 20\newcommand{\fv}{\textit{fv}} 21 22\newtheorem{lemma}{Lemma}[section] 23\newtheorem{theorem}[lemma]{Theorem} 24 25\theoremstyle{definition} 26\newtheorem{definition}[lemma]{Definition} 27\newtheorem{example}[lemma]{Example} 28 29\theoremstyle{remark} 30\newtheorem{remark}[lemma]{Remark} 31 32\newcommand{\GE}{\ensuremath{G_\exists}} 33\newcommand{\GEP}{\ensuremath{G_{\accentset{\bullet}{\exists}}}} 34\newcommand{\GEG}{\ensuremath{G_{\accentset{\_\,\_}{\exists}}}} 35\newcommand{\GU}{\ensuremath{G_\forall}} 36\newcommand{\GUP}{\ensuremath{G_{\accentset{\bullet}{\forall}}}} 37\newcommand{\GUG}{\ensuremath{G_{\accentset{\_\,\_}{\forall}}}} 38\newcommand{\GO}{\ensuremath{G_{?}}} 39 40\pagestyle{plain} 41 42%------------------------------------------------------------------------------------------ 43% The title page 44%------------------------------------------------------------------------------------------ 45 46\begin{document} 47 48\title{Quantifier Heuristics Library} 49\author{Thomas Tuerk} 50 51\maketitle 52 53\tableofcontents 54 55\chapter{Introduction} 56\section{Motivation} 57\label{sec_motivation} 58 59In interactive proofs it is often useful to be able to find instantiations 60for quantifiers. The unwind library\footnote{see \texttt{src/simp/src/Unwind.sml}} allows 61instantiations of ``trivial'' quantifiers: 62 63\[ \forall x_1\ \ldots x_i \ldots x_n.\ P_1 \wedge \ldots \wedge x_i = c \wedge \ldots \wedge P_n \Longrightarrow Q \] 64and 65\[ \exists x_1\ \ldots x_i \ldots x_n.\ P_1 \wedge \ldots \wedge x_i = 66c \wedge \ldots \wedge P_n \] can be simplified by 67instantiating $x_i$ with $c$. Because unwind-conversions are 68part of \texttt{bool\_ss}, they are used with nearly every call of the simplifier 69and often simplify proofs considerably. However, the unwind library can only handle these common cases. If the term structure is 70only slightly more complicated, it fails. For example, $\exists x.\ P(a) \Longrightarrow (x = 2) \wedge Q(x)$ 71cannot be tackled. 72 73There is also the satisfy library\footnote{see \texttt{src/simp/src/Satisfy.sml}}, which uses unification to 74show existentially quantified formulas. It can handle problems like 75$\exists x.\ P_1(x,c_1)\ \wedge \ldots P_n(x,c_n)$ if given 76theorems of the form $\forall x\ c.\ P_i(x, c)$. This is often handy, but still rather limited. 77 78The quantifier heuristics library\footnote{see 79 \texttt{src/quantHeur/quantHeuristicsLib.sml}} provides more power 80and flexibility. It can handle all the examples that the unwind and 81satisfy libraries can handle. A few simple examples of what it can do 82are shown in Table~\ref{table_examples}. Besides the power demonstrated 83by these examples, the library is highly flexible as well. At it's 84core, there is a modular, syntax driven search for instantiation. 85This search consists of a collection of interleaved heuristics. Users 86can easily configure existing heuristics and add own ones. Thereby, it 87is easy to teach the library about new predicates, logical connectives 88or datatypes. 89 90\begin{table}[h] 91\centering\scriptsize 92\begin{tabularx}{\textwidth}{lll}\toprule 93\textbf{Problem} & \textbf{Result} \\\midrule 94 95\tablehead{basic examples} 96$\exists x.\ x = 2 \wedge P (x)$ & $P(2)$ \\ 97$\forall x.\ x = 2 \Longrightarrow P (x)$ & $P(2)$ \\ 98 99\tablehead{solutions and counterexamples} 100$\exists x.\ x = 2$ & $\textit{true}$ \\ 101$\forall x.\ x = 2$ & $\textit{false}$ \\ 102 103\tablehead{complicated nestings of standard operators} 104$\exists x_1. \forall x_2.\ (x_1 = 2) \wedge P(x_1, x_2)$ & 105$\forall x_2.\ P(2, x_2)$ \\ 106 107$\exists x_1, x_2.\ P_1(x_2) \Longrightarrow (x_1 = 2) \wedge P(x_1, x_2)$ & 108$\exists x_2.\ P_1(x_2) \Longrightarrow P(2, x_2)$ \\ 109$\exists x.\ ((x = 2) \vee (2 = x)) \wedge P(x)$ & $P(2)$ \\ 110 111\tablehead{exploiting unification} 112$\exists x.\ (f (8 + 2) = f (x + 2)) \wedge P (f(10))$ & $P (f(10))$ \\ 113$\exists x.\ (f (8 + 2) = f (x + 2)) \wedge P (f(x + 2))$ & $P (f(8 + 2))$ \\ 114$\exists x.\ (f (8 + 2) = f (x + 2)) \wedge P (f(x))$ & - (\text{no instantiation found}) \\ 115 116\tablehead{partial instantiation for datatypes} 117$\forall p.\ c = \textsf{FST}(p) \Longrightarrow P(p)$ & $\forall p_2.\ P(c, p_2)$ \\ 118 119$\forall x.\ \textsf{IS\_NONE}(x) \vee P(x)$ & $\forall x'.\ P (\textsf{SOME}(x'))$ \\ 120 121$\forall l.\ l \neq [\,] \Longrightarrow P(l)$ & $\forall \textit{hd}, \textit{tl}.\ 122P(\textit{hd} :: \textit{tl})$ \\ 123 124\tablehead{context} 125$P_1(c) \Longrightarrow \exists x.\ P_1(x) \vee P_2(x)$ & \textit{true} \\ 126$P_1(c) \Longrightarrow \forall x.\ \neg P_1(x) \wedge P_2(x)$ & $\neg P_1(c)$ \\ 127 128$(\forall x.\ P_1(x) \Rightarrow (x = 2)) \Longrightarrow (\forall x.\ P_1(x) \Rightarrow P_2(x))$ & 129$(\forall x.\ P_1(x) \Rightarrow (x = 2)) \Rightarrow (P_1(2) \Rightarrow P_2(2))$ \\ 130 131$\big((\forall x.\ P_1(x) \Rightarrow P_2(x)) \wedge P_1(2)\big) \Longrightarrow \exists x.\ P_2(x)$ & 132\textit{true} \\ 133\bottomrule 134\end{tabularx} 135\caption{Examples} 136\label{table_examples} 137\end{table} 138 139\section{Structure} 140 141This presentation of the quantifier heuristics library is structured into two parts. 142The first part presents the logical foundations, whereas the second part presents the HOL~4 interface. 143Readers not interested in the foundations, might skip the first part. 144 145The first part starts with an introduction of the concept of guesses in Section~\ref{sec_guesses}. Then, 146Section \ref{sec_base_guesses} shows how guesses can be derived for interesting terms like equations. 147These guesses form the base cases of the search for instantiations. Then, Section \ref{sec_lifting_guesses} 148discusses how these guesses are lifted over the term structure. Other concepts used for the search 149are discussed in Section~\ref{sec_other_techniques}. In order to illustrate 150this abstract presentation, Section~\ref{sec_examples} shows how 151guess-search works for simple examples. 152 153The second part starts with a high level presentation of the user-interface in 154Section~\ref{sec_interface}. An important concept of the interface are 155quantifier heuristic parameters, which allow configuring the behaviour of the library. 156In Section~\ref{sec_qps} first predefined parameters are presented. 157Then it is demonstrated using concrete examples, how own parameters can be developed. 158 159The presentation closes with a short conclusion. 160 161 162\chapter{Theoretical Foundations} 163 164\section{Guesses}\label{sec_guesses} 165 166\subsection{Weak Guesses for Existential Quantifiers} 167 168In the introduction, it is stated that the core component of this work 169is a search based on heuristics. Abstractly, given a term $\exists x.\ 170P(x)$ we want to find an instantiation $\lambda \fv. i(\fv)$ such that 171$\exists x.\ P(x) \Longleftrightarrow \exists \fv.\ P(i(\fv))$ 172holds. In the following, such an $i$ is called a \emph{guess} for 173variable $x$ in $P(x)$. In order to justify such a guess, we define 174special predicates that capture the intended semantics. 175 176\begin{definition}[Existential Guess] 177 $i$ is an \emph{existential guess} for $P$ (denoted by $\GE(i, P)$) 178 if and only if the equivalence $\exists x.\ P(x) \Longleftrightarrow 179 \exists \fv.\ P(i(\fv))$ holds. 180\end{definition} 181 182\begin{example} 183$\GE(K\ 2, \lambda x.\ x = 2)$ holds, because $\exists x.\ x = 2 184\Longleftrightarrow 2 = 2$ holds. More interestingly, 185$\GE(\lambda(x, xs').\ x::xs'), \lambda xs.\ xs \neq [] \wedge P(xs))$ 186holds. Therefore, $\exists xs.\ xs \neq []\ \wedge\ P(xs)$ can be simplified 187to $\exists x\ xs'.\ x::xs' \neq []\ \wedge\ P(x::xs')$. 188\end{example} 189 190So, when trying to process $\exists x.\ P(x)$, we search 191for an existential guess $i$ such that $\GE(i, \lambda x. P(x))$ 192holds. If such a guess is found, the original term can be simplified to 193$\exists \fv.\ P(i(\fv))$, which is really \emph{simpler} provided sensible heuristics for creating 194guesses are used. In particular, guesses $i$ that do not depend on $\fv$ frequently occur in practice. 195The quantifier disappears completely in this common case. 196 197\subsection{Strong Guesses for Existential Quantifiers} 198 199The general idea for coming up with a guess $\GE(i, P)$ is preforming 200a bottom-up search of the syntax tree of $P$. Unluckily, $\GE$ is 201not well suited for such a search, because it is too weak to easily lift 202guesses for subterms. Consider, for example, terms of the form 203$\exists x.\ P_1(x) \vee P_2(x)$. If we have a guess $\GE(i, P_1)$, we unluckily can't lift it 204to a guess $\GE(i, \lambda x.\ P_1(x) \vee P_2(x))$ in general. A counterexample 205is $P_1(x) := \textit{false}$, $P_2(x) := (x = 2)$ and $i := K\ 3 = \lambda \fv.\ 3$. 206Therefore, stronger types of guesses are introduced that work well with lifting: 207 208\begin{definition}[Point Existenstial Guess] 209$i$ is a \emph{point existential guess} for $P$ (denoted by $\GEP(i, P)$) if and only if $\forall \fv.\ P(i(\fv))$ holds. 210\end{definition} 211 212\begin{example} 213 $\GEP(K\ 2, \lambda x.\ x=2)$ holds, because $2=2$ holds. In 214 addition to weak existential guesses $\GE(i,P)$, point existential 215 guesses $\GEP(i,P)$ carry information about the point $i$: the point 216 $i$ satisfies $P$. For example $\GEP(\lambda (x,xs').\ x::xs',\ \lambda 217 xs.\ xs \neq [])$ means that $\lambda xs.\ xs \neq []$ holds for all 218 points of the form $x :: xs'$ (for arbitrary $x$, $xs'$). 219\end{example} 220 221 222\begin{definition}[Gap Existential Guess] 223 $i$ is a \emph{gap existential guess} for $P$ (denoted by $\GEG(i, P)$) 224 if and only if $\forall v.\ \big(\big(\forall \fv.\ v \neq 225 i(\fv)\big) \Longrightarrow \neg P(v)\big)$ holds. 226\end{definition} 227 228\begin{example} 229In addition to weak existential guesses $\GE(i,P)$, gap existential 230guesses $\GEG(i,P)$ carry information about all points except the gap $i$. 231The guess $\GEG(K\ 2, \lambda x.\ x = 2\ \wedge\ Q(x))$ holds, because $\lambda x.\ (x = 2)\ \wedge\ Q(x)$ 232does not hold for all values except possibly $2$. Since nothing is known about $Q$, we don't know, 233whether $P$ holds for the point $2$. This point is a gap in the argument. 234\end{example} 235 236\noindent 237Point and gap existential guesses are stronger than existential 238guesses, i.\,e.\ $\GEP(i, P)$ and $\GEG(i, P)$ imply $\GE(i, P)$ for 239all $i$, $P$. Therefore, they can also be used to instantiate 240existential quantifiers. Moreover, they allow lifting. For example, 241the rule $\GEP(i, P_1) \Longrightarrow \GEP(i, \lambda x.\ P_1(x) \vee 242P_2(x))$ holds. 243 244\subsection{Guesses for Universal Quantifiers} 245 246Existential and universal quantification are closely related to each 247other by negation. In order to lift guesses over negation and also in 248order to be able to instantiate universal quantifiers, it makes sense 249to define corresponding guesses for universal quantification 250exploiting this duality. 251 252\begin{definition}[Universal Guess] 253 $i$ is an \emph{universal guess} for $P$ (denoted by $\GU(i, P)$) 254 if and only if the equivalence $\forall x.\ P(x) \Longleftrightarrow 255 \forall \fv.\ P(i(\fv))$ holds. 256\end{definition} 257 258\begin{definition}[Point Universal Guess] 259$i$ is a \emph{point universal guess} for $P$ (denoted by $\GUP(i, P)$) if and only if $\forall \fv.\ \neg\ P(i(\fv))$ holds. 260\end{definition} 261 262\begin{definition}[Gap Universal Guess] 263 $i$ is a \emph{gap universal guess} for $P$ (denoted by $\GUG(i, 264 P)$) if and only if $\forall v.\ \big(\big(\forall \fv.\ v \neq 265 i(\fv)\big) \Longrightarrow P(v)\big)$ holds. 266\end{definition} 267 268Similar to guesses for existential quantification, we are mainly interested in weak universal guesses. Point and gap 269universal guesses are stronger than universal ones and allow lifting. 270 271 272\subsection{Overview} 273 274Above, 6 types of guesses are formally introduced. Informally, they can be described by the following table: 275% 276\begin{center} 277\begin{tabular}{cc@{\quad}|@{\quad}l} 278\textbf{$i$ is a $\ldots$ guess for $P$} & & \textbf{intuition} \\\hline 279(weak) existential & ($\GE$) & $\exists x.\ P(x)$ can be safely instantiated with $i$ \\ 280(weak) universal & ($\GU$) & $\forall x.\ P(x)$ can be safely instantiated with $i$ \\ 281point existential & ($\GEP$) & $P(i)$ holds \\ 282point universal & ($\GUP$) & $\neg P(i)$ holds \\ 283gap existential & ($\GEG$) & all $v$ except possibly $i$ do not satisfy $P$\\ 284gap universal & ($\GUG$) & all $v$ except possibly $i$ satisfy $P$\\ 285\end{tabular} 286\end{center} 287% 288This informal description also shows the relative strength of these guesses. 289% 290\begin{lemma}[Strength of Guesses]\label{lemma_guesses_strength}% 291Point and gap guesses are stronger than weak guesses. This means that the following 292implications hold for all $i$ and $P$: 293\[ 294\begin{array}{rcl@{\qquad}rcl} 295 \GEG(i, P) & \Longrightarrow & \GE(i, P) & 296 \GEP(i, P) & \Longrightarrow & \GE(i, P) \\ 297 \GUG(i, P) & \Longrightarrow & \GU(i, P) & 298 \GUP(i, P) & \Longrightarrow & \GU(i, P) 299\end{array} 300\] 301\noindent 302Point and gap guesses cannot be compared to each other in general. 303\end{lemma} 304 305So, the core of the framework searches for guesses. Once found, the guesses are used as described by the following theorem: 306 307\begin{theorem}[Usage of Guesses]\label{lemma_guesses_usage} 308Guesses are used to simplify formulae with quantifiers in various ways. In the most basic case, they can 309be used to (partially) instantiate quantifiers as follows: 310\[% 311\begin{array}[t]{cccrclc} 312 \GE(i, P) & \Longrightarrow & \Big( & \exists x.\ P(x) & \Leftrightarrow & \exists \fv.\ P(i(\fv)) & \Big) \\ 313 \GU(i, P) & \Longrightarrow & \Big( & \forall x.\ P(x) & \Leftrightarrow & \forall \fv.\ P(i(\fv)) & \Big) \\ 314\end{array} 315\] 316% 317If the guess does not depend on a free variable (as denoted by $K\ i_c$), the quantifier can be removed completely: 318\[ 319\begin{array}[t]{cccrclc} 320 \GE(K\ i_c, P) & \Longrightarrow & \Big( & \exists x.\ P(x) & \Leftrightarrow & P(i_c) & \Big) \\ 321 \GU(K\ i_c, P) & \Longrightarrow & \Big( & \forall x.\ P(x) & \Leftrightarrow & P(i_c) & \Big) \\ 322\end{array} 323\] 324Point guesses lead to even more simplification: 325\[ 326\begin{array}[t]{cccrclc} 327 \GEP(i, P) & \Longrightarrow & \Big( & \exists x.\ P(x) & \Leftrightarrow & \textit{true} & \Big) \\ 328 \GUP(i, P) & \Longrightarrow & \Big( & \forall x.\ P(x) & \Leftrightarrow & \textit{false} & \Big) \\ 329\end{array} 330\] 331In contrast, the additional strength of gap guesses 332is mainly important for lifting. For instantiating quantifiers the same rules as for 333existential and universal guesses apply. 334However, gap existential guesses are useful for handling unique existential quantification, provided 335the guess does not contain free variables. 336\[ 337\begin{array}[t]{cccrclc} 338 \GE(K\ i_c, P) & \Longrightarrow & \Big( & \exists! x.\ P(x) & \Leftrightarrow & 339 (P(i_c)\ \wedge\ \forall v.\ P(v) \Rightarrow v = i_c) & \Big) \\ 340 \GEG(K\ i_c, P) & \Longrightarrow & \Big( & \exists! x.\ P(x) & \Leftrightarrow & 341 P(i_c) & \Big) \\ 342 \GEP(K\ i_c, P) & \Longrightarrow & \Big( & \exists! x.\ P(x) & \Leftrightarrow & 343 (\forall v.\ P(v) \Rightarrow v = i_c) & \Big) 344\end{array} 345\] 346\end{theorem} 347 348 349\subsection{Oracle Guesses} 350 351So far, we discussed guesses that carry semantic information and allow 352proving equivalences. These are the ones interesting from a theoretical point of view. 353For implementing an actual tool, guesses without justification are interesting as well. 354The HOL~4 implementation supports also \emph{oracle guesses}. 355\begin{definition}[Oracle Guess] 356 $i$ is an \emph{oracle guess} for $P$ (denoted by $\GO(i, 357 P)$) if the user says so. This means that $\GO(i, P)$ holds for all $i$ and $P$. 358\end{definition} 359% 360An oracle guess carries no semantic information, it just states something 361like ``\textit{Trust me! This is a sensible guess!}''. Therefore, oracle 362guesses can only be used to prove implications instead of 363equivalences. 364% 365\begin{lemma}[Usage of Oracle Guesses] 366\[ 367\begin{array}[t]{cccrclc} 368 \GO(i, P) & \Longrightarrow & \Big( & \exists x.\ P(x) & \Leftarrow & \exists \fv.\ P(i(\fv)) & \Big) \\ 369 \GO(i, P) & \Longrightarrow & \Big( & \forall x.\ P(x) & \Rightarrow & \forall \fv.\ P(i(\fv)) & \Big) 370\end{array} 371\] 372\end{lemma} 373% 374Oracle guesses allow the user to instantiate quantifiers without formal justification. 375Therefore, they require hardly any theoretical foundation and 376are mainly interesting for tool implementation. Therefore, they won't be discussed much below. 377 378\section{Base Guesses} 379\label{sec_base_guesses} 380After introducing guesses, guess-search can be presented now. 381This presentation is twofold. In this section, guesses for basic terms are discussed. Lifting guesses 382is presented in the next section. 383 384\subsection{Equations} 385The most basic, but also most common source of guesses are equations: 386 387\begin{lemma}[Guesses for Equations with Variables at Top-Level]\label{lemma_guesses_equation_top} 388Given an equation $x = t$ such that the variable $x$ 389does not occur in $t$, the term $t$ is both a point and gap existential guess for 390$x$: 391\[% 392\begin{array}{ccc} 393\GEP(K\ t,\ \lambda x.\ (x = t)) & \qquad\qquad & \GEG(K\ t,\ \lambda x.\ (x = t)) \\ 394\end{array} 395\] 396\end{lemma} 397% 398\begin{lemma}[Point Existential Guesses for Equations]\label{lemma_guesses_equation_T} 399Given an equation $t_1(x) = t_2(x)$ and a term $i_c$ such that 400the formula $t_1(i_c) = t_2(i_c)$ holds, the term $i_c$ is a point existential guess for 401$x$. This means that the following holds. 402\[ 403t_1(i_c) = t_2(i_c) \Longrightarrow 404\GEP(K\ i_c,\ \lambda x.\ (t_1(x) = t_2(x))) 405\] 406\end{lemma} 407\noindent 408Therefore, unification can be used to find point existential guesses for equations. 409 410 411\subsection{Dichotomies}\label{subsec_base_guesses_dichotomies} 412Many datatype definitions provide dichotomy theorems of the form 413\[ 414 \forall x.\ x = c_1\ \vee\ (\exists \fv.\ x = c_2(\fv)) \qquad \text{and} \qquad 415 \forall \fv.\ c_1\ \neq c_2(\fv) 416\] 417The option- and list-datatypes of HOL~4, for example, provide the following theorems: 418\[ 419\begin{array}{ccc} 420 \forall x.\ x = \textsf{NONE}\ \vee\ (\exists v.\ x = \textsf{SOME}(v)) & \qquad \qquad & 421 \forall v.\ \textsf{NONE} \neq \textsf{SOME}(v) \\ 422 423 \forall x.\ x = [\,]\ \vee\ (\exists \textit{hd}, \textit{tl}.\ x = \textit{hd}::\textit{tl}) & & 424 \forall \textit{hd}, \textit{tl}.\ [\,] \neq \textit{hd}::\textit{tl} 425\end{array} 426\] 427% 428Such theorems can be exploited for creating guesses: 429\begin{lemma}[Dichotomy Guesses]\label{lemma_guesses_dichotomy} 430\[ 431\begin{array}{l@{\quad}l@{\quad}l} 432(\forall \fv.\ c_1 \neq c_2(\fv)) & \Longrightarrow & 433\GUP(\lambda \fv.\ c_2(\fv),\ \lambda x.\ (x = c_1)) \\ 434 435(\forall x.\ x = c_1\ \vee\ (\exists \fv.\ x = c_2(\fv))) & \Longrightarrow & 436\GUG(\lambda \fv.\ c_2(\fv),\ \lambda x.\ (x = c_1)) 437\end{array} 438\] 439\end{lemma} 440% 441Exploiting dichotomy is very useful in practice. Holfoot uses it to reason about lists. 442The variable \textit{pdata'} in the list-reversal example of the introduction can, for example, 443be instantiated using the dichotomy of lists. Without this rule, Holfoot's inference rules for 444singly-linked list predicates would need to unfold the data-content manually. 445 446Many other datatypes unluckily have more than just two 447cases. Currently, general $n$-chotomies cannot be exploited, because 448this would require an extension of the guess concept. However, 449monochotomies can be handled. 450 451\subsection{Monochotomies} 452Datatypes like pairs and records do not have two cases, but only one. This 453structure can be exploited as well. Notice, that for this case, the guess does not depend on the predicate $P$ any 454more. It just depends on the type of the variable we try to instantiate. 455% 456\begin{lemma}[Monochotomy Guesses]\label{lemma_guesses_monochotomy} 457\[ 458\begin{array}{l@{\quad}l@{\quad}l} 459(\forall x.\ \exists \fv.\ x = c(\fv))) & \Longrightarrow & 460\forall P.\ \GEG(\lambda \fv.\ c(\fv),\ P) \\ 461(\forall x.\ \exists \fv.\ x = c(\fv))) & \Longrightarrow & 462\forall P.\ \GUG(\lambda \fv.\ c(\fv),\ P) \\ 463\end{array} 464\] 465\end{lemma} 466 467\subsection{Other guesses} 468The base guesses presented above are at the most important ones. However, other 469trivial base guesses are exploited as well for the implementation. 470The most important ones are point guesses that can be derived 471from some context information: 472% 473\begin{lemma}[Context Guesses]\label{lemma_guesses_context} 474\[ 475\begin{array}{l@{\quad\quad}l} 476P(c) \Longrightarrow \GEP(K\ c,\ \lambda x.\ P(x)) \\ 477\neg P(c) \Longrightarrow \GUP(K\ c,\ \lambda x.\ P(x)) 478\end{array} 479\] 480\end{lemma} 481% 482\noindent 483Moreover, generating guesses on the fly for constants is important to 484implement lifting efficiently: 485% 486\begin{lemma}[Guesses for Constants]\label{lemma_guesses_const} 487Given a term $c$ such that a variable $x$ does not occur in $c$, any term $i$ is a 488valid existential and universal guess: 489\[ 490\begin{array}{l@{\quad\quad}l} 491\GE(i,\ \lambda x.\ c) & \GU(i,\ \lambda x.\ c) 492\end{array} 493\] 494\end{lemma} 495 496 497 498\section{Lifting Guesses}\label{sec_lifting_guesses} 499 500In Sec.~\ref{sec_base_guesses} the base cases of the search for guesses have been presented. 501It remains to discuss, how guesses are lifted over common operators. 502 503\subsection{Negation} 504Guesses are defined with negation in mind. Therefore, it is straightforward to lift 505guesses over negation: 506% 507\begin{lemma}[Lifting Guesses over Negation]\label{lemma_guesses_lift_neg} 508\[ 509\begin{array}{lll@{\quad}lll} 510\GEP(i,\ \lambda x.\ P(x)) & \Rightarrow & \GUP(i,\ \lambda x.\ \neg P(x)) & 511\GUP(i,\ \lambda x.\ P(x)) & \Rightarrow & \GEP(i,\ \lambda x.\ \neg P(x)) \\ 512\GE(i,\ \lambda x.\ P(x)) & \Rightarrow & \GU(i,\ \lambda x.\ \neg P(x)) & 513\GU(i,\ \lambda x.\ P(x)) & \Rightarrow & \GE(i,\ \lambda x.\ \neg P(x)) \\ 514\GEG(i,\ \lambda x.\ P(x)) & \Rightarrow & \GUG(i,\ \lambda x.\ \neg P(x)) & 515\GUG(i,\ \lambda x.\ P(x)) & \Rightarrow & \GEG(i,\ \lambda x.\ \neg P(x)) 516\end{array} 517\] 518\end{lemma} 519 520\subsection{Disjunction} 521 522Lifting guesses over a disjunction $P_1(x) \vee P_2(x)$ is a bit more 523complicated. Point existential guesses are straightforward to lift. If we 524have a point existential guess for either $P_1$ or $P_2$, it is also one for 525the disjunction: 526% 527\begin{lemma}[Lifting Point Existential Guesses over Disjunction]\label{lemma_guesses_lift_disj_T} 528\[ 529\begin{array}{l@{\quad}l@{\quad}l} 530\GEP(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GEP(i,\ \lambda x.\ P_1(x) \vee P_2(x)) \\ 531\GEP(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GEP(i,\ \lambda x.\ P_1(x) \vee P_2(x)) 532\end{array} 533\] 534\end{lemma} 535% 536In contrast, point universal guesses have to hold for both disjuncts: 537\begin{lemma}[Lifting Point Universal Guesses over Disjunction]\label{lemma_guesses_lift_disj_F} 538\[ 539\begin{array}{l@{\quad}l@{\quad}l} 540\GUP(i,\ \lambda x.\ P_1(x)) \wedge \GUP(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GUP(i,\ \lambda x.\ P_1(x) \vee P_2(x)) 541\end{array} 542\] 543\end{lemma} 544% 545For gap guesses, it is the other way round: 546% 547\begin{lemma}[Lifting Gap Existential Guesses over Disjunction]\label{lemma_guesses_lift_disj_SE} 548\[ 549\begin{array}{l@{\quad}l@{\quad}l} 550\GEG(i,\ \lambda x.\ P_1(x)) \wedge \GEG(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GEG(i,\ \lambda x.\ P_1(x) \vee P_2(x)) 551\end{array} 552\] 553\end{lemma} 554% 555\begin{lemma}[Lifting Gap Universal Guesses over Disjunction]\label{lemma_guesses_lift_disj_SA} 556\[ 557\begin{array}{l@{\quad}l@{\quad}l} 558\GUG(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GUG(i,\ \lambda x.\ P_1(x) \vee P_2(x)) \\ 559\GUG(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GUG(i,\ \lambda x.\ P_1(x) \vee P_2(x)) 560\end{array} 561\] 562\end{lemma} 563 564For weak existential guesses, existential guesses for both subterms are needed. However, 565Lemma~\ref{lemma_guesses_const} leads to a nice rule, provided the 566variable does not occur in one of the operands. 567 568\begin{lemma}[Lifting Existential Guesses over Disjunction]\label{lemma_guesses_lift_disj_E} 569\[ 570\begin{array}{c@{\quad}c@{\quad}l} 571\GE(i,\ \lambda x.\ P_1(x)) \wedge \GE(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GE(i,\ \lambda x.\ P_1(x) \vee P_2(x)) \\ 572\GE(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GE(i,\ \lambda x.\ P_1(x) \vee p_2) \\ 573\GE(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GE(i,\ \lambda x.\ p_1 \vee P_2(x)) 574\end{array} 575\] 576\end{lemma} 577 578For universal guesses it is even more complicated, because the handling of free variables does not fit well. 579The guess is not allowed to depend on any free variable (denoted by $K\ i_c$). 580\begin{lemma}[Lifting Universal Guesses over Disjunction]\label{lemma_guesses_lift_disj_A} 581\[ 582\begin{array}{c@{\quad}c@{\quad}l} 583\begin{array}{cl} 584\GU(K\ i_c,\ \lambda x.\ P_1(x)) & \wedge \\ 585\GU(K\ i_c,\ \lambda x.\ P_2(x)) 586\end{array} & \Longrightarrow & \GU(K\ i_c,\ \lambda x.\ P_1(x) \vee P_2(x)) \\[1em] 587\GU(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GU(i,\ \lambda x.\ P_1(x) \vee p_2) \\ 588\GU(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GU(i,\ \lambda x.\ p_1 \vee P_2(x)) 589\end{array} 590\] 591\end{lemma} 592 593So, for the strong types of guesses, one of the dual guesses behaves 594nicely. In contrast, none of the weak guesses does. As motivated 595above, this is the main reason for introducing the stronger types of 596guesses. 597 598 599\subsection{Other Boolean Operations} 600 601We have seen above how to handle negation and disjunction. Other Boolean operations can be expressed in terms of these. 602Therefore, the above lemmata can also be used to lift guesses over other Boolean operations. However, for efficiency 603reasons the implementation in HOL~4 uses special, derived rules. Here, some of these rules are listed without further explanation: 604 605\begin{lemma}[Lifting Guesses over Conjunction]\label{lemma_guesses_lift_conj} 606\[ 607\begin{array}{c@{\quad}c@{\quad}l} 608\GEP(i,\ \lambda x.\ P_1(x)) \wedge \GEP(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GEP(i,\ \lambda x.\ P_1(x) \wedge P_2(x)) \\ 609\GUP(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GUP(i,\ \lambda x.\ P_1(x) \wedge P_2(x)) \\ 610\GUP(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GUP(i,\ \lambda x.\ P_1(x) \wedge P_2(x)) \\ 611\GEG(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GEG(i,\ \lambda x.\ P_1(x) \wedge P_2(x)) \\ 612\GEG(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GEG(i,\ \lambda x.\ P_1(x) \wedge P_2(x)) \\ 613\GUG(i,\ \lambda x.\ P_1(x)) \wedge \GUG(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GUG(i,\ \lambda x.\ P_1(x) \wedge P_2(x)) \\ 614 615\GE(K\ i_c,\ \lambda x.\ P_1(x)) \wedge \GE(K\ i_c,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GE(K\ i_c,\ \lambda x.\ P_1(x) \wedge P_2(x)) \\ 616\GE(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GE(i,\ \lambda x.\ P_1(x) \wedge p_2) \\ 617\GE(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GE(i,\ \lambda x.\ p_1 \wedge P_2(x)) \\ 618 619\GU(i,\ \lambda x.\ P_1(x)) \wedge \GU(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GU(i,\ \lambda x.\ P_1(x) \wedge P_2(x)) \\ 620\GU(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GU(i,\ \lambda x.\ P_1(x) \wedge p_2) \\ 621\GU(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GU(i,\ \lambda x.\ p_1 \wedge P_2(x)) 622\end{array} 623\] 624\end{lemma} 625 626\begin{lemma}[Lifting Guesses over Implication]\label{lemma_guesses_lift_imp} 627\[ 628\begin{array}{c@{\quad}c@{\quad}l} 629\GEP(i,\ \lambda x.\ P_1(x)) \wedge \GUP(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GUP(i,\ \lambda x.\ P_1(x) \Rightarrow P_2(x)) \\ 630\GUP(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GEP(i,\ \lambda x.\ P_1(x) \Rightarrow P_2(x)) \\ 631\GEP(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GEP(i,\ \lambda x.\ P_1(x) \Rightarrow P_2(x)) \\ 632 633\GEG(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GUG(i,\ \lambda x.\ P_1(x) \Rightarrow P_2(x)) \\ 634\GUG(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GUG(i,\ \lambda x.\ P_1(x) \Rightarrow P_2(x)) \\ 635\GUG(i,\ \lambda x.\ P_1(x)) \wedge \GEG(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GEG(i,\ \lambda x.\ P_1(x) \Rightarrow P_2(x)) \\ 636 637\GU(i,\ \lambda x.\ P_1(x)) \wedge \GE(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GE(i,\ \lambda x.\ P_1(x) \Rightarrow P_2(x)) \\ 638\GU(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GE(i,\ \lambda x.\ P_1(x) \Rightarrow p_2) \\ 639\GE(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GE(i,\ \lambda x.\ p_1 \Rightarrow P_2(x)) \\ 640 641\GE(K\ i_c,\ \lambda x.\ P_1(x)) \wedge \GU(K\ i_c,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GU(K\ i_c,\ \lambda x.\ P_1(x) \Rightarrow P_2(x)) \\ 642\GE(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GU(i,\ \lambda x.\ P_1(x) \Rightarrow p_2) \\ 643\GU(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GU(i,\ \lambda x.\ p_1 \Rightarrow P_2(x)) \\ 644\end{array} 645\] 646\end{lemma} 647 648 649\subsection{Quantifiers} 650 651It remains to lift guesses over quantifiers. Let's first consider universal quantification. 652If the guess does depend on the quantified variables, it becomes a free variable of the guess: 653 654\begin{lemma}[Lifting Guesses over Universal Quantification (1)]\label{lemma_guesses_lift_forall_1} 655\[ 656\begin{array}{c} 657(\forall y.\ \GEP(\lambda \fv.\ i(\fv, y),\ \lambda x.\ P(x, y)) \Longrightarrow \\ 658\GEP(\lambda \fv'.\ i(\textsf{FST}(\fv'), \textsf{SND}(\fv')),\ \lambda x.\ \forall y.\ P(x, y)) \\[1em] 659 660(\forall y.\ \GU(\lambda \fv.\ i(\fv, y),\ \lambda x.\ P(x, y)) \Longrightarrow \\ 661\GU(\lambda \fv'.\ i(\textsf{FST}(\fv'), \textsf{SND}(\fv')),\ \lambda x.\ \forall y.\ P(x, y)) \\[1em] 662 663(\forall y.\ \GUG(\lambda \fv.\ i(\fv, y),\ \lambda x.\ P(x, y)) \Longrightarrow \\ 664\GUG(\lambda \fv'.\ i(\textsf{FST}(\fv'), \textsf{SND}(\fv')),\ \lambda x.\ \forall y.\ P(x, y)) \\[1em] 665 666(\forall y.\ \GEG(\lambda \fv.\ i(\fv, y),\ \lambda x.\ P(x, y)) \Longrightarrow \\ 667\GEG(\lambda \fv'.\ i(\textsf{FST}(\fv'), \textsf{SND}(\fv')),\ \lambda x.\ \forall y.\ P(x, y)) \\ 668\end{array} 669\] 670\end{lemma} 671% 672Notice however, that weak existential and point universal guesses can't be lifted that way. If a guess does not depend on the quantified variable, 673it is possible, though: 674 675\begin{lemma}[Lifting Guesses over Universal Quantification (2)]\label{lemma_guesses_lift_forall_2} 676\[ 677\begin{array}{c@{\quad}c@{\quad}l} 678(\forall y.\ \GEP(i,\ \lambda x.\ P(x, y)) & \Longrightarrow & \GEP(i,\ \lambda x.\ \forall y.\ P(x, y)) \\ 679(\forall y.\ \GE(K\ i_c,\ \lambda x.\ P(x, y)) & \Longrightarrow & \GE(K\ i_c,\ \lambda x.\ \forall y.\ P(x, y)) \\ 680(\forall y.\ \GEG(i,\ \lambda x.\ P(x, y)) & \Longrightarrow & \GEG(i,\ \lambda x.\ \forall y.\ P(x, y)) \\ 681(\forall y.\ \GUP(i,\ \lambda x.\ P(x, y)) & \Longrightarrow & \GUP(i,\ \lambda x.\ \forall y.\ P(x, y)) \\ 682(\forall y.\ \GU(i,\ \lambda x.\ P(x, y)) & \Longrightarrow & \GU(i,\ \lambda x.\ \forall y.\ P(x, y)) \\ 683(\forall y.\ \GUG(i,\ \lambda x.\ P(x, y)) & \Longrightarrow & \GUG(i,\ \lambda x.\ \forall y.\ P(x, y)) 684\end{array} 685\] 686\end{lemma} 687 688Rules for lifting guesses over existential quantification are dual. However, unique existential quantification needs a bit 689of attention: 690 691\begin{lemma}[Lifting Guesses over Unique Existential Quantification] 692\[ 693\begin{array}{c@{\quad}c@{\quad}l} 694(\forall y.\ \GUP(i,\ \lambda x.\ P(x, y)) & \Longrightarrow & \GUP(i,\ \lambda x.\ \exists! y.\ P(x, y)) \\ 695(\forall y.\ \GEG(i,\ \lambda x.\ P(x, y)) & \Longrightarrow & \GEG(i,\ \lambda x.\ \exists! y.\ P(x, y)) 696\end{array} 697\] 698\end{lemma} 699 700 701\section{Related Techniques}\label{sec_other_techniques} 702 703Above base guesses and lifting of guesses have been presented. This section now 704briefly discusses other techniques that enhance guess search: 705 706\subsection{Rewrites}\label{subsec_other_techniques_rewrites} 707 708A very powerful, yet simple technique for teaching the guess search 709about new constructs are rewrite rules. For example, the rules above 710cannot generate guesses for the predicate $\textsf{IS\_SOME}$. By 711rewriting $\textsf{IS\_SOME}(x)$ to $\exists x'.\ x = 712\textsf{SOME}(x')$, however, the rules for equations and 713quantification as well as the dichotomy rule for option types can be 714used. 715 716The HOL~4 implementation uses rewrites to add support for predicates 717like $\textsf{IS\_SOME}$ or $\textsf{NULL}$ on lists. However, adding 718rules like $\textsf{append}(l_1, l_2) = [\,] \Longleftrightarrow (l_1 = 719[\,]\ \wedge\ l_2 = [\,])$ for list-append turned out to be beneficial 720in practice as well. 721 722\subsection{Strengthening and Weakening}\label{subsec_other_techniques_imp} 723 724Rewrite rules are very useful. However, sometimes only implications instead of 725equivalences are available. These can be exploited as well: 726 727\begin{lemma}[Strengthening / Weakening Guesses]\label{lemma_guesses_strengthen_weaken} 728\[ 729\left(\forall x.\ P_1(x) \Rightarrow P_2(x)\right) \Longrightarrow 730\left(\begin{array}{@{}rcl} 731\forall x.\ \GEP(i, P_1) & \Longrightarrow & \GEP(i,\ \lambda x.\ P_2) \qquad \wedge\\ 732\forall x.\ \GUG(i, P_1) & \Longrightarrow & \GUG(i,\ \lambda x.\ P_2) \qquad \wedge\\ 733\forall x.\ \GUP(i, P_2) & \Longrightarrow & \GUP(i,\ \lambda x.\ P_1) \qquad \wedge\\ 734\forall x.\ \GEG(i, P_2) & \Longrightarrow & \GEG(i,\ \lambda x.\ P_1) 735\end{array} 736\right) 737\] 738\end{lemma} 739 740 741 742\subsection{Minimising Variable Occurrences}\label{subsec_varmin} 743 744As for example Lemma~\ref{lemma_guesses_lift_disj_E} illustrates, it 745is easier to find guesses for a variable if it occurs in fewer 746positions. Therefore, the HOL~4 implementation preprocesses the term and tries to 747minimise the number of occurrences. For example, 748$\exists x.\ (f (8 + 2) = f (x + 2)) \wedge P (f (x + 2))$ is 749rewritten to $\exists x.\ (f (8 + 2) = f (x + 2)) \wedge P (f (8 + 7502))$ by this prepossessing step. This explains, why this example 751can be handled, whereas apparently similar ones cannot (see Table~\ref{table_examples}). 752The implementation for minimising variable occurrences is based 753on simple rules like $(x = t) \wedge P(x) 754\ \Longleftrightarrow\ (x = t) \wedge P(t)$ or $x \neq t \vee P(x) 755\ \Longleftrightarrow\ x \neq t \vee P(t)$. 756 757 758\section{Examples}\label{sec_examples} 759 760In the last few sections, the method for searching guesses has been presented on an abstract level. 761Let's now consider a few examples to see how this methods works in practice. 762 763\subsection{Example 1} 764Let's start with the example 765$\exists x.\ (\forall y.\ Q(y)\ \wedge\ (x=7)) \ 766\wedge\ P(x)$. This example cannot be handled by 767existing tools. However, the lemmata presented above allow to 768derive a guess for this example: 769% 770\[\begin{array}{cc@{\qquad}l} 771\GEG(K\ 7, \lambda x.\ x = 7) & \text{(1)} & \text{from Lemma~\ref{lemma_guesses_equation_top}} \\ 772\GEG(K\ 7, \lambda x.\ Q(y)\ \wedge\ (x=7)) & \text{(2)} & \text{from (1) and Lemma~\ref{lemma_guesses_lift_conj}} \\ 773\GEG(K\ 7, \lambda x.\ \forall y.\ Q(y)\ \wedge\ (x=7)) & \text{(3)} & \text{from (2) and Lemma~\ref{lemma_guesses_lift_forall_2}} \\ 774\GEG(K\ 7, \lambda x.\ (\forall y.\ Q(y)\ \wedge\ (x=7)) \wedge P(x)) & \text{(4)} & \text{from (3) and Lemma~\ref{lemma_guesses_lift_conj}} 775\end{array} 776\] 777% 778With Lemma~\ref{lemma_guesses_usage} we can therefore simplify 779$\exists x.\ (\forall y.\ Q(y)\ \wedge\ (x=7)) \ \wedge\ P(x)$ to 780$(\forall y.\ Q(y)\ \wedge\ (7=7)) \ \wedge\ P(7)$ and with some general infrastructure further to 781$(\forall y.\ Q(y)) \ \wedge\ P(7)$. 782Here, only the trace that succeeds is presented. The search actually produces more guesses. 783For example, $\GEP(K\ 7, \lambda x.\ x = 7)$ is derived as well, but then fails to be lifted over 784the conjunction. 785 786\subsection{Example 2}\label{subsec_Example_2} 787The example $\forall x.\ \textsf{IS\_NONE}(x) \vee P(x)$ illustrates partial instantiations for datatypes. 788\[\begin{array}{cc@{\qquad}l} 789\GUG(\lambda x'.\ \textsf{SOME}(x'), \lambda x.\ x = \textsf{NONE}) & \text{(1)} & \text{from Lemma~\ref{lemma_guesses_dichotomy}} \\ 790\GUG(\lambda x'.\ \textsf{SOME}(x'), \lambda x.\ \textsf{IS\_NONE}(x)) & \text{(2)} & \text{rewrite of (1)} \\ 791\GUG(\lambda x'.\ \textsf{SOME}(x'), \lambda x.\ \textsf{IS\_NONE}(x) \vee P(x)) & \text{(3)} & \text{from (2) and Lemma~\ref{lemma_guesses_lift_disj_SA}} 792\end{array} 793\] 794Therefore, 795$\forall x.\ \textsf{IS\_NONE}(x) \vee P(x)$ can be simplified to 796$\forall x'.\ P(\textsf{SOME}(x'))$. 797 798\subsection{Example 3} 799Let's consider $\exists x.\ (f (8 + 2) = f (x + 2)) \wedge P (f (x + 2))$. The guess 800\[\begin{array}{cc@{\quad}l} 801\GEP(K\ 8, \lambda x.\ f (8 + 2) = f (x + 2)) & \text{(1)} & \text{from Lemma~\ref{lemma_guesses_equation_T}} \\ 802\end{array} 803\] 804can be easily derived. However, then we are stuck, because we cannot derive a point existential guess for the conjunct $P (f (x + 2))$. 805So, we weaken the guess: 806\[\begin{array}{cc@{\quad}l} 807\GE(K\ 8, \lambda x.\ f (8 + 2) = f (x + 2)) & \text{(2)} & \text{from (1) and Lemma~\ref{lemma_guesses_strength}} \\ 808\end{array} 809\] 810Unluckily, we are still stuck, because $P (f (x + 2))$ depends on $x$. However, our tool can rewrite the overall term 811such that this dependence disappears (see Sec.~\ref{subsec_varmin}). 812\[\begin{array}{cc@{\quad}l} 813\GE(K\ 8, \lambda x.\ (f (8 + 2) = f (x + 2)) \wedge P(f(8 + 2))) & \text{(3)} & \text{from (2), Lemma~\ref{lemma_guesses_lift_conj}, 814\ref{lemma_guesses_lift_neg}} \\ 815\GE(K\ 8, \lambda x.\ (f (8 + 2) = f (x + 2)) \wedge P(f(x + 2))) & \text{(4)} & \text{from (3) and rewrite} 816\end{array} 817\] 818Thus, we found a guess and can instantiate the quantifier with 8. 819 820\subsection{Example 4} 821Finally, consider $\big((\forall x.\ P_1(x) \Rightarrow P_2(x)) \wedge P_1(2)\big) \Longrightarrow \exists x.\ P_2(x)$. 822First, HOL~4's general infrastructure processes this and allows us to concentrate on 823$\exists x.\ P_2(x)$, while using (1) $\forall x.\ P_1(x) \Rightarrow P_2(x)$ and (2)~$P_1(2)$ as lemmata. 824Then guesses can be derived as follows: 825\[\begin{array}{cc@{\qquad}l} 826\GEP(K\ 2, \lambda x.\ P_1(x)) & \text{(3)} & \text{from (2), Lemma~\ref{lemma_guesses_context}} \\ 827\GEP(K\ 2, \lambda x.\ P_2(x)) & \text{(4)} & \text{from (1), (3), Lemma~\ref{lemma_guesses_strengthen_weaken}} 828\end{array} 829\] 830Thus, we found a guess and can simplify the original goal first to 831$\big((\forall x.\ P_1(x) \Rightarrow P_2(x)) \wedge P_1(2)\big) \Longrightarrow \textit{true}$ and then further to 832\textit{true}. 833 834 835\chapter{HOL~4 implementation} 836 837\section{User Interface}\label{sec_interface} 838 839The quantifier heuristics library can be found in the sub-directory 840\texttt{src/quantHeuristics}. The entry point to the framework is the 841library \texttt{quantHeuristicsLib}. 842 843\subsection{Conversions} 844Usually the library is used for 845converting a term containing quantifiers to an equivalent one. For this, 846the following high level entry points exists: 847\bigskip 848 849\noindent 850\begin{tabular}{@{}ll} 851\texttt{QUANT\_INSTANTIATE\_CONV} & \texttt{: quant\_param list -> conv} \\ 852\texttt{QUANT\_INST\_ss} & \texttt{: quant\_param list -> ssfrag} \\ 853\texttt{QUANT\_INSTANTIATE\_TAC} & \texttt{: quant\_param list -> tactic} \\ 854\texttt{ASM\_QUANT\_INSTANTIATE\_TAC} & \texttt{: quant\_param list -> tactic} 855\end{tabular} 856\bigskip 857 858All these functions get a list of \emph{quantifier heuristic parameters} as arguments. These 859parameters essentially configure, which heuristics are used during the guess-search. If 860an empty list is provided, the tools know about the standard Boolean combinators and equations. 861\texttt{std\_qp} adds support for context and common datatypes like pairs or lists. 862Quantifier heuristic parameters are explained in more detail in 863Section~\ref{sec_qps}. 864 865So, some simple usage of the quantifier heuristic library looks like: 866{\scriptsize 867\begin{verbatim} 868> QUANT_INSTANTIATE_CONV [] ``?x. (!z. Q z /\ (x=7)) /\ P x``; 869val it = |- (?x. (!z. Q z /\ (x = 7)) /\ P x) <=> (!z. Q z) /\ P 7: thm 870 871> QUANT_INSTANTIATE_CONV [std_qp] ``!x. IS_SOME x ==> P x`` 872val it = |- (!x. IS_SOME x ==> P x) <=> !x_x'. P (SOME x_x'): thm 873\end{verbatim}} 874 875Usually, the quantifier heuristics library is used together with the 876simplifier using \texttt{QUANT\_INST\_ss}. Besides interleaving 877simplification and quantifier instantiation, this has the benefit of 878being able to use context information collected by the simplifier: 879 880{\scriptsize 881\begin{verbatim} 882> QUANT_INSTANTIATE_CONV [] ``P m ==> ?n. P n`` 883Exception- UNCHANGED raised 884 885> SIMP_CONV (bool_ss ++ QUANT_INST_ss []) [] ``P m ==> ?n. P n`` 886val it = |- P m ==> (?n. P n) <=> T: thm 887\end{verbatim}} 888 889It's usually best to use \texttt{QUANT\_INST\_ss} 890together with e.\,g.\ \texttt{SIMP\_TAC} when using the library with tactics. 891However, if free variables of the goal should be instantiated, then 892\texttt{ASM\_QUANT\_INSTANTIATE\_TAC} should be used: 893 894{\scriptsize 895\begin{verbatim} 896P x 897------------------------------------ 898 IS_SOME x 899 : proof 900 901> e (ASM\_QUANT_INSTANTIATE_TAC [std_qp]) 902P (SOME x_x') : proof 903\end{verbatim}} 904 905There is also \texttt{QUANT\_INSTANTIATE\_TAC} as a shortcut 906for using \texttt{QUANT\_INSTANTIATE\_CONV} as a tactic. It does not 907instantiate free variables or considers the assumptions. 908 909 910\subsection{Unjustified Guesses} 911 912Most heuristics justify the guesses they produce and therefore allow to 913prove equivalences. 914However, the implementation also supports unjustified guesses, which may be bogus. 915Let's consider the example $\exists x.\ P(x) \Longrightarrow (x = 2)\ \wedge\ Q(x)$. 916Because nothing is known about $P$ and $Q$, we can't find a safe instantiation for $x$ here. 917However, $2$ looks tempting and is probably sensible in many situations. (Counterexample: 918$P(2)$, $\neg Q(2)$ and $\neg P(3)$ hold) 919 920\texttt{implication\_concl\_qp} is a quantifier parameter that looks for valid guesses in the conclusion of an implication. 921Then, it assumes without justification that these guesses are probably sensible for the whole implication as well. 922Because these guesses might be wrong, one can either use implications or 923expansion theorems like $\exists x. P(x)\ \Leftrightarrow (\forall x.\ (x \neq c) \Rightarrow \neg P(x)) \Rightarrow P(c)$. 924 925{\scriptsize 926\begin{verbatim} 927> QUANT_INSTANTIATE_CONV [implication_concl_qp] ``?x. P x ==> (x = 2) /\ Q x`` 928Exception- UNCHANGED raised 929 930> QUANT_INSTANTIATE_CONSEQ_CONV [implication_concl_qp] CONSEQ_CONV_STRENGTHEN_direction 931 ``?x. P x ==> (x = 2) /\ Q x`` 932val it = 933 |- (P 2 ==> Q 2) ==> ?x. P x ==> (x = 2) /\ Q x: thm 934 935> EXPAND_QUANT_INSTANTIATE_CONV [implication_concl_qp] ``?x. P x ==> (x = 2) /\ Q x`` 936val it = |- (?x. P x ==> (x = 2) /\ Q x) <=> 937 (!x. x <> 2 ==> ~(P x ==> (x = 2) /\ Q 2)) ==> P 2 ==> Q 2: thm 938 939> SIMP_CONV (std_ss++EXPAND_QUANT_INST_ss [implication_concl_qp]) [] ``?x. P x ==> (x = 2) /\ Q x`` 940val it = 941 |- (?x. P x ==> (x = 2) /\ Q x) <=> (!x. x <> 2 ==> P x) ==> P 2 ==> Q 2: thm 942\end{verbatim}} 943 944 945The following entry points should be used to exploit unjustified guesses: 946\bigskip 947 948\noindent 949\begin{tabular}{@{}ll} 950\texttt{QUANT\_INSTANTIATE\_CONSEQ\_CONV} & \texttt{: quant\_param list -> directed\_conseq\_conv} \\ 951\texttt{EXPAND\_QUANT\_INSTANTIATE\_CONV} & \texttt{: quant\_param list -> conv} \\ 952\texttt{EXPAND\_QUANT\_INST\_ss} & \texttt{: quant\_param list -> ssfrag} \\ 953\texttt{QUANT\_INSTANTIATE\_CONSEQ\_TAC} & \texttt{: quant\_param list -> tactic} 954\end{tabular} 955 956\subsection{Debugging} 957 958To debug the guess-search, it is possible to print tracing information. 959This is done by setting the trace \texttt{QUANT\_INSTANTIATE\_HEURISTIC} to 1 or 2. For 960the example in Sec.~\ref{subsec_Example_2} the debug output looks like: 961 962{\scriptsize 963\begin{verbatim} 964val _ = set_trace "QUANT_INSTANTIATE_HEURISTIC" 1 965val thm = QUANT_INSTANTIATE_CONV [std_qp] ``!x. IS_NONE x \/ P x`` 966 967searching guesses for ``x`` in ``~(IS_NONE x \/ P x)`` 968 searching guesses for ``x`` in ``IS_NONE x \/ P x`` 969 searching guesses for ``x`` in ``IS_NONE x`` 970 searching guesses for ``x`` in ``x = NONE`` 971 7 guesses found for ``x`` in ``x = NONE`` 972 - guess_exists_point (``NONE``, [], X) 973 - guess_forall_point (``SOME x_x``, [x_x], X) 974 - guess_forall (``SOME x_x``, [x_x], X) 975 - guess_forall (``SOME x_x'``, [x_x'], X) 976 - guess_exists (``NONE``, [], X) 977 - guess_forall_gap (``SOME x_x'``, [x_x'], X) 978 - guess_exists_gap (``NONE``, [], X) 979 7 guesses found for ``x`` in ``IS_NONE x`` 980 - guess_exists_point (``NONE``, [], X) 981 - guess_forall_point (``SOME x_x``, [x_x], X) 982 - guess_forall (``SOME x_x``, [x_x], X) 983 - guess_forall (``SOME x_x'``, [x_x'], X) 984 - guess_exists (``NONE``, [], X) 985 - guess_forall_gap (``SOME x_x'``, [x_x'], X) 986 - guess_exists_gap (``NONE``, [], X) 987 searching guesses for ``x`` in ``P x`` 988 no guesses found for ``x`` in ``P x`` 989 4 guesses found for ``x`` in ``IS_NONE x \/ P x`` 990 - guess_exists_point (``NONE``, [], X) 991 - guess_forall (``SOME x_x'``, [x_x'], X) 992 - guess_exists (``NONE``, [], X) 993 - guess_forall_gap (``SOME x_x'``, [x_x'], X) 9944 guesses found for ``x`` in ``~(IS_NONE x \/ P x)`` 995 - guess_forall_point (``NONE``, [], X) 996 - guess_forall (``NONE``, [], X) 997 - guess_exists (``SOME x_x'``, [x_x'], X) 998 - guess_exists_gap (``SOME x_x'``, [x_x'], X) 999searching guesses for ``x_x'`` in ``~P (SOME x_x')`` 1000 searching guesses for ``x_x'`` in ``P (SOME x_x')`` 1001 no guesses found for ``x_x'`` in ``P (SOME x_x')`` 1002no guesses found for ``x_x'`` in ``~P (SOME x_x')`` 1003 1004val thm = |- (!x. IS_NONE x \/ P x) <=> !x_x'. P (SOME x_x'): thm 1005\end{verbatim}} 1006 1007 1008\subsection{Interface Details} 1009 1010The high level interface is mainly build around 1011an highly configurable conversion and a corresponding consequence conversion. 1012\texttt{EXTENSIBLE\_QUANT\_INSTANTIATE\_CONV} gets the following arguments: 1013 1014\begin{description} 1015 \item[\texttt{cache\_ref\_opt\ :\ quant\_heuristic\_cache ref option}] 1016 a cache for guesses. If \texttt{NONE} is passed, 1017 a new cache is created on the fly. New caches can be created by \texttt{mk\_quant\_heuristic\_cache} and then 1018 used to cache results through multiple calls. 1019 \item[\texttt{re\ :\ bool}] redescent into a term after some instantiation has been found? 1020 It determines, whether internally \texttt{DEPTH\_CONV} or \texttt{REDEPTH\_CONV} is used. 1021 1022 \item[\texttt{min\_var\_occs\ :\ bool}] add a preprocessing step to minimise the number of occurrences of 1023 a variable (see Sec.\ref{subsec_varmin}). Since this preprocessing might be slow, one might want to skip it. 1024 1025 \item[\texttt{expand\ :\ bool}] use expansion to exploit unjustified guesses? 1026 1027 \item[\texttt{ctx\ :\ thm list}] a list of theorems that come from the context (e.\,g.\ collected by the simplifier). 1028 1029 \item[\texttt{base\_arg\ :\ quant\_param}] a parameter that should always be used. This is by default 1030 \texttt{basic\_qp}, which can handle the standard Boolean connectives and equations. In special circumstances, 1031 it might be beneficial to use \texttt{empty\_qp}, though. 1032 1033 \item[\texttt{args\ :\ quant\_param list}] list of quantifier heuristic parameters to use. 1034\end{description} 1035 1036The consequence conversion 1037\texttt{EXTENSIBLE\_QUANT\_INSTANTIATE\_CONSEQ\_CONV} gets the same 1038arguments, except \texttt{expand} and \texttt{ctx}. Since it can use 1039implications, expansion is not needed. Because 1040\texttt{DEPTH\_CONSEQ\_CONV} collects its own context and can't easily 1041be used with the simplifier anyhow, \texttt{ctx} is unnecessary. 1042\texttt{EXTENSIBLE\_QUANT\_INST\_ss} is a wrapper of the conversion that removes the arguments 1043\texttt{re} and \texttt{ctx}, because they are taken care of by the simplifier. 1044 1045All other entry points, including the ones presented above are derived 1046form the conversion and consequence conversion. By default the argument 1047\texttt{cache\_ref\_opt} is set to \texttt{NONE}, \texttt{re} is false, 1048preprocessing turned on, expanding turned off, an empty context is used and 1049\texttt{basic\_qp} is always present. Versions of the high level entry points 1050containing \texttt{FAST} in their name, turn preprocessing off; \texttt{EXPAND} means that 1051expansion is turned on and \texttt{RE} that \texttt{re} is set to true. 1052 1053\subsection{Explicit Instantiations} 1054 1055A special (slightly degenerated) use of the framework, is turning guess search off completely and 1056providing instantiations explicitly. The tactic \texttt{QUANT\_TAC} allows this. This means that 1057it allows to partially instantiate quantifiers at subpositions 1058with explicitly given terms. As such, it can be seen as 1059a generalisation of \texttt{EXISTS\_TAC}. 1060% 1061{\scriptsize 1062\begin{verbatim} 1063val it = !x. (!z. P x z) ==> ?a b. Q a b z : proof 1064 1065> e( QUANT_INST_TAC [("z", `0`, []), ("a", `SUC a'`, [`a'`])] ) 1066 1067val it = !x. ( P x 0) ==> ? b a'. Q (SUC a') b z : proof 1068\end{verbatim}} 1069% 1070This tactic is implemented using oracle guesses. It normally 1071produces implications, which is fine when used as a tactic. There is 1072also a conversion called \texttt{INST\_QUANT\_CONV} with the same 1073functionality. For a conversion, implications are 1074problematic. Therefore, the simplifier and Metis are used to prove 1075the validity of the explicitly given instantiations. This succeeds 1076usually only for simple examples. 1077 1078 1079\subsection{Simple Quantifier Heuristics}\label{subsec_simple} 1080 1081The full quantifier heuristics described above are powerful and very flexible. 1082However, they are sometimes slow. 1083The unwind library\footnote{see \texttt{src/simp/src/Unwind.sml}} on the other hand is limited, but fast. 1084The simple version of the quantifier heuristics fills the gap in the middle. 1085They just search for gap guesses without any free variables. 1086Moreover, slow operations like recombining or automatically looking up datatype information is omitted. 1087As a result, the conversion \texttt{SIMPLE\_QUANT\_INSTANTIATE\_CONV} (and corresponding \texttt{SIMPLE\_QUANT\_INST\_ss}) is nearly as fast as the corresponding unwind conversions. 1088However, it supports more complicated syntax. Moreover, there is support for quantifiers, pairs, list and much more. 1089 1090\section{Quantifier Heuristic Parameters}\label{sec_qps} 1091 1092Quantifier heuristic parameters play a similar role for the quantifier 1093instantiation library as simpsets do for the simplifier. They contain 1094theorems, ML code and general configuration parameters that allow to configure 1095guess-search. There are predefined parameters that handle 1096common constructs and the user can define own parameters. 1097 1098\subsection{Quantifier Heuristic Parameters for Common Datatypes} 1099 1100There are \texttt{option\_qp}, \texttt{list\_qp}, \texttt{num\_qp} and \texttt{sum\_qp} for option types, lists, 1101natural numbers and sum types respectively. 1102Some examples are displayed in the following table: 1103% 1104\[\begin{array}{r@{\quad \Longleftrightarrow \quad}l} 1105\forall x.\ \texttt{IS\_SOME}(x) \Rightarrow P(x) & \forall x'.\ P (\texttt{SOME}(x')) \\ 1106\forall x.\ \texttt{IS\_NONE}(x)& \textit{false} \\ 1107\forall l.\ l \neq [\,] \Rightarrow P(l)& \forall h, l'.\ P(h::l') \\ 1108\forall x.\ x = c + 3& \textit{false} \\ 1109\forall x.\ x \neq 0 \Rightarrow P(x)& \forall x'.\ P(\texttt{SUC}(x')) 1110\end{array}\] 1111 1112\subsection{Quantifier Heuristic Parameters for Tuples} 1113 1114For tuples the situation is peculiar, because each quantifier over a variable of a product type 1115can be instantiated. The challenge is to decide which quantifiers should be instantiated and 1116which new variable names to use for the components of the pair. 1117There is a quantifier heuristic parameter called \texttt{pair\_default\_qp}. It first looks for 1118subterms of the form $(\lambda (x_1, \ldots, x_n).\ \ldots)\ x$. If such a term is found, $x$ is instantiated with 1119$(x_1, \ldots, x_n)$. Otherwise, subterms of the form $\texttt{FST}(x)$ and $\texttt{SND}(x)$ are searched. If such a term 1120is found, $x$ is instantiated as well. This parameter therefore allows simplifications like: 1121% 1122\[\begin{array}{r@{\quad \Longleftrightarrow \quad}l} 1123\forall p.\ (x = \texttt{SND}(p)) \Rightarrow P(p)& \forall p_1.\ P(p_1, x) \\ 1124\exists p.\ (\lambda (p_a, p_b, p_c). P(p_a, p_b, p_c))\ p & \exists p_a, p_b, p_c.\ P(p_a, p_b, p_c) 1125\end{array}\] 1126 1127\texttt{pair\_default\_qp} is implemented in terms of the more general 1128quantifier heuristic parameter \texttt{pair\_qp}, which allows the 1129user to provide a list of ML functions. These functions get the 1130variable and the term. If they return a tuple of variables, these 1131variables are used for the instantiation, otherwise the next function 1132in the list is called or - if there is no function left - the variable 1133is not instantiated. In the example of $\exists p.\ (\lambda (p_a, 1134p_b, p_c). P(p_a, p_b, p_c))\ p$ these functions are given the 1135variable $p$ and the term $(\lambda (p_a, p_b, p_c). P(p_a, p_b, 1136p_c))\ p$ and return $\texttt{SOME} (p_a, p_b, p_c)$. 1137 1138\subsection{Quantifier Heuristic Parameter for Records} 1139 1140Records are similar to pairs, because they can always be instantiated. Here, it is interesting that the necessary 1141monochotomy lemma comes from HOL~4's \texttt{Type\_Base} library. This means that \texttt{record\_qp} is stateful. 1142If a new record type is defined, the automatically proven monochotomy lemma is then automatically used 1143by \texttt{record\_qp}. In contrast to the pair parameter, the one for records gets only one function instead of a 1144list of functions to decide which variables to instantiate. However, this function is simpler, because it just needs 1145to return true or false. The names of the new variables are constructed from the field-names of the record. 1146The quantifier heuristic parameter \texttt{default\_record\_qp} expands all records. 1147 1148\subsection{Stateful Quantifier Heuristic Parameters} 1149 1150The parameter for records is stateful, as it uses knowledge from 1151\texttt{Type\_Base}. Such information is not only useful for records 1152but for general datatypes. The quantifier heuristic parameter 1153\texttt{TypeBase\_qp} uses automatically proven theorems about new 1154datatypes to exploit mono- and dichotomies. Moreover, there is also a 1155stateful \texttt{pure\_stateful\_qp} that allows the user to 1156explicitly add other parameters to it. \texttt{stateful\_qp} is a 1157combination of \texttt{pure\_stateful\_qp} and \texttt{TypeBase\_qp}. 1158 1159\subsection{Standard Quantifier Heuristic Parameter} 1160 1161The standard quantifier heuristic parameter \texttt{std\_qp} combines 1162the parameters for lists, options, natural numbers, the default one 1163for pairs and the default one for records. 1164 1165 1166\section{User defined Quantifier Heuristic Parameters}\label{sec_qps_user} 1167 1168The user is also able to define own parameters. There 1169is \texttt{empty\_qp}, which does not contain any information. Several 1170parameters can be combined using the function 1171\texttt{combine\_qps}. Together with the basic types of user defined 1172parameters that are explained below, these functions provide an 1173interface for user defined quantifier heuristic parameters. 1174 1175\subsection{Rewrites / Conversions} 1176 1177As discussed in Sec.~\ref{subsec_other_techniques_rewrites}, adding 1178rewrites is a very powerful technique. \texttt{rewrite\_qp} allows to provide rewrites in the form of rewrite theorems. 1179For the example of \texttt{IS\_SOME} discussed in Sec.~\label{subsec_other_techniques_rewrites} this 1180looks like: 1181 1182{\scriptsize 1183\begin{verbatim} 1184> val thm = QUANT_INSTANTIATE_CONV [] ``!x. IS_SOME x ==> P x`` 1185Exception- UNCHANGED raised 1186 1187> val IS_SOME_EXISTS = prove (``IS_SOME x = (?x'. x = SOME x')``, Cases_on `x` THEN SIMP_TAC std_ss []); 1188val IS_SOME_EXISTS = |- IS_SOME x <=> ?x'. x = SOME x': thm 1189 1190> val thm = QUANT_INSTANTIATE_CONV [rewrite_qp[IS_SOME_EXISTS]] ``!x. IS_SOME x ==> P x`` 1191val thm = |- (!x. IS_SOME x ==> P x) <=> !x'. IS_SOME (SOME x') ==> P (SOME x'): thm 1192\end{verbatim}} 1193 1194To clean up the result after instantiation, theorems used to rewrite the result after instantiation can be provided via 1195\texttt{final\_rewrite\_qp}. 1196 1197{\scriptsize 1198\begin{verbatim} 1199> val thm = QUANT_INSTANTIATE_CONV [rewrite_qp[IS_SOME_EXISTS], final_rewrite_qp[option_CLAUSES]] 1200 ``!x. IS_SOME x ==> P x`` 1201val thm = |- (!x. IS_SOME x ==> P x) <=> !x'. P (SOME x'): thm 1202\end{verbatim}} 1203 1204If rewrites are not enough, \texttt{conv\_qp} can be used to add conversions: 1205 1206{\scriptsize 1207\begin{verbatim} 1208> val thm = QUANT_INSTANTIATE_CONV [] ``?x. (\y. y = 2) x`` 1209Exception- UNCHANGED raised 1210 1211> val thm = QUANT_INSTANTIATE_CONV [convs_qp[BETA_CONV]] ``?x. (\y. y = 2) x`` 1212val thm = |- (?x. (\y. y = 2) x) <=> T: thm 1213\end{verbatim}} 1214 1215\subsection{Strengthening / Weakening} 1216 1217In rare cases, equivalences that can be used for rewrites are unavailable. There might be just implications that 1218can be used for strengthening or weakening (see Sec.~\ref{subsec_other_techniques_imp}). The function 1219\texttt{imp\_qp} might be used to provide such implication. 1220 1221{\scriptsize 1222\begin{verbatim} 1223> val thm = QUANT_INSTANTIATE_CONV [list_qp] ``!l. 0 < LENGTH l ==> P l`` 1224Exception- UNCHANGED raised 1225 1226> val LENGTH_LESS_IMP = prove (``!l n. n < LENGTH l ==> l <> []``, Cases_on `l` THEN SIMP_TAC list_ss []); 1227val LENGTH_LESS_IMP = |- !l n. n < LENGTH l ==> l <> []: thm 1228 1229> val thm = QUANT_INSTANTIATE_CONV [imp_qp[LENGTH_LESS_IMP], list_qp] ``!l. 0 < LENGTH l ==> P l`` 1230val thm = 1231 |- (!l. 0 < LENGTH l ==> P l) <=> 1232 !l_t l_h. 0 < LENGTH (l_h::l_t) ==> P (l_h::l_t): thm 1233 1234> val thm = SIMP_CONV (list_ss ++ QUANT_INST_ss [imp_qp[LENGTH_LESS_IMP], list_qp]) [] 1235 ``!l. SUC (SUC n) < LENGTH l ==> P l`` 1236val thm = 1237 |- (!l. SUC (SUC n) < LENGTH l ==> P l) <=> 1238 !l_h l_t_h l_t_t_t l_t_t_h. n < SUC (LENGTH l_t_t_t) ==> P (l_h::l_t_h::l_t_t_h::l_t_t_t): thm 1239\end{verbatim}} 1240 1241 1242\subsection{Filtering} 1243Sometimes, one might want to avoid to instantiate certain quantifiers. 1244The function \texttt{filter\_qp} allows to add ML-functions that filter the handled 1245quantifiers. These functions are given a variable $x$ and a term $P(x)$. 1246The tool only tries to find instantiate $x$ in $P(x)$, if all filter functions 1247return \textit{true}. 1248 1249{\scriptsize 1250\begin{verbatim} 1251> val thm = QUANT_INSTANTIATE_CONV [] ``?x y z. (x = 1) /\ (y = 2) /\ (z = 3) /\ P (x, y, z)`` 1252val thm = |- (?x y z. (x = 1) /\ (y = 2) /\ (z = 3) /\ P (x,y,z)) <=> P (1,2,3): thm 1253 1254> val thm = QUANT_INSTANTIATE_CONV [filter_qp [fn v => fn t => (v = ``y:num``)]] 1255 ``?x y z. (x = 1) /\ (y = 2) /\ (z = 3) /\ P (x, y, z)`` 1256val thm = |- (?x y z. (x = 1) /\ (y = 2) /\ (z = 3) /\ P (x,y,z)) <=> 1257 ?x z. (x = 1) /\ (z = 3) /\ P (x,2,z): thm 1258\end{verbatim}} 1259 1260\subsection{Satisfying and Contradicting Instantiations} 1261 1262As the satisfy library\footnote{see \texttt{src/simp/src/Satisfy.sml}} demonstrates, it is often 1263useful to use unification and explicitly given theorems to 1264find instantiations. In addition to satisfying instantiations, the quantifier heuristics framework 1265is also able to use contradicting ones. The theorems used for finding instantiations usually come from 1266the context. However, \texttt{instantiation\_qp} allows to add additional ones: 1267 1268{\scriptsize 1269\begin{verbatim} 1270> val thm = SIMP_CONV (std_ss++QUANT_INST_ss[]) [] ``P n ==> ?m:num. n <= m /\ P m`` 1271Exception- UNCHANGED raised 1272 1273> val thm = SIMP_CONV (std_ss++QUANT_INST_ss[instantiation_qp[arithmeticTheory.LESS_EQ_REFL]]) [] 1274 ``P n ==> ?m:num. n <= m /\ P m`` 1275> val thm = 1276 |- P n ==> ?m:num. n <= m /\ P m = T : thm 1277\end{verbatim}} 1278 1279\subsection{Di- and Monochotomies} 1280 1281As discussed in Sec.~\ref{subsec_base_guesses_dichotomies}, dichotomies can be exploited for guess search. 1282\texttt{distinct\_qp} provides an interface to add theorems 1283of the form $\forall x.\ c_1(x) \neq c_2(x)$. 1284\texttt{cases\_qp} expects theorems of the form 1285$\forall x. \ (x = \exists \fv. c_1(\fv))\ \vee \ldots \vee (x = \exists \fv. c_n(\fv))$. 1286These theorems are for $n = 2$ used with Lemma~\ref{lemma_guesses_dichotomy} and 1287for $n=1$ with Lemma~\ref{lemma_guesses_monochotomy}. All other cases are currently ignored. 1288 1289\subsection{Lifting Theorems} 1290 1291In Section~\ref{sec_lifting_guesses} theorems have been presented that 1292allow lifting guesses. The function \texttt{inference\_qp} enables the 1293user to provide it's own lifting inference rules. Those rules have to 1294be theorems of the form $G_1 \wedge \ldots \wedge G_n \Longrightarrow 1295G$, where all $G_i$ are guesses that might be universally quantified 1296and $G$ is a guess. Examples for such inference rules can be found in 1297Section~\ref{sec_lifting_guesses}. Usually, inferences look like 1298Lemma~\ref{lemma_guesses_lift_conj}. However, also rules like 1299Lemma~\ref{lemma_guesses_lift_forall_1} or 1300\ref{lemma_guesses_lift_forall_2} are supported. 1301 1302\begin{example} 1303When trying to add support for the Boolean operation of equivalence, 1304there are two choices. One can use rewriting and replace every 1305occurrence of $P_1 \Leftrightarrow P_2$ with for example $(P_1 \wedge 1306P_2) \vee (\neg P_1 \wedge \neg P_2)$. However, this may lead to an 1307exponential blowup of the size of the original term, since both $P_1$ 1308and $P_2$ occur twice in the result. Therefore, it is more efficient to 1309provide a new lifting inference for equivalences. Such a rule can easily be derived 1310using the existing rules for basic Boolean operations. 1311\end{example} 1312 1313\subsection{Oracle Guesses} 1314 1315Sometimes, the user does not want to justify guesses. The tactic 1316\texttt{QUANT\_TAC} is implemented using oracle guesses for example. 1317A simple interface to oracle guesses is provided by \texttt{oracle\_qp}. 1318It expects a ML function that given a variable and a term returns 1319an pair of an instantiation and the free variables in this instantiation. 1320 1321As an example, lets define a parameter that states that every list is non-empty: 1322{\scriptsize 1323\begin{verbatim} 1324val dummy_list_qp = oracle_qp (fn v => fn t => 1325 let 1326 val (v_name, v_list_ty) = dest_var v; 1327 val v_ty = listSyntax.dest_list_type v_list_ty; 1328 1329 val x = mk_var (v_name ^ "_hd", v_ty); 1330 val xs = mk_var (v_name ^ "_tl", v_list_ty); 1331 val x_xs = listSyntax.mk_cons (x, xs) 1332 in 1333 SOME (x_xs, [x, xs]) 1334 end) 1335\end{verbatim}} 1336 1337\noindent 1338Notice, that an option type is returned and that the function is 1339allowed to throw \texttt{HOL\_ERR} exceptions. 1340With this definition, the call 1341\begin{verbatim} 1342NORE_QUANT_INSTANTIATE_CONSEQ_CONV [dummy_list_qp] 1343 CONSEQ_CONV_STRENGTHEN_direction ``?x:'a list y:'b. P (x, y)`` 1344\end{verbatim} 1345results in 1346\verb+(?y x_hd x_tl. P (x_hd::x_tl,y)) ==> ?x y. P (x,y) : thm+. 1347 1348\subsection{User defined Quantifier Heuristics}\label{subsec_user_defined_quantheu} 1349 1350At the lowest level, our tool searches guesses using ML-functions 1351called \emph{quantifier heuristics}. Slightly simplified, such a 1352quantifier heuristic gets a variable and a term and returns a set of 1353guesses for this variable and term. Heuristics allow full 1354flexibility. However, to write your own heuristics a lot of knowledge 1355about the ML-datastructures and auxiliary functions is 1356required. Therefore, no details are discussed here. Please have a look 1357at the source code and contact Thomas Tuerk 1358(\url{tt291@cl.cam.ac.uk}), if you have questions. 1359\texttt{heuristics\_qp} and \texttt{top\_heuristics\_qp} provide 1360interfaces to add user defined heuristics to a quantifier heuristics 1361parameter. 1362 1363\chapter{Conclusion}\label{sec_conclusion} 1364 1365The quantifier heuristic is a powerful tool to instantiate quantifiers. 1366It subsumes the power of the existing unwind and satisfy libraries. More importantly though, 1367it is very flexible and easily extendable by the user. Moreover, 1368it can be used to instantiate quantifiers using unjustified guesses. 1369 1370\bibliographystyle{plain} 1371\bibliography{paper} 1372 1373\end{document}