如何在存在证明中使用获取？

Question

我试图证明一个存在定理

\n\n

lemma "\xe2\x88\x83 x. x * (t :: nat) = t"\nproof\n  obtain y where "y * t = t" by (auto)\n

\n\n

但我无法完成证明。所以我有了必要的东西y，但我怎样才能将其纳入最初的目标呢？

\n

Answer 1

自然演绎的合理性要求你在打开存在量词之前先找到证人。这就是为什么不允许在show语句中使用获得的变量的原因。在您的示例中，该proof步骤隐式应用规则exI。这会将存在量化变量转换x为原理图变量?x，稍后可以对其进行实例化，但实例化可能仅引用出现时已在范围内的变量?x。在低级证明状态下，获得的变量被元量化（!!），并且 的实例化?x只能引用作为 的参数出现的变量?x。

\n\n

因此，您必须更改证明中的顺序：

\n\n

lemma "\xe2\x88\x83 x. x * (t :: nat) = t"\nproof - (* method - does not change the goal *)\n  obtain y where "y * t = t" by (auto)\n  then show ?thesis by(rule exI)\nqed\n

\n

Answer 2

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

\n\n

lemma "\xe2\x88\x83 x. x * (t :: nat) = t"\nproof\n  show "1*t = t" by simp\nqed\n

\n