Rat.effective

-- intNonZero first, to fix the elaboration order of the transitive
-- imports (docs/ProvingFeedback.md B-8)
-- ℚ IS EFFECTIVE: equal classes give cross-multiplication back.
--
-- Core/quotEffective.nova asks for one thing — that the relation be an
-- equivalence. For RatR only transitivity is real work, and it is the
-- usual argument: multiply through by the middle denominator and
-- CANCEL it. Cancellation in ℤ is where Int/nonZero.nova's
-- no-zero-divisors finally pays off a second time.
--
-- The corollary is the converse that was out of reach before: a
-- rational built from a non-zero numerator is not zero, so qOfNzq's
-- image is exactly the non-zero rationals.
-- ===== cancellation in ℤ =====

import Int.nonZero (nzOfInt, nzToIntNonZero, intNoZeroDiv)
import Int (Int, intZero, intOne, intNeg)
import Int.add (+, intAddAssoc)
import Int.mul (*, intMulComm, intMulAssoc, intMulOneR, intMulZeroL, intMulDistribR, intMulNegL, intAddNegL, intAddNegR, intAddCong2, intMulCong2)
import Core.prop (¬, ⊥, ↔, iffIntro, absurdP)
import Rat.frac (NZ, nzToInt, nzOne, Rat, mkRat, num, den, ratZero, ratOne, intAddZeroL, intAddZeroR)
import Rat (Q, qcls, qZero, qOne, *, qMulZeroL, RatR, dInt, clsEqOfRel, mulCongL, mulCongR, NZQ, qOfNzq, nzqToRat, nzToIntMul)
import Rat.inv (notIntro, notApply, numNonZero, ratZeroOfNumZero, qNonZeroIsNzq, qInvExists)
import Core.quotEffective (effectiveAtEquiv)
import Core.equality (trans, sym, cong)

addCongL : {x y z : Int} → (x ≡ y) → x + z ≡ y + z using (Int.Int.unfold, Int.mul.intAddCong2)
addCongL = λx y z h. ⋆

addCongR : {x y z : Int} → (y ≡ z) → x + y ≡ x + z using (Int.Int.unfold, Int.mul.intAddCong2)
addCongR = λx y z h. ⋆

-- x·d ≡ y·d with d ≠ 0 gives x ≡ y: the difference times d is zero,
-- so the difference is zero
intMulCancel : (x y d : Int) (h : x * d ≡ y * d) (hd : ¬ (d ≡ intZero)) → x ≡ y
  using (intAddNegL, intMulNegL, intAddZeroL, intAddZeroR)
intMulCancel =
  λx y d h hd. sym
    _
    _
    trans
      _
      _
      _
      sym _ _ (intAddZeroL y)
      trans
        {Int}
        intZero + y
        x + intNeg y + y
        _
        addCongL
          sym
            _
            _
            intNoZeroDiv
              _
              trans
                _
                _
                _
                intMulDistribR x (intNeg y) d
                trans _ _ _ (intAddCong2 _ _ _ _ h (intMulNegL y d)) (intAddNegR (y * d))
              hd
        trans
          _
          _
          _
          intAddAssoc x (intNeg y) y
          trans {Int} (x + (intNeg y + y)) (x + intZero) _ (addCongR (intAddNegL y)) (intAddZeroR x)

-- ===== RatR is an equivalence =====
-- (a·b)·c ≡ (a·c)·b, the one rearrangement transitivity needs
-- (a·b)·c ≡ (a·c)·b, the one rearrangement transitivity needs — a
-- calc chain: only tier-0/½ conversion is implicit, every step a
-- named link, no holes
mulSwapRight : {a b c : Int} → a * b * c ≡ a * c * b using (Int.Int.unfold)
mulSwapRight =
  λa b c. a * b * c
    ≡⟨ intMulAssoc a b c ⟩ a * (b * c)
    ≡⟨ mulCongR a _ _ (intMulComm b c) ⟩ a * (c * b)
    ≡⟨ intMulAssoc a c b ⟩ a * c * b

ratRRefl : (p : Rat) → RatR p p using (Rat.RatR.unfold)
ratRRefl = λp. ⋆

ratRSymm : (p q : Rat) → RatR p q → RatR q p
  using (Int.Int.eq,
    Int.Int.unfold,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.num.eq,
    Rat.RatR.eq,
    Rat.RatR.unfold,
    Rat.dInt.eq)
ratRSymm = λp q h. sym {Int} (num p * dInt q) (num q * dInt p) h

-- multiply the goal through by the middle denominator, walk it across
-- the two hypotheses, and cancel — the middle denominator is non-zero
-- because it is the image of an NZ
ratRTrans : (p q r : Rat) → RatR p q → RatR q r → RatR p r
  using (intMulAssoc,
    Int.Int.eq,
    Int.Int.unfold,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.num.eq,
    Rat.frac.nzToInt.eq,
    Rat.RatR.eq,
    Rat.RatR.unfold,
    Rat.dInt.eq)
ratRTrans =
  λp q r h1 h2. intMulCancel
    _
    _
    _
    trans
      num p * dInt r * dInt q
      _
      _
      mulSwapRight
      trans
        _
        _
        _
        mulCongL (num p * dInt q) (num q * dInt p) (dInt r) h1
        trans
          num q * dInt p * dInt r
          _
          _
          mulSwapRight
          trans
            _
            _
            num r * dInt p * dInt q
            mulCongL (num q * dInt r) (num r * dInt q) (dInt p) h2
            mulSwapRight
    nzToIntNonZero (den q)

-- ===== effectivity =====
qEffective : (p q : Rat) → (class p ≡ class q ∈ Q) → RatR p q
  using (Int.Int.unfold, Rat.frac.NZ.unfold, Rat.frac.Rat.unfold, Rat.Q.unfold, Rat.RatR.unfold)
qEffective = effectiveAtEquiv RatR ratRRefl ratRTrans ratRSymm

-- the converse of Rat/inv.nova's ratZeroOfNumZero, which needed
-- effectivity and so could not be stated until now
numZeroOfRatZero : (p : Rat) (h : class p ≡ qZero) → num p ≡ intZero
  using (intMulOneR,
    intMulZeroL,
    Int.Int.eq,
    Int.Int.unfold,
    Int.intOne.eq,
    Int.intZero.eq,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzOne.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratZero.eq,
    Rat.Q.unfold,
    Rat.RatR.eq,
    Rat.dInt.eq,
    Rat.qZero.eq,
    Rat.qcls.eq)
numZeroOfRatZero =
  λp h. trans
    _
    num p * dInt ratZero
    _
    sym _ _ (intMulOneR (num p))
    trans
      num p * dInt ratZero
      num ratZero * dInt p
      intZero
      qEffective _ ratZero h
      intMulZeroL (dInt p)

numZeroIff : (p : Rat) → (class p ≡ qZero) ↔ (num p ≡ intZero)
  using (Core.prop.↔.unfold, Core.prop.∧.unfold, Rat.Q.unfold)
numZeroIff = λp. iffIntro (numZeroOfRatZero p) (ratZeroOfNumZero p)

-- ===== the image of NZQ is exactly the non-zero rationals =====
qOfNzqNonZero : (x : NZQ) → ¬ (qOfNzq x ≡ qZero)
  using (Core.prop.¬.unfold,
    Core.prop.⊃.unfold,
    Rat.frac.NZ.unfold,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzToInt.eq,
    Rat.NZQ.unfold,
    Rat.nzqToRat.eq,
    Rat.qOfNzq.eq,
    Rat.qcls.eq)
qOfNzqNonZero =
  λx. notIntro _ (λh. notApply _ (nzToIntNonZero (x .π₁)) (numZeroOfRatZero (nzqToRat x) h))

-- so "non-zero" and "of the form qOfNzq x" coincide — the classical
-- description of ℚ's units, with the structural one
qNonZeroIffNzq : (u : Q) → ¬ (u ≡ qZero) ↔ ∥(x : NZQ) × qOfNzq x ≡ u∥
  using (Core.prop.↔.unfold, Core.prop.∧.unfold)
qNonZeroIffNzq =
  λu. iffIntro
    λh. qNonZeroIsNzq h
    λh. squash-elim
      h
      w. notIntro (u ≡ qZero) (λe. notApply _ (qOfNzqNonZero (w .π₁)) (trans _ _ _ (w .π₂) e))

-- ===== the field axiom, classically =====
-- 1 ≠ 0: nzToInt nzOne IS intOne, and the image of an NZ misses zero
qOneNotZero : ¬ (qOne ≡ qZero)
  using (Int.intOne.eq,
    Core.prop.¬.unfold,
    Core.prop.⊃.unfold,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzOne.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratOne.eq,
    Rat.qOne.eq,
    Rat.qcls.eq)
qOneNotZero =
  notIntro _ (λh. notApply (intOne ≡ intZero) (nzToIntNonZero nzOne) (numZeroOfRatZero ratOne h))

-- INVERTIBLE ⟺ NON-ZERO. Forwards is the inverse theorem; backwards,
-- a zero u would make 1 = u·v = 0·v = 0
qInvertibleIffNonZero : (u : Q) → ¬ (u ≡ qZero) ↔ ∥(v : Q) × u * v ≡ qOne∥
  using (Int.Int.unfold,
    Core.prop.↔.unfold,
    Core.prop.∧.unfold,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.Q.unfold)
qInvertibleIffNonZero =
  λu. iffIntro
    λh. qInvExists h
    λh. squash-elim
      h
      w. notIntro
        u ≡ qZero
        λe. notApply
          _
          qOneNotZero
          trans
            qOne
            _
            _
            sym (class (class (S Z, Z), inj₁ Z)) (class (class (S Z, Z), inj₁ Z)) (w .π₂)
            trans _ _ qZero (cong (λt. Q) (λx. x * w .π₁) e) qMulZeroL