The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is there a way to rewrite with a hypothesis that whose type is convertible with [pointwise_relation A R f g] without first explicitly changing its type to that?  For example, is there an instance I can add to get the following [setoid_rewrite] to work?

Require Import Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms.

Add Parametric Morphism A B : (@map A B)

    with signature (pointwise_relation A (@eq B)) ==> @eq _ ==> @eq _

      as map_eq_mor.

Proof.

  intros x y H ls; hnf in H.

  induction ls; auto; simpl.

  rewrite -> H, -> IHls; reflexivity.

Qed.

Goal forall A B (f g : A -> B) (H : forall x, f x = g x) ls, map f ls = map g ls.

Proof.

  intros.

  setoid_rewrite H. (* Toplevel input, characters 15-31:

Error: Tactic failure:setoid rewrite failed: Nothing to rewrite. *)

Thanks,

Jason