Re: [Hol-info] Viewing HOL proofs
One method is editor integration, which makes the process of viewing the
proof less painful than manual copy-paste.
In HOL4 there is integration for both Vim (
https://github.com/HOL-Theorem-Prover/HOL/tree/master/tools/vim) and Emacs,
which might be a suitable starting point. (These essentially just automate
the copy-paste process.)
For HOL Light, I have seen a Vim-integration by Freek Wiedijk which is
perhaps even better for interactive proof-viewing, since it also keeps
track of where you are up to in the editor buffer, and shows all subgoals
of the proof in the viewing terminal.
What you really want is something like Proviola (
http://mws.cs.ru.nl/proviola/). Something like that could be implemented
for HOL Light, with a bit of work.
I made something 4 years ago for annotating proofs. I'll copy an email I
sent to Michael Norrish about it (probably should have gone to this list!),
in case it's helpful. The code linked from the email is still there.
I've decided that HTML is too difficult at the moment.
I also looked at MathML - seems like it would be worthwhile writing a
function to turn a HOL term into a Content MathML ... thing (i.e. a
math element), and then use some stylesheet magic to turn the
Content MathML into Presentation MathML that can be viewed in
(basically not) any browser. I tried doing this for a few hours but
got too confused about what MathML actually is and how to write it
properly... do you know if there are any XML tools for SML?
But the real purpose of this email is to tell you what I did succeed with!
1. Some tactics for annotating a proof, and
2. Some technology for turning an annotated proof into LaTeX.
Code is here https://github.com/xrchz/CERN-LHC-BLMTC-SRS/tree/explanation
In particular, see annotate.{sig,sml}, the proof of
output_input_at_update_times in simplifiedScript.sml, and proof.tex.
For 1, the basic idea is a tactic that acts like ALL_TAC but takes a
string description of what's going on and side-effects some reference
with the description and the current proof state.
So while you're stepping through your proof you can insert ... THEN
anno_tac Now we apply some theorem and it simplifies as follows.
THEN ... at significant points in the proof to save the state for
later viewing.
Actually it's a bit more ugly than that, and I would appreciate any
pointers on how to make it nicer.
The overall design might (i.e. side effects) might also be considered
ugly, in which case don't bother :) - but any better ideas?
For 2, I use EmitTeX to do most of the work.
Perhaps the most interesting things here are my pretty-printings rules
for dealing with SIGMA (\m. f m) (count n) and n ** m, which get them
to print nicely in LaTeX.
I had to use a custom printer for the sums.
There's a lot of hackery here too, in particular with getting the
pretty-printer to think that the superscripts and subscripts for SIGMA
are of 0 width, so it doesn't think the lines are much longer than
they actually are.
Is there a better way to do that?
LaTeX dies when there are linebreaks in the source inside a \sp or \sb
inside an alltt, so it's really annoying if the pretty-printer puts
them in.
On Fri, Mar 13, 2015 at 12:56 AM, Petros Papapanagiotou p...@ed.ac.uk
wrote:
Hello,
You might find Mark Adams's Tactician helpful:
http://www.proof-technologies.com/tactician/index.html
It can break down packaged proofs to g() and e() statements (among
other things).
I am not aware of any other alternatives.
Also, unless I misunderstood, you can use b() to undo a proof step in an
interactive proof.
Hope this helps.
Regards,
Petros
On 13/03/2015 00:07, Mario Carneiro wrote:
Hello all,
What is the usual method for viewing a proof stored in HOL Light, if
you wanted to read it like a regular math textbook (assuming you can get
over syntax difficulties)? (Of course it is not really feasible to look
at the code in isolation, because you can't see the formulas.) The
method I have been using so far is to copy the tactics one at a time
into a HOL session using g() and e(), but it's very tedious and
time-consuming, and it is also difficult to undo if you make a copying
mistake during the process. (I should note that I am still a relative
newbie to using HOL Light and this is essentially the only thing I have
tried to do with it - I have yet to write an actual proof of my own in
HOL Light.)
I feel like this is a common enough goal that there should be some
program to do what I am doing and log the output. Better yet, if there
was a website or downloadable collection of these proofs processed into
a form that did not require interactivity in the OCaml session, this
would make it much easier for mathematicians who do not necessarily want
to write proofs but want to examine the many existing HOL Light proofs
in order to understand them (like me). Does such a thing exist?
Mario Carneiro
Re: [Hol-info] Viewing HOL proofs
Ramana: For HOL Light, I have seen a Vim-integration by Freek Wiedijk which is perhaps even better for interactive proof-viewing, since it also keeps track of where you are up to in the editor buffer, and shows all subgoals of the proof in the viewing terminal. FWIW, this thing I developed for my own use, and I have hardly used it myself yet either. It also is a big hack. OTOH, I kind of like it, and anyone who wants to try it can have it, just mail me. What it is, it is a thing for HOL Light that clones the user experience of the Proof General/CoqIDE/etc way of working with proofs. You can step through HOL Light proofs as long as you use John's prove(`...`, ... THEN ... THENL ...) style (and I guess you can hack it to work for different styles too). So the proof will have been processed up to a certain point, and the goal at that point is shown in a different window. As it is low-tech vi, there's no highlighting, instead the current location in the proof is marked with a |# sign. But one doesn't need to copy-paste from one window to another, one just edits in the final file, and it gets processed. The thing can step through multiple goals in parallel (in Coq words it can stop at semicolons too), when a tactic produces multiple goals but one doesn't do a THENL then. This is something I first saw in Matita, and that I liked, so I imitated that. It means it behaves different from the normal interactive way of using HOL Light, as in that case you always only work on one goal at the time. The interface also can show the goals you're not working on right now (although you can turn that off too, if you don't want to be bothered). Freek -- Dive into the World of Parallel Programming The Go Parallel Website, sponsored by Intel and developed in partnership with Slashdot Media, is your hub for all things parallel software development, from weekly thought leadership blogs to news, videos, case studies, tutorials and more. Take a look and join the conversation now. http://goparallel.sourceforge.net/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Viewing HOL proofs
Hello all, What is the usual method for viewing a proof stored in HOL Light, if you wanted to read it like a regular math textbook (assuming you can get over syntax difficulties)? (Of course it is not really feasible to look at the code in isolation, because you can't see the formulas.) The method I have been using so far is to copy the tactics one at a time into a HOL session using g() and e(), but it's very tedious and time-consuming, and it is also difficult to undo if you make a copying mistake during the process. (I should note that I am still a relative newbie to using HOL Light and this is essentially the only thing I have tried to do with it - I have yet to write an actual proof of my own in HOL Light.) I feel like this is a common enough goal that there should be some program to do what I am doing and log the output. Better yet, if there was a website or downloadable collection of these proofs processed into a form that did not require interactivity in the OCaml session, this would make it much easier for mathematicians who do not necessarily want to write proofs but want to examine the many existing HOL Light proofs in order to understand them (like me). Does such a thing exist? Mario Carneiro -- Dive into the World of Parallel Programming The Go Parallel Website, sponsored by Intel and developed in partnership with Slashdot Media, is your hub for all things parallel software development, from weekly thought leadership blogs to news, videos, case studies, tutorials and more. Take a look and join the conversation now. http://goparallel.sourceforge.net/___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Viewing HOL proofs
Hello, You might find Mark Adams's Tactician helpful: http://www.proof-technologies.com/tactician/index.html It can break down packaged proofs to g() and e() statements (among other things). I am not aware of any other alternatives. Also, unless I misunderstood, you can use b() to undo a proof step in an interactive proof. Hope this helps. Regards, Petros On 13/03/2015 00:07, Mario Carneiro wrote: Hello all, What is the usual method for viewing a proof stored in HOL Light, if you wanted to read it like a regular math textbook (assuming you can get over syntax difficulties)? (Of course it is not really feasible to look at the code in isolation, because you can't see the formulas.) The method I have been using so far is to copy the tactics one at a time into a HOL session using g() and e(), but it's very tedious and time-consuming, and it is also difficult to undo if you make a copying mistake during the process. (I should note that I am still a relative newbie to using HOL Light and this is essentially the only thing I have tried to do with it - I have yet to write an actual proof of my own in HOL Light.) I feel like this is a common enough goal that there should be some program to do what I am doing and log the output. Better yet, if there was a website or downloadable collection of these proofs processed into a form that did not require interactivity in the OCaml session, this would make it much easier for mathematicians who do not necessarily want to write proofs but want to examine the many existing HOL Light proofs in order to understand them (like me). Does such a thing exist? Mario Carneiro -- Dive into the World of Parallel Programming The Go Parallel Website, sponsored by Intel and developed in partnership with Slashdot Media, is your hub for all things parallel software development, from weekly thought leadership blogs to news, videos, case studies, tutorials and more. Take a look and join the conversation now. http://goparallel.sourceforge.net/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Petros Papapanagiotou, Ph.D. CISA, School of Informatics The University of Edinburgh Email: p...@ed.ac.uk --- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. -- Dive into the World of Parallel Programming The Go Parallel Website, sponsored by Intel and developed in partnership with Slashdot Media, is your hub for all things parallel software development, from weekly thought leadership blogs to news, videos, case studies, tutorials and more. Take a look and join the conversation now. http://goparallel.sourceforge.net/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
