我正在学习 lean tutorial 的第 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 .
关于dependent-type - 如何在精益中证明 a = b → a + 1 = b + 1？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/41946310/