Email Gateway (Aug 19 2022 at 11:27): Email Gateway (Aug 19 2022 at 11:27):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
try sledgehammer on these things. You can also use a more detailed Isar
proof:
lemma ineq:
fixes a::real and b::real
assumes "a > 0" "a < 1" "b > 0" "b < 0"
shows "a + b - a * b > 0"
proof-
from a < 1 and b > 0 have "b * (1 - a) > 0"
by (simp add: algebra_simps)
with a > 0 show ?thesis
by (simp add: algebra_simps)
qed
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 11:27):From: Tobias Nipkow <nipkow@in.tum.de>
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
Email Gateway (Aug 19 2022 at 11:27):From: Steffen Juilf Smolka <steffen.smolka@in.tum.de>
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
Last updated: Apr 25 2024 at 12:23 UTC