3

我已经定义了一个运算符，+-（忽略可怕的名字），如下：

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比f调用weakenN. 但是，在FZ具有类型的特定情况下Fin 1，类型（和值）应该匹配。

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

4

1 回答 1

2

如果我们(+-)稍微改一下定义，证明就变得容易了：

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 中工作，而且我相信让它工作将是一个相当痛苦的经历。这是在阿格达。

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

(+-) : 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')
于 2015-07-26T18:38:33.203 回答