The Coq mailing list

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

Interesting enough,  the following is long too.

Lemma test_rewrite x y :
  P.eq x y ->
  (P.mem (A, B) x, true, true) =
  (P.mem (A, B) y, true , true).
Proof.
intros H. rewrite H.
Abort.

while the two followings are fast.

Lemma test_rewrite x y :
  P.eq x y ->
  (P.mem (A, B) x && true && true) =
  (P.mem (A, B) y && true && true).
Proof.
intros H. rewrite H. reflexivity.
Qed.

Lemma test_rewrite x y :
  P.eq x y ->
  (P.mem (A, B) x , true ) =
  (P.mem (A, B) y,  true ).
Proof.
intros H. rewrite H. reflexivity.
Qed.

is fast.

I would guess that the way rewrites are handled under tuples has
changed. Indeed, generating the proof term showing that one can
rewrite in one component of a tuple of arbitrary size could be tricky.
On the other hand, I cannot arrive to the point when I can have a look
at the generated proof term.


thomas



On Thu, Jun 10, 2010 at 12:06 PM, Adam Koprowski
<adam.koprowski AT gmail.com>
 wrote:
>    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]
>