Open JimmyZJX opened 4 years ago
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.
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.
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.
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.)
Grammar:
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 writeapplys HYP H2 H1.
and get the same result (if it is very "easy" to re-order the hypothesis).What
applys
does:match
basically checks top-level constructor and induction restrictions. Each hypothesis is put into its first successful match and take the place.applys HYP.
behaves the same asapplys HYP to _ _ ... _
._
to skip one match for the next hypothesis. E.g.applys IH to _ H1
will requireH1
to have at least 2 matches within assumptions ofIH
(and putH1
to the second position). The error message "[%s] is not compatible with any subgoal (skip %d/%d)" should be self-explanatory.Changes to the code:
applys
switchgenCompatibleArgs
that hacks theargs
hyps
from the prover toapply_with
for fixing inductionPred
sUser feedback:
Unfortunately only I used
applys
during the past weeks. I hardly use the originalapply
for new developments once I hadapplys
. 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.