Suggestion: simultaneous induction

[lambdacalculator]

I'm guessing it would be relatively straightforward to extend the induction tactic to include support for simultaneous induction, as follows:

induction on (i1,...,ik) would introduce an IH where arguments i1, ..., ik are all labeled with and would label all corresponding arguments in the goal with @. After this, everything would work as before: an application of IH would require all arguments labeled with to be instantiated with hypotheses labeled with *. We could also provide a corresponding case H1,...,Hk tactic that would do simultaneous (or iterated) cases.

The effects of this can already be easily achieved currently with no extra overhead -- just pick one of the i1,...,ik to do induction on -- but the advantage of the proposed tactic is threefold:

• symmetry - in a simultaneous induction, it doesn't matter on which of the arguments we do induction, and thus on which others we do inversion, and there is some advantage in not forcing users to make an arbitrary choice
• useful restriction - much like a typing system limits the bad programs we might be tempted to write, the extra annotations (although not technically necessary) would limit the bad proofs we might try to give, reminding us that we still need to do inversion on other judgments before we are ready to apply the IH
• proof documentation - it allows us to announce up front that a particular set of arguments will get smaller simultaneously during induction and furthermore announces our intent to do an inversion on each of other arguments in each case, leading to a more perspicuous proof.

In the case of mutual induction, the tactic could look like

induction on (i1,...,ik) (j1,...,jn) ...

I assume it would also work with nested (lexigraphic) inductions.

[chaudhuri]

This is an interesting idea, but I would need to have a better understanding of the termination ordering. Currently in Abella we use a simple lexicographic ordering generated from * < @. If we allow multisets of these, then we have to be careful about well-foundedness. We don't want to get into a situation of {*, @) < {@, *} < {*, @} < ....

[kyagrd]

I'm not sure about the details but Multiset Ordering (a.k.a. Dershowitz--Manna ordering) seems to be something more general than lexicographic ordering for termination problems.

[lambdacalculator]

When I said that I was guessing that it was straightforward, I was thinking that, from an implementation standpoint, once you attached the inductive-restriction annotations to the appropriate arguments of the IH and goal, everything else after that would be the same: whenever an argument to the IH was labeled with a restriction, the actual argument provided would have to have the same (or lower) restriction, and the restrictions would behave the same under case. It's just that you would be annotating more than one argument at a time.

I guess that if you are implicitly converting these restrictions into some internal well-ordering, then you might want to check to make sure that it interacts well with the ordering that you have. From an order-theoretic perspective, the simultaneous ordering I'm proposing is just the pointwise ordering on the product: (a,b) < (c,d) iff a < c and b < d. It is weaker than either of the two lexigraphic orderings possible on the product, so it doesn't add any new capabilities, but it's just convenient from the point of view of documentation. And, by the way, Twelf supported this ordering, where the lexigraphic ordering was called {o1,...,on} and the simultaneous ordering was called [o1,...,on].

EDIT: I just looked again at the Twelf manual, and my memory of their simultaneous ordering was incorrect: their ordering is essentially the symmetric sum of the individual orders: (a,b) < (c,d) iff (a < c and b <= d) or (a <= c and b < d). So my proposed ordering is even more restrictive than this one. Their ordering would be harder to implement in Abella, I would guess.

[chaudhuri]

Indeed, Twelf's simultaneous order is what I imagined you were asking. I think if you have:

===============
 A -> B -> C

and then declare induction on (1 2), according to you, you would have:

H : A* -> B* -> C
===============
 A@ -> B@ -> C

This would mean that to apply H you would need to reduce both A@ and B@ to *s, not just one. I can imagine a variation of the size restriction that only requires at least one of the multiple *-assumptions to be matched. That is why I asked the well-foundedness question because it has to be done very carefully.

@kyagrd It is very unlikely that the multiset ordering or any generalization is what @lambdacalculator meant. These orderings are, anyhow, probably incomptible with a tactics-style interactive prover. I tried to get them to work in the rpo branch of Abella and eventually gave up.

[chaudhuri]

Can you try out the simulind branch of Abella to see if it fits your needs? It's not a finished implementation, just something to see if we're on the right track.

[lambdacalculator]

Thanks for the quick implementation! It seems to be working (see preserv.zip).

However, I see that you implemented the Twelf-style simultaneous induction. Although this is more general, it somewhat defeats the purpose of my suggestion, since now I have no way to announce that all induction arguments are getting smaller simultaneously. Also, I can't think of a good example where I really use the ability to make different induction arguments smaller in different cases, leaving the others the same, although I'm sure that examples could be constructed. By contrast, the weaker simultaneous induction I had it mind is used all the time (again, see attached).

Also, notice in my example how each case begins with case H1. This really illustrates the usefulness of my additional suggestion of case H1 H2, which also makes the induction truly symmetric, since I don't have to choose an order to do the cases. If I had chosen to do case H1 first and then case H2 in each branch, then I would have gotten nested subgoals (e.g., 3.1, 3.2, 3.3, 3.4), again violating the symmetry of the situation.

Finally, it occurred to me while doing the attached proof that there might be a situation were a simultaneous induction (of either kind) is performed on a proposition with two similar arguments and they get swapped in an application of the IH. I guess this wouldn't cause a problem in terms of the induction measure, but it is something that wouldn't be possible if the induction was only on one argument.

[chaudhuri]

Proof-theoretically, case analysis is an "invertible" rule, so the order in which we do case steps does not matter. We can always do case H1 H2 ... Hn for any case-able hypotheses H1, ..., Hn that are in the context at the same time. I am not sure what benefit is gained in generalizing case in this way.

I think using something like the semi-colon tactical of Coq or THEN from LCF is a better choice if we want to indicate that we do case H1 and then in every ensuing subgoal we immediately do case H2. It's a much more malleable combinator and avoids complicating individual tactics. Abella's tactics already feel a bit bloated in the number of knobs and dials they have.

But, we should get some other opinions. I don't feel strongly about this. Maybe asking on the list is a good thing here.

[lambdacalculator]

The semi-colon/THEN tactical would be an improvement over my suggestion, which is more limited, but then, having done that, we would still be in a position to introduce case H1 H2 ... Hn as a convenient abbreviation for case H1; case H2; ... ; case Hn. However, I would add one more recommendation: that when the subgoals that result from a such a tactic sequence are numbered, they be numbered all on one level, and not nested the way they would be if the tactics were applied sequentially.

Also, when discussing tacticals, I want to make the remark that one thing I like about Abella's tactics is that they are all or nothing: if a tactic fails, the proof has failed. That's why I thought it was a good move to make this change from the changelog (2.0.4):

The search tactic has the same error handling behavior in interactive and non-interactive modes, functioning like a failed tactic in both cases if no subgoals were closed.

Tactics that try to do something to the proof state but do nothing instead of fail mean that proofs in some sense can no longer be read directly from the proof script. I know that improving automation may eventually require abandoning this principle, but it's a trade-off that should not be taken lightly.

[chaudhuri]

I've checked in a version with a simultaneous_decr flag, which if set to all uses your order with all inductive arguments smaller, and if set to any uses the Twelf order. See if it improves matters.

With regard to numbering of subgoals in repeated case statements: since subgoal numbers are only used to display goals, it's mainly a cosmetic change. I'll leave that to a more full-fledged implementation if we ever get to that. Currently I've only lightly tested the apply tactic. I don't know how this change interacts with search, backchain, etc. Even apply with unknowns is problematic, though we have never allowed unknown arguments in * positions.

Tactics that try to do something to the proof state but do nothing instead of fail [...]

This is not really relevant to the ; tactical of Coq, I don't think.

[chaudhuri]

I tried to quickly hammer out the iterated case thing just to get a feel for it. Very lightly tested, but this works now:

Specification "preserv".

Set simultaneous_decr all.

Theorem preserv : forall E T E', {of E T} -> {step E E'} -> {of E' T}.
induction on (1 2). intros. case H2 H1.
  apply IH to H4 H3. search.
  apply IH to H4 H3. search.
  apply IH to H6 H4. search.
  search.
  case H5. search.
  apply IH to H4 H3. search.
  apply IH to H6 H4. search.
  case H4. inst H6 with n1 = E2. cut H7 with H5. search.

Still not really sure if I like it or not.

[lambdacalculator]

Thanks again for the quick implementation. After playing around with it a bit, I'd like to share my conclusions.

• If simultaneous cases are available, then my simultaneous induction order is really a red herring: we can always choose any argument to induct on and then, after intros, do a simultaneous case. That has the clearer effect of announcing the simultaneous nature of the induction, since it forces all hypotheses to be inverted at the same time.
• Having the extra induction annotations around may help marginally with keeping the hypotheses straight, but the advantage is almost insignificant, and there is the potential problem of getting the arguments swapped on calls to the IH.
• The flattening of subgoal numbers turned out to be less helpful than I though it would be. The nested subgoal numbers actually give a better indication of where you are in the proof and also better indicate the grouping of subgoals that arise.

In short, I no longer like the simultaneous order I was proposing and find the simultaneous case you implemented much more useful. The Twelf-style simultaneous order may still be useful in some cases (for example, proving the termination of the merge operation in merge-sort), so it may be worth keeping.

[chaudhuri]

OK, I'll keep the branch around for now. Reopen this if you want to revisit this in the future.