Open JimmyZJX opened 3 years ago
Thanks. I plan to take a look at this proposal in detail soon.
One quick question: you would be OK with changing your proofs if your proposed syntax isn't accepted, right? I am completely OK with the try
and ;
tactic(al)s, but I'm not yet convinced that applys
is needed (and, as an English speaker, I definitely don't like the word applys
). I definitely wouldn't mind the |
tactical as well.
In the long term I don't want to end up in the same place as Coq, because I think the proposal to have λProlog based tactics programming is overall superior. However, that will only come with Abella 3.x.
By the way, since you are contributing a lot of interesting stuff to Abella, would you be interested in joining the Abella dev team? Currently we could really use the manpower since everyone else is too busy to focus on Abella of late.
@chaudhuri Thanks for the response.
It's perfectly fine for me to accept a different name.
But just to clarify, this name comes from the UseAuto library in Coq, where applys
means apply_star
, or apply*
. I am not good at naming things and just picked that temporarily.
Talking about the tactic itself, it does not introduce any new abilities, but it does help when I am facing a theorem/hypothesis with a long list of parameters. It would take quite some time to figure out the correct order by counting the number of underscores. Additionally, adding a minor condition in the theorem might cause every single use of IH to change.
(This an extreme case I can find in my current project, where the theorem uses size measures and
applys
helps a lot)
Applying theorems is significantly simplified with applys
; usually, the programmer is very familiar with the theorem and knows which conditions are critical, therefore applys
help eliminate unnecessary arguments. In contrast, they would write underscores in those places if using apply
, but the cost is to memorize those locations.
I understand that the long-term goal is to use a different proof language, and I'm also looking forward to that!
I'm happy to join the dev and help taking care of some features in my spare time.
Implement #121.
Summary
Support Coq-like semi-colons,
try
andsolve
tactics.induction on 1. intros. case H1; try case H2; search.
Implementation details
The implementation patches
sequent
by adding apending_commands : command list
.Due to OCaml's restriction on dependencies (a function must be defined before usage), a dirty workaround is used on the function
process_proof_command
, by manually "link" the function when the program starts. It avoids refactoring the code on a large scale (across existing modules). And I'm happy to hear any better ideas (given that I'm not an experienced programmer in OCaml).Experience
I've been using this feature for around 2 months (and also another Ph.D. in the same group for weeks). No problems are found so far. In addition to the
applys
feature, a lot of uninteresting proof scripts can be eliminated, for example,induction on 1. intros. case H1; try applys IH; try search.
or multiple tactics in combination,induction on 1. intros. case H1; try (case H2; case H3; applys IH; search).
or when I'm debugging why a search does not solve a case,unfold. intros. split; try search.
Future directions
[ tactic1 | tactic2 ... ]
might be helpful in some cases.search
may hang for a large amount of time (unprovable case, perhaps exponential time), which may causetry search
to be less useful. But in general, this does not happen that often.I don't mean to push the dev on extending features. But I really hope that these little features may help users who use Abella heavily, being 100% backward-compatible without changing any core logic of Abella.