Grace/Cumulus/Real/Core.g17

Open in Workbench Download source

Imports

Defs · Cumulus.Order

Declarations

Source

1-- Core laws of Dedekind cuts2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Real.Core8import Defs9import Cumulus.Order1011theorem ProperSubset.subset (A B : Set)12  requires h : A ⊂ B13  shows (A ⊆ B)14proof15  simp [ProperSubset]1617theorem ProperSubset.ne (A B : Set)18  requires h : A ⊂ B19  shows A ≠ B20proof21  simp [ProperSubset]2223theorem ProperSubset.missing (A B : Set)24  requires proper : A ⊂ B25  shows ∃ x ∈ B, ¬(x ∈ A)26proof27  rcases proper with ⟨subset, unequal⟩28  by_contra noMissing29  apply unequal30  ext x31  constructor32  . intro xInA33    exact subset with x, xInA34  . intro xInB35    by_contra xNotInA36    apply noMissing37    refine ⟨x, xInB, xNotInA⟩3839theorem ProperSubset.irreflexive (A : Set)40  shows ¬(A ⊂ A)41proof42  intro proper43  rcases proper with ⟨subset, unequal⟩44  apply unequal45  rfl4647theorem ProperSubset.transitive (A B C : Set)48  requires hAB : A ⊂ B49  requires hBC : B ⊂ C50  shows (A ⊂ C)51proof52  rcases hAB with ⟨subsetAB, neAB⟩53  rcases hBC with ⟨subsetBC, neBC⟩54  constructor55  . exact Subset.transitive with subsetAB, subsetBC56  . intro equalAC57    rw ← equalAC at subsetBC58    have equalAB := Subset.antisymmetric with subsetAB, subsetBC59    exact neAB with equalAB6061theorem DedekindCut.subset_rationals (A : Set)62  requires cut : DedekindCut(A)63  shows (A ⊆ ℚ)64proof65  simp [DedekindCut]6667theorem DedekindCut.nonempty (A : Set)68  requires cut : DedekindCut(A)69  shows Nonempty(A)70proof71  simp [DedekindCut]7273theorem DedekindCut.proper (A : Set)74  requires cut : DedekindCut(A)75  shows (A ⊂ ℚ)76proof77  rcases cut with ⟨subset, inhabited, proper, rest⟩78  refine ⟨subset, proper⟩7980theorem DedekindCut.downward (A p q : Set)81  requires cut : DedekindCut(A)82  requires hq : q ∈ A83  requires hp : p ∈ ℚ84  requires less : relates(rationalLess, p, q)85  shows p ∈ A86proof87  rcases cut with ⟨subset, inhabited, proper, downward, rounded⟩88  exact downward with q, hq, p, hp, less8990theorem DedekindCut.no_greatest (A q : Set)91  requires cut : DedekindCut(A)92  requires hq : q ∈ A93  shows ∃ r ∈ A, relates(rationalLess, q, r)94proof95  rcases cut with ⟨subset, inhabited, proper, downward, rounded⟩96  exact rounded with q, hq9798-- Every member of a lower cut lies strictly below each rational omitted by99-- that cut. Connectedness rules out the reverse comparison by downward closure.100theorem DedekindCut.lt_missing (A a u : Set)101  requires cut : DedekindCut(A)102  requires aInA : a ∈ A103  requires uInQ : u ∈ ℚ104  requires uMissing : ¬(u ∈ A)105  shows relates(rationalLess, a, u)106proof107  have subset := DedekindCut.subset_rationals with cut108  have aInQ := subset with a, aInA109  have distinct : a ≠ u110    intro equal111    apply uMissing112    rwa ← equal113  have connected := rationalLess.connected_on114  have comparison := connected with a, aInQ, u, uInQ, distinct115  cases comparison with aLessU | uLessA116  . exact aLessU117  . have uInA := DedekindCut.downward with cut, aInA, uInQ, uLessA118    exfalso119    exact uMissing with uInA120121theorem reals.membership (A : Set)122  shows A ∈ ℝ ↔ DedekindCut(A)123proof124  simp [ℝ, DedekindCut, Subset, set.powerset]125126theorem Real.characterization (A : Set)127  shows Real(A) ↔ DedekindCut(A)128proof129  simp [Real, reals.membership]130131theorem Real.extensionality (A B : Set)132  requires realA : Real(A)133  requires realB : Real(B)134  requires same : ∀ q ∈ ℚ, (q ∈ A ↔ q ∈ B)135  shows A = B136proof137  ext q138  have cutA := Real.characterization.forward with realA139  have cutB := Real.characterization.forward with realB140  have subsetA := DedekindCut.subset_rationals with cutA141  have subsetB := DedekindCut.subset_rationals with cutB142  constructor143  . intro hqA144    specialize subsetA with q, hqA145    specialize same with q, subsetA146    apply same.forward147    exact hqA148  . intro hqB149    specialize subsetB with q, hqB150    specialize same with q, subsetB151    apply same.backward152    exact hqB153154theorem RealLess.irreflexive (A : Set)155  shows ¬RealLess(A, A)156proof157  intro h158  rcases h with ⟨realA, realAgain, proper⟩159  exact ProperSubset.irreflexive with proper160161theorem RealLess.transitive (A B C : Set)162  requires hAB : RealLess(A, B)163  requires hBC : RealLess(B, C)164  shows RealLess(A, C)165proof166  rcases hAB with ⟨realA, realB, properAB⟩167  rcases hBC with ⟨realBAgain, realC, properBC⟩168  constructor169  exact realA170  constructor171  exact realC172  exact ProperSubset.transitive with properAB, properBC173174theorem realLess.membership (p : Set)175  shows p ∈ realLess ↔ (p ∈ ℝ × ℝ ∧ ∃ x ∈ ℝ, ∃ y ∈ ℝ, p = (x, y) ∧ (x ⊂ y))176proof177  simp178179theorem realLess.characterization (A B : Set)180  shows relates(realLess, A, B) ↔ RealLess(A, B)181proof182  constructor183  . intro less184    unfold relates at less185    simp [realLess.membership] at less186    rcases less with ⟨_, x, realX, y, realY, pairShape, proper⟩187    obtain ⟨equalA, equalB⟩ := orderedPair.injective with pairShape188    constructor189    . unfold Real190      rwa equalA191    . constructor192      . unfold Real193        rwa equalB194      . rw [equalA, equalB]195        exact proper196  . intro less197    rcases less with ⟨realA, realB, proper⟩198    unfold relates199    apply realLess.membership.backward200    constructor201    . apply product.pair at A, B, ℝ, ℝ202        exact realA203        exact realB204    . witness A205      constructor206        exact realA207      . witness B208        constructor209          exact realB210        refine ⟨rfl, proper⟩211212theorem realLess.relation213  shows RelationBetween(realLess, ℝ, ℝ)214proof215  intros p hp216  simp [realLess.membership] at hp217  rcases hp with ⟨bounded, witnesses⟩218  exact bounded219220instance realLess.operation221  shows LessOperation(ℝ, realLess)222proof223  exact realLess.relation224225notation infix 50 "<" => relates via LessOperation(ℝ, _) for Real226227theorem realLess.irreflexive_on228  shows IrreflexiveOn(ℝ, realLess)229proof230  intros A realA less231  have proposition := realLess.characterization.forward with less232  exact RealLess.irreflexive with proposition233234theorem realLess.transitive_on235  shows TransitiveOn(ℝ, realLess)236proof237  intros A realA B realB C realC lessAB lessBC238  have propositionAB := realLess.characterization.forward with lessAB239  have propositionBC := realLess.characterization.forward with lessBC240  have propositionAC := RealLess.transitive with propositionAB, propositionBC241  exact realLess.characterization.backward with propositionAC242243-- Mainstream typed interface used by calculations and ordered algebra.244theorem realLess.transitive (A B C : Real)245  requires AB : A < B246  requires BC : B < C247  shows A < C248proof249  have transitive := realLess.transitive_on250  exact transitive with A, B, C, AB, BC251252theorem realLess.strict_order253  shows StrictOrder(ℝ, realLess)254proof255  refine ⟨realLess.relation, realLess.irreflexive_on, realLess.transitive_on⟩256257-- Lower cuts are nested.  If some b belongs to B but not A, every member of258-- A lies below b and hence belongs to B by downward closure; otherwise B is259-- already a subset of A.260theorem DedekindCut.comparable (A B : Set)261  requires cutA : DedekindCut(A)262  requires cutB : DedekindCut(B)263  shows (A ⊆ B) ∨ (B ⊆ A)264proof265  by_contra incomparable266  have notAB : ¬(A ⊆ B)267    intro subsetAB268    apply incomparable269    left270    exact subsetAB271  have notBA : ¬(B ⊆ A)272    intro subsetBA273    apply incomparable274    right275    exact subsetBA276  apply notBA277  intros b bInB278  by_contra bMissingA279  apply notAB280  intros a aInA281  have subsetA := DedekindCut.subset_rationals with cutA282  have subsetB := DedekindCut.subset_rationals with cutB283  have aInQ := subsetA with a, aInA284  have bInQ := subsetB with b, bInB285  have aLessB := DedekindCut.lt_missing with cutA, aInA, bInQ, bMissingA286  exact DedekindCut.downward with cutB, bInB, aInQ, aLessB287288theorem realLess.connected_on289  shows ConnectedOn(ℝ, realLess)290proof291  intros A realA B realB distinct292  have typedA : Real(A) by exact realA293  have typedB : Real(B) by exact realB294  have cutA := Real.characterization.forward with typedA295  have cutB := Real.characterization.forward with typedB296  have comparable := DedekindCut.comparable with cutA, cutB297  rcases comparable with subsetAB | subsetBA298  . left299    have properAB : (A ⊂ B)300      unfold ProperSubset301      refine ⟨subsetAB, distinct⟩302    apply realLess.characterization.backward303    unfold RealLess304    refine ⟨typedA, typedB, properAB⟩305  . right306    have properBA : (B ⊂ A)307      constructor308      . exact subsetBA309      . intro equalBA310        apply distinct311        rw equalBA312        rfl313    apply realLess.characterization.backward314    unfold RealLess315    refine ⟨typedB, typedA, properBA⟩316317theorem realLess.strict_linear_order318  shows StrictLinearOrder(ℝ, realLess)319proof320  refine ⟨realLess.strict_order, realLess.connected_on⟩321322theorem rationalCut.subset_rationals (q : Set)323  shows (rationalCut(q) ⊆ ℚ)324proof325  simp326327-- Rational lower segments are Dedekind cuts.  Unboundedness supplies328-- an inhabitant, density supplies roundedness, and transitivity supplies329-- downward closure.330theorem rationalCut.cut (q : Set)331  requires qRational : Rational(q)332  shows DedekindCut(rationalCut(q))333proof334  have qInQ := qRational335  unfold Rational at qInQ336  unfold DedekindCut337  refine ⟨rationalCut.subset_rationals at q, _, _, _, _⟩338  . unfold Nonempty339    obtain ⟨p, pInQ, pLessQ⟩ := rationalLess.exists_below with qRational340    witness p341    apply rationalCut.membership.backward342    constructor343    . exact pInQ344    . exact pLessQ345  . intro allRationals346    have qInCut : q ∈ rationalCut(q) by rwa allRationals347    obtain ⟨_, selfLess⟩ := rationalCut.membership.forward with qInCut348    have irreflexive := rationalLess.irreflexive_on349    exact irreflexive with q, qInQ, selfLess350  . intros r rInCut p pInQ pLessR351    obtain ⟨rInQ, rLessQ⟩ := rationalCut.membership.forward with rInCut352    have transitive := rationalLess.transitive_on353    have pLessQ := transitive with354      p, pInQ, r, rInQ, q, qInQ, pLessR, rLessQ355    apply rationalCut.membership.backward356    constructor357    . exact pInQ358    . exact pLessQ359  . intros p pInCut360    obtain ⟨pInQ, pLessQ⟩ := rationalCut.membership.forward with pInCut361    have pRational : Rational(p) by exact pInQ362    obtain ⟨s, sInQ, pLessS, sLessQ⟩ := rationalLess.dense with pRational, qRational, pLessQ363    witness s364    constructor365    . apply rationalCut.membership.backward at q, s366      constructor367      . exact sInQ368      . exact sLessQ369    . exact pLessS370371theorem rationalCut.real (q : Set)372  requires qRational : Rational(q)373  shows Real(rationalCut(q))374proof375  apply Real.characterization.backward376  exact rationalCut.cut with qRational377378theorem rationalCut.strict_mono (q r : Set)379  requires qRational : Rational(q)380  requires rRational : Rational(r)381  requires less : relates(rationalLess, q, r)382  shows RealLess(rationalCut(q), rationalCut(r))383proof384  have qInQ := qRational385  have rInQ := rRational386  unfold RealLess387  refine ⟨rationalCut.real at q with qRational,388    rationalCut.real at r with rRational, _⟩389  constructor390    intros p pInQCut391    obtain ⟨pInQ, pLessQ⟩ := rationalCut.membership.forward with pInQCut392    have transitive := rationalLess.transitive_on393    have pLessR := transitive with394      p, pInQ, q, qInQ, r, rInQ, pLessQ, less395    apply rationalCut.membership.backward396    constructor397    . exact pInQ398    . exact pLessR399  . intro cutsEqual400    have qInRCut : q ∈ rationalCut(r) := rationalCut.membership.backward with ⟨qInQ, less⟩401    rw ← cutsEqual at qInRCut402    obtain ⟨_, selfLess⟩ := rationalCut.membership.forward with qInRCut403    have irreflexive := rationalLess.irreflexive_on404    exact irreflexive with q, qInQ, selfLess405