E-matching is procedure for efficiently instantiating quantified theorem statements with ground terms that is widely employed in SMT solvers, 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.
E-matching adds new facts to the metaphorical whiteboard, based on an index of theorems.
When the whiteboard contains terms that match the index, the E-matching engine instantiates the corresponding theorems, and the resulting terms can feed further rounds of congruence closure, constraint propagation, and theory-specific solvers.
Each fact added to the whiteboard by E-matching is referred to as an instance.
Annotating theorems for E-matching, thus adding them to the index, is essential for enabling grind to make effective use of a library.
In addition to user-specified theorems, grind uses automatically generated equations for Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match-expressions as E-matching theorems.
Behind the scenes, the elaborator generates auxiliary functions that implement pattern matches, along with equational theorems that specify their behavior.
Using these equations with E-matching enables grind to reduce these instances of pattern matching.
The E-matching index is a table of patterns.
When a term matches one of the patterns in the table, grind attempts to instantiate and apply the corresponding theorem, giving rise to further facts and equalities.
Selecting appropriate patterns is an important part of using grind effectively: if the patterns are too restrictive, then useful theorems may not be applied; if they are too general, performance may suffer.
Consider the following functions and theorems:
def f (a : Nat) : Nat :=
a + 1
def g (a : Nat) : Nat :=
a - 1
@[grind =]
theorem gf (x : Nat) : g (f x) = x := x:Nat⊢ g (f x) = x
All goals completed! 🐙
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.
This proof goal does not include an instance of g (f x), but grind is nonetheless able to solve it:
example {a b} (h : f b = a) : g a = b := x:Nata✝:Natb✝:Nata:Natb:Nath:f b = a⊢ g a = b
All goals completed! 🐙
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 command Lean.Parser.Command.grind_patterngrind_pattern command can be used to manually select an E-matching pattern for a theorem.
Enabling the option trace.grind.ematch.instance causes grind print a trace message for each theorem instance it generates, which can be helpful when determining E-matching patterns.
command ::= ...
| `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`.
Associates a theorem with one or more patterns.
When multiple patterns are provided in a single Lean.Parser.Command.grind_patterngrind_pattern command, all of them must match a term before grind will attempt to instantiate the theorem.
The grind = attribute uses the left side of the equality as the E-matching pattern for gf:
def f (a : Nat) : Nat :=
a + 1
def g (a : Nat) : Nat :=
a - 1
@[grind =]
theorem gf (x : Nat) : g (f x) = x := x:Nat⊢ g (f x) = x
All goals completed! 🐙
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.
In this example, grind fails because the pattern is too restrictive: the goal does not contain the function symbol g.
example (h₁ : f b = a) (h₂ : f c = a) : b = c := b:Nata:Natc:Nath₁:f b = ah₂:f c = a⊢ b = c
b:Nata:Natc:Nath₁:f b = ah₂:f c = a⊢ b = c
Using just f x as the pattern allows grind to solve the goal automatically:
grind_pattern gf => f x
example {a b c} (h₁ : f b = a) (h₂ : f c = a) : b = c := a:Natb:Natc:Nath₁:f b = ah₂:f c = a⊢ b = c
All goals completed! 🐙
Enabling trace.grind.ematch.instance makes it possible to see the equalities found by E-matching:
example (h₁ : f b = a) (h₂ : f c = a) : b = c := b:Nata:Natc:Nath₁:f b = ah₂:f c = a⊢ b = c
set_option trace.grind.ematch.instance true in
All goals completed! 🐙
After E-matching, the proof succeeds because congruence closure equates g (f c) with g (f b), because both f b and f c are equal to a.
Thus, b and c must be in the same equivalence class.
When multiple patterns are specified together, all of them must match in the current context before grind attempts to instantiate the theorem.
This is referred to as a multi-pattern.
This is useful for lemmas such as transitivity rules, where multiple premises must be simultaneously present for the rule to apply.
A single theorem may be associated with multiple separate patterns by using multiple invocations of Lean.Parser.Command.grind_patterngrind_pattern or the @[grind _=_] attribute.
If any of these separate patterns match, the theorem will be instantiated.
R is a transitive binary relation over Int:
opaque R : Int → Int → Prop
axiom Rtrans {x y z : Int} : R x y → R y z → R x z
To use the fact that R is transitive, grind must already be able to satisfy both premises.
This is represented using a multi-pattern:
grind_pattern Rtrans => R x y, R y z
example {a b c d} : R a b → R b c → R c d → R a d := a:Intb:Intc:Intd:Int⊢ R a b → R b c → R c d → R a d
All goals completed! 🐙
The multi-pattern R x y, R y z instructs 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.
The grind attribute automatically generates an E-matching pattern or multi-pattern using a heuristic, instead of using Lean.Parser.Command.grindPattern : commandgrind_pattern to explicitly specify a pattern.
It includes a number of variants that select different heuristics.
The grind? attribute displays an info message showing the pattern which was selected—this is very helpful for debugging!
Patterns are subexpressions of theorem statements.
A subexpression is indexable if it has an indexable constant as its head, and it is said to cover one of the theorem's arguments if it fixes the argument's value.
Indexable constants are all constants other than Eq, HEq, Iff, And, Or, and Not.
The set of arguments that are covered by a pattern or multi-pattern is referred to as its coverage.
Some constants are lower priority than others; in particular, the arithmetic operators HAdd.hAdd, HSub.hSub, HMul.hMul, Dvd.dvd, HDiv.hDiv, and HMod.hMod have low priority.
An indexable subexpression is minimal if there is no smaller indexable subexpression whose head constant has at least as high priority.
attr ::= ... | grind grindMod?
The grind attribute automatically generates an E-matching pattern for a theorem, using a strategy determined by the provided modifier.
attr ::= ... | grind? grindMod?
The grind? displays the generated pattern.
Without any modifier, @[grind] traverses the conclusion and then the hypotheses from left to right, adding patterns as they increase the coverage, stopping when all arguments are covered.
grindMod ::= ... | →
@[grind →] selects a multi-pattern from the hypotheses of the theorem.
In other words, grind will use the theorem for forwards reasoning.
To generate a pattern, it traverses the hypotheses of the theorem from left to right. Each time it encounters a minimal indexable subexpression which covers an argument which was not previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
Although it is tempting to just use @[grind] by default, we recommend using one of the other forms when it achieves the desired effect.
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:
grindMod ::= ... | ←=
@[grind ←=] is unlike the other modifiers, and it used specifically for backwards reasoning on equality.
When a theorem's conclusion is an equality proposition and it is annotated with @[grind ←=], grind will instantiate it whenever the corresponding disequality is assumed—this is a consequence of the fact that grind performs all proofs by contradiction.
Ordinarily, the grind attribute does not consider the = symbol when generating patterns.
@[grind ←=] Attribute@[grind ext] Attribute
grind does not automatically apply the η-equality rule for structures.
Point is a structure with two fields:
structure Point where
x : Int
y : Int
By default, grind can't solve goals like this one:
example (p : Point) : p = ⟨p.x, p.y⟩ := p:Point⊢ p = { x := p.x, y := p.y } p:Point⊢ p = { x := p.x, y := p.y }
This kind of goal may come up when proving theorems like the fact that swapping the fields of a point twice is the identity:
def Point.swap (p : Point) : Point := ⟨p.y, p.x⟩
theorem swap_swap_eq_id : Point.swap ∘ Point.swap = id := ⊢ Point.swap ∘ Point.swap = id
⊢ ((fun p => { x := p.y, y := p.x }) ∘ fun p => { x := p.y, y := p.x }) = id
⊢ ((fun p => { x := p.y, y := p.x }) ∘ fun p => { x := p.y, y := p.x }) = id
Adding the @[grind ext] attribute to Point enables grind to solve both the original example and prove this theorem:
attribute [grind ext] Point
example (p : Point) : p = ⟨p.x, p.y⟩ := p:Point⊢ p = { x := p.x, y := p.y }
All goals completed! 🐙
theorem swap_swap_eq_id' : Point.swap ∘ Point.swap = id := ⊢ Point.swap ∘ Point.swap = id
⊢ ((fun p => { x := p.y, y := p.x }) ∘ fun p => { x := p.y, y := p.x }) = id
All goals completed! 🐙
The grind? attribute is a version of the grind attribute that additionally displays the generated pattern or multi-pattern.
Patterns and multi-patterns are displayed as lists of subexpressions, each of which is a pattern; ordinary patters are displayed as singleton lists.
In these displayed patterns, the names of defined constants are printed as-is.
When the theorem's parameters occur in the pattern, they are displayed using numbers rather than names.
In particular, they are numbered from right to left, starting at 0; this representation is referred as de Bruijn indices.
In order to use this proof that divisibility is transitive with grind, it requires E-matching patterns:
theorem div_trans {n k j : Nat} : n ∣ k → k ∣ j → n ∣ j := n:Natk:Natj:Nat⊢ n ∣ k → k ∣ j → n ∣ j
n:Natk:Natj:Natd₁:Natp₁:k = n * d₁d₂:Natp₂:j = k * d₂⊢ n ∣ j
exact ⟨d₁ * d₂, n:Natk:Natj:Natd₁:Natp₁:k = n * d₁d₂:Natp₂:j = k * d₂⊢ j = n * (d₁ * d₂) All goals completed! 🐙⟩
The right attribute to use is @[grind →], because there should be a pattern for each premise.
Using @[grind? →], it is possible to see which patterns are generated:
attribute [grind? →] div_trans
There are two:
Arguments are numbered from right to left, so #0 is the assumption that k ∣ j, while #4 is n.
Thus, these two patterns correspond to the terms n ∣ k and k ∣ j.
The rules for selecting patterns from subexpressions of the hypotheses and conclusion are subtle.
axiom p : Nat → Nat
axiom q : Nat → Nat
@[grind? →] theorem h₁ (w : 7 = p (q x)) : p (x + 1) = q x := sorry
The pattern is q x.
Counting from the right, parameter #0 is the premise w and parameter #1 is the implicit parameter x.
Why did @[grind →]? select q #1?
The attribute @[grind →] finds patterns by traversing the hypotheses (that is, parameters whose types are propositions) from left to right.
In this case, there's only a single hypothesis: 7 = p (q x).
The heuristic described above says that grind will search for a minimal indexable subexpression which covers a previously uncovered parameter.
There's just one uncovered parameter, namely x.
The whole hypothesis p (q x) = 7 can't be used because grind will not index on equality.
The right-hand side 7 is not helpful, because it doesn't determine the value of x.
p (q x) is not suitable 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, q x is selected as the pattern.
In this example, the Lean.Parser.Attr.grindMod← modifier indicates that the pattern should be found in the conclusion:
set_option trace.grind.debug.ematch.pattern true in
@[grind? ←] theorem h₂ (w : 7 = p (q x)) : p (x + 1) = q x := sorry
The left side of the equality is used because Eq is not indexable and HAdd.hAdd has lower priority than p.
In this example, two separate E-matching patterns are generated from the equality conclusion. One matches the left-hand side, and the other matches the right-hand side.
@[grind? _=_] theorem h₃ (w : 7 = p (q x)) : p (x + 1) = q x := sorry
The entire left side of the equality is used instead of just x + 1 because HAdd.hAdd has lower priority than p.
Without any modifiers, @[grind] produces a multipattern by first checking the conclusion and then the premises:
@[grind?] theorem h₄ (w : p x = q y) : p (x + 2) = 7 := sorry
Here, argument x is #2, y is #1, and w is #0.
The resulting multipattern contains the left-hand side of the equality, which is the only minimal indexable subexpression of the conclusion that covers an argument (namely x).
It also contains q y, which is the only minimal indexable subexpression of the hypothesis w that covers an additional argument (namely y).
In this example, pattern generation fails because the theorem's conclusion doesn't mention the the argument y.
@[grind? ←] theorem h₅ (w : p x = q y) : p (x + 2) = 7 := sorry
In this example, the pattern is generated by traversing the premises from left to right, followed by the conclusion:
@[grind? =>] theorem h₆
(_ : q (y + 2) = q y)
(_ : q (y + 1) = q y) :
p (x + 2) = 7 :=
sorry
In the patterns, y is argument #3 and x is argument #2, because automatic implicit parameters are inserted from left to right and y occurs before x in the theorem statement.
The premises are arguments #1 and #0.
In the resulting multipattern, y is covered by a subexpression of the first premise, and z is covered by a subexpression of the conclusion:
E-matching can generate an unbounded number of theorem instances.
For the sake of both efficiency and termination, grind limits the number of times that E-matching can run using two mechanisms:
Each term is assigned a generation, and terms produced by E-matching have a generation that is one greater than the maximal generation of all the terms used to instantiate the theorem.
E-matching only considers terms whose generation is beneath a configurable threshold.
The gen option to grind controls the generation threshold.
Each invocation of the E-matching engine is referred to as a round.
Only a limited number of rounds of E-matching are performed.
The ematch option to grind controls the round limit.
E-matching can generate too many theorem instances. Some patterns may even generate an unbounded number of instances.
In this example, s_eq is added to the index with the pattern s x:
def s (x : Nat) := 0
@[grind? =] theorem s_eq (x : Nat) : s x = s (x + 1) :=
rfl
Attempting to use this theorem results in many facts about s applied to concrete values being generated.
In particular, s_eq is instantiated with a new Nat in each of the five rounds.
First, grind instantiates s_eq with x := 0, which generates the term s 1.
This matches the pattern s x, and is thus used to instantiate s_eq with x := 1, which generates the term s 2,
and so on until the round limit is reached.
example : s 0 > 0 := ⊢ s 0 > 0
⊢ s 0 > 0
Increasing the round limit to 20 causes E-matching to terminate due to the default generation limit of 8:
example : s 0 > 0 := ⊢ s 0 > 0
⊢ s 0 > 0
iota returns the list of all numbers strictly less than its argument, and the theorem iota_succ describes its behavior on Nat.succ:
def iota : Nat → List Nat
| 0 => []
| n + 1 => n :: iota n
@[grind =] theorem iota_succ : iota (n + 1) = n :: iota n :=
rfl
The fact that (iota 20).length > 10 can be proven by repeatedly instantiating iota_succ and List.length_cons.
However, grind does not succeed:
example : (iota 20).length > 10 := ⊢ (iota 20).length > 10
⊢ (iota 20).length > 10
Due to the limited number of E-matching rounds, the chain of instantiations is not completed.
Increasing these limits allows grind to succeed:
example : (iota 20).length > 10 := ⊢ (iota 20).length > 10
All goals completed! 🐙
When the option diagnostics is set to true, grind displays the number of instances that it generates for each theorem.
This is useful to detect theorems that contain patterns that are triggering too many instances.
In this case, the diagnostics show that iota_succ is instantiated 14 times:
set_option diagnostics true in
example : (iota 20).length > 10 := ⊢ (iota 20).length > 10
All goals completed! 🐙
By default, grind uses automatically generated equations for Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match-expressions as E-matching theorems.
This can be disabled by setting the matchEqs flag to false.
Enabling diagnostics shows that grind uses one of the equations of the auxiliary matching function during E-matching:
theorem gt1 (x y : Nat) :
x = y + 1 →
0 < match x with
| 0 => 0
| _ + 1 => 1 := x:Naty:Nat⊢ x = y + 1 →
0 <
match x with
| 0 => 0
| n.succ => 1
set_option diagnostics true in
All goals completed! 🐙
The theorem has this type:
#check gt1.match_1.congr_eq_2
Disabling the use of matcher function equations causes the proof to fail:
example (x y : Nat)
: x = y + 1 →
0 < match x with
| 0 => 0
| _+1 => 1 := x:Naty:Nat⊢ x = y + 1 →
0 <
match x with
| 0 => 0
| n.succ => 1
x:Naty:Nat⊢ x = y + 1 →
0 <
match x with
| 0 => 0
| n.succ => 1
trace.grind.ematch.instance
Default value: false
enable/disable tracing for the given module and submodules
