The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

Hi Mark,

Le 9 nov. 08 à 14:20, Mark Dickinson a écrit :

> (**
>
> Section 23.12 of the reference manual for Coq v8.2, 'Constant
> unfolding', seems to say that setoid_rewrite and related tactics
> should automatically unfold definitions declared using "Typeclasses
> unfold ...".

</snip>

> But the proof stops at the first 'setoid_rewrite', with the error  
> message:
>
>  Toplevel input, characters 16-44:
>  Error: The term does not end with an applied homogeneous relation.
>
> So it looks as though setoid_rewrite can't or won't unfold
> 'associative'.  If I manually unfold 'associative' in the declaration
> of assoc:
>
>  assoc : forall a b c : carrier,
>    addition a (addition b c) == addition (addition a b) c;
>
> (and similarly for comm) then the proof works as intended.  I can also
> make it work by supplying enough arguments to assoc to force the
> unfolding;  for example,
>
>  setoid_rewrite <- (assoc A x) at 1.
>  setoid_rewrite (comm A x) at 1.
>
> But if I'm reading section 23.12 right, then neither of these tricks
> should be necessary.  What am I missing here?  Is there a good reason
> why setoid_rewrite doesn't automatically unfold 'associative'?

To quote 18.5.4: "It is useful when some constants prevent some
unifications and make resolution fail." This is meant for the typeclass
resolution process. For [setoid_rewrite], it simply means that if you
declared say [map] as a morphism and you use a definition [fn] which  
really
hides a call to [map] in your goal, then you don't have to redeclare  
[fn]
itself as a morphism. As all constants are transparent by default, you  
don't
have anything to do to benefit from that. But it has little to do with  
reduction
in the type of the lemma.

On the other hand, [setoid_rewrite] could indeed try a little harder at
finding an applied homogeneous relation under definitions, like  
[rewrite]
does when it tries to find a Leibniz equality. The [setoid_rewrite]  
tactic
simply didn't try to reduce the type of the lemma at all if it failed,  
whereas
[rewrite] did as much beta-delta-iota as needed to find the arity of  
the type
and search for a relation there. I will fix this in the trunk and 8.2  
branches.
Your initial proof script will then go through.

Cheers,
-- Matthieu