證明繼承人超越平等的替代財產

我試圖從chapter 7 of "theorem proving in lean"瞭解歸納類型。證明繼承人超越平等的替代財產

我給自己設定了證明自然數的是繼任者的任務，擁有平等的一個替代性質：

inductive natural : Type 
| zero : natural 
| succ : natural -> natural 

lemma succ_over_equality (a b : natural) (H : a = b) : 
    (natural.succ a) = (natural.succ b) := sorry

一些猜測和相當詳盡的搜索我是能夠滿足編譯器有幾個可能的原因後：

lemma succ_over_equality (a b : natural) (H : a = b) : 
    (natural.succ a) = (natural.succ b) := 
    eq.rec_on H (eq.refl (natural.succ a)) 
    --eq.rec_on H rfl 
    --eq.subst H rfl 
    --eq.subst H (eq.refl (natural.succ a)) 
    --congr_arg (λ (n : natural), (natural.succ n)) H

我不明白我剛纔給出的任何證明實際上是如何工作的。

什麼是eq（inductive）類型的完整定義？在VSCode中，我可以看到eq的類型簽名爲eq Π {α : Type} α → α → Prop，但我看不到單獨的（歸納）構造函數（zero和succ的類似項從natural開始）。我可以在源代碼doesn't look quite right中找到最好的。
爲什麼eq.subst高興地接受(natural.succ a) = (natural.succ a)的證明來提供(natural.succ a) = (natural.succ b)的證明？
什麼是higher order unification它是如何適用於這個特殊的例子？
什麼是錯誤，當我鍵入#check (eq.rec_on H (eq.refl (natural.succ a)))我得到的，這是[Lean] invalid 'eq.rec_on' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but the expected type must be known eq.rec_on : Π {α : Sort u} {a : α} {C : α → Sort l} {a_1 : α}, a = a_1 → C a → C a_1

來源

2017-07-17 Adam Kurkiewicz

在https://github.com/leanprover/lean/blob/master/library/init/core.lean – Adam

均衡生活的定義，爲什麼它接受的證明，據我所知，當你破壞它引起a和b的相等性（畢竟它們是構造函數的相同參數），所以在返回類型中它也被替換，產生一個類型爲（natural.suc c）=（natural.succ a）你碰巧有 – Adam

我甚至不明白這個問題的單個句子:-)雖然好運！ – Stimul8d

eq在https://github.com/leanprover/lean/blob/master/library/init/core.lean#L120定義爲 inductive eq {α : Sort u} (a : α) : α → Prop | refl : eq a 這個想法的意思是，任何項等於本身，兩個條件相等的唯一方法就是讓它們成爲相同的術語。這可能感覺像是一點ITT魔術。美麗來自自動產生的recursor這個定義： eq.rec : Π {α : Sort u_2} {a : α} {C : α → Sort u_1}, C a → Π {a_1 : α}, a = a_1 → C a_1 這是平等的替代原則。「如果C持有a，a = a_1，則C持有a_1。」（有一個類似的解釋如果C類型值，而不是道具值。）
eq.subst與的succ a = succ a證明一起服用a = b證明。請注意，eq.subst基本上是上述eq.rec的重新配置。假設通過變量x參數化的屬性C是succ a = succ x。 C通過反身性保持a，並且自a = b，我們有C持有b。
當你編寫eq.subst H rfl時，精益需要弄清楚屬性（或「動機」）應該是什麼。這是高階統一的例子：未知變量需要與lambda表達式統一。有關於https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf的第6.10節以及https://en.wikipedia.org/wiki/Unification_(computer_science)#Higher-order_unification的一些常規信息的討論。
您要求Lean用a = b替換成succ a = succ a，而不告訴它你想要證明什麼。你可能試圖證明succ b = succ b或succ b = succ a，或甚至succ a = succ a（通過替代無處）。除非它有這個信息，否則精益不能推斷動機C。

一般而言，做取代「手動」（與eq.rec，subst等）是困難的，因爲更高階統一是挑剔和昂貴的。你經常會發現它是更好地使用戰術像rw（重寫）： lemma succ_over_equality (a b : natural) (H : a = b) : (natural.succ a) = (natural.succ b) := by rw H

如果你要聰明一點，你可以利用精益的公式編譯器，以及一個事實，即a=b「唯一」證據是rfl： lemma succ_over_equality : Π (a b : natural), a = b → (natural.succ a) = (natural.succ b) | ._ _ rfl := rfl

來源

2017-07-26 10:30:50

謝謝，這是很多細節！我會慢慢咀嚼:) –

證明繼承人超越平等的替代財產

回答

相關問題