Lean 语言参考

16.11. 还原性🔗

可简化术语定义由grind 热切地展开。 这可以实现更高效的 定义等价 比较和索引。

Reducibility and Congruence Closure

one 的定义不是 可约化：

def one := 1

这意味着 grind 不会展开它：

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

[grind] Goal diagnostics
  • [facts] Asserted facts
  • [eqc] False propositions
  • [cutsat] Assignment satisfying linear constraints
    • [assign] one := 2

另一方面，two 是缩写，因此可以简化：

abbrev two := 2

grind 将 two 展开，然后将其添加到“白板”中，从而可以立即完成证明：

example : two = 2 := ⊢ two = 2 All goals completed! 🐙
Live ↪

电子匹配模式还展现了可简化的定义。 为有关缩写的定理生成的模式以展开的缩写表示。 缩写一般不应是递归的；特别是，当使用 grind 时，递归缩写可能会导致索引性能较差和不可预测的模式。

E-matching and Unfolding Abbreviations

当向定理添加 grind 注释时，将根据定理语句生成 E 匹配模式。 这些模式决定了定理何时被实例化。 定理 one_eq_1 提到了 半可约 定义 one，结果模式也是 one：

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

将相同的注释应用于有关 reducible 缩写 two 的定理会产生 two 展开的模式：

abbrev two := 2 @[two_eq_2: [@OfNat.ofNat `[Nat] `[2] `[instOfNatNat 2]]grind? =] theorem two_eq_2: two = 2 := ⊢ two = 2 All goals completed! 🐙 
two_eq_2: [@OfNat.ofNat `[Nat] `[2] `[instOfNatNat 2]]
Live ↪
Recursive Abbreviations and grind

使用 grind 属性为递归缩写的 等式引理 添加电子匹配模式不会产生递归缩写的有用模式。 斐波那契函数定义中的 @[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))]