The Coq mailing list

[Laurent Th�ry <Laurent.Thery AT inria.fr>]

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!

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) *)

(*******************************************************************************)