证明后继者对平等的替代性

问题描述

我正在尝试从精益定理证明"第7章中理解归纳类型.

我为自己设定了一个任务，以证明自然数的后继者具有对等式的替代属性:

I set myself a task of proving that successor of natural numbers has a substitution property over equality:

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

经过一些猜测和相当详尽的搜索，我能够满足编译器的多种可能:

After some guesswork and fairly exhaustive search I was able to satisfy the compiler with a couple of possibilities:

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

我不明白我刚刚给的任何证明是如何工作的.

I don't understand how any of the proofs I've just given actually work.

1. eq(归纳)类型的完整定义是什么?在VSCode中，我可以看到eq的类型签名为eq Π {α : Type} α → α → Prop，但是看不到单独的(归纳)构造函数(natural中的zero和succ的类似物).我能在源代码中找到的最好的看起来不太正确.
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
)时出现的错误是什么意思?

1. What is the full definition of the eq (inductive) type? In VSCode I can see the type signature of eq as eq Π {α : Type} α → α → Prop, but I can't see individual (inductive) constructors (analogues of zero and succ from natural). The best I could find in source code doesn't look quite right.
2. Why is eq.subst happy to accept a proof of (natural.succ a) = (natural.succ a) to provide a proof of (natural.succ a) = (natural.succ b)?
3. What is higher order unification and how does it apply to this particular example?
4. What is the meaning of the error I get when I type #check (eq.rec_on H (eq.refl (natural.succ a))), which is [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

推荐答案

1. eq是定义的成为

inductive eq {α : Sort u} (a : α) : α → Prop
| refl : eq a

这个想法是，任何一项都等于其自身，并且使两项相等的唯一方法是使它们成为同一项.这可能感觉有点像ITT魔术.美来自此定义的自动生成的递归:

The idea is that any term is equal to itself, and the only way for two terms to be equal is for them to be the same term. This may feel like a bit of ITT magic. The beauty comes from the automatically generated recursor for this definition:

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

This is the substitution principle for equality. "If C holds of a, and a = a_1, then C holds of a_1." (There's a similar interpretation if C is type-valued instead of Prop-valued.)

eq.subst正在接受a = b的证明以及succ a = succ a的证明.注意，eq.subst基本上是上面的eq.rec的重新表述.假设在变量x上参数化的属性C是succ a = succ x. C通过反射性为a成立，并且由于a = b，我们拥有C的b成立.

eq.subst is taking a proof of a = b along with the proof of succ a = succ a. Note that eq.subst is basically a reformulation of eq.rec above. Suppose that the property C, parametrized over a variable x, is succ a = succ x. C holds for a by reflexivity, and since a = b, we have that C holds of b.

编写eq.subst H rfl时，精益需要弄清楚C应该具有的属性(或动机").这是一个高阶统一的示例:未知变量需要与lambda表达式统一.在 https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean .pdf ，以及 https://en上的一些常规信息.wikipedia.org/wiki/Unification_(computer_science)#Higher-order_unification .

When you write eq.subst H rfl, Lean needs to figure out what the property (or "motive") C is supposed to be. This is an example of higher order unification: the unknown variable needs to unify with a lambda expression. There's a discussion of this in section 6.10 in https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf, and some general information at 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，除非它具有此信息.

You're asking Lean to substitute a = b into succ a = succ a, without telling it what you're trying to prove. You could be trying to prove succ b = succ b, or succ b = succ a, or even succ a = succ a (by substituting nowhere). Lean can't infer the motive C unless it has this information.

通常，很难进行手动"替换(使用eq.rec，subst等)，因为更高阶的统一是复杂且昂贵的.您通常会发现，最好使用rw(重写)这样的策略:

In general, doing substitutions "manually" (with eq.rec, subst, etc) is difficult, since higher order unification is finicky and expensive. You'll often find that it's better to use tactics like rw (rewrite):

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

如果您想变得聪明，可以使用Lean的方程式编译器，并且a=b的唯一"证明是rfl:

If you want to be clever, you can make use of Lean's equation compiler, and the fact that the "only" proof of a=b is rfl:

lemma succ_over_equality : Π (a b : natural),
   a = b → (natural.succ a) = (natural.succ b)
| ._ _ rfl := rfl

这篇关于证明后继者对平等的替代性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！