-- The rational intervals: open intervals with rational endpoints form a
-- countable basis of the real line, by the density of ℚ in ℝ
-- (Real/Embedding)
-- 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.Topology.Real.RationalBase
import Basis
import Rat.Countable

-- The open intervals with rational endpoints.
def rationalIntervals : Set :=
  { W ∈ 𝒫(ℝ) | ∃ p ∈ ℚ, ∃ q ∈ ℚ, p < q ∧
    W = openInterval(rationalCut(p), rationalCut(q)) }

theorem openInterval.member_intervals (p q : Rational)
  requires less : p < q
  shows openInterval(rationalCut(p), rationalCut(q)) ∈ rationalIntervals
proof
  have realP := rationalCut.real at p with assumption
  have realQ := rationalCut.real at q with assumption
  have pInQ : p ∈ ℚ by typecheck
  have qInQ : q ∈ ℚ by typecheck
  apply rationalIntervals.membership.backward
  refine ⟨?_, p, pInQ, q, qInQ, less, rfl⟩
  apply powerset.membership_iff.backward
  exact openInterval.subset_reals at rationalCut(p), rationalCut(q)

theorem rationalIntervals.open
  shows rationalIntervals ⊆ realTopology
proof
  intros W hW
  have parts := rationalIntervals.membership.forward with hW
  obtain ⟨p, hp, q, hq, less, shape⟩ := parts.right
  have realP := rationalCut.real at p with hp
  have realQ := rationalCut.real at q with hq
  rw shape
  exact openInterval.open at rationalCut(p), rationalCut(q)

-- Every open set around a real contains a rational interval around it.
theorem rationalIntervals.basis
  shows Basis(ℝ, realTopology, rationalIntervals)
proof
  constructor
  . exact rationalIntervals.open
  . intros U hU x hx
    have parts := realTopology.membership.forward with hU
    have inside := powerset.membership_iff.forward with parts.left
    have realX := inside with x, hx
    obtain ⟨E, hE, positive, below⟩ := parts.right with x, hx
    have lowerReal : x - E ∈ ℝ by typecheck
    have upperReal : x + E ∈ ℝ by typecheck
    have lowerLess : x - E < x by linarith
    have upperLess : x < x + E by linarith
    obtain ⟨p, hp, lowerP, upperP⟩ := rationalCut.between with lowerLess
    obtain ⟨q, hq, lowerQ, upperQ⟩ := rationalCut.between with upperLess
    have realP := rationalCut.real at p with hp
    have realQ := rationalCut.real at q with hq
    have cutsOrdered := realLess.transitive with upperP, lowerQ
    have proper := realLess.characterization.forward with cutsOrdered
    have ordered := rationalCut.lt_of_cut_lt with proper
    have found := openInterval.member_intervals with ordered
    have center : x ∈ openInterval(rationalCut(p), rationalCut(q)) :=
      openInterval.membership.backward with ⟨realX, upperP, lowerQ⟩
    refine ⟨openInterval(rationalCut(p), rationalCut(q)), found, center, ?_⟩
    . intros y hy
      obtain ⟨realY, lowerY, upperY⟩ :=
        openInterval.membership.forward with hy
      have bounds : x - E < y ∧ y < x + E
        constructor
        . linarith
        . linarith
      have inBall := openBall.order_characterization.backward with bounds
      exact below with y, inBall

-- The pairs of rationals in increasing order index the rational intervals.
def rationalPairs : Set :=
  { r ∈ ℚ × ℚ | relates(rationalLess, fst(r), snd(r)) }

theorem rationalPairs.countable
  shows Countable(rationalPairs)
proof
  have rationals := rationals.countable
  have pairs := Countable.product at ℚ, ℚ with rationals, rationals
  have subset : rationalPairs ⊆ ℚ × ℚ
    intros r hr
    have parts := rationalPairs.membership.forward with hr
    exact parts.left
  exact Countable.subset with pairs, subset

defgraph rationalInterval (r ∈ rationalPairs) : rationalIntervals :=
  openInterval(rationalCut(fst(r)), rationalCut(snd(r)))
proof
  have parts := rationalPairs.membership.forward with member
  obtain ⟨bound, p, hp, q, hq, shape⟩ :=
    product.membership.forward with parts.left
  have less := parts.right
  rw [shape, fst.pair, snd.pair] at less
  rw [shape, fst.pair, snd.pair]
  exact openInterval.member_intervals with less

theorem rationalInterval.surjective
  shows SurjectiveBetween(rationalInterval, rationalPairs, rationalIntervals)
proof
  constructor
  . exact rationalInterval.function
  . intros W hW
    have parts := rationalIntervals.membership.forward with hW
    obtain ⟨p, hp, q, hq, less, shape⟩ := parts.right
    have pairIn : (p, q) ∈ ℚ × ℚ := product.pair with hp, hq
    have inPairs : (p, q) ∈ rationalPairs
      apply rationalPairs.membership.backward
      refine ⟨pairIn, ?_⟩
      rw [fst.pair, snd.pair]
      exact less
    have value := rationalInterval.relates with inPairs
    rw [fst.pair, snd.pair, ← shape] at value
    exact ⟨(p, q), inPairs, value⟩

theorem rationalIntervals.countable
  shows Countable(rationalIntervals)
proof
  have countable := rationalPairs.countable
  have surjection := rationalInterval.surjective
  exact Countable.of_surjection with countable, surjection