The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

Le 25 août 08 à 22:22, Brian Aydemir a écrit :

> Hi,

Hi,

> I'm taking a look at type classes in the current svn version of Coq  
> 8.2.  Below, is a silly example that I have a couple questions about.
>
> <<
> Class Foo (A : Type) :=
>  op : A -> bool;
>  op_axiom : forall (x : A), op x = false.
>
> Lemma test : forall [Foo A] [Foo B] (x : A) (y : B),
>  op x = op y.
> Proof.
>  intros.
>  rewrite op_axiom.  (* Succeeds. *)
>  rewrite op_axiom.  (* Fails.  Must say (@op_axiom A) instead. *)
> >>
>
> First, is the failure of the second invocation of rewrite because of  
> how maximally set implicit arguments and type class inference  
> interact?

This whole issue is due to the fact that [rewrite] expects its
argument to be a well-typed, _closed_ term before trying to
unify it with the goal. So, if you use rewrite with any lemma
having maximal implicits and do not give enough arguments so
that these are filled after type-checking with no constraint,
it will fail. Otherwise, rewrite works with classes in the
sense that if your lemma generates class constraints they will
be resolved after unification with the goal, hence the tactic
[rewrite 2 @op_axiom] works (the @ makes every argument explicit).

Actually, the first rewrite succeeds only because when typechecking
[@opaxiom
 ?A ?FooA] we fill ?FooA with the last Foo instance
appearing in the goal, which is a debatable choice, and certainly
not a robust one.

> Second, are there any particular "style guidelines" for writing  
> proofs involving type classes?  The above example maybe suggests  
> that maybe I should be explicit about what type I'm using op_axiom  
> at, i.e., "rewrite (@op_axiom A). rewrite (@op_axiom B)."  That  
> seems like it would lead to a more robust proof script in the long  
> run.  On the other hand, maybe one wants to omit such information  
> from scripts normally, so instead the implicit arguments on op_axiom  
> should be declared to be non-maximal.
>
> Any thoughts here?  I'm simply trying to understand the current  
> design and the expected use patterns.  It's looking nice so far.  (-:

I don't really have style guidelines at this moment but in my
experience the two syntaxes @lemma for unambiguous rewriting
or (lemma (arg:=t)) for disambiguation are enough.

In the long run, we want rewrite/apply/exists etc... to take
open terms and do resolution after whatever unification they
perform. For [apply] there is an experimental [typeclass_app]
tactic that precisely do that and may become the default in the
future. Otherwise it can be somewhat emulated using [refine]
which also works up-to class resolution.

Cheers,
-- Matthieu