Library Coq.QArith.Qcanon
Qc : A canonical representation of rational numbers.
based on the setoid representation Q.
Record Qc :
Set :=
Qcmake {
this :>
Q ;
canon :
Qred this = this }.
Delimit Scope Qc_scope with Qc.
Open Scope Qc_scope.
Lemma Qred_identity :
forall q:
Q,
Z.gcd (
Qnum q) (
QDen q)
= 1%
Z ->
Qred q = q.
Lemma Qred_identity2 :
forall q:
Q,
Qred q = q ->
Z.gcd (
Qnum q) (
QDen q)
= 1%
Z.
Lemma Qred_iff :
forall q:
Q,
Qred q = q <-> Z.gcd (
Qnum q) (
QDen q)
= 1%
Z.
Lemma Qred_involutive :
forall q:
Q,
Qred (
Qred q)
= Qred q.
Definition Q2Qc (
q:
Q) :
Qc :=
Qcmake (
Qred q) (
Qred_involutive q).
Notation " !! " :=
Q2Qc :
Qc_scope.
Lemma Qc_is_canon :
forall q q' :
Qc,
q == q' ->
q = q'.
Hint Resolve Qc_is_canon.
Notation " 0 " := (
!!0) :
Qc_scope.
Notation " 1 " := (
!!1) :
Qc_scope.
Definition Qcle (
x y :
Qc) := (
x <= y)%
Q.
Definition Qclt (
x y :
Qc) := (
x < y)%
Q.
Notation Qcgt := (
fun x y :
Qc =>
Qlt y x).
Notation Qcge := (
fun x y :
Qc =>
Qle y x).
Infix "<" :=
Qclt :
Qc_scope.
Infix "<=" :=
Qcle :
Qc_scope.
Infix ">" :=
Qcgt :
Qc_scope.
Infix ">=" :=
Qcge :
Qc_scope.
Notation "x <= y <= z" := (
x<=y/\y<=z) :
Qc_scope.
Notation "x < y < z" := (
x<y/\y<z) :
Qc_scope.
Definition Qccompare (
p q :
Qc) := (
Qcompare p q).
Notation "p ?= q" := (
Qccompare p q) :
Qc_scope.
Lemma Qceq_alt :
forall p q,
(p = q) <-> (p ?= q) = Eq.
Lemma Qclt_alt :
forall p q,
(p<q) <-> (p?=q = Lt).
Lemma Qcgt_alt :
forall p q,
(p>q) <-> (p?=q = Gt).
Lemma Qle_alt :
forall p q,
(p<=q) <-> (p?=q <> Gt).
Lemma Qge_alt :
forall p q,
(p>=q) <-> (p?=q <> Lt).
equality on Qc is decidable:
The addition, multiplication and opposite are defined
in the straightforward way:
0 and 1 are apart
Addition is associative:
0 is a neutral element for addition:
Commutativity of addition:
Properties of Qopp
Multiplication is associative:
1 is a neutral element for multiplication:
Commutativity of multiplication
Distributivity
Integrality
Inverse and division.
Properties of order upon Q.
Large = strict or equal
x<y iff ~(y<=x)
Some decidability results about orders.
Compatibility of operations with respect to order.
Rational to the n-th power
And now everything is easier concerning tactics:
A ring tactic for rational numbers
A field tactic for rational numbers