The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Dec 12, 2014, at 6:10 , Guillaume Melquiond 
<guillaume.melquiond AT inria.fr>
 wrote:
> 
> If I am not mistaken, you have never told Coq that vecequiv is an 
> equivalence relation (and thus reflexive). As a consequence, it cannot 
> prove "@vecequiv A Ae n z z" and thus it is unable to perform the 
> replacement due to the "@vecequiv M Me n" part of your Proper.

Guillaume,

I am not sure this is the reason. I have extended my example with another 
Proper instance, this time for Vcons and in example lemma 'Vcons_equiv_intro' 
it works using the same 'vecequiv'.

Set Printing Implicit.

Require Import Setoid.
Require Import Morphisms.
Require Import Vector.

Class Equiv A := equiv : relation A.
Class Setoid A {Ae : Equiv A} : Prop := setoid_eq :> Equivalence (@equiv A 
Ae).
Class Mult A := mult: A -> A -> A.
Instance vecequiv A `{Equiv A} n : Equiv (Vector.t A n). admit. Defined.
Definition Vmap_reord (A B: Type) (n:nat) (f:A->B) (x: Vector.t A n): 
Vector.t B n := Vector.map f x.
Definition Vcons_reord {A} {n} (t: Vector.t A n) (h:A): Vector.t A (S n) := 
@Vector.cons A h n t.

Instance vec_Equivalence (A:Type) `{Ae: Equiv A} {n:nat}
         `{!Equivalence (@equiv A _)}
: Equivalence (@vecequiv A Ae n).
Proof. admit. Qed.

Instance Vcons_reord_proper (A:Type) `{Equiv A} n:
  Proper (@vecequiv A _ n ==> (equiv) ==> @vecequiv A _ (S n))
         (@Vcons_reord A n).
Proof. admit. Qed.

Instance Vmap_reord_proper_pointwise n  (M N:Type) `{Ne:!Equiv N, Me:!Equiv 
M}:
  Proper ((pointwise_relation M Ne) ==> (@vecequiv M Me n) ==> (@vecequiv N 
Ne n)) (@Vmap_reord M N n).
Proof. admit. Qed.

Lemma Vcons_equiv_intro (A:Type) `{Setoid A} : forall a1 a2 n (v1 v2 : 
Vector.t A n),
                            a1 = a2 -> v1 = v2 -> Vcons_reord v1 a1 = 
Vcons_reord v2 a2.
Proof.
  intros.
  rewrite H0.
  rewrite H1.
  reflexivity.
Qed.

Lemma test (A:Type) `{Setoid A, Ma:!Mult A} (x:A) {n} (z: Vector.t A n):
  equiv
    (Vmap_reord A A n (@mult A Ma x) z)
    (Vmap_reord A A n (fun x0 : A => mult x0 x) z).
Proof.
  setoid_replace (fun x0 : A => mult x0 x) with (@mult A Ma x).
  (* ... *)
Qed.

P.S. I also added Equivalence instance for vecequiv but it did not help 
either.

> PS: Do not ask me how I was able to infer that from the error message; I 
> didn't.

I wish there is a better error reporting for such situations. For example 
when I try
to use f_equiv sometimes it gives a pretty clear message that Proper instance 
is missing.
I wish rewrite did the same.

Sincerely,
Vadim Zaliva

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