*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] prove simple inequality*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 05 Jul 2013 15:01:32 +0200*In-reply-to*: <fb9efb751ad816.51d5611b@rwth-aachen.de>*References*: <fb9efb751ad816.51d5611b@rwth-aachen.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:17.0) Gecko/20130620 Thunderbird/17.0.7

This is a cute one. For a start, it is (a) non-linear and (b) not provable by just multiplying things out and reasoning modulo AC, which is essentially what algebra/field_simps are doing. At first I tried what I thought to be the perfect match, namely I imported "~~/src/HOL/Library/Sum_of_Squares", a proof procedure esp for non-linear inequalities by John Harrison. Unfortunately, although the problem is simple, "by sos" did not work (in the amount of time I waited). Then I did what Manuel already suggested and got this: by (metis add_less_cancel_left comm_monoid_add_class.add.right_neutral comm_monoid_mult_class.mult.left_neutral comm_semiring_1_class.normalizing_semiring_rules(24) diff_add_cancel pos_add_strict real_mult_less_iff1) Not very informative, but it does the job. Although sledgehammer is unlikely to be effective on more complicated arithmetic formulas. Having seen Manuel's proof and the fact that one assumption is not needed, I tried John's sos again and got this proof with certificate: by (sos_cert "((((A<0 * (A<1 * A<2)) * R<1) + (((A<2 * R<1) * (R<1/4 * [a]^2)) + (((A<1 * R<1) * (R<1/4 * [~1*a + b]^2)) + (((A<0 * R<1) * (R<1/4 * [a]^2)) + (((A<=0 * (A<2 * R<1)) * (R<1/4 * [1]^2)) + ((A<=0 * (A<0 * R<1)) * (R<1/4 * [1]^2))))))))") Again, a bit cryptic, but for general non-linear inequalities sos is the recommended method. Tobias Am 04/07/2013 11:48, schrieb Michael Vu: > 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 >

**References**:**[isabelle] prove simple inequality***From:*Michael Vu

- Previous by Date: Re: [isabelle] prove simple inequality
- Next by Date: [isabelle] SMT and bound variables.
- Previous by Thread: Re: [isabelle] prove simple inequality
- Next by Thread: [isabelle] Tutorial 'Mechanised Reasoning in Economics' (Koblenz, Germany, 17 Sept.): early registration until 15 July
- Cl-isabelle-users July 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list