The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

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