Re: [isabelle] prove simple inequality



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
> 




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