The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Jean Goubault-Larrecq wrote:
> Le 18/07/12 22:36, Adam Chlipala a écrit :
> > Thanks for the suggestion, but I think this won't help. My conjunctions
> > are generated programmatically and can get arbitrarily long.
>
> Hi, I had exactly the same problem in 2008, where I was
> generating Coq proofs of cryptographic protocols automatically.
> I concur with Laurent that variable arity conjunctions (and
> disjunctions, too) solved my problems.
> For each n-argument conjunction, my proof producing program
> just added a new inductively defined n-ary and, plus a few
> useful lemmas.  The nice thing about Coq here is that split
> will work right away on these new conjunctions.

This is an intuitively appealing idea, with a clear story for why it 
would produce asymptotically significant time and space improvements.  
However, it doesn't seem natural to use in my case.  I essentially have 
an extensible recursive function, with a case added for any programming 
language syntax feature the programmer implements.  Each case naturally 
only has at most a 4-way conjunction (and that's in just one case, with 
no other above a 3-way conjunction).  It's only application to large 
programs that produces many-way conjunctions with medium-sized 
individual conjuncts.

So, I think it would require some extra work to take advantage of larger 
"block size."  Are you suggesting that I do something like build a flat 
list of facts and use a Gallina function to block it into the special 
conjunction type?

I'll also note that even just a single [split] takes multiple seconds in 
my example.  It would be nice for the overall split to be instantaneous, 
and your suggestion doesn't seem to lead in that direction.

Thanks to everyone for the help!