isabelle - 证明 isabelle 中的简单不等式

Question

我是 isabelle 的新手，并试图证明以下简单的不等式:

lemma ineq:
  "(a::real) > 0 ⟹ a < 1 ⟹ (b::real) > 0 ⟹ b < 1 ⟹ (a + b - a * b) > 0"
proof
  have "1/a + 1/b > 1" by auto
qed

我正在尝试使用上面的行来展示它，但无论我尝试什么(show、have、from 的几个组合)，它显然都不是那么容易，isabelle 展示了 Illegal application of proof command在“证明”模式下。我不知道这是什么意思。有人可以告诉我如何进行吗？

Answer 1

通常:如果 Isabelle 显示多个错误，您应该特别注意第一个错误。在这种情况下，“proof”命令已经给了你一个错误，它说:

Failed to apply initial proof method:
goal (1 subgoal):
 1. 0 < a ⟹ a < 1 ⟹ 0 < b ⟹ b < 1 ⟹ 0 < a + b - a * b

这是因为 proof隐含地尝试找到合适的引入规则并应用它。如果它不能做到这一点，它就会失败。你必须写 proof -在这种情况下告诉它不要做任何事情。

在一个不相关的注释上:

• 用 ⟹ 编写的假设引理陈述中的内容不会自 Action 为 Isar 中的事实提供。你需要 assume他们自己。或者，您可以使用 assumes在引理声明中，那么它们可作为名称assms 下的事实使用或者，您也可以给他们起名字。
• 类型注解b::real是多余的，可以从a的那个推断出来.
• 按照您的方式使用类型注释变量/子项很好，但作为提示，您也可以使用 fixes要做到这一点。对于大类型注释，它通常会使内容更清晰。
• throw auto在证明事物时，观察事物并查看剩下的东西是一个很好的标准策略，但您需要提供所有您拥有的事实(在您的情况下，a > 0、a < 1 等)。
• 即便如此，auto在这种情况下无能为力，因为它主要使用简化规则和经典逻辑推理。您的目标中没有逻辑连接词，默认的简化集中也没有匹配的简化规则，因此 auto 无法执行任何操作。
• algebra_simps是对群和环有用的简化引理的集合。 field_simps是相同的加上乘法逆和除法的一些规则。将它们喂给 simp/auto因为简化规则解决或简化了简单的代数问题。

因此，您可以将引理写成这种形式:

lemma ineq:
  fixes a b :: real
  assumes "a > 0" "a < 1" "b > 0" "b < 1"
  shows   "a + b - a * b > 0"
proof -
  from assms have "1/a > 1/2" and "1/b > 1/2" by (simp_all add: field_simps)
  hence "1/a + 1/b > 1" by simp
  with assms show ?thesis by (simp add: field_simps)
qed