proof - 在 Fin 上证明二元运算符的身份

Question

我已经定义了一个运算符，+-(忽略这个可怕的名字)，如下:

infixr 10 +-
(+-) : Fin (S n) -> Fin (S m) -> Fin (S (n + m))
(+-) {n} {m} FZ f' = rewrite plusCommutative n m in weakenN n f'
(+-) {n = S n} (FS f) f' = FS (f +- f')

目的是它的行为与 Fin 上定义的 + 完全一样，但结果的上限更严格 1。据我所知，它工作正常。

我遇到的问题是试图证明 (FZ +- f) = f 对于任何 f : Fin n。我并不期望这在一般情况下是正确的，因为通常情况下 FZ +- f 由于调用weakenN。但是，在 FZ 的类型为 Fin 1 的特定情况下，类型(和值)应该匹配。

有什么方法可以向 Idris 表明我只想断言特定情况下的相等性，而不是所有可能类型的 FZ？还是我应该采取完全不同的方法？

Answer 1

如果我们稍微调整一下 (+-) 的定义，证明就变得容易了:

import Data.Fin

infixr 10 +-
total
(+-) : Fin (S n) -> Fin (S m) -> Fin (S (n + m))
(+-) {n = Z}    {m = m} a      b = b
(+-) {n = (S n)}{m = m} FZ     b = rewrite plusCommutative (S n) m in weakenN (S n) b
(+-) {n = (S n)}{m = m} (FS a) b = FS (a +- b)

lem : (f : Fin (S n)) -> the (Fin 1) FZ +- f = f
lem FZ     = Refl
lem (FS x) = Refl

这是因为 (+-) 定义右侧的 rewrite 恰好规范化为具体值而不是替换/强制转换。

另一方面，如果我们想坚持 (+-) 的原始定义，那么 rewrite 不会消失，我们整个世界都充满了痛苦，因为现在我们必须面对异质性的平等。我在 Agda 中用异构等式做了一个证明，但是我无法在短时间内让它在 Idris 中工作，我相信让它工作将是一个相当痛苦的经历。 Here it is in Agda.

请注意，尽管我们必须在原始定义中再添加一个案例，以便首先证明关于它的属性是可行的。那是因为它没有按原样通过覆盖率检查器。我们很明显 Fin 1 只有 FZ 作为构造函数，但这也必须向编译器解释:

(+-) : Fin (S n) -> Fin (S m) -> Fin (S (n + m))
(+-) {n} {m} FZ f' = rewrite plusCommutative n m in weakenN n f'
(+-) {n = Z} (FS FZ) f' impossible
(+-) {n = S n} (FS f) f' = FS (f +- f')