proving simple inequality in isabelle

Question

I'm new to isabelle and tried to prove the following simple inequality:

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

I'm trying to show it using the line above but it clearly is not so easy as no matter what I try (a couple of combinations of show, have, from), isabelle shows Illegal application of proof command in 'prove' mode. I have no idea what this means. Can somebody illuminate me on how to proceed?

Manuel Eberl Manuel Eberl · Accepted Answer · 2015-07-15T09:47:39

As a rule: if Isabelle displays several errors, you should pay particular attention to the first one. In this case, the ‘proof’ command already gives you an error, and it says:

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

This is because proof implicitly tries to find a suitable introduction rule and apply it. If it cannot do that, it will fail. You have to write proof - in this case to tell it not to do anything.

On an unrelated note:

Assumptions written with ⟹ in the lemma statement are not automatically available as facts in Isar. You need to assume them yourself. Alternatively, you can use assumes in the lemma statement, then they are available as facts under the name assms or, optionally, you can give them names.
The type annotation b::real is redundant, it can be inferred from the one at a.
Annotating variables/subterms with types the way you did is fine, but just as a hint, you can also use fixes to do that. For big type annotations, it often makes things more legible.
Throwing auto at things and looking at what remains is a good standard tactic when proving things, but you need to give it all the facts that you have (in your case, a > 0, a < 1, etc.).
Even then, auto cannot do anything in this case, because it mainly uses simplification rules and classical logical reasoning. There are no logical connectives in your goal and there are no matching simplification rules in the default simpset, so auto cannot do anything.
algebra_simps is a collection of useful simplifiation lemmas for groups and rings. field_simps is the same plus some rules for multiplicative inverses and divisions. Feeding them to simp/auto as simplification rules solves or simplifies simple algebraic problems.

You can therefore write your lemma in this form:

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

proving simple inequality in isabelle

1 Answers