The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

> On Nov 18, 2014, at 19:31 , Daniel Schepler 
> <dschepler AT gmail.com>
>  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.

Daniel,

I am not sure I understand your suggestion. Are we talking about
your definition of vector (for which you have 'vector_cons_proper')
or the one from standard library?

I am hesitant switching to new vector definition as it would entail
redoing a lot of my existing proofs.

Sincerely,
Vadim Zaliva

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva