The Coq mailing list

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

On 07/19/2012 09:05 AM, Jason Gross wrote:
> 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?

Yes, I've also observed that the tactic runs much more quickly with 
variables introduced to stand for the conjuncts.  The problem is that 
Ltac code to perform this manipulation runs for a long time in its own 
right, and getting the conjuncts to be abstracted with names in the 
first place would require significant changes to the Gallina function 
generating the goals, harming the modularity of the implementation.