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

我正在通过lean tutorial的第4章。如何在精益中证明a = b→a + 1 = b + 1？

我希望能够证明简单的平等性，如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

来源

2017-01-30 Adam Kurkiewicz

请注意链接的教程是* Lean 2 *。您可以在http://leanprover.github.io/documentation/上找到当前精益版本的文档。 –

谢谢@Kha，我可以看到，精益3包含一个更新的改进版本的教程： https://leanprover.github.io/theorem_proving_in_lean/ （至少没有未实现的TODO），我会切换并使用它因此。 –

顺便说一句，这个教程的新版本是超酷的，它显示了鼠标悬停的术语类型！ –

可以使用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

注意，精益能够推断，我们的功能是λ n, n + 1，所以证明可以简化为congr_arg _ H。

来源

2017-01-31 10:19:04

谢谢，这确实有效，从现在开始，我会知道如何使用'congr_arg'。但是，我不明白'congr_arg'的类型声明。未知数是： 1.宇宙变量'u v'。他们是否在精益教程中进一步涵盖？ 2.'排序'关键字。有没有什么地方可以快速了解这些，或者我应该耐心地继续教程？ –

第一部分介绍了宇宙变量。 2.2 [定理证明在精益]（https://leanprover.github.io/theorem_proving_in_lean/）。 [issue＃1341]（https://github.com/leanprover/lean/issues/1341）解释了'Sort'关键字。 *现在*你可以忽略这些微妙的东西，并且把'congr_arg'引理看作一个函数，它可以从a 1 = a 2的证明中得出'f a 1 = f a 2'的证明，对于任何函数f：α →β'，其中'Sort'只是告诉你'α'和'β'是一些类型。 HTH。 –

虽然congr_arg是在一般一个很好的解决方案，该具体示例中的确可以与eq.subst +高阶统（其congr_arg内部使用）来解决。

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

来源

2017-01-31 12:35:00

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

回答

相关问题