The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

   Dear all,

  I have a pretty simple example, attached below, where a rewrite step takes virtually no time in Coq 8.2pl1, but is very slow in newer versions. The timing is as follows:

  Coq 8.2pl1:        0.2sec.

  Coq 8.3-beta:    403.1sec.

  Coq-trunk-13107: 158.1sec.

  Any ideas where this huge difference comes from? This is not a made-up problem, as I have precise instances of this is my development and this problem effectively stops me from being able to upgrade to new versions. Any ideas?

  Best, 

  Adam

--------------------------------- Coq script follows ---------------------------------

Require Import OrderedType OrderedTypeEx FSetAVL Setoid FSetProperties.

Inductive test := A | B | C.

Module Tord_mini <: MiniOrderedType.

  Definition t := test.

  Definition eq := @eq t.

  Axiom eq_refl : forall x : t, eq x x.

  Axiom eq_sym : forall x y : t, eq x y -> eq y x.

  Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.

  Axiom lt : t -> t -> Prop.

  Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.

  Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.

  Parameter compare : forall x y : t, Compare lt eq x y.

End Tord_mini.

Module Tord := MOT_to_OT Tord_mini.

Module TTord := PairOrderedType Tord Tord.

Module P := FSetAVL.Make TTord.

Module PP := FSetProperties.Properties P.

Lemma test_rewrite x y :

  P.eq x y ->

  (P.mem (A, B) x, P.mem (B, C) x, P.mem (A, C) x) =

  (P.mem (A, B) y, P.mem (B, C) y, P.mem (A, C) y).

Proof.

  intros. Time rewrite H. reflexivity.  (* This rewrite step is the problematic one... *)

Qed.

--
Adam Koprowski   [http://adam-koprowski.net]
R&D @ MLstate    [http://mlstate.com, 15 rue Berlier, 75013 Paris, France]