我发现 plusNat 函数是在 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 类型的 Nat)?本质上,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/

10-11 17:37