The Coq mailing list

[Christopher Ernest Sally <christopherernestsally AT gmail.com>]

Hi Ilmars

Hmm... what about comparison functions on finite partial maps of different values (but similar keys)?

Best

Chris

On 2 July 2015 at 02:12, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

I had fun with Equivalences today.

At first I made equivalence for functions.

Definition fun_equiv {A B} (f g: A -> B) := forall x y, x = y -> f x = g y.

Instance fun_Equiv {A B}: Equivalence (fun_equiv (A := A) (B := B)).
Proof.
 split; unfold fun_equiv.
  unfold Reflexive. congruence.
  unfold Symmetric. intros. symmetry. eauto.
  unfold Transitive. intros. pose (H _ _ H1). pose (H0 _ _ H1). congruence.
Defined.

Then I had idea of doing the same things for Proper.

Definition Proper_equiv {A B RA RB} (f g: A -> B) (FA: Proper (RA ==> RB) f) (FB: Proper (RA ==> RB) g)
 := forall x y, RA x y -> RB (f x) (g y).

After some time I understood why I can't make an Equivalence. It's because Proper_equiv isn't relation (FA and FB has different types).

Of course, I can make something like this and then further:

Structure morphism A B RA RB := {
 morphism_fun: A -> B;
 morphism_Proper: Proper (RA ==> RB) morphism_fun
}.

Have anyone encountered situation where such structure as 'morphism' had to be made?

I'm just fooling around with Equivalences, and the idea wasn't from any practical problems, so it is interesting for me if it has happened in serious developments.