The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Nov 19, 2014, at 12:30 , Daniel Schepler <dschepler AT gmail.com> wrote:

I've replied privately to Vadim with my file, rewritten to use standard library Vector.t.  f_equiv works beautifully after changing Vector.cons to vcons_reord, though the rewrite still isn't working.

While I am still studying Daniel’s solution which is quite involved I could not help thinking that should be an easier way to do this.

I want to use simple setoid rewriting here. For example, why it does not work here:

Proof state:

1 subgoals, subgoal 1 (ID 1804)

  

  B : Type

  H : Equiv B

  A : Type

  f : A → A → B

  CO : ∀ x y : A, f x y = f y x

  SB : Setoid B

  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

  ============================

   VConsR (map2 f (Vtail a) (Vtail b)) (f (Vhead a) (Vhead b)) = map2 f b a

I want to swap arguments of ‘f'. Using standard ‘eq’ I could easily do that by:

setoid_replace  (f (Vhead a) (Vhead b)) with (f (Vhead b) (Vhead a)) using relation (@eq B).

and I will get 

(… same context as above ...)

  ============================

   VConsR (map2 f (Vtail a) (Vtail b)) (f (Vhead b) (Vhead a)) = map2 f b a

subgoal 2 (ID 1821) is:

 f (Vhead a) (Vhead b) ≡ f (Vhead b) (Vhead a)

Which is what I expect. However if I try to do the same trick using ‘equiv’:

  setoid_replace  (f (Vhead a) (Vhead b)) with (f (Vhead b) (Vhead a)) using relation (@equiv B).

I get the following error:

Toplevel input, characters 0-94:

In nested Ltac calls to "setoid_replace" and "(rel x y)" (with rel:=equiv,

y:=f (Vhead b) (Vhead a), x:=f (Vhead a) (Vhead b)), last term evaluation

failed.

Error:

In environment

B : Type

H : Equiv B

A : Type

f : A → A → B

CO : ∀ x y : A, f x y = f y x

SB : Setoid B

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

The term "f (Vhead a) (Vhead b)" has type "B"

 while it is expected to have type "Equiv B".

Am I using wrong syntax here or the problem's elsewhere? 

Thanks!

Sincerely,
Vadim