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 prime.
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 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 _).
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.
#[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 rat_ZmodMixin := ZmodMixin addqA addqC add0q addNq.
Canonical rat_ZmodType := ZmodType rat rat_ZmodMixin.
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.
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) : 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 rat_ZmodMixin := ZmodMixin addqA addqC add0q addNq.
Canonical rat_ZmodType := ZmodType rat rat_ZmodMixin.
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.
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) : 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).
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).
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|.
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).
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).
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|.
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}.
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.
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 _%