The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 09/09/2016 01:46 PM, Jonathan Leivent wrote:
> 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.

On second thought, there may be a way in 8.5 to tactically detect if a 
function is basically a projection - either defined directly, or acts 
like one.  Roughly, the way to do this would be to show that calling 
that function on an arbitrary instance of its first non-dependent arg 
type, then destructing that instance produces exactly one subgoal in 
which the function call reduces to a component of that instance (which 
would be a single var in that subgoal introduced by the destruct).  I 
think that can be done in 8.5.

However, I still think there's no way to detect instances vs. other 
definitions.

-- Jonathan