The Coq mailing list

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

On 07/19/2012 11:50 AM, Adam Chlipala wrote:
> On 07/19/2012 09:59 AM, Frédéric Besson wrote:
> > I tried to tackle your problem using proof by reflection.
> > This seems to be significantly faster:
> > the equivalent of repeat split takes 180s for (truuue 40) ~ 40000 
> > sub-goals but bigger problems trigger a stack overflow.
>
> This is indeed a very interesting idea!  Thanks for sharing it.
>
> I find that there are no time savings if I need to do an explicit 
> reification step, converting a "real" conjunction into your [Tree] 
> type.  (Though, based on our recent experiences, implementing 
> reification in OCaml would probably lead to an overall speed-up.)
>
> However, I can reformulate the Gallina function generating the goals, 
> so that it outputs [list Prop] instead of just [Prop] with ad-hoc use 
> of conjunction.  I manually rearranged one of my largest goals (34-way 
> conjunction, with various nesting patterns) into a [List.Forall] on a 
> [list Prop] and tried your basic method on it.  The impact is not 
> huge, but it reduces time from about 7 seconds to about 2 seconds, 
> compared against [repeat (apply List.Forall_nil || apply 
> List.Forall_cons)].
>
> This is still a big enough difference that I will try the 
> reformulation.  Thanks again for the idea!

Update on the outcome: I've made the change and tested on my largest 
goal, which was a 93-way conjunction.  The whole proof step now takes 
less time than the was previously taken by a subset of the 
conjunctions.  Using reflection vs. a naive [repeat constructor] style 
reduces the running time from about 50 seconds to about 10 seconds.