The Coq mailing list

[Francesco Zappa Nardelli <francesco.zappa_nardelli AT inria.fr>]

Dear all

> I meant solutions written in Coq, of course.  Could it be the case
> that other provers are less challenged than Coq by mutual inductive
> definitions and by T / list T inductive definitions?

As a test case for the Ott tool, we defined several fragments of  
languages defined in TAPL (using a "fully concrete" representation  
for binders) and we proved type preservation in Isabelle/Hol, Hol,  
and Coq.

The result of our experience is that proofs of fragments involving  
list types (e.g.. records) turned out to be much simpler in Hol  
(proofs done by Scott Owens) and Isabelle/Hol (proofs done by Thomas  
Ridge) than in Coq.  (However this is a personal experience, and the  
result might just be related to the experience of the man driving the  
theorem prover).

The Hol and Isabelle/Hol scripts are available from http:// 
moscova.inria.fr/~zappa/software/ott (example   TAPL-roughly-full- 
simple).

> In Coq developments related to programming language theory,  
> extending "Scheme" would save a lot of redefinitions of list types  
> like in the example above.

Very suboptimal, but, given the syntax of your language definition,  
the Ott tool can generate the most general induction principle, which  
you can then copy/paste into your Coq development.

Regards
-francesco