The Coq mailing list

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

I'm running into some trouble with efficient proving of large 
conjunctions being produced by Gallina functions.  (My concrete context 
is a verification condition generator, in the Hoare Logic style, 
implemented in Gallina).

The basic problem is how to reduce a large conjunction into a subgoal 
per conjunct, without taking an excessive amount of time.  I run into 
the same basic issue with such alternatives as [List.Forall] with long 
list arguments.

Here's an example with a contrived very large conjunction.  The single 
[split] invocation near the end takes 5 seconds, and just "peeling away" 
the outer tier of conjunctions would require about 100 further [split] 
calls, each taking only a little less time than the previous one.  This 
quickly comes to be a dominating factor in the time to run proof scripts.

So, my question/challenge regarding this example is: how could I prove 
the goal in substantially less time?  Of course, I'm really interested 
in a strategy that would apply to large conjunctions in general.  Thanks!

(**)
Fixpoint truue (n : nat) : Prop :=
  match n with
    | O => True
    | S n' => True /\ truue n'
  end.

Fixpoint truuue (n : nat) : Prop :=
  match n with
    | O => True
    | S n' => truue 1000 /\ truuue n'
  end.

Goal truuue 100.
  compute.
  Time split. (* 5 secs *)
(**)