The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, Nov 18, 2014 at 6:08 PM, Vadim Zaliva 
<vzaliva AT cmu.edu>
 wrote:
> Thanks. I've fixed my lemma definition to avoid duplicate Equiv and added
> Setoid:
>
> Lemma map2_setoid_comm {A} `{HS: Setoid B, !Commutative f}:
>   forall n (a b: vector A n),
>      (map2 f a b) = (map2 f b a).
>
> Still as in your example the problem remains. It looks like we are stuck
> here.

Well, in this case you could always just directly "apply
vector_cons_proper." and decompose into equivalences of the arguments.
That way, you wouldn't even need the Setoid B assumption.

Which reminds me: I've been meaning to ask whether there's some
existing tactic that would act like "setoid f_equal".  It would mostly
be a convenience tactic for finding an appropriate instance of Proper
and then applying it, where "apply proper_prf" usually doesn't work
because it tries to unify (f a b) and (f c d) in R (f a b) (f c d).
-- 
Daniel Schepler