精益 : eq.subst h 窒息:(n=0)

Question

使用 Lean，计算机校对系统。

第一个证明成功，第二个不成功。

variables n m : nat

theorem works (h1 : n = m) (h2 : 0 < n) : (0 < m) :=
eq.subst h1 h2

theorem nowrk (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
eq.subst h3 h4

错误发生在 eq.subst 中，错误如下：

"eliminator" elaborator type mismatch, term
  h4
has type
  0 < n
but is expected to have type
  n < n

[然后是一些附加信息]

我不明白错误信息。我在假设中尝试了各种明显的排列，例如 0 = n 或 n > 0，但我无法让它工作，也无法产生我能理解的错误消息。

谁能澄清一下？我阅读了有关 congr_arg 等的 Theorem Proving In Lean 部分，但这些其他命令对我没有帮助。

Answer 1

首先，为您的函数指定有意义的名称是一种很好的编程习惯。

第一个引理可以称为 subst_ineq_right 或 subst_ineq，如果从上下文中可以清楚地看出您总是在右边替换。

现在，对于您的第一个引理，阐述者将综合哪个术语是明确的。给定 n = m 类型的 h1 和 0 < n 类型的 h2，细化者执行，用 n 代替 m 0 < n 并根据需要生成 0 < m 类型的术语：

lemma subst_ineq (h1 : n = m) (h2 : 0 < n) : (0 < m) :=
    eq.subst h1 h2

不幸的是，这在你的第二个引理中失败了，比如 subst_zero_ineq

lemma subst_zero_ineq (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
    eq.subst h3 h4

这是因为现在对阐述者将合成的术语存在歧义。它可以用 n 代替 0，或者用 0 代替 0 < n 中的 n。出于莫名其妙的原因，阐述者选择了后者，产生了 n < n 类型的术语。结果不是 0 < 0 类型的术语，并且证明不进行类型检查。

消除歧义的一种方法是在 subst_zero_ineq 的证明中使用 subst_ineq，例如：

lemma subst_zero_ineq (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
    subst_ineq n 0 h3 h4

类型检查正确。

Answer 2

eq.subst 依靠高阶统一来计算替换的动机，这本质上是一种启发式的和有点挑剔的过程。在你的第二种情况下，精益的启发式方法失败了。（您可以在错误消息中看到不正确的动机。）还有其他方法可以更智能地执行此操作。

使用自动化：

theorem nowrk (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
by simp * at * -- this may not work on 3.2.0

theorem nowrk2 (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
by cc

使用重写：

theorem nowrk3 (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
by rw h3 at h4; assumption

使用eq.subst并明确给出动机：

theorem nowrk4 (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
@eq.subst _ (λ h, 0 < h) _ _ h3 h4

theorem nowrk4' (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
@eq.subst _ ((<) 0) _ _ h3 h4 -- more concise notation for the above

使用计算模式：

theorem nowrk5 (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
calc 0 < n : h4
   ... = 0 : h3

使用模式匹配：

theorem nowork6 : Π n, n = 0 → 0 < n → 0 < 0
| ._ rfl prf := prf

精益 : eq.subst h 窒息:(n=0)

lean : eq.subst chokes on h:(n=0)

theorem-proving

lean