search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

Basic tactical support #121

Open JimmyZJX opened 5 years ago

JimmyZJX commented 5 years ago

Abella offers a great HOAS system for PL proofs. However, projects developed in Abella seems to have much more SLOC compared with (more or less) equivalent proof written in Coq.

Sometimes a simple proof looks stupid when most of the induction cases are not interesting, which can be solved by case H2. search. or simply search. If I could write

induction on 1. intros. case H1; try case H2; search.

and Abella automatically filtered the trivial cases, I believe it is a good step towards productivity.

To sum up, I am expecting these basic tactical features: 1 semi-colon; 2 try; 3 "solve" or just a combined "try solve".

If the developers don't have much time, I am also curious about the difficulty and try to help.

chaudhuri commented 4 years ago

I've wanted the semicolon tactical for a long time, but it is a huge pain to implement based on how Abella does subgoals currently (i.e., with a flat subgoal list). Definitely worth revisiting.

(Sorry for the long delay. I'm just getting back to Abella after other dealing with lots of other duties.)