HOL: Description

The Quantifier Heuristics Library

Motivation

Often interactive proofs can be simplified by instantiating quantifiers. The Unwind library, which is part of the simplifier, allows instantiations of “trivial” quantifiers: $$ \forall x_1\ \ldots x_i \ldots x_n.\ P_1 \wedge \ldots \wedge x_i = c \wedge \ldots \wedge P_n \Longrightarrow Q $$ and $$ \exists x_1\ \ldots x_i \ldots x_n.\ P_1 \wedge \ldots \wedge x_i = c \wedge \ldots \wedge P_n $$ can be simplified by instantiating $x_i$ with $c$. Because unwind-conversions are part of bool_ss, they are used with nearly every call of the simplifier and often simplify proofs considerably. However, the Unwind library can only handle these common cases. If the term structure is only slightly more complicated, it fails. For example, $\exists x.\ P(x) \Longrightarrow (x = 2) \wedge Q(x)$ cannot be tackled.

There is also the Satisfy library, which uses unification to show existentially quantified formulas. It can handle problems like $\exists x.\ P_1(x,c_1)\ \wedge \ldots P_n(x,c_n)$ if given theorems of the form $\forall x\ c.\ P_i(x, c)$. This is often handy, but still rather limited.

The quantifier heuristics library (quantHeuristicsLib) provides more power and flexibility. A few simple examples of what it can do are shown in Table 8.14.1. Besides the power demonstrated by these examples, the library is highly flexible as well. At its core, there is a modular, syntax driven search for instantiation. This search consists of a collection of interleaved heuristics. Users can easily configure existing heuristics and add own ones. Thereby, it is easy to teach the library about new predicates, logical connectives or datatypes.

Table: Examples.

User Interface

The quantifier heuristics library can be found in the sub-directory src/quantHeuristics. The entry point to the framework is the library quantHeuristicsLib.

Conversions

Usually the library is used for converting a term containing quantifiers to an equivalent one. For this, the following high-level entry points exists:

All these functions get a list of quantifier heuristic parameters as arguments. These parameters essentially configure which heuristics are used during the guess-search. If an empty list is provided, the tools know about the standard Boolean combinators, equations and context. std_qp adds support for common datatypes like pairs or lists. Quantifier heuristic parameters are explained in more detail in Section 8.14.4.

So, some simple usage of the quantifier heuristic library looks like:

- QUANT_INSTANTIATE_CONV [] ``?x. (!z. Q z /\ (x=7)) /\ P x``;
> val it = |- (?x. (!z. Q z /\ (x = 7)) /\ P x) <=> (!z. Q z) /\ P 7: thm

- QUANT_INSTANTIATE_CONV [std_qp] ``!x. IS_SOME x ==> P x``
> val it = |- (!x. IS_SOME x ==> P x) <=> !x_x'. P (SOME x_x'): thm

Usually, the quantifier heuristics library is used together with the simplifier using QUANT_INST_ss. Besides interleaving simplification and quantifier instantiation, this has the benefit of being able to use context information collected by the simplifier:

- QUANT_INSTANTIATE_CONV [] ``P m ==> ?n. P n``
Exception- UNCHANGED raised

- SIMP_CONV (bool_ss ++ QUANT_INST_ss []) [] ``P m ==> ?n. P n``
> val it = |- P m ==> (?n. P n) <=> T: thm

It's usually best to use QUANT_INST_ss together with e.g. SIMP_TAC when using the library with tactics. However, if free variables of the goal should be instantiated, then ASM_QUANT_INSTANTIATE_TAC should be used:

P x
------------------------------------
  IS_SOME x
  : proof

- e (ASM_QUANT_INSTANTIATE_TAC [std_qp])
> P (SOME x_x') : proof

There is also QUANT_INSTANTIATE_TAC. This tactic does not instantiate free variables. Neither does it take assumptions into consideration. It is just a shortcut for using QUANT_INSTANTIATE_CONV as a tactic.

Unjustified Guesses

Most heuristics justify the guesses they produce and therefore allow to prove equivalences of e.g. the form $\exists x.\ P(x) \Leftrightarrow P(i)$. However, the implementation also supports unjustified guesses, which may be bogus. Let's consider e.g. the formula $\exists x.\ P(x) \Longrightarrow (x = 2)\ \wedge\ Q(x)$. Because nothing is known about $P$ and $Q$, we can't find a safe instantiation for $x$ here. However, $2$ looks tempting and is probably sensible in many situations. (Counterexample: $P(2)$, $\neg Q(2)$ and $\neg P(3)$ hold.)

implication_concl_qp is a quantifier parameter that looks for valid guesses in the conclusion of an implication. Then, it assumes without justification that these guesses are probably sensible for the whole implication as well. Because these guesses might be wrong, one can either use implications or expansion theorems like $\exists x.\ P(x)\ \Longleftrightarrow (\forall x.\ x \neg c \Rightarrow \neg P(x)) \Rightarrow P(c)$.

- QUANT_INSTANTIATE_CONV [implication_concl_qp]
     ``?x. P x ==> (x = 2) /\ Q x``
Exception- UNCHANGED raised

- QUANT_INSTANTIATE_CONSEQ_CONV [implication_concl_qp]
     CONSEQ_CONV_STRENGTHEN_direction
     ``?x. P x ==> (x = 2) /\ Q x``
> val it =
   |- (P 2 ==> Q 2) ==> ?x. P x ==> (x = 2) /\ Q x: thm

- EXPAND_QUANT_INSTANTIATE_CONV [implication_concl_qp]
    ``?x. P x ==> (x = 2) /\ Q x``
> val it = |- (?x. P x ==> (x = 2) /\ Q x) <=>
              (!x. x <> 2 ==> ~(P x ==> (x = 2) /\ Q 2)) ==> P 2 ==> Q 2

- SIMP_CONV (std_ss++EXPAND_QUANT_INST_ss [implication_concl_qp]) []
    ``?x. P x ==> (x = 2) /\ Q x``
> val it =
   |- (?x. P x ==> (x = 2) /\ Q x) <=>
      (!x. x <> 2 ==> P x) ==> P 2 ==> Q 2: thm

The following entry points should be used to exploit unjustified guesses:

Explicit Instantiations

A special (degenerated) use of the framework is turning guess search off completely and providing instantiations explicitly. The tactic QUANT_TAC allows this. This means that it allows to partially instantiate quantifiers at subpositions with explicitly given terms. As such, it can be seen as a generalisation of EXISTS_TAC.

- val it = !x. (!z. P x z) ==> ?a b.    Q a        b z : proof

> e( QUANT_INST_TAC [("z", `0`, []), ("a", `SUC a'`, [`a'`])] )
- val it = !x. (    P x 0) ==> ?  b a'. Q (SUC a') b z : proof

This tactic is implemented using unjustified guesses. It normally produces implications, which is fine when used as a tactic. There is also a conversion called INST_QUANT_CONV with the same functionality. For a conversion, implications are problematic. Therefore, the simplifier and Metis are used to prove the validity of the explicitly given instantiations. This succeeds only for simple examples.

Simple Quantifier Heuristics

The full quantifier heuristics described above are powerful and very flexible. However, they are sometimes slow. The unwind library¹ on the other hand is limited, but fast. The simple version of the quantifier heuristics fills the gap in the middle. They just search for gap guesses without any free variables. Moreover, slow operations like recombining or automatically looking up datatype information is omitted. As a result, the conversion SIMPLE_QUANT_INSTANTIATE_CONV (and corresponding SIMPLE_QUANT_INST_ss) is nearly as fast as the corresponding unwind conversions. However, it supports more complicated syntax. Moreover, there is support for quantifiers, pairs, list and much more.

Quantifier Heuristic Parameters

Quantifier heuristic parameters play a similar role for the quantifier instantiation library as simpsets do for the simplifier. They contain theorems, ML code and general configuration parameters that allow to configure guess-search. There are predefined parameters that handle common constructs and the user can define own parameters.

Quantifier Heuristic Parameters for Common Datatypes

There are option_qp, list_qp, num_qp and sum_qp for option types, lists, natural numbers and sum types respectively. Some examples are displayed in the following table:

$$ \begin{array}{r@{\quad \Longleftrightarrow \quad}l} \forall x.\ \holtxt{IS\_SOME}(x) \Rightarrow P(x) & \forall x'.\ P (\holtxt{SOME}(x')) \\ \forall x.\ \holtxt{IS\_NONE}(x)& \textit{false} \\ \forall l.\ l \neq [\,] \Rightarrow P(l)& \forall h, l'.\ P(h::l') \\ \forall x.\ x = c + 3& \textit{false} \\ \forall x.\ x \neq 0 \Rightarrow P(x)& \forall x'.\ P(\holtxt{SUC}(x')) \end{array} $$

Quantifier Heuristic Parameters for Tuples

For tuples the situation is peculiar, because each quantifier over a variable of a product type can be instantiated. The challenge is to decide which quantifiers should be instantiated and which new variable names to use for the components of the pair.

There is a quantifier heuristic parameter called pair_default_qp. It first looks for subterms of the form $(\lambda (x_1, \ldots, x_n).\ \ldots)\ x$. If such a term is found $x$ is instantiated with $(x_1, \ldots, x_n)$. Otherwise, subterms of the form $\holtxt{FST}(x)$ and $\holtxt{SND}(x)$ are searched. If such a term is found, $x$ is instantiated as well. This parameter therefore allows simplifications like:

$$ \begin{array}{r@{\quad \Longleftrightarrow \quad}l} \forall p.\ (x = \holtxt{SND}(p)) \Rightarrow P(p)& \forall p_1.\ P(p_1, x) \\ \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) \end{array} $$

pair_default_qp is implemented in terms of the more general quantifier heuristic parameter pair_qp, which allows the user to provide a list of ML functions. These functions get the variable and the term. If they return a tuple of variables, these variables are used for the instantiation, otherwise the next function in the list is called or — if there is no function left — the variable is not instantiated. In the example of $\exists p.\ (\lambda (p_a, p_b, p_c). P(p_a, p_b, p_c))\ p$ these functions are given the variable $p$ and the term $(\lambda (p_a, p_b, p_c). P(p_a, p_b, p_c))\ p$ and return $\holtxt{SOME} (p_a, p_b, p_c)$. This simple ML interface gives the user full control over what quantifier over product types to expand and how to name the new variables.

Quantifier Heuristic Parameter for Records

Records are similar to pairs, because they can always be instantiated. Here, it is interesting that the necessary monochotomy lemma comes from HOL 4's Type_Base library. This means that record_qp is stateful. If a new record type is defined, the automatically proven monochotomy lemma is then automatically used by record_qp. In contrast to the pair parameter, the one for records gets only one function instead of a list of functions to decide which variables to instantiate. However, this function is simpler, because it just needs to return true or false. The names of the new variables are constructed from the field-names of the record. The quantifier heuristic parameter default_record_qp expands all records.

Stateful Quantifier Heuristic Parameters

The parameter for records is stateful, as it uses knowledge from Type_Base. Such information is not only useful for records but for general datatypes. The quantifier heuristic parameter TypeBase_qp uses automatically proven theorems about new datatypes to exploit mono- and dichotomies. Moreover, there is also a stateful pure_stateful_qp that allows the user to explicitly add other parameters to it. stateful_qp is a combination of pure_stateful_qp and TypeBase_qp.

Standard Quantifier Heuristic Parameter

The standard quantifier heuristic parameter std_qp combines the parameters for lists, options, natural numbers, the default one for pairs and the default one for records.

User defined Quantifier Heuristic Parameters

The user is also able to define own parameters. There is empty_qp, which does not contain any information. Several parameters can be combined using combine_qps. Together with the basic types of user defined parameters that are explained below, these functions provide an interface for user defined quantifier heuristic parameters.

Rewrites / Conversions

A very powerful, yet simple technique for teaching the guess search about new constructs are rewrite rules. For example, the standard rules for equations and basic logical operations cannot generate guesses for the predicate IS_SOME. By rewriting IS_SOME(x) to ?x'. x = SOME(x'), however, these rules fire.

option_qp uses this rewrite to implement support for IS_SOME. Similarly support for predicates like NULL is implemented using rewrites. Even adding rewrites like $\mathsf{append}(l_1, l_2) = [\,] \Longleftrightarrow (l_1 = [\,]\ \wedge\ l_2 = [\,])$ for list-append turned out to be beneficial in practice.

rewrite_qp allows to provide rewrites in the form of rewrite theorems. For the example of IS_SOME this looks like:

> val thm = QUANT_INSTANTIATE_CONV [] ``!x. IS_SOME x ==> P x``
Exception- UNCHANGED raised

> val IS_SOME_EXISTS = prove (``IS_SOME x = (?x'. x = SOME x')``,
   Cases_on `x` THEN SIMP_TAC std_ss []);
val IS_SOME_EXISTS = |- IS_SOME x <=> ?x'. x = SOME x': thm

> val thm = QUANT_INSTANTIATE_CONV [rewrite_qp[IS_SOME_EXISTS]]
    ``!x. IS_SOME x ==> P x``
val thm = |- (!x. IS_SOME x ==> P x) <=>
             !x'. IS_SOME (SOME x') ==> P (SOME x'): thm

To clean up the result after instantiation, theorems used to rewrite the result after instantiation can be provided via final_rewrite_qp.

> val thm = QUANT_INSTANTIATE_CONV [rewrite_qp[IS_SOME_EXISTS],
                                    final_rewrite_qp[option_CLAUSES]]
      ``!x. IS_SOME x ==> P x``
val thm = |- (!x. IS_SOME x ==> P x) <=> !x'. P (SOME x'): thm

If rewrites are not enough, conv_qp can be used to add conversions:

- val thm = QUANT_INSTANTIATE_CONV [] ``?x. (\y. y = 2) x``
Exception- UNCHANGED raised

- val thm = QUANT_INSTANTIATE_CONV [convs_qp[BETA_CONV]] ``?x. (\y. y = 2) x``
> val thm = |- (?x. (\y. y = 2) x) <=> T: thm

Strengthening / Weakening

In rare cases, equivalences that can be used for rewrites are unavailable. There might be just implications that can be used for strengthening or weakening. The function imp_qp might be used to provide such implication.

- val thm = QUANT_INSTANTIATE_CONV [list_qp] ``!l. 0 < LENGTH l ==> P l``
Exception- UNCHANGED raised

- val LENGTH_LESS_IMP = prove (``!l n. n < LENGTH l ==> l <> []``,
    Cases_on `l` THEN SIMP_TAC list_ss []);
> val LENGTH_LESS_IMP = |- !l n. n < LENGTH l ==> l <> []: thm

- val thm = QUANT_INSTANTIATE_CONV [imp_qp[LENGTH_LESS_IMP], list_qp]
    ``!l. 0 < LENGTH l ==> P l``
> val thm =
   |- (!l. 0 < LENGTH l ==> P l) <=>
      !l_t l_h. 0 < LENGTH (l_h::l_t) ==> P (l_h::l_t): thm

- val thm = SIMP_CONV (list_ss ++
              QUANT_INST_ss [imp_qp[LENGTH_LESS_IMP], list_qp]) []
              ``!l. SUC (SUC n) < LENGTH l ==> P l``
> val thm =
   |- (!l. SUC (SUC n) < LENGTH l ==> P l) <=>
      !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

Filtering

Sometimes, one might want to avoid to instantiate certain quantifiers. The function filter_qp allows to add ML-functions that filter the handled quantifiers. These functions are given a variable $x$ and a term $P(x)$. The tool only tries to instantiate $x$ in $P(x)$, if all filter functions return true.

- val thm = QUANT_INSTANTIATE_CONV []
     ``?x y z. (x = 1) /\ (y = 2) /\ (z = 3) /\ P (x, y, z)``
> val thm = |- (?x y z. (x = 1) /\ (y = 2) /\ (z = 3) /\ P (x,y,z)) <=>
               P (1,2,3): thm

- val thm = QUANT_INSTANTIATE_CONV
     [filter_qp [fn v => fn t => (v = ``y:num``)]]
     ``?x y z. (x = 1) /\ (y = 2) /\ (z = 3) /\ P (x, y, z)``
> val thm = |- (?x y z. (x = 1) /\ (y = 2) /\ (z = 3) /\ P (x,y,z)) <=>
                ?x   z. (x = 1) /\            (z = 3) /\ P (x,2,z): thm

Satisfying and Contradicting Instantiations

As the satisfy library demonstrates, it is often useful to use unification and explicitly given theorems to find instantiations. In addition to satisfying instantiations, the quantifier heuristics framework is also able to use contradicting ones. The theorems used for finding instantiations usually come from the context. However, instantiation_qp allows to add additional ones:

> val thm = SIMP_CONV (std_ss++QUANT_INST_ss[]) []
    ``P n ==> ?m:num. n <= m /\ P m``
Exception- UNCHANGED raised

> val thm = SIMP_CONV (std_ss++
               QUANT_INST_ss[instantiation_qp[LESS_EQ_REFL]]) []
               ``P n ==> ?m:num. n <= m /\ P m``
> val thm = |- P n ==> ?m:num. n <= m /\ P m = T : thm

Di- and Monochotomies

Dichotomies can be exploited for guess search. distinct_qp provides an interface to add theorems of the form $\forall x.\ c_1(x) \neq c_2(x)$. cases_qp expects theorems of the form $\forall x. \ (x = \exists \mathit{fv}. c_1(\mathit{fv}))\ \vee \ldots \vee (x = \exists \mathit{fv}. c_n(\mathit{fv}))$. However, only theorems for $n = 2$ and $n = 1$ are used. All other cases are currently ignored.

Oracle Guesses

Sometimes, the user does not want to justify guesses. The tactic QUANT_TAC is implemented using oracle guesses for example. A simple interface to oracle guesses is provided by oracle_qp. It expects a ML function that given a variable and a term returns a pair of an instantiation and the free variables in this instantiation.

As an example, let's define a parameter that states that every list is non-empty:

   val dummy_list_qp = oracle_qp (fn v => fn t =>
     let
        val (v_name, v_list_ty) = dest_var v;
        val v_ty = listSyntax.dest_list_type v_list_ty;

        val x = mk_var (v_name ^ "_hd", v_ty);
        val xs = mk_var (v_name ^ "_tl", v_list_ty);
        val x_xs = listSyntax.mk_cons (x, xs)
     in
        SOME (x_xs, [x, xs])
     end)

Notice, that an option type is returned and that the function is allowed to throw HOL_ERR exceptions. With this definition, we get

- NORE_QUANT_INSTANTIATE_CONSEQ_CONV [dummy_list_qp]
    CONSEQ_CONV_STRENGTHEN_direction ``?x:'a list y:'b. P (x, y)``
> val it = ?y x_hd x_tl. P (x_hd::x_tl,y)) ==> ?x y. P (x,y) : thm

Lifting Theorems

The function inference_qp enables the user to provide theorems that allow lifting guesses over user defined connectives. As writing these lifting theorems requires deep knowledge about guesses, it is not discussed here. Please have a look at the detailed documentation of the quantifier heuristics library as well as its sources. You might also want to contact Thomas Tuerk (tt291@cl.cam.ac.uk).

User defined Quantifier Heuristics

At the lowest level, the tool searches guesses using ML-functions called quantifier heuristics. Slightly simplified, such a quantifier heuristic gets a variable and a term and returns a set of guesses for this variable and term. Heuristics allow full flexibility. However, to write your own heuristics a lot of knowledge about the ML-datastructures and auxiliary functions is required. Therefore, no details are discussed here. Please have a look at the source code and contact Thomas Tuerk (tt291@cl.cam.ac.uk), if you have questions. heuristics_qp and top_heuristics_qp provide interfaces to add user defined heuristics to a quantifier heuristics parameter.

1. see src/simp/src/Unwind.sml ↩