The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

I am trying to prove following lemma:

Lemma map2_setoid_comm `{Equiv B} `{Commutative B A}:
  forall n (a b: vector A n),
     (map2 f a b) = (map2 f b a).

I am using Equiv and Commutative type classes from CoRN. For convenience I am 
also using VecUtil from CoLoR which provide several handy definitions for 
fixed-size vectors.

Require Import abstract_algebra orders.minmax interfaces.orders.
Require Import MathClasses.theory.rings.
Require Import CoLoR.Util.Vector.VecUtil.
Import VectorNotations.

The equivalence used here (=) is 'equiv'. I was able to instantiate:

Definition vec_equiv `{Equiv A} {n}: relation (vector A n) := Vforall2 (n:=n) 
equiv.
Instance vec_Equiv `{Equiv A} {n}: Equiv (vector A n) := vec_equiv.

which permitted me to use reflexivity tactics to prove IH. Now I am trying
to use 'commutativity' but no luck so far:

1 subgoals, subgoal 1 (ID 1405)
  
  B : Type
  H : Equiv B
  H0 : Equiv B
  A : Type
  f : A → A → B
  H1 : Commutative f
  n : nat
  a : vector A (S n)
  b : vector A (S n)
  IHn : ∀ a0 b0 : vector A n, map2 f a0 b0 = map2 f b0 a0
  ============================
   Vcons (f (Vhead a) (Vhead b)) (map2 f (Vtail a) (Vtail b)) = map2 f b a

As the next step I want rewrite LHS cons head by replacing  (f (Vhead a) 
(Vhead b)) with (f (Vhead b) (Vhead a)) by commutativity. I could not make it 
work with any of rewrite tactics.

I will appreciate if somebody would point me in the right direction. Thanks!

Sincerely,
Vadim