8

我试图从“精益定理证明”的第 7 章中理解归纳类型。

我为自己设定了一项任务，即证明自然数的后继具有替代等式的属性：

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

我不明白我刚刚给出的任何证明实际上是如何工作的。

  1. eq（归纳）类型的完整定义是什么？在 VSCode 中，我可以看到eqas的类型签名eq Π {α : Type} α → α → Prop，但看不到单个（归纳）构造函数（zero和succfrom的类似物natural）。我能在源代码中找到的最好的看起来不太正确。
  2. 为什么eq.subst乐于接受一个证明(natural.succ a) = (natural.succ a)提供一个证明(natural.succ a) = (natural.succ b)？
  3. 什么是高阶统一，它如何应用于这个特定的例子？
  4. 我输入时收到的错误是什么意思#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
4

1 回答 1

5

  1. eq被定义为

    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 值，则有类似的解释。）

  2. eq.subst正在获取 的证明a = b以及 的证明succ a = succ a。请注意，这eq.subst基本上是eq.rec上面的重新表述。假设C在变量 x 上参数化的属性 是succ a = succ x。C通过自反性成立a，并且因为a = b，我们C拥有b.

  3. 当你写作时eq.subst H rfl，精益需要弄清楚属性（或“动机”）C应该是什么。这是一个高阶统一的例子：未知变量需要与一个 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有一些一般信息.

  4. 您要求 Lean 替换a = b为succ a = succ a，而没有告诉它您要证明什么。您可能试图证明succ b = succ b，或succ b = succ a，甚至succ a = succ a（通过无处替换）。C除非拥有这些信息，否则Lean 无法推断出动机。

一般来说，“手动”（使用 , 等）进行替换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是rfl：

lemma succ_over_equality : Π (a b : natural),
   a = b → (natural.succ a) = (natural.succ b)
| ._ _ rfl := rfl
于 2017-07-26T10:30:50.000 回答