Dear HOL4 users, There have been various minor improvements made to HOL4 over the last few years about which some of you may not be aware. Of course, the release notes are available [*]. But I thought I'd collect some of my own tips, some of which didn't make it into release notes, and some of which don't apply to any release but to the latest sources. These might eventually make it into an updated tutorial or maybe a wiki page or something. I welcome comments, other tips, and corrections! [*] http://hol.sourceforge.net/kananaskis-7.release.html (decrement the 7 for earlier ones)
==Github== The HOL4 sources now live here: https://github.com/mn200/HOL. It is a longstanding issue [*] to update the homepage (hol.sf.net) to make links to code point to Github. [*] https://github.com/mn200/HOL/issues/45 Github includes an issue tracker. Submit bugs and feature requests. It also includes a Wiki that we currently don't use, but could. Github also makes it dead simple to fork the HOL4 repository and make changes to it. You can then submit those changes back to the canonical repository by making a ``pull request''. ==lcsymtacs== The lcsymtacs library contains lower-case aliases for many common HOL4 tactics, as well as abbreviations for commonly used instances of general tactics. Simply `open lcysmtacs` in your script file to use it. The contents can be seen by typing `help "lcsymtacs"` at your HOL prompt, or you can look at the library definition directly (https://github.com/mn200/HOL/blob/master/src/boss/lcsymtacs.sml). Especially common tactics include `rw` and `fs`, which abbreviate `SRW_TAC[]` and `FULL_SIMP_TAC(srw_ss())` respectively. ==match_rename== There are tactics for renaming variables in your goal by writing a pattern that matches the goal using the desired names. It is good practice to rename variables before using them (e.g. passing them to qexists_tac, or qspec_then, or stating subgoals involving them) to avoid dependence on the exact spelling of generated names. Type `help "match_rename_tac"` for more information. Also, you can use matching before metis/decide/prove to guarantee the call is appropriate; this enables use of potentially-looping tactics within, say, a TRY or ORELSE. ==qx_gen_tac== You can specify exact names when your goal is a forall by using qx_gen_tac. ==PairCases_on== PairCases_on splits all pairs in a variable recursively, and generates predictable (numbered) names for the sub-pieces. Thus, you can use it to split apart, say, triples quickly and won't have to do qmatch_rename_assum_tac afterwards to get back good names. (If you've ever had to deal with variables like q, r, r', r'', r''', you know what I mean!) Type `help "PairCases_on"` for more information. ==conj_asm1/2_tac== These tactics allow you to work on one branch of a conjunction and then assume it when working on the other branch. Type `help "conj_asm1_tac"` for more information. ==save the proof state== proofManagerLib.save allows you to save the current prove state, with the possibility of jumping back to that point later using proofManagerLib.restore. This is useful when you're working on a subgoal in a very large proof, and want your "restart" operation to be back to the top of that subgoal rather than the initial goal (because then you'd have to replay the whole proof to get to that point again). Type `help "save"` for more information. (These functions are mapped to the keys hv and hB in the HOL Vim mode (where h is the Vim mode local leader key.)) ==THEN1== Use >- (THEN1) instead of >| (THENL). This enables you to zip down part of a proof more easily in the Emacs and Vim interactive modes. ==exporting rewrites== Export everything that looks like a rewrite as a rewrite to improve automation in subsequent proof efforts. The only things to avoid here are looping rewrites, huge terms, and too many subgoals (e.g. from conjunctions). ==use and improve the library== Use store_thm, not prove: store everything that's vaguely abstract/reusable, because then you're more likely to notice good abstractions and to reuse work rather than duplicating it. Move reusable stuff solely about constants in the library into the HOL sources eventually, so others can benefit! (Make a pull request on Github, or write to the developers (or this list).) Reuse constants in the standard library: don't reprove the same lemmas over and over. Use DB.match and DB.find to find relevant lemmas. The library might already have more than you think. (E.g. there is a theory about association lists.) I don't know a good way to search for theories, but you can see its contents by looking at the sources. I think there's a theory graph available somewhere too. That's all I've got for now. Cheers, Ramana ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
