(Joint Center)Library rat

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
Require Import bigop ssralg div ssrnum ssrint.

This file defines the rational numbers rat == the type of rational number, with the constructor Rat that takes a pair of integers p and a proof of (0 < p.2) && coprime `|p.1| `|p.2| n%:Q == explicit cast from int to rat
The type rat has an archimedian field structure with int and nat being closed subrings

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 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 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.