Library mathcomp.algebra.rat
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
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 prime.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
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 prime.
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
<number> == <number> as a rat with <number> a decimal constant.
This notation is in rat_scope (delimited with %Q).
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 non-negative element of rat whose denominator
is equal to 1
ratr r == generic embedding of (r : rat) into an arbitrary unit ring.
[rat x // y] == smart constructor for rationals, definitionally equal
to x / y for concrete values, intended for printing only
of normal forms. The parsable notation is for debugging.
Import Order.TTheory GRing.Theory Num.Theory.
Set Implicit Arguments.
Reserved Notation "[ 'rat' x // y ]" (format "[ 'rat' x // y ]", at level 0).
Reserved Notation "n %:Q" (at level 2, left associativity, format "n %:Q").
Local Open Scope ring_scope.
Record rat : Set := Rat {
valq : (int × int);
_ : (0 < valq.2) && coprime `|valq.1| `|valq.2|
}.
Bind Scope ring_scope with rat.
Delimit Scope rat_scope with Q.
Definition ratz (n : int) := @Rat (n, 1) (coprimen1 _).
Coercion ratz (n : int) := @Rat (n, 1) (coprimen1 _).
Definition rat_isSub := Eval hnf in [isSub for valq].
#[hnf] HB.instance Definition _ := [Equality of rat by <:].
Definition numq x := nosimpl ((valq x).1).
Definition denq x := nosimpl ((valq x).2).
Lemma denq_gt0 x : 0 < denq x.
#[global] 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.
#[global] 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.
Definition fracq_subdef x :=
if x.2 != 0 then let g := gcdn `|x.1| `|x.2| in
((-1) ^ ((x.2 < 0) (+) (x.1 < 0)) × (`|x.1| %/ g)%:Z, (`|x.2| %/ g)%:Z)
else (0, 1).
Arguments fracq_subdef /.
Definition fracq_opt_subdef (x : int × int) :=
if (0 < x.2) && coprime `|x.1| `|x.2| then x else fracq_subdef x.
Lemma fracq_opt_subdefE x : fracq_opt_subdef x = fracq_subdef x.
Fact fracq_subproof x (y := fracq_opt_subdef x) :
(0 < y.2) && (coprime `|y.1| `|y.2|).
Lemma fracq_opt_subdef_id x :
fracq_opt_subdef (fracq_opt_subdef x) = fracq_subdef x.
We use a match expression in order to "lock" the definition of fracq.
Indeed, the kernel will try to reduce a fracq only when applied to
a term which has "enough" constructors: i.e. it reduces to a pair of
a Posz or Negz on the first component, and a Posz of 0 or S, or a Negz
on the second component. See issue #698.
Additionally, we use fracq_opt_subdef to precompute the normal form
before we use fracq_subproof in order to make sure the proof will be
independent from the input of fracq. This ensure reflexivity of any
computation involving rationals as long as all operators use fracq.
As a consequence val (fracq x) = fracq_opt_subdef (fracq_opt_subdef x))
Definition fracq '((n', d')) : rat :=
match d', n' with
| Posz 0 as d, _ as n ⇒ Rat (fracq_subproof (1, 0))
| _ as d, Posz _ as n | _ as d, _ as n ⇒
Rat (fracq_subproof (fracq_opt_subdef (n, d)))
end.
Arguments fracq : simpl never.
match d', n' with
| Posz 0 as d, _ as n ⇒ Rat (fracq_subproof (1, 0))
| _ as d, Posz _ as n | _ as d, _ as n ⇒
Rat (fracq_subproof (fracq_opt_subdef (n, d)))
end.
Arguments fracq : simpl never.
Define a Number Notation for rat in rat_scope
Since rat values obtained from fracq contain fracq_subdef, which is not
an inductive constructor, we need to go through an intermediate
inductive type.
Variant Irat_prf := Ifracq_subproof : (int × int) → Irat_prf.
Variant Irat := IRat : (int × int) → Irat_prf → Irat.
Definition parse (x : Number.number) : option Irat :=
let parse_pos i f :=
let nf := Decimal.nb_digits f in
let d := (10 ^ nf)%nat in
let n := (Nat.of_uint i × d + Nat.of_uint f)%nat in
valq (fracq (Posz n, Posz d)) in
let parse i f :=
match i with
| Decimal.Pos i ⇒ parse_pos i f
| Decimal.Neg i ⇒ let (n, d) := parse_pos i f in ((- n)%R, d)
end in
match x with
| Number.Decimal (Decimal.Decimal i f) ⇒
let nd := parse i f in
Some (IRat nd (Ifracq_subproof nd))
| Number.Decimal (Decimal.DecimalExp _ _ _) ⇒ None
| Number.Hexadecimal _ ⇒ None
end.
Definition print (r : Irat) : option Number.number :=
let print_pos n d :=
if d == 1%nat then Some (Nat.to_uint n, Decimal.Nil) else
let d2d5 :=
match prime_decomp d with
| [:: (2, d2); (5, d5)] ⇒ Some (d2, d5)
| [:: (2, d2)] ⇒ Some (d2, O)
| [:: (5, d5)] ⇒ Some (O, d5)
| _ ⇒ None
end in
match d2d5 with
| Some (d2, d5) ⇒
let f := (2 ^ (d5 - d2) × 5 ^ (d2 - d5))%nat in
let (i, f) := edivn (n × f) (d × f) in
Some (Nat.to_uint i, Nat.to_uint f)
| None ⇒ None
end in
let print_IRat nd :=
match nd with
| (Posz n, Posz d) ⇒
match print_pos n d with
| Some (i, f) ⇒ Some (Decimal.Pos i, f)
| None ⇒ None
end
| (Negz n, Posz d) ⇒
match print_pos n.+1 d with
| Some (i, f) ⇒ Some (Decimal.Neg i, f)
| None ⇒ None
end
| (_, Negz _) ⇒ None
end in
match r with
| IRat nd _ ⇒
match print_IRat nd with
| Some (i, f) ⇒ Some (Number.Decimal (Decimal.Decimal i f))
| None ⇒ None
end
end.
Variant Irat := IRat : (int × int) → Irat_prf → Irat.
Definition parse (x : Number.number) : option Irat :=
let parse_pos i f :=
let nf := Decimal.nb_digits f in
let d := (10 ^ nf)%nat in
let n := (Nat.of_uint i × d + Nat.of_uint f)%nat in
valq (fracq (Posz n, Posz d)) in
let parse i f :=
match i with
| Decimal.Pos i ⇒ parse_pos i f
| Decimal.Neg i ⇒ let (n, d) := parse_pos i f in ((- n)%R, d)
end in
match x with
| Number.Decimal (Decimal.Decimal i f) ⇒
let nd := parse i f in
Some (IRat nd (Ifracq_subproof nd))
| Number.Decimal (Decimal.DecimalExp _ _ _) ⇒ None
| Number.Hexadecimal _ ⇒ None
end.
Definition print (r : Irat) : option Number.number :=
let print_pos n d :=
if d == 1%nat then Some (Nat.to_uint n, Decimal.Nil) else
let d2d5 :=
match prime_decomp d with
| [:: (2, d2); (5, d5)] ⇒ Some (d2, d5)
| [:: (2, d2)] ⇒ Some (d2, O)
| [:: (5, d5)] ⇒ Some (O, d5)
| _ ⇒ None
end in
match d2d5 with
| Some (d2, d5) ⇒
let f := (2 ^ (d5 - d2) × 5 ^ (d2 - d5))%nat in
let (i, f) := edivn (n × f) (d × f) in
Some (Nat.to_uint i, Nat.to_uint f)
| None ⇒ None
end in
let print_IRat nd :=
match nd with
| (Posz n, Posz d) ⇒
match print_pos n d with
| Some (i, f) ⇒ Some (Decimal.Pos i, f)
| None ⇒ None
end
| (Negz n, Posz d) ⇒
match print_pos n.+1 d with
| Some (i, f) ⇒ Some (Decimal.Neg i, f)
| None ⇒ None
end
| (_, Negz _) ⇒ None
end in
match r with
| IRat nd _ ⇒
match print_IRat nd with
| Some (i, f) ⇒ Some (Number.Decimal (Decimal.Decimal i f))
| None ⇒ None
end
end.
Now, the following should parse as rat (and print unchaged)
Check 12%Q.
Check 3.14%Q.
Check (-3.14)%Q.
Check 0.5%Q.
Check 0.2%Q.
Lemma val_fracq x : val (fracq x) = fracq_subdef x.
Lemma num_fracq x : numq (fracq x) = if x.2 != 0 then
(-1) ^ ((x.2 < 0) (+) (x.1 < 0)) × (`|x.1| %/ gcdn `|x.1| `|x.2|)%:Z else 0.
Lemma den_fracq x : denq (fracq x) =
if x.2 != 0 then (`|x.2| %/ gcdn `|x.1| `|x.2|)%:Z else 1.
Fact ratz_frac n : ratz n = fracq (n, 1).
Fact valqK x : fracq (valq x) = x.
Definition scalq '(n, d) := sgr d × (gcdn `|n| `|d|)%:Z.
Lemma scalq_def x : scalq x = sgr x.2 × (gcdn `|x.1| `|x.2|)%:Z.
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 := 0%Q.
Definition oneq := 1%Q.
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).
We "lock" the definition of addq, oppq, mulq and invq, using a match on
the constructor Rat for both arguments, so that it may only be reduced
when applied to explicit rationals. Since fracq is also "locked" in a
similar way, fracq will not reduce to a Rat x xP unless it is also applied
to "enough" constructors. This preserves the reduction on gound elements
while it suspends it when applied to at least one variable at the leaf of
the arithmetic operation.
Moreover we optimize addition when one or both arguments are integers,
in which case we presimplify the output, this shortens the size of the hnf
of terms of the form N%:Q when N is a concrete natural number.
Definition addq_subdef (x y : int × int) :=
let: (x1, x2) := x in
let: (y1, y2) := y in
match x2, y2 with
| Posz 1, Posz 1 ⇒
match x1, y1 with
| Posz 0, _ ⇒ (y1, 1)
| _, Posz 0 ⇒ (x1, 1)
| Posz n, Posz 1 ⇒ (Posz n.+1, 1)
| Posz 1, Posz n ⇒ (Posz n.+1, 1)
| _, _ ⇒ (x1 + y1, 1)
end
| Posz 1, _ ⇒ (x1 × y2 + y1, y2)
| _, Posz 1 ⇒ (x1 + y1 × x2, x2)
| _, _ ⇒ (x1 × y2 + y1 × x2, x2 × y2)
end.
Definition addq '(Rat x xP) '(Rat y yP) := fracq (addq_subdef x y).
Lemma addq_def x y : addq x y = fracq (addq_subdef (valq x) (valq y)).
Lemma addq_subdefE x y : addq_subdef x y = (x.1 × y.2 + y.1 × x.2, x.2 × y.2).
Definition oppq_subdef (x : int × int) := (- x.1, x.2).
Definition oppq '(Rat x xP) := fracq (oppq_subdef x).
Definition oppq_def x : oppq x = 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 mulq_subdef (x y : int × int) :=
let: (x1, x2) := x in
let: (y1, y2) := y in
match x2, y2 with
| Posz 1, Posz 1 ⇒ (x1 × y1, 1)
| Posz 1, _ ⇒ (x1 × y1, y2)
| _, Posz 1 ⇒ (x1 × y1, x2)
| _, _ ⇒ (x1 × y1, x2 × y2)
end.
Definition mulq '(Rat x xP) '(Rat y yP) := fracq (mulq_subdef x y).
Lemma mulq_def x y : mulq x y = fracq (mulq_subdef (valq x) (valq y)).
Lemma mulq_subdefE x y : mulq_subdef x y = (x.1 × y.1, x.2 × y.2).
Fact mulq_subdefC : commutative mulq_subdef.
Fact mul_subdefA : associative mulq_subdef.
Definition invq_subdef (x : int × int) := (x.2, x.1).
Definition invq '(Rat x xP) := fracq (invq_subdef x).
Lemma invq_def x : invq x = 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.
Fact mulVq x : x != 0 → mulq (invq x) x = 1.
Fact invq0 : invq 0 = 0.
Lemma numq_eq0 x : (numq x == 0) = (x == 0).
Notation "n %:Q" := ((n : int)%:~R : rat) : ring_scope.
#[global] 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)).
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.
let: (x1, x2) := x in
let: (y1, y2) := y in
match x2, y2 with
| Posz 1, Posz 1 ⇒
match x1, y1 with
| Posz 0, _ ⇒ (y1, 1)
| _, Posz 0 ⇒ (x1, 1)
| Posz n, Posz 1 ⇒ (Posz n.+1, 1)
| Posz 1, Posz n ⇒ (Posz n.+1, 1)
| _, _ ⇒ (x1 + y1, 1)
end
| Posz 1, _ ⇒ (x1 × y2 + y1, y2)
| _, Posz 1 ⇒ (x1 + y1 × x2, x2)
| _, _ ⇒ (x1 × y2 + y1 × x2, x2 × y2)
end.
Definition addq '(Rat x xP) '(Rat y yP) := fracq (addq_subdef x y).
Lemma addq_def x y : addq x y = fracq (addq_subdef (valq x) (valq y)).
Lemma addq_subdefE x y : addq_subdef x y = (x.1 × y.2 + y.1 × x.2, x.2 × y.2).
Definition oppq_subdef (x : int × int) := (- x.1, x.2).
Definition oppq '(Rat x xP) := fracq (oppq_subdef x).
Definition oppq_def x : oppq x = 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 mulq_subdef (x y : int × int) :=
let: (x1, x2) := x in
let: (y1, y2) := y in
match x2, y2 with
| Posz 1, Posz 1 ⇒ (x1 × y1, 1)
| Posz 1, _ ⇒ (x1 × y1, y2)
| _, Posz 1 ⇒ (x1 × y1, x2)
| _, _ ⇒ (x1 × y1, x2 × y2)
end.
Definition mulq '(Rat x xP) '(Rat y yP) := fracq (mulq_subdef x y).
Lemma mulq_def x y : mulq x y = fracq (mulq_subdef (valq x) (valq y)).
Lemma mulq_subdefE x y : mulq_subdef x y = (x.1 × y.1, x.2 × y.2).
Fact mulq_subdefC : commutative mulq_subdef.
Fact mul_subdefA : associative mulq_subdef.
Definition invq_subdef (x : int × int) := (x.2, x.1).
Definition invq '(Rat x xP) := fracq (invq_subdef x).
Lemma invq_def x : invq x = 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.
Fact mulVq x : x != 0 → mulq (invq x) x = 1.
Fact invq0 : invq 0 = 0.
Lemma numq_eq0 x : (numq x == 0) = (x == 0).
Notation "n %:Q" := ((n : int)%:~R : rat) : ring_scope.
#[global] 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)).
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_deprecated (nx dx ny dy : rat) :
dx != 0 → dy != 0 → (nx / dx == ny / dy) = (nx × dy == ny × dx).
#[deprecated(since="mathcomp 1.13.0", note="Use eqr_div instead.")]
Notation divq_eq := divq_eq_deprecated (only parsing).
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 '(Rat x _) : rat := `|x.1|%:~R / (x.2)%:~R.
Definition le_rat '(Rat x _) '(Rat y _) := x.1 × y.2 ≤ y.1 × x.2.
Definition lt_rat '(Rat x _) '(Rat y _) := x.1 × y.2 < y.1 × x.2.
Lemma normqE x : normq x = `|numq x|%:~R / (denq x)%:~R.
Lemma le_ratE x y : le_rat x y = (numq x × denq y ≤ numq y × denq x).
Lemma lt_ratE x y : lt_rat x y = (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).
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].
Section QintPred.
Definition Qint_pred := fun x : rat ⇒ denq x == 1.
Arguments Qint_pred _ /.
Definition Qint := [qualify a x : rat | Qint_pred x].
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.
End QintPred.
Arguments Qint_pred _ /.
Section QnatPred.
Definition Qnat_pred := fun x : rat ⇒ (x \is a Qint) && (0 ≤ x).
Arguments Qnat_pred _ /.
Definition Qnat := [qualify a x | Qnat_pred x].
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.
End QnatPred.
Arguments Qnat_pred _ /.
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 : divringClosed R) a : ratr a \in S.
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 → scalable f.
End Linear.
Section InPrealField.
Variable F : numFieldType.
Fact ratr_is_additive : additive (@ratr F).
Fact ratr_is_multiplicative : multiplicative (@ratr F).
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|.
Lemma minr_rat : {morph ratr F : x y / Num.min x y}.
Lemma maxr_rat : {morph ratr F : x y / Num.max x y}.
End InPrealField.
Arguments ratr {R}.
Lemma divq_eq_deprecated (nx dx ny dy : rat) :
dx != 0 → dy != 0 → (nx / dx == ny / dy) = (nx × dy == ny × dx).
#[deprecated(since="mathcomp 1.13.0", note="Use eqr_div instead.")]
Notation divq_eq := divq_eq_deprecated (only parsing).
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 '(Rat x _) : rat := `|x.1|%:~R / (x.2)%:~R.
Definition le_rat '(Rat x _) '(Rat y _) := x.1 × y.2 ≤ y.1 × x.2.
Definition lt_rat '(Rat x _) '(Rat y _) := x.1 × y.2 < y.1 × x.2.
Lemma normqE x : normq x = `|numq x|%:~R / (denq x)%:~R.
Lemma le_ratE x y : le_rat x y = (numq x × denq y ≤ numq y × denq x).
Lemma lt_ratE x y : lt_rat x y = (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).
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].
Section QintPred.
Definition Qint_pred := fun x : rat ⇒ denq x == 1.
Arguments Qint_pred _ /.
Definition Qint := [qualify a x : rat | Qint_pred x].
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.
End QintPred.
Arguments Qint_pred _ /.
Section QnatPred.
Definition Qnat_pred := fun x : rat ⇒ (x \is a Qint) && (0 ≤ x).
Arguments Qnat_pred _ /.
Definition Qnat := [qualify a x | Qnat_pred x].
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.
End QnatPred.
Arguments Qnat_pred _ /.
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 : divringClosed R) a : ratr a \in S.
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 → scalable f.
End Linear.
Section InPrealField.
Variable F : numFieldType.
Fact ratr_is_additive : additive (@ratr F).
Fact ratr_is_multiplicative : multiplicative (@ratr F).
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|.
Lemma minr_rat : {morph ratr F : x y / Num.min x y}.
Lemma maxr_rat : {morph ratr F : x y / Num.max x y}.
End InPrealField.
Arguments ratr {R}.
Connecting rationals to the ring and 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.
Pretty printing or normal element of rat.
For debugging purposes we provide the parsable version
Notation "[ 'rat' x // y ]" :=
(@Rat (x : int, y : int) (fracq_subproof (x : int, y : int))) : ring_scope.
(@Rat (x : int, y : int) (fracq_subproof (x : int, y : int))) : ring_scope.
A specialization of vm_compute rewrite rule for pattern _%