The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Fri, Sep 9, 2016 at 10:47 AM, Gaetan Gilbert
<gaetan.gilbert AT ens-lyon.fr>
 wrote:
> 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.

I don't know if it would always be "the right thing", but as a first
cut I'd be happy with something like (ltac pseudocode):

Ltac class_simpl :=
repeat match goal with
|- context [?f ?x] =>
   is_class_proj f; is_nonatom_instance x;
   change (f T1 ... Tn x) with (eval red in x) at context
end.

For now, I haven't found an "Arguments" command that would make this work:
set (x := 0 : A*B).  (* x = @zero (A*B) (@prod_zero A B H H3) *)
simpl in x.  (* want x := (0, 0) : A * B, or without notation
  x := @pair A B (@zero A H) (@zero B H3) *)

(So in the pseudocode above, is_class_proj would match f = @zero
(A*B); but I don't want is_nonatom_instance to match subsequently with
f = @zero A, x = H.)
-- 
Daniel