Zulip Chat Archive
Stream: general
Topic: timeout (universe or diamond? not sure)
Kevin Buzzard (Feb 21 2022 at 17:50):
Here's something @David Ang pointed out on the Discord. units_mod.fintype and units_mod.fintype' are identical modulo an extra id. They both compile fine and give defeq answers. However if I generalise the units.fg instance to allow K : Type u then the first instance still compiles but the second one starts timing out. I feel like I've been getting quite good at these issues recently but here I'm lost; I'm not sure whether I should be looking for a diamond, or whether this is a universe issue.
import number_theory.number_field
open_locale number_field
universe u
variables {G : Type u} [comm_group G]
local notation n`⬝`G := (zpow_group_hom n : G →* G).range
noncomputable instance quotient_group.fintype_of_fg [group.fg G] (n : ℤ) : fintype $ G ⧸ (n⬝G) :=
classical.choice sorry -- avoiding sorrying data
-- change {K : Type} to {K : Type u} and units_mod.fintype' times out
instance units.fg {K : Type} [field K] [number_field K] : group.fg (𝓞 K)ˣ := sorry
variables {L : Type} [field L] [number_field L]
noncomputable instance units_mod.fintype (n : ℤ) : fintype $ (𝓞 L)ˣ ⧸ (n⬝(𝓞 L)ˣ) :=
@quotient_group.fintype_of_fg (𝓞 L)ˣ _ (@id _ @units.fg L _ _) n
-- the same but without an id
noncomputable instance units_mod.fintype' (n : ℤ) : fintype $ (𝓞 L)ˣ ⧸ (n⬝(𝓞 L)ˣ) :=
@quotient_group.fintype_of_fg (𝓞 L)ˣ _ (@units.fg L _ _) n
example : @units_mod.fintype = @units_mod.fintype' := rfl
Mario Carneiro (Feb 21 2022 at 17:53):
by the way the id there is doing a weird thing, it's applying directly to @units.fg, not @units.fg L _ _
Mario Carneiro (Feb 21 2022 at 17:54):
and since id is not reducible you should expect it to change the results of all the typeclass searches in those _
Mario Carneiro (Feb 21 2022 at 17:54):
although that doesn't really solve the question
Kevin Buzzard (Feb 21 2022 at 17:55):
oh yeah, thanks; putting in the brackets doesn't change anything though.
Kevin Buzzard (Feb 21 2022 at 18:01):
With trace.class_instances true the traces for units_mod.fintype and units_mod.fintype' are identical (over 5800 lines of it).
Mario Carneiro (Feb 21 2022 at 18:02):
My guess is something in defeq checking
Mario Carneiro (Feb 21 2022 at 18:10):
Hm, there is a type mismatch:
--- src/expected.txt 2022-02-21 13:06:48.514253485 -0500
+++ src/produced.txt 2022-02-21 13:06:58.170170784 -0500
@@ -1,140 +1,93 @@
@group.fg.{0}
(@units.{0}
(@coe_sort.{1 2} ...)
(@ring.to_monoid.{0}...))
- (@comm_group.to_group.{0}
- (@units.{0}
- (@coe_sort.{1 2}
+ (@units.group.{0}
+ (@coe_sort.{1 2}
+ (@subalgebra.{0 0} int L (@comm_ring.to_comm_semiring.{0} int int.comm_ring)
+ (@ring.to_semiring.{0} L
+ (@comm_ring.to_ring.{0} L
+ (@euclidean_domain.to_comm_ring.{0} L (@field.to_euclidean_domain.{0} L _inst_2))))
+ (@algebra_int.{0} L (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_2))))
+ Type
+ (@set_like.has_coe_to_sort.{0 0}
(@subalgebra.{0 0} int L (@comm_ring.to_comm_semiring.{0} int int.comm_ring)
(@ring.to_semiring.{0} L
(@comm_ring.to_ring.{0} L
(@euclidean_domain.to_comm_ring.{0} L (@field.to_euclidean_domain.{0} L _inst_2))))
(@algebra_int.{0} L (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_2))))
- Type
- (@set_like.has_coe_to_sort.{0 0}
- (@subalgebra.{0 0} int L (@comm_ring.to_comm_semiring.{0} int int.comm_ring)
- (@ring.to_semiring.{0} L
- (@comm_ring.to_ring.{0} L
- (@euclidean_domain.to_comm_ring.{0} L (@field.to_euclidean_domain.{0} L _inst_2))))
- (@algebra_int.{0} L (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_2))))
- L
- (@subalgebra.set_like.{0 0} int L (@comm_ring.to_comm_semiring.{0} int int.comm_ring)
- (@ring.to_semiring.{0} L
- (@comm_ring.to_ring.{0} L
- (@euclidean_domain.to_comm_ring.{0} L (@field.to_euclidean_domain.{0} L _inst_2))))
- (@algebra_int.{0} L (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_2)))))
- (@number_field.ring_of_integers.{0} L _inst_2))
- (@ring.to_monoid.{0}
- (@coe_sort.{1 2}
- (@subalgebra.{0 0} int L (@comm_ring.to_comm_semiring.{0} int int.comm_ring)
- (@ring.to_semiring.{0} L
- (@comm_ring.to_ring.{0} L
- (@euclidean_domain.to_comm_ring.{0} L (@field.to_euclidean_domain.{0} L _inst_2))))
- (@algebra_int.{0} L (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_2))))
- Type
- (@set_like.has_coe_to_sort.{0 0}
- (@subalgebra.{0 0} int L (@comm_ring.to_comm_semiring.{0} int int.comm_ring)
- (@ring.to_semiring.{0} L
- (@comm_ring.to_ring.{0} L
- (@euclidean_domain.to_comm_ring.{0} L (@field.to_euclidean_domain.{0} L _inst_2))))
- (@algebra_int.{0} L (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_2))))
- L
- (@subalgebra.set_like.{0 0} int L (@comm_ring.to_comm_semiring.{0} int int.comm_ring)
- (@ring.to_semiring.{0} L
- (@comm_ring.to_ring.{0} L
- (@euclidean_domain.to_comm_ring.{0} L (@field.to_euclidean_domain.{0} L _inst_2))))
- (@algebra_int.{0} L (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_2)))))
- (@number_field.ring_of_integers.{0} L _inst_2))
- (@subalgebra.to_ring.{0 0} int L int.comm_ring
- (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_2))
- (@algebra_int.{0} L (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_2)))
- (@number_field.ring_of_integers.{0} L _inst_2))))
- (@units.comm_group.{0}
+ L
+ (@subalgebra.set_like.{0 0} int L (@comm_ring.to_comm_semiring.{0} int int.comm_ring)
+ (@ring.to_semiring.{0} L
+ (@comm_ring.to_ring.{0} L
+ (@euclidean_domain.to_comm_ring.{0} L (@field.to_euclidean_domain.{0} L _inst_2))))
+ (@algebra_int.{0} L (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_2)))))
+ (@number_field.ring_of_integers.{0} L _inst_2))
+ (@ring.to_monoid.{0}
(@coe_sort.{1 2} ...)
- (@comm_ring.to_comm_monoid.{0}
- (@coe_sort.{1 2}
- (@subalgebra.{0 0} int L (@comm_ring.to_comm_semiring.{0} int int.comm_ring)
- (@ring.to_semiring.{0} L
- (@comm_ring.to_ring.{0} L
- (@euclidean_domain.to_comm_ring.{0} L (@field.to_euclidean_domain.{0} L _inst_2))))
- (@algebra_int.{0} L (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_2))))
- Type
- (@set_like.has_coe_to_sort.{0 0}
- (@subalgebra.{0 0} int L (@comm_ring.to_comm_semiring.{0} int int.comm_ring)
- (@ring.to_semiring.{0} L
- (@comm_ring.to_ring.{0} L
- (@euclidean_domain.to_comm_ring.{0} L (@field.to_euclidean_domain.{0} L _inst_2))))
- (@algebra_int.{0} L (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_2))))
- L
- (@subalgebra.set_like.{0 0} int L (@comm_ring.to_comm_semiring.{0} int int.comm_ring)
- (@ring.to_semiring.{0} L
- (@comm_ring.to_ring.{0} L
- (@euclidean_domain.to_comm_ring.{0} L (@field.to_euclidean_domain.{0} L _inst_2))))
- (@algebra_int.{0} L (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_2)))))
- (@number_field.ring_of_integers.{0} L _inst_2))
- (@subalgebra.to_comm_ring.{0 0} int L int.comm_ring
- (@euclidean_domain.to_comm_ring.{0} L (@field.to_euclidean_domain.{0} L _inst_2))
- (@algebra_int.{0} L (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_2)))
- (@number_field.ring_of_integers.{0} L _inst_2)))))
+ (@subalgebra.to_ring.{0 0} int L int.comm_ring
+ (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_2))
+ (@algebra_int.{0} L (@division_ring.to_ring.{0} L (@field.to_division_ring.{0} L _inst_2)))
+ (@number_field.ring_of_integers.{0} L _inst_2))))
Mario Carneiro (Feb 21 2022 at 18:11):
so somewhere in that monstrosity is an expensive defeq test
Kevin Buzzard (Feb 21 2022 at 18:15):
I found something like this and extracted two terms and checked they were equal with rfl and it was really quick
Mario Carneiro (Feb 21 2022 at 18:15):
For context, I'm comparing the goal to the have in this example:
-- to ensure that units.fg is not getting unfolded
constant {v} units.fg {K : Type v} [field K] [number_field K] : group.fg (𝓞 K)ˣ
-- the same but without an id
noncomputable example {L : Type} [field L] [number_field L] (n : ℤ) : fintype $ (𝓞 L)ˣ ⧸ (n⬝(𝓞 L)ˣ) :=
begin
refine @quotient_group.fintype_of_fg (𝓞 L)ˣ _ (id _) n,
have := @units.fg L _ _,
exact @units.fg L _ _,
end
Mario Carneiro (Feb 21 2022 at 18:15):
if you use exact this it is quick, and if you use @units.fg.{0} L _ _ it is also quick
Mario Carneiro (Feb 21 2022 at 18:16):
so I think it has something to do with solving that equation while units.fg.{?u} still has a metavariable
Mario Carneiro (Feb 21 2022 at 18:16):
even though applying it to L will solve the metavariable
Kevin Buzzard (Feb 21 2022 at 18:17):
Aah yes, the two humungous terms of type comm_group (↥(𝓞 L))ˣ which I had were when we were in Type 0.
Kevin Buzzard (Feb 21 2022 at 19:00):
If I tell Lean the universe level of units.fg it works. This really surprises me; I guess I don't know how Lean is solving universe variables (in the sense that this proves that it's not looking at L and saying "aah yes, let's use u=0"). Note we're id-free here.
import number_theory.number_field
open_locale number_field
universe u
variables {G : Type u} [comm_group G]
local notation n`⬝`G := (zpow_group_hom n : G →* G).range
noncomputable instance quotient_group.fintype_of_fg [group.fg G] (n : ℤ) : fintype $ G ⧸ (n⬝G) :=
classical.choice sorry -- avoiding sorrying data
instance units.fg {K : Type u} [field K] [number_field K] : group.fg (𝓞 K)ˣ := sorry
variables {L : Type} [field L] [number_field L]
-- works!
noncomputable instance units_mod.fintype' (n : ℤ) : fintype $ (𝓞 L)ˣ ⧸ (n⬝(𝓞 L)ˣ) :=
@quotient_group.fintype_of_fg (𝓞 L)ˣ _ (@units.fg.{0} L _inst_2 _inst_3) n
-- Now remove `.{0}` in `units.fg` and it fails
noncomputable instance units_mod.fintype (n : ℤ) : fintype $ (𝓞 L)ˣ ⧸ (n⬝(𝓞 L)ˣ) :=
@quotient_group.fintype_of_fg (𝓞 L)ˣ _ (@units.fg L _inst_2 _inst_3) n
Kevin Buzzard (Feb 21 2022 at 19:09):
-- make field explicit in units.fg
instance units.fg (K : Type u) [field K] [number_field K] : group.fg (𝓞 K)ˣ := sorry
variables {L : Type} [field L] [number_field L]
-- works very quickly
noncomputable instance units_mod.fintype'' (n : ℤ) : fintype $ (𝓞 L)ˣ ⧸ (n⬝(𝓞 L)ˣ) :=
@quotient_group.fintype_of_fg (𝓞 L)ˣ _ (@units.fg.{0} L _ _) n
-- works but takes quite a long time
noncomputable instance units_mod.fintype' (n : ℤ) : fintype $ (𝓞 L)ˣ ⧸ (n⬝(𝓞 L)ˣ) :=
@quotient_group.fintype_of_fg (𝓞 L)ˣ _ (units.fg.{0} L) n
-- times out without universe hint
noncomputable instance units_mod.fintype (n : ℤ) : fintype $ (𝓞 L)ˣ ⧸ (n⬝(𝓞 L)ˣ) :=
@quotient_group.fintype_of_fg.{0} (𝓞 L)ˣ _ (@units.fg L _ _) n
-- times out without universe hint
noncomputable instance units_mod.fintype (n : ℤ) : fintype $ (𝓞 L)ˣ ⧸ (n⬝(𝓞 L)ˣ) :=
@quotient_group.fintype_of_fg.{0} (𝓞 L)ˣ _ (units.fg L) n
Last updated: Dec 20 2023 at 11:08 UTC