The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

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?

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.  (-:

Cheers,
Brian