open import 1Lab.Prelude

open import Algebra.Ring.Commutative
open import Algebra.Monoid

open import Data.Rational.Reflection
open import Data.Rational.Order
open import Data.Rational.Base
open import Data.Nat.Base hiding (Positive ; _<_ ; _≀_)

import Algebra.Ring.Reasoning as Kit

import Data.Int.Properties as β„€
import Data.Int.Order as β„€
import Data.Int.Base as β„€
module Data.Rational.Properties where

Misc. properties of the rationalsπŸ”—

private module β„šr = Kit (β„š-ring .fst , record { CRing-on (β„š-ring .snd) })
open β„šr renaming (*-negater to *β„š-negater ; *-negatel to *β„š-negatel) using () public

abstract

Properties of multiplicationπŸ”—

  *β„š-distrib-minusr : βˆ€ {x y z} β†’ (y -β„š z) *β„š x ≑ y *β„š x -β„š z *β„š x
  *β„š-distrib-minusr {x@(inc _)} {y@(inc _)} {z@(inc _)} = *β„š-distribr x y (-β„š z) βˆ™ apβ‚‚ _+β„š_ (Ξ» i β†’ y *β„š x) (β„šr.*-negatel {z} {x})

  *β„š-distrib-minusl : βˆ€ {x y z} β†’ x *β„š (y -β„š z) ≑ x *β„š y -β„š x *β„š z
  *β„š-distrib-minusl = *β„š-commutative _ _ βˆ™ *β„š-distrib-minusr βˆ™ apβ‚‚ _-β„š_ (*β„š-commutative _ _) (*β„š-commutative _ _)

  *β„š-invl : βˆ€ {x} ⦃ p : Nonzero x ⦄ β†’ invβ„š x *β„š x ≑ 1
  *β„š-invl = *β„š-commutative _ _ βˆ™ *β„š-invr

Nonzero rationalsπŸ”—

  /β„š-def : {x y : β„š} ⦃ p : Nonzero y ⦄ β†’ (x /β„š y) ≑ x *β„š invβ„š y
  /β„š-def {inc x} {inc y} = refl

  *β„š-nonzero : βˆ€ {x y} β†’ Nonzero x β†’ Nonzero y β†’ Nonzero (x *β„š y)
  /β„š-nonzero-num : βˆ€ {n d} ⦃ p : Nonzero d ⦄ β†’ Nonzero (n /β„š d) β†’ Nonzero n
  negβ„š-nonzero : βˆ€ {n} β†’ Nonzero n β†’ Nonzero (-β„š n)
  invβ„š-nonzero : βˆ€ {n} ⦃ d : Nonzero n ⦄ β†’ Nonzero (invβ„š n)

  unquoteDef *β„š-nonzero /β„š-nonzero-num negβ„š-nonzero invβ„š-nonzero = do
    by-elim-β„š *β„š-nonzero Ξ» d a b Ξ± Ξ² β†’
      to-nonzero-frac (β„€.*β„€-nonzero (from-nonzero-frac Ξ±) (from-nonzero-frac Ξ²))

    by-elim-β„š /β„š-nonzero-num Ξ» where
      d x β„€.posz ⦃ p ⦄ nz β†’ absurd (from-nonzero-frac p refl)
      d x (β„€.possuc y) nz β†’ to-nonzero-frac (β„€.*β„€-nonzero-cancel {x} {d} (from-nonzero-frac nz))
      (β„€.possuc x) ⦃ β„€.pos .x ⦄ y (β„€.negsuc z) nz β†’ to-nonzero-frac (β„€.*β„€-nonzero-cancel {y} {β„€.negsuc x} (from-nonzero-frac nz))

    by-elim-β„š negβ„š-nonzero Ξ» where
      d β„€.posz (inc Ξ±) β†’ absurd (Ξ± (quotβ„š (to-same-rational refl)))
      d (℀.possuc x) (inc α) → to-nonzero-frac ℀.negsuc≠pos
      d (β„€.negsuc x) (inc Ξ±) β†’ to-nonzero-frac (sucβ‰ zero ∘ β„€.pos-injective)

    by-elim-β„š invβ„š-nonzero Ξ» where
      d β„€.posz ⦃ inc Ξ± ⦄ β†’ absurd (Ξ± (quotβ„š (to-same-rational refl)))
      (β„€.possuc d) ⦃ β„€.pos .d ⦄ (β„€.possuc x) ⦃ inc Ξ± ⦄ β†’ to-nonzero-frac (sucβ‰ zero ∘ β„€.pos-injective)
      (β„€.possuc d) ⦃ β„€.pos .d ⦄ (β„€.negsuc x) ⦃ inc Ξ± ⦄ β†’ to-nonzero-frac β„€.negsucβ‰ pos

  instance
    Nonzero-*β„š : βˆ€ {x y : β„š} ⦃ p : Nonzero x ⦄ ⦃ q : Nonzero y ⦄ β†’ Nonzero (x *β„š y)
    Nonzero-*β„š ⦃ p ⦄ ⦃ q ⦄ = *β„š-nonzero p q

    Nonzero-invβ„š : βˆ€ {x} ⦃ p : Nonzero x ⦄ β†’ Nonzero (invβ„š x)
    Nonzero-invβ„š ⦃ p ⦄ = invβ„š-nonzero ⦃ p ⦄

    Nonzero-/β„š : βˆ€ {x y} ⦃ p : Nonzero x ⦄ ⦃ q : Nonzero y ⦄ β†’ Nonzero (x /β„š y)
    Nonzero-/β„š {x} {y} ⦃ p ⦄ ⦃ q ⦄ = subst Nonzero (sym /β„š-def) (*β„š-nonzero p invβ„š-nonzero)

    {-# OVERLAPPABLE Nonzero-*β„š Nonzero-invβ„š Nonzero-/β„š #-}

Properties of divisionπŸ”—

  /β„š-oner : βˆ€ x β†’ x /β„š 1 ≑ x
  /β„š-oner (inc x) = *β„š-idr (inc x)

  /β„š-ap : βˆ€ {x y x' y'} {p : Nonzero y} {q : Nonzero y'} β†’ x ≑ x' β†’ y ≑ y' β†’ (_/β„š_ x y ⦃ p ⦄) ≑ (_/β„š_ x' y' ⦃ q ⦄)
  /β„š-ap {p = Ξ±} {Ξ²} p q i = _/β„š_ (p i) (q i) ⦃ is-propβ†’pathp (Ξ» i β†’ hlevel {T = Nonzero (q i)} 1) Ξ± Ξ² i ⦄

  /β„š-factorr : βˆ€ {x y} ⦃ p : Nonzero y ⦄ β†’ (x *β„š y) /β„š y ≑ x
  /β„š-factorr = /β„š-def βˆ™ sym (*β„š-associative _ _ _) βˆ™ apβ‚‚ _*β„š_ refl *β„š-invr βˆ™ *β„š-idr _

  /β„š-self : βˆ€ {x} ⦃ p : Nonzero x ⦄ β†’ x /β„š x ≑ 1
  /β„š-self {x} = /β„š-def βˆ™ *β„š-invr

  /β„š-factorl : βˆ€ {x y} ⦃ p : Nonzero y ⦄ β†’ (y *β„š x) /β„š y ≑ x
  /β„š-factorl = /β„š-ap (*β„š-commutative _ _) refl βˆ™ /β„š-factorr

  /β„š-scaler : βˆ€ {x y z} ⦃ p : Nonzero y ⦄ β†’ (x /β„š y) *β„š z ≑ (x *β„š z) /β„š y
  /β„š-scaler = ap (_*β„š _) /β„š-def βˆ™ sym (*β„š-associative _ _ _) βˆ™ ap (_ *β„š_) (*β„š-commutative _ _) βˆ™ *β„š-associative _ _ _ βˆ™ sym /β„š-def

  /β„š-scalel : βˆ€ {x y z} ⦃ p : Nonzero z ⦄ β†’ x *β„š (y /β„š z) ≑ (x *β„š y) /β„š z
  /β„š-scalel {z = z} = *β„š-commutative _ _ βˆ™ /β„š-scaler βˆ™ ap (Ξ» e β†’ e /β„š z) (*β„š-commutative _ _)

  /β„š-cross : βˆ€ {q q' d} ⦃ Ξ± : Nonzero d ⦄ β†’ q *β„š d ≑ q' β†’ q ≑ (q' /β„š d)
  /β„š-cross {d = d} p = sym (ap (Ξ» e β†’ (e /β„š d) ⦃ _ ⦄) (sym p) βˆ™ /β„š-factorr)

  /β„š-same
    : βˆ€ {q q' d d'} ⦃ Ξ± : Nonzero d ⦄ ⦃ Ξ² : Nonzero d' ⦄
    β†’ q *β„š d' ≑ q' *β„š d β†’ q /β„š d ≑ q' /β„š d'
  /β„š-same p = /β„š-cross (/β„š-scaler βˆ™ sym (/β„š-cross (sym p)))

  /β„š-frac
    : βˆ€ {n d} ⦃ p : β„€.Positive d ⦄
    β†’ (n / 1) /β„š (d / 1) ≑ (n / d)
  /β„š-frac {n} {d = β„€.possuc x} ⦃ p = β„€.pos x ⦄ = quotβ„š (to-same-rational (sym (β„€.*β„€-associative n 1 (β„€.possuc x))))

  invβ„š-*β„š
    : βˆ€ {d d'} ⦃ p : Nonzero d ⦄ ⦃ p' : Nonzero d' ⦄
    β†’ invβ„š (d *β„š d') ≑ invβ„š d *β„š invβ„š d'
  invβ„š-*β„š {d} {d'} = monoid-inverse-unique *β„š-monoid (d *β„š d') _ _ *β„š-invl
    (sym (*β„š-associative _ _ _) βˆ™ ap (d *β„š_)
      (ap (d' *β„š_) (*β„š-commutative _ _)
      βˆ™ *β„š-associative d' _ _
      βˆ™ ap (_*β„š invβ„š d) *β„š-invr βˆ™ *β„š-idl (invβ„š d))
    βˆ™ *β„š-invr {d})

  invβ„š-invβ„š : βˆ€ {d} ⦃ p : Nonzero d ⦄ β†’ invβ„š (invβ„š d) ≑ d
  invβ„š-invβ„š {d} = monoid-inverse-unique *β„š-monoid (invβ„š d) _ _ (*β„š-commutative _ _ βˆ™ *β„š-invr) (*β„š-commutative _ _ βˆ™ *β„š-invr)

  invβ„š-/β„š
    : βˆ€ {q d} ⦃ p : Nonzero d ⦄ ⦃ p' : Nonzero q ⦄
    β†’ invβ„š (q /β„š d) ≑ (d /β„š q)
  invβ„š-/β„š = apβ‚‚ (Ξ» e p β†’ invβ„š e ⦃ p ⦄) /β„š-def prop! βˆ™ invβ„š-*β„š βˆ™ apβ‚‚ _*β„š_ refl invβ„š-invβ„š βˆ™ *β„š-commutative _ _ βˆ™ sym /β„š-def

  /β„š-negatel
    : βˆ€ {q d} ⦃ p : Nonzero d ⦄ β†’ -β„š (q /β„š d) ≑ (-β„š q) /β„š d
  /β„š-negatel = ap -β„š_ /β„š-def Β·Β· sym *β„š-negatel Β·Β· sym /β„š-def

  /β„š-def-+β„š
    : βˆ€ {q q' d d'} ⦃ p : Nonzero d ⦄ ⦃ p' : Nonzero d' ⦄
    β†’ (q /β„š d) +β„š (q' /β„š d') ≑ ((q *β„š d' +β„š q' *β„š d) /β„š (d *β„š d'))
  /β„š-def-+β„š {d = d} {d'} = /β„š-cross
    (*β„š-distribr _ _ _ βˆ™ apβ‚‚ _+β„š_
      (/β„š-scaler βˆ™ ap (Ξ» e β†’ e /β„š d) (ap (_ *β„š_) (*β„š-commutative d d') βˆ™ *β„š-associative _ d' d) βˆ™ /β„š-factorr)
      (/β„š-scaler βˆ™ ap (Ξ» e β†’ e /β„š d') (*β„š-associative _ d d') βˆ™ /β„š-factorr))

  /β„š-def-subβ„š
    : βˆ€ {q q' d d'} ⦃ p : Nonzero d ⦄ ⦃ p' : Nonzero d' ⦄
    β†’ (q /β„š d) -β„š (q' /β„š d') ≑ ((q *β„š d' -β„š q' *β„š d) /β„š (d *β„š d'))
  /β„š-def-subβ„š {d = d} {d'} = /β„š-cross
    (*β„š-distrib-minusr βˆ™ apβ‚‚ _-β„š_
      (/β„š-scaler βˆ™ ap (Ξ» e β†’ e /β„š d) (ap (_ *β„š_) (*β„š-commutative d d') βˆ™ *β„š-associative _ d' d) βˆ™ /β„š-factorr)
      (/β„š-scaler βˆ™ ap (Ξ» e β†’ e /β„š d') (*β„š-associative _ d d') βˆ™ /β„š-factorr))

  /β„š-def-*β„š
    : βˆ€ {q q' d d'} ⦃ p : Nonzero d ⦄ ⦃ p' : Nonzero d' ⦄
    β†’ (q /β„š d) *β„š (q' /β„š d') ≑ (q *β„š q') /β„š (d *β„š d')
  /β„š-def-*β„š {d = d} {d'} = /β„š-cross
    (sym (*β„š-associative _ _ _)
      βˆ™ ap (_ *β„š_) (/β„š-scaler βˆ™ ap (Ξ» e β†’ e /β„š d') (*β„š-associative _ d d') βˆ™ /β„š-factorr)
      βˆ™ /β„š-scaler βˆ™ ap (Ξ» e β†’ e /β„š d) (*β„š-associative _ _ d) βˆ™ /β„š-factorr)

PositivityπŸ”—

abstract
  *β„š-positive : βˆ€ {x y} β†’ Positive x β†’ Positive y β†’ Positive (x *β„š y)
  +β„š-positive : βˆ€ {x y} β†’ Positive x β†’ Positive y β†’ Positive (x +β„š y)
  +β„š-nonneg-positive : βˆ€ {x y} β†’ 0 ≀ x β†’ Positive y β†’ Positive (x +β„š y)
  invβ„š-positive : βˆ€ {d} (p : Positive d) β†’ Positive (invβ„š d ⦃ inc (positiveβ†’nonzero p) ⦄)

  unquoteDef *β„š-positive +β„š-positive invβ„š-positive +β„š-nonneg-positive = do
    by-elim-β„š *β„š-positive Ξ» d a b (inc x) (inc y) β†’ inc (β„€.*β„€-positive x y)
    by-elim-β„š +β„š-positive Ξ» d a b (inc x) (inc y) β†’ inc (β„€.+β„€-positive (β„€.*β„€-positive x auto) (β„€.*β„€-positive y auto))
    by-elim-β„š invβ„š-positive Ξ» where
      d@(β„€.possuc d') ⦃ β„€.pos .d' ⦄ (β„€.possuc x) px β†’ inc (β„€.pos d')

    by-elim-β„š +β„š-nonneg-positive Ξ» where
      d (β„€.posz) b (inc x) (inc y) β†’ inc (subst β„€.Positive (sym (β„€.+β„€-zerol (b β„€.*β„€ d))) (β„€.*β„€-positive y auto))
      d (β„€.possuc a) b (inc x) (inc y) β†’ inc (β„€.+β„€-positive {β„€.possuc a β„€.*β„€ d} {b β„€.*β„€ d} (β„€.*β„€-positive (β„€.pos a) auto) (β„€.*β„€-positive y auto))

  /β„š-positive : βˆ€ {x y} (p : Positive x) (q : Positive y) β†’ Positive ((x /β„š y) ⦃ inc (positiveβ†’nonzero q) ⦄)
  /β„š-positive {y = y} p q = subst Positive
    (sym (/β„š-def ⦃ _ ⦄)) (*β„š-positive p (invβ„š-positive q))

  from-positive : βˆ€ {x} β†’ Positive x β†’ 0 < x
  to-positive : βˆ€ {x} β†’ 0 < x β†’ Positive x

  unquoteDef from-positive to-positive = do
    by-elim-β„š from-positive Ξ» where
      d (β„€.possuc x) (inc (β„€.pos .x)) β†’ inc (β„€.pos<pos (s≀s 0≀x))

    by-elim-β„š to-positive Ξ» where
      d (β„€.pos zero) (inc p) β†’ inc (absurd (β„€.<-irrefl refl p))
      d (β„€.pos (suc x)) (inc p) β†’ inc (β„€.pos x)

  absβ„š-nonneg : βˆ€ {x} β†’ 0 ≀ absβ„š x
  unquoteDef absβ„š-nonneg = by-elim-β„š absβ„š-nonneg Ξ» where
    d (β„€.pos x) β†’ inc (β„€.apos≀apos {0} {x * 1} 0≀x)
    d (β„€.negsuc x) β†’ inc (β„€.pos≀pos 0≀x)
abstract
  negβ„š-anti-< : βˆ€ {x y} β†’ x < y β†’ -β„š y < -β„š x
  negβ„š-anti-full-< : βˆ€ {x y} β†’ -β„š x < -β„š y β†’ y < x

  unquoteDef negβ„š-anti-< negβ„š-anti-full-< = do
    by-elim-β„š negβ„š-anti-< Ξ» d x y Ξ± β†’ common-denom-< (β„€.negβ„€-anti-< (<-common-denom Ξ±))
    by-elim-β„š negβ„š-anti-full-< Ξ» d x y Ξ± β†’ common-denom-< (β„€.negβ„€-anti-full-< (<-common-denom Ξ±))