isabelle - 如何在存在性证明中使用get？

Question

我试图证明一个存在定理

lemma "∃ x. x * (t :: nat) = t"
proof
  obtain y where "y * t = t" by (auto)

但我无法完成证明。所以我有必要y，但我怎样才能将它投入到最初的目标中呢？

Answer 1

show您可以在子句中给出见证（即您要为 x 放入的元素） ：

lemma "∃ x. x * (t :: nat) = t"
proof
  show "1*t = t" by simp
qed

Answer 2

自然演绎的健全性要求您在打开存在量词之前获得证人。这就是为什么不允许在show语句中使用已获得的变量的原因。在您的示例中，该proof步骤隐式应用了 rule exI。这将存在量化的变量x变成了示意图变量，可以稍后实例化，但实例化可能只引用到位?x时已经在范围内的变量。?x在低级证明状态下，获得的变量是元!!量化?x的?x（

因此，您必须在证明中切换顺序：

lemma "∃ x. x * (t :: nat) = t"
proof - (* method - does not change the goal *)
  obtain y where "y * t = t" by (auto)
  then show ?thesis by(rule exI)
qed

Answer 3

或者，当您已经知道见证人（1或Suc 0此处）时，您可以显式实例化规则exI以引入存在术语：

lemma "∃ x. x * (t :: nat) = t"
  by (rule exI[where x = "Suc 0"], simp)

这里，存在量词引入规则thm exI是

?P ?x ⟹ ∃x. ?P x

你可以用答案逐步探索和实例化它。

thm exI[where x = "Suc 0"]是：

?P (Suc 0) ⟹ ∃x. ?P x

并且exI[where P = "λ x. x * t = t" and x = "Suc 0"]是

Suc 0 * t = t ⟹ ∃x. x * t = t

并且Suc 0 * t = t只有一个简化（simp）。但是系统可以P = "λ x. x * t = t"通过统一计算出最后的实例化，所以它不是真的必要。

有关的：

在 Isabelle 中实例化定理