The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

When working with typeclasses, I often find myself wanting something
like a class_simpl tactic which would unfold typeclass projections and
instances (except where the instance is an atomic variable, section
hypothesis, axiom/parameter, etc.).  So, for example, in this:

Require Import Morphisms.

Class Zero (A:Type) : Type :=
zero : A.

Class Plus (A:Type) : Type :=
plus : A -> A -> A.

Class Equiv (A:Type) : Type :=
equiv : A -> A -> Prop.

Notation "0" := zero.
Infix "+" := plus.
Infix "==" := equiv (at level 70).

Class Plus0L (A:Type) `{Zero A} `{Plus A}
  `{Equiv A} : Prop :=
plus_0_l : forall x:A, 0 + x == x.

Instance prod_zero (A B:Type) `{Zero A} `{Zero B} :
  Zero (A * B) :=
(0, 0).

Instance prod_plus (A B:Type) `{Plus A} `{Plus B} :
  Plus (A * B) :=
fun p1 => let '(a1, b1) := p1 in
fun p2 => let '(a2, b2) := p2 in
(a1 + a2, b1 + b2).

Inductive prod_equiv (A B:Type) `{Equiv A} `{Equiv B} :
  Equiv (A * B) :=
| pair_proper_pre : Proper (equiv ==> equiv ==> prod_equiv A B)
  (@pair A B).
Existing Instance prod_equiv.
Instance pair_proper (A B:Type) `{Equiv A} `{Equiv B} :
  Proper (equiv ==> equiv ==> equiv) (@pair A B) :=
pair_proper_pre A B.

Instance prod_plus0l (A B:Type) `{Plus0L A} `{Plus0L B} :
  Plus0L (A * B).
Proof.
intros [a b].

Here, I would love a class_simpl tactic to do the equivalent of:
unfold equiv, plus, prod_plus, zero, prod_zero.
to convert:
0 + (a, b) == (a, b)
to:
prod_equiv (0 + a, 0 + b) (a, b)

(And then the proof would finish with:
constructor; apply plus_0_l.
Qed.
)

So, is there an existing tactic which would do this, that I'm missing?
-- 
Daniel