The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

With huge help from Daniel we have been able to work out a solution.
I will summarize my findings in case somebody interested. The main missing 
part
was proving Proper for Vcons. It requires two things:

1. Reordering Vcons arguments. I did this like this:

Definition VConsR {A} {n} (t: vector A n) (h:A): vector A (S n) := Vcons h t.

Lemma ConsR_VConsR: forall A n (t: t A n) (h:A), Vcons h t  ≡ VConsR t h.
Proof.
  intros. reflexivity.
Qed.

2. Proving 'Proper' instance:

Global Instance vconsR_proper `{Equiv A} n:
  Proper (@vec_equiv A _ n ==> (=) ==> @vec_equiv A _ (S n))
         (@VConsR A n).
Proof.
  split.
  assumption.
  unfold vec_equiv, Vforall2 in H0.  assumption.
Qed.

Now to use commutativity in the original proof we can just do:

  rewrite ConsR_VConsR.
  rewrite commutativity.

My only remaining regret is that I have two to 2 steps to apply commutativity 
to Vcons.
I guess this could be automated via custom tactics, but I have not even 
started learning LTAC :)

Vadim

> On Nov 18, 2014, at 11:25 , Vadim Zaliva 
> <vzaliva AT cmu.edu>
>  wrote:
> 
> 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

Sincerely,
Vadim Zaliva

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