Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] simple proof question

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

From: Ian Lynagh <igloo@earth.li>
Hi all,

I'm trying to write a simple proof in Isabelle, but I'm a little lost. I
wonder if anyone can help me please? I've attached the script I have so
far.

At the point at which I am stuck, I have
using this:
(EBool bool_, t) : STyping
and I want to show that "t = TBool", which must be true as
STypingBool: "forall (b :: bool) ==> STyping (EBool b, TBool)"
is the only constructor matching that pattern. My best guess was
proof (cases this)
but that says
*** empty result sequence -- proof command failed
*** At command "proof".
Can anyone give me a pointer in the right direction please?

I'm also not sure why I can't do
apply simpl
immediately after
case EBool
? My goal here was to try to get "principalType (EBool bool)" to reduce.

Finally, I'd also be very interested to know if the general structure
looks sensible, or if there would be a more sensible way to write this
sort of proof.

Thanks
Ian
simple.thy

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

From: Tobias Nipkow <nipkow@in.tum.de>
Ian Lynagh schrieb:

Hi all,

I'm trying to write a simple proof in Isabelle, but I'm a little lost. I
wonder if anyone can help me please? I've attached the script I have so
far.

At the point at which I am stuck, I have
using this:
(EBool bool_, t) : STyping
and I want to show that "t = TBool", which must be true as
STypingBool: "forall (b :: bool) ==> STyping (EBool b, TBool)"

For a start, your "forall (b :: bool) ==>" is a bit weird. Isabelle
accepted it but had to interpret "forall" as a free function variable to
make sense of it. Probably not what you meant. Note that "forall" is not
Isabelle speak, and that outermost universal quantifiers can and should
be dropped. Just write "STyping (EBool b, TBool)".

Now the proof.

is the only constructor matching that pattern. My best guess was
proof (cases this)

You cannot do a case distintinction on a theorem ("this") but only on a
term. This suggests

proof (cases t)

Although this step works, it does not get you anywhere. Before you start
the whole proof you should deduce some elimination rules that allow you
to move from "(EBool b, t) : STyping" to "t = TBool". This can be done
automatically:

inductive_cases STypingE[elim!]:
"STyping (EBool b, t)"

The resulting lemma STypingE is what you need. The magic "[elim!]" tells
auto and blast and friends to apply this rule eagerly. Now your proof
should just be

from this have "t = TBool" by auto

Important: you will have to extend STypingE with other cases, at least

inductive_cases STypingE[elim!]:
"STyping (EBool b, t)"
"STyping (EInt n, t)"

Tobias

but that says
*** empty result sequence -- proof command failed
*** At command "proof".
Can anyone give me a pointer in the right direction please?

I'm also not sure why I can't do
apply simpl
immediately after
case EBool
? My goal here was to try to get "principalType (EBool bool)" to reduce.

Finally, I'd also be very interested to know if the general structure
looks sensible, or if there would be a more sensible way to write this
sort of proof.

Thanks
Ian

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

From: Tobias Nipkow <nipkow@in.tum.de>
My mistake: I didn't run it. Your mistake: you had phrased the theorem
as "... : STyping" but the rules as "STyping ...". Don't mix the two
notations, it complicates your life. Either set or predicate. And if
predicate, then it is usually better to curry it.

Concerning your overall proof strategy, I recommend rule induction on
STyping:

proof(induct rule: STyping.induct)

That takes care of all the case distinctins you were going to do by hand.

Tobias

Ian Lynagh schrieb:

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

From: Ian Lynagh <igloo@earth.li>
Hi Tobias,

On Fri, Aug 13, 2010 at 09:42:23AM +0200, Tobias Nipkow wrote:

outermost universal quantifiers can and should
be dropped. Just write "STyping (EBool b, TBool)".

Aha, thanks!

inductive_cases STypingE[elim!]:
"STyping (EBool b, t)"

The resulting lemma STypingE is what you need. The magic "[elim!]" tells
auto and blast and friends to apply this rule eagerly. Now your proof
should just be

from this have "t = TBool" by auto

Do you mean like this?:

lemma "((e, t) \<in> STyping) ==> (principalType e = Some t)"
proof (induct e)
case EBool
from this have "t = TBool" by auto

If so, the "by auto" fails with:

*** Failed to finish proof
*** At command "by".

Thanks
Ian

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

From: Ian Lynagh <igloo@earth.li>
On Fri, Aug 13, 2010 at 01:37:12PM +0200, Tobias Nipkow wrote:

My mistake: I didn't run it. Your mistake: you had phrased the theorem
as "... : STyping" but the rules as "STyping ...". Don't mix the two
notations, it complicates your life. Either set or predicate.

Aha, thanks!

Concerning your overall proof strategy, I recommend rule induction on
STyping:

proof(induct rule: STyping.induct)

That takes care of all the case distinctins you were going to do by hand.

Hmm, that gives me:

  1. !!b. principalType e = Some t

which doesn't look provable to me. And there's also:

  1. !!guard exprTrue ta exprFalse.
    [| STyping (guard, TBool); principalType e = Some t;
    STyping (exprTrue, ta); principalType e = Some t;
    STyping (exprFalse, ta); principalType e = Some t |]
    ==> principalType e = Some t

but the t's shouldn't all be the same.

Thanks
Ian

Last updated: Apr 25 2024 at 04:18 UTC