The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

Hi!

I am trying to do something like this:

Require Import Setoid.
Require Import Morphisms.

Class Equiv A := equiv : relation A.
Class Setoid A {Ae : Equiv A} : Prop := setoid_eq :> Equivalence (@equiv A 
Ae).
Class Mult A := mult: A -> A -> A.
Instance: Equiv nat := eq.

Set Printing Implicit.

Definition testF (A B: Type) (f:A->B) : nat := 0.

Lemma test (A:Type) `{Setoid A, Mult A} (x:A):
  equiv (testF A A (mult x)) (testF A A (fun (x0:A) => mult x x0)) .
Proof.
  setoid_replace (fun (x0:A) => mult x x0) with (mult x).
Qed.

How one would define Proper instance to make this possible?
It looks like I need something like FunctionalExtensionality.

Thanks!

P.S. Obviously this is artificial example just to demonstrate the kind
of rewriting I am trying to do.

Sincerely,
Vadim