The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thu, Nov 20, 2014 at 7:58 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

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).

@equiv is of type (forall (A:Type), Equiv A -> (A -> A -> Prop)).  You probably want (@equiv B _) to let it autoresolve the instance of Equiv B to fill in for the second argument.

By the way, we finally figured out how to get rewriting to work as expected: it turned out to be a case where putting in a copy of the original Proper instance, but with slightly relabeled type, allowed the system to resolve the properness.  i.e. the original was Proper ((=) ==> vector_equiv ==> vector_equiv), the copy was Proper ((=) ==> (=) ==> (=)).

-- 

Daniel Schepler