16.11. 可约性🔗

grind 会及早展开项中的可约定义。这使定义相等性比较和索引更高效。

可约性与同余闭包

one 的定义不是可约的：

def one := 1

这意味着 grind 不会展开它：

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 是缩写，因此可约：

abbrev two := 2

grind 在将 two 加入“白板”前先展开它，从而可以立即完成证明：

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

在线查看 ↪

E-匹配模式也会展开可约定义。为涉及缩写的定理生成的模式会用展开后的缩写来表示。缩写通常不应递归；特别是在使用 grind 时，递归缩写可能导致索引性能不佳以及模式不可预测。

E-匹配与展开缩写

为定理添加 grind 标注时，会根据定理陈述生成 E-匹配模式。这些模式决定何时实例化该定理。定理 one_eq_1 提到了半可约定义 one，生成的模式也同样是 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]

将相同标注应用于涉及可约缩写 two 的定理，会得到一个展开了 two 的模式：

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]]

在线查看 ↪

递归缩写与 grind

使用 grind 属性为递归缩写的等式引理添加 E-匹配模式，并不能为递归缩写生成有用的模式。这个斐波那契函数定义上的 @[grind?] 属性会生成三个模式，分别对应三种可能情况：

@[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)]

将该定义替换为缩写后，生成的模式会展开其中出现的函数。这些模式并没有多大用处：

@[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))]