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 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 ::= ...
| Marks a theorem or definition for use by the `grind` tactic.
An optional modifier (e.g. `=`, `→`, `←`, `cases`, `intro`, `ext`, `inj`, etc.)
controls how `grind` uses the declaration:
* whether it is applied forwards, backwards, or both,
* whether equalities are used on the left, right, or both sides,
* whether case-splits, constructors, extensionality, or injectivity are applied,
* or whether custom instantiation patterns are used.
See the individual modifier docstrings for details.
The grind attribute automatically generates an E-matching pattern for a theorem, using a strategy determined by the provided modifier.
If no modifier is provided, then grind suggests suitable modifiers, displaying the resulting patterns.
attr ::= ...
| Like `@[grind]`, but enforces the **minimal indexable subexpression condition**:
when several subterms cover the same free variables, `grind!` chooses the smallest one.
This influences E-matching pattern selection.
### Example
```lean
theorem fg_eq (h : x > 0) : f (g x) = x
@[grind <-] theorem fg_eq (h : x > 0) : f (g x) = x
-- Pattern selected: `f (g x)`
-- With minimal subexpression:
@[grind! <-] theorem fg_eq (h : x > 0) : f (g x) = x
-- Pattern selected: `g x`
The grind! attribute automatically generates an E-matching pattern for a theorem, using a strategy determined by the provided modifier.
It additionally enforces the condition that the selected pattern(s) should be minimal indexable subexpressions.
attr ::= ...
| Like `@[grind]`, but also prints the pattern(s) selected by `grind`
as info messages. Useful for debugging annotations and modifiers.
The grind? displays the pattern that was generated.
attr ::= ...
| Like `@[grind!]`, but also prints the pattern(s) selected by `grind`
as info messages. Combines minimal subexpression selection with debugging output.
The grind!? attribute is equivalent to grind!, except it displays the resulting pattern for inspection.
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.
This default strategy can be explicitly requested using the Lean.Parser.Attr.grindDefThe `.` modifier instructs `grind` to select a multi-pattern by traversing the conclusion of the
theorem, and then the hypotheses from eft to right. We say this is the default modifier.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
. modifier.
In addition to using the default strategy, the attribute checks which other strategies could be applied, and displays all of the resulting patterns.
grindMod ::= ...
| The `.` modifier instructs `grind` to select a multi-pattern by traversing the conclusion of the
theorem, and then the hypotheses from eft to right. We say this is the default modifier.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
grindMod ::= ...
| The `.` modifier instructs `grind` to select a multi-pattern by traversing the conclusion of the
theorem, and then the hypotheses from eft to right. We say this is the default modifier.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
The . modifier instructs grind to select a multi-pattern by traversing the conclusion of the
theorem, and then the hypotheses from eft to right. We say this is the default modifier.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If grind! is used, then only minimal indexable subexpressions are considered.
grindMod ::= ...
| The `=` modifier instructs `grind` to check 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.
The = modifier instructs grind to check 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.
grindMod ::= ...
| The `=_` modifier instructs `grind` to check that the conclusion of the theorem is an equality,
and then uses the right-hand side of the equality as a pattern. This may fail if not all of the arguments appear
in the right-hand side.
The =_ modifier instructs grind to check that the conclusion of the theorem is an equality,
and then uses the right-hand side of the equality as a pattern. This may fail if not all of the arguments appear
in the right-hand side.
grindMod ::= ...
| The `_=_` modifier acts like a macro which expands to `=` and `=_`. It adds two patterns,
allowing the equality theorem to trigger in either direction.
The _=_ modifier acts like a macro which expands to = and =_. It adds two patterns,
allowing the equality theorem to trigger in either direction.
grindMod ::= ...
| The `→` modifier instructs `grind` to select 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 subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
The → modifier instructs grind to select 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 subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If grind! is used, then only minimal indexable subexpressions are considered.
grindMod ::= ...
| The `←` modifier instructs `grind` to select a multi-pattern from the conclusion of theorem.
In other words, `grind` will use the theorem for backwards reasoning.
This may fail if not all of the arguments to the theorem appear in the conclusion.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
The ← modifier instructs grind to select a multi-pattern from the conclusion of theorem.
In other words, grind will use the theorem for backwards reasoning.
This may fail if not all of the arguments to the theorem appear in the conclusion.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If grind! is used, then only minimal indexable subexpressions are considered.
It is important to inspect the patterns generated by the @[grind] attribute to ensure that they match the correct parts of the lemma.
If the pattern is too strict, the lemma will not be applied in situations where it would be relevant, leading to less automation.
If it is too general, then performance will suffer as the lemma is tried in many situations where it is not helpful.
There are also three less commonly used modifiers for lemmas:
grindMod ::= ...
| The `⇒` modifier instructs `grind` to select a multi-pattern by traversing all the hypotheses from
left to right, followed by the conclusion.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
grindMod ::= ...
| The `⇒` modifier instructs `grind` to select a multi-pattern by traversing all the hypotheses from
left to right, followed by the conclusion.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
The ⇒ modifier instructs grind to select a multi-pattern by traversing all the hypotheses from
left to right, followed by the conclusion.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If grind! is used, then only minimal indexable subexpressions are considered.
grindMod ::= ...
| The `⇐` modifier instructs `grind` to select a multi-pattern by traversing the conclusion, and then
all the hypotheses from right to left.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
grindMod ::= ...
| The `⇐` modifier instructs `grind` to select a multi-pattern by traversing the conclusion, and then
all the hypotheses from right to left.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
The ⇐ modifier instructs grind to select a multi-pattern by traversing the conclusion, and then
all the hypotheses from right to left.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If grind! is used, then only minimal indexable subexpressions are considered.
grindMod ::= ...
| The `←=` modifier is unlike the other `grind` 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.
The ←= modifier is unlike the other grind 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 ←=] AttributeSome additional modifiers can be used to add other kinds of lemmas to the index. This includes extensionality theorems, injectivity theorems for functions, and a shortcut to add all constructors of an inductively defined predicate to the index.
grindMod ::= ...
| The `ext` modifier marks extensionality theorems for use by `grind`.
For example, the standard library marks `funext` with this attribute.
Whenever `grind` encounters a disequality `a ≠ b`, it attempts to apply any
available extensionality theorems whose matches the type of `a` and `b`.
The ext modifier marks extensionality theorems for use by grind.
For example, the standard library marks funext with this attribute.
Whenever grind encounters a disequality a ≠ b, it attempts to apply any
available extensionality theorems whose matches the type of a and b.
In addition, adding @[grind ext] to a structure registers a its extensionality theorem
@[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! 🐙
grindMod ::= ...
| The `inj` modifier marks injectivity theorems for use by `grind`.
The conclusion of the theorem must be of the form `Function.Injective f`
where the term `f` contains at least one constant symbol.
The inj modifier marks injectivity theorems for use by grind.
The conclusion of the theorem must be of the form Function.Injective f
where the term f contains at least one constant symbol.
This function double doubles its argument:
def double (x : Nat) : Nat := x + x
By default, grind cannot prove the following theorem:
theorem A {n k : Nat} :
double (n + 5) = double (k - 3) →
n + 8 = k := n:Natk:Nat⊢ double (n + 5) = double (k - 3) → n + 8 = k
n:Natk:Nat⊢ double (n + 5) = double (k - 3) → n + 8 = k
However, double is injective, and this fact can be registered for grind using the grind inj attribute:
@[grind inj]
theorem double_inj : Function.Injective double := ⊢ Function.Injective double
⊢ ∀ ⦃a₁ a₂ : Nat⦄, a₁ + a₁ = a₂ + a₂ → a₁ = a₂
All goals completed! 🐙
This injectivity lemma suffices to prove the theorem:
theorem B {n k : Nat} :
double (n + 5) = double (k - 3) →
n + 8 = k := n:Natk:Nat⊢ double (n + 5) = double (k - 3) → n + 8 = k
All goals completed! 🐙
grindMod ::= ...
| The `intro` modifier instructs `grind` to use the constructors (introduction rules)
of an inductive predicate as E-matching theorems.Example:
```
inductive Even : Nat → Prop where
| zero : Even 0
| add2 : Even x → Even (x + 2)
attribute [grind intro] Even
example (h : Even x) : Even (x + 6) := by grind
example : Even 0 := by grind
```
Here `attribute [grind intro] Even` acts like a macro that expands to
`attribute [grind] Even.zero` and `attribute [grind] Even.add2`.
This is especially convenient for inductive predicates with many constructors.
The intro modifier instructs grind to use the constructors (introduction rules)
of an inductive predicate as E-matching theorems.Example:
inductive Even : Nat → Prop where
| zero : Even 0
| add2 : Even x → Even (x + 2)
attribute [grind intro] Even
example (h : Even x) : Even (x + 6) := x:Nath:Even x⊢ Even (x + 6) All goals completed! 🐙
example : Even 0 := ⊢ Even 0 All goals completed! 🐙
Here attribute [grind intro] Even acts like a macro that expands to
attribute [grind] Even.zero and attribute [grind] Even.add2.
This is especially convenient for inductive predicates with many constructors.
The predicate Decreasing states that each of the values in a list of integers is less than the one before, and the function decreasing checks this property, returning a Bool.
inductive Decreasing : List Int → Prop
| nil : Decreasing []
| singleton : Decreasing [x]
| cons : Decreasing (x :: xs) → y > x → Decreasing (y :: x :: xs)
def decreasing : List Int → Bool
| [] | [_] => true
| y :: x :: xs => y > x && decreasing (x :: xs)
The function is correct if it returns true exactly when Decreasing holds for its argument.
Attempting to prove this fact using a combination of fun_induction and grind fails immediately, with none of the three cases proven:
def decreasingCorrect : decreasing xs = Decreasing xs := xs:List Int⊢ (decreasing xs = true) = Decreasing xs
⊢ (true = true) = Decreasing []head✝:Int⊢ (true = true) = Decreasing [head✝]y✝:Intx✝:Intxs✝:List Intih1✝:(decreasing (x✝ :: xs✝) = true) = Decreasing (x✝ :: xs✝)⊢ ((decide (y✝ > x✝) && decreasing (x✝ :: xs✝)) = true) = Decreasing (y✝ :: x✝ :: xs✝) ⊢ (true = true) = Decreasing []head✝:Int⊢ (true = true) = Decreasing [head✝]y✝:Intx✝:Intxs✝:List Intih1✝:(decreasing (x✝ :: xs✝) = true) = Decreasing (x✝ :: xs✝)⊢ ((decide (y✝ > x✝) && decreasing (x✝ :: xs✝)) = true) = Decreasing (y✝ :: x✝ :: xs✝) y✝:Intx✝:Intxs✝:List Intih1✝:(decreasing (x✝ :: xs✝) = true) = Decreasing (x✝ :: xs✝)⊢ ((decide (y✝ > x✝) && decreasing (x✝ :: xs✝)) = true) = Decreasing (y✝ :: x✝ :: xs✝)
Adding the grind intro attribute to Decreasing results in E-matching patterns being added for each of the three constructors, after which grind can prove the first two goals, and requires only a case analysis of a hypothesis to prove the final goal:
attribute [grind intro] Decreasing
def decreasingCorrect' : decreasing xs = Decreasing xs := xs:List Int⊢ (decreasing xs = true) = Decreasing xs
⊢ (true = true) = Decreasing []head✝:Int⊢ (true = true) = Decreasing [head✝]y✝:Intx✝:Intxs✝:List Intih1✝:(decreasing (x✝ :: xs✝) = true) = Decreasing (x✝ :: xs✝)⊢ ((decide (y✝ > x✝) && decreasing (x✝ :: xs✝)) = true) = Decreasing (y✝ :: x✝ :: xs✝) ⊢ (true = true) = Decreasing []head✝:Int⊢ (true = true) = Decreasing [head✝]y✝:Intx✝:Intxs✝:List Intih1✝:(decreasing (x✝ :: xs✝) = true) = Decreasing (x✝ :: xs✝)⊢ ((decide (y✝ > x✝) && decreasing (x✝ :: xs✝)) = true) = Decreasing (y✝ :: x✝ :: xs✝) try y✝:Intx✝:Intxs✝:List Intih1✝:(decreasing (x✝ :: xs✝) = true) = Decreasing (x✝ :: xs✝)⊢ ((decide (y✝ > x✝) && decreasing (x✝ :: xs✝)) = true) = Decreasing (y✝ :: x✝ :: xs✝)
case case3 y x xs ih y:Intx:Intxs:List Intih:(decreasing (x :: xs) = true) = Decreasing (x :: xs)⊢ ((decide (y > x) && decreasing (x :: xs)) = true) = Decreasing (y :: x :: xs)
y:Intx:Intxs:List Intih:(decreasing (x :: xs) = true) = Decreasing (x :: xs)⊢ (decide (y > x) && decreasing (x :: xs)) = true ↔ Decreasing (y :: x :: xs)
y:Intx:Intxs:List Intih:(decreasing (x :: xs) = true) = Decreasing (x :: xs)⊢ (decide (y > x) && decreasing (x :: xs)) = true → Decreasing (y :: x :: xs)y:Intx:Intxs:List Intih:(decreasing (x :: xs) = true) = Decreasing (x :: xs)⊢ Decreasing (y :: x :: xs) → (decide (y > x) && decreasing (x :: xs)) = true
y:Intx:Intxs:List Intih:(decreasing (x :: xs) = true) = Decreasing (x :: xs)⊢ (decide (y > x) && decreasing (x :: xs)) = true → Decreasing (y :: x :: xs) All goals completed! 🐙
y:Intx:Intxs:List Intih:(decreasing (x :: xs) = true) = Decreasing (x :: xs)⊢ Decreasing (y :: x :: xs) → (decide (y > x) && decreasing (x :: xs)) = true intro
y:Intx:Intxs:List Intih:(decreasing (x :: xs) = true) = Decreasing (x :: xs)x✝:Decreasing (y :: x :: xs)hDec:Decreasing (x :: xs)hLt:y > x⊢ (decide (y > x) && decreasing (x :: xs)) = true
All goals completed! 🐙
Adding grind cases to Decreasing enables this case analysis automatically, resulting in a fully automatic proof:
attribute [grind cases] Decreasing
def decreasingCorrect'' : decreasing xs = Decreasing xs := xs:List Int⊢ (decreasing xs = true) = Decreasing xs
⊢ (true = true) = Decreasing []head✝:Int⊢ (true = true) = Decreasing [head✝]y✝:Intx✝:Intxs✝:List Intih1✝:(decreasing (x✝ :: xs✝) = true) = Decreasing (x✝ :: xs✝)⊢ ((decide (y✝ > x✝) && decreasing (x✝ :: xs✝)) = true) = Decreasing (y✝ :: x✝ :: xs✝) ⊢ (true = true) = Decreasing []head✝:Int⊢ (true = true) = Decreasing [head✝]y✝:Intx✝:Intxs✝:List Intih1✝:(decreasing (x✝ :: xs✝) = true) = Decreasing (x✝ :: xs✝)⊢ ((decide (y✝ > x✝) && decreasing (x✝ :: xs✝)) = true) = Decreasing (y✝ :: x✝ :: xs✝) 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
intro ⟨d₁, p₁⟩ 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