Isabelle结构化证明中含蕴含与存在量词的目标处理方法

问题背景 #

在使用Isabelle结构化风格编写除法定理证明时，需要补全证明中的sorry部分。已知证明逻辑，但不清楚如何在结构化风格中显式指定存在量词的变量取值。原证明代码如下：

lemma division_theorem: "lt Zero n ⟹ ∃ q r. lt r n ∧ m = add (mul q n) r"
proof (induct m)
  case Zero
  then show ?case
    by (metis add_zero_right mul.simps(1)) 
next
  case (Suc m)
  then show ?case
  proof (cases "Suc r = n")
    case True
    then show ?thesis sorry
  next
    case False
    then show ?thesis sorry
  qed
qed

其中Zero、add、mul是自定义的简易数论nat类型相关符号。当前生成的两个证明目标为：

1. (lt Zero n ⟹ ∃q r. lt r n ∧ m = add (mul q n) r) ⟹
    lt Zero n ⟹ cnat.Suc r = n ⟹ ∃q r. lt r n ∧ cnat.Suc m = add (mul q n) r
 2. (lt Zero n ⟹ ∃q r. lt r n ∧ m = add (mul q n) r) ⟹
    lt Zero n ⟹ cnat.Suc r ≠ n ⟹ ∃q r. lt r n ∧ cnat.Suc m = add (mul q n) r 

核心证明思路：

• 第一个目标：从归纳假设的存在量词中提取q和r，指定新的存在变量为q' = Suc q、r' = Zero
• 第二个目标：指定新的存在变量为q' = q、r' = Suc r

解决方案 #

结构化风格中处理存在量词的核心是用obtain提取归纳假设中的具体变量，再用exI规则显式指定新存在变量的取值。补全后的完整证明如下：

lemma division_theorem: "lt Zero n ⟹ ∃ q r. lt r n ∧ m = add (mul q n) r"
proof (induct m)
  case Zero
  then show ?case
    by (metis add_zero_right mul.simps(1)) 
next
  case (Suc m)
  -- 从归纳假设和前提中提取满足条件的q、r
  obtain q r where r_lt_n: "lt r n" and m_eq: "m = add (mul q n) r"
    using Suc.prems Suc.hyps by blast
  then show ?case
  proof (cases "Suc r = n")
    case True
    -- 构造新存在实例：q' = Suc q，r' = Zero
    show ?thesis
      by (rule exI[of _ "Suc q"], rule exI[of _ Zero],
          metis True r_lt_n m_eq add.simps(2) mul.simps(2) lt_zero)
  next
    case False
    -- 构造新存在实例：q' = q，r' = Suc r
    show ?thesis
      by (rule exI[of _ q], rule exI[of _ "Suc r"],
          metis False r_lt_n m_eq add.simps(2) lt_suc)
  qed
qed

关键步骤说明 #

1. obtain提取变量：
   obtain q r where ... using Suc.prems Suc.hyps by blast 将归纳假设中的存在量词转化为具体的变量q和r，并绑定它们满足的条件，后续证明可直接使用这两个变量。
2. exI指定存在变量值：
   rule exI[of _ <term>] 是存在引入规则的显式调用，of _ <term> 用来指定存在量词绑定的变量取值：
   • 第一个_是占位符，对应目标中存在量词的变量名
   • <term>是我们要给该变量赋的具体值
3. 自动推导剩余逻辑：
   最后用metis结合自定义的算术引理（如add.simps、mul.simps、lt_suc等）完成剩余的等式和不等式推导。

更清晰的结构化写法 #

也可以将存在实例的构造单独用have声明，提升可读性：

lemma division_theorem: "lt Zero n ⟹ ∃ q r. lt r n ∧ m = add (mul q n) r"
proof (induct m)
  case Zero
  then show ?case by (metis add_zero_right mul.simps(1)) 
next
  case (Suc m)
  obtain q r where r_lt_n: "lt r n" and m_eq: "m = add (mul q n) r" 
    using Suc.prems Suc.hyps by blast
  show ?case
  proof (cases "Suc r = n")
    case True
    have "∃ q r. lt r n ∧ Suc m = add (mul q n) r" 
      by (rule exI[of _ "Suc q"], rule exI[of _ Zero], 
          metis True r_lt_n m_eq add.simps(2) mul.simps(2) lt_zero)
    then show ?thesis .
  next
    case False
    have "∃ q r. lt r n ∧ Suc m = add (mul q n) r"
      by (rule exI[of _ q], rule exI[of _ "Suc r"],
          metis False r_lt_n m_eq add.simps(2) lt_suc)
    then show ?thesis .
  qed
qed

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