From 489365885d28ca0c881d477fc09a6b6e676eb9eb Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Fri, 17 Apr 2026 16:31:18 +0800 Subject: [PATCH 01/10] Upgrade to leanprover/lean4:v4.30.0-rc1 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Update lean-toolchain to v4.30.0-rc1 - Run lake update to refresh all dependencies - Fix removed/moved Mathlib modules: - Mathlib.Data.Sign → Mathlib.Data.Sign.Basic - Mathlib.Data.Real.GoldenRatio → Mathlib.NumberTheory.Real.GoldenRatio - Mathlib.Data.Real.Pi.Bounds → Mathlib.Analysis.Real.Pi.Bounds - Mathlib.Data.Complex.Exponential → Mathlib.Analysis.Complex.Exponential - Fix removed typeclasses in aux_lemmas.lean: - LinearOrderedAddCommGroup → AddCommGroup + LinearOrder + IsOrderedAddMonoid - LinearOrderedField → Field + LinearOrder + IsStrictOrderedRing Co-Authored-By: Claude Sonnet 4.6 --- ComputableReal/ComputableRSeq.lean | 2 +- ComputableReal/SpecialFunctions/Exp.lean | 2 +- ComputableReal/SpecialFunctions/Pi.lean | 2 +- ComputableReal/SpecialFunctions/Sqrt.lean | 2 +- ComputableReal/aux_lemmas.lean | 4 +-- lake-manifest.json | 33 ++++++++++++----------- lean-toolchain | 2 +- 7 files changed, 24 insertions(+), 23 deletions(-) diff --git a/ComputableReal/ComputableRSeq.lean b/ComputableReal/ComputableRSeq.lean index ab7a818..1baa075 100644 --- a/ComputableReal/ComputableRSeq.lean +++ b/ComputableReal/ComputableRSeq.lean @@ -1,6 +1,6 @@ import Mathlib.Algebra.Order.Interval.Basic import Mathlib.Data.Real.Archimedean -import Mathlib.Data.Sign +import Mathlib.Data.Sign.Basic import Mathlib.Tactic.Rify import ComputableReal.aux_lemmas diff --git a/ComputableReal/SpecialFunctions/Exp.lean b/ComputableReal/SpecialFunctions/Exp.lean index 4a53a45..185603e 100644 --- a/ComputableReal/SpecialFunctions/Exp.lean +++ b/ComputableReal/SpecialFunctions/Exp.lean @@ -1,5 +1,5 @@ import ComputableReal.IsComputable -import Mathlib.Data.Complex.Exponential +import Mathlib.Analysis.Complex.Exponential import Mathlib.Analysis.SpecialFunctions.Exp import Mathlib.Analysis.SpecialFunctions.Pow.Real diff --git a/ComputableReal/SpecialFunctions/Pi.lean b/ComputableReal/SpecialFunctions/Pi.lean index 86d5996..160ef72 100644 --- a/ComputableReal/SpecialFunctions/Pi.lean +++ b/ComputableReal/SpecialFunctions/Pi.lean @@ -1,5 +1,5 @@ import ComputableReal.SpecialFunctions.Sqrt -import Mathlib.Data.Real.Pi.Bounds +import Mathlib.Analysis.Real.Pi.Bounds import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic open scoped QInterval diff --git a/ComputableReal/SpecialFunctions/Sqrt.lean b/ComputableReal/SpecialFunctions/Sqrt.lean index 18cbf6e..0444a14 100644 --- a/ComputableReal/SpecialFunctions/Sqrt.lean +++ b/ComputableReal/SpecialFunctions/Sqrt.lean @@ -1,7 +1,7 @@ import ComputableReal.IsComputable import Mathlib.Data.Real.Sqrt import Mathlib.Analysis.SpecialFunctions.Log.Base -import Mathlib.Data.Real.GoldenRatio +import Mathlib.NumberTheory.Real.GoldenRatio namespace ComputableℝSeq diff --git a/ComputableReal/aux_lemmas.lean b/ComputableReal/aux_lemmas.lean index 9ee77b0..9e473f0 100644 --- a/ComputableReal/aux_lemmas.lean +++ b/ComputableReal/aux_lemmas.lean @@ -2,7 +2,7 @@ import Mathlib.Data.Real.Archimedean --============ --silly lemmas -theorem abs_ite_le [inst : LinearOrderedAddCommGroup α] (x : α) : +theorem abs_ite_le [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (x : α) : abs x = if 0 ≤ x then x else -x := by split_ifs <;> simp_all next h => @@ -10,7 +10,7 @@ theorem abs_ite_le [inst : LinearOrderedAddCommGroup α] (x : α) : namespace CauSeq -variable [LinearOrderedField α] {a b : CauSeq α abs} +variable [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : CauSeq α abs} theorem sup_equiv_of_equivs (ha : a ≈ c) (hb : b ≈ c) : a ⊔ b ≈ c := by intro n hn diff --git a/lake-manifest.json b/lake-manifest.json index 92699ce..1e73031 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,11 +1,11 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "2e4bea3590e14768d39b454d51bc438cf1731503", + "rev": "0e62b4b350acebbead46f0427c6df5ba6d09e3ea", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "59a8514bb0ee5bae2689d8be717b5272c9b3dc1c", + "rev": "264309b5c0c10e569025a53ab6440a45c03133e4", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5013810061a18ca1f5510106172b94c6fbd0a2fc", + "rev": "4411c5f89c797401c609b3a946c8874569e69731", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,51 +45,52 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8fff3f074da9237cd4e179fd6dd89be6c4022d41", + "rev": "82d457fb3bdd9efadbae06608ff337d689efdddf", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.52-pre", + "inputRev": "v0.0.97", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ba9a63be53f16b3b6e4043641c6bad4883e650b4", + "rev": "f74c7555aaa94eadd7b7bff9170f7983f92aac21", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7b3b0c8327b3c0214ac49ca6d6922edbb81ab8c9", + "rev": "7aa86cb20b8458748dc24d55dab2d7ea01161057", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "24cbb071689802fd6d3ff42198b19b125004c4e3", + "rev": "bf597c77bf9b8e66720d724928207f5911533113", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.30.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "a2eb24a3dbf681f2b655f82ba5ee5b139d4a5abc", + "rev": "f7d0ca7c926cdde0562af20394dd25d028b839a5", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.30.0-rc1", "inherited": true, "configFile": "lakefile.toml"}], "name": "computableReal", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lean-toolchain b/lean-toolchain index 3ca992c..2210cba 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.17.0-rc1 +leanprover/lean4:v4.30.0-rc1 From 9269242c78baf42127b7df5cd4de7420fc815892 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Wed, 22 Apr 2026 16:12:33 +0800 Subject: [PATCH 02/10] pin to 4.29 --- lake-manifest.json | 33 ++++++++++++++++----------------- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 18 insertions(+), 19 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 1e73031..ae1ecdc 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,21 +1,21 @@ -{"version": "1.2.0", +{"version": "1.1.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "0e62b4b350acebbead46f0427c6df5ba6d09e3ea", + "rev": "5e932f97dd25535344f80f9dd8da3aab83df0fe6", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "v4.29.1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "264309b5c0c10e569025a53ab6440a45c03133e4", + "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4411c5f89c797401c609b3a946c8874569e69731", + "rev": "48d5698bc464786347c1b0d859b18f938420f060", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,52 +45,51 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "82d457fb3bdd9efadbae06608ff337d689efdddf", + "rev": "4dd0959c44d1af0462bd604d0f87c5781307d709", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.97", + "inputRev": "v0.0.95+lean-v4.29.1", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f74c7555aaa94eadd7b7bff9170f7983f92aac21", + "rev": "7152850e7b216a0d409701617721b6e469d34bf6", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc1", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7aa86cb20b8458748dc24d55dab2d7ea01161057", + "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc1", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "bf597c77bf9b8e66720d724928207f5911533113", + "rev": "756e3321fd3b02a85ffda19fef789916223e578c", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc1", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "f7d0ca7c926cdde0562af20394dd25d028b839a5", + "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc1", + "inputRev": "v4.29.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "computableReal", - "lakeDir": ".lake", - "fixedToolchain": false} + "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index 0ff1d58..d1fbbcd 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ package «computableReal» { } require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" + "https://github.com/leanprover-community/mathlib4.git"@"v4.29.1" @[default_target] lean_lib «ComputableReal» { diff --git a/lean-toolchain b/lean-toolchain index 2210cba..05a063a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.30.0-rc1 +leanprover/lean4:v4.29.1 \ No newline at end of file From 5f58497ac44ca153d72694941ac871e57dfec552 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Wed, 22 Apr 2026 16:13:16 +0800 Subject: [PATCH 03/10] ignore .claude --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index cc75e48..d89e0dc 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ /build /lake-packages/* .lake/* +.claude From 4e5e97cf3769c03e916c2a9b74dcecbf6f8e1f7c Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Wed, 22 Apr 2026 16:17:14 +0800 Subject: [PATCH 04/10] some work by claude --- ComputableReal/ComputableRSeq.lean | 30 ++++++------- ComputableReal/ComputableReal.lean | 69 +++++++++++++++++++----------- 2 files changed, 59 insertions(+), 40 deletions(-) diff --git a/ComputableReal/ComputableRSeq.lean b/ComputableReal/ComputableRSeq.lean index 1baa075..db93636 100644 --- a/ComputableReal/ComputableRSeq.lean +++ b/ComputableReal/ComputableRSeq.lean @@ -44,9 +44,9 @@ theorem mul_pair_lb_is_lb {x y : ℚInterval} : ∀ xv ∈ x, ∀ yv ∈ y, intro xv ⟨hxl,hxu⟩ yv ⟨hyl,hyu⟩ dsimp [mul_pair] push_cast - rcases le_or_lt xv 0 with hxn|hxp - all_goals rcases le_or_lt (y.fst:ℝ) 0 with hyln|hylp - all_goals rcases le_or_lt (y.snd:ℝ) 0 with hyun|hyup + rcases le_or_gt xv 0 with hxn|hxp + all_goals rcases le_or_gt (y.fst:ℝ) 0 with hyln|hylp + all_goals rcases le_or_gt (y.snd:ℝ) 0 with hyun|hyup all_goals try linarith all_goals repeat rw [min_def] all_goals split_ifs with h₁ h₂ h₃ h₃ h₂ h₃ h₃ @@ -57,9 +57,9 @@ theorem mul_pair_ub_is_ub {x y : ℚInterval} : ∀ xv ∈ x, ∀ yv ∈ y, intro xv ⟨hxl,hxu⟩ yv ⟨hyl,hyu⟩ dsimp [mul_pair] push_cast - rcases le_or_lt xv 0 with hxn|hxp - all_goals rcases le_or_lt (y.1.1:ℝ) 0 with hyln|hylp - all_goals rcases le_or_lt (y.1.2:ℝ) 0 with hyun|hyup + rcases le_or_gt xv 0 with hxn|hxp + all_goals rcases le_or_gt (y.1.1:ℝ) 0 with hyln|hylp + all_goals rcases le_or_gt (y.1.2:ℝ) 0 with hyun|hyup all_goals try linarith all_goals repeat rw [max_def] all_goals split_ifs with h₁ h₂ h₃ h₃ h₂ h₃ h₃ @@ -802,7 +802,7 @@ theorem lb_inv_converges {x : ComputableℝSeq} (hnz : x.val ≠ 0) : rw [Real.cauchy_inv, Real.cauchy, Real.cauchy, Real.mk, val_eq_mk_ub, Real.mk, CauSeq.Completion.inv_mk (neg_LimZero_ub_of_val hnz), CauSeq.Completion.mk_eq, lb_inv] split_ifs with h - · rfl + · rw [sub_self]; exact CauSeq.zero_limZero · exact fun _ hε ↦ have hxv : x.val < 0 := by rw [is_pos_iff] at h @@ -832,7 +832,7 @@ theorem ub_inv_converges {x : ComputableℝSeq} (hnz : x.val ≠ 0) : ⟨i, fun j hj ↦ have : ¬x.lb j ≤ 0 := by linarith [H _ hj] by simp [this, hε]⟩ - · rfl + · rw [sub_self]; exact CauSeq.zero_limZero /-- When applied to a `dropTilSigned`, `ub_inv` is converges to x⁻¹. TODO: version without hnz hypothesis. -/ @@ -844,7 +844,7 @@ theorem ub_inv_signed_converges {x : ComputableℝSeq} (hnz : x.val ≠ 0) : nonzero, then we can prove that at some point we learn the sign, and so can start giving actual upper and lower bounds. There is a separate `inv` that uses `sign` to construct the proof of nonzeroness by searching along the sequence (but isn't guaranteed to terminate). -/ -def safe_inv (x : ComputableℝSeq) (hnz : x.val ≠ 0) : ComputableℝSeq := +noncomputable def safe_inv (x : ComputableℝSeq) (hnz : x.val ≠ 0) : ComputableℝSeq := --TODO currently this passes the sequence to lb_inv and ub_inv separately, which means we evaluate --things twice (and this can lead to exponential slowdown for long series of inverses). This should --be bundled @@ -870,14 +870,14 @@ theorem val_safe_inv_ne_zero {x : ComputableℝSeq} (hnz : x.val ≠ 0) : (x.saf /-- Subtype of sequences with nonzero values. These admit a (terminating) inverse function. -/ def nzSeq := {x : ComputableℝSeq // x.val ≠ 0} -def inv_nz : nzSeq → nzSeq := +noncomputable def inv_nz : nzSeq → nzSeq := fun x ↦ ⟨x.val.safe_inv x.prop, val_safe_inv_ne_zero _⟩ @[simp] theorem val_inv_nz (x : nzSeq) : (inv_nz x).val.val = x.val.val⁻¹ := val_safe_inv _ -instance instNzInv : Inv nzSeq := +noncomputable instance instNzInv : Inv nzSeq := ⟨inv_nz⟩ end safe_inv @@ -887,16 +887,16 @@ section inv /-- Inverse of a computable real. Will terminate if the argument is nonzero, or if it is zero and the upper and lower bounds become exactly zero at some point. See `ComputableℝSeq.sign`. If you want to only call this in a way guaranteed to terminate, use `ComputableℝSeq.safe_inv`. -/ -def inv : ComputableℝSeq → ComputableℝSeq := +noncomputable def inv : ComputableℝSeq → ComputableℝSeq := fun x ↦ match h : x.sign with | SignType.pos => x.safe_inv (x.sign_pos_iff.1 h).ne' | SignType.neg => x.safe_inv (x.sign_neg_iff.1 h).ne | SignType.zero => 0 -instance instInv : Inv ComputableℝSeq := +noncomputable instance instInv : Inv ComputableℝSeq := ⟨inv⟩ -instance instDiv : Div ComputableℝSeq := +noncomputable instance instDiv : Div ComputableℝSeq := ⟨fun x y ↦ x * y⁻¹⟩ theorem inv_def (x : ComputableℝSeq) : x⁻¹ = x.inv := @@ -1028,7 +1028,7 @@ class CompSeqClass (G : Type u) extends AddCommMonoid G, CommMagma G, MulZeroOneClass G, Inv G, Div G, HasDistribNeg G, SubtractionCommMonoid G, NatCast G, IntCast G, RatCast G -instance instSeqCompSeqClass : CompSeqClass ComputableℝSeq := by +noncomputable instance instSeqCompSeqClass : CompSeqClass ComputableℝSeq := by refine' { natCast := fun n => n intCast := fun z => z diff --git a/ComputableReal/ComputableReal.lean b/ComputableReal/ComputableReal.lean index 286f6ab..64d0a67 100644 --- a/ComputableReal/ComputableReal.lean +++ b/ComputableReal/ComputableReal.lean @@ -152,6 +152,12 @@ instance instCommRing : CommRing Computableℝ := by npow := npowRec --todo faster instances nsmul := nsmulRec zsmul := zsmulRec + natCast_succ := fun n => by + rw [← eq_iff_eq_val] + simp only [val_mk_eq_val, val_add, val_one, ComputableℝSeq.val_natCast] + push_cast; ring + sub_eq_add_neg := fun a b => by + rw [← eq_iff_eq_val, val_sub, val_add, val_neg]; ring .. } all_goals intros @@ -159,7 +165,7 @@ instance instCommRing : CommRing Computableℝ := by | rfl | rw [← eq_iff_eq_val] simp - try ring_nf! + try ring @[simp] theorem val_natpow (x : Computableℝ) (n : ℕ): (x ^ n).val = x.val ^ n := by @@ -191,14 +197,14 @@ private def nz_quot_equiv := Equiv.subtypeQuotientEquivQuotientSubtype (fun _ _ ↦ Iff.rfl) /-- Auxiliary inverse definition that operates on the nonzero Computableℝ values. -/ -def safe_inv' : { x : Computableℝ // x ≠ 0 } → { x : Computableℝ // x ≠ 0 } := +noncomputable def safe_inv' : { x : Computableℝ // x ≠ 0 } → { x : Computableℝ // x ≠ 0 } := fun v ↦ nz_quot_equiv.invFun <| Quotient.map _ fun x y h₁ ↦ by change (ComputableℝSeq.inv_nz x).val.val = (ComputableℝSeq.inv_nz y).val.val rw [ComputableℝSeq.val_inv_nz x, ComputableℝSeq.val_inv_nz y, h₁] (nz_quot_equiv.toFun v) /-- Inverse of a nonzero Computableℝ, safe (terminating) as long as x is nonzero. -/ -irreducible_def safe_inv (hnz : x ≠ 0) : Computableℝ := safe_inv' ⟨x, hnz⟩ +noncomputable irreducible_def safe_inv (hnz : x ≠ 0) : Computableℝ := safe_inv' ⟨x, hnz⟩ @[simp] theorem safe_inv_val (hnz : x ≠ 0) : (x.safe_inv hnz).val = x.val⁻¹ := by @@ -219,7 +225,7 @@ end safe_inv section field -instance instComputableInv : Inv Computableℝ := +noncomputable instance instComputableInv : Inv Computableℝ := ⟨mapℝ' (·⁻¹) ⟨(·⁻¹), ComputableℝSeq.val_inv⟩⟩ @[simp] @@ -230,7 +236,7 @@ theorem inv_val : (x⁻¹).val = (x.val)⁻¹ := by example : True := ⟨⟩ -instance instField : Field Computableℝ := { instCommRing with +noncomputable instance instField : Field Computableℝ := { instCommRing with qsmul := _ nnqsmul := _ exists_pair_ne := ⟨0, 1, by @@ -302,26 +308,39 @@ instance instDecidableLE : DecidableRel (fun (x y : Computableℝ) ↦ x ≤ y) infer_instance --TODO: add a faster `min` and `max` that don't require sign computation. -instance instLinearOrderedField : LinearOrderedField Computableℝ := by - refine' { instField, instLT, instLE with - decidableLE := inferInstance - le_refl := _ - le_trans := _ - le_antisymm := _ - add_le_add_left := _ - zero_le_one := _ - mul_pos := _ - le_total := _ - lt_iff_le_not_le := _ - } - all_goals - intros - simp only [← le_iff_le, ← lt_iff_lt, ← eq_iff_eq_val, val_add, val_mul, val_zero, val_one] at * - first - | linarith (config := {splitNe := true}) - | apply mul_pos ‹_› ‹_› - | apply le_total - | apply lt_iff_le_not_le +noncomputable instance instLinearOrder : LinearOrder Computableℝ where + le_refl x := by rw [← le_iff_le] + le_trans a b c h₁ h₂ := by rw [← le_iff_le] at *; exact le_trans h₁ h₂ + lt_iff_le_not_ge a b := by + simp only [← lt_iff_lt, ← le_iff_le] + exact ⟨fun h => ⟨le_of_lt h, not_le_of_lt h⟩, fun ⟨h₁, h₂⟩ => lt_of_le_not_le h₁ h₂⟩ + le_antisymm a b h₁ h₂ := by + rw [← le_iff_le] at h₁ h₂; rw [← eq_iff_eq_val]; exact le_antisymm h₁ h₂ + le_total a b := by simp only [← le_iff_le]; exact le_total _ _ + toDecidableLE := instDecidableLE + +instance instIsOrderedAddMonoid : IsOrderedAddMonoid Computableℝ where + add_le_add_left a b h c := by + simp only [← le_iff_le, val_add] at *; linarith + +instance instIsOrderedCancelAddMonoid : IsOrderedCancelAddMonoid Computableℝ where + le_of_add_le_add_left a b c h := by + simp only [← le_iff_le, val_add] at *; linarith + +noncomputable instance instPosMulStrictMono : PosMulStrictMono Computableℝ where + mul_lt_mul_of_pos_left := by + intro a ha b c hbc + simp only [← lt_iff_lt, val_mul] at * + exact mul_lt_mul_of_pos_left hbc ha + +noncomputable instance instMulPosStrictMono : MulPosStrictMono Computableℝ where + mul_lt_mul_of_pos_right := by + intro c hc a b hab + simp only [← lt_iff_lt, val_mul] at * + exact mul_lt_mul_of_pos_right hab hc + +instance instIsStrictOrderedRing : IsStrictOrderedRing Computableℝ where + zero_le_one := by rw [← le_iff_le, val_zero, val_one]; exact zero_le_one end ordered From 8b1011123c83dfc1f7a3a0a09bf1d9130f71e452 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Wed, 22 Apr 2026 17:37:47 +0800 Subject: [PATCH 05/10] fixed warnings --- ComputableReal/ComputableRSeq.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/ComputableReal/ComputableRSeq.lean b/ComputableReal/ComputableRSeq.lean index db93636..7bf077f 100644 --- a/ComputableReal/ComputableRSeq.lean +++ b/ComputableReal/ComputableRSeq.lean @@ -983,13 +983,13 @@ theorem right_distrib (x y z : ComputableℝSeq) : (x + y) * z = x * z + y * z : theorem neg_mul (x y : ComputableℝSeq) : -x * y = -(x * y) := by ext · rw [lb_neg, lb_mul, ub_mul] - simp only [lb_neg, ub_neg, CauSeq.coe_inf, CauSeq.coe_mul, CauSeq.coe_neg, neg_mul, + simp only [lb_neg, ub_neg, CauSeq.coe_inf, CauSeq.coe_mul, CauSeq.coe_neg, Pi.inf_apply, Pi.neg_apply, Pi.mul_apply, CauSeq.neg_apply, CauSeq.coe_sup, Pi.sup_apply, neg_sup] nth_rewrite 2 [inf_comm] nth_rewrite 3 [inf_comm] ring_nf · rw [ub_neg, lb_mul, ub_mul] - simp only [lb_neg, ub_neg, CauSeq.coe_inf, CauSeq.coe_mul, CauSeq.coe_neg, neg_mul, + simp only [lb_neg, ub_neg, CauSeq.coe_inf, CauSeq.coe_mul, CauSeq.coe_neg, Pi.inf_apply, Pi.neg_apply, Pi.mul_apply, CauSeq.neg_apply, CauSeq.coe_sup, Pi.sup_apply, neg_inf] nth_rewrite 2 [sup_comm] nth_rewrite 3 [sup_comm] @@ -1062,8 +1062,8 @@ noncomputable instance instSeqCompSeqClass : CompSeqClass ComputableℝSeq := by | rfl | ext all_goals - try simp only [natCast_ub, natCast_lb, Nat.cast_add, Nat.cast_one, CauSeq.add_apply, CauSeq.one_apply, - CauSeq.zero_apply, CauSeq.neg_apply, lb_add, ub_add, one_ub, one_lb, zero_ub, zero_lb, ub_neg, + try simp only [CauSeq.add_apply, + CauSeq.zero_apply, CauSeq.neg_apply, lb_add, ub_add, zero_ub, zero_lb, ub_neg, lb_neg, neg_add_rev, neg_neg, zero_add, add_zero] try ring_nf try rfl From 5274c7f5b4049afd4bd180f172f79c77e9305560 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Wed, 22 Apr 2026 17:44:27 +0800 Subject: [PATCH 06/10] fixed instLinearOrder --- ComputableReal/ComputableReal.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ComputableReal/ComputableReal.lean b/ComputableReal/ComputableReal.lean index 64d0a67..01caf31 100644 --- a/ComputableReal/ComputableReal.lean +++ b/ComputableReal/ComputableReal.lean @@ -313,7 +313,7 @@ noncomputable instance instLinearOrder : LinearOrder Computableℝ where le_trans a b c h₁ h₂ := by rw [← le_iff_le] at *; exact le_trans h₁ h₂ lt_iff_le_not_ge a b := by simp only [← lt_iff_lt, ← le_iff_le] - exact ⟨fun h => ⟨le_of_lt h, not_le_of_lt h⟩, fun ⟨h₁, h₂⟩ => lt_of_le_not_le h₁ h₂⟩ + exact lt_iff_le_not_ge le_antisymm a b h₁ h₂ := by rw [← le_iff_le] at h₁ h₂; rw [← eq_iff_eq_val]; exact le_antisymm h₁ h₂ le_total a b := by simp only [← le_iff_le]; exact le_total _ _ From ada116373da532197c79dacaaefb0b9aed1b4b45 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Wed, 22 Apr 2026 19:36:36 +0800 Subject: [PATCH 07/10] cleared ComputableReal.lean --- ComputableReal/ComputableReal.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ComputableReal/ComputableReal.lean b/ComputableReal/ComputableReal.lean index 01caf31..2a8f334 100644 --- a/ComputableReal/ComputableReal.lean +++ b/ComputableReal/ComputableReal.lean @@ -330,13 +330,13 @@ instance instIsOrderedCancelAddMonoid : IsOrderedCancelAddMonoid Computableℝ w noncomputable instance instPosMulStrictMono : PosMulStrictMono Computableℝ where mul_lt_mul_of_pos_left := by intro a ha b c hbc - simp only [← lt_iff_lt, val_mul] at * + simp only [← lt_iff_lt, val_mul, val_zero] at * exact mul_lt_mul_of_pos_left hbc ha noncomputable instance instMulPosStrictMono : MulPosStrictMono Computableℝ where mul_lt_mul_of_pos_right := by intro c hc a b hab - simp only [← lt_iff_lt, val_mul] at * + simp only [← lt_iff_lt, val_mul, val_zero] at * exact mul_lt_mul_of_pos_right hab hc instance instIsStrictOrderedRing : IsStrictOrderedRing Computableℝ where From ebae6225b5530e2c42e07ad6de568612aab0dcee Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Wed, 22 Apr 2026 19:45:18 +0800 Subject: [PATCH 08/10] minor warning fix --- ComputableReal/ComputableRSeq.lean | 4 ++-- ComputableReal/IsComputable.lean | 7 +++++-- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/ComputableReal/ComputableRSeq.lean b/ComputableReal/ComputableRSeq.lean index 7bf077f..4d16069 100644 --- a/ComputableReal/ComputableRSeq.lean +++ b/ComputableReal/ComputableRSeq.lean @@ -575,7 +575,7 @@ noncomputable def sign_witness_term (x : ComputableℝSeq) (hnz : x.val ≠ 0) : theorem sign_witness_term_prop (x : ComputableℝSeq) (n : ℕ) (hnz : x.val ≠ 0) (hub : ¬(x.ub).val n < 0) (hlb: ¬(x.lb).val n > 0) : n + Nat.succ 0 ≤ (x.sign_witness_term hnz).val.1 := by - push_neg at hub hlb + push Not at hub hlb obtain ⟨⟨k, q⟩, ⟨h₁, h₂, h₃⟩⟩ := x.sign_witness_term hnz by_contra hn replace h₃ := h₃ n (by linarith) @@ -941,7 +941,7 @@ theorem add_comm (x y: ComputableℝSeq) : x + y = y + x := by theorem mul_comm (x y : ComputableℝSeq) : x * y = y * x := by ext n - <;> simp only [lb_mul, ub_mul, mul_lb, mul_ub] + <;> simp only [lb_mul, ub_mul] · repeat rw [_root_.mul_comm (lb x)] repeat rw [_root_.mul_comm (ub x)] dsimp diff --git a/ComputableReal/IsComputable.lean b/ComputableReal/IsComputable.lean index 48ee05f..f3e480e 100644 --- a/ComputableReal/IsComputable.lean +++ b/ComputableReal/IsComputable.lean @@ -13,15 +13,18 @@ namespace IsComputable /-- Turns one `IsComputable` into another one, given a proof that they're equal. This is directly analogous to `decidable_of_iff`, as a way to avoid `Eq.rec` on data-carrying instances. -/ +@[reducible] def lift_eq {x y : ℝ} (h : x = y) : IsComputable x → IsComputable y := fun ⟨sx, hsx⟩ ↦ ⟨sx, h ▸ hsx⟩ +@[reducible] def lift (fr : ℝ → ℝ) (fs : ComputableℝSeq → ComputableℝSeq) (h : ∀ a, (fs a).val = fr a.val) : IsComputable x → IsComputable (fr x) := fun ⟨sx, hsx⟩ ↦ ⟨fs sx, hsx ▸ h sx⟩ +@[reducible] def lift₂ (fr : ℝ → ℝ → ℝ) (fs : ComputableℝSeq → ComputableℝSeq → ComputableℝSeq) (h : ∀a b, (fs a b).val = fr a.val b.val) : IsComputable x → IsComputable y → IsComputable (fr x y) := @@ -84,7 +87,7 @@ instance instComputableNatPow [hx : IsComputable x] (n : ℕ) : IsComputable (x instance instComputableZPow [hx : IsComputable x] (z : ℤ) : IsComputable (x ^ z) := by cases z - · rw [Int.ofNat_eq_coe, zpow_natCast] + · rw [Int.ofNat_eq_natCast, zpow_natCast] infer_instance · simp only [zpow_negSucc] infer_instance @@ -194,7 +197,7 @@ theorem Real_mk_of_TendstoLocallyUniformly' (fImpl : ℕ → ℚ → ℚ) (f : calc |↑(fImpl j (x j)) - f (Real.mk ⟨x, hx⟩)| = |(↑(fImpl j (x j)) - f ↑(x j)) + (f ↑(x j) - f (Real.mk ⟨x, hx⟩))| := by congr; ring_nf - _ ≤ |(↑(fImpl j (x j)) - f ↑(x j))| + |(f ↑(x j) - f (Real.mk ⟨x, hx⟩))| := abs_add _ _ + _ ≤ |(↑(fImpl j (x j)) - f ↑(x j))| + |(f ↑(x j) - f (Real.mk ⟨x, hx⟩))| := abs_add_le _ _ _ < ε := by rw [abs_sub_comm]; linarith open scoped QInterval From 92c58b581a38f7781741ef15660d9949d02a0fe1 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Wed, 22 Apr 2026 20:18:43 +0800 Subject: [PATCH 09/10] add noncomputable --- ComputableReal/ComputableReal.lean | 2 +- ComputableReal/IsComputable.lean | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/ComputableReal/ComputableReal.lean b/ComputableReal/ComputableReal.lean index 2a8f334..2fa08ee 100644 --- a/ComputableReal/ComputableReal.lean +++ b/ComputableReal/ComputableReal.lean @@ -308,7 +308,7 @@ instance instDecidableLE : DecidableRel (fun (x y : Computableℝ) ↦ x ≤ y) infer_instance --TODO: add a faster `min` and `max` that don't require sign computation. -noncomputable instance instLinearOrder : LinearOrder Computableℝ where +instance instLinearOrder : LinearOrder Computableℝ where le_refl x := by rw [← le_iff_le] le_trans a b c h₁ h₂ := by rw [← le_iff_le] at *; exact le_trans h₁ h₂ lt_iff_le_not_ge a b := by diff --git a/ComputableReal/IsComputable.lean b/ComputableReal/IsComputable.lean index f3e480e..3ea8fd5 100644 --- a/ComputableReal/IsComputable.lean +++ b/ComputableReal/IsComputable.lean @@ -58,7 +58,7 @@ instance instComputableOfNatAtLeastTwo : (n : ℕ) → [n.AtLeastTwo] → IsComp instance instComputableNeg (x : ℝ) [hx : IsComputable x] : IsComputable (-x) := lift _ (- ·) ComputableℝSeq.val_neg hx -instance instComputableInv (x : ℝ) [hx : IsComputable x] : IsComputable (x⁻¹) := +noncomputable instance instComputableInv (x : ℝ) [hx : IsComputable x] : IsComputable (x⁻¹) := lift _ (·⁻¹) ComputableℝSeq.val_inv hx instance instComputableAdd [hx : IsComputable x] [hy : IsComputable y] : IsComputable (x + y) := @@ -70,7 +70,7 @@ instance instComputableSub [hx : IsComputable x] [hy : IsComputable y] : IsCompu instance instComputableMul [hx : IsComputable x] [hy : IsComputable y] : IsComputable (x * y) := lift₂ _ (· * ·) ComputableℝSeq.val_mul hx hy -instance instComputableDiv [hx : IsComputable x] [hy : IsComputable y] : IsComputable (x / y) := +noncomputable instance instComputableDiv [hx : IsComputable x] [hy : IsComputable y] : IsComputable (x / y) := lift₂ _ (· / ·) ComputableℝSeq.val_div hx hy instance instComputableNatPow [hx : IsComputable x] (n : ℕ) : IsComputable (x ^ n) := by @@ -85,14 +85,14 @@ instance instComputableNatPow [hx : IsComputable x] (n : ℕ) : IsComputable (x · rw [pow_succ] infer_instance -instance instComputableZPow [hx : IsComputable x] (z : ℤ) : IsComputable (x ^ z) := by +noncomputable instance instComputableZPow [hx : IsComputable x] (z : ℤ) : IsComputable (x ^ z) := by cases z · rw [Int.ofNat_eq_natCast, zpow_natCast] infer_instance · simp only [zpow_negSucc] infer_instance -instance instComputableNSMul [hx : IsComputable x] (n : ℕ) : IsComputable (n • x) := +noncomputable instance instComputableNSMul [hx : IsComputable x] (n : ℕ) : IsComputable (n • x) := lift _ (n • ·) (by --TODO move to a ComputableℝSeq lemma intro a From 7079cea062da2e77a344872a66be3cf00f6568b1 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Wed, 22 Apr 2026 23:19:29 +0800 Subject: [PATCH 10/10] point out the Real.instInv place --- ComputableReal/ComputableRSeq.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/ComputableReal/ComputableRSeq.lean b/ComputableReal/ComputableRSeq.lean index 4d16069..220b78a 100644 --- a/ComputableReal/ComputableRSeq.lean +++ b/ComputableReal/ComputableRSeq.lean @@ -850,6 +850,7 @@ noncomputable def safe_inv (x : ComputableℝSeq) (hnz : x.val ≠ 0) : Computab --be bundled let signed := x.dropTilSigned hnz let hnz' := val_dropTilSigned hnz ▸ hnz + -- x.val⁻¹ use `Real.instInv` here, which is noncomputable. mk (x := x.val⁻¹) (lub := fun n ↦ ⟨⟨(signed.lb_inv hnz') n, (signed.ub_inv hnz') n⟩, Rat.cast_le.mp ((lb_inv_correct hnz n).trans (ub_inv_correct hnz n))⟩)