伊莎贝尔 - 需要 exI 和 refl 行为解释

Question

我正在尝试理解下面的引理。

• 为什么exI中引入了?y2原理图变量？
• 为什么在 refl 中不考虑它(因此:x = x)？

lemma "∀x. ∃y. x = y"   
  apply(rule allI)     (*  ⋀x.      ∃y. x = y *)
  thm exI              (*  ?P ?x ⟹ ∃x. ?P x  *)
  apply(rule exI)      (*  ⋀x. x = ?y2 x      *)
  thm refl             (*  ?t = ?t            *)   
  apply(rule refl)   
done

<小时/>

更新(因为我无法格式化注释中的代码):

这是具有不同证明的相同引理，使用simp。

lemma "∀x. ∃y. x = y"
  using [[simp_trace, simp_trace_depth_limit = 20]]
  apply (rule allI)  (*So that we start from the same problem state. *)   
  apply (simp only:exI) 
done

跟踪显示:

[0]Adding rewrite rule "HOL.exI":
?P1 ?x1 ⟹ ∃x. ?P1 x ≡ True 
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
⋀x. ∃y. x = y 
[1]Applying instance of rewrite rule "HOL.exI":
?P1 ?x1 ⟹ ∃x. ?P1 x ≡ True    
[1]Trying to rewrite:
x = ?x1 ⟹ ∃xa. x = xa ≡ True   <-- NOTE: not ?y2 xa or similar!
[2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
x = ?x1 
[1]SUCCEEDED
∃xa. x = xa ≡ True

显然 simp 和 rule 处理 exI 的方式不同。剩下的问题是:规则行为背后的机械(编程)推理是什么。

Answer 1

当您使用rule thm时对于某些事实thm ，Isabelle 对 thm 的结论进行高阶统一与当前的目标。如果有统一符，则用它实例化定理的目标和结论，然后进行解析(即将目标替换为 thm 的假设)。

这意味着:

1. 目标中的原理图变量可以通过 rule 实例化通过统一

2. 仅出现在 thm 假设中的变量不会被统一实例化，因此仍然是示意性的。这样，您最终就会在新目标中获得示意性变量。这些变量在某种意义上可以被视为存在，因为thm的结论如果您可以证明一个任意值的假设，则成立。

以exI为例，你有?P ?x ⟹ ∃x. ?P x 。当您申请rule exI ，变量?P实例化为λy. x = y ，但是变量?x仅出现在 exI 的假设中，所以它仍然是示意性的。这意味着您可以为 ?x 选择任何您想要的值。稍后在你的证明中。

更准确地说，您最终得到 ⋀x. x = ?y2 x作为你的目标。您可能会问‘为什么不只是 ⋀x. x = ?y2 ？’这意味着您必须证明 x等于某个固定值y2对于x的所有可能值。一般来说，这显然是不正确的。 ⋀x. x = ?y2 x意味着你必须证明每个 x等于一些y2这可能取决于x – 或者，等效地，有一个函数 y2当给定 x 时，输出x .

当然，有这样一个函数，它就是恒等函数 λx. x 。这正是 ?y2当您申请 rule refl 时被实例化:目标x = ?y2 x与refl ?t = ?t的结论统一你最终得到 ?t = x和?y2 = λx. x ，并且自 refl没有任何假设，这个决议完成了证明。

我不完全确定你的意思是“以及为什么它没有在 refl 中考虑” ？”，但我希望我已经回答了您的问题。