Zulip Chat Archive

Stream: general

Topic: typeclass for has_coe_to_fun is slow?


view this post on Zulip 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)

view this post on Zulip Kenny Lau (Apr 21 2020 at 05:21):

I can't profiler the time for some reason

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 21 2020 at 05:31):

are we ready for bundled morphisms?

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Apr 21 2020 at 05:37):

what's going on?

view this post on Zulip 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 } }

view this post on Zulip Kenny Lau (Apr 21 2020 at 05:57):

practically impossible

view this post on Zulip 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.

view this post on Zulip 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...)

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 22 2020 at 11:42):

link to what I think Kenny is doing

view this post on Zulip Kenny Lau (Apr 22 2020 at 11:44):

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

view this post on Zulip Kenny Lau (Apr 22 2020 at 11:45):

particularly the definition of exact couple

view this post on Zulip Kenny Lau (Apr 22 2020 at 11:45):

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

view this post on Zulip 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.

view this post on Zulip 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})

view this post on Zulip Kevin Buzzard (Apr 22 2020 at 11:48):

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

view this post on Zulip Kenny Lau (Apr 22 2020 at 11:48):

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

view this post on Zulip Kenny Lau (Apr 22 2020 at 11:48):

maybe that's why

view this post on Zulip Kenny Lau (Apr 22 2020 at 11:49):

so maybe I should really factor this out

view this post on Zulip Kenny Lau (Apr 22 2020 at 11:49):

but then why is the exact couple definition slow?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 22 2020 at 11:50):

interesting

view this post on Zulip 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
}

view this post on Zulip Kevin Buzzard (Apr 22 2020 at 11:50):

Try that.

view this post on Zulip Kenny Lau (Apr 22 2020 at 11:50):

thanks

view this post on Zulip Kevin Buzzard (Apr 22 2020 at 11:50):

it's much better


Last updated: May 08 2021 at 04:14 UTC