The Coq mailing list

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

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!

Still, 2 seconds to split a 34-way conjunction seems excessive; a 
standalone tool implemented in OCaml would never take anywhere near that 
long.  Further suggestions on closing this gap would be very welcome.

> Inductive Tree : Type :=
> | Leaf (A:Prop)
> | Node (L:Tree) (R:Tree).
>
> Fixpoint iTree (t : Tree) : Prop :=
>    match t with
>      | Leaf A =>  A
>      | Node L R =>  (iTree L) /\ (iTree R)
>    end.
>
> Fixpoint xflatten (t : Tree) (acc: Prop) : Prop :=
>    match t with
>      | Leaf A =>  A ->  acc
>      | Node L R =>  xflatten L (xflatten R acc)
>    end.
>
> Lemma xflatten_split : forall t (p:Prop), (iTree t ->  p) ->   xflatten t p.
> Proof.
>    induction t.
>    simpl. tauto.
>    simpl.
>    intros.
>    apply IHt1.
>    intros.
>    apply IHt2.
>    intros.
>    apply H ; tauto.
> Qed.
>
> Lemma flatten_split : forall t, xflatten t (iTree t).
> Proof.
>    intros.
>    apply xflatten_split ; auto.
> Qed.
>
> Fixpoint truueT (n : nat) : Tree :=
>   match n with
>     | O =>  Leaf True
>     | S n' =>  Node (Leaf True)  (truueT n')
>   end.
>
> Fixpoint truuueT (n : nat) : Tree :=
>   match n with
>     | O =>  Leaf True
>     | S n' =>  Node (truueT 1000) (truuueT n')
>   end.
>
> Set Silent.
>
> Goal iTree (truuueT 40).
> Time generalize (flatten_split (truuueT 40));
>    set (f := truuueT 40);
>    generalize (iTree f);
>    intros ; compute in H; apply H; clear H.
>