coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Matthieu Sozeau <mattam AT mattam.org>
- To: Thomas Braibant <thomas.braibant AT gmail.com>
- Cc: Adam Koprowski <adam.koprowski AT gmail.com>, coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Dreadful performance of setoid rewrite in Coq 8.3-beta & trunk.
- Date: Thu, 10 Jun 2010 10:17:12 -0400
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to:x-mailer; b=iIFQnVu0DHs2ysfkTJndBP8zZ/hPaKZjIuFaUkgMV5gIvuYnuA74m04AQ4oQEV/wV+ LM4EHQAV1lL95cmxz8CTI5VJvK96N5nsu9fxj8NIEsf7malWm/egRpvLvg9anev+vqGF Hugz2MxMicltwf+zS4ad2K4tSDSdTIphCp58k=
Hi everyone,
Le 10 juin 2010 à 06:57, Thomas Braibant a écrit :
> 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.
It is the resolution that is (apparently) diverging, due to the (new) set of
instances
in RelationPairs. A quick workaround for this example is to define:
Instance pair_proper A B : Proper (@eq A ==> @eq B ==> eq) (@pair A B).
Admitted.
Before the lemmas, it will take precedence over the general pair_compat
instance
in RelationPairs and avoid a costly search.
The heart of the problem (same for Adam's example) is that pair_compat uses
the RelProd relation (noted *). In that case it produces a constraint like
[Proper (eq * eq ==> eq ==> eq) pair] which cannot be solved if we don't know
that
[@eq
A * @eq B] is equivalent to
[@eq
(A * B)]. As this is not derivable currently, the proof search explores a
very large state space, also applying instances from RelationPairs that it
shouldn't try. This fact can be added though, by defining the following
recursive [subrelation] instances:
Import RelationPairs.
Generalizable All Variables.
Instance subrela_eqprod A B `(subrelation A RA (@eq A)) `(subrelation B RB
(@eq B)) :
subrelation (RelProd RA RB) (@eq (A * B)).
Proof.
unfold RelProd, relation_conjunction, predicate_intersection. reduce.
destruct H1. red in H1, H2.
destruct x ; destruct x0; simpl in *. apply H in H1. apply H0 in H2.
congruence.
Qed.
Instance subrela_eqprod' A B `(subrelation A (@eq A) RA) `(subrelation B (@eq
B) RB) :
subrelation (@eq (A * B)) (RelProd RA RB).
Proof.
unfold RelProd, relation_conjunction, predicate_intersection. reduce. subst.
destruct x0; firstorder.
Qed.
Then all examples go through in reasonable time. I will add these to the
standard library and fix the dangerous instances as well.
Cheers,
-- Matthieu
> 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]
>>
>
- [Coq-Club] Dreadful performance of setoid rewrite in Coq 8.3-beta & trunk., Adam Koprowski
- Re: [Coq-Club] Dreadful performance of setoid rewrite in Coq 8.3-beta & trunk., AUGER Cedric
- Re: [Coq-Club] Dreadful performance of setoid rewrite in Coq 8.3-beta & trunk.,
Thomas Braibant
- Re: [Coq-Club] Dreadful performance of setoid rewrite in Coq 8.3-beta & trunk., Adam Koprowski
- Re: [Coq-Club] Dreadful performance of setoid rewrite in Coq 8.3-beta & trunk., Matthieu Sozeau
Archive powered by MhonArc 2.6.16.