Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proving lemmas containing a squareroot

view this post on Zulip Email Gateway (Aug 18 2022 at 15:26):

From: Michael Daniels <dayzman@gmail.com>
Hi

I'm hoping some of you could help me with the following lemma:

consts
pl :: "real => real"

axioms
gt: "EX x y. pl x > pl y"

lemma rt4: "ALL a b. sqrt(4) / pl a > sqrt(4) / pl b"
using gt
sledgehammer;

It seems like a rather simple lemma but sledgehammer (E, SPASS, and
Vampire) can't seem to return the set of theorems for metis. Does
anyone know how to prove it?

Moreover, if I simplify the lemma by removing the sqrt to:

lemma rt4: "ALL a b. (4) / pl a > (4) / pl b"
using gt
sledgehammer;

Vampire gives me a minimal set of 14 theorems for metis:

apply (metis comm_monoid_add.mult_commute comp_arith(112)
divide_inverse eq_diff_eq' eq_number_of inverse_inverse_eq
linorder_neqE_ordered_idom monoid_add_class.add_0_right
mult.diff_right mult.zero_left real_less_def real_mult_right_cancel
rel_simps(38) rel_simps(46))

However, metis actually will not terminate. Assuming those 14 theorems
are the required theorems, why is having sqrt so difficult for
sledgehammer?

Thanks!

Michael

view this post on Zulip Email Gateway (Aug 18 2022 at 15:26):

From: Brian Huffman <brianh@cs.pdx.edu>
On Thu, Jun 3, 2010 at 9:15 PM, Michael Daniels <dayzman@gmail.com> wrote:

Hi

I'm hoping some of you could help me with the following lemma:
...
lemma rt4: "ALL a b. sqrt(4) / pl a > sqrt(4) / pl b"
using gt
sledgehammer;

It seems like a rather simple lemma but sledgehammer (E, SPASS, and
Vampire) can't seem to return the set of theorems for metis. Does
anyone know how to prove it?

This lemma rt4 is obviously false. Consider the case where a and b are equal.

lemma rt4_wrong: "~ (ALL a b. sqrt(4) / pl a > sqrt(4) / pl b)"
apply simp
apply (rule exI [where x=1])
apply (rule exI [where x=1])
apply simp
done

Perhaps you meant "EX a b. sqrt(4) / pl a > sqrt(4) / pl b" ?

view this post on Zulip Email Gateway (Aug 18 2022 at 15:26):

From: Brian Huffman <brianh@cs.pdx.edu>
On Fri, Jun 4, 2010 at 8:11 AM, Michael Daniels <dayzman@gmail.com> wrote:

On Fri, Jun 4, 2010 at 3:36 PM, Brian Huffman <brianh@cs.pdx.edu> wrote:

Perhaps you meant "EX a b. sqrt(4) / pl a > sqrt(4) / pl b" ?

Indeed, I've sent a follow-up about the typo but it hasn't reached the
mailing list yet. What I meant is indeed EX rather than ALL. Any idea
on what theorems should be used here and why sledgehammer fails to
find any when it's sqrt?

If you are just interested in finding a proof, then here's one that works:

lemma exists_gt_conv_neq:
fixes f :: "real => real"
shows "(EX x y. f x > f y) = (EX x y. f x ~= f y)"
unfolding neq_iff by auto

lemma rt4: "EX a b. sqrt(4) / pl a > sqrt(4) / pl b"
using gt unfolding exists_gt_conv_neq by simp

But I think maybe your real question is why sledgehammer/metis are
having such trouble. One strategy you can try is to insert gt into the
subgoal before calling sledgehammer, instead of passing it via the
chained facts.

lemma rt4: "EX a b. sqrt(4) / pl a > sqrt(4) / pl b"
using gt
apply - (* this inserts axiom gt into the subgoal *)
sledgehammer;

Another thing you could do is realize that the only relevant property
of "sqrt(4)" is that it is positive. Sledgehammer and metis were able
to handle the following generalization:

lemma gt4': "0 < z ==> EX a b. z / pl a > z / pl b"
using gt apply -
sledgehammer;

Showing that "0 < sqrt(4)" is easy for the simplifier, but it requires
several extra rules to be passed to metis. (I think the numeral "4" is
actually a bigger problem than "sqrt".) The proof of the generalized
version gt4' is already rather difficult for metis (taking over a
minute on my machine), so I am not really surprised that the extra
complexity of "sqrt(4)" takes longer than you want to wait.

Thanks
Michael

view this post on Zulip Email Gateway (Aug 18 2022 at 15:26):

From: Michael Daniels <dayzman@gmail.com>
2010/6/4 grechukbogdan <grechukbogdan@yandex.ru>:

Hi

The lemma "ALL a b. (4) / pl a > (4) / pl b" is not correct. Counterexample a=b
May be, you wanted to say "EX a b. (4) / pl a > (4) / pl b"?

That's correct; sorry for the typo. Like wise for rt4 and it should
read "EX a b. sqrt(4) / pl a > sqrt(4) / pl b" instead. So anyone
knows what theorems are needed for rt4 and why metis won't terminate?

Thanks
Michael

Bogdan.

04.06.10, 08:15, "Michael Daniels" <dayzman@gmail.com>:

Hi

I'm hoping some of you could help me with the following lemma:

consts
 pl :: "real => real"

axioms
 gt: "EX x y. pl x > pl y"

lemma rt4: "ALL a b. sqrt(4) / pl a > sqrt(4) / pl b"
 using gt
 sledgehammer;

It seems like a rather simple lemma but sledgehammer (E, SPASS, and
 Vampire) can't seem to return the set of theorems for metis. Does
 anyone know how to prove it?

Moreover, if I simplify the lemma by removing the sqrt to:

lemma rt4: "ALL a b. (4) / pl a > (4) / pl b"
 using gt
 sledgehammer;

Vampire gives me a minimal set of 14 theorems for metis:

apply (metis comm_monoid_add.mult_commute comp_arith(112)
 divide_inverse eq_diff_eq' eq_number_of inverse_inverse_eq
 linorder_neqE_ordered_idom monoid_add_class.add_0_right
 mult.diff_right mult.zero_left real_less_def real_mult_right_cancel
 rel_simps(38) rel_simps(46))

However, metis actually will not terminate. Assuming those 14 theorems
 are the required theorems, why is having sqrt so difficult for
 sledgehammer?

Thanks!

Michael

--
Здесь спама нет http://mail.yandex.ru/nospam/sign

view this post on Zulip Email Gateway (Aug 18 2022 at 15:27):

From: Michael Daniels <dayzman@gmail.com>
On Fri, Jun 4, 2010 at 3:36 PM, Brian Huffman <brianh@cs.pdx.edu> wrote:

On Thu, Jun 3, 2010 at 9:15 PM, Michael Daniels <dayzman@gmail.com> wrote:

Hi

I'm hoping some of you could help me with the following lemma:
...
lemma rt4: "ALL a b. sqrt(4) / pl a > sqrt(4) / pl b"
using gt
sledgehammer;

It seems like a rather simple lemma but sledgehammer (E, SPASS, and
Vampire) can't seem to return the set of theorems for metis. Does
anyone know how to prove it?

This lemma rt4 is obviously false. Consider the case where a and b are equal.

lemma rt4_wrong: "~ (ALL a b. sqrt(4) / pl a > sqrt(4) / pl b)"
apply simp
apply (rule exI [where x=1])
apply (rule exI [where x=1])
apply simp
done

Perhaps you meant "EX a b. sqrt(4) / pl a > sqrt(4) / pl b" ?

Indeed, I've sent a follow-up about the typo but it hasn't reached the
mailing list yet. What I meant is indeed EX rather than ALL. Any idea
on what theorems should be used here and why sledgehammer fails to
find any when it's sqrt?

Thanks
Michael

view this post on Zulip Email Gateway (Aug 18 2022 at 15:27):

From: Michael Daniels <dayzman@gmail.com>
On Fri, Jun 4, 2010 at 6:07 PM, Brian Huffman <brianh@cs.pdx.edu> wrote:

On Fri, Jun 4, 2010 at 8:11 AM, Michael Daniels <dayzman@gmail.com> wrote:

On Fri, Jun 4, 2010 at 3:36 PM, Brian Huffman <brianh@cs.pdx.edu> wrote:

Perhaps you meant "EX a b. sqrt(4) / pl a > sqrt(4) / pl b" ?

If you are just interested in finding a proof, then here's one that works:

lemma exists_gt_conv_neq:
 fixes f :: "real => real"
 shows "(EX x y. f x > f y) = (EX x y. f x ~= f y)"
unfolding neq_iff by auto

lemma rt4: "EX a b. sqrt(4) / pl a > sqrt(4) / pl b"
using gt unfolding exists_gt_conv_neq by simp

I have a somewhat related question. How come the subgoal in rt2a isn't
unfolded, given:

consts
pl :: "real => real => real"
pm :: "real => real"
j :: real

axioms
gt1: "EX a b x y. pl (pm a) x > pl (pm b) y"
gt2: "EX x y. pl (pm j) x > pl (pm j) y"

lemma rt2a: "EX x y. ( 1/(pl (pm j) x)) > ( 1/ (pl (pm j) y))"
using gt2
unfolding exists_gt_conv_neq2
oops

whereas, the following is unfolded:

lemma rt2b: "EX x y. ( (pl (pm j) x)) > ( (pl (pm j) y))"
using gt2
unfolding exists_gt_conv_neq2
by simp

Also, if the argument to pm was an existential variable, then it is
also unfolded:

lemma exists_gt_conv_neq1:
fixes f :: "real => real => real"
shows "(EX a b x y. f a x > f b y) = (EX a b x y. f a x ~= f b y)"
unfolding neq_iff by blast

lemma rt1: "EX a b x y. ( 1/ (pl (pm a) x)) > ( 1/ (pl (pm b) y))"
using gt1
unfolding exists_gt_conv_neq1
by simp

How come giving pm a constant disables unfolding?

Thanks again.
Michael

Thanks
Michael

  • Brian

Last updated: Nov 21 2024 at 12:39 UTC