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.) Alexandre Pilkiewicz implemented an even more powerful cases plugin. (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. 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. 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. Tactic Notation "remember" constr(c) " as" ident(x) := remembertac x c.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. (set (x:=a) in * assert (H: x=a) by reflexivity clearbody x). Ltac remembertac x a := let x := fresh x in let H := fresh "Heq" x in Tactic Notation "rewrite_all" "<-" constr(eq) := repeat rewrite <- eq in *. Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *. Ltac f_equal := let cg := try congruence in let r := try reflexivity in match goal with Ltac case_eq x := generalize ( refl_equal x) pattern x at -1 case x. Ltac absurd_hyp h := let T := type of h inĪbsurd T. Tactic Notation "revert" ne_hyp_list(l) := generalize l clear l.
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |