如何在精益中證明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？

回答

相關問題