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,
Zgcd (
Qnum q) (
QDen q) = 1%Z ->
Qred q =
q.
Lemma Qred_identity2 :
forall q:Q,
Qred q =
q ->
Zgcd (
Qnum q) (
QDen q) = 1%Z.
Lemma Qred_iff :
forall q:Q,
Qred q =
q <->
Zgcd (
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:
Theorem Qc_eq_dec :
forall x y:Qc, {
x=y} + {
x<>y}.
The addition, multiplication and opposite are defined
in the straightforward way:
Definition Qcplus (
x y :
Qc) := !!(x+y).
Infix "+" :=
Qcplus :
Qc_scope.
Definition Qcmult (
x y :
Qc) := !!(x*y).
Infix "*" :=
Qcmult :
Qc_scope.
Definition Qcopp (
x :
Qc) := !!(-x).
Notation "- x" := (
Qcopp x) :
Qc_scope.
Definition Qcminus (
x y :
Qc) :=
x+-y.
Infix "-" :=
Qcminus :
Qc_scope.
Definition Qcinv (
x :
Qc) := !!(/x).
Notation "/ x" := (
Qcinv x) :
Qc_scope.
Definition Qcdiv (
x y :
Qc) :=
x*/y.
Infix "/" :=
Qcdiv :
Qc_scope.
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.
Lemma Qc_dec :
forall x y, {
x<y} + {
y<x} + {
x=y}.
Lemma Qclt_le_dec :
forall x y, {
x<y} + {
y<=x}.
Compatibility of operations with respect to order.
Rational to the n-th power
Fixpoint Qcpower (
q:Qc)(n:nat) {
struct n } :
Qc :=
match n with
|
O => 1
|
S n =>
q * (
Qcpower q n)
end.
Notation " q ^ n " := (
Qcpower q n) :
Qc_scope.
Lemma Qcpower_1 :
forall n, 1^n = 1.
Lemma Qcpower_0 :
forall n,
n<>O -> 0^n = 0.
Lemma Qcpower_pos :
forall p n, 0 <=
p -> 0 <=
p^n.
And now everything is easier concerning tactics:
A ring tactic for rational numbers
A field tactic for rational numbers