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 archimedean.
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 archimedean.
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)
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.
Local Notation sgr := Num.sg.
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.
Number Notation rat parse print (via Irat
mapping [Rat ⇒ IRat, fracq_subproof ⇒ Ifracq_subproof])
: rat_scope.
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.
Number Notation rat parse print (via Irat
mapping [Rat ⇒ IRat, fracq_subproof ⇒ Ifracq_subproof])
: rat_scope.
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 _%:Q / _%:Q
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).
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.
Module ratArchimedean.
Section ratArchimedean.
Implicit Types x : rat.
Let trunc x : nat := if 0 ≤ x then (`|numq x| %/ `|denq x|)%N else 0%N.
Lemma truncP x :
if 0 ≤ x then (trunc x)%:R ≤ x < (trunc x).+1%:R else trunc x == 0%N.
Let is_nat x := (0 ≤ x) && (denq x == 1).
Lemma is_natE x : is_nat x = ((trunc x)%:R == x).
Lemma is_intE x : (denq x == 1) = is_nat x || is_nat (- x).
End ratArchimedean.
End ratArchimedean.
Lemma Qint_def (x : rat) : (x \is a Num.int) = (denq x == 1).
Lemma numqK : {in Num.int, cancel (fun x ⇒ numq x) intr}.
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.
Section InParchiField.
Variable F : archiNumFieldType.
Lemma floor_rat : {mono (@ratr F) : x / Num.floor x}.
Lemma ceil_rat : {mono (@ratr F) : x / Num.ceil x}.
End InParchiField.
Arguments ratr {R}.
Lemma divq_eq_deprecated (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 '(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.
Module ratArchimedean.
Section ratArchimedean.
Implicit Types x : rat.
Let trunc x : nat := if 0 ≤ x then (`|numq x| %/ `|denq x|)%N else 0%N.
Lemma truncP x :
if 0 ≤ x then (trunc x)%:R ≤ x < (trunc x).+1%:R else trunc x == 0%N.
Let is_nat x := (0 ≤ x) && (denq x == 1).
Lemma is_natE x : is_nat x = ((trunc x)%:R == x).
Lemma is_intE x : (denq x == 1) = is_nat x || is_nat (- x).
End ratArchimedean.
End ratArchimedean.
Lemma Qint_def (x : rat) : (x \is a Num.int) = (denq x == 1).
Lemma numqK : {in Num.int, cancel (fun x ⇒ numq x) intr}.
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.
Section InParchiField.
Variable F : archiNumFieldType.
Lemma floor_rat : {mono (@ratr F) : x / Num.floor x}.
Lemma ceil_rat : {mono (@ratr F) : x / Num.ceil x}.
End InParchiField.
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 _%:Q
Lemma rat_vm_compute n (x : rat) : vm_compute_eq n%:Q x → n%:Q = x.
Module mc_2_0.
Local Notation Qint := (Num.int : qualifier 1 rat) (only parsing).
Local Notation Qnat := (Num.nat : qualifier 1 rat) (only parsing).
Local Lemma QintP (x : rat) : reflect (∃ z, x = z%:~R) (x \in Qint).
Local Lemma Qnat_def (x : rat) : (x \is a Qnat) = (x \is a Qint) && (0 ≤ x).
Local Lemma QnatP x : reflect (∃ n : nat, x = n%:R) (x \in Qnat).
End mc_2_0.
#[deprecated(since="mathcomp 2.1.0", note="Use Num.int instead.")]
Notation Qint := (Num.int : qualifier 1 rat) (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use Num.nat instead.")]
Notation Qnat := (Num.nat : qualifier 1 rat) (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intrP instead.")]
Notation QintP := mc_2_0.QintP (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natrEint instead.")]
Notation Qnat_def := mc_2_0.Qnat_def (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natrP instead.")]
Notation QnatP := mc_2_0.QnatP (only parsing).
Module mc_2_0.
Local Notation Qint := (Num.int : qualifier 1 rat) (only parsing).
Local Notation Qnat := (Num.nat : qualifier 1 rat) (only parsing).
Local Lemma QintP (x : rat) : reflect (∃ z, x = z%:~R) (x \in Qint).
Local Lemma Qnat_def (x : rat) : (x \is a Qnat) = (x \is a Qint) && (0 ≤ x).
Local Lemma QnatP x : reflect (∃ n : nat, x = n%:R) (x \in Qnat).
End mc_2_0.
#[deprecated(since="mathcomp 2.1.0", note="Use Num.int instead.")]
Notation Qint := (Num.int : qualifier 1 rat) (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use Num.nat instead.")]
Notation Qnat := (Num.nat : qualifier 1 rat) (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use intrP instead.")]
Notation QintP := mc_2_0.QintP (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natrEint instead.")]
Notation Qnat_def := mc_2_0.Qnat_def (only parsing).
#[deprecated(since="mathcomp 2.1.0", note="Use natrP instead.")]
Notation QnatP := mc_2_0.QnatP (only parsing).