The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I don't know if this is useful in the long-run, or only in solving the problem with [split], but [split] is much faster if you ake it so that Coq doesn't have to move as much stuff around in memory when you [split].  So, for example, with your original code, Adam,

[Time (hnf; split).] takes 0. secs (0.059u,0.s)
[Time (hnf; split; compute).] takes 7. secs (6.286u,0.s)
[Time (compute; split).] takes 10. secs (9.489u,0.s)

[compute. Time split.] gives 8s

[Time compute. Time split.] gives 6. secs (6.151u,0.s), then 9. secs (9.148u,0.s)

The fact that chaining [compute] and [split] makes such a difference (vs. summing their times) suggests that a decent chunk of the time is spent in ... post-processing?  (Does [Time] count the amount of time Coq spends figuring out how to display something to ProofGeneral/emacs?)

So it seems like one possible method of solving this is to keep things as folded as possible when you're splitting (or to fold them up before splitting).

Moving everything into the hypotheses portion, by

  match goal with

    | [ |- ?a /\ ?b ] => pose a as a'; pose b as b'; change (a' /\ b')

  end.

, doesn't seem to buy me anything, so I suspect that (by and large) what matters might be how big the current proof term (as given by [Show Proof]) is in memory.

It's unclear to me how much time working this way actually buys you when you're not doing the proof interactively, though (and Coq doesn't spend time displaying things.)

If I define [truuue] with [truue 100] instead of [truue 1000], then with [Goal truuue 100.], I get the following times:

[compute. Time repeat split.] gives 22. secs (22.314u,0.s)

[Time (compute; repeat split).] takes 26. secs (25.364u,0.s)

  Ltac t' := (split; [ constructor | t' ]) || constructor.

  Ltac t := hnf; (split; [ abstract t' | t ]) || constructor.

  Time t. (* 23. secs (23.36u,0.s) *)

  Ltac t' := (split; [ constructor | t' ]) || constructor.

  Ltac t := hnf; (split; [ t' | t ]) || constructor.

  Time t. (* 9. secs (9.19u,0.s) *)

The time difference between the last two ([abstract] vs. not) is made up for in how long it takes [Qed] to run; about 3 seconds in the former case, and about 10-15 in the latter.

Hopefully some of this is helpful in pointing you to a solution.

-Jason

On Thu, Jul 19, 2012 at 8:15 AM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

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!