Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] A proof for existential

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

From: Tjark Weber <webertj@in.tum.de>
Yes; see the attached Isabelle theory for an automatic proof.

Regards,
Tjark
John.thy

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

From: Tjark Weber <webertj@in.tum.de>
There's usually not much value in writing a manual proof when metis can
solve the goal. Anyway, I've attached both an apply-style proof, and an
Isar-style proof.

I recommend the Isabelle/HOL tutorial and Tobias Nipkow's "Tutorial
Introduction to Structured Isar Proofs" (both available from
http://isabelle.in.tum.de/documentation.html) for further reading.

Regards,
Tjark
John.thy

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

From: munddr@gmail.com
On Aug 5, 2010 1:10pm, Tjark Weber <webertj@in.tum.de> wrote:

On Thu, 2010-08-05 at 11:19 +0100, John Munroe wrote:

Thanks for the reply. What if ax2 was ax2 :"ALL x. (ALL y. x ~= y -->

hx > hy) --> gx = 0", would the lemma follow from ax1 and ax2 then?

Yes; see the attached Isabelle theory for an automatic proof.

Thanks. Just curious, without using metis, what would a manual proof look
like?

John

Regards,

Tjark

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

From: munddr@gmail.com
Hi all,

I've been stuck trying to find a proof for the following, could someone
please shed some light?

axiomatization
f :: "real => real" and
g :: "real => real" and
h :: "real => real" where
ax1: "EX x. ALL y. x ~= y => hx > h y" and
ax2 :"EX x. (ALL y. x ~= y => hx > hy) => gx = 0"

lemma "EX x. gx = 0"
oops

I've tried:

lemma "EX x. gx = 0"
using ax1 ax2
apply (intro exI)
apply (erule exE)+
apply (erule allE)
apply (erule impE)

which gives 2 subgoals, but they don't seem to be in the right direction...

Thanks for the help in advance.

Thanks
John

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

From: Tjark Weber <webertj@in.tum.de>
Dear John,

On Tue, 2010-08-03 at 18:29 +0000, munddr@gmail.com wrote:

I've been stuck trying to find a proof for the following, could someone
please shed some light?

axiomatization
f :: "real => real" and
g :: "real => real" and
h :: "real => real" where
ax1: "EX x. ALL y. x ~= y => hx > h y" and
ax2 :"EX x. (ALL y. x ~= y => hx > hy) => gx = 0"

Your formalization contains a few typos. Note that you need a space
between functions and their arguments, e.g. "h x" instead of "hx".
Also, => denotes function types, but implication must be written -->.

lemma "EX x. gx = 0"
oops

The lemma doesn't follow from ax1 and ax2. ax1 says that h has a strict
global maximum. ax2 says that there is an x such that if x is a strict
global maximum of h, then x is a root of g. (Note that the scope of the
existential quantifier extends all the way to the end of the formula.)

ax2 is actually a theorem (for any functions h and g, regardless of
ax1). Proof: simply choose some x that is not a strict global maximum
of h, then the implication becomes vacuously true.

So you're trying to show that g has a root, provided that h has a strict
global maximum. Well, it's no surprise you can't find a proof ...

Regards,
Tjark

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

From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
There is a parse problem with your axioms ax1 and ax2. I am assuming that by => you mean the operator --> which is the implication operator of HOL.

If so, the problem is that your goal is false. The real problem is that your second axiom is a truism. It says there exists an x which is a zero of g if it is a strict maximum of h. In fact there always exist infinitely many x which satisfy this property - they may not be zeroes of g, but they are not the strict maximum of h.

Yours,
Thomas.

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

From: John Munroe <munddr@gmail.com>
On Wed, Aug 4, 2010 at 8:41 AM, Thomas Sewell
<Thomas.Sewell@nicta.com.au> wrote:

There is a parse problem with your axioms ax1 and ax2. I am assuming that by => you mean the operator --> which is the implication operator of HOL.

Indeed. Apologies for the typo.

If so, the problem is that your goal is false. The real problem is that your second axiom is a truism. It says there exists an x which is a zero of g if it is a strict maximum of h. In fact there always exist infinitely many x which satisfy this property - they may not be zeroes of g, but they are not the strict maximum of h.

I'm a bit confused: If ax2 is a truism, why is the goal false? To
prove the goal, wouldn't I need to show that there exists some x which
is a strict maximum of h (ax1)?

Thanks
John

Yours,
   Thomas.

From: cl-isabelle-users-bounces@lists.cam.ac.uk [cl-isabelle-users-bounces@lists.cam.ac.uk] On Behalf Of munddr@gmail.com [munddr@gmail.com]
Sent: Wednesday, August 04, 2010 4:29 AM
To: isabelle-users@cl.cam.ac.uk
Subject: [isabelle] A proof for existential

Hi all,

I've been stuck trying to find a proof for the following, could someone
please shed some light?

axiomatization
f :: "real => real" and
g :: "real => real" and
h :: "real => real" where
ax1: "EX x. ALL y. x ~= y => hx > h y" and
ax2 :"EX x. (ALL y. x ~= y => hx > hy) => gx = 0"

lemma "EX x. gx = 0"
oops

I've tried:

lemma "EX x. gx = 0"
using ax1 ax2
apply (intro exI)
apply (erule exE)+
apply (erule allE)
apply (erule impE)

which gives 2 subgoals, but they don't seem to be in the right direction...

Thanks for the help in advance.

Thanks
John

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi John,

your lemma does not follow from your axioms, even after fixing your
typos. I guess you meant your axioms to be

ax1: "EX x. ALL y. x ~= y --> h x > h y" and
ax2: "EX x. (ALL y. x ~= y --> h x > h y) --> g x = 0"

Take g(x) = 1 and h(x) = if x = 0 then 1 else 2.
Then g and h satisfy both ax1 and ax2:
Take x=0 for the existential quantifier in ax1 and take x=1 for the
existential in ax2 (with y=0 for the universal quantifier).

Andreas

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

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi John,

in my previous post, the counter example was no counter example because
I had inverted all less signs in my head, but it is easily fixed:

Just take h(x) = if x = 0 then -1 else -2
instead of h(x) = if x = 0 then 1 else 2

Regards,
Andreas

Last updated: Apr 20 2024 at 08:16 UTC