我试图理解归纳类型《精益中的定理证明》第 7 章 https://leanprover.github.io/theorem_proving_in_lean/#07_Inductive_Types.html.
我给自己设定了一个任务，证明自然数的后继具有优于相等的替换性质：
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（感应）类型？在 VSCode 中我可以看到类型签名eq as eq Π {α : Type} α → α → Prop，但我看不到单独的（归纳）构造函数（类似物zero and succ from natural）。我能在源代码中找到的最好的看起来不太对劲 https://github.com/leanprover/lean/blob/41bf46dbba2c1846ebcb9319f326170c41f17fd4/tests/lean/quot_abuse2.lean.
- Why is
eq.subst很高兴接受证明(natural.succ a) = (natural.succ a)提供证明(natural.succ a) = (natural.succ b)?
- What is 高阶统一 https://stackoverflow.com/questions/41946310/how-to-prove-a-b-%E2%86%92-a-1-b-1-in-lean它如何应用于这个特定的例子？
- 我输入时出现的错误是什么意思
#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
-
eq is defined https://github.com/leanprover/lean/blob/f59c2f0ef59fdc1833b6ead6adca721123bd7932/library/init/core.lean#L145 to be
inductive eq {α : Sort u} (a : α) : α → Prop
| refl : eq a
这个想法是，任何一项都等于其自身，而两项相等的唯一方法就是它们是同一项。这可能感觉有点像 ITT 的魔法。其美妙之处在于自动生成的递归器：
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 是类型值而不是 Prop 值，则有类似的解释。）
eq.subst正在证明a = b连同证明succ a = succ a。注意eq.subst基本上是重新表述eq.rec多于。假设该财产C，对变量 x 进行参数化，是succ a = succ x. C成立于a通过反身性，并且因为a = b，我们有那个C持有b.
当你写的时候eq.subst H rfl，精益需要弄清楚属性（或“动机”）是什么C应该是。这是高阶统一的一个例子：未知变量需要与 lambda 表达式统一。在第 6.10 节中对此进行了讨论https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf，以及一些一般信息https://en.wikipedia.org/wiki/Unification_(computer_science)#Higher-order_unification https://en.wikipedia.org/wiki/Unification_(computer_science)#Higher-order_unification.
你要求 Lean 代替a = b into succ a = succ a，而不告诉它你想证明什么。你可能试图证明succ b = succ b, or 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
如果你想变得聪明，你可以利用 Lean 的方程编译器，事实上，“唯一”的证明a=b is rfl:
lemma succ_over_equality : Π (a b : natural),
a = b → (natural.succ a) = (natural.succ b)
| ._ _ rfl := rfl
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
