From 45689f00c1e0e0c7a971d504326205a5bcc36f6b Mon Sep 17 00:00:00 2001 From: grunweg Date: Sat, 27 Jul 2024 23:01:29 +0000 Subject: [PATCH 1/2] chore: remove some obsolete porting notes mentioning noncomputable (#15172) - Two porting notes are obsolete: the `noncomputable` modifier could simply be removed. - A few others don't seem actionable. - lean4#2077 is fixed now: no point referencing this issue any more (The `noncomputable` needs to stay, as the definition relies on other noncomputable items.) --- Mathlib/Analysis/CstarAlgebra/Multiplier.lean | 2 +- Mathlib/Analysis/Quaternion.lean | 1 - .../Monoidal/Types/Coyoneda.lean | 7 ------- Mathlib/Computability/PartrecCode.lean | 1 - Mathlib/Computability/TMToPartrec.lean | 1 - Mathlib/Data/Analysis/Topology.lean | 4 +--- Mathlib/MeasureTheory/Measure/Haar/Basic.lean | 18 ------------------ 7 files changed, 2 insertions(+), 32 deletions(-) diff --git a/Mathlib/Analysis/CstarAlgebra/Multiplier.lean b/Mathlib/Analysis/CstarAlgebra/Multiplier.lean index 292cdbe93975f..bc423401f3149 100644 --- a/Mathlib/Analysis/CstarAlgebra/Multiplier.lean +++ b/Mathlib/Analysis/CstarAlgebra/Multiplier.lean @@ -447,7 +447,7 @@ maps `Lโ‚ Rโ‚ : A โ†’L[๐•œ] A` given by left- and right-multiplication by `a` Warning: if `A = ๐•œ`, then this is a coercion which is not definitionally equal to the `algebraMap ๐•œ ๐“œ(๐•œ, ๐•œ)` coercion, but these are propositionally equal. See `DoubleCentralizer.coe_eq_algebraMap` below. -/ --- Porting note: added `noncomputable` because an IR check failed? +-- Porting note: added `noncomputable`; IR check does not recognise `ContinuousLinearMap.mul` @[coe] protected noncomputable def coe (a : A) : ๐“œ(๐•œ, A) := { fst := ContinuousLinearMap.mul ๐•œ A a diff --git a/Mathlib/Analysis/Quaternion.lean b/Mathlib/Analysis/Quaternion.lean index 14a079dfa5a35..e41480ad1e545 100644 --- a/Mathlib/Analysis/Quaternion.lean +++ b/Mathlib/Analysis/Quaternion.lean @@ -86,7 +86,6 @@ noncomputable instance : NormedDivisionRing โ„ where simp only [norm_eq_sqrt_real_inner, inner_self, normSq.map_mul] exact Real.sqrt_mul normSq_nonneg _ --- Porting note: added `noncomputable` noncomputable instance : NormedAlgebra โ„ โ„ where norm_smul_le := norm_smul_le toAlgebra := Quaternion.algebra diff --git a/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean b/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean index ee138b0e38a78..633d6872c7ad0 100644 --- a/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean +++ b/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean @@ -25,14 +25,7 @@ open Opposite open MonoidalCategory --- Porting note: made it noncomputable. --- `failed to compile definition, consider marking it as 'noncomputable' because it` --- `depends on 'CategoryTheory.typesMonoidal', and it does not have executable code` --- I don't know if that is a problem, might need to change it back in the future, but --- if so it might be better to fix then instead of at the moment of porting. - /-- `(๐Ÿ™_ C โŸถ -)` is a lax monoidal functor to `Type`. -/ -noncomputable def coyonedaTensorUnit (C : Type u) [Category.{v} C] [MonoidalCategory C] : LaxMonoidalFunctor C (Type v) := .ofTensorHom (F := coyoneda.obj (op (๐Ÿ™_ C))) diff --git a/Mathlib/Computability/PartrecCode.lean b/Mathlib/Computability/PartrecCode.lean index 5bb50ca1e5675..d061b8f7736f9 100644 --- a/Mathlib/Computability/PartrecCode.lean +++ b/Mathlib/Computability/PartrecCode.lean @@ -79,7 +79,6 @@ inductive Code : Type | prec : Code โ†’ Code โ†’ Code | rfind' : Code โ†’ Code --- Porting note: `Nat.Partrec.Code.recOn` is noncomputable in Lean4, so we make it computable. compile_inductive% Code end Nat.Partrec diff --git a/Mathlib/Computability/TMToPartrec.lean b/Mathlib/Computability/TMToPartrec.lean index 762a216837a6e..dcc03fdf10e6c 100644 --- a/Mathlib/Computability/TMToPartrec.lean +++ b/Mathlib/Computability/TMToPartrec.lean @@ -867,7 +867,6 @@ inductive ฮ›' | pred (qโ‚ qโ‚‚ : ฮ›') | ret (k : Cont') --- Porting note: `Turing.PartrecToTM2.ฮ›'.rec` is noncomputable in Lean4, so we make it computable. compile_inductive% Code compile_inductive% Cont' compile_inductive% K' diff --git a/Mathlib/Data/Analysis/Topology.lean b/Mathlib/Data/Analysis/Topology.lean index 1e7c2003dc521..f8db5f20dd999 100644 --- a/Mathlib/Data/Analysis/Topology.lean +++ b/Mathlib/Data/Analysis/Topology.lean @@ -153,10 +153,8 @@ theorem ext [T : TopologicalSpace ฮฑ] {ฯƒ : Type*} {F : Ctop ฮฑ ฯƒ} (Hโ‚ : โˆ€ variable [TopologicalSpace ฮฑ] --- Porting note: add non-computable : because --- > ... it depends on `Inter.inter`, and it does not have executable code. /-- The topological space realizer made of the open sets. -/ -protected noncomputable def id : Realizer ฮฑ := +protected def id : Realizer ฮฑ := โŸจ{ x : Set ฮฑ // IsOpen x }, { f := Subtype.val top := fun _ โ†ฆ โŸจuniv, isOpen_univโŸฉ diff --git a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean index e0216810f736e..4710b819f0406 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean @@ -83,10 +83,6 @@ variable {G : Type*} [Group G] namespace haar --- Porting note: Even in `noncomputable section`, a definition with `to_additive` require --- `noncomputable` to generate an additive definition. --- Please refer to leanprover/lean4#2077. - /-- The index or Haar covering number or ratio of `K` w.r.t. `V`, denoted `(K : V)`: it is the smallest number of (left) translates of `V` that is necessary to cover `K`. It is defined to be 0 if no finite number of translates cover `K`. -/ @@ -341,11 +337,6 @@ theorem nonempty_iInter_clPrehaar (Kโ‚€ : PositiveCompacts G) : ### Lemmas about `chaar` -/ - --- Porting note: Even in `noncomputable section`, a definition with `to_additive` require --- `noncomputable` to generate an additive definition. --- Please refer to leanprover/lean4#2077. - /-- This is the "limit" of `prehaar Kโ‚€ U K` as `U` becomes a smaller and smaller open neighborhood of `(1 : G)`. More precisely, it is defined to be an arbitrary element in the intersection of all the sets `clPrehaar Kโ‚€ V` in `haarProduct Kโ‚€`. @@ -463,10 +454,6 @@ theorem is_left_invariant_chaar {Kโ‚€ : PositiveCompacts G} (g : G) (K : Compact apply is_left_invariant_prehaar; rw [h2U.interior_eq]; exact โŸจ1, h3UโŸฉ ยท apply continuous_iff_isClosed.mp this; exact isClosed_singleton --- Porting note: Even in `noncomputable section`, a definition with `to_additive` require --- `noncomputable` to generate an additive definition. --- Please refer to leanprover/lean4#2077. - /-- The function `chaar` interpreted in `โ„โ‰ฅ0`, as a content -/ @[to_additive "additive version of `MeasureTheory.Measure.haar.haarContent`"] noncomputable def haarContent (Kโ‚€ : PositiveCompacts G) : Content G where @@ -518,13 +505,8 @@ open haar ### The Haar measure -/ - variable [TopologicalSpace G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] --- Porting note: Even in `noncomputable section`, a definition with `to_additive` require --- `noncomputable` to generate an additive definition. --- Please refer to leanprover/lean4#2077. - /-- The Haar measure on the locally compact group `G`, scaled so that `haarMeasure Kโ‚€ Kโ‚€ = 1`. -/ @[to_additive "The Haar measure on the locally compact additive group `G`, scaled so that From 85db8c7fd2bcb8d447952bf124670d70e3815d10 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Sat, 27 Jul 2024 23:23:26 +0000 Subject: [PATCH 2/2] feat: generalize `Int.cast_nonneg` and related lemmas (#15186) --- Mathlib/Algebra/Order/Ring/Cast.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Order/Ring/Cast.lean b/Mathlib/Algebra/Order/Ring/Cast.lean index 2f8d74e4b82bf..06e3f2297e000 100644 --- a/Mathlib/Algebra/Order/Ring/Cast.lean +++ b/Mathlib/Algebra/Order/Ring/Cast.lean @@ -24,15 +24,17 @@ open Function Nat variable {R : Type*} namespace Int -section OrderedRing -variable [OrderedRing R] +section OrderedAddCommGroupWithOne + +variable [AddCommGroupWithOne R] [PartialOrder R] [CovariantClass R R (ยท + ยท) (ยท โ‰ค ยท)] +variable [ZeroLEOneClass R] [NeZero (1 : R)] lemma cast_mono : Monotone (Int.cast : โ„ค โ†’ R) := by intro m n h rw [โ† sub_nonneg] at h lift n - m to โ„• using h with k hk rw [โ† sub_nonneg, โ† cast_sub, โ† hk, cast_natCast] - exact k.cast_nonneg + exact k.cast_nonneg' variable [Nontrivial R] {m n : โ„ค} @@ -56,7 +58,7 @@ lemma cast_strictMono : StrictMono (fun x : โ„ค => (x : R)) := @[simp] lemma cast_lt_zero : (n : R) < 0 โ†” n < 0 := by rw [โ† cast_zero, cast_lt] -end OrderedRing +end OrderedAddCommGroupWithOne section LinearOrderedRing variable [LinearOrderedRing R] {a b n : โ„ค} {x : R}