A Coq question : How to prove the image of the two same valued variables under a function are same?

Question

I want to prove the following Coq theorem. However, I couldn't proceed. Please, give me an advice if possible. Thank you.

---

Require Import QArith.

Variable f : Q -> Q.

Theorem function (x y : Q) : x == y -> f x == f y.

Proof.

---

Answer 1

You can't do that.

You can actually define a function which doesn't respect Q's setoid structure.

Require Import QArith.

Goal exists (f : Q -> Q) (x y : Q), x == y /\ ~(f x == f y).
Proof.
  exists (fun q => Qmake (Qnum q) 1).
  exists (Qmake 2 1), (Qmake 4 2).
  split.
  - reflexivity.
  - discriminate.
Qed.

You have to prove the well-definedness for each function. For example, the well-definedess of Qplus and Qle are provided in QArith as

Instance Qplus_comp : Proper (Qeq==>Qeq==>Qeq) Qplus.
Instance Qle_comp : Proper (Qeq==>Qeq==>iff) Qle.

By defining them as instances of Proper, you can use Generalized rewriting with those functions.