我正在学习精益教程的第 4 章。
我希望能够证明简单的等式，例如a = b → a + 1 = b + 1 不必使用 calc 环境。换句话说，我想明确地构建以下证明项：
example (a b : nat) (H1 : a = b) : a + 1 = b + 1 := sorry
我最好的猜测是，我需要使用eq.subst标准库中关于自然数相等性的一些相关引理，但我不知所措。我能找到的最接近的精益示例是：
example (A : Type) (a b : A) (P : A → Prop) (H1 : a = b) (H2 : P a) : P b :=
eq.subst H1 H2
你可以使用congr_arg引理
lemma congr_arg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) :
a₁ = a₂ → f a₁ = f a₂
这意味着如果您为函数提供相等的输入，则输出值也将相等。
证明是这样的：
example (a b : nat) (H : a = b) : a + 1 = b + 1 :=
congr_arg (λ n, n + 1) H
请注意，Lean 能够推断出我们的函数是λ n, n + 1，因此可以将证明简化为congr_arg _ H。
虽然congr_arg一般来说是一个很好的解决方案，但这个具体的例子确实可以用eq.subst+ 高阶统一（congr_arg内部使用）来解决。
example (a b : nat) (H1 : a = b) : a + 1 = b + 1 :=
eq.subst H1 rfl
由于您有一个相等 ( a = b)，您还可以使用策略模式重写目标：
example (a b : nat) (H1 : a = b) : a + 1 = b + 1 :=
by rw H1
有关策略的介绍，请参阅精益中的定理证明的第 5 章。
更一般的：a = b -> a + c = b + c in a Ring
import algebra.ring
open algebra
variable {A : Type}
variables [s : ring A] (a b c : A)
include s
example (a b c : A) (H1 : a = b) : a + c = b + c :=
eq.subst H1 rfl