The Coq mailing list

[Jean Goubault-Larrecq <goubault AT lsv.ens-cachan.fr>]

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.
Best,

-- Jean.