如何证明递归函数具有一定的价值

Question

这是一个平凡的函数和一个引理：

fun count_from where
  "count_from y 0 = []"
| "count_from y (Suc x) = y # count_from (Suc y) x"

lemma "count_from 3 5 = [3,4,5,6,7]"

这只是一个例子。真正的功能更复杂。

您能否建议如何证明这样的引理？

我使用尾递归重新定义了函数，并证明了引理如下：

fun count_from2 where
  "count_from2 y 0 ys = ys"
| "count_from2 y (Suc x) ys = count_from2 (Suc y) x (ys @ [y])"

lemma "count_from2 3 5 [] = xs ⟹ xs = [3,4,5,6,7]"
  apply (erule count_from2.elims)
  apply simp
  apply (drule_tac s="xs" in sym)
  apply (erule count_from2.elims)
  apply simp
  apply (drule_tac s="xs" in sym)
  apply (erule count_from2.elims)
  apply simp
  apply (drule_tac s="xs" in sym)
  apply (erule count_from2.elims)
  by auto

这肯定不是一个合适的解决方案。

我有几个问题：

1. 是否首选使用尾递归定义函数？它通常会简化定理证明吗？
2. 为什么不能应用函数简化规则（count_from.simps 或count_from2.simps）？
3. 我应该定义一个引入规则来证明第一个引理吗？
4. 是否可以应用函数归纳规则来证明这样的引理？

Answer 1

您的问题可能更好地表述为“我如何评估递归定义的函数并将该评估作为定理获得？”

答案是通常简化器应该在评估它时做得不错。这里的问题是像 1、2、3 这样的数字使用自然数的二进制表示，而函数是通过0 和Suc 上的模式匹配来定义的。这就是您的simps 无法应用的原因：它们仅匹配count_from ?y 0 或count_from ?y (Suc ?x) 形式的条款，而count_from 3 5 两者都不是。

你可以做的就是使用定理集合eval_nat_numeral，它只是将像1、2、3这样的数字重写为后继符号：

lemma "count_from 3 5 = [3,4,5,6,7]"
  by (simp add: eval_nat_numeral)

另一种可能性是code_simp 和eval 证明方法，它们试图通过评估它并检查您是否得到True 来证明在某种意义上是“可执行的”语句。他们都在这里工作正常：

lemma "count_from 3 5 = [3,4,5,6,7]"
  by code_simp

两者之间的区别在于 code_simp 使用简化器，它为您提供了通过 Isabelle 内核的“正确”证明（但对于更大的示例，这可能非常慢），而 eval 使用代码生成器作为受信任的预言机，因此可能不那么值得信赖（尽管我在实践中从未见过问题），但速度要快得多。

至于你的其他问题：不，我不明白归纳法在这里是如何应用的。我不知道你定义介绍规则是什么意思（它们会是什么样子？）。并且尾递归在证明事情方面并没有任何优势——事实上，如果你“人为地”使函数定义为尾递归，就像你为 count_from2 所做的那样，你实际上会让事情变得更加困难，因为你想要的任何属性证明然后需要额外的概括，然后才能通过归纳证明它们。一个经典的例子是普通与尾递归列表反转（我想你可以在“编程和证明”教程中找到）。

另请注意，库中已经存在与您的count_from 非常相似的函数：它被称为upt :: nat ⇒ nat ⇒ nat list，并具有[a..<b] 形式的自定义语法。它以升序为您提供a 和b-1 之间的自然数列表。查看“主要内容”文档以了解内容是个好主意。