Qcanon.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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 }.

Declare Scope Qc_scope.
Delimit Scope Qc_scope with Qc.
Bind Scope Qc_scope with Qc.
Arguments Qcmake this%Q _.
Open Scope Qc_scope.

An alternative statement of Qred q = q via Z.gcd

Lemma Qred_identity :
  forall q:Q, Z.gcd (Qnum q) (QDen q) = 1%Z -> Qred q = q.forall q : Q,
Z.gcd (Qnum q) (QDen q) = 1 -> Qred q = q
Proof.forall q : Q,
Z.gcd (Qnum q) (QDen q) = 1 -> Qred q = q
  intros (a,b) H; simpl in *.a:Z
b:positive
H:Z.gcd a (Z.pos b) = 1
(let (r1, r2) := snd (Z.ggcd a (Z.pos b)) in
 r1 # Z.to_pos r2) = a # b
  rewrite <- Z.ggcd_gcd in H.a:Z
b:positive
H:fst (Z.ggcd a (Z.pos b)) = 1
(let (r1, r2) := snd (Z.ggcd a (Z.pos b)) in
 r1 # Z.to_pos r2) = a # b
  generalize (Z.ggcd_correct_divisors a (Zpos b)).a:Z
b:positive
H:fst (Z.ggcd a (Z.pos b)) = 1
(let
 '(g, (aa, bb)) := Z.ggcd a (Z.pos b) in
  a = g * aa /\ Z.pos b = g * bb) ->
(let (r1, r2) := snd (Z.ggcd a (Z.pos b)) in
 r1 # Z.to_pos r2) = a # b
  destruct Z.ggcd as (g,(aa,bb)); simpl in *; subst.a:Z
b:positive
aa, bb:Z
a = 1 * aa /\ Z.pos b = 1 * bb ->
aa # Z.to_pos bb = a # b
  rewrite !Z.mul_1_l.a:Z
b:positive
aa, bb:Z
a = aa /\ Z.pos b = bb -> aa # Z.to_pos bb = a # b now intros (<-,<-).
Qed.

Lemma Qred_identity2 :
  forall q:Q, Qred q = q -> Z.gcd (Qnum q) (QDen q) = 1%Z.forall q : Q,
Qred q = q -> Z.gcd (Qnum q) (QDen q) = 1
Proof.forall q : Q,
Qred q = q -> Z.gcd (Qnum q) (QDen q) = 1
  intros (a,b) H; simpl in *.a:Z
b:positive
H:(let (r1, r2) := snd (Z.ggcd a (Z.pos b)) in
 r1 # Z.to_pos r2) = a # b
Z.gcd a (Z.pos b) = 1
  generalize (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)).a:Z
b:positive
H:(let (r1, r2) := snd (Z.ggcd a (Z.pos b)) in
 r1 # Z.to_pos r2) = a # b
0 <= Z.gcd a (Z.pos b) ->
(let
 '(g, (aa, bb)) := Z.ggcd a (Z.pos b) in
  a = g * aa /\ Z.pos b = g * bb) ->
Z.gcd a (Z.pos b) = 1
  rewrite <- Z.ggcd_gcd.a:Z
b:positive
H:(let (r1, r2) := snd (Z.ggcd a (Z.pos b)) in
 r1 # Z.to_pos r2) = a # b
0 <= fst (Z.ggcd a (Z.pos b)) ->
(let
 '(g, (aa, bb)) := Z.ggcd a (Z.pos b) in
  a = g * aa /\ Z.pos b = g * bb) ->
fst (Z.ggcd a (Z.pos b)) = 1
  destruct Z.ggcd as (g,(aa,bb)); simpl in *.a:Z
b:positive
g, aa, bb:Z
H:aa # Z.to_pos bb = a # b
0 <= g -> a = g * aa /\ Z.pos b = g * bb -> g = 1
  injection H as <- <-.g, aa, bb:Z
0 <= g ->
aa = g * aa /\ Z.pos (Z.to_pos bb) = g * bb -> g = 1 intros H (_,H').g, aa, bb:Z
H:0 <= g
H':Z.pos (Z.to_pos bb) = g * bb
g = 1
  destruct g as [|g|g]; [ discriminate | | now elim H ].g:positive
aa, bb:Z
H:0 <= Z.pos g
H':Z.pos (Z.to_pos bb) = Z.pos g * bb
Z.pos g = 1
  destruct bb as [|b|b]; simpl in *; try discriminate.g:positive
aa:Z
b:positive
H:0 <= Z.pos g
H':Z.pos b = Z.pos (g * b)
Z.pos g = 1
  injection H' as H'.g:positive
aa:Z
b:positive
H:0 <= Z.pos g
H':b = (g * b)%positive
Z.pos g = 1 f_equal.g:positive
aa:Z
b:positive
H:0 <= Z.pos g
H':b = (g * b)%positive
g = 1%positive
  apply Pos.mul_reg_r with b.g:positive
aa:Z
b:positive
H:0 <= Z.pos g
H':b = (g * b)%positive
(g * b)%positive = (1 * b)%positive now rewrite Pos.mul_1_l.
Qed.

Lemma Qred_iff : forall q:Q, Qred q = q <-> Z.gcd (Qnum q) (QDen q) = 1%Z.forall q : Q,
Qred q = q <-> Z.gcd (Qnum q) (QDen q) = 1
Proof.forall q : Q,
Qred q = q <-> Z.gcd (Qnum q) (QDen q) = 1
  split; intros.q:Q
H:Qred q = q
Z.gcd (Qnum q) (QDen q) = 1
q:Q
H:Z.gcd (Qnum q) (QDen q) = 1
Qred q = q
  apply Qred_identity2; auto.q:Q
H:Z.gcd (Qnum q) (QDen q) = 1
Qred q = q
  apply Qred_identity; auto.
Qed.

Coercion from Qc to Q and equality

Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'.forall q q' : Qc, q == q' -> q = q'
Proof.forall q q' : Qc, q == q' -> q = q'
  intros (q,hq) (q',hq') H.q:Q
hq:Qred q = q
q':Q
hq':Qred q' = q'
H:{| this := q; canon := hq |} ==
{| this := q'; canon := hq' |}
{| this := q; canon := hq |} =
{| this := q'; canon := hq' |} simpl in *.q:Q
hq:Qred q = q
q':Q
hq':Qred q' = q'
H:q == q'
{| this := q; canon := hq |} =
{| this := q'; canon := hq' |}
  assert (H' := Qred_complete _ _ H).q:Q
hq:Qred q = q
q':Q
hq':Qred q' = q'
H:q == q'
H':Qred q = Qred q'
{| this := q; canon := hq |} =
{| this := q'; canon := hq' |}
  rewrite hq, hq' in H'.q:Q
hq:Qred q = q
q':Q
hq':Qred q' = q'
H:q == q'
H':q = q'
{| this := q; canon := hq |} =
{| this := q'; canon := hq' |} subst q'.q:Q
hq:Qred q = q
H:q == q
hq':Qred q = q
{| this := q; canon := hq |} =
{| this := q; canon := hq' |} f_equal.q:Q
hq:Qred q = q
H:q == q
hq':Qred q = q
hq = hq'
  apply eq_proofs_unicity.q:Q
hq:Qred q = q
H:q == q
hq':Qred q = q
forall x y : Q, x = y \/ x <> y intros.q:Q
hq:Qred q = q
H:q == q
hq':Qred q = q
x, y:Q
x = y \/ x <> y  repeat decide equality.
Qed.
Hint Resolve Qc_is_canon : core.

Theorem Qc_decomp: forall q q': Qc, (q:Q) = q' -> q = q'.forall q q' : Qc, (q : Q) = q' -> q = q'
Proof.forall q q' : Qc, (q : Q) = q' -> q = q'
  intros.q, q':Qc
H:(q : Q) = q'
q = q' apply Qc_is_canon.q, q':Qc
H:(q : Q) = q'
q == q' now rewrite H.
Qed.

Q2Qc : a conversion from Q to Qc.

Lemma Qred_involutive : forall q:Q, Qred (Qred q) = Qred q.forall q : Q, Qred (Qred q) = Qred q
Proof.forall q : Q, Qred (Qred q) = Qred q
  intros; apply Qred_complete.q:Q
Qred q == q
  apply Qred_correct.
Qed.

Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q).
Arguments Q2Qc q%Q.

Lemma Q2Qc_eq_iff (q q' : Q) : Q2Qc q = Q2Qc q' <-> q == q'.q, q':Q
Q2Qc q = Q2Qc q' <-> q == q'
Proof.q, q':Q
Q2Qc q = Q2Qc q' <-> q == q'
 split; intro H.q, q':Q
H:Q2Qc q = Q2Qc q'
q == q'
q, q':Q
H:q == q'
Q2Qc q = Q2Qc q'
 -q, q':Q
H:Q2Qc q = Q2Qc q'
q == q' now injection H as H%Qred_eq_iff.
 -q, q':Q
H:q == q'
Q2Qc q = Q2Qc q' apply Qc_is_canon.q, q':Q
H:q == q'
Q2Qc q == Q2Qc q' simpl.q, q':Q
H:q == q'
Qred q == Qred q' now rewrite H.
Qed.

Notation " 0 " := (Q2Qc 0) : Qc_scope.
Notation " 1 " := (Q2Qc 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.forall p q : Qc, p = q <-> (p ?= q) = Eq
Proof.forall p q : Qc, p = q <-> (p ?= q) = Eq
  unfold Qccompare.forall p q : Qc, p = q <-> (p ?= q)%Q = Eq
  intros; rewrite <- Qeq_alt.p, q:Qc
p = q <-> p == q
  split; auto.p, q:Qc
p = q -> p == q now intros <-.
Qed.

Lemma Qclt_alt : forall p q, (p<q) <-> (p?=q = Lt).forall p q : Qc, p < q <-> (p ?= q) = Lt
Proof.forall p q : Qc, p < q <-> (p ?= q) = Lt
  intros; exact (Qlt_alt p q).
Qed.

Lemma Qcgt_alt : forall p q, (p>q) <-> (p?=q = Gt).forall p q : Qc,
(fun x0 y0 : Qc => (y0 < x0)%Q) p q <-> (p ?= q) = Gt
Proof.forall p q : Qc,
(fun x0 y0 : Qc => (y0 < x0)%Q) p q <-> (p ?= q) = Gt
  intros; exact (Qgt_alt p q).
Qed.

Lemma Qcle_alt : forall p q, (p<=q) <-> (p?=q <> Gt).forall p q : Qc, p <= q <-> (p ?= q) <> Gt
Proof.forall p q : Qc, p <= q <-> (p ?= q) <> Gt
  intros; exact (Qle_alt p q).
Qed.

Lemma Qcge_alt : forall p q, (p>=q) <-> (p?=q <> Lt).forall p q : Qc,
(fun x0 y0 : Qc => (y0 <= x0)%Q) p q <->
(p ?= q) <> Lt
Proof.forall p q : Qc,
(fun x0 y0 : Qc => (y0 <= x0)%Q) p q <->
(p ?= q) <> Lt
  intros; exact (Qge_alt p q).
Qed.

equality on Qc is decidable:

Theorem Qc_eq_dec : forall x y:Qc, {x=y} + {x<>y}.forall x y : Qc, {x = y} + {x <> y}
Proof.forall x y : Qc, {x = y} + {x <> y}
  intros.x, y:Qc
{x = y} + {x <> y}
  destruct (Qeq_dec x y) as [H|H]; auto.x, y:Qc
H:~ x == y
{x = y} + {x <> y}
  right; contradict H; subst; auto with qarith.
Defined.

The addition, multiplication and opposite are defined in the straightforward way:

Definition Qcplus (x y : Qc) := Q2Qc (x+y).
Infix "+" := Qcplus : Qc_scope.
Definition Qcmult (x y : Qc) := Q2Qc (x*y).
Infix "*" := Qcmult : Qc_scope.
Definition Qcopp (x : Qc) := Q2Qc (-x).
Notation "- x" := (Qcopp x) : Qc_scope.
Definition Qcminus (x y : Qc) := x+-y.
Infix "-" := Qcminus : Qc_scope.
Definition Qcinv (x : Qc) := Q2Qc (/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.1 <> 0
Proof.1 <> 0
  unfold Q2Qc.{| this := Qred 1; canon := Qred_involutive 1 |} <>
{| this := Qred 0; canon := Qred_involutive 0 |}
  intros H; discriminate H.
Qed.

Ltac qc := match goal with
 | q:Qc |- _ => destruct q; qc
 | _ => apply Qc_is_canon; simpl; rewrite !Qred_correct
end.

Opaque Qred.

Addition is associative:

Theorem Qcplus_assoc : forall x y z, x+(y+z)=(x+y)+z.forall x y z : Qc, x + (y + z) = x + y + z
Proof.forall x y z : Qc, x + (y + z) = x + y + z
  intros; qc; apply Qplus_assoc.
Qed.

0 is a neutral element for addition:

Lemma Qcplus_0_l : forall x, 0+x = x.forall x : Qc, 0 + x = x
Proof.forall x : Qc, 0 + x = x
  intros; qc; apply Qplus_0_l.
Qed.

Lemma Qcplus_0_r : forall x, x+0 = x.forall x : Qc, x + 0 = x
Proof.forall x : Qc, x + 0 = x
  intros; qc; apply Qplus_0_r.
Qed.

Commutativity of addition:

Theorem Qcplus_comm : forall x y, x+y = y+x.forall x y : Qc, x + y = y + x
Proof.forall x y : Qc, x + y = y + x
  intros; qc; apply Qplus_comm.
Qed.

Properties of Qopp

Lemma Qcopp_involutive : forall q, - -q = q.forall q : Qc, - - q = q
Proof.forall q : Qc, - - q = q
  intros; qc; apply Qopp_involutive.
Qed.

Theorem Qcplus_opp_r : forall q, q+(-q) = 0.forall q : Qc, q + - q = 0
Proof.forall q : Qc, q + - q = 0
  intros; qc; apply Qplus_opp_r.
Qed.

Multiplication is associative:

Theorem Qcmult_assoc : forall n m p, n*(m*p)=(n*m)*p.forall n m p : Qc, n * (m * p) = n * m * p
Proof.forall n m p : Qc, n * (m * p) = n * m * p
  intros; qc; apply Qmult_assoc.
Qed.

0 is absorbing for multiplication:

Lemma Qcmult_0_l : forall n, 0*n = 0.forall n : Qc, 0 * n = 0
Proof.forall n : Qc, 0 * n = 0
  intros; qc; split.
Qed.

Theorem Qcmult_0_r : forall n, n*0=0.forall n : Qc, n * 0 = 0
Proof.forall n : Qc, n * 0 = 0
  intros; qc; rewrite Qmult_comm; split.
Qed.

1 is a neutral element for multiplication:

Lemma Qcmult_1_l : forall n, 1*n = n.forall n : Qc, 1 * n = n
Proof.forall n : Qc, 1 * n = n
  intros; qc; apply Qmult_1_l.
Qed.

Theorem Qcmult_1_r : forall n, n*1=n.forall n : Qc, n * 1 = n
Proof.forall n : Qc, n * 1 = n
  intros; qc; apply Qmult_1_r.
Qed.

Commutativity of multiplication

Theorem Qcmult_comm : forall x y, x*y=y*x.forall x y : Qc, x * y = y * x
Proof.forall x y : Qc, x * y = y * x
  intros; qc; apply Qmult_comm.
Qed.

Distributivity

Theorem Qcmult_plus_distr_r : forall x y z, x*(y+z)=(x*y)+(x*z).forall x y z : Qc, x * (y + z) = x * y + x * z
Proof.forall x y z : Qc, x * (y + z) = x * y + x * z
  intros; qc; apply Qmult_plus_distr_r.
Qed.

Theorem Qcmult_plus_distr_l : forall x y z, (x+y)*z=(x*z)+(y*z).forall x y z : Qc, (x + y) * z = x * z + y * z
Proof.forall x y z : Qc, (x + y) * z = x * z + y * z
  intros; qc; apply Qmult_plus_distr_l.
Qed.

Integrality

Theorem Qcmult_integral : forall x y, x*y=0 -> x=0 \/ y=0.forall x y : Qc, x * y = 0 -> x = 0 \/ y = 0
Proof.forall x y : Qc, x * y = 0 -> x = 0 \/ y = 0
  intros.x, y:Qc
H:x * y = 0
x = 0 \/ y = 0
  destruct (Qmult_integral x y); try qc; auto.x, y:Qc
H:x * y = 0
x * y == 0
  injection H as H.x, y:Qc
H:Qred (x * y) = Qred 0
x * y == 0
  rewrite <- (Qred_correct (x*y)).x, y:Qc
H:Qred (x * y) = Qred 0
Qred (x * y) == 0
  rewrite <- (Qred_correct 0).x, y:Qc
H:Qred (x * y) = Qred 0
Qred (x * y) == Qred 0
  rewrite H; auto with qarith.
Qed.

Theorem Qcmult_integral_l : forall x y, ~ x = 0 -> x*y = 0 -> y = 0.forall x y : Qc, x <> 0 -> x * y = 0 -> y = 0
Proof.forall x y : Qc, x <> 0 -> x * y = 0 -> y = 0
  intros; destruct (Qcmult_integral _ _ H0); tauto.
Qed.

Inverse and division.

Theorem Qcmult_inv_r : forall x, x<>0 -> x*(/x) = 1.forall x : Qc, x <> 0 -> x * / x = 1
Proof.forall x : Qc, x <> 0 -> x * / x = 1
  intros; qc; apply Qmult_inv_r; auto.
Qed.

Theorem Qcmult_inv_l : forall x, x<>0 -> (/x)*x = 1.forall x : Qc, x <> 0 -> / x * x = 1
Proof.forall x : Qc, x <> 0 -> / x * x = 1
  intros.x:Qc
H:x <> 0
/ x * x = 1
  rewrite Qcmult_comm.x:Qc
H:x <> 0
x * / x = 1
  apply Qcmult_inv_r; auto.
Qed.

Lemma Qcinv_mult_distr : forall p q, / (p * q) = /p * /q.forall p q : Qc, / (p * q) = / p * / q
Proof.forall p q : Qc, / (p * q) = / p * / q
  intros; qc; apply Qinv_mult_distr.
Qed.

Theorem Qcdiv_mult_l : forall x y, y<>0 -> (x*y)/y = x.forall x y : Qc, y <> 0 -> x * y / y = x
Proof.forall x y : Qc, y <> 0 -> x * y / y = x
  unfold Qcdiv.forall x y : Qc, y <> 0 -> x * y * / y = x
  intros.x, y:Qc
H:y <> 0
x * y * / y = x
  rewrite <- Qcmult_assoc.x, y:Qc
H:y <> 0
x * (y * / y) = x
  rewrite Qcmult_inv_r; auto.x, y:Qc
H:y <> 0
x * 1 = x
  apply Qcmult_1_r.
Qed.

Theorem Qcmult_div_r : forall x y, ~ y = 0 -> y*(x/y) = x.forall x y : Qc, y <> 0 -> y * (x / y) = x
Proof.forall x y : Qc, y <> 0 -> y * (x / y) = x
  unfold Qcdiv.forall x y : Qc, y <> 0 -> y * (x * / y) = x
  intros.x, y:Qc
H:y <> 0
y * (x * / y) = x
  rewrite Qcmult_assoc.x, y:Qc
H:y <> 0
y * x * / y = x
  rewrite Qcmult_comm.x, y:Qc
H:y <> 0
/ y * (y * x) = x
  rewrite Qcmult_assoc.x, y:Qc
H:y <> 0
/ y * y * x = x
  rewrite Qcmult_inv_l; auto.x, y:Qc
H:y <> 0
1 * x = x
  apply Qcmult_1_l.
Qed.

Properties of order upon Qc.

Lemma Qcle_refl : forall x, x<=x.forall x : Qc, x <= x
Proof.forall x : Qc, x <= x
  unfold Qcle; intros; simpl; apply Qle_refl.
Qed.

Lemma Qcle_antisym : forall x y, x<=y -> y<=x -> x=y.forall x y : Qc, x <= y -> y <= x -> x = y
Proof.forall x y : Qc, x <= y -> y <= x -> x = y
  unfold Qcle; intros; simpl in *.x, y:Qc
H:(x <= y)%Q
H0:(y <= x)%Q
x = y
  apply Qc_is_canon; apply Qle_antisym; auto.
Qed.

Lemma Qcle_trans : forall x y z, x<=y -> y<=z -> x<=z.forall x y z : Qc, x <= y -> y <= z -> x <= z
Proof.forall x y z : Qc, x <= y -> y <= z -> x <= z
  unfold Qcle; intros; eapply Qle_trans; eauto.
Qed.

Lemma Qclt_not_eq : forall x y, x<y -> x<>y.forall x y : Qc, x < y -> x <> y
Proof.forall x y : Qc, x < y -> x <> y
  unfold Qclt; intros; simpl in *.x, y:Qc
H:(x < y)%Q
x <> y
  intro; destruct (Qlt_not_eq _ _ H).x, y:Qc
H:(x < y)%Q
H0:x = y
x == y
  subst; auto with qarith.
Qed.

Large = strict or equal

Lemma Qclt_le_weak : forall x y, x<y -> x<=y.forall x y : Qc, x < y -> x <= y
Proof.forall x y : Qc, x < y -> x <= y
  unfold Qcle, Qclt; intros; apply Qlt_le_weak; auto.
Qed.

Lemma Qcle_lt_trans : forall x y z, x<=y -> y<z -> x<z.forall x y z : Qc, x <= y -> y < z -> x < z
Proof.forall x y z : Qc, x <= y -> y < z -> x < z
  unfold Qcle, Qclt; intros; eapply Qle_lt_trans; eauto.
Qed.

Lemma Qclt_le_trans : forall x y z, x<y -> y<=z -> x<z.forall x y z : Qc, x < y -> y <= z -> x < z
Proof.forall x y z : Qc, x < y -> y <= z -> x < z
  unfold Qcle, Qclt; intros; eapply Qlt_le_trans; eauto.
Qed.

Lemma Qclt_trans : forall x y z, x<y -> y<z -> x<z.forall x y z : Qc, x < y -> y < z -> x < z
Proof.forall x y z : Qc, x < y -> y < z -> x < z
  unfold Qclt; intros; eapply Qlt_trans; eauto.
Qed.

x<y iff ~(y≤x)

Lemma Qcnot_lt_le : forall x y, ~ x<y -> y<=x.forall x y : Qc, ~ x < y -> y <= x
Proof.forall x y : Qc, ~ x < y -> y <= x
  unfold Qcle, Qclt; intros; apply Qnot_lt_le; auto.
Qed.

Lemma Qcnot_le_lt : forall x y, ~ x<=y -> y<x.forall x y : Qc, ~ x <= y -> y < x
Proof.forall x y : Qc, ~ x <= y -> y < x
  unfold Qcle, Qclt; intros; apply Qnot_le_lt; auto.
Qed.

Lemma Qclt_not_le : forall x y, x<y -> ~ y<=x.forall x y : Qc, x < y -> ~ y <= x
Proof.forall x y : Qc, x < y -> ~ y <= x
  unfold Qcle, Qclt; intros; apply Qlt_not_le; auto.
Qed.

Lemma Qcle_not_lt : forall x y, x<=y -> ~ y<x.forall x y : Qc, x <= y -> ~ y < x
Proof.forall x y : Qc, x <= y -> ~ y < x
  unfold Qcle, Qclt; intros; apply Qle_not_lt; auto.
Qed.

Lemma Qcle_lt_or_eq : forall x y, x<=y -> x<y \/ x=y.forall x y : Qc, x <= y -> x < y \/ x = y
Proof.forall x y : Qc, x <= y -> x < y \/ x = y
  unfold Qcle, Qclt; intros x y H.x, y:Qc
H:(x <= y)%Q
(x < y)%Q \/ x = y
  destruct (Qle_lt_or_eq _ _ H); [left|right]; trivial.x, y:Qc
H:(x <= y)%Q
H0:x == y
x = y
  now apply Qc_is_canon.
Qed.

Some decidability results about orders.

Lemma Qc_dec : forall x y, {x<y} + {y<x} + {x=y}.forall x y : Qc, {x < y} + {y < x} + {x = y}
Proof.forall x y : Qc, {x < y} + {y < x} + {x = y}
  unfold Qclt, Qcle; intros.x, y:Qc
{(x < y)%Q} + {(y < x)%Q} + {x = y}
  destruct (Q_dec x y) as [H|H].x, y:Qc
H:{(x < y)%Q} + {(y < x)%Q}
{(x < y)%Q} + {(y < x)%Q} + {x = y}
x, y:Qc
H:x == y
{(x < y)%Q} + {(y < x)%Q} + {x = y}
  left; auto.x, y:Qc
H:x == y
{(x < y)%Q} + {(y < x)%Q} + {x = y}
  right; apply Qc_is_canon; auto.
Defined.

Lemma Qclt_le_dec : forall x y, {x<y} + {y<=x}.forall x y : Qc, {x < y} + {y <= x}
Proof.forall x y : Qc, {x < y} + {y <= x}
  unfold Qclt, Qcle; intros; apply Qlt_le_dec; auto.
Defined.

Compatibility of operations with respect to order.

Lemma Qcopp_le_compat : forall p q, p<=q -> -q <= -p.forall p q : Qc, p <= q -> - q <= - p
Proof.forall p q : Qc, p <= q -> - q <= - p
  unfold Qcle, Qcopp; intros; simpl in *.p, q:Qc
H:(p <= q)%Q
(Qred (- q) <= Qred (- p))%Q
  repeat rewrite Qred_correct.p, q:Qc
H:(p <= q)%Q
(- q <= - p)%Q
  apply Qopp_le_compat; auto.
Qed.

Lemma Qcle_minus_iff : forall p q, p <= q <-> 0 <= q+-p.forall p q : Qc, p <= q <-> 0 <= q + - p
Proof.forall p q : Qc, p <= q <-> 0 <= q + - p
  unfold Qcle, Qcminus; intros; simpl in *.p, q:Qc
(p <= q)%Q <-> (Qred 0 <= Qred (q + Qred (- p)))%Q
  repeat rewrite Qred_correct.p, q:Qc
(p <= q)%Q <-> (0 <= q + - p)%Q
  apply Qle_minus_iff; auto.
Qed.

Lemma Qclt_minus_iff : forall p q, p < q <-> 0 < q+-p.forall p q : Qc, p < q <-> 0 < q + - p
Proof.forall p q : Qc, p < q <-> 0 < q + - p
  unfold Qclt, Qcplus, Qcopp; intros; simpl in *.p, q:Qc
(p < q)%Q <-> (Qred 0 < Qred (q + Qred (- p)))%Q
  repeat rewrite Qred_correct.p, q:Qc
(p < q)%Q <-> (0 < q + - p)%Q
  apply Qlt_minus_iff; auto.
Qed.

Lemma Qcplus_le_compat :
  forall x y z t, x<=y -> z<=t -> x+z <= y+t.forall x y z t : Qc,
x <= y -> z <= t -> x + z <= y + t
Proof.forall x y z t : Qc,
x <= y -> z <= t -> x + z <= y + t
  unfold Qcplus, Qcle; intros; simpl in *.x, y, z, t:Qc
H:(x <= y)%Q
H0:(z <= t)%Q
(Qred (x + z) <= Qred (y + t))%Q
  repeat rewrite Qred_correct.x, y, z, t:Qc
H:(x <= y)%Q
H0:(z <= t)%Q
(x + z <= y + t)%Q
  apply Qplus_le_compat; auto.
Qed.

Lemma Qcmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z.forall x y z : Qc, x <= y -> 0 <= z -> x * z <= y * z
Proof.forall x y z : Qc, x <= y -> 0 <= z -> x * z <= y * z
  unfold Qcmult, Qcle; intros; simpl in *.x, y, z:Qc
H:(x <= y)%Q
H0:(Qred 0 <= z)%Q
(Qred (x * z) <= Qred (y * z))%Q
  repeat rewrite Qred_correct.x, y, z:Qc
H:(x <= y)%Q
H0:(Qred 0 <= z)%Q
(x * z <= y * z)%Q
  apply Qmult_le_compat_r; auto.
Qed.

Lemma Qcmult_lt_0_le_reg_r : forall x y z, 0 <  z  -> x*z <= y*z -> x <= y.forall x y z : Qc, 0 < z -> x * z <= y * z -> x <= y
Proof.forall x y z : Qc, 0 < z -> x * z <= y * z -> x <= y
  unfold Qcmult, Qcle, Qclt; intros; simpl in *.x, y, z:Qc
H:(Qred 0 < z)%Q
H0:(Qred (x * z) <= Qred (y * z))%Q
(x <= y)%Q
  rewrite !Qred_correct in * |-.x, y, z:Qc
H:(0 < z)%Q
H0:(x * z <= y * z)%Q
(x <= y)%Q
  eapply Qmult_lt_0_le_reg_r; eauto.
Qed.

Lemma Qcmult_lt_compat_r : forall x y z, 0 < z  -> x < y -> x*z < y*z.forall x y z : Qc, 0 < z -> x < y -> x * z < y * z
Proof.forall x y z : Qc, 0 < z -> x < y -> x * z < y * z
  unfold Qcmult, Qclt; intros; simpl in *.x, y, z:Qc
H:(Qred 0 < z)%Q
H0:(x < y)%Q
(Qred (x * z) < Qred (y * z))%Q
  rewrite !Qred_correct in *.x, y, z:Qc
H:(0 < z)%Q
H0:(x < y)%Q
(x * z < y * z)%Q
  eapply Qmult_lt_compat_r; eauto.
Qed.

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.forall n : nat, 1 ^ n = 1
Proof.forall n : nat, 1 ^ n = 1
  induction n; simpl; auto with qarith.n:nat
IHn:1 ^ n = 1
1 * 1 ^ n = 1
  rewrite IHn; auto with qarith.
Qed.

Lemma Qcpower_0 : forall n, n<>O -> 0^n = 0.forall n : nat, n <> 0%nat -> 0 ^ n = 0
Proof.forall n : nat, n <> 0%nat -> 0 ^ n = 0
  destruct n; simpl.0%nat <> 0%nat -> 1 = 0
n:nat
S n <> 0%nat -> 0 * 0 ^ n = 0
  destruct 1; auto.n:nat
S n <> 0%nat -> 0 * 0 ^ n = 0
  intros.n:nat
H:S n <> 0%nat
0 * 0 ^ n = 0
  now apply Qc_is_canon.
Qed.

Lemma Qcpower_pos : forall p n, 0 <= p -> 0 <= p^n.forall (p : Qc) (n : nat), 0 <= p -> 0 <= p ^ n
Proof.forall (p : Qc) (n : nat), 0 <= p -> 0 <= p ^ n
  induction n; simpl; auto with qarith.p:Qc
0 <= p -> 0 <= 1
p:Qc
n:nat
IHn:0 <= p -> 0 <= p ^ n
0 <= p -> 0 <= p * p ^ n
  easy.p:Qc
n:nat
IHn:0 <= p -> 0 <= p ^ n
0 <= p -> 0 <= p * p ^ n
  intros.p:Qc
n:nat
IHn:0 <= p -> 0 <= p ^ n
H:0 <= p
0 <= p * p ^ n
  apply Qcle_trans with (0*(p^n)).p:Qc
n:nat
IHn:0 <= p -> 0 <= p ^ n
H:0 <= p
0 <= 0 * p ^ n
p:Qc
n:nat
IHn:0 <= p -> 0 <= p ^ n
H:0 <= p
0 * p ^ n <= p * p ^ n
  easy.p:Qc
n:nat
IHn:0 <= p -> 0 <= p ^ n
H:0 <= p
0 * p ^ n <= p * p ^ n
  apply Qcmult_le_compat_r; auto.
Qed.

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.forall x y : Qc, Qc_eq_bool x y = true -> x = y
Proof.forall x y : Qc, Qc_eq_bool x y = true -> x = y
  intros x y; unfold Qc_eq_bool; case (Qc_eq_dec x y); simpl; auto.x, y:Qc
x <> y -> false = true -> x = y
  intros _ H; inversion H.
Qed.

Definition Qcrt : ring_theory 0 1 Qcplus Qcmult Qcminus Qcopp (eq(A:=Qc)).ring_theory 0 1 Qcplus Qcmult Qcminus Qcopp eq
Proof.ring_theory 0 1 Qcplus Qcmult Qcminus Qcopp eq
  constructor.forall x : Qc, 0 + x = x
forall x y : Qc, x + y = y + x
forall x y z : Qc, x + (y + z) = x + y + z
forall x : Qc, 1 * x = x
forall x y : Qc, x * y = y * x
forall x y z : Qc, x * (y * z) = x * y * z
forall x y z : Qc, (x + y) * z = x * z + y * z
forall x y : Qc, x - y = x + - y
forall x : Qc, x + - x = 0
  exact Qcplus_0_l.forall x y : Qc, x + y = y + x
forall x y z : Qc, x + (y + z) = x + y + z
forall x : Qc, 1 * x = x
forall x y : Qc, x * y = y * x
forall x y z : Qc, x * (y * z) = x * y * z
forall x y z : Qc, (x + y) * z = x * z + y * z
forall x y : Qc, x - y = x + - y
forall x : Qc, x + - x = 0
  exact Qcplus_comm.forall x y z : Qc, x + (y + z) = x + y + z
forall x : Qc, 1 * x = x
forall x y : Qc, x * y = y * x
forall x y z : Qc, x * (y * z) = x * y * z
forall x y z : Qc, (x + y) * z = x * z + y * z
forall x y : Qc, x - y = x + - y
forall x : Qc, x + - x = 0
  exact Qcplus_assoc.forall x : Qc, 1 * x = x
forall x y : Qc, x * y = y * x
forall x y z : Qc, x * (y * z) = x * y * z
forall x y z : Qc, (x + y) * z = x * z + y * z
forall x y : Qc, x - y = x + - y
forall x : Qc, x + - x = 0
  exact Qcmult_1_l.forall x y : Qc, x * y = y * x
forall x y z : Qc, x * (y * z) = x * y * z
forall x y z : Qc, (x + y) * z = x * z + y * z
forall x y : Qc, x - y = x + - y
forall x : Qc, x + - x = 0
  exact Qcmult_comm.forall x y z : Qc, x * (y * z) = x * y * z
forall x y z : Qc, (x + y) * z = x * z + y * z
forall x y : Qc, x - y = x + - y
forall x : Qc, x + - x = 0
  exact Qcmult_assoc.forall x y z : Qc, (x + y) * z = x * z + y * z
forall x y : Qc, x - y = x + - y
forall x : Qc, x + - x = 0
  exact Qcmult_plus_distr_l.forall x y : Qc, x - y = x + - y
forall x : Qc, x + - x = 0
  reflexivity.forall x : Qc, x + - x = 0
  exact Qcplus_opp_r.
Qed.

Definition Qcft :
  field_theory 0%Qc 1%Qc Qcplus Qcmult Qcminus Qcopp Qcdiv Qcinv (eq(A:=Qc)).field_theory 0 1 Qcplus Qcmult Qcminus Qcopp Qcdiv
  Qcinv eq
Proof.field_theory 0 1 Qcplus Qcmult Qcminus Qcopp Qcdiv
  Qcinv eq
  constructor.ring_theory 0 1 Qcplus Qcmult Qcminus Qcopp eq
1 <> 0
forall p q : Qc, p / q = p * / q
forall p : Qc, p <> 0 -> / p * p = 1
  exact Qcrt.1 <> 0
forall p q : Qc, p / q = p * / q
forall p : Qc, p <> 0 -> / p * p = 1
  exact Q_apart_0_1.forall p q : Qc, p / q = p * / q
forall p : Qc, p <> 0 -> / p * p = 1
  reflexivity.forall p : Qc, p <> 0 -> / p * p = 1
  exact Qcmult_inv_l.
Qed.

Add Field Qcfield : Qcft.

A field tactic for rational numbers

Example test_field : (forall x y : Qc, y<>0 -> (x/y)*y = x)%Qc.forall x y : Qc, y <> 0 -> x / y * y = x
Proof.forall x y : Qc, y <> 0 -> x / y * y = x
intros.x, y:Qc
H:y <> 0
x / y * y = x
field.x, y:Qc
H:y <> 0
y <> 0
auto.
Qed.