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

现在我想证明，从plus的定义来看，Zero是加法的中性元素。事实上，Idris接受以下证据：

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 (反之亦然)。也许这是一个bug，或者我错过了什么？

Answer 1

如果您只知道l是l (即某个任意参数)，那么您就不能进一步减少plus l Zero，因为您被困在plus的哪个分支上。

例如，当你在l = Zero上进行模式匹配时，右边的类型现在被细化为plus Zero Zero = Zero，它可以被简化(通过plus的定义)为Zero = Zero。构造函数Refl的类型很容易与这种改进的结果类型相统一，因此子句plusRZeroNeutral {l = Zero} = Refl类型检查。

其他分支由您的第一个plusRZeroNeutral定义中的其他子句进行类似的处理。