Zulip Chat Archive

Stream: general

Topic: typeclass for has_coe_to_fun is slow?


Kenny Lau (Apr 21 2020 at 05:21):

import group_theory.quotient_group

universes u v

structure exact_couple : Type ((max u v) + 1) :=
(A : Type u) [Ag: add_comm_group A]
(E : Type v) [Eg: add_comm_group E]
(i : A →+ A)
(j : A →+ E)
(k : E →+ A)
(hij :  x : A, (j (i x) : E) = 0)
(hji :  y : A, (j y : E) = 0   x : A, (i x : A) = y)

Kenny Lau (Apr 21 2020 at 05:21):

I can't profiler the time for some reason

Kenny Lau (Apr 21 2020 at 05:22):

but has_coe_to_fun (A →+ E) takes a long time to resolve according to trace.class_instances

Kenny Lau (Apr 21 2020 at 05:31):

are we ready for bundled morphisms?

Kenny Lau (Apr 21 2020 at 05:32):

looks like I didn't do the control, because somehow this is slow also:

structure exact_couple : Type ((max u v) + 1) :=
(A : Type u) [Ag: add_comm_group A]
(E : Type v) [Eg: add_comm_group E]
(i : A  A) --[hi : is_add_group_hom i]
(j : A  E) --[hi : is_add_group_hom i]
(k : E  A) --[hi : is_add_group_hom i]
(hij :  x : A, (j (i x) : E) = 0)
(hji :  y : A, (j y : E) = 0   x : A, (i x : A) = y)
(hjk :  x : A, (k (j x) : A) = 0)
(hkj :  y : E, (k y : A) = 0   x : A, (j x : E) = y)
(hki :  x : E, (i (k x) : A) = 0)
(hik :  y : A, (i y : A) = 0   x : E, (k x : A) = y)

Kenny Lau (Apr 21 2020 at 05:33):

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : has_sizeof (Type u) := @add_submonoid.has_sizeof_inst ?x_1 ?x_2
failed is_def_eq
[...]
[class_instances] (0) ?x_0 : has_sizeof ( (x : A), k (j x) = 0) := @is_lawful_traversable.has_sizeof_inst ?x_128 ?x_129
failed is_def_eq
[class_instances] (0) ?x_0 : has_sizeof ( (x : A), k (j x) = 0) := traversable.has_sizeof_inst ?x_130
failed is_def_eq
[class_instances] (0) ?x_
(message too long, truncated at 262144 characters)

Kenny Lau (Apr 21 2020 at 05:35):

does this mean I have to move everything to the left of the colon? I've never seen this before

Kenny Lau (Apr 21 2020 at 05:36):

but this is still slow:

structure exact_couple (A : Type u) [add_comm_group A] (E : Type v) [add_comm_group E]
  (i : A  A) --[hi : is_add_group_hom i]
(j : A  E) --[hi : is_add_group_hom i]
(k : E  A) --[hi : is_add_group_hom i]
: Prop :=
(hij :  x : A, (j (i x) : E) = 0)
(hji :  y : A, (j y : E) = 0   x : A, (i x : A) = y)
(hjk :  x : A, (k (j x) : A) = 0)
(hkj :  y : E, (k y : A) = 0   x : A, (j x : E) = y)
(hki :  x : E, (i (k x) : A) = 0)
(hik :  y : A, (i y : A) = 0   x : E, (k x : A) = y)

Kenny Lau (Apr 21 2020 at 05:37):

what's going on?

Kenny Lau (Apr 21 2020 at 05:57):

Lean is so slow, this is impossible to finish:

import group_theory.quotient_group

universes u v

structure exact_couple : Type ((max u v) + 1) :=
(A : Type u) [Ag: add_comm_group A]
(E : Type v) [Eg: add_comm_group E]
(i : A  A) [hi : is_add_group_hom i]
(j : A  E) [hj : is_add_group_hom j]
(k : E  A) [hk : is_add_group_hom k]
(hij :  x : A, (j (i x) : E) = 0)
(hji :  y : A, (j y : E) = 0   x : A, (i x : A) = y)
(hjk :  x : A, (k (j x) : A) = 0)
(hkj :  y : E, (k y : A) = 0   x : A, (j x : E) = y)
(hki :  x : E, (i (k x) : A) = 0)
(hik :  y : A, (i y : A) = 0   x : E, (k x : A) = y)
attribute [instance] exact_couple.Ag exact_couple.Eg exact_couple.hi exact_couple.hj exact_couple.hk

def exact_couple.derived (C : exact_couple.{u v}) : exact_couple.{u v} :=
{ A := set.range C.i,
  --Ag := range.is_add_submonoid C.i,
  E := by letI := is_add_group_hom.comp C.k C.j; exact @quotient_add_group.quotient
    (is_add_group_hom.ker (C.j  C.k)) _
    { y |  x : C.E, C.j (C.k x) = y.1 }
    { add_mem := by rintros ⟨_, h1 ⟨_, h2 x1, h3 x2, h4⟩; dsimp only at h3 h4; substs h3 h4; use x1+x2;
        rw [is_add_monoid_hom.map_add C.k, is_add_monoid_hom.map_add C.j]; refl,
      zero_mem := 0, by rw [is_add_group_hom.map_zero C.k, is_add_group_hom.map_zero C.j]; refl,
      neg_mem := by rintros ⟨_, h x, H⟩; dsimp only at H; subst H; use -x;
        rw [is_add_group_hom.map_neg C.k, is_add_group_hom.map_neg C.j]; refl } }

Kenny Lau (Apr 21 2020 at 05:57):

practically impossible

Kevin Buzzard (Apr 22 2020 at 11:37):

Why don't you factor out the construction of derived E? The derived E is just ker(d) over im(d), right? with d=j \circ k. This construction deserves a bit of API of its own I should think. You seem to be proving that the image of d is a normal subgroup of the kernel of d in the middle of things. I should think that if you're going for the spectral sequence of an exact couple then the fact that d^2=0 gives some magic new ker(d)/im(d) which is functorial in (A,d) is a pretty important thing which needs maybe to be done first.

Kevin Buzzard (Apr 22 2020 at 11:37):

Note also that everything should be done for R-modules (and Scott would say everything needs to be done for abelian categories, but at the minute this would be out of the frying pan...)

Kevin Buzzard (Apr 22 2020 at 11:41):

It takes 1 second on my home PC to compile the partial derived couple code, it's not practically impossible at all to work with the definition as it stands, I just wrote i := λ a, ⟨C.i a, a, rfl⟩, no problem at all. Do you have access to a faster computer? It's holding you back. Still I think that pulling out the definition of derived E is the correct thing to do.

Kevin Buzzard (Apr 22 2020 at 11:42):

link to what I think Kenny is doing

Kenny Lau (Apr 22 2020 at 11:44):

yes, there are work-arounds, but this shouldn't be slow is my point

Kenny Lau (Apr 22 2020 at 11:45):

particularly the definition of exact couple

Kenny Lau (Apr 22 2020 at 11:45):

"Nothing is more permanent than a temporary solution." -- Russian Proverb

Kevin Buzzard (Apr 22 2020 at 11:47):

I just filled in all the remaining fields with sorry and I think there's a problem with your code.

Kevin Buzzard (Apr 22 2020 at 11:48):

failed to synthesize type class instance for
C : exact_couple
 add_comm_group
    (let _inst : is_add_group_hom (C.j  C.k) := _
     in quotient_add_group.quotient {y : (is_add_group_hom.ker (C.j  C.k)) |  (x : C.E), C.j (C.k x) = y.val})

Kevin Buzzard (Apr 22 2020 at 11:48):

could the slowness be the time it's taking this to fail?

Kenny Lau (Apr 22 2020 at 11:48):

it isn't an instance the composition of group hom is a group hom

Kenny Lau (Apr 22 2020 at 11:48):

maybe that's why

Kenny Lau (Apr 22 2020 at 11:49):

so maybe I should really factor this out

Kenny Lau (Apr 22 2020 at 11:49):

but then why is the exact couple definition slow?

Kevin Buzzard (Apr 22 2020 at 11:49):

def exact_couple.derived (C : exact_couple.{u v}) : exact_couple.{u v} :=
{ A := set.range C.i,
  --Ag := range.is_add_submonoid C.i,
  E := by letI := is_add_group_hom.comp C.k C.j; exact @quotient_add_group.quotient
    (is_add_group_hom.ker (C.j  C.k)) _
    { y |  x : C.E, C.j (C.k x) = y.1 }
    { add_mem := by rintros ⟨_, h1 ⟨_, h2 x1, h3 x2, h4⟩; dsimp only at h3 h4; substs h3 h4; use x1+x2;
        rw [is_add_monoid_hom.map_add C.k, is_add_monoid_hom.map_add C.j]; refl,
      zero_mem := 0, by rw [is_add_group_hom.map_zero C.k, is_add_group_hom.map_zero C.j]; refl,
      neg_mem := by rintros ⟨_, h x, H⟩; dsimp only at H; subst H; use -x;
        rw [is_add_group_hom.map_neg C.k, is_add_group_hom.map_neg C.j]; refl },
  i := λ a, C.i a, a, rfl,
  hi := sorry,
  j := sorry,
  hj := sorry,
  k := sorry,
  hk := sorry,
  hij := sorry,
  hji := sorry,
  hjk := sorry,
  hkj := sorry,
  hki := sorry,
  hik := sorry
}

It's much faster for me now, when I fill in all the remaining fields

Kenny Lau (Apr 22 2020 at 11:50):

interesting

Kevin Buzzard (Apr 22 2020 at 11:50):

def exact_couple.derived (C : exact_couple.{u v}) : exact_couple.{u v} :=
{ A := set.range C.i,
  --Ag := range.is_add_submonoid C.i,
  Ag := sorry,
  E := by letI := is_add_group_hom.comp C.k C.j; exact @quotient_add_group.quotient
    (is_add_group_hom.ker (C.j  C.k)) _
    { y |  x : C.E, C.j (C.k x) = y.1 }
    { add_mem := by rintros ⟨_, h1 ⟨_, h2 x1, h3 x2, h4⟩; dsimp only at h3 h4; substs h3 h4; use x1+x2;
        rw [is_add_monoid_hom.map_add C.k, is_add_monoid_hom.map_add C.j]; refl,
      zero_mem := 0, by rw [is_add_group_hom.map_zero C.k, is_add_group_hom.map_zero C.j]; refl,
      neg_mem := by rintros ⟨_, h x, H⟩; dsimp only at H; subst H; use -x;
        rw [is_add_group_hom.map_neg C.k, is_add_group_hom.map_neg C.j]; refl },
  Eg := sorry,
  i := λ a, C.i a, a, rfl,
  hi := sorry,
  j := sorry,
  hj := sorry,
  k := sorry,
  hk := sorry,
  hij := sorry,
  hji := sorry,
  hjk := sorry,
  hkj := sorry,
  hki := sorry,
  hik := sorry
}

Kevin Buzzard (Apr 22 2020 at 11:50):

Try that.

Kenny Lau (Apr 22 2020 at 11:50):

thanks

Kevin Buzzard (Apr 22 2020 at 11:50):

it's much better


Last updated: Dec 20 2023 at 11:08 UTC