On Mon, 29 Oct 2012, Alexey Solovyev wrote: > I would like to present a new tool for formal verification of nonlinear > inequalities in HOL Light. The tool can be downloaded at: > http://code.google.com/p/flyspeck/downloads/list
It is always interesting for me to see projects that try to redefine the old ways of doing interactive proof -- I did this myself with Isabelle/Isar in 1998/1999. I've looked a bit through the manual http://flyspeck.googlecode.com/files/HOL-SSReflect%20v1.1.pdf and here is some random feedback on it: * Concerning specifications it looks a lot like an imitation of Coq "vernacular". How do hardcore HOL users like the style? BTW, the use of capital keywords like Definition or Lemma was recently considered a historical mistake on coq-club, on the "Coq and RSI" thread, about pain inflicted on users by Coq conventions and Emacs keymaps coming together. * How much SSReflect is there in SSReflect/HOL Light actually? The "small-scale reflection" aspect of the Coq version appears to be mainly an approach to make Coq propositions work more like HOL propositions, but you have that already. In your section about views it sounds like there is little or nothing of it in your version of SSReflect. So is it just a marketing aspect to retain the name? (Even for Coq it might be just a branding issue to keep this obscure name that everybody knows already.) * Page 15: move: {1}x a transforms the goal into !x1 a. a + x1 = x + 3, where x1 is an automatically generated name. How does that compare to SSReflect by Gonthier? It is one of the very few points where SSReflect and Isar agree, to have generated names never intrude the proof text implicitly. Does that actually happen above for HOL Light, or is it just the text confusing me? * wlog: Can you give some examples? Despite some talks and papers about "wlog" reasoning by John Harrison, I've never quite understood how this would work in Isabelle/Isar. Maybe I can learn something new. * 'by' vs. 'done': Is this copied from Isar, or did Gonthier copy it from Isar for SSReflect? BTW, in Isabelle/Isar 'by' does a bit more: it solves the remaining situation "by assumption", and then insists in being finished. The proof structure is already known, so one can afford implicit "trivial steps" at the end of a sub-proof. * 'have' as subgoal: I reckon it is simular to subgoal_tac in Isabelle or its counterpart in HOL. In Isar, I made this quite different: having a first-class notion of proof context, 'have' is just a fresh local goal within it, and its result a theorem with certain assumptions, which is then re-used in the enclosing proof. This gives you more structure and scalability than just goal-modifications in the old style. Makarius ------------------------------------------------------------------------------ Monitor your physical, virtual and cloud infrastructure from a single web console. Get in-depth insight into apps, servers, databases, vmware, SAP, cloud infrastructure, etc. Download 30-day Free Trial. Pricing starts from $795 for 25 servers or applications! http://p.sf.net/sfu/zoho_dev2dev_nov _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
