The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

If you do

Arguments plus {A Plus} !_ !_ /.

then simpl on

0 + (a, b) == (a, b)

reduces to

prod_equiv A B (0 + a, 0 + b) (a, b)

without reducing 0 + x == x for x : A * B

I don't know that it would do the right thing (whatever that means) in 
other situations though.

Gaëtan Gilbert

On 09/09/2016 19:09, 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.
> )
>
> So, is there an existing tactic which would do this, that I'm missing?