16.11. Reducibility🔗

Reducible definitions in terms are eagerly unfolded by grind. This enables more efficient definitional equality comparisons and indexing.

Reducibility and Congruence Closure

The definition of one is not reducible:

def one := 1

This means that grind does not unfold it:

example : one = 1 := by⊢ one = 1 `grind` failed
grindh:¬one = 1⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] ¬one = 1
[eqc] False propositions
[prop] one = 1
[cutsat] Assignment satisfying linear constraints
[assign] one := 2grindAll goals completed! 🐙

`grind` failed
grindh:¬one = 1⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] ¬one = 1
[eqc] False propositions
[prop] one = 1
[cutsat] Assignment satisfying linear constraints
[assign] one := 2

two, on the other hand, is an abbreviation and thus reducible:

abbrev two := 2

grind unfolds two before adding it to the “whiteboard”, allowing the proof to be completed immediately:

example : two = 2 := by⊢ two = 2 grindAll goals completed! 🐙

Live ↪

E-matching patterns also unfold reducible definitions. The patterns generated for theorems about abbreviations are expressed in terms of the unfolded abbreviations. Abbreviations should not generally be recursive; in particular, when using grind, recursive abbreviations can result in poor indexing performance and unpredictable patterns.

E-matching and Unfolding Abbreviations

When adding grind annotations to theorems, E-matching patterns are generated based on the theorem statement. These patterns determine when the theorem is instantiated. The theorem one_eq_1 mentions the semireducible definition one, and the resulting pattern is also one:

def one := 1

@[one_eq_1: [one]grind? =]
theorem one_eq_1 : one = 1 := by⊢ one = 1 rflAll goals completed! 🐙

one_eq_1: [one]

Applying the same annotation to a theorem about the reducible abbreviation two results in a pattern in which two is unfolded:

abbrev two := 2

@[two_eq_2: [@OfNat.ofNat `[Nat] `[2] `[instOfNatNat 2]]grind? =]
theorem two_eq_2: two = 2 := by⊢ two = 2 grindAll goals completed! 🐙

two_eq_2: [@OfNat.ofNat `[Nat] `[2] `[instOfNatNat 2]]

Live ↪

Recursive Abbreviations and grind

Using the grind attribute to add E-matching patterns for a recursive abbreviation's equational lemmas does not result in useful patterns for recursive abbreviations. The @[grind?] attribute on this definition of the Fibonacci function results in three patterns, each corresponding to one of the three possibilities:

@[fib.eq_3: [fib (#0 + 2)]fib.eq_1: [fib `[0]]fib.eq_2: [fib `[1]]grind?]
def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)

fib.eq_1: [fib `[0]]

fib.eq_2: [fib `[1]]

fib.eq_3: [fib (#0 + 2)]

Replacing the definition with an abbreviation results in patterns in which occurrences of the function are unfolded. These patterns are not particularly useful:

@[fib.eq_3: [@HAdd.hAdd `[Nat] `[Nat] `[Nat] `[instHAdd] (fib #0) (fib (#0 + 1))]fib.eq_1: [@OfNat.ofNat `[Nat] `[0] `[instOfNatNat 0]]fib.eq_2: [@OfNat.ofNat `[Nat] `[1] `[instOfNatNat 1]]grind?]
abbrev fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)

fib.eq_1: [@OfNat.ofNat `[Nat] `[0] `[instOfNatNat 0]]

fib.eq_2: [@OfNat.ofNat `[Nat] `[1] `[instOfNatNat 1]]

fib.eq_3: [@HAdd.hAdd `[Nat] `[Nat] `[Nat] `[instHAdd] (fib #0) (fib (#0 + 1))]