typeclass for has_coe_to_fun is slow?

Stream: general

[Kenny Lau]

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]

I can't profiler the time for some reason

[Kenny Lau]

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

[Kenny Lau]

are we ready for bundled morphisms?

[Kenny Lau]

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]

[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]

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

[Kenny Lau]

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]

what's going on?

[Kenny Lau]

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]

practically impossible

[Kevin Buzzard]

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]

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]

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]

link to what I think Kenny is doing

[Kenny Lau]

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

[Kenny Lau]

particularly the definition of exact couple

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kenny Lau]

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

[Kenny Lau]

maybe that's why

[Kenny Lau]

so maybe I should really factor this out

[Kenny Lau]

but then why is the exact couple definition slow?

[Kevin Buzzard]

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]

interesting

[Kevin Buzzard]

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]

Try that.

[Kenny Lau]

thanks

[Kevin Buzzard]

it's much better