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:
Let ex1 :
forall x y z :
Q, (
x+y)*z == (
x*z)+(y*z).
Qed.
Let ex2 :
forall x y :
Q, ~
y==0 -> (
x/y)*y ==
x.
Qed.
End LegacyQField.