The Coq mailing list

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

On Thu, 10 Jun 2010 12:06:17 +0200
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.
> 

Sorry, I have uninstalled 8.3 and trunk, but if you replace rewrite H
with case H (or destruct H), will there be the same problem?

I avoid when possible use of "rewrite", which gives often very ugly
proof terms, when case or destruct remains readable
(compare it in your example with a "Print test_rewrite."),
and sometimes some complicate mutual recursion are broken with a
rewrite, while it is not the case with a "case",
although, be warned that "case H" produces same goals as "rewrite <- H"
and not "rewrite H".

I know that "rewrite H in *." is more handy than writing a complex
script to do that with "case", so I use it sometimes, as well as I use
"subst".

If the "case" is what you want, then you may have interest in doing
such a tactic.