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.

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.

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.

Coercion from Qc to Q and equality

Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'.
Hint Resolve Qc_is_canon : core.

Theorem Qc_decomp: forall q q': Qc, (q:Q) = q' -> q = q'.

Q2Qc : a conversion from Q to Qc.

Lemma Qred_involutive : forall q:Q, Qred (Qred q) = Qred q.

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

Lemma Q2Qc_eq_iff (q q' : Q) : Q2Qc q = Q2Qc q' <-> q == q'.

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.

Lemma Qclt_alt : forall p q, (p<q) <-> (p?=q = Lt).

Lemma Qcgt_alt : forall p q, (p>q) <-> (p?=q = Gt).

Lemma Qcle_alt : forall p q, (p<=q) <-> (p?=q <> Gt).

Lemma Qcge_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) := 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.

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.

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.

0 is absorbing for multiplication:

Lemma Qcmult_0_l : forall n, 0*n = 0.

Theorem Qcmult_0_r : forall n, n*0=0.

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

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.