Isabelle中如何用含示意变量的假设证明带约束变量的子目标

问题描述 #

使用sublocale做locale解释时，会生成一批带元全称量词（⋀）约束的子目标，这类子目标内容和已有locale中定义的假设完全一致，但直接引用对应假设时会生成示意变量，规则实例化仅支持替换自由变量，无法直接匹配带元全称量词约束的子目标。

当前待证子目标 #

1. ⋀n. plus n zero = n
 2. ⋀n m. plus n (suc m) = suc (plus n m)
 3. ⋀n. times n zero = zero
 4. ⋀n m. times n (suc m) = plus (times n m) n
 5. ⋀x. (zero = zero ∨ (∃m. suc m = zero)) ∧
         (x = zero ∨ (∃m. suc m = x) ⟶
          suc x = zero ∨ (∃m. suc m = suc x)) ⟶
         (∀x. x = zero ∨ (∃m. suc m = x))

可复用的已有Locale假设 #

locale th2 = th1 +
  fixes 
    plus :: "'a ⇒ 'a ⇒ 'a"
  assumes
     arith_1: "plus n zero = n"
    and plus_suc: "plus n (suc m) = suc ( plus n m)"

解决方法 #

出现匹配失败的核心原因是变量作用域不匹配：Locale中写的带自由变量的假设，在定理库中存储为上下文自由变量形式，而子目标前的⋀是元级全称量词，绑定的变量属于受约束的作用域，和定理中的自由示意变量不在同一层级，直接用rule类方法引用定理时无法自动完成替换。
对应解决操作如下：

• 最简便的方式是直接使用Isabelle内置的unfold_locales证明方法，该方法专为sublocale、locale解释场景设计：执行时会自动消解所有子目标前的元全称量词，把⋀绑定的变量转化为当前证明上下文中的固定自由变量，再自动搜索匹配上下文中已有的locale假设。列出的前4个子目标和th1、th2中的假设字面完全一致，调用该方法后会被自动解决，仅需单独处理第5个归纳相关子目标即可。
• 如果需要手动编写证明步骤，不要直接在带⋀的目标上套用定理，先通过fix语句把元量词绑定的变量转化为上下文固定变量，再引用对应假设即可完成匹配，示例证明框架如下：

  sublocale your_locale < th2
  proof (unfold_locales)
    (* 前4个算术相关子目标会被unfold_locales自动解决，此处仅需处理第5个归纳子目标 *)
    fix x
    show "(zero = zero ∨ (∃m. suc m = zero)) ∧
          (x = zero ∨ (∃m. suc m = x) ⟶
           suc x = zero ∨ (∃m. suc m = suc x)) ⟶
          (∀x. x = zero ∨ (∃m. suc m = x))"
    by (induction rule: th1.induct) (* 调用th1中已定义的结构归纳规则即可完成证明 *)
  qed
  

• 注意不要跳过变量固定步骤直接匹配定理：这种情况下定理中的自由变量是全局示意变量，和⋀绑定的局部约束变量无法统一，会出现实例化失败的问题。

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