2

使用精益，计算机校样检查系统。

这些证明中的第一个成功，第二个没有。

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但这些其他命令对我没有帮助。

4

2 回答 2

3

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
于 2017-07-30T21:15:33.833 回答
2

首先，给函数起有意义的名称是一种很好的编程习惯。

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

现在，在您的第一个引理的情况下，阐述者将综合哪个术语是明确的。给定h1typen = m和h2of type 0 < n，细化器会做一些复杂的递归魔术n，它会根据需要替换min0 < n并产生一个 type 项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

这是因为现在对于阐述者将综合什么术语存在歧义。它可以代替或代替in n。由于深不可测的原因，阐述者选择做后者，产生一个类型的术语。结果不是 type 的术语，并且证明不进行类型检查。00n0 < nn < n0 < 0

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

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

正确排版。

于 2017-07-29T19:48:45.443 回答