简化的 Idris 证明导致“类型不匹配”错误

Question

我正在通过这本书学习 Idris：https://idris-hackers.github.io/software-foundations/pdf/sf-idris-2018.pdf

在进入简化证明部分时，我有点遇到障碍（是的，一开始就是正确的）。我正在处理的一小段代码是：

namespace Numbers

  data Nat : Type where
    Zero : Numbers.Nat
    Successor : Numbers.Nat -> Numbers.Nat

  plus : Numbers.Nat -> Numbers.Nat -> Numbers.Nat
  plus Zero b = b
  plus (Successor a) b = Successor(plus a b)

这些更简单的证明可以正常工作：

One : Numbers.Nat
One = Successor Zero

Two : Numbers.Nat
Two = Successor One

Three : Numbers.Nat
Three = Successor Two

proofOnePlusZero : plus One Zero = One
proofOnePlusZero = Refl

proofOnePlusZero' : plus Zero One = One
proofOnePlusZero' = Refl

但是，当我尝试复制更复杂的证明时，我得到了一个错误

-- works
plus_Z_n : (n : Numbers.Nat) -> plus Zero n = n
plus_Z_n n = Refl

-- breaks / errors
plus_Z_n' : (n : Numbers.Nat) -> plus n Zero = n
plus_Z_n' n = Refl

这是错误

When checking right hand side of plus_Z_n' with expected type
        plus n One = Successor n

Type mismatch between
        Successor n = Successor n (Type of Refl)
and
        plus n (Successor Zero) = Successor n (Expected type)

Specifically:
        Type mismatch between
                Successor n
        and
                plus n (Successor Zero)

这是预期的行为 - 但建议是能够理解原因。我很茫然，正在寻找提示或如何考虑这一点。

Answer 1

这里 Idris 只是遵循定义（“简化证明”）。所以采取plus Zero n = n。为了简化这种类型，plus 的定义有帮助：一个分支定义了plus Zero b = b。所以我们可以用n 替换plus Zero n 来得到n = n，瞧。另一方面，如果尝试简化plus n Zero = n，则plus 定义中的所有分支都不匹配plus n Zero。因此无法进行替换，并且 Idris 被 plus n Zero = n 卡住了，直到您帮助​​ f.e.通过n 上的大小写拆分。

---

更准确地说，如果 Idris 尝试替换 plus x Zero，它会一个接一个地遍历所有分支并尝试匹配它们，就像它评估它一样。如果它可以匹配，它将停止。但只有分支等于plus x Zero，才会被替换。所以给定：

plus : Numbers.Nat -> Numbers.Nat -> Numbers.Nat
plus Zero b = b
plus a Zero = a
plus (Successor a) b = Successor(plus a b)

plus1 : plus n Zero = n
plus1 = Refl

这不会编译，因为plus n Zero 可以由plus Zero b = b 处理，这取决于n 是什么。但是因为n 是未知的，所以Idris 已经停在了这里，但是并没有取代它。所以没有到达第二个分支。