<p>You can't do that.</p>
<p>You can actually define a function which doesn't respect Q's setoid structure.</p>
<pre><code>Require Import QArith.

Goal exists (f : Q -&gt; Q) (x y : Q), x == y /\ ~(f x == f y).
Proof.
  exists (fun q =&gt; Qmake (Qnum q) 1).
  exists (Qmake 2 1), (Qmake 4 2).
  split.
  - reflexivity.
  - discriminate.
Qed.
</code></pre>
<p>You have to prove the well-definedness for each function.
For example, the well-definedess of Qplus and Qle are provided in QArith as</p>
<pre><code>Instance Qplus_comp : Proper (Qeq==&gt;Qeq==&gt;Qeq) Qplus.
Instance Qle_comp : Proper (Qeq==&gt;Qeq==&gt;iff) Qle.
</code></pre>
<p>By defining them as instances of <code>Proper</code>, you can use <a href="https://coq.inria.fr/refman/addendum/generalized-rewriting.html" rel="nofollow noreferrer">Generalized rewriting</a> with those functions.</p>

CC BY-SA 4.0
2022-07-10T02:19:38.930Z
2022-07-10T02:34:51.493Z
2022-07-10T02:34:51.493Z
Kazuhiro Kobayashi
<p>I want to prove the following Coq theorem.
However, I couldn't proceed.
Please, give me an advice if possible.
Thank you.</p>
<hr />
<p>Require Import QArith.</p>
<p>Variable f : Q -&gt; Q.</p>
<p>Theorem function (x y : Q) :
x == y -&gt; f x == f y.</p>
<p>Proof.</p>
<hr />

CC BY-SA 4.0
2022-07-10T08:18:58.113Z
Are you aware of https://proofassistants.stackexchange.com?
Andrej Bauer
<coq>
A Coq question : How to prove the image of the two same valued variables under a function are same?
with-forest
# A Coq question : How to prove the image of the two same valued variables under a function are same?

(Asked by: username_0 on 2022-07-10)

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.

---

**Tags:** coq
> **Comments:**
> **username_1**: Are you aware of https://proofassistants.stackexchange.com?  

---

## 1 answers

### Answer by username_2 on 2022-07-10. Score: 1 | Accepted answer

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.


---

