如何证明Isabelle中递归函数满足特定输出的相关引理

这类递归函数输出等价性引理的通用证明方法 #

对于参数全为具体常量的测试类引理，直接用simp方法调用函数自动生成的简化规则即可完成证明，你给出的第一个示例仅需一行代码即可得证：

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

对于带自由变量的通用性质证明，通用流程如下：

• 优先使用非尾递归的自然形式定义函数，避免累加器参数带来的额外证明复杂度
• 调用函数自动生成的归纳规则（格式为函数名.induct）对参数做归纳
• 结合自然数、列表的基础简化规则完成归纳步的推导
• 如果必须使用尾递归实现，优先证明尾递归函数与非尾递归函数的等价性辅助引理，后续所有尾递归相关的证明都可以借助该辅助引理转用非尾递归版本的性质推导

具体问题解答 #

1. 函数定义是否优先采用尾递归形式？尾递归是否通常会简化定理证明流程？

不需要优先采用尾递归形式，尾递归不仅不会简化证明，大多数情况下反而会增加证明复杂度。
尾递归的核心价值是执行时的栈空间优化，仅在你需要将Isabelle函数提取为可执行的命令式代码时才有必要考虑。证明场景下非尾递归的原始递归形式更匹配归纳证明的结构，不需要处理额外的累加器参数等量关系，证明步骤会更简洁，你给出的count_from2证明远长于原始版本的证明就是典型例子。

2. 为什么函数的简化规则（count_from.simps 或 count_from2.simps）无法直接应用？

你给出的count_from的简化规则是可以直接应用的，参数为具体构造子组成的常量时，simp方法会自动匹配simps规则完成递归展开。你遇到无法应用的情况大概率是实际场景中函数参数包含自由变量，而非封闭的常量，此时simp无法完成全量展开就会中止。
count_from2的简化规则容易卡壳的原因是累加器参数参与的列表拼接操作@没有对应的简化规则匹配，变量状态下无法直接化简，才会出现规则无法应用的假象。

3. 要证明第一个引理，是否需要自定义对应的引入规则？

不需要。第一个引理的所有参数都是具体的常量值，仅靠默认的simp方法调用自动生成的简化规则就可以完成证明，完全不需要自定义引入规则。
只有当你需要批量证明大量同类型的引理时，才可以自定义引入规则来减少重复的证明步骤，单个场景下没有额外定义的必要。

4. 这类引理是否可以通过应用函数归纳规则完成证明？

完全可以，函数归纳规则正是这类递归函数性质证明的通用工具。
比如要证明更通用的性质count_from y x = map (λk. y + k) [0..<x]，只需要调用count_from自动生成的归纳规则即可完成：

lemma count_from_prop: "count_from y x = map (λk. y + k) [0..<x]"
  apply (induct y x rule: count_from.induct)
  by simp_all

对于尾递归版本count_from2，也可以用归纳法先证明辅助引理count_from2 y x ys = ys @ count_from y x，后续所有count_from2的性质都可以通过该辅助引理转换为count_from的性质推导，远比你手动反复调用elims的方案通用。

内容的提问来源于stack exchange，提问作者Denis