瘦：eq.subst扼流器上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 

Answer 2

首先，给你的函数赋予有意义的名字是一种很好的编程习惯。

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

现在，在你的第一个引理的情况下，它是明确的elaborator将合成这个术语。鉴于n = m型h1和h20 < n类型中，elaborator确实some complicated recursor magic，其替代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 

这是因为现在有歧义什么长期的elaborator将合成。它可以替代n代替0或代替0代替n代替0 < n。由于不可理解的原因，阐述者选择做后者，产生n < n类型的术语。结果不是0 < 0类型的术语，证明没有类型检查。除去inambiguity

一种方法是在subst_zero_ineq证明使用subst_ineq，例如：

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

typechecs正确。