The Coq mailing list

[Cedric Auger <Cedric.Auger AT lri.fr>]

Adam Chlipala a écrit :
> tumenjargal tsagaan wrote:
> > I wanted to rewrite coq-code in a sequence form.
> > Is there any automated tool for this purpose?
> >
> > even better is it if possible in a tex format.
>
> Since there was another very similar question recently, it seems like 
> it might be worth making the following point: It's far from clear to 
> me that the full generality of Coq proof terms can be represented 
> nicely in natural deduction form, or in any other form that most 
> people are going to want to read.  Tactics aren't generally generating 
> proof terms with an eye toward readability, and many subtle aspects of 
> the underlying logic don't match up well with informal mathematical 
> practice.
Maybe, but I think that for small proofs (such as tutorial/lectures 
examples), getting sequents from coq script is readable, what ever the 
tactics you used were (as long as they don't contain complex lambda 
terms, e.g. with pattern-matching), see below.
Another funny tool (but less usefull) would be to get non trivial (i.e. 
not using exact/refine tactics) coq script from a lambda term.
> All this is to say that it's not obvious how such a tool would work; 
> it's not just a matter of no one having bothered to implement a clear 
> specification yet.  You would almost certainly need to target a 
> particular domain of proofs to get good results.
>
> --------------------------------------------------------
> 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
That is not really a tool, but ProofWeb 
(http://prover.cs.ru.nl/index.html) has this kind of interesting feature.
But it is not really up to date: it is the trunk version ...
... of 2006.

Maybe is it possible to upgrade this tool to the current version.

As I am too new to coq, I don't know if this feature was once in the coq 
distribution and removed for problems with new features...

with pred_001.v (http://prover.cs.ru.nl/logged.html), it gives 
(Display->...):

    ─── apply[H]     
    P a              
───────────── intro[H]
∀x, P x → P a         


or

─────────────── apply[H]
H:∀x, P x ⊢ P a         
─────────────── intro[H]
⊢ ∀x, P x → P a         


or


1               H:      ∀x, P x   assumption
2                       P a       apply[H]
3                       ∀x, P x → P a     intro[H] 1-2



--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay