我发现 Nat 的 plus 函数是在 this way 中实现的
total plus : (n, m : Nat) -> Nat
plus Z right = right
plus (S left) right = S (plus left right)
我想知道是否有特殊原因不对第二个参数进行模式匹配，就像这里一样:
total plus : (n, m : Nat) -> Nat
plus Z right = right
plus left Z = left
plus (S left) right = S (plus left right)
正如我目前所看到的那样，此实现将使许多证明和代码的工作变得更简单。例如
total plusZeroRightNeutral : (left : Nat) -> left + 0 = left
plusZeroRightNeutral Z = Refl
plusZeroRightNeutral (S n) =
let inductiveHypothesis = plusZeroRightNeutral n in
rewrite inductiveHypothesis in Refl
看起来像plusZeroLeftNeutral:
total plusZeroRightNeutral : (left : Nat) -> left + 0 = left
plusZeroRightNeutral left = Refl
在现实生活中我们甚至不需要使用 plusZeroLeftNeutral 定理，因为 Idris 可以自动进行模式匹配(正如这个问题的答案中已经提到的:Concatenation of two vectors - why are lengths not treated as commutative?)。
那么为什么不添加额外的案例让生活更轻松呢？
最佳答案
实际上，plusZeroLeftNeutral 不能仅用Refl 来证明。
当您使用 Refl 时，您是在说:“这通过计算成立”(另一个名称是定义相等性或判断相等性)。
但是我们如何计算 left + 0(即 plus left Z for the Nat type)？本质上，Idris 从上到下逐个子句处理函数定义，在我们的例子中，它首先查看 plus Z right 子句。此时 Idris 需要决定 left 是否为 Z，但它不能，因为我们还没有析构 left。 Idris 不能跳过第一个子句并转到 plus left Z 子句。
现在，有了 plus 的替代定义，就不需要归纳来证明加法的右中性了:
total plusZeroRightNeutral : (left : Nat) -> plus left 0 = left
plusZeroRightNeutral Z = Refl
plusZeroRightNeutral (S _) = Refl
但另一方面，许多证明变得冗长，因为它们现在需要更多的模式匹配。让我们来看看加法的结合性。以下是 plus 原始定义的可能证明:
total plusAssoc : (m,n,p : Nat) -> m + (n + p) = m + n + p
plusAssoc Z n p = Refl
plusAssoc (S m) n p = cong $ plusAssoc m n p
这里作为修改后的plus的相应证明:
total plusAssoc : (m,n,p : Nat) -> m + (n + p) = m + n + p
plusAssoc Z n p = Refl
plusAssoc (S m) Z p = Refl
plusAssoc (S m) (S n) Z = Refl
plusAssoc (S m) (S n) (S p) = cong $ plusAssoc m (S n) (S p)
在这里，您被迫销毁 plus 函数出现的第二个参数，因为它们会阻止求值，但您需要将 S 构造函数移到能够利用您的归纳假设。
关于pattern-matching - `plus` 类型的 `Nat` 中第二个参数的附加模式匹配，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/49353735/