如何在精益中证明a = b → a + 1 = b + 1？

Question

我正在学习精益教程的第 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

Answer 1

您可以使用

congrArg

引理

lemma congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) :
  a₁ = a₂ → f a₁ = f a₂

这意味着如果您向函数提供相同的输入，则输出值也将相等。

证明是这样的：

example (a b : Nat) (h : a = b) : a + 1 = b + 1 :=
  congrArg (fun n => n + 1) h

注意，Lean 能够推断出我们的函数是

fun n => n + 1

，因此证明可以简化为 

congrArg _ h

。

Answer 2

虽然

congr_arg

 一般来说是一个很好的解决方案，但这个具体示例确实可以通过 

eq.subst

 + 高阶统一（

congr_arg

 内部使用）来解决。

example (a b : nat) (H1 : a = b) : a + 1 = b + 1 :=
eq.subst H1 rfl

Answer 3

既然你有一个平等（

a = b

），你也可以使用战术模式重写目标：

example (a b : nat) (H1 : a = b) : a + 1 = b + 1 :=
by rw H1

有关策略的介绍，请参阅

精益定理证明的第 5 章。

Answer 4

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