0
$\begingroup$

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.


$\endgroup$
1

1 Answer 1

1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.