Re: [isabelle] prove simple inequality



There is actually another option since recently (assuming you are using the repository version of Isabelle). If you are interested in a step-by-step proof but don't won't to do the work yourself, you can try calling sledgehammer with the isar_proofs option:

lemma test:
  assumes a1: "(a::real)>0" and a2: "a<1" and b1: "(b::real)>0" and b2: "b<1"
  shows "a+b - a*b > 0"
sledgehammer [isar_proofs, isar_compress=2]

The isar_compress option lets you control the level of detail of the generated proof(s).
On my machine, sledgehammer came up with the following proof:

proof -
  have "a * b < b"
    by (metis a2 b1 comm_semiring_1_class.normalizing_semiring_rules(11) mult_strict_right_mono)
  hence "a * b < a + b"
    by (metis a1 pos_add_strict)
  thus "0 < a + b - a * b"
    by (metis add_less_imp_less_right comm_semiring_1_class.normalizing_semiring_rules(5) diff_add_cancel)
qed

I think the resulting proof is actually quite nice and easy to follow. (Unfortunately, it doesn't always work that well.)
The proof gets even nicer after some manual post-processing (which may be done automatically in the near future):

proof -
  have "a * b < b"
    by (simp add: algebra_simps a2 b1)
  hence "a * b < a + b"
    by (simp add: a1 pos_add_strict)
  thus "0 < a + b - a * b"
    by simp
qed

Regards,
Steffen

On 05.07.2013, at 15:02, cl-isabelle-users-request at lists.cam.ac.uk wrote:

> Dear Isabelle experts,
> 
> i have following simple lemma:
> 
> lemma ineq:
>  "(a::real) > 0 ⟹ a < 1 ⟹ (b::real) > 0 ⟹ b < 1 ⟹ (a + b - a * b) > 0"
> 
> My problem is that i cannot prove this lemma, i tried tools like 'simp' with algebra/field_simps etc. but i cannot figure out 
> which rule to use. Any help would be appreciated!
> 
> Regards,
> Michael



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.