The old Google Groups will be going away soon, but your browser is incompatible with the new version.
lifting specifications?
 There are currently too many topics in this group that display first. To make this topic appear first, remove this option from another topic. There was an error processing your request. Please try again. Standard view   View as tree
 3 messages

From:
To:
Cc:
Followup To:
Subject:
 Validation: For verification purposes please type the characters you see in the picture below or the numbers you hear by clicking the accessibility icon.

More options Mar 7 2008, 5:16 pm
From: Randy Pollack <rpoll...@inf.ed.ac.uk>
Date: Fri, 7 Mar 2008 22:16:46 +0000
Local: Fri, Mar 7 2008 5:16 pm
Subject: lifting specifications?
Hi Andrew.

The .mod file:

trm (app M N) :- trm M, trm N.
trm (abs R) :- pi x\ trm x => trm (R x).

And we have

Define ctxs nil nil nil.
Define nabla x, ctxs (trm x :: L) (pr1 x x :: K)
(cd1 x x :: notabs x :: J)
:= ctxs L K J.

Can I lift "trm" to contexts, like

Theorem trm_app: forall L K J M N,
ctxs L K J -> {L |- trm M} -> {L |- trm N} -> {L |- trm (app M N)}.

I don't see how to prove this.  In your example poplmark-1a.thm I see
you define something similar:

Define cty L top.
Define cty L X := exists U, member (bound X U) L.
Define cty L (arrow T1 T2) := cty L T1 /\ cty L T2.
Define cty L (all T1 T2) :=
cty L T1 /\ nabla x, cty (bound x T1 :: L) (T2 x).

What is going on here?

Best,
Randy

To post a message you must first join this group.
You do not have the permission required to post.
More options Mar 7 2008, 5:55 pm
From: "Andrew Gacek" <andrew.ga...@gmail.com>
Date: Fri, 7 Mar 2008 16:55:20 -0600
Local: Fri, Mar 7 2008 5:55 pm
Subject: Re: [Abella] lifting specifications?
Hi Randy,

I don't have Abella handy, but I think the following should work.

Theorem trm_app: forall L M N,
{L |- trm M} -> {L |- trm N} -> {L |- trm (app M N)}.
intros. search.

>  I don't see how to prove this.  In your example poplmark-1a.thm I see
>  you define something similar:

>   Define cty L top.
>   Define cty L X := exists U, member (bound X U) L.
>   Define cty L (arrow T1 T2) := cty L T1 /\ cty L T2.
>   Define cty L (all T1 T2) :=
>     cty L T1 /\ nabla x, cty (bound x T1 :: L) (T2 x).

>  What is going on here?

Here I'm defining a predicate which recognizes closed types. I could
have defined this in the specification logic with

cty top.
cty (arrow T1 T2) :- cty T1, cty T2.
cty (all T1 T2) :- cty T1, pi x\ cty x => cty (T2 x).

But the definition I used in poplmark-1a is a little more convenient
since it generates contexts like (bound x T :: ...) rather than (cty x
:: ...). And this former style of contexts matches that of the sub
judgment. In summary, I could define cty in the specification logic,
but reasoning would take a little more work.

-Andrew

To post a message you must first join this group.
You do not have the permission required to post.
More options Mar 7 2008, 6:04 pm
From: Randy Pollack <rpoll...@inf.ed.ac.uk>
Date: Fri, 7 Mar 2008 23:04:28 +0000
Local: Fri, Mar 7 2008 6:04 pm
Subject: Re: [Abella] Re: lifting specifications?
Andrew Gacek writes:

> [...]
> >  Can I lift "trm" to contexts, like
> >
> >   Theorem trm_app: forall L K J M N,
> >    ctxs L K J -> {L |- trm M} -> {L |- trm N} -> {L |- trm (app M N)}.
>
> I don't have Abella handy, but I think the following should work.
>
> Theorem trm_app: forall L M N,
>   {L |- trm M} -> {L |- trm N} -> {L |- trm (app M N)}.
> intros. search.

It does work.

> >  I don't see how to prove this.  In your example poplmark-1a.thm I see
> >  you define something similar:
> >
> >   Define cty L top.
> >   Define cty L X := exists U, member (bound X U) L.
> >   Define cty L (arrow T1 T2) := cty L T1 /\ cty L T2.
> >   Define cty L (all T1 T2) :=
> >     cty L T1 /\ nabla x, cty (bound x T1 :: L) (T2 x).
> >
> >  What is going on here?
>
> Here I'm defining a predicate which recognizes closed types. I could
> have defined this in the specification logic with
>
> cty top.
> cty (arrow T1 T2) :- cty T1, cty T2.
> cty (all T1 T2) :- cty T1, pi x\ cty x => cty (T2 x).
>
> But the definition I used in poplmark-1a is a little more convenient
> since it generates contexts like (bound x T :: ...) rather than (cty x
> :: ...). And this former style of contexts matches that of the sub
> judgment. In summary, I could define cty in the specification logic,
> but reasoning would take a little more work.

Thanks,
Randy

To post a message you must first join this group.
You do not have the permission required to post.
 End of messages
 « Back to Discussions « Newer topic Older topic »