The Coq mailing list

[CoqUser CoqUser <coquser AT yahoo.com>]

Was anything similar ever a feature in Coq?

---

From: CoqUser CoqUser <coquser AT yahoo.com>
To: CHA Reeseo <reeseo AT formal.korea.ac.kr>; coq-club AT pauillac.inria.fr
Sent: Monday, July 20, 2009 2:10:14 PM
Subject: Re: [Coq-Club] Generating Proof Trees in CoQ

The output from BuffProofs is similar to what I'm looking for except I was hoping that there was already a tool that did this in Coq...maybe there isn't?

---

From: CHA Reeseo <reeseo AT formal.korea.ac.kr>
To: coq-club <coq-club AT pauillac.inria.fr>
Sent: Monday, July 20, 2009 2:01:43 PM
Subject: Re: [Coq-Club] Generating Proof Trees in CoQ

2009/7/20 CoqUser CoqUser <coquser AT yahoo.com>:
> I need standard proofs trees as on page 123 of the Coq 8.2 Reference Manual
> preferably in latex form not dependency graphs.

On page 123 of Reference Manual[1], I found a bunch of inference (typing)
rules.  For type-setting trees made up of these rules (in LaTeX), I've
usually hand-coded everything using BuffProofs[2] package.

According to the man page[3], coq-tex doesn't seem to be an appropriate
tool for proof TREEs.  It rather seems to be a tool to interact with
coqtop for some snippet of Coq code embedded in LaTeX source.

If you just want to get a hierarchical structure of your proof, the
command "Show Tree" will help[4].

[1] http://coq.inria.fr/distrib/V8.2pl1/files/Reference-Manual.pdf
[2] http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/
[3] http://www.penguin-soft.com/penguin/man/1/coq-tex.html
[4] http://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#toc46

--
CHA Reeseo
http://www.reeseo.net/

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club