The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

> I'll also note that even just a single [split] takes multiple seconds in my
> example.  It would be nice for the overall split to be instantaneous, and
> your suggestion doesn't seem to lead in that direction.

Not so long ago, Laurent asked a related question on Coq-club, about a
drop of performance when manipulating big terms. I adapted his example
(define a data-structure and a lemma that makes the goal grow, and
then test the time the tactic split is taking). As the terms grow,
split becomes more and more slow, even if there is conceptually
nothing to do...

Note that my system cannot manage the 19th split: it runs out of memory...

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

Require Import Bool.

(* Binary trees *)
Inductive BTree :=  BLeaf (b : bool) | BNode (bT1 bT2 : BTree).

(* Stupid lemma to make things grow *)
Lemma BTinv2 : forall bt,
                 let bt1 := BNode bt bt in
                   bt1 = bt1 /\ bt1 = bt1 ->
                   bt = bt /\ bt = bt.
intros; split; auto using  BTinv.
Qed.

Lemma idem A : A /\ A -> A. tauto. Qed.

Lemma BTex: BLeaf true = BLeaf true /\ BLeaf true = BLeaf true.
Proof.
idtac "1-> 10". Time do 10 apply BTinv2. Time split. apply idem. admit.
idtac "11". Time apply BTinv2. Time split. apply idem. admit.
idtac "12". Time apply BTinv2. Time split. apply idem. admit.
idtac "13". Time apply BTinv2. Time split. apply idem. admit.
idtac "14". Time apply BTinv2. Time split. apply idem. admit.
idtac "15". Time apply BTinv2. Time split. apply idem. admit.
idtac "16". Time apply BTinv2. Time split. apply idem. admit.
idtac "17". Time apply BTinv2. Time split. apply idem. admit.
idtac "18". Time apply BTinv2. Time split. apply idem. admit.
idtac "19". Time apply BTinv2. Time split. apply idem. admit.
idtac "20". Time apply BTinv2. Time split. apply idem. admit.
idtac "final split"
Time split.
idtac "refl_equal".
Time apply refl_equal.
Time apply refl_equal.
Time Qed.

(*************************************************************************)
(* Compiling with coqc 8.4 beta2 *)

1-> 10
Finished transaction in 0. secs (0.033383u,0.001061s)
Finished transaction in 0. secs (0.051013u,0.001227s)
11
Finished transaction in 0. secs (0.045126u,0.000939s)
Finished transaction in 1. secs (0.10977u,0.003316s)
12
Finished transaction in 0. secs (0.094997u,0.002151s)
Finished transaction in 0. secs (0.249122u,0.005024s)
13
Finished transaction in 0. secs (0.210198u,0.006272s)
Finished transaction in 0. secs (0.51702u,0.00723s)
14
Finished transaction in 1. secs (0.536459u,0.013254s)
Finished transaction in 1. secs (1.147184u,0.014393s)
15
Finished transaction in 2. secs (1.402735u,0.028499s)
Finished transaction in 2. secs (2.70808u,0.030295s)
16
Finished transaction in 4. secs (4.219761u,0.067783s)
Finished transaction in 7. secs (7.010735u,0.079442s)
17
Finished transaction in 13. secs (13.671158u,0.165469s)
Finished transaction in 21. secs (20.624784u,0.198532s)
18
Finished transaction in 46. secs (44.696678u,0.450727s)
Finished transaction in 75. secs (74.620911u,0.610548s)
19
Finished transaction in 180. secs (161.582276u,4.756405s)