def Lean.Grind.genPattern {α : Sort u} (_h : Prop) (x _val : α) : α

Gadget for representing generalization steps h : x = val in patterns This gadget is used to represent patterns in theorems that have been generalized to reduce the number of casts introduced during E-matching based instantiation.

For example, consider the theorem

Option.pbind_some {α1 : Type u_1} {a : α1} {α2 : Type u_2}
    {f : (a_1 : α1) → some a = some a_1 → Option α2}
    : (some a).pbind f = f a rfl

Now, suppose we have a goal containing the term c.pbind g and the equivalence class {c, some b}. The E-matching module generates the instance

(some b).pbind (cast ⋯ g)

The cast is necessary because g's type contains c instead of some b. This cast` problematic because we don't have a systematic way of pushing casts over functions to its arguments. Moreover, heterogeneous equality is not effective because the following theorem is not provable in DTT:

theorem hcongr (h₁ : f ≍ g) (h₂ : a ≍ b)  : f a ≍ g b := ...

The standard solution is to generalize the theorem above and write it as

theorem Option.pbind_some'
        {α1 : Type u_1} {a : α1} {α2 : Type u_2}
        {x : Option α1}
        {f : (a_1 : α1) → x = some a_1 → Option α2}
        (h : x = some a)
        : x.pbind f = f a h := by
  subst h
  apply Option.pbind_some

Internally, we use this gadget to mark the E-matching pattern as

(genPattern h x (some a)).pbind f

This pattern is matched in the same way we match (some a).pbind f, but it saves the proof for the actual term to the some-application in f, and the actual term in x.

In the example above, c.pbind g also matches the pattern (genPattern h x (some a)).pbind f, and stores c in x, b in a, and the proof that c = some b in h.

Equations

• Lean.Grind.genPattern _h x _val = x

def Lean.Grind.genHEqPattern {α β : Sort u} (_h : Prop) (x : α) (_val : β) : α

Similar to genPattern but for the heterogeneous case

Equations

• Lean.Grind.genHEqPattern _h x _val = x

def Lean.Parser.resetGrindAttrs : ParserDescr

Reset all grind attributes. This command is intended for testing purposes only and should not be used in applications.

Equations

• Lean.Parser.resetGrindAttrs = Lean.ParserDescr.node `Lean.Parser.resetGrindAttrs 1024 (Lean.ParserDescr.symbol "reset_grind_attrs%")

def Lean.Parser.Attr.grindGen : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindEq : ParserDescr

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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindEqRhs : ParserDescr

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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindEqBoth : ParserDescr

The _=_ modifier acts like a macro which expands to = and =_. It adds two patterns, allowing the equality theorem to trigger in either direction.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindEqBwd : ParserDescr

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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindBwd : ParserDescr

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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindFwd : ParserDescr

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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindRL : ParserDescr

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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindLR : ParserDescr

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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindDef : ParserDescr

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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindUsr : ParserDescr

The usr modifier indicates that this theorem was applied using a user-defined instantiation pattern. Such patterns are declared with the grind_pattern command, which lets you specify how grind should match and use particular theorems.

Example:

• grind [usr myThm] means grind is using myThm, but with the the custom pattern you defined with grind_pattern.

Equations

• Lean.Parser.Attr.grindUsr = Lean.ParserDescr.nodeWithAntiquot "grindUsr" `Lean.Parser.Attr.grindUsr (Lean.ParserDescr.nonReservedSymbol "usr" false)

def Lean.Parser.Attr.grindCases : ParserDescr

The cases modifier marks inductively-defined predicates as suitable for case splitting.

Equations

• Lean.Parser.Attr.grindCases = Lean.ParserDescr.nodeWithAntiquot "grindCases" `Lean.Parser.Attr.grindCases (Lean.ParserDescr.nonReservedSymbol "cases" false)

def Lean.Parser.Attr.grindCasesEager : ParserDescr

The cases eager modifier marks inductively-defined predicates as suitable for case splitting, and instructs grind to perform it eagerly while preprocessing hypotheses.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindIntro : ParserDescr

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.

Equations

• Lean.Parser.Attr.grindIntro = Lean.ParserDescr.nodeWithAntiquot "grindIntro" `Lean.Parser.Attr.grindIntro (Lean.ParserDescr.nonReservedSymbol "intro" false)

def Lean.Parser.Attr.grindExt : ParserDescr

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.

Equations

• Lean.Parser.Attr.grindExt = Lean.ParserDescr.nodeWithAntiquot "grindExt" `Lean.Parser.Attr.grindExt (Lean.ParserDescr.nonReservedSymbol "ext" false)

def Lean.Parser.Attr.grindInj : ParserDescr

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.

Equations

• Lean.Parser.Attr.grindInj = Lean.ParserDescr.nodeWithAntiquot "grindInj" `Lean.Parser.Attr.grindInj (Lean.ParserDescr.nonReservedSymbol "inj" false)

def Lean.Parser.Attr.grindSym : ParserDescr

symbol <prio> sets the priority of a constant for grind’s pattern-selection procedure. grind prefers patterns that contain higher-priority symbols. Example:

opaque p : Nat → Nat → Prop
opaque q : Nat → Nat → Prop
opaque r : Nat → Nat → Prop

attribute [grind symbol low] p
attribute [grind symbol high] q

axiom bar {x y} : p x y → q x x → r x y → r y x
attribute [grind →] bar

Here p is low priority, q is high priority, and r is default. grind first tries to find a multi-pattern covering x and y using only high-priority symbols while scanning hypotheses left to right. This fails because q x x does not cover y. It then allows both high and default symbols and succeeds with the multi-pattern q x x, r x y. The term p x y is ignored due to p’s low priority. Symbols with priority 0 are never used in patterns.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grindMod : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grind : ParserDescr

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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grind! : ParserDescr

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

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`

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grind? : ParserDescr

Like @[grind], but also prints the pattern(s) selected by grind as info messages. Useful for debugging annotations and modifiers.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.grind!? : ParserDescr

Like @[grind!], but also prints the pattern(s) selected by grind as info messages. Combines minimal subexpression selection with debugging output.

Equations

• One or more equations did not get rendered due to their size.