Library mathcomp.algebra.rat
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype bigop order ssralg countalg div ssrnum.
From mathcomp Require Import ssrint.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype bigop order ssralg countalg div ssrnum.
From mathcomp Require Import ssrint.
This file defines a datatype for rational numbers and equips it with a
structure of archimedean, real field, with int and nat declared as closed
subrings.
rat == the type of rational number, with single constructor Rat
n%:Q == explicit cast from int to rat, ie. the specialization to
rationals of the generic ring morphism n%:~R
numq r == numerator of (r : rat)
denq r == denominator of (r : rat)
x \is a Qint == x is an element of rat whose denominator is equal to 1
x \is a Qnat == x is a positive element of rat whose denominator is equal
to 1
ratr x == generic embedding of (r : R) into an arbitrary unitring.
Import Order.TTheory GRing.Theory Num.Theory.
Set Implicit Arguments.
Local Open Scope ring_scope.
Record rat : Set := Rat {
valq : (int × int);
_ : (0 < valq.2) && coprime `|valq.1| `|valq.2|
}.
Delimit Scope rat_scope with Q.
Definition ratz (n : int) := @Rat (n, 1) (coprimen1 _).
Coercion ratz (n : int) := @Rat (n, 1) (coprimen1 _).
Canonical rat_subType := Eval hnf in [subType for valq].
Definition rat_eqMixin := [eqMixin of rat by <:].
Canonical rat_eqType := EqType rat rat_eqMixin.
Definition rat_choiceMixin := [choiceMixin of rat by <:].
Canonical rat_choiceType := ChoiceType rat rat_choiceMixin.
Definition rat_countMixin := [countMixin of rat by <:].
Canonical rat_countType := CountType rat rat_countMixin.
Canonical rat_subCountType := [subCountType of rat].
Definition numq x := nosimpl ((valq x).1).
Definition denq x := nosimpl ((valq x).2).
Lemma denq_gt0 x : 0 < denq x.
Hint Resolve denq_gt0 : core.
Definition denq_ge0 x := ltW (denq_gt0 x).
Lemma denq_lt0 x : (denq x < 0) = false.
Lemma denq_neq0 x : denq x != 0.
Hint Resolve denq_neq0 : core.
Lemma denq_eq0 x : (denq x == 0) = false.
Lemma coprime_num_den x : coprime `|numq x| `|denq x|.
Fact RatK x P : @Rat (numq x, denq x) P = x.
Fact fracq_subproof : ∀ x : int × int,
let n :=
if x.2 == 0 then 0 else
(-1) ^ ((x.2 < 0) (+) (x.1 < 0)) × (`|x.1| %/ gcdn `|x.1| `|x.2|)%:Z in
let d := if x.2 == 0 then 1 else (`|x.2| %/ gcdn `|x.1| `|x.2|)%:Z in
(0 < d) && (coprime `|n| `|d|).
Definition fracq (x : int × int) := nosimpl (@Rat (_, _) (fracq_subproof x)).
Fact ratz_frac n : ratz n = fracq (n, 1).
Fact valqK x : fracq (valq x) = x.
Fact scalq_key : unit.
Definition scalq_def x := sgr x.2 × (gcdn `|x.1| `|x.2|)%:Z.
Definition scalq := locked_with scalq_key scalq_def.
Canonical scalq_unlockable := [unlockable fun scalq].
Fact scalq_eq0 x : (scalq x == 0) = (x.2 == 0).
Lemma sgr_scalq x : sgr (scalq x) = sgr x.2.
Lemma signr_scalq x : (scalq x < 0) = (x.2 < 0).
Lemma scalqE x :
x.2 != 0 → scalq x = (-1) ^+ (x.2 < 0)%R × (gcdn `|x.1| `|x.2|)%:Z.
Fact valq_frac x :
x.2 != 0 → x = (scalq x × numq (fracq x), scalq x × denq (fracq x)).
Definition zeroq := fracq (0, 1).
Definition oneq := fracq (1, 1).
Fact frac0q x : fracq (0, x) = zeroq.
Fact fracq0 x : fracq (x, 0) = zeroq.
Variant fracq_spec (x : int × int) : int × int → rat → Type :=
| FracqSpecN of x.2 = 0 : fracq_spec x (x.1, 0) zeroq
| FracqSpecP k fx of k != 0 : fracq_spec x (k × numq fx, k × denq fx) fx.
Fact fracqP x : fracq_spec x x (fracq x).
Lemma rat_eqE x y : (x == y) = (numq x == numq y) && (denq x == denq y).
Lemma sgr_denq x : sgr (denq x) = 1.
Lemma normr_denq x : `|denq x| = denq x.
Lemma absz_denq x : `|denq x|%N = denq x :> int.
Lemma rat_eq x y : (x == y) = (numq x × denq y == numq y × denq x).
Fact fracq_eq x y : x.2 != 0 → y.2 != 0 →
(fracq x == fracq y) = (x.1 × y.2 == y.1 × x.2).
Fact fracq_eq0 x : (fracq x == zeroq) = (x.1 == 0) || (x.2 == 0).
Fact fracqMM x n d : x != 0 → fracq (x × n, x × d) = fracq (n, d).
Definition addq_subdef (x y : int × int) := (x.1 × y.2 + y.1 × x.2, x.2 × y.2).
Definition addq (x y : rat) := nosimpl fracq (addq_subdef (valq x) (valq y)).
Definition oppq_subdef (x : int × int) := (- x.1, x.2).
Definition oppq (x : rat) := nosimpl fracq (oppq_subdef (valq x)).
Fact addq_subdefC : commutative addq_subdef.
Fact addq_subdefA : associative addq_subdef.
Fact addq_frac x y : x.2 != 0 → y.2 != 0 →
(addq (fracq x) (fracq y)) = fracq (addq_subdef x y).
Fact ratzD : {morph ratz : x y / x + y >-> addq x y}.
Fact oppq_frac x : oppq (fracq x) = fracq (oppq_subdef x).
Fact ratzN : {morph ratz : x / - x >-> oppq x}.
Fact addqC : commutative addq.
Fact addqA : associative addq.
Fact add0q : left_id zeroq addq.
Fact addNq : left_inverse (fracq (0, 1)) oppq addq.
Definition rat_ZmodMixin := ZmodMixin addqA addqC add0q addNq.
Canonical rat_ZmodType := ZmodType rat rat_ZmodMixin.
Definition mulq_subdef (x y : int × int) := nosimpl (x.1 × y.1, x.2 × y.2).
Definition mulq (x y : rat) := nosimpl fracq (mulq_subdef (valq x) (valq y)).
Fact mulq_subdefC : commutative mulq_subdef.
Fact mul_subdefA : associative mulq_subdef.
Definition invq_subdef (x : int × int) := nosimpl (x.2, x.1).
Definition invq (x : rat) := nosimpl fracq (invq_subdef (valq x)).
Fact mulq_frac x y : (mulq (fracq x) (fracq y)) = fracq (mulq_subdef x y).
Fact ratzM : {morph ratz : x y / x × y >-> mulq x y}.
Fact invq_frac x :
x.1 != 0 → x.2 != 0 → invq (fracq x) = fracq (invq_subdef x).
Fact mulqC : commutative mulq.
Fact mulqA : associative mulq.
Fact mul1q : left_id oneq mulq.
Fact mulq_addl : left_distributive mulq addq.
Fact nonzero1q : oneq != zeroq.
Definition rat_comRingMixin :=
ComRingMixin mulqA mulqC mul1q mulq_addl nonzero1q.
Canonical rat_Ring := Eval hnf in RingType rat rat_comRingMixin.
Canonical rat_comRing := Eval hnf in ComRingType rat mulqC.
Fact mulVq x : x != 0 → mulq (invq x) x = 1.
Fact invq0 : invq 0 = 0.
Definition RatFieldUnitMixin := FieldUnitMixin mulVq invq0.
Canonical rat_unitRing :=
Eval hnf in UnitRingType rat RatFieldUnitMixin.
Canonical rat_comUnitRing := Eval hnf in [comUnitRingType of rat].
Fact rat_field_axiom : GRing.Field.mixin_of rat_unitRing.
Definition RatFieldIdomainMixin := (FieldIdomainMixin rat_field_axiom).
Canonical rat_idomainType :=
Eval hnf in IdomainType rat (FieldIdomainMixin rat_field_axiom).
Canonical rat_fieldType := FieldType rat rat_field_axiom.
Canonical rat_countZmodType := [countZmodType of rat].
Canonical rat_countRingType := [countRingType of rat].
Canonical rat_countComRingType := [countComRingType of rat].
Canonical rat_countUnitRingType := [countUnitRingType of rat].
Canonical rat_countComUnitRingType := [countComUnitRingType of rat].
Canonical rat_countIdomainType := [countIdomainType of rat].
Canonical rat_countFieldType := [countFieldType of rat].
Lemma numq_eq0 x : (numq x == 0) = (x == 0).
Notation "n %:Q" := ((n : int)%:~R : rat)
(at level 2, left associativity, format "n %:Q") : ring_scope.
Hint Resolve denq_neq0 denq_gt0 denq_ge0 : core.
Definition subq (x y : rat) : rat := (addq x (oppq y)).
Definition divq (x y : rat) : rat := (mulq x (invq y)).
Notation "0" := zeroq : rat_scope.
Notation "1" := oneq : rat_scope.
Infix "+" := addq : rat_scope.
Notation "- x" := (oppq x) : rat_scope.
Infix "×" := mulq : rat_scope.
Notation "x ^-1" := (invq x) : rat_scope.
Infix "-" := subq : rat_scope.
Infix "/" := divq : rat_scope.
ratz should not be used, %:Q should be used instead
Lemma ratzE n : ratz n = n%:Q.
Lemma numq_int n : numq n%:Q = n.
Lemma denq_int n : denq n%:Q = 1.
Lemma rat0 : 0%:Q = 0.
Lemma rat1 : 1%:Q = 1.
Lemma numqN x : numq (- x) = - numq x.
Lemma denqN x : denq (- x) = denq x.
Lemma numq_int n : numq n%:Q = n.
Lemma denq_int n : denq n%:Q = 1.
Lemma rat0 : 0%:Q = 0.
Lemma rat1 : 1%:Q = 1.
Lemma numqN x : numq (- x) = - numq x.
Lemma denqN x : denq (- x) = denq x.
Will be subsumed by pnatr_eq0
fracq should never appear, its canonical form is _%
Lemma fracqE x : fracq x = x.1%:Q / x.2%:Q.
Lemma divq_num_den x : (numq x)%:Q / (denq x)%:Q = x.
Variant divq_spec (n d : int) : int → int → rat → Type :=
| DivqSpecN of d = 0 : divq_spec n d n 0 0
| DivqSpecP k x of k != 0 : divq_spec n d (k × numq x) (k × denq x) x.
Lemma divq_num_den x : (numq x)%:Q / (denq x)%:Q = x.
Variant divq_spec (n d : int) : int → int → rat → Type :=
| DivqSpecN of d = 0 : divq_spec n d n 0 0
| DivqSpecP k x of k != 0 : divq_spec n d (k × numq x) (k × denq x) x.
replaces fracqP
Lemma divqP n d : divq_spec n d n d (n%:Q / d%:Q).
Lemma divq_eq (nx dx ny dy : rat) :
dx != 0 → dy != 0 → (nx / dx == ny / dy) = (nx × dy == ny × dx).
Variant rat_spec (* (x : rat) *) : rat → int → int → Type :=
Rat_spec (n : int) (d : nat) & coprime `|n| d.+1
: rat_spec (* x *) (n%:Q / d.+1%:Q) n d.+1.
Lemma ratP x : rat_spec x (numq x) (denq x).
Lemma coprimeq_num n d : coprime `|n| `|d| → numq (n%:~R / d%:~R) = sgr d × n.
Lemma coprimeq_den n d :
coprime `|n| `|d| → denq (n%:~R / d%:~R) = (if d == 0 then 1 else `|d|).
Lemma denqVz (i : int) : i != 0 → denq (i%:~R^-1) = `|i|.
Lemma numqE x : (numq x)%:~R = x × (denq x)%:~R.
Lemma denqP x : {d | denq x = d.+1}.
Definition normq (x : rat) : rat := `|numq x|%:~R / (denq x)%:~R.
Definition le_rat (x y : rat) := numq x × denq y ≤ numq y × denq x.
Definition lt_rat (x y : rat) := numq x × denq y < numq y × denq x.
Lemma gt_rat0 x : lt_rat 0 x = (0 < numq x).
Lemma lt_rat0 x : lt_rat x 0 = (numq x < 0).
Lemma ge_rat0 x : le_rat 0 x = (0 ≤ numq x).
Lemma le_rat0 x : le_rat x 0 = (numq x ≤ 0).
Fact le_rat0D x y : le_rat 0 x → le_rat 0 y → le_rat 0 (x + y).
Fact le_rat0M x y : le_rat 0 x → le_rat 0 y → le_rat 0 (x × y).
Fact le_rat0_anti x : le_rat 0 x → le_rat x 0 → x = 0.
Lemma sgr_numq_div (n d : int) : sgr (numq (n%:Q / d%:Q)) = sgr n × sgr d.
Fact subq_ge0 x y : le_rat 0 (y - x) = le_rat x y.
Fact le_rat_total : total le_rat.
Fact numq_sign_mul (b : bool) x : numq ((-1) ^+ b × x) = (-1) ^+ b × numq x.
Fact numq_div_lt0 n d : n != 0 → d != 0 →
(numq (n%:~R / d%:~R) < 0)%R = (n < 0)%R (+) (d < 0)%R.
Lemma normr_num_div n d : `|numq (n%:~R / d%:~R)| = numq (`|n|%:~R / `|d|%:~R).
Fact norm_ratN x : normq (- x) = normq x.
Fact ge_rat0_norm x : le_rat 0 x → normq x = x.
Fact lt_rat_def x y : (lt_rat x y) = (y != x) && (le_rat x y).
Definition ratLeMixin : realLeMixin rat_idomainType :=
RealLeMixin le_rat0D le_rat0M le_rat0_anti subq_ge0
(@le_rat_total 0) norm_ratN ge_rat0_norm lt_rat_def.
Canonical rat_porderType := POrderType ring_display rat ratLeMixin.
Canonical rat_latticeType := LatticeType rat ratLeMixin.
Canonical rat_distrLatticeType := DistrLatticeType rat ratLeMixin.
Canonical rat_orderType := OrderType rat le_rat_total.
Canonical rat_numDomainType := NumDomainType rat ratLeMixin.
Canonical rat_normedZmodType := NormedZmodType rat rat ratLeMixin.
Canonical rat_numFieldType := [numFieldType of rat].
Canonical rat_realDomainType := [realDomainType of rat].
Canonical rat_realFieldType := [realFieldType of rat].
Lemma numq_ge0 x : (0 ≤ numq x) = (0 ≤ x).
Lemma numq_le0 x : (numq x ≤ 0) = (x ≤ 0).
Lemma numq_gt0 x : (0 < numq x) = (0 < x).
Lemma numq_lt0 x : (numq x < 0) = (x < 0).
Lemma sgr_numq x : sgz (numq x) = sgz x.
Lemma denq_mulr_sign (b : bool) x : denq ((-1) ^+ b × x) = denq x.
Lemma denq_norm x : denq `|x| = denq x.
Fact rat_archimedean : Num.archimedean_axiom [numDomainType of rat].
Canonical archiType := ArchiFieldType rat rat_archimedean.
Section QintPred.
Definition Qint := [qualify a x : rat | denq x == 1].
Fact Qint_key : pred_key Qint.
Canonical Qint_keyed := KeyedQualifier Qint_key.
Lemma Qint_def x : (x \is a Qint) = (denq x == 1).
Lemma numqK : {in Qint, cancel (fun x ⇒ numq x) intr}.
Lemma QintP x : reflect (∃ z, x = z%:~R) (x \in Qint).
Fact Qint_subring_closed : subring_closed Qint.
Canonical Qint_opprPred := OpprPred Qint_subring_closed.
Canonical Qint_addrPred := AddrPred Qint_subring_closed.
Canonical Qint_mulrPred := MulrPred Qint_subring_closed.
Canonical Qint_zmodPred := ZmodPred Qint_subring_closed.
Canonical Qint_semiringPred := SemiringPred Qint_subring_closed.
Canonical Qint_smulrPred := SmulrPred Qint_subring_closed.
Canonical Qint_subringPred := SubringPred Qint_subring_closed.
End QintPred.
Section QnatPred.
Definition Qnat := [qualify a x : rat | (x \is a Qint) && (0 ≤ x)].
Fact Qnat_key : pred_key Qnat.
Canonical Qnat_keyed := KeyedQualifier Qnat_key.
Lemma Qnat_def x : (x \is a Qnat) = (x \is a Qint) && (0 ≤ x).
Lemma QnatP x : reflect (∃ n : nat, x = n%:R) (x \in Qnat).
Fact Qnat_semiring_closed : semiring_closed Qnat.
Canonical Qnat_addrPred := AddrPred Qnat_semiring_closed.
Canonical Qnat_mulrPred := MulrPred Qnat_semiring_closed.
Canonical Qnat_semiringPred := SemiringPred Qnat_semiring_closed.
End QnatPred.
Lemma natq_div m n : n %| m → (m %/ n)%:R = m%:R / n%:R :> rat.
Section InRing.
Variable R : unitRingType.
Definition ratr x : R := (numq x)%:~R / (denq x)%:~R.
Lemma ratr_int z : ratr z%:~R = z%:~R.
Lemma ratr_nat n : ratr n%:R = n%:R.
Lemma rpred_rat (S : {pred R}) (ringS : divringPred S) (kS : keyed_pred ringS)
a :
ratr a \in kS.
End InRing.
Section Fmorph.
Implicit Type rR : unitRingType.
Lemma fmorph_rat (aR : fieldType) rR (f : {rmorphism aR → rR}) a :
f (ratr _ a) = ratr _ a.
Lemma fmorph_eq_rat rR (f : {rmorphism rat → rR}) : f =1 ratr _.
End Fmorph.
Section Linear.
Implicit Types (U V : lmodType rat) (A B : lalgType rat).
Lemma rat_linear U V (f : U → V) : additive f → linear f.
Lemma rat_lrmorphism A B (f : A → B) : rmorphism f → lrmorphism f.
End Linear.
Section InPrealField.
Variable F : numFieldType.
Fact ratr_is_rmorphism : rmorphism (@ratr F).
Canonical ratr_additive := Additive ratr_is_rmorphism.
Canonical ratr_rmorphism := RMorphism ratr_is_rmorphism.
Lemma ler_rat : {mono (@ratr F) : x y / x ≤ y}.
Lemma ltr_rat : {mono (@ratr F) : x y / x < y}.
Lemma ler0q x : (0 ≤ ratr F x) = (0 ≤ x).
Lemma lerq0 x : (ratr F x ≤ 0) = (x ≤ 0).
Lemma ltr0q x : (0 < ratr F x) = (0 < x).
Lemma ltrq0 x : (ratr F x < 0) = (x < 0).
Lemma ratr_sg x : ratr F (sgr x) = sgr (ratr F x).
Lemma ratr_norm x : ratr F `|x| = `|ratr F x|.
End InPrealField.
Lemma divq_eq (nx dx ny dy : rat) :
dx != 0 → dy != 0 → (nx / dx == ny / dy) = (nx × dy == ny × dx).
Variant rat_spec (* (x : rat) *) : rat → int → int → Type :=
Rat_spec (n : int) (d : nat) & coprime `|n| d.+1
: rat_spec (* x *) (n%:Q / d.+1%:Q) n d.+1.
Lemma ratP x : rat_spec x (numq x) (denq x).
Lemma coprimeq_num n d : coprime `|n| `|d| → numq (n%:~R / d%:~R) = sgr d × n.
Lemma coprimeq_den n d :
coprime `|n| `|d| → denq (n%:~R / d%:~R) = (if d == 0 then 1 else `|d|).
Lemma denqVz (i : int) : i != 0 → denq (i%:~R^-1) = `|i|.
Lemma numqE x : (numq x)%:~R = x × (denq x)%:~R.
Lemma denqP x : {d | denq x = d.+1}.
Definition normq (x : rat) : rat := `|numq x|%:~R / (denq x)%:~R.
Definition le_rat (x y : rat) := numq x × denq y ≤ numq y × denq x.
Definition lt_rat (x y : rat) := numq x × denq y < numq y × denq x.
Lemma gt_rat0 x : lt_rat 0 x = (0 < numq x).
Lemma lt_rat0 x : lt_rat x 0 = (numq x < 0).
Lemma ge_rat0 x : le_rat 0 x = (0 ≤ numq x).
Lemma le_rat0 x : le_rat x 0 = (numq x ≤ 0).
Fact le_rat0D x y : le_rat 0 x → le_rat 0 y → le_rat 0 (x + y).
Fact le_rat0M x y : le_rat 0 x → le_rat 0 y → le_rat 0 (x × y).
Fact le_rat0_anti x : le_rat 0 x → le_rat x 0 → x = 0.
Lemma sgr_numq_div (n d : int) : sgr (numq (n%:Q / d%:Q)) = sgr n × sgr d.
Fact subq_ge0 x y : le_rat 0 (y - x) = le_rat x y.
Fact le_rat_total : total le_rat.
Fact numq_sign_mul (b : bool) x : numq ((-1) ^+ b × x) = (-1) ^+ b × numq x.
Fact numq_div_lt0 n d : n != 0 → d != 0 →
(numq (n%:~R / d%:~R) < 0)%R = (n < 0)%R (+) (d < 0)%R.
Lemma normr_num_div n d : `|numq (n%:~R / d%:~R)| = numq (`|n|%:~R / `|d|%:~R).
Fact norm_ratN x : normq (- x) = normq x.
Fact ge_rat0_norm x : le_rat 0 x → normq x = x.
Fact lt_rat_def x y : (lt_rat x y) = (y != x) && (le_rat x y).
Definition ratLeMixin : realLeMixin rat_idomainType :=
RealLeMixin le_rat0D le_rat0M le_rat0_anti subq_ge0
(@le_rat_total 0) norm_ratN ge_rat0_norm lt_rat_def.
Canonical rat_porderType := POrderType ring_display rat ratLeMixin.
Canonical rat_latticeType := LatticeType rat ratLeMixin.
Canonical rat_distrLatticeType := DistrLatticeType rat ratLeMixin.
Canonical rat_orderType := OrderType rat le_rat_total.
Canonical rat_numDomainType := NumDomainType rat ratLeMixin.
Canonical rat_normedZmodType := NormedZmodType rat rat ratLeMixin.
Canonical rat_numFieldType := [numFieldType of rat].
Canonical rat_realDomainType := [realDomainType of rat].
Canonical rat_realFieldType := [realFieldType of rat].
Lemma numq_ge0 x : (0 ≤ numq x) = (0 ≤ x).
Lemma numq_le0 x : (numq x ≤ 0) = (x ≤ 0).
Lemma numq_gt0 x : (0 < numq x) = (0 < x).
Lemma numq_lt0 x : (numq x < 0) = (x < 0).
Lemma sgr_numq x : sgz (numq x) = sgz x.
Lemma denq_mulr_sign (b : bool) x : denq ((-1) ^+ b × x) = denq x.
Lemma denq_norm x : denq `|x| = denq x.
Fact rat_archimedean : Num.archimedean_axiom [numDomainType of rat].
Canonical archiType := ArchiFieldType rat rat_archimedean.
Section QintPred.
Definition Qint := [qualify a x : rat | denq x == 1].
Fact Qint_key : pred_key Qint.
Canonical Qint_keyed := KeyedQualifier Qint_key.
Lemma Qint_def x : (x \is a Qint) = (denq x == 1).
Lemma numqK : {in Qint, cancel (fun x ⇒ numq x) intr}.
Lemma QintP x : reflect (∃ z, x = z%:~R) (x \in Qint).
Fact Qint_subring_closed : subring_closed Qint.
Canonical Qint_opprPred := OpprPred Qint_subring_closed.
Canonical Qint_addrPred := AddrPred Qint_subring_closed.
Canonical Qint_mulrPred := MulrPred Qint_subring_closed.
Canonical Qint_zmodPred := ZmodPred Qint_subring_closed.
Canonical Qint_semiringPred := SemiringPred Qint_subring_closed.
Canonical Qint_smulrPred := SmulrPred Qint_subring_closed.
Canonical Qint_subringPred := SubringPred Qint_subring_closed.
End QintPred.
Section QnatPred.
Definition Qnat := [qualify a x : rat | (x \is a Qint) && (0 ≤ x)].
Fact Qnat_key : pred_key Qnat.
Canonical Qnat_keyed := KeyedQualifier Qnat_key.
Lemma Qnat_def x : (x \is a Qnat) = (x \is a Qint) && (0 ≤ x).
Lemma QnatP x : reflect (∃ n : nat, x = n%:R) (x \in Qnat).
Fact Qnat_semiring_closed : semiring_closed Qnat.
Canonical Qnat_addrPred := AddrPred Qnat_semiring_closed.
Canonical Qnat_mulrPred := MulrPred Qnat_semiring_closed.
Canonical Qnat_semiringPred := SemiringPred Qnat_semiring_closed.
End QnatPred.
Lemma natq_div m n : n %| m → (m %/ n)%:R = m%:R / n%:R :> rat.
Section InRing.
Variable R : unitRingType.
Definition ratr x : R := (numq x)%:~R / (denq x)%:~R.
Lemma ratr_int z : ratr z%:~R = z%:~R.
Lemma ratr_nat n : ratr n%:R = n%:R.
Lemma rpred_rat (S : {pred R}) (ringS : divringPred S) (kS : keyed_pred ringS)
a :
ratr a \in kS.
End InRing.
Section Fmorph.
Implicit Type rR : unitRingType.
Lemma fmorph_rat (aR : fieldType) rR (f : {rmorphism aR → rR}) a :
f (ratr _ a) = ratr _ a.
Lemma fmorph_eq_rat rR (f : {rmorphism rat → rR}) : f =1 ratr _.
End Fmorph.
Section Linear.
Implicit Types (U V : lmodType rat) (A B : lalgType rat).
Lemma rat_linear U V (f : U → V) : additive f → linear f.
Lemma rat_lrmorphism A B (f : A → B) : rmorphism f → lrmorphism f.
End Linear.
Section InPrealField.
Variable F : numFieldType.
Fact ratr_is_rmorphism : rmorphism (@ratr F).
Canonical ratr_additive := Additive ratr_is_rmorphism.
Canonical ratr_rmorphism := RMorphism ratr_is_rmorphism.
Lemma ler_rat : {mono (@ratr F) : x y / x ≤ y}.
Lemma ltr_rat : {mono (@ratr F) : x y / x < y}.
Lemma ler0q x : (0 ≤ ratr F x) = (0 ≤ x).
Lemma lerq0 x : (ratr F x ≤ 0) = (x ≤ 0).
Lemma ltr0q x : (0 < ratr F x) = (0 < x).
Lemma ltrq0 x : (ratr F x < 0) = (x < 0).
Lemma ratr_sg x : ratr F (sgr x) = sgr (ratr F x).
Lemma ratr_norm x : ratr F `|x| = `|ratr F x|.
End InPrealField.
Conntecting rationals to the ring an field tactics
Ltac rat_to_ring :=
rewrite -?[0%Q]/(0 : rat)%R -?[1%Q]/(1 : rat)%R
-?[(_ - _)%Q]/(_ - _ : rat)%R -?[(_ / _)%Q]/(_ / _ : rat)%R
-?[(_ + _)%Q]/(_ + _ : rat)%R -?[(_ × _)%Q]/(_ × _ : rat)%R
-?[(- _)%Q]/(- _ : rat)%R -?[(_ ^-1)%Q]/(_ ^-1 : rat)%R /=.
Ltac ring_to_rat :=
rewrite -?[0%R]/0%Q -?[1%R]/1%Q
-?[(_ - _)%R]/(_ - _)%Q -?[(_ / _)%R]/(_ / _)%Q
-?[(_ + _)%R]/(_ + _)%Q -?[(_ × _)%R]/(_ × _)%Q
-?[(- _)%R]/(- _)%Q -?[(_ ^-1)%R]/(_ ^-1)%Q /=.
Lemma rat_ring_theory : (ring_theory 0%Q 1%Q addq mulq subq oppq eq).
Require setoid_ring.Field_theory setoid_ring.Field_tac.
Lemma rat_field_theory :
Field_theory.field_theory 0%Q 1%Q addq mulq subq oppq divq invq eq.
Add Field rat_field : rat_field_theory.