Isabelle中proof与proof-的区别及证明失败问题咨询

核心区别 #

• proof（无参数）：会自动应用默认证明策略（通常是rule），尝试分解当前目标。对于even P这类谓词，它会展开even的定义（even n ≡ ∃k. n=2*k），将原目标even (a^2)转化为存在性目标a^2 = 2 * ?k，这就是你看到的证明状态变化。
• proof-：完全跳过初始策略应用，直接进入结构化证明模式，保留原始目标不变，让你完全手动控制后续证明步骤。

你的证明失败原因分析 #

当你用proof启动证明时，初始目标已经被拆分为a^2 = 2 * ?k，但后续用have ?thesis证明的是even (a^2)——这个结论和当前待解决的子目标类型不匹配，因此thus ?thesis无法将已证结论关联到pending的目标，最终导致报错。

不使用proof (rule)的修复方案 #

方案1：直接匹配拆分后的目标 #

既然proof已经把目标拆成了等式，直接针对这个等式构造证明：

theorem example:
  fixes a :: nat
  assumes h0: "even a"
  shows "even (a^2)"
proof
  obtain k where "a = 2*k" using h0 by (auto simp: even_def)
  thus "a^2 = 2 * (2*k^2)" by simp
qed

通过obtain从even a拿到a的分解式，再直接推导出a^2的偶数形式，匹配拆分后的目标。

方案2：用恒等策略保留原始目标 #

如果想继续用show ?thesis using h0 by auto的写法，可以用(id)策略（恒等策略，不做任何操作）替代proof-，效果完全一致：

theorem example:
  fixes a :: nat
  assumes h0: "even a"
  shows "even (a^2)"
proof (id)
  show ?thesis using h0 by auto
qed

方案3：从已证结论推导拆分后的目标 #

如果一定要保留have ?thesis的步骤，可以从已证的even (a^2)推导出拆分后的等式目标：

theorem example:
  fixes a :: nat
  assumes h0: "even a"
  shows "even (a^2)"
proof
  have "even (a^2)" using h0 by auto
  then show "a^2 = 2 * ?k" by (auto simp: even_def)
qed

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