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
> >
> >
> >
> ------------------------------------------------------------------------------
> > 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
>
------------------------------------------------------------------------------
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
