关于依赖于替代项顺序的函数的证明

Question

我在 Haskell 方面有相当多的经验，最近才开始使用 Idris 进行定理证明。这是一个最小的例子，说明了我在尝试证明相当简单的陈述时遇到的问题。

考虑我们有一个总函数 test:

total test : Integer -> Integer
test 1 = 1
test n = n

当然我们看到函数可以简化为test n = n，但让我们证明一下。我只是简单地回顾了所有的案例：

total lemma_test : (n : Integer) -> test n = n
lemma_test 1 = Refl
lemma_test n = Refl

但是，这没有类型检查：

Type mismatch between
        n = n (Type of Refl) and
        test n = n (Expected type)

Specifically:
        Type mismatch between
                n
        and
                test n

所以，问题似乎是 Idris 无法推断 lemma_test 的第二种情况 n 不等于 1 以及 [= 的第二种情况必须应用 14=]。

当然，我们可以尝试明确列出所有情况，这可能很麻烦，或者不可能，例如 Integers:

total lemma_test : (n : Integer) -> test n = n
lemma_test 1 = Refl
lemma_test 2 = Refl
lemma_test 3 = Refl
...

对于不是在有限的数据构造函数集上定义而是依赖于模式匹配从上到下工作的事实的函数，有没有办法证明这样的语句，比如 test这个例子？

考虑到像这样的功能经常出现，也许有一个我没有看到的相当简单的解决方案。

Answer 1

我不确定 Integer 是如何定义的，或者如何对其进行归纳等等，所以这不是您问题的完整答案；但也许 Nat 版本也能为您提供信息？（另外，也许您实际上是指 Nat，因为在您的第二个示例中您只列举了正自然数？）

如果您将 test 更改为使用 Nats:

total test : Nat -> Nat
test (S Z) = 1
test n = n

那么你可以在 lemma_test:

中进行详尽的模式匹配

total lemma_test : (n : Nat) -> test n = n
lemma_test (S Z) = Refl
lemma_test Z = Refl
lemma_test (S (S k)) = Refl

Answer 2

Integer 未在 Idris 中定义，而是遵循 GMP bigints。它对 Idris 来说实际上是不透明的，并且显然不是您可以通过这种方式在编译时推理的情况。对于类似 Nat 的归纳定义，您可以以基本情况和递归情况的形式讨论证明。

关于 n 不是 test n 的类型错误告诉您 Idris 无法减少表达式 test n。我不确定它应该如何表现 - 显然它是一个总功能，并且它应该减少总功能 afaik。也许这与 Integer 对 Idris 的不透明度有关？

您可以通过引入自由变量作为 labmda 参数来测试 repl 的减少。例如。 \n => test n 只是回应 \n => test n : Integer -> Integer（没有任何改变），但是，如果您从定义中删除 test 1 = 1 案例并重试，它会回应 \n => n : Integer -> Integer - 它减少了 test n 到 n。然后您的证明将按原样工作。

Answer 3

正如其他人所说，Integer 是原始类型，而不是归纳定义的 Idris 类型，因此我们无法对其进行详尽的模式匹配。更具体地说，问题是在 Idris 中（实际上在最先进的 Agda 中也是如此！）我们无法真正证明关于 "default" 模式匹配的事情，因为它们不携带关于所有模式匹配的信息先前未能匹配的模式。在我们的例子中，test n = 1 没有给我们证据表明 n 不等于 1。

通常的解决方案是使用可判定的相等性（Boolean 相等性也可能很好）而不是失败：

import Prelude

%default total

test : Integer -> Integer
test n with (decEq n 1)
  test n | Yes p = 1
  test n | No  p = n

lemma_test : (n : Integer) -> (test n) = n
lemma_test n with (decEq n 1)
 lemma_test _ | (Yes Refl)  = Refl
 lemma_test n | (No contra) = Refl

此处，No 结果带有关于失败匹配的明确证据。

关于依赖于替代项顺序的函数的证明

Proofs about functions that depend on the ordering of their alternatives

pattern-matching

dependent-type

idris

theorem-proving