The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

Le 23 nov. 08 à 20:18, Brian Aydemir a écrit :

> Hi,

Hi,

> I have a question about working with type classes in 8.2beta.  In case
> it matters, I'm currently using the subversion branch (r11609).  I'll
> being with some commented code to illustrate my question.

<snip/>

> (* Let's try working with the class now. *)
>
> Lemma test : forall t1 t2,
>  twiddle 2 (bar_two t1 t2) = bar_two t1 t2.
> Proof.
>  intros.
>  simpl.
>
>  (* The goal is:
>
>       bar_two (twiddle_bar 2 t1) (twiddle_bar 2 t2) = bar_two t1 t2
>
>     While not surprising, one might hope for the following instead,
>     especially since [rewrite twiddle_ax] and [f_equal; apply  
> twiddle_ax]
>     fail on the above.
>
>       bar_two (twiddle 2 t1) (twiddle 2 t2) = bar_two t1 t2
>
>  *)
>
>  change twiddle_bar with (@twiddle bar _).
>
>  do 2 rewrite twiddle_ax.
>  reflexivity.
> Qed.
>
> In the above code, I saw twiddle_bar where I wanted to see twiddle.  I
> couldn't apply facts about twiddle because "twiddle_bar" and "twiddle"
> didn't match in any way (so the error messages tell me).
>
> In general, I imagine that when working with type classes, I want to  
> see
> things in terms of the abstractions those classes provide, because I'm
> likely to have all my theorems and other definitions stated in terms  
> of
> those abstractions, and I'm likely to be thinking in terms of those
> abstractions.  I don't want to see the names of the definitions for
> specific instances if I can avoid it.

There's a choice to make because even if you don't want to see  
[twiddle_bar]
here, you still want to get it's reduction behavior. Having one  
without the other
seems impossible to me. However having a [fold] command that works up
to typeclasses could help recover the abstraction more easily.

> In the above example, I used the [change] tactic, in some sense, to
> restore the abstraction provided by the type class.  Is there any  
> advice
> on how to do this in general, or to avoid the problem altogether?
> Alternatively, am I thinking about type classes in the wrong way?  I
> would appreciate hearing people's thoughts on this.

I've not enough experience for definite statements, all I can say is  
that I
never had this issue before. I guess that's mainly because I usually  
didn't
use the abstract methods to reason on effective code but mostly used  
them
after the fact and to reason on the abstract structures. Currently I  
have no
better suggestion than a folding tactic. Even if you add sufficient  
information
to the [twiddle_ax] lemma to infer the instance, [rewrite] won't unify
[twiddle 2 t1] and [twiddle_bar 2 t1] due to restrictions on the delta- 
reductions
allowed.

I guess users of Canonical Structures may have had a similar problem.
Application of the [rewrite] lemma on the simplified goal would require
infering "back" the [Twiddle_bar] record during unification. The  
ssreflect
[rewrite] might be able to do that (simply declaring [Twiddle_bar] as
canonical in Coq doesn't work of course).

Cheers,
-- Matthieu