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 的第一个定义的其他子句类似地处理。

Idris 证明中的案例分析

Case analysis in Idris proofs

pattern-matching

proof

idris