(Joint Center)Library MathComp.rat

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
Require Import bigop ssralg div ssrnum ssrint.

This file defines a datatype for rational numbers and equips it with a structure of archimedean, real field, with int and nat declared as closed subrings. rat == the type of rational number, with single constructor Rat 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.
Local Notation sgr := Num.sg.

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 × intratType :=
  | 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.

Will be subsumed by pnatr_eq0
Fact intq_eq0 n : (n%:~R == 0 :> rat) = (n == 0)%N.

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.

CoInductive divq_spec (n d : int) : intintratType :=
| 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) *) : ratintintType :=
  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 xle_rat 0 yle_rat 0 (x + y).

Fact le_rat0M x y : le_rat 0 xle_rat 0 yle_rat 0 (x × y).

Fact le_rat0_anti x : le_rat 0 xle_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 xnormq 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 xnumq 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 aRrR}) a :
  f (ratr _ a) = ratr _ a.

Lemma fmorph_eq_rat rR (f : {rmorphism ratrR}) : f =1 ratr _.

End Fmorph.

Section Linear.

Implicit Types (U V : lmodType rat) (A B : lalgType rat).

Lemma rat_linear U V (f : UV) : additive flinear f.

Lemma rat_lrmorphism A B (f : AB) : rmorphism flrmorphism 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.