证明继承人超越平等的替代财产

我试图从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

谢谢，这是很多细节！我会慢慢咀嚼:) –

证明继承人超越平等的替代财产

回答

相关问题