lifting specifications?

[Randy Pollack]

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

[Andrew Gacek]

Hi Randy,

> 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 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

[Randy Pollack]

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