Feature request: explicitly specify * and @ by user

[JimmyZJX]

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,

Kind nat type.
Type z nat.
Type s nat -> nat.

Define is_nat : nat -> prop by
	is_nat z;
	is_nat (s N) := is_nat N.

Define add : nat -> nat -> nat -> prop by
	add z N N; % maybe better with ":= is_nat N"?
	add (s M) N (s K) := add M N K.

% Feature expected
Theorem add_smaller_or_eq : forall m n k, add m n k -> is_nat k * -> is_nat n *.
Theorem add_smaller : forall m n k, add m n k -> is_nat (s k) @ -> is_nat n *.

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.

[chaudhuri]

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.

[lambdacalculator]

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.

[chaudhuri]

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.