The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Wed, 22 Jun 2011 18:19:15 +0200,
Laurent Théry 
<Laurent.Thery AT inria.fr>
 a écrit :

> 
> Hi,
> 
> I'm experiencing a severe performance degradation when I am doing 
> interactive proofs with very big terms in Coq.
> Why is it so? Here is a stupid small example:
> 
> I define a dastructure and a lemma that makes the goal grow, and I
> test the time the tactic apply is taking:
> 
> (*************************************************************************)
> 
> Require Import Bool.
> 
> (* Binary trees *)
> Inductive BTree :=  BLeaf (b : bool) | BNode (bT1 bT2 : BTree).
> 
> (* Stupid lemma to make things grow *)
> Lemma BTinv:  forall bt (bt1 := BNode bt bt),  bt1 = bt1 -> bt = bt.
> Proof. auto. Qed.
> 
> Lemma BTex: BLeaf true = BLeaf true.
> Proof.
> idtac "1-> 15". Time do 15 apply BTinv.
> idtac "16". Time apply BTinv.
> idtac "17". Time apply BTinv.
> idtac "18". Time apply BTinv.
> idtac "19". Time apply BTinv.
> idtac "20". Time apply BTinv.
> idtac "refl_equal". Time apply refl_equal.
> Time Qed.
> 
> (*************************************************************)
> 
> Compiling this with coqc I get (I'm using coq8.3pl1)
> 
> ====================================
> 
> 1-> 15
> Finished transaction in 1. secs (0.884866u,0.007999s)
> 16
> Finished transaction in 1. secs (1.132828u,0.010999s)
> 17
> Finished transaction in 2. secs (2.008695u,0.026995s)
> 18
> Finished transaction in 5. secs (4.437325u,0.037995s)
> 19
> Finished transaction in 10. secs (9.628537u,0.331949s)
> 20
> Finished transaction in 31. secs (28.279701u,1.209816s)
> refl_equal
> Finished transaction in 15. secs (12.974027u,0.905862s)
> Finished transaction in 52. secs (51.655147u,0.158976s)
> 
> =====================================
> 
> 
> 15 seconds for the refl_equal  !!!! 52 second for the Qed!
> 

Maybe that tactics build effectively a tree of 2²⁰ elements, which is
quite big for coq, and at the end it has to check equality between two
big trees.


> If I try to build and check inside Coq the equality of two trees of 
> height 20, it takes less
> than 2 seconds:
> 
> (*************************************************************)
> 
> Fixpoint eBt (bt1 bt2 : BTree) :=
>   match bt1 with
>   |  BLeaf b1 =>
>        match bt2 with
>        | BLeaf b2 => eqb b1 b2
>        | _ => false
>        end
>   |  BNode bt11 bt12 =>
>          match bt2 with
>          | BLeaf b2 => false
>          | BNode bt21 bt22 =>
>              match eBt bt11 bt21 with
>              | true => eBt bt12 bt22
>              | _ => false
>              end
>          end
> end.
> 
> Fixpoint vBt (n : nat) :=
>    match n with O => BLeaf true | S n1 => let v := vBt n1 in BNode v
> v end.
> 
> Time Eval compute in
>    let v1 := vBt 20 in
>    let v2 := vBt 20 in eBt v1 v2.
> (* Finished transaction in 2. secs (1.752734u,0.001999s) *)
> 
> (*******************************************************************************)

In the second part, you write directly the tree, so the branches points
to the same location, so that you only have a chain of 20 nodes which
is a lot smaller.

It is the only possible reason I see.
(For the second part, I am pretty sure it is the way it works, for the
first part I don't know enough about tactic mechanism, but with a
linear representation, it shouldn't take so much time, so I guess
that the tree is completely expanded; taking a look at memory
consumption, should tell us more.)