Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proving a simple lemma

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

From: dayzman@gmail.com
Hi all,

I'm trying to prove a simple lemma, but am stuck at the last proof step:

lemma test_wrong:
fixes f :: "real => real"
shows "(EX x y. fx ~= fy) --> ~(EX x y. fx > fy)"
apply (rule impI)
apply (rule notE)
apply auto

goal (1 subgoal):

  1. !!(x::real) y::real. fx ~= fy --> False

I think I'm supposed to let x be y, but how do I do that in Isar? Also, is
what I've done so far reasonable?

Thanks for the help.

Michael

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

From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Michael,

The conjecture is not valid. Indeed, Nitpick (which you can invoke by typing "nitpick" after the statement of the lemma or at any point in the proof) gives a counterexample.

One problem seems to be that you should put a space between "f" and "x" (or "y"). The second problem is that there shouldn't be any negation in the right-hand side of "-->".

Regards,

Jasmin

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

From: Joachim Breitner <mail@joachim-breitner.de>
Hi,

this might be a copy’n’paste problem, but did you really write "fx"
instead of "f x"? Then "fx" becomes a variable, independent of your
function f and the parameters x and y, and the lemma would be unprovable
(e.g. with fx = 0 and fy = 1).

Greetings,
Joachim
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 07:56):

From: Steve Wong <s.wong.731@gmail.com>
Hi

I'm struggling to prove the following lemma:

lemma "EX k:S. P k == EX k. k : S --> P k"

If my understand is right, the lemma should be correct. However, I can't
find a proof using sledgehammer.

Any help will be appreciated. Thanks.

Steve

view this post on Zulip Email Gateway (Aug 19 2022 at 07:56):

From: Elsa L Gunter <egunter@illinois.edu>
This is not true. "EX k : S . P K" is equivalent to "EX k. ((k : S) &
(P k))" , which is stronger than "EX k. k : S --> P k". If S is empty,
"EX k. k : S --> P k" is true, but "EX k : S . P K" is false.
---Elsa

view this post on Zulip Email Gateway (Aug 19 2022 at 07:57):

From: Tjark Weber <webertj@in.tum.de>
On Thu, 2012-07-26 at 20:10 +0100, Steve Wong wrote:

I'm struggling to prove the following lemma:

lemma "EX k:S. P k == EX k. k : S --> P k"

If my understand is right, the lemma should be correct.

If you try nitpick, it will quickly show you a counterexample.

However, I can't find a proof using sledgehammer.

A correct version of the lemma is

lemma "EX k:S. P k == EX k. k : S ∧ P k"
by (rule eq_reflection) metis

eq_reflection (in HOL.thy) states that object equality (=) implies
meta-equality (==). You might want to use = in your lemma in the first
place; then sledgehammer will succeed.

Best regards,
Tjark

Last updated: Apr 20 2024 at 08:16 UTC