如何证明 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引理

\n

lemma congrArg {\xce\xb1 : Sort u} {\xce\xb2 : Sort v} {a\xe2\x82\x81 a\xe2\x82\x82 : \xce\xb1} (f : \xce\xb1 \xe2\x86\x92 \xce\xb2) :\n  a\xe2\x82\x81 = a\xe2\x82\x82 \xe2\x86\x92 f a\xe2\x82\x81 = f a\xe2\x82\x82\n

\n

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

\n

证明是这样的：

\n

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

\n

请注意，Lean 能够推断出我们的函数是fun n => n + 1，因此证明可以简化为congrArg _ h。

\n

Answer 2

虽然congr_arg总体上这是一个很好的解决方案，但这个具体示例确实可以通过eq.subst+高阶统一（congr_arg内部使用）来解决。

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