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

Question

我试图从"精益证明中的证据"第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和succ来自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

Answer 1

1. eq被定义为

   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是类型值而不是支持值,则有类似的解释.)

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表达式统一.有这个在6.10节讨论https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf,在一些常规信息https://en.wikipedia.org/wiki/Unification_(computer_science)#Higher-order_unification.

4. 你问精益替换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