The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Nov 18, 2014, at 17:47 , Daniel Schepler <dschepler AT gmail.com> wrote:

You appear to have two instances of Equiv B, which could be confusing things.  My guess would be that you have something like `{Equiv B} `{Commutative f} where the second should be `{!Commutative f} instead.  Also, I don't see any instances of Setoid B which could be useful in inferring Setoid (Vector.t B (S n)), which in turn would be useful for doing the rewriting.

That said, when I tried it with a similar situation with only one Equiv B, and Setoid B in the context (and a registered instance of forall (A:Type) `{Setoid A} (n:nat), Setoid (Vector.t A n)), it still didn't work for me.

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.

Sincerely,
Vadim Zaliva

--

CMU ECE PhD student

Mobile: +1(510)220-1060

Skype: vzaliva