# Library Coq.QArith.Qcanon

Require Import Field.
Require Import QArith.
Require Import Znumtheory.
Require Import Eqdep_dec.
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
Lemma Q_apart_0_1 : 1 <> 0.
Ltac qc := match goal with
| q:Qc |- _ => destruct q; qc
| _ => apply Qc_is_canon; simpl; repeat rewrite Qred_correct
end.
Opaque Qred.
Addition is associative:
Theorem Qcplus_assoc : forall x y z, x +( y + z ) = ( x + y )+ z.
0 is a neutral element for addition:
Lemma Qcplus_0_l : forall x, 0+ x = x.
Lemma Qcplus_0_r : forall x, x +0 = x.
Commutativity of addition:
Theorem Qcplus_comm : forall x y, x + y = y + x.
Properties of Qopp
Lemma Qcopp_involutive : forall q, - - q = q.
Theorem Qcplus_opp_r : forall q, q +( - q ) = 0.
Multiplication is associative:
Theorem Qcmult_assoc : forall n m p, n *( m * p ) = ( n * m )* p.
1 is a neutral element for multiplication:
Lemma Qcmult_1_l : forall n, 1* n = n.
Theorem Qcmult_1_r : forall n, n *1= n.
Commutativity of multiplication
Theorem Qcmult_comm : forall x y, x * y = y * x.
Distributivity
Theorem Qcmult_plus_distr_r : forall x y z, x *( y + z ) = ( x * y )+( x * z ).
Theorem Qcmult_plus_distr_l : forall x y z, ( x + y )* z = ( x * z )+( y * z ).
Integrality
Theorem Qcmult_integral : forall x y, x * y =0 -> x =0 \/ y =0.
Theorem Qcmult_integral_l : forall x y, ~ x = 0 -> x * y = 0 -> y = 0.
Inverse and division.
Theorem Qcmult_inv_r : forall x, x <>0 -> x *( / x ) = 1.
Theorem Qcmult_inv_l : forall x, x <>0 -> ( / x )* x = 1.
Lemma Qcinv_mult_distr : forall p q, / ( p * q ) = / p * / q.
Theorem Qcdiv_mult_l : forall x y, y <>0 -> ( x * y )/ y = x.
Theorem Qcmult_div_r : forall x y, ~ y = 0 -> y *( x / y ) = x.
Properties of order upon Q.
Lemma Qcle_refl : forall x, x <= x.
Lemma Qcle_antisym : forall x y, x <= y -> y <= x -> x = y.
Lemma Qcle_trans : forall x y z, x <= y -> y <= z -> x <= z.
Lemma Qclt_not_eq : forall x y, x < y -> x <> y.
Large = strict or equal
Lemma Qclt_le_weak : forall x y, x < y -> x <= y.
Lemma Qcle_lt_trans : forall x y z, x <= y -> y < z -> x < z.
Lemma Qclt_le_trans : forall x y z, x < y -> y <= z -> x < z.
Lemma Qclt_trans : forall x y z, x < y -> y < z -> x < z.
x<y iff ~(y<=x)
Lemma Qcnot_lt_le : forall x y, ~ x < y -> y <= x.
Lemma Qcnot_le_lt : forall x y, ~ x <= y -> y < x.
Lemma Qclt_not_le : forall x y, x < y -> ~ y <= x.
Lemma Qcle_not_lt : forall x y, x <= y -> ~ y < x.
Lemma Qcle_lt_or_eq : forall x y, x <= y -> x < y \/ x == y.
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.
Lemma Qcopp_le_compat : forall p q, p <= q -> - q <= - p.
Lemma Qcle_minus_iff : forall p q, p <= q <-> 0 <= q + - p.
Lemma Qclt_minus_iff : forall p q, p < q <-> 0 < q + - p.
Lemma Qcplus_le_compat :
forall x y z t, x <= y -> z <= t -> x + z <= y + t.
Lemma Qcmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x * z <= y * z.
Lemma Qcmult_lt_0_le_reg_r : forall x y z, 0 < z -> x * z <= y * z -> x <= y.
Lemma Qcmult_lt_compat_r : forall x y z, 0 < z -> x < y -> x * z < y * z.
Rational to the n-th power
Fixpoint Qcpower (q:Qc)(n:nat) : 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
Definition Qc_eq_bool (x y : Qc) :=
if Qc_eq_dec x y then true else false.
Lemma Qc_eq_bool_correct : forall x y : Qc, Qc_eq_bool x y = true -> x = y.
Definition Qcrt : ring_theory 0 1 Qcplus Qcmult Qcminus Qcopp (eq(A:=Qc)).
Definition Qcft :
field_theory 0%Qc 1%Qc Qcplus Qcmult Qcminus Qcopp Qcdiv Qcinv (eq(A:=Qc)).
Add Field Qcfield : Qcft.
A field tactic for rational numbers
Example test_field : (forall x y : Qc, y <>0 -> ( x / y )* y = x)%Qc.
Qed.
Theorem Qc_decomp: forall x y: Qc,
(Qred x = x -> Qred y = y -> ( x:Q ) = y)-> x = y.