The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

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]
>> 
>