Library mathcomp.algebra.rat
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
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
Rat p h == the element of type rat build from p a pair of integers and
h a proof of (0 < p.2) && coprime `|p.1| `|p.2|
n%:Q == explicit cast from int to rat, postfix notation for the
ratz constant
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 GRing.Theory.
Import 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.
Definition denq_ge0 x := ltrW (denq_gt0 x).
Lemma denq_lt0 x : (denq x < 0) = false.
Lemma denq_neq0 x : denq x != 0.
Hint Resolve denq_neq0.
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.
CoInductive 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_iDomain :=
Eval hnf in IdomainType rat (FieldIdomainMixin rat_field_axiom).
Canonical rat_fieldType := FieldType rat rat_field_axiom.
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.
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.
CoInductive 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.
CoInductive 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).
CoInductive 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 le_rat0D le_rat0M le_rat0_anti
subq_ge0 (@le_rat_total 0) norm_ratN ge_rat0_norm lt_rat_def.
Canonical rat_numDomainType := NumDomainType rat ratLeMixin.
Canonical rat_numFieldType := [numFieldType of rat].
Canonical rat_realDomainType := RealDomainType rat (@le_rat_total 0).
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 (ringS : @divringPred R 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.
Implicit Arguments ratr [[R]].
Lemma divq_eq (nx dx ny dy : rat) :
dx != 0 → dy != 0 → (nx / dx == ny / dy) = (nx × dy == ny × dx).
CoInductive 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 le_rat0D le_rat0M le_rat0_anti
subq_ge0 (@le_rat_total 0) norm_ratN ge_rat0_norm lt_rat_def.
Canonical rat_numDomainType := NumDomainType rat ratLeMixin.
Canonical rat_numFieldType := [numFieldType of rat].
Canonical rat_realDomainType := RealDomainType rat (@le_rat_total 0).
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 (ringS : @divringPred R 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.
Implicit Arguments ratr [[R]].
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.