0

我正在阅读第 5 章（Isar）并尝试进行结构归纳证明，"Σ{0..n::nat} = n*(n+1) div 2"但失败了：

lemma "Σ{0..n::nat} = n*(n+1) div 2" 
proof (induction n)
  show "Σ{0..0::nat} = 0*(0+1) div 2" by simp
next
  fix n 
  assume "Σ {0..n} = n * (n + 1) div 2"
  thus "Σ {0..Suc n} = Suc n * (Suc n + 1) div 2" by simp
qed

它说：

show Σ {0..0} = 0 * (0 + 1) div 2 
Successful attempt to solve goal by exported rule:
  Σ {0..0} = 0 * (0 + 1) div 2 
proof (state)
this:
  Σ {0..0} = 0 * (0 + 1) div 2

goal (1 subgoal):
 1. ⋀n. Σ {0..n} = n * (n + 1) div 2 ⟹ Σ {0..Suc n} = Suc n * (Suc n + 1) div 2 
Failed to finish proof⌂:
goal (1 subgoal):
 1. Σ {0} = 0

我不知道为什么。大锤也没有解决。我确实尝试过blast，auto等等，但我知道他们会失败，因为大锤之前曾向我提出过​​这些建议，但值得一试吗？

我尝试使用应用样式来查看发生了什么：

lemma "Σ{0..n::nat} = n*(n+1) div 2"
  apply (induction n)
   apply simp
apply simp

同样的错误：

proof (prove)
goal (2 subgoals):
 1. Σ {0} = 0
 2. ⋀n. Σ {0..n} = n * (n + 1) div 2 ⟹ Σ {0..Suc n} = Suc n * (Suc n + 1) div 2 
Failed to apply proof method⌂:
goal (2 subgoals):
 1. Σ {0} = 0
 2. ⋀n. Σ {0..n} = n * (n + 1) div 2 ⟹ Σ {0..Suc n} = Suc n * (Suc n + 1) div 2

为什么这不起作用？我的 Isabelle 安装有问题吗？

我还尝试了一个没有任何东西的文件的证明，它也失败了，所以它不是我之前的任何定义（我假设很有可能）。

4

1 回答 1

0

似乎去右下角我可以手动插入符号是一个坏主意。它插入符号 sigma 而不是 Sum。我通过做来修复它\<Sum>（实际上我用标签自动完成）。证明现在有效：

lemma "∑{0..n::nat} = n*(n+1) div 2"
  apply (induction n)
   apply simp
  by simp
于 2020-05-18T20:44:11.210 回答