The Coq mailing list

[Jean-Yves Vion-Dury <jean-yves.vion-dury AT inrialpes.fr>]

This is certainly not possible: the equality in coq is really "strong", as shown by "Print eq", whereas it looks like you rather need an equivalence relation "~".

I used the following definition for my own purposes:

Variable A B:Type.
Inductive sim (f g:(A->B)) : Prop := simi: (forall x:A,(f x)=(g x)) -> (sim f g).

Notation "f '~' g" := (sim f g) (at level 60).

then you can easily prove it is an equivalence relation and use it further.


Require Import Relations.

Theorem sim_equiv: (equivalence _ sim).
constructor.

(* reflexive *)
unfold reflexive;intro;constructor;reflexivity.

(* transitive *)
unfold transitive.
   intros x y z [H1] [H2]; constructor;intro.
   rewrite H1; rewrite H2; reflexivity.

(* symmetric *)
unfold symmetric.
   intros x y [H];constructor.
   intro;rewrite H;reflexivity.

Qed.


on this basis you can extend the inductive definition if required...
hope this heps.

Jean-Yves

--

Jean-Yves Vion-Dury   Research Scientist	Xerox Research Centre Europe
INRIA (sabbatical) 655 avenue de l'Europe, 38334 Montbonnot (FRANCE) Jean-Yves.Vion-Dury AT inrialpes.fr	from France:   0 4 76 61 53 83 from abroad: +33 4 76 61 53 83
you may have heard of Circusthe Transformation Language I designed ?	show me