对于"0"的介绍规则.在伊莎贝尔 [英] Intro rule for "∀r>0" in Isabelle

问题描述

当我有一个目标，例如伊莎贝尔(Isabelle)中的"∀x. P x"时，我知道我会写

When I have a goal such as "∀x. P x" in Isabelle, I know that I can write

show "∀x. P x"
proof (rule allI)

但是，当目标是"∀x>0. P x"时，我无法做到这一点.我可以在proof之后使用类似的规则/方法来简化目标吗?对于您的目标格式为"∃x>0. P x"的情况，我也会对此感兴趣.

However, when the goal is "∀x>0. P x", I cannot do that. Is there a similar rule/method that I can use after proof in order to simplify my goal? I would also be interested in one for the situation where you have a goal of the form "∃x>0. P x".

我正在寻找使用proof (rule something)样式的Isar证明.

I'm looking for an Isar proof that uses the proof (rule something) style.

推荐答案

通用量词

进一步解释Lars的答案:∀x>0. P x只是∀x. x > 0 ⟶ P x的语法糖.结果，如果要证明这样的陈述，则首先必须用allI除去通用量词，然后用impI除去含义.您可以执行以下操作:

Universal quantifier

To expand on Lars's answer: ∀x>0. P x is just syntactic sugar for ∀x. x > 0 ⟶ P x. As a consequence, if you want to prove a statement like this, you first have to strip away the universal quantifier with allI and then strip away the implication with impI. You can do something like this:

lemma "∀x>0. P x"
proof (rule allI, rule impI)

或使用intro，它与应用rule几乎相同，直到不再可用为止:

Or using intro, which is more or less the same as applying rule until it is not possible anymore:

lemma "∀x>0. P x"
proof (intro allI impI)

或者您可以使用safe，它会急切应用所有声明为安全"的介绍规则，例如allI和impI:

Or you can use safe, which eagerly applies all introduction rules that are declared as ‘safe’, such as allI and impI:

lemma "∀x>0. P x"
proof safe

无论如何，您的新证明状态为

In any case, your new proof state is then

proof (state)
goal (1 subgoal):
 1. ⋀x. 0 < x ⟹ P x

您可以这样进行:

lemma "∀x>0. P (x :: nat)"
proof safe
  fix x :: nat assume "x > 0"
  show "P x"

请注意，我添加了注释；我不知道您的P具有什么类型，所以我只使用了nat.当您在Isar中修复变量并且假设中的类型不清楚时，您将收到警告，提示您引入了新的自由类型变量，这不是您想要的.当您收到该警告时，您应该像上面所做的那样向fix添加类型注释.

Note that I added an annotation; I didn't know what type your P has, so I just used nat. When you fix a variable in Isar and the type is not clear from the assumptions, you will get a warning that a new free type variable was introduced, which is not what you want. When you get that warning, you should add a type annotation to the fix like I did above.

对于存在量词，safe将不起作用，因为由于技术原因，介绍规则exI并不总是安全的. ∃x>0. P x的典型证明模式如下:

For an existential quantifier, safe will not work because the intro rule exI is not always safe due to technical reasons. The typical proof pattern for an ∃x>0. P x would be something like:

lemma "∃x>0. P (x :: nat)"
proof -
  have "42 > (0 :: nat)" by simp
  moreover have "P 42" sorry
  ultimately show ?thesis by blast
qed

或更明确地说:

lemma "∃x>0. P (x :: nat)"
proof -
  have "42 > 0 ∧ P 42" sorry
  thus ?thesis by (rule exI)
qed

如果存在的见证人(即本示例中的42)不依赖于您从obtain命令中获得的任何变量，那么您也可以直接进行以下操作:

In cases when the existential witness (i.e. the 42 in this example) does not depend on any variables that you got out of an obtain command, you can also do it more directly:

lemma "∃x>0. P (x :: nat)"
proof (intro exI conjI)

这将为您提供目标?x > 0和P ?x.请注意，?x是一个示意图变量，您可以为它添加任何内容.因此，您可以像这样完成证明:

This leaves you with the goals ?x > 0 and P ?x. Note that the ?x is a schematic variable for which you can put it anything. So you can complete the proof like this:

lemma "∃x>0. P (x :: nat)"
proof (intro exI conjI)
  show "42 > (0::nat)" by simp
  show "P 42" sorry
qed

正如我所说，如果存在的见证人由于技术限制而依赖于您从obtain获得的某些变量，那么这不会奏效.在这种情况下，您必须使用我提到的其他解决方案.

As I said, this does not work if your existential witness depends on some variable that you got from obtain due to technical restrictions. In that case, you have to fall back to the other solution I mentioned.

这篇关于对于"0"的介绍规则.在伊莎贝尔的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！