Open JimmyZJX opened 5 years ago
This is unlikely to ever be implemented, since we do not treat *
and @
as connectives, only as annotations with an implied meaning in the scope of an inductive proof. Moreover, these annotations are only internal to Abella: users can't even write them explicitly.
We have discussed ideas for promoting something like these annotations to connectives in a variant of G, but it's not an easy thing to get right. Needless to say, any implementation must be preceeded by a careful theoretical justification first.
I just wanted to add that I've come across many instances where it would be nice to be able to say that applying a theorem doesn't change the height of a derivation. For example, in the notation above,
Theorem convert : forall X Y, {p X Y}* -> {p Y X}*.
This would allow one to induct on a p-judgment and swap the arguments without losing the ability to apply the IH. In the standard translation from the specification language to G, there is an added natural-number argument representing the height of the derivation, and in the context of that translation, theorems like the above are easy to state and prove. It would be nice if that implicit argument could somehow be made accessible for this use. Maybe something like
Theorem convert : forall X Y N, {p X Y}@N -> {p Y X}@N.
using a built-in nat
type.
Right now you have to reify the "size" of p somewhere and use that to drive your induction instead:
Theorem convert : forall X Y N, nat N -> p N X Y -> p N Y X.
Abella's inductive restriction annotations are not natural numbers but rather ordinals of a certain form depending on the precise form of induction being performed. You can't take the annotations out of the context they're in. Imagine, for instance, you're doing a nested induction -- then you couldn't use your form of convert because the annotation would be *, not . Figuring this out formally is one of the things I am working on these days research wise, but things are not as easy as they seemed when I started.
I like the inductive restriction symbols @(equal) and *(smaller) for their simplicity. I wonder if we could make use of these symbols to prove the size of objects. For example,
With this feature, proof by induction could be more flexible (just like applying unfold multiple times). It seems that this is somehow related to nested induction. Please correct me if I am wrong.