From 33ef86aeef39eb6b687d3321102c49bbc17b5e6e Mon Sep 17 00:00:00 2001 From: Eduardo Aguilar Pelaez Date: Thu, 10 Sep 2026 15:15:48 +0000 Subject: [PATCH] Fix build against Mathlib at Lean v4.29.1 Two independent breakages, both small. 1. Interval/Fixed.lean: Fixed.ofInt0_natCast On current Mathlib, simp normalises both sides of the goal to the same term but no longer closes it, leaving an X = X goal. Appending rfl closes it. 2. Interval/Interval/Preinterval.lean and Mul.lean: a real-valued argument defeats erasure Preinterval.mix' took a real-valued implicit argument whose only purpose was to state the proposition in the next argument: def mix' (x : Preinterval) {a : R} (m : approx x a) : Interval A real is data, not a proof, so it is not erased. mix' is @[inline], and at its sole definitional call site, Interval.mul, that argument instantiates to a term containing Floating.val, which is noncomputable by design. Interval.mul therefore failed to compile with 'depends on Floating.val, which is noncomputable'. Moving the real inside the proposition means nothing real crosses the boundary: def mix' (x : Preinterval) (m : exists a : R, approx x a) : Interval mix' has exactly one non-lemma use, so this touches one definition, two lemma signatures and one call site. Tested: with these changes Interval.Interval.Mul, Interval.Interval.Exp and Interval.Interval.Log all build against Mathlib v4.29.1 (rev 5e932f97). Not addressed here: Interval.Interval.Pow still fails via Interval/Interval/Division.lean, which has the same underlying problem in a harder place. There the real is a type index (Around x.val inverse), computed through Real.instInv, so this fix does not transfer. Repairing it needs a decision about whether Around should carry its centre as an index, which is a design question rather than a repair. See the accompanying issue. The lean-toolchain pin is deliberately left untouched. --- Interval/Fixed.lean | 4 +++- Interval/Interval/Mul.lean | 2 +- Interval/Interval/Preinterval.lean | 7 ++++--- 3 files changed, 8 insertions(+), 5 deletions(-) diff --git a/Interval/Fixed.lean b/Interval/Fixed.lean index 1777572..46b01e4 100644 --- a/Interval/Fixed.lean +++ b/Interval/Fixed.lean @@ -902,7 +902,9 @@ lemma Real.cast_natCast (n : ℤ) (n0 : 0 ≤ n) : (n : ℝ) = (n.toNat : ℝ) : simp only [Nat.log2_lt n0', ← Nat.cast_lt (α := ℤ), Nat.cast_pow, Nat.cast_two, Nat.cast_natAbs] at nn rw [Int64.toInt_ofInt' nn] -@[simp] lemma Fixed.ofInt0_natCast (n : ℕ) : ofInt0 (n : ℤ) = ofNat0 n := by simp [ofInt0, ofNat0] +@[simp] lemma Fixed.ofInt0_natCast (n : ℕ) : ofInt0 (n : ℤ) = ofNat0 n := by + simp [ofInt0, ofNat0] + rfl /-- `Fixed.ofNat0` is conservative -/ @[approx] lemma Fixed.approx_ofNat0 (n : ℕ) : approx (ofNat0 n) (n : ℝ) := by diff --git a/Interval/Interval/Mul.lean b/Interval/Interval/Mul.lean index 8e945e8..a4b6884 100644 --- a/Interval/Interval/Mul.lean +++ b/Interval/Interval/Mul.lean @@ -141,7 +141,7 @@ variable {x y : Interval} {x' y' : ℝ} /-- Multiply two intervals -/ @[irreducible] def mul (x : Interval) (y : Interval) : Interval := - (x.premul y).mix' (approx_premul x.lo_mem y.lo_mem) + (x.premul y).mix' ⟨_, approx_premul x.lo_mem y.lo_mem⟩ /-- `* = mul` -/ instance : Mul Interval where diff --git a/Interval/Interval/Preinterval.lean b/Interval/Interval/Preinterval.lean index e03b80f..99865e6 100644 --- a/Interval/Interval/Preinterval.lean +++ b/Interval/Interval/Preinterval.lean @@ -55,8 +55,9 @@ instance : ApproxNan Preinterval ℝ where Interval.mix x.lo x.hi le /-- If a `Preinterval` is nonempty`, it can be turned into an `Interval` -/ -@[irreducible, inline] def mix' (x : Preinterval) {a : ℝ} (m : approx x a) : Interval := +@[irreducible, inline] def mix' (x : Preinterval) (m : ∃ a : ℝ, approx x a) : Interval := x.mix (by + obtain ⟨a, m⟩ := m intro ln hn simp only [approx, ln, hn, mem_Icc, false_or] at m linarith) @@ -73,7 +74,7 @@ instance : ApproxNan Preinterval ℝ where simp only [approx, ln, hn, or_self, dite_false, false_or, mem_Icc] /-- `mix'` commutes with `approx` -/ -@[simp] lemma approx_mix' (x : Preinterval) {a b : ℝ} (m : approx x a) : +@[simp] lemma approx_mix' (x : Preinterval) {b : ℝ} (m : ∃ a : ℝ, approx x a) : approx (x.mix' m) b = approx x b := by rw [mix', approx_mix] @@ -84,5 +85,5 @@ instance : ApproxNan Preinterval ℝ where rw [mix]; simp only [lo_nan, hi_nan, Interval.mix_self, Interval.coe_nan] /-- `mix'` propagates `nan` -/ -@[simp] lemma mix_nan' {a : ℝ} (m : approx (nan : Preinterval) a) : mix' nan m = nan := by +@[simp] lemma mix_nan' (m : ∃ a : ℝ, approx (nan : Preinterval) a) : mix' nan m = nan := by rw [mix', mix_nan]