Library Coq.QArith.Qreals
Injection of rational numbers into real numbers.
Definition Q2R (
x :
Q) :
R := (
IZR (
Qnum x)
* / IZR (
QDen x))%
R.
Lemma IZR_nz :
forall p :
positive,
IZR (
Zpos p)
<> 0%
R.
Hint Resolve IZR_nz Rmult_integral_contrapositive.
Lemma eqR_Qeq :
forall x y :
Q,
Q2R x = Q2R y ->
x==y.
Lemma Qeq_eqR :
forall x y :
Q,
x==y ->
Q2R x = Q2R y.
Lemma Rle_Qle :
forall x y :
Q, (
Q2R x <= Q2R y)%
R ->
x<=y.
Lemma Qle_Rle :
forall x y :
Q,
x<=y -> (
Q2R x <= Q2R y)%
R.
Lemma Rlt_Qlt :
forall x y :
Q, (
Q2R x < Q2R y)%
R ->
x<y.
Lemma Qlt_Rlt :
forall x y :
Q,
x<y -> (
Q2R x < Q2R y)%
R.
Lemma Q2R_plus :
forall x y :
Q,
Q2R (
x+y)
= (
Q2R x + Q2R y)%
R.
Lemma Q2R_mult :
forall x y :
Q,
Q2R (
x*y)
= (
Q2R x * Q2R y)%
R.
Lemma Q2R_opp :
forall x :
Q,
Q2R (
- x)
= (
- Q2R x)%
R.
Lemma Q2R_minus :
forall x y :
Q,
Q2R (
x-y)
= (
Q2R x - Q2R y)%
R.
Lemma Q2R_inv :
forall x :
Q,
~ x==0 ->
Q2R (
/x)
= (
/ Q2R x)%
R.
Lemma Q2R_div :
forall x y :
Q,
~ y==0 ->
Q2R (
x/y)
= (
Q2R x / Q2R y)%
R.
Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div :
q2r_simpl.
Section LegacyQField.
In the past, the field tactic was not able to deal with setoid datatypes,
so translating from Q to R and applying field on reals was a workaround.
See now Qfield for a direct field tactic on Q.
Ltac QField :=
apply eqR_Qeq;
autorewrite with q2r_simpl;
try field;
auto.
Examples of use: