theorem-proving - 精益 : eq. h 上的替代扼流圈:(n=0)

Question

使用精益计算机校对系统。

第一个证明成功，第二个证明失败。

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

Answer 1

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