Eşitlik yerine varlığın yerine geçme özelliği

Question

chapter 7 of "theorem proving in lean"'dan endüktif türleri anlamaya çalışıyorum. Ben olasılıklar çift ile derleyici tatmin edebildi bazı varsayım ve oldukça kapsamlı aramadan sonra

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 

:

Kendime doğal sayıların bu halefi kanıtlayan bir görevi ayarlamak eşitlik üzerinde ikame özelliği vardır:

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 

Verdiğim provalardan herhangi birinin aslında nasıl çalıştığını anlamıyorum.

1. eq (endüktif) tipi nedir? VSCode'da eq'un tip imzasını eq Π {α : Type} α → α → Prop olarak görebiliyorum, ancak bireysel (endüktif) kurucular göremiyorum (zero ve succ analogları natural). Kaynak kodunda bulabildiğim en iyisi doesn't look quite right.
2. eq.subst niçin (natural.succ a) = (natural.succ a) bir kanıtı kabul etmek için (natural.succ a) = (natural.succ b) kanıtı sunmaktan mutluluk duyarsınız?
3. higher order unification nedir ve bu örnek için nasıl geçerlidir?
4. [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

Answer 1

1. eq inductive eq {α : Sort u} (a : α) : α → Prop | refl : eq a fikir olduğu https://github.com/leanprover/lean/blob/master/library/init/core.lean#L120 de tanımlanır olduğunu ben #check (eq.rec_on H (eq.refl (natural.succ a))) yazarken alıyorum hatası, anlamı nedir herhangi bir terim kendisine eşit olmasıdır, ve iki terimin eşit olmasının tek yolu onların aynı terim olmalarıdır. Bu biraz ITT büyüsü gibi hissedebilir. Güzellik, bu tanım için otomatik olarak oluşturulan işaretçiden gelir: eq.rec : Π {α : Sort u_2} {a : α} {C : α → Sort u_1}, C a → Π {a_1 : α}, a = a_1 → C a_1 Eşitlik için ikame ilkesidir. "C bir a ve a = a_1 tutarsa, o zaman C, a_1." (C tipi değerli yerine Prop değerli ait ise benzer bir yorumlama var.)

2. eq.subst

   succ a = succ a kanıtı ile birlikte a = b bir kanıtı alıyor. eq.subst'un temel olarak yukarıda eq.rec bir yeniden formülasyon olduğunu unutmayın. Bir değişken x üzerinden parametrelendirilmiş olan C numaralı özelliğin succ a = succ x olduğunu varsayalım. C, yansıma ile a için geçerlidir ve a = b'dan beri, b'un sahibine sahibiz.

3. eq.subst H rfl yazdığınızda, Yalın, özellik (veya "neden") C öğesinin ne olması gerektiğini bulması gerekir. Bu, yüksek mertebeden bir birleşme örneğidir: bilinmeyen değişkenin bir lambda ifadesiyle birleşmesi gerekir. Bu bölümün 6.101 bölümünde https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf'da ve bazı genel bilgiler https://en.wikipedia.org/wiki/Unification_(computer_science)#Higher-order_unification'da tartışılmaktadır.

4. a = b'u succ a = succ a yerine, kanıtlamaya çalıştığınız şeyi söylemeden Yalın'ı mı istiyorsunuz? succ b = succ b veya succ b = succ a veya hatta succ a = succ a (hiçbir yerini değiştirerek) ispatlamaya çalışıyor olabilirsiniz.Yalın, bu bilgiye sahip olmadıkça C nedenini çıkaramaz. yüksek mertebeden birleşme titiz ve pahalı olduğu için oyuncu değişikliği yaparak Genelde

, "elle" (eq.rec, subst, vs ile), zordur. Sık sık bu rw (yeniden yazma) gibi taktikleri kullanmanız daha iyi olduğunu göreceksiniz: Eğer zeki olmaya istiyorsanız, en Yalın denklemi derleyici yararlanabilirler lemma succ_over_equality (a b : natural) (H : a = b) : (natural.succ a) = (natural.succ b) := by rw H

ve aslında o a=b arasında "sadece" kanıt rfl geçerli: lemma succ_over_equality : Π (a b : natural), a = b → (natural.succ a) = (natural.succ b) | ._ _ rfl := rfl