The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

In my earlier email, I thought "=" was a notation for :

https://coq.inria.fr/library/Coq.Init.Logic.html#eq

When rewriting using other relations (e.g. Equiv in your case), you can directly apply the Proper instances. 

Below, I've completed your proof in 8.5 beta 2.

Require Import Setoid Morphisms Vector.

Class Equiv A := equiv : A -> A -> Prop.
Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv).

Global Instance vec_equiv {A} `{Equiv A} {n}: Equiv (Vector.t A n). Admitted.
Global Instance vec_setoid A `{Setoid A} n : Setoid (Vector.t A n). Admitted.

Global Instance tl_proper1 {A} `{Equiv A} n:
 Proper ((equiv) ==> (equiv))
        (@tl A n).
Admitted.

Lemma test:
 forall {A} `{Setoid A} n (xa ya: Vector.t A (S n)),
   (equiv xa ya) -> equiv (tl xa) (tl ya).
Proof.
 intros.
 apply tl_proper1.
 exact H1.
Qed.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sat, May 9, 2015 at 10:49 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

On May 8, 2015, at 18:00 , Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

A small self-contained example would definitely help.

Here is an example which works under 8.4 but gives an error on 8.5:

Require Import Setoid Morphisms Vector.

Class Equiv A := equiv : A -> A -> Prop.

Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv).

Global Instance vec_equiv {A} `{Equiv A} {n}: Equiv (Vector.t A n). Admitted.

Global Instance vec_setoid A `{Setoid A} n : Setoid (Vector.t A n). Admitted.

Global Instance tl_proper1 {A} `{Equiv A} n:

  Proper ((equiv) ==> (equiv))

         (@tl A n).

Admitted.

Lemma test:

  forall {A} `{Setoid A} n (xa ya: Vector.t A (S n)),

    (equiv xa ya) -> equiv (tl xa) (tl ya).

Proof.

  intros.

  setoid_rewrite H1.

  reflexivity.

Qed.

Under Coq 8.5 'setoid_rewrite' gives "Error: build_signature: no constraint can apply on a dependent argument”.

When rewrite fails, I often find it useful to directly invoke or apply eq_rect or eq_ind (these are automatically generated induction principles for the equality type).

Can you show me how to do this in example above? I would love to learn how to debug things like this. Thanks!

Sincerely,
Vadim Zaliva

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060

Skype: vzaliva