-- The embedding of the rationals in the reals preserves addition
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Real.RationalEmbedding
import Natural
import Rat.Density

-- The cut of a sum is the sum of the cuts. A rational below p + q splits as
-- a + b with a below p and b below q, by density; the converse is monotonicity.
theorem rationalCut.add (p q : Rational)
  shows rationalCut(p + q) = rationalCut(p) + rationalCut(q)
proof
  have sumReal := rationalCut.real at p + q with *
  have cutForm := realAddValue.cut at rationalCut(p), rationalCut(q) with *
  have addReal := realAddValue.real at rationalCut(p), rationalCut(q) with *
  rw cutForm
  rw cutForm at addReal
  apply Real.extensionality
  . exact sumReal
  . exact addReal
  . intros r rInQ
    constructor
    . intro member
      obtain ⟨rMember, less⟩ := rationalCut.membership.forward with member
      have commuted := rationalAddValue.commutative at p, q with *
      rw commuted at less
      have shifted := rationalLess.sub_left at r, q, p with *
      obtain ⟨a, aInQ, aAbove, aBelow⟩ := rationalLess.dense at r - q, p with *
      have aMember : a ∈ rationalCut(p) := rationalCut.membership.backward with ⟨aInQ, aBelow⟩
      have moved := rationalLess.add_left_of_sub_left at r, q, a with *
      have commutedA := rationalAddValue.commutative at q, a with *
      rw commutedA at moved
      have shiftedA := rationalLess.sub_left at r, a, q with *
      obtain ⟨b, bInQ, bAbove, bBelow⟩ := rationalLess.dense at r - a, q with *
      have bMember : b ∈ rationalCut(q) := rationalCut.membership.backward with ⟨bInQ, bBelow⟩
      have below := rationalLess.add_left_of_sub_left at r, a, b with *
      rw rationalAddValue.notation at below
      exact realAddCut.membership_value.backward with ⟨rInQ, a, aMember, b, bMember, below⟩
    . intro member
      obtain ⟨rMember, a, aMember, b, bMember, below⟩ := realAddCut.membership_value.forward with member
      obtain ⟨aInQ, aBelow⟩ := rationalCut.membership.forward with aMember
      obtain ⟨bInQ, bBelow⟩ := rationalCut.membership.forward with bMember
      rw ← rationalAddValue.notation at below
      have first := rationalLess.add_right at a, p, b with *
      have second := rationalLess.add_left at b, q, p with *
      have chain := rationalLess.transitive at r, a + b, p + b with *
      have whole := rationalLess.transitive at r, p + b, p + q with *
      apply rationalCut.membership.backward
      constructor
      . exact rInQ
      . exact whole

theorem rationalCut.zero
  shows rationalCut(rationalZero) = realZero
proof
  simp

theorem rationalCut.one
  shows rationalCut(rationalOne) = realOne
proof
  simp

theorem rationalCut.neg (q : Rational)
  shows rationalCut(-q) = -(rationalCut(q))
proof
  have cancel := rationalAddValue.neg_right at q with *
  have sum := rationalCut.add at q, -q with *
  rw [cancel, rationalCut.zero] at sum
  linarith

theorem rationalCut.sub (p q : Rational)
  shows rationalCut(p - q) = rationalCut(p) - rationalCut(q)
proof
  have negation := rationalCut.neg at q with *
  unfold rationalSubValue
  have sum := rationalCut.add at p, -q with *
  rw [sum, negation]
  unfold realSubValue
  rfl

-- The rational n, built like realNat so the two embeddings line up.
def rationalNat (n : Nat) → Set
  | zero => rationalZero
  | succ(k) => rationalAddValue(rationalNat(k), rationalOne)

theorem rationalNat.zero
  shows rationalNat(0) = rationalZero
proof
  simp

theorem rationalNat.succ (n : Nat)
  shows rationalNat(succ(n)) = (rationalNat(n):Q) + rationalOne
proof
  rw [rationalNat, rationalAddValue.notation]
  rfl

theorem rationalNat.rational (n : Nat)
  shows Rational(rationalNat(n))
proof
  induction n
  | zero =>
    rw rationalNat.zero
    exact rationalZero.rational
  | succ(k) using ih =>
    rw rationalNat.succ
    exact rationalAddValue.rational at rationalNat(k), rationalOne with *

theorem realNat.successor (n : Nat)
  shows realNat(succ(n)) = (realNat(n):R) + 1
proof
  rw realNat.succ
  unfold realAddValue
  unfold call2
  rfl

theorem rationalCut.natural (n : Nat)
  shows rationalCut(rationalNat(n)) = realNat(n)
proof
  induction n
  | zero =>
    rw [rationalNat.zero, realNat.zero]
    exact rationalCut.zero
  | succ(k) using ih =>
    rw rationalNat.succ
    have sum := rationalCut.add at rationalNat(k), rationalOne with *
    rw [sum, ih, rationalCut.one, realNat.successor]
    rfl

theorem rationalNat.class (n : Nat)
  shows rationalNat(n) = rationalClass(n, 0, 1)
proof
  induction n
  | zero =>
    rw rationalNat.zero
    unfold rationalZero
    rfl
  | succ(k) using ih =>
    rw [rationalNat.succ, ih]
    unfold rationalOne
    have oneNonzero : 1 ≠ 0
      intro bad
      have positive : 0 < 1 by arith
      rw bad at positive
      exact Less.irreflexive at 0 with *, positive
    rw rationalAddValue.notation
    have classes := rationalAddValue.classes at k, 0, 1, 1, 0, 1 with *
    rw classes
    unfold rationalClassSum
    have productNonzero : 1 * 1 ≠ 0
      have unit := mul.right_unit at 1 with *
      rwa unit
    have equivalent : 1 * (1 * k + 1 * 1) + (1 * 1) * 0 = (1 * 1) * succ(k) + 1 * (1 * 0 + 1 * 0) by ring
    exact rationalClass.eq at 1 * k + 1 * 1, 1 * 0 + 1 * 0, 1 * 1, succ(k), 0, 1 with *

-- Multiplying a rational by the natural m scales its cut by realNat(m).
theorem rationalCut.mul_natural (q : Rational) (m : Nat)
  shows rationalCut(q * (rationalNat(m):Q)) = rationalCut(q) * realNat(m)
proof
  induction m
  | zero =>
    rw rationalNat.zero
    have zero := rationalMulValue.zero_right at q with *
    rw [zero, rationalCut.zero, realNat.zero]
    ring
  | succ(k) using ih =>
    rw rationalNat.succ
    have distribute := rationalMulValue.distributive_left at q, rationalNat(k), rationalOne with *
    rw distribute
    have unit := rationalMulValue.one_right at q with *
    rw unit
    have sum := rationalCut.add at q * (rationalNat(k):Q), q with *
    rw [sum, ih, realNat.successor]
    ring

-- A rational a/m, written as the class of ((a, b), m), scales to the difference
-- of two naturals: (a − b)/m times m is a − b.
theorem rationalClass.mul_denominator (a b m : Nat)
  requires nonzero : m ≠ 0
  shows (rationalClass(a, b, m):Q) * (rationalNat(m):Q) = (rationalNat(a):Q) - (rationalNat(b):Q)
proof
  have oneNonzero : 1 ≠ 0
    intro bad
    have positive : 0 < 1 by arith
    rw bad at positive
    exact Less.irreflexive with *, positive
  have classA := rationalNat.class at a with *
  have classB := rationalNat.class at b with *
  have classM := rationalNat.class at m with *
  rw [classA, classB, classM]
  rw rationalMulValue.notation
  have product := rationalMulValue.classes at a, b, m, m, 0, 1 with *
  rw product
  unfold rationalClassMul
  unfold rationalSubValue
  rw rationalNegValue.notation
  have negation := rationalNegValue.classes at b, 0, 1 with *
  rw negation
  unfold rationalClassNeg
  rw rationalAddValue.notation
  have sum := rationalAddValue.classes at a, 0, 1, 0, b, 1 with *
  rw sum
  unfold rationalClassSum
  have mulNonzero : m * 1 ≠ 0
    have unit := mul.right_unit at m with *
    rwa unit
  have productNonzero : 1 * 1 ≠ 0
    have unit := mul.right_unit at 1 with *
    rwa unit
  have equivalent : (1 * 1) * (a * m + b * 0) + (m * 1) * (1 * 0 + 1 * b) = (m * 1) * (1 * a + 1 * 0) + (1 * 1) * (a * 0 + b * m)
    ring
  exact rationalClass.eq with *

theorem rationalCut.scaled (a b m : Nat)
  requires nonzero : m ≠ 0
  shows (rationalCut(rationalClass(a, b, m)):R) * (realNat(m):R) = (realNat(a):R) - (realNat(b):R)
proof
  have qRational := rationalClass.rational at a, b, m with *
  have scaled := rationalCut.mul_natural at rationalClass(a, b, m), m with *
  rw ← scaled
  have integer := rationalClass.mul_denominator at a, b, m with *
  rw integer
  have difference := rationalCut.sub at rationalNat(a), rationalNat(b) with *
  rw [difference, rationalCut.natural, rationalCut.natural]
  rfl