-- Core laws of Dedekind cuts
-- 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.Core
import Defs
import Cumulus.Order

theorem ProperSubset.subset (A B : Set)
  requires h : A ⊂ B
  shows (A ⊆ B)
proof
  simp [ProperSubset]

theorem ProperSubset.ne (A B : Set)
  requires h : A ⊂ B
  shows A ≠ B
proof
  simp [ProperSubset]

theorem ProperSubset.missing (A B : Set)
  requires proper : A ⊂ B
  shows ∃ x ∈ B, ¬(x ∈ A)
proof
  rcases proper with ⟨subset, unequal⟩
  by_contra noMissing
  apply unequal
  ext x
  constructor
  . intro xInA
    exact subset with x, xInA
  . intro xInB
    by_contra xNotInA
    apply noMissing
    refine ⟨x, xInB, xNotInA⟩

theorem ProperSubset.irreflexive (A : Set)
  shows ¬(A ⊂ A)
proof
  intro proper
  rcases proper with ⟨subset, unequal⟩
  apply unequal
  rfl

theorem ProperSubset.transitive (A B C : Set)
  requires hAB : A ⊂ B
  requires hBC : B ⊂ C
  shows (A ⊂ C)
proof
  rcases hAB with ⟨subsetAB, neAB⟩
  rcases hBC with ⟨subsetBC, neBC⟩
  constructor
  . exact Subset.transitive with subsetAB, subsetBC
  . intro equalAC
    rw ← equalAC at subsetBC
    have equalAB := Subset.antisymmetric with subsetAB, subsetBC
    exact neAB with equalAB

theorem DedekindCut.subset_rationals (A : Set)
  requires cut : DedekindCut(A)
  shows (A ⊆ ℚ)
proof
  simp [DedekindCut]

theorem DedekindCut.nonempty (A : Set)
  requires cut : DedekindCut(A)
  shows Nonempty(A)
proof
  simp [DedekindCut]

theorem DedekindCut.proper (A : Set)
  requires cut : DedekindCut(A)
  shows (A ⊂ ℚ)
proof
  rcases cut with ⟨subset, inhabited, proper, rest⟩
  refine ⟨subset, proper⟩

theorem DedekindCut.downward (A p q : Set)
  requires cut : DedekindCut(A)
  requires hq : q ∈ A
  requires hp : p ∈ ℚ
  requires less : relates(rationalLess, p, q)
  shows p ∈ A
proof
  rcases cut with ⟨subset, inhabited, proper, downward, rounded⟩
  exact downward with q, hq, p, hp, less

theorem DedekindCut.no_greatest (A q : Set)
  requires cut : DedekindCut(A)
  requires hq : q ∈ A
  shows ∃ r ∈ A, relates(rationalLess, q, r)
proof
  rcases cut with ⟨subset, inhabited, proper, downward, rounded⟩
  exact rounded with q, hq

-- Every member of a lower cut lies strictly below each rational omitted by
-- that cut. Connectedness rules out the reverse comparison by downward closure.
theorem DedekindCut.lt_missing (A a u : Set)
  requires cut : DedekindCut(A)
  requires aInA : a ∈ A
  requires uInQ : u ∈ ℚ
  requires uMissing : ¬(u ∈ A)
  shows relates(rationalLess, a, u)
proof
  have subset := DedekindCut.subset_rationals with cut
  have aInQ := subset with a, aInA
  have distinct : a ≠ u
    intro equal
    apply uMissing
    rwa ← equal
  have connected := rationalLess.connected_on
  have comparison := connected with a, aInQ, u, uInQ, distinct
  cases comparison with aLessU | uLessA
  . exact aLessU
  . have uInA := DedekindCut.downward with cut, aInA, uInQ, uLessA
    exfalso
    exact uMissing with uInA

theorem reals.membership (A : Set)
  shows A ∈ ℝ ↔ DedekindCut(A)
proof
  simp [ℝ, DedekindCut, Subset, set.powerset]

theorem Real.characterization (A : Set)
  shows Real(A) ↔ DedekindCut(A)
proof
  simp [Real, reals.membership]

theorem Real.extensionality (A B : Set)
  requires realA : Real(A)
  requires realB : Real(B)
  requires same : ∀ q ∈ ℚ, (q ∈ A ↔ q ∈ B)
  shows A = B
proof
  ext q
  have cutA := Real.characterization.forward with realA
  have cutB := Real.characterization.forward with realB
  have subsetA := DedekindCut.subset_rationals with cutA
  have subsetB := DedekindCut.subset_rationals with cutB
  constructor
  . intro hqA
    specialize subsetA with q, hqA
    specialize same with q, subsetA
    apply same.forward
    exact hqA
  . intro hqB
    specialize subsetB with q, hqB
    specialize same with q, subsetB
    apply same.backward
    exact hqB

theorem RealLess.irreflexive (A : Set)
  shows ¬RealLess(A, A)
proof
  intro h
  rcases h with ⟨realA, realAgain, proper⟩
  exact ProperSubset.irreflexive with proper

theorem RealLess.transitive (A B C : Set)
  requires hAB : RealLess(A, B)
  requires hBC : RealLess(B, C)
  shows RealLess(A, C)
proof
  rcases hAB with ⟨realA, realB, properAB⟩
  rcases hBC with ⟨realBAgain, realC, properBC⟩
  constructor
  exact realA
  constructor
  exact realC
  exact ProperSubset.transitive with properAB, properBC

theorem realLess.membership (p : Set)
  shows p ∈ realLess ↔ (p ∈ ℝ × ℝ ∧ ∃ x ∈ ℝ, ∃ y ∈ ℝ, p = (x, y) ∧ (x ⊂ y))
proof
  simp

theorem realLess.characterization (A B : Set)
  shows relates(realLess, A, B) ↔ RealLess(A, B)
proof
  constructor
  . intro less
    unfold relates at less
    simp [realLess.membership] at less
    rcases less with ⟨_, x, realX, y, realY, pairShape, proper⟩
    obtain ⟨equalA, equalB⟩ := orderedPair.injective with pairShape
    constructor
    . unfold Real
      rwa equalA
    . constructor
      . unfold Real
        rwa equalB
      . rw [equalA, equalB]
        exact proper
  . intro less
    rcases less with ⟨realA, realB, proper⟩
    unfold relates
    apply realLess.membership.backward
    constructor
    . apply product.pair at A, B, ℝ, ℝ
        exact realA
        exact realB
    . witness A
      constructor
        exact realA
      . witness B
        constructor
          exact realB
        refine ⟨rfl, proper⟩

theorem realLess.relation
  shows RelationBetween(realLess, ℝ, ℝ)
proof
  intros p hp
  simp [realLess.membership] at hp
  rcases hp with ⟨bounded, witnesses⟩
  exact bounded

instance realLess.operation
  shows LessOperation(ℝ, realLess)
proof
  exact realLess.relation

notation infix 50 "<" => relates via LessOperation(ℝ, _) for Real

theorem realLess.irreflexive_on
  shows IrreflexiveOn(ℝ, realLess)
proof
  intros A realA less
  have proposition := realLess.characterization.forward with less
  exact RealLess.irreflexive with proposition

theorem realLess.transitive_on
  shows TransitiveOn(ℝ, realLess)
proof
  intros A realA B realB C realC lessAB lessBC
  have propositionAB := realLess.characterization.forward with lessAB
  have propositionBC := realLess.characterization.forward with lessBC
  have propositionAC := RealLess.transitive with propositionAB, propositionBC
  exact realLess.characterization.backward with propositionAC

-- Mainstream typed interface used by calculations and ordered algebra.
theorem realLess.transitive (A B C : Real)
  requires AB : A < B
  requires BC : B < C
  shows A < C
proof
  have transitive := realLess.transitive_on
  exact transitive with A, B, C, AB, BC

theorem realLess.strict_order
  shows StrictOrder(ℝ, realLess)
proof
  refine ⟨realLess.relation, realLess.irreflexive_on, realLess.transitive_on⟩

-- Lower cuts are nested.  If some b belongs to B but not A, every member of
-- A lies below b and hence belongs to B by downward closure; otherwise B is
-- already a subset of A.
theorem DedekindCut.comparable (A B : Set)
  requires cutA : DedekindCut(A)
  requires cutB : DedekindCut(B)
  shows (A ⊆ B) ∨ (B ⊆ A)
proof
  by_contra incomparable
  have notAB : ¬(A ⊆ B)
    intro subsetAB
    apply incomparable
    left
    exact subsetAB
  have notBA : ¬(B ⊆ A)
    intro subsetBA
    apply incomparable
    right
    exact subsetBA
  apply notBA
  intros b bInB
  by_contra bMissingA
  apply notAB
  intros a aInA
  have subsetA := DedekindCut.subset_rationals with cutA
  have subsetB := DedekindCut.subset_rationals with cutB
  have aInQ := subsetA with a, aInA
  have bInQ := subsetB with b, bInB
  have aLessB := DedekindCut.lt_missing with cutA, aInA, bInQ, bMissingA
  exact DedekindCut.downward with cutB, bInB, aInQ, aLessB

theorem realLess.connected_on
  shows ConnectedOn(ℝ, realLess)
proof
  intros A realA B realB distinct
  have typedA : Real(A) by exact realA
  have typedB : Real(B) by exact realB
  have cutA := Real.characterization.forward with typedA
  have cutB := Real.characterization.forward with typedB
  have comparable := DedekindCut.comparable with cutA, cutB
  rcases comparable with subsetAB | subsetBA
  . left
    have properAB : (A ⊂ B)
      unfold ProperSubset
      refine ⟨subsetAB, distinct⟩
    apply realLess.characterization.backward
    unfold RealLess
    refine ⟨typedA, typedB, properAB⟩
  . right
    have properBA : (B ⊂ A)
      constructor
      . exact subsetBA
      . intro equalBA
        apply distinct
        rw equalBA
        rfl
    apply realLess.characterization.backward
    unfold RealLess
    refine ⟨typedB, typedA, properBA⟩

theorem realLess.strict_linear_order
  shows StrictLinearOrder(ℝ, realLess)
proof
  refine ⟨realLess.strict_order, realLess.connected_on⟩

theorem rationalCut.subset_rationals (q : Set)
  shows (rationalCut(q) ⊆ ℚ)
proof
  simp

-- Rational lower segments are Dedekind cuts.  Unboundedness supplies
-- an inhabitant, density supplies roundedness, and transitivity supplies
-- downward closure.
theorem rationalCut.cut (q : Set)
  requires qRational : Rational(q)
  shows DedekindCut(rationalCut(q))
proof
  have qInQ := qRational
  unfold Rational at qInQ
  unfold DedekindCut
  refine ⟨rationalCut.subset_rationals at q, _, _, _, _⟩
  . unfold Nonempty
    obtain ⟨p, pInQ, pLessQ⟩ := rationalLess.exists_below with qRational
    witness p
    apply rationalCut.membership.backward
    constructor
    . exact pInQ
    . exact pLessQ
  . intro allRationals
    have qInCut : q ∈ rationalCut(q) by rwa allRationals
    obtain ⟨_, selfLess⟩ := rationalCut.membership.forward with qInCut
    have irreflexive := rationalLess.irreflexive_on
    exact irreflexive with q, qInQ, selfLess
  . intros r rInCut p pInQ pLessR
    obtain ⟨rInQ, rLessQ⟩ := rationalCut.membership.forward with rInCut
    have transitive := rationalLess.transitive_on
    have pLessQ := transitive with
      p, pInQ, r, rInQ, q, qInQ, pLessR, rLessQ
    apply rationalCut.membership.backward
    constructor
    . exact pInQ
    . exact pLessQ
  . intros p pInCut
    obtain ⟨pInQ, pLessQ⟩ := rationalCut.membership.forward with pInCut
    have pRational : Rational(p) by exact pInQ
    obtain ⟨s, sInQ, pLessS, sLessQ⟩ := rationalLess.dense with pRational, qRational, pLessQ
    witness s
    constructor
    . apply rationalCut.membership.backward at q, s
      constructor
      . exact sInQ
      . exact sLessQ
    . exact pLessS

theorem rationalCut.real (q : Set)
  requires qRational : Rational(q)
  shows Real(rationalCut(q))
proof
  apply Real.characterization.backward
  exact rationalCut.cut with qRational

theorem rationalCut.strict_mono (q r : Set)
  requires qRational : Rational(q)
  requires rRational : Rational(r)
  requires less : relates(rationalLess, q, r)
  shows RealLess(rationalCut(q), rationalCut(r))
proof
  have qInQ := qRational
  have rInQ := rRational
  unfold RealLess
  refine ⟨rationalCut.real at q with qRational,
    rationalCut.real at r with rRational, _⟩
  constructor
    intros p pInQCut
    obtain ⟨pInQ, pLessQ⟩ := rationalCut.membership.forward with pInQCut
    have transitive := rationalLess.transitive_on
    have pLessR := transitive with
      p, pInQ, q, qInQ, r, rInQ, pLessQ, less
    apply rationalCut.membership.backward
    constructor
    . exact pInQ
    . exact pLessR
  . intro cutsEqual
    have qInRCut : q ∈ rationalCut(r) := rationalCut.membership.backward with ⟨qInQ, less⟩
    rw ← cutsEqual at qInRCut
    obtain ⟨_, selfLess⟩ := rationalCut.membership.forward with qInRCut
    have irreflexive := rationalLess.irreflexive_on
    exact irreflexive with q, qInQ, selfLess