The Lean Language Reference

17.10. Annotating Libraries for grind🔗

To use grind effectively with a library, it must be annotated by applying the grind attribute to suitable lemmas or declaring Lean.Parser.Command.grindPattern : commandThe `grind_pattern` command can be used to manually select a pattern for theorem instantiation. Enabling the option `trace.grind.ematch.instance` causes `grind` to print a trace message for each theorem instance it generates, which can be helpful when determining patterns. 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 theorems such as transitivity rules, where multiple premises must be simultaneously present for the rule to apply. In the following example, `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 := by grind ``` 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`. You can add constraints to restrict theorem instantiation. For example: ``` grind_pattern extract_extract => (as.extract i j).extract k l where as =/= #[] ``` The constraint instructs `grind` to instantiate the theorem only if `as` is **not** definitionally equal to `#[]`. ## Constraints - `x =/= term`: The term bound to `x` (one of the theorem parameters) is **not** definitionally equal to `term`. The term may contain holes (i.e., `_`). - `x =?= term`: The term bound to `x` is definitionally equal to `term`. The term may contain holes (i.e., `_`). - `size x < n`: The term bound to `x` has size less than `n`. Implicit arguments and binder types are ignored when computing the size. - `depth x < n`: The term bound to `x` has depth less than `n`. - `is_ground x`: The term bound to `x` does not contain local variables or meta-variables. - `is_value x`: The term bound to `x` is a value. That is, it is a constructor fully applied to value arguments, a literal (`Nat`, `Int`, `String`, etc.), or a lambda `fun x => t`. - `is_strict_value x`: Similar to `is_value`, but without lambdas. - `not_value x`: The term bound to `x` is a **not** value (see `is_value`). - `not_strict_value x`: Similar to `not_value`, but without lambdas. - `gen < n`: The theorem instance has generation less than `n`. Recall that each term is assigned a generation, and terms produced by theorem instantiation have a generation that is one greater than the maximal generation of all the terms used to instantiate the theorem. This constraint complements the `gen` option available in `grind`. - `max_insts < n`: A new instance is generated only if less than `n` instances have been generated so far. - `guard e`: The instantiation is delayed until `grind` learns that `e` is `true` in this state. - `check e`: Similar to `guard e`, but `grind` checks whether `e` is implied by its current state by assuming `¬ e` and trying to deduce an inconsistency. ## Example Consider the following example where `f` is a monotonic function ``` opaque f : Nat → Nat axiom fMono : x ≤ y → f x ≤ f y ``` and you want to instruct `grind` to instantiate `fMono` for every pair of terms `f x` and `f y` when `x ≤ y` and `x` is **not** definitionally equal to `y`. You can use ``` grind_pattern fMono => f x, f y where guard x ≤ y x =/= y ``` Then, in the following example, only three instances are generated. ``` /-- trace: [grind.ematch.instance] fMono: a ≤ f a → f a ≤ f (f a) [grind.ematch.instance] fMono: f a ≤ f (f a) → f (f a) ≤ f (f (f a)) [grind.ematch.instance] fMono: a ≤ f (f a) → f a ≤ f (f (f a)) -/ #guard_msgs in example : f b = f c → a ≤ f a → f (f a) ≤ f (f (f a)) := by set_option trace.grind.ematch.instance true in grind ``` grind_patterns. These annotations direct grind's selection of theorems, which lead to further facts on the metaphorical whiteboard. With too few annotations, grind will fail to use the lemmas; with too many, it may become slow or it fail due to exhausting resource limitations. Annotations should generally be conservative: only add an annotation if you expect that grind should always instantiate the theorem once the patterns are matched.

17.10.1. Simp Lemmas

Typically, many theorems that are annotated with @[simp] should also be annotated with @[grind =]. One significant exception is that typically we avoid having @[simp] theorems that introduce an Lean.Parser.Term.ifif on the right hand side, instead preferring a pair of theorems with the positive and negative conditions as hypotheses. Because grind is designed to perform case splitting, it is generally better to instead annotate the single theorem introducing the Lean.Parser.Term.ifif with @[grind =].

Besides using @[grind =] to encourage grind to perform rewriting from left to right, you can also use @[grind _=_] to “saturate”, allowing bidirectional rewriting whenever either side is encountered.

17.10.2. Backwards and Forwards Reasoning

Use @[grind ←] (which generates patterns from the conclusion of the theorem) for backwards reasoning theorems, i.e. theorems that should be tried when their conclusion matches a goal. Some examples of theorems in the standard library that are annotated with grind ← are:

In each case, the lemma is relevant when its conclusion matches a proof goal.

Use @[grind →] (which generates patterns from the hypotheses) for forwards reasoning theorems, i.e. where facts should be propagated from existing facts on the whiteboard. Some examples of theorems in the standard library that are annotated with grind → are:

  • List.getElem_of_getElem? {l : List α} : l[i]? = some a → ∃ h : i < l.length, l[i] = a
  • Array.mem_of_mem_erase [BEq α] {a b : α} {xs : Array α} (h : a ∈ xs.erase b) : a ∈ xs
  • List.forall_none_of_filterMap_eq_nil (h : filterMap f xs = []) : ∀ x ∈ xs, f x = none

In these cases, the theorems' assumptions determine when they are relevant.

There are many uses for custom patterns created with the Lean.Parser.Command.grindPattern : commandThe `grind_pattern` command can be used to manually select a pattern for theorem instantiation. Enabling the option `trace.grind.ematch.instance` causes `grind` to print a trace message for each theorem instance it generates, which can be helpful when determining patterns. 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 theorems such as transitivity rules, where multiple premises must be simultaneously present for the rule to apply. In the following example, `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 := by grind ``` 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`. You can add constraints to restrict theorem instantiation. For example: ``` grind_pattern extract_extract => (as.extract i j).extract k l where as =/= #[] ``` The constraint instructs `grind` to instantiate the theorem only if `as` is **not** definitionally equal to `#[]`. ## Constraints - `x =/= term`: The term bound to `x` (one of the theorem parameters) is **not** definitionally equal to `term`. The term may contain holes (i.e., `_`). - `x =?= term`: The term bound to `x` is definitionally equal to `term`. The term may contain holes (i.e., `_`). - `size x < n`: The term bound to `x` has size less than `n`. Implicit arguments and binder types are ignored when computing the size. - `depth x < n`: The term bound to `x` has depth less than `n`. - `is_ground x`: The term bound to `x` does not contain local variables or meta-variables. - `is_value x`: The term bound to `x` is a value. That is, it is a constructor fully applied to value arguments, a literal (`Nat`, `Int`, `String`, etc.), or a lambda `fun x => t`. - `is_strict_value x`: Similar to `is_value`, but without lambdas. - `not_value x`: The term bound to `x` is a **not** value (see `is_value`). - `not_strict_value x`: Similar to `not_value`, but without lambdas. - `gen < n`: The theorem instance has generation less than `n`. Recall that each term is assigned a generation, and terms produced by theorem instantiation have a generation that is one greater than the maximal generation of all the terms used to instantiate the theorem. This constraint complements the `gen` option available in `grind`. - `max_insts < n`: A new instance is generated only if less than `n` instances have been generated so far. - `guard e`: The instantiation is delayed until `grind` learns that `e` is `true` in this state. - `check e`: Similar to `guard e`, but `grind` checks whether `e` is implied by its current state by assuming `¬ e` and trying to deduce an inconsistency. ## Example Consider the following example where `f` is a monotonic function ``` opaque f : Nat → Nat axiom fMono : x ≤ y → f x ≤ f y ``` and you want to instruct `grind` to instantiate `fMono` for every pair of terms `f x` and `f y` when `x ≤ y` and `x` is **not** definitionally equal to `y`. You can use ``` grind_pattern fMono => f x, f y where guard x ≤ y x =/= y ``` Then, in the following example, only three instances are generated. ``` /-- trace: [grind.ematch.instance] fMono: a ≤ f a → f a ≤ f (f a) [grind.ematch.instance] fMono: f a ≤ f (f a) → f (f a) ≤ f (f (f a)) [grind.ematch.instance] fMono: a ≤ f (f a) → f a ≤ f (f (f a)) -/ #guard_msgs in example : f b = f c → a ≤ f a → f (f a) ≤ f (f (f a)) := by set_option trace.grind.ematch.instance true in grind ``` grind_pattern command. One common use is to introduce inequalities about terms, or membership propositions.

We might have

variable [BEq α] theorem count_le_size {a : α} {xs : Array α} : count a xs ≤ xs.size := ... grind_pattern count_le_size => count a xs

which will register this inequality as soon as a count a xs term is encountered (even if the problem has not previously involved inequalities).

We can also use multi-patterns to be more restrictive, e.g. only introducing an inequality about sizes if the whiteboard already contains facts about sizes:

theorem declaration uses 'sorry'size_pos_of_mem {xs : Array α} (h : a ∈ xs) : 0 < xs.size := sorry grind_pattern size_pos_of_mem => a ∈ xs, xs.size

Unlike a @[grind →] attribute, which would cause this theorem to be instantiated whenever a ∈ xs is encountered, this pattern will only be used when xs.size is already on the whiteboard. (Note that this grind pattern could also be produced using the @[grind <=] attribute, which looks at the conclusion first, then backwards through the hypotheses to select patterns. On the other hand, @[grind →] would select only a ∈ xs.)

In Mathlib we might want to enable polynomial reasoning about the sine and cosine functions, and so add a custom grind pattern

theorem sin_sq_add_cos_sq : sin x ^ 2 + cos x ^ 2 = 1 := ... grind_pattern sin_sq_add_cos_sq => sin x, cos x

which will instantiate the theorem as soon as both sin x and cos x (with the same x) are encountered. This theorem will then automatically enter the Gröbner basis module, and be used to reason about polynomial expressions involving both sin x and cos x. One both alternatively, more aggressively, write two separate grind patterns so that this theorem instantiated when either sin x or cos x is encountered.