17.8. E‑matching

E-matching is a mechanism used by grind to instantiate theorems efficiently. It is especially effective when combined with congruence closure, enabling grind to discover non-obvious consequences of equalities and annotated theorems automatically.

Consider the following functions and theorems:

The theorem gf asserts that g (f x) = x for all natural numbers x. The attribute [grind =] instructs grind to use the left-hand side of the equation, g (f x), as a pattern for heuristic instantiation via E-matching. Suppose we now have a goal involving:

Although g a is not an instance of the pattern g (f x), it becomes one modulo the equation f b = a. By substituting a with f b in g a, we obtain the term g (f b), which matches the pattern g (f x) with the assignment x := b. Thus, the theorem gf is instantiated with x := b, and the new equality g (f b) = b is asserted. grind then uses congruence closure to derive the implied equality g a = g (f b) and completes the proof.

The pattern used to instantiate theorems affects the effectiveness of grind. For example, the pattern g (f x) is too restrictive in the following case: the theorem gf will not be instantiated because the goal does not even contain the function symbol g.

You can use the command grind_pattern to manually select a pattern for a given theorem. In the following example, we instruct grind to use f x as the pattern, allowing it to solve the goal automatically:

You can enable the option trace.grind.ematch.instance to make grind print a trace message for each theorem instance it generates.

You can also specify a multi-pattern to control when grind should instantiate a theorem. A multi-pattern requires that all specified patterns are matched in the current context before the theorem is instantiated. This is useful for lemmas such as transitivity rules, where multiple premises must be simultaneously present for the rule to apply. The following example demonstrates this feature using a transitivity axiom for a binary relation R:

By specifying the multi-pattern R x y, R y z, we instruct grind to instantiate Rtrans only when both R x y and R y z are available in the context. In the example, grind applies Rtrans to derive R a c from R a b and R b c, and can then repeat the same reasoning to deduce R a d from R a c and R c d.

Instead of using grind_pattern to explicitly specify a pattern, you can use the @[grind] attribute or one of its variants, which will use a heuristic to generate a (multi-)pattern. The @[grind?] attribute displays an info message showing the pattern which was selected—this is very helpful for debugging!

• @[grind →] will select a multi-pattern from the hypotheses of the theorem (i.e. it will use the theorem for forwards reasoning). In more detail, it will traverse the hypotheses of the theorem from left-to-right, and each time it encounters a minimal indexable (i.e. has a constant as its head) subexpression which "covers" (i.e. fixes the value of) an argument which was not previously covered, it will add that subexpression as a pattern, until all arguments have been covered. This rule is described in more detail below.

• @[grind ←] will select a multi-pattern from the conclusion of theorem (i.e. it will use the theorem for backwards reasoning). This may fail if not all the arguments to the theorem appear in the conclusion.

• @[grind] will traverse the conclusion and then the hypotheses left-to-right, adding patterns as they increase the coverage, stopping when all arguments are covered.

• @[grind =] checks that the conclusion of the theorem is an equality, and then uses the left-hand-side of the equality as a pattern. This may fail if not all of the arguments appear in the left-hand-side.

• @[grind =_] is like @[grind =], but using the right-hand-side of the equality.

• @[grind _=_] acts like a macro which expands to @[grind =, grind =_] (i.e. it will add two multipatterns, allowing the equality theorem to trigger in either direction).

Although it is tempting to just use @[grind] by default, we recommend that when one of the other forms achieves the desired effect, you use those. In every case, it is worthwhile to verify the chosen pattern using @[grind?] (which accepts all of these modifiers).

There are also three less commonly used modifiers:

• @[grind =>] traverses all the hypotheses left-to-right and then the conclusion.

• @[grind <=] traverses the conclusion and then all hypotheses right-to-left.

• @[grind ←=] is unlike the others, and it used specifically for backwards reasoning on equality. As an example, suppose we have a theorem

  theorem declaration uses 'sorry'inv_eq [One α] [Mul α] [Inv α] {a b : α} (w : a * b = 1) : a⁻¹ = b := sorry

  Adding @[grind ←=] will cause this theorem to be instantiated whenever we are trying to prove a⁻¹ = b, i.e. whenever we have the disequality a⁻¹ ≠ b (recall grind proves goals by contradiction). Without special support via ←= this instantiation would be not possible as grind does not consider the = symbol while generating patterns.

The rule for selecting patterns from subexpressions of the hypotheses and conclusion as described above is subtle, so we'll give some examples.

First, to understand the output we need to recall that the #n appearing in patterns are arguments of the theorem, numbered as de-Bruijn variables, i.e. in reverse order (so #0 would be w : p (q x) = 7, while #1 is the implicit argument x).

Why was q #1 selected when we use @[grind →]? The attribute @[grind →] instructed grind to find patterns by traversing the hypotheses from left-to-right. In this case, there's only the one hypothesis p (q x) = 7. The heuristic described above says that grind will search for a minimal indexable subexpression which covers a previously uncovered argument. There's just one uncovered argument, x, so we're looking for a minimal expression containing that. We can't take the whole p (q x) = 7 because grind will not index on equality. The right-hand-side 7 is not helpful, because it doesn't determine the value of x. We don't take p (q x) because it is not minimal: it has q x inside of it, which is indexable (its head is the constant q), and it determines the value of x. The expression q x itself is minimal, because x is not indexable. Thus grind selects q x as the pattern.

Let's see some more examples:

If you're planning to do substantial annotation work, you should study these examples and verify that they follow the rules described above.

E-matching can generate too many theorem instances. Some patterns may even generate an unbounded number of instances. For example, consider the pattern s x in the following example.

In the example above, grind instantiates s_eq with x := 0 which generates the term s 1 with is then used to instantiate s_eq with x := 1 which generates the term s 2 and so on. The instantiation process is interrupted using the generation threshold. Terms occurring in the input goal have generation zero. When grind instantiates a theorem using terms with generation ≤ n, the new generated terms have generation n+1. You can set the maximum generation using the option grind (gen := <num>). You can also control the number of E-matching rounds using the option grind (ematch := <num>). In the following example, we prove that (iota 20).length > 10 by instantiating iota_succ and List.length_cons

You can set the option set_option diagnostics true to obtain the number of theorem instances generated by grind per theorem. This is useful to detect theorems that contain patterns that are triggering too many instances.

By default, grind uses that automatically generated equations for match-expressions as E-matching theorems.

You can disable this feature by using grind -matchEqs