## Stream: general

### Topic: slow elaboration of a proof

#### Yakov Pechersky (Jan 03 2022 at 23:02):

Consider the following on master:

import ring_theory.laurent_series

lemma is_unit_of_mem_non_zero_divisors {G₀ : Type*} [group_with_zero G₀]
{x : G₀} (hx : x ∈ non_zero_divisors G₀) :
is_unit x :=
⟨⟨x, x⁻¹, mul_inv_cancel (non_zero_divisors.ne_zero hx),
inv_mul_cancel (non_zero_divisors.ne_zero hx)⟩, rfl⟩

set_option profiler true

instance {K : Type*} [field K] : is_fraction_ring (power_series K) (laurent_series K) :=
{ map_units := begin
rintro ⟨y, hy⟩,
rw [laurent_series.coe_algebra_map, subtype.coe_mk],
refine is_unit_of_mem_non_zero_divisors _,
have : function.injective (hahn_series.of_power_series ℤ K) :=
hahn_series.of_power_series_injective,
exact ring_hom.map_mem_non_zero_divisors (hahn_series.of_power_series ℤ K) this hy
end,
surj := sorry,
eq_iff_exists := sorry }

#exit


On my machine it takes 40 seconds, where the offending line seems to be the one starting with exact ring_hom.... What's going on here?

#### Yakov Pechersky (Jan 03 2022 at 23:03):

Something else is up too -- if I change the proof to

{ map_units := begin
rintro ⟨y, hy⟩,
rw [laurent_series.coe_algebra_map],
refine is_unit_of_mem_non_zero_divisors _,
have : function.injective (algebra_map (power_series K) (laurent_series K)) :=
hahn_series.of_power_series_injective,
sorry,
end,


that is also very slow

#### Eric Rodriguez (Jan 03 2022 at 23:07):

injective algebra maps and slow functions :) does specifying the TC arguments speed it up?

#### Alex J. Best (Jan 03 2022 at 23:28):

I don't know the root cause, but this is some sort of universe issue, changing to

universe u
instance {K : Type*} [field K] : is_fraction_ring (power_series K) (laurent_series K) :=
{ map_units := begin
rintro ⟨y, hy⟩,
rw [laurent_series.coe_algebra_map, subtype.coe_mk],
refine is_unit_of_mem_non_zero_divisors _,
have : function.injective (hahn_series.of_power_series ℤ K) :=
hahn_series.of_power_series_injective,
exact ring_hom.map_mem_non_zero_divisors (hahn_series.of_power_series ℤ K) this hy,
end,
surj := sorry,
eq_iff_exists := sorry }


it becomes instant for me, edit: ok maybe not instant but seems way faster

#### Yakov Pechersky (Jan 03 2022 at 23:28):

@Eric Rodriguez which of the TC arguments? For which statement?

#### Yakov Pechersky (Jan 03 2022 at 23:29):

Even with universes, this is slow for me:

import ring_theory.laurent_series

universe u

lemma is_unit_of_mem_non_zero_divisors {G₀ : Type u} [group_with_zero G₀]
{x : G₀} (hx : x ∈ non_zero_divisors G₀) :
is_unit x :=
⟨⟨x, x⁻¹, mul_inv_cancel (non_zero_divisors.ne_zero hx),
inv_mul_cancel (non_zero_divisors.ne_zero hx)⟩, rfl⟩

set_option profiler true

instance {K : Type u} [field K] : is_fraction_ring (power_series K) (laurent_series K) :=
{ map_units := begin
rintro ⟨y, hy⟩,
rw [laurent_series.coe_algebra_map],
refine is_unit_of_mem_non_zero_divisors _,
have : function.injective (algebra_map (power_series K) (laurent_series K)) :=
hahn_series.of_power_series_injective,
sorry,
end,
surj := sorry,
eq_iff_exists := sorry }

#exit


#### Yakov Pechersky (Jan 03 2022 at 23:30):

But I can corroborate that {K : Type u} speeds it up!

#### Alex J. Best (Jan 03 2022 at 23:31):

Hm very strange, I have that exact file and it is only a second or so

#### Yakov Pechersky (Jan 03 2022 at 23:32):

Alex, with the exact line or the function.injective (algebra_map ...) line?

#### Alex J. Best (Jan 03 2022 at 23:33):

Oh right sorry, with exact + universes it is fast

#### Alex J. Best (Jan 03 2022 at 23:34):

But the second one is still slow

#### Yakov Pechersky (Jan 03 2022 at 23:38):

Strange. Gonna sweep it under the rug and just PR with the fast version. Thanks for the quick fix! #11220

Last updated: Dec 20 2023 at 11:08 UTC