The Coq mailing list

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

How about

Arguments prod_zero A B {_ _} /.
Arguments zero {_ !_} /.

?

Gaëtan Gilbert

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