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
