Coq tactics
(Again, this fails if the first proof step changes to prove too much or too little.) With bullets you would write induction foo. The difference is that when the subgoal is finished, you do not have a closing construction, you must use the same bullet to move to the next subgoal. Bulletsīullets are actually a combination of two features, braces (* would fail if a new subgoal appeared *) List bulletsĪ bullet, for example -, also focuses on the next subgoal. I found bullets very useful for the first step, and during the refinement process. (I have been going to Adam Chlipala’s Formal Reasoning about Programs 2017 class, where Adam ignores bullets because that is his usual style.) Because I am not crushy enough to do this from the start, my proofs tend to start with cases and subgoals, and then I refine them to add more automation for robustness. I learned a lot from Arthur Azevedo de Amorim’s Bullets.v file.įinally, some people don’t use bullets, because they systematically use so much automation that they never see subgoals - each lemma has a one-line proof. There is not much discussion of bullets around see the documentation in the Coq manual. Bullets are available in standard Coq since 8.4 (released in 2012), and can be used with no effort.)
![coq tactics coq tactics](https://static.wixstatic.com/media/ed50b4_60bb39674050423d80577e37708cebc1~mv2.jpg)
![coq tactics coq tactics](https://www.vivementmercredi.bzh/wp-content/uploads/2017/09/COMBAT_DE_COQ_1.jpg)
Alexandre Pilkiewicz implemented an even more powerful cases plugin.
Coq tactics software#
(The S*Case tactics used in (older versions of) Software Foundations can solve this problem if used in a carefully, systematic way, and additionally provides naming. What we need for robustness is a way to indicate our intent to Coq, when we think that a subgoal is finished and that a new subgoal starts, so that Coq can fail loudly at the moment where it notices that this intent does not match reality, instead of at an arbitrary later time. If a proof step now proves more things, it is also very bad! The next proof steps, meant for the first subgoal (for example), would then apply to the beginning of the second subgoal, and you get very confusing errors again. Coq would then start reading the proof of the next subgoal and try to apply it to the unfinished previous goals, generating very confusing errors (you believe you are in the second subgoal, but the context talks about a leaf case of the first goal). If a proof step now proves less things, then what used to be the end of a subgoal may not be anymore. It could be very hard of what was happening when a proof suddenly broke after a change before in the file: But, in my experience, a major problem with this style was maintainability in the face of changes to the definitions or parts of automation. There are many ways to structure this to make the structure more apparent: people would typically have a comment on each subgoal, or make disciplined use of indentation and blank lines.
![coq tactics coq tactics](https://2.bp.blogspot.com/-JEObTGA8YeY/XHFpqjIQb9I/AAAAAAAAEpI/NLPLKhiF6SERadm-4lQjqL_RAgK2YrkUQCLcBGAs/s1600/0B86EA66-998E-4202-9F5D-1F0E7080B145.jpeg)
Most proof steps will operate on the current active subgoal, changing the hypotheses or the goal to prove, but some proof steps will split it into several subgoals (growing the total list of goals), or may terminate the proof of the current subgoal and show you the next active subgoal.īefore bullets, a typical proof script would contain the proofs of each subgoal, one after another.
![coq tactics coq tactics](https://image.slidesharecdn.com/tutorial-110423092501-phpapp01/95/coq-tutorial-78-728.jpg)
While you are doing a proof, Coq shows a list of subgoals that have to be proved before the whole proof is complete. In this post I will give the general rules, and explain my current usage style. Unfortunately, they are not very well-known, due to the fact that some introductory documents have not been updated to use them.īullets are a very general construction and there are several possible ways to use them I have iterated through different styles. They had a big impact on the maintainability of my proofs. I believe that bullets are one of the most impactful features of recent versions of Coq, among those that non-super-expert users can enjoy.