The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 09/09/2016 01:09 PM, Daniel Schepler wrote:
> 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.
> )

One can use "constructor; apply plus_0_l" to prove this without doing 
any unfolding.  So, I suppose you are just asking for the unfold so that 
you see the simplification interactively first?

I don't think there is a way tactically to decide if a definition is an 
instance, let alone a particular kind of instance.  Similarly for 
projections - although in 8.6, there is an is_proj tactic (thanks to 
Jason), but I think that is only for primitive projections.

However, it might be possible to get something close to what you want 
via the Arguments notations that interact with cbn and simpl.

Otherwise, probably autounfold using a db that you populate with just 
the instances and projections you want is your best bet.

-- Jonathan