Idris 证明中的案例分析

Question

所以我写了以下类型来证明整数的一些属性：

data Number : Type where
    PosN : Nat -> Number
    Zero : Number
    NegN : Nat -> Number

plusPosNeg : Nat -> Nat -> Number
plusPosNeg n m with (cmp n m)
    plusPosNeg (k + S d) k  | CmpGT d = PosN d
    plusPosNeg k k          | CmpEQ = Zero
    plusPosNeg k (k + S d)  | CmpLT d = NegN d

plus : Number -> Number -> Number
plus Zero y = y
plus x Zero = x
plus (PosN k) (PosN j) = PosN (k + j)
plus (NegN k) (NegN j) = NegN (k + j)
plus (PosN k) (NegN j) = plusPosNeg k j
plus (NegN k) (PosN j) = plusPosNeg j k

现在我想证明Zero 是加法的中性元素，这从plus 的定义中是很明显的。事实上，伊德里斯接受以下证明：

plusRZeroNeutral : {l : Number} -> plus l Zero = l
plusRZeroNeutral {l = Zero} = Refl
plusRZeroNeutral {l = PosN _} = Refl
plusRZeroNeutral {l = NegN _} = Refl

但拒绝我首先提出的较短版本：

plusRZeroNeutral : {l : Number} -> plus l Zero = l
plusRZeroNeutral {l} = Refl

我的问题是为什么会这样？查看plus 的定义，编译器似乎应该知道作为右参数传递给plus 的构造函数并不重要，只要左参数是Zero（反之亦然）。也许这是一个错误，或者我错过了什么？

Answer 1

如果您对l 的了解只是它是l（即某个任意参数），那么您将无法进一步减少plus l Zero，因为您被困在plus 的哪个分支上.

当您在例如模式匹配时l = Zero，右侧的类型现在被细化为plus Zero Zero = Zero，可以减少（通过plus的定义）到Zero = Zero。构造函数Refl 的类型很容易与这个细化的结果类型相结合，因此子句plusRZeroNeutral {l = Zero} = Refl 类型检查。

其他分支由您的第一个plusRZeroNeutral 定义的其他子句以类似方式处理。