Isar证明中的驯服元蕴涵

Question

证明了一个简单的定理，我在证明中遇到了元级的含义。拥有它们是可以的还是可以避免的？如果我要处理这些问题，这是否正确的做法？

theory Sandbox
imports Main
begin

lemma "(x::nat) > 0 ∨ x = 0"
proof (cases x)
  assume "x = 0"
  show "0 < x ∨ x = 0" by (auto)
next
  have "x = Suc n ⟹ 0 < x" by (simp only: Nat.zero_less_Suc)
  then have "x = Suc n ⟹ 0 < x ∨ x = 0" by (auto)
  then show "⋀nat. x = Suc nat ⟹ 0 < x ∨ x = 0" by (auto)
qed

end

我想这可以更容易证明，但我想有一个结构化的证明。

Answer 1

从原则上讲，元蕴涵==>不是什么可以避免的(事实上，它是在Isabelle中表达推理规则的“原生”方式)。有一种规范的方法，通常允许我们在写Isar证明时避免元含义。例如，为了一个总体目标

"!!x. A ==> B"

我们可以用Isar写

fix x
assume "A"
...
show "B"

对于具体的示例，在Isabelle/jEdit中查看它时，您可能会注意到第二种情况的n是高亮显示的。原因是它是一个自由变量。虽然这本身并不是一个问题，但在本地修复这些变量更为规范(就像典型的语句“用于任意但固定的.”)。在教科书中)。例如，

next
  fix n
  assume "x = Suc n"
  then have "0 < x" by (simp only: Nat.zero_less_Suc)
  then show "0 < x ∨ x = 0" ..
qed

在这里，可以再次看到fix/assume/show在Isar中如何与实际目标相对应，即，

1. ⋀nat. x = Suc nat ⟹ 0 < x ∨ x = 0

Answer 2

在编写结构化证明时，最好避免子目标最外层结构的元蕴涵(和量化)。也就是说，与其谈论

⋀x. P x ⟹ Q x ⟹ R x

你应该使用

fix x
assume "P x" "Q x"
...
show "R x"

如果P x和Q x有某种结构，则可以使用元蕴涵和-quantification。

在结构化证明中，选择fix/assumes而不是元操作符有很多原因。

• 在某种程度上，您不必在每一次have和Show语句中再次声明它们。
• 更重要的是，当您使用fix量化变量时，它在整个证明中保持不变。如果使用⋀，则在每个have语句中都会对其进行新的量化(并且不存在于外部)。这使得不可能直接引用这个变量，而且常常使自动工具的搜索空间复杂化。同样的情况也适用于assume和⟹。
• 更复杂的一点是show在元含义存在下的行为.考虑以下证明尝试： 引理"P⟷Q“证明"P⟹Q”抱歉下一次显示"Q⟹P“对不起qed 在proof命令之后，有两个子目标：P ⟹ Q和Q ⟹ P。然而，最终的qed失败了。怎么会出这事？ 第一个show将规则P ⟹ Q应用于第一个可应用的子目标，即P ⟹ Q。利用伊莎贝尔常用的规则分解机制，得到了Pandqedcannot close the goal. In many cases, we don't notice this behaviour ofshow, as trivial subgoals likeP P ⟹ P (assume Pwould have removed the subgoal). The second显示applies the ruleQ⟹P⟹Qagain. As a result, we are still have the two subgoalsP⟹Q⟹Q⟹P⟹Pcan be solved byq‘)。

关于show行为的几句话:正如我们在上面看到的，show中的元含义与assume不相对应。相反，它对应于assume的不太知名的兄弟presume。presume允许您引入新的假设，但要求您在之后执行它们。作为一个例子，比较

lemma "P 2 ⟹ P 0"
proof -
  presume "P 1" then show "P 0" sorry
next
  assume "P 2" then show "P 1" sorry
qed

和

lemma "P 2 ⟹ P 0"
proof -
  show "P 1 ⟹ P 0" sorry
next
  assume "P 2" then show "P 1" sorry
qed