Feature: tactic `applys` as a handy version of `apply`

[JimmyZJX]

Grammar:

applys <HYP NAME> [to] <HYP NAMES> [with X1 = T1, ..., Xn = Tn].
applys <HYP NAME> [with X1 = T1, ..., Xn = Tn].

Why not apply

A script like apply HYP to _ _ _ H1 _ _ H2 _ _. is tedious to write---the user needs to figure out the correct order of the application, which might not be important for its correctness.

With applys, the user may write applys HYP H2 H1. and get the same result (if it is very "easy" to re-order the hypothesis).

(I'm not a user of emacs, so I wrote this minimal plugin for SublimeText to use Abella)

What applys does:

• Iterate over user-specified hypotheses, and try to match them with the assumptions of the lemma in order. The match basically checks top-level constructor and induction restrictions. Each hypothesis is put into its first successful match and take the place.
• Supply no hypothesis like applys HYP. behaves the same as applys HYP to _ _ ... _.
• One may use the underscore _ to skip one match for the next hypothesis. E.g. applys IH to _ H1 will require H1 to have at least 2 matches within assumptions of IH (and put H1 to the second position). The error message "[%s] is not compatible with any subgoal (skip %d/%d)" should be self-explanatory.
• After the steps above, if there are still assumptions that have induction restrictions, try to find proper hypotheses from the current hypothesis list.

Changes to the code:

• Grammar
• Abella.Types: the Apply constructor now contains an applys switch
• Naive "compatibility" check used to match a hypothesis with an assumption
• A single function genCompatibleArgs that hacks the args
• Pass in hyps from the prover to apply_with for fixing induction Preds

User feedback:

Unfortunately only I used applys during the past weeks. I hardly use the original apply for new developments once I had applys. It really boosts my efficiency and let me focus more on the logic. However, I am not a user of the specification logic or coinduction. So I am not sure whether it works together with those features.

[chaudhuri]

This is an interesting idea. Thanks for the implementation. I'll give it a test run to see if it breaks any of our existing examples.

Not particularly fond of the name applys though, but I don't have an alternative as of now.

[lambdacalculator]

I can also see the potential advantages of a tactic like this, but I want to add a few dissenting points. My preference has always been to make proof scripts as explicit as possible. As a consequence, I only use an underscore when the hypothesis I need is not immediately available but provable by search, not as a substitute for searching through the hypothesis list myself and including the correct hypothesis number. Similarly, I always provide a "with" argument to cut when it's available, instead of asking Abella to find it for me. For one thing, this makes it easier for external tools to scrape information from proof scripts (I have a student working on a project now that does this). For another, it makes the loading of files much faster, since Abella doesn't have to spend time doing these searches again every time the proof is reloaded.

If we want the advantages of convenience that this proposed tactic represents, I would suggest instead a kind of information-producing command or "hint mode" that would take an input like the applys statement and produce the fully explicit apply statement in return, which could then be inserted into the proof script. That way, the search is done once and for all, and the proof script ends up being more explicit.

[JimmyZJX]

Thanks for the comments!

It is interesting to know that people have different preferences when developing in Abella.

For my projects (6k~8k lines), Abella compiles relatively fast (~10s) and reloads fast (~3s for a file of ~1k lines). Therefore, development (proving theorems) itself takes much more and I would like to focus on that. (Although I do seldom optimize speed by supplying the search depth argument.) Some lemmas in my projects have a lot of premises (due to the lack of fixpoint function), and a large number of them are not interesting. Supplying all of the arguments in the right order is indeed a tedious and useless job (I need to look up the definition every time and count the number of hypotheses; a very fast search should take care of that).

I also thought about producing a standard apply command for every applys, so that I could use the feature without modifying the base branch. One of the tiny external tools I ever tried is to generate the dependency map for lemmas/theorems, which does not rely on the hypothesis arguments of apply but only the theorem name.

[lambdacalculator]

This is probably not the place to discuss proof engineering, but when I have to deal with lemmas with many variables and many hypotheses involving these variables, I define new types that are in effect tuples of existing types, and then define new predicates on these types to stand for these complicated combinations of hypotheses, the same way you'd bundle together data in records in a programming language and then define functions on these records. At a basic level, constructive proofs are just programs, and so the same abstraction principles that work in programming to make programs more manageable can work with theorems and proofs to make them more manageable. (Again, apologies for going off-topic.)