用计数器证明求和函数的正确性

Question

给定以下求和函数：

function sum :: "nat ⇒ nat ⇒ nat" where
"sum i N = (if i > N then 0 else i + sum (Suc i) N)"
by pat_completeness auto
termination sum
apply (relation "measure (λ(i,N). N + 1 - i)")
apply auto
done

停止条件是根据N和i。我通常对列表进行归纳，所以我真的不知道如何证明这个功能。

能否请您提供下一个证明的解决方案和说明？

lemma sum_general[simp] : "c ≤ n ⟹ 2 * sum c n + (c - 1) * c = n * (n + 1)

Answer 1

当您想证明由 function 命令定义的 recursively-defined 函数以及递归超出原始递归的地方时，最好的方法通常是使用归纳规则function 命令为您提供：

lemma "i ≤ N ⟹ N * Suc N = 2 * sum i N + i * (i - 1)"
proof (induction i N rule: sum.induct)
  case (1 i N)
  show ?case
  proof (cases "i = N")
  case True
  thus ?thesis sorry
next
  case False
  thus ?thesis sorry
qed

这使您可以访问归纳假设为“1.IH”。我还已经添加了您需要的区分大小写。

请注意，function 包将 sum (sum.simps) 的定义方程注册为 simp 规则。这在这里不是一个好主意，因为它可以使简化器循环，因为方程式不受保护。我通常从 simp 集中删除等式并添加受保护的版本来避免这种情况：

lemmas [simp del] = sum.simps

lemma sum_simps [simp]: "i > N ⟹ sum i N = 0" "i ≤ N ⟹ sum i N = i + sum (Suc i) N"
  by (auto simp: sum.simps)

用计数器证明求和函数的正确性

proof of correctness for summation function with a counter

isabelle

proof-of-correctness