证明了伊莎贝尔的简单不平等

Question

我是伊莎贝尔的新手并试图证明以下简单的不等式:

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 in 'prove' mode.我不知道这是什么意思.有人可以说明如何继续吗？

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 -这个案子告诉它不要做任何事情.

在一个不相关的说明:

• ?在引理语句中写入的假设不会自动作为Isar中的事实提供.你assume自己需要它们.另外,您也可以使用assumes在引理声明,那么他们是可以作为名下的事实assms,或可选,您可以给他们的名字.
• 类型注释b::real是多余的,可以从中的一个推断出来a.
• 使用您所使用的方式注释变量/子类很好,但作为提示,您也可以使用fixes它来做.对于大型注释,它通常使事情更清晰.
• 投掷auto的东西,看什么仍然是一个很好的标准战术证明事情的时候,但你需要给它你的所有的事实(在你的情况,a > 0,a < 1,等).
• 即使这样,auto在这种情况下也无能为力,因为它主要使用简化规则和经典的逻辑推理.您的目标中没有逻辑连接词,默认的simpset中没有匹配的简化规则,因此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