refactoring proofs

Stream: new members

[Vasily Ilin]

I have a proof that compiles but takes a while to do so. What tricks can I use to refactor the proof to make it as "minimal" as possible? Here is the proof (the last lemma):

import ring_theory.tensor_product
import tactic

open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial

universe u
variables (K : Type u) [comm_semiring K]

@[simp] lemma assoc_symm_tmul {R : Type u} [comm_semiring R] {A : Type u} [semiring A] [algebra R A] {B : Type u} [semiring B] [algebra R B] {C : Type u} [semiring C] [algebra R C] (a : A) (b : B) (c : C) :
(algebra.tensor_product.assoc R A B C).symm (a ⊗ₜ[R] (b ⊗ₜ[R] c)) = a ⊗ₜ[R] b ⊗ₜ[R] c :=
begin
  apply_fun (algebra.tensor_product.assoc R A B C),
  rw assoc_tmul,
  rw alg_equiv.apply_symm_apply (algebra.tensor_product.assoc R A B C) (a ⊗ₜ[R] (b ⊗ₜ[R] c)),
  simp,
  unfold function.injective,
  intros a b h,
  exact h,
end

-- noncomputable def counit : K[X] →ₐ[K] K := polynomial.aeval 0

noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := aeval ((X ⊗ₜ 1) + (1 ⊗ₜ X))

@[simp] lemma comul_1 : comul K (1 : K[X]) = (1 ⊗ₜ 1 : K[X] ⊗[K] K[X]) :=
begin
  rw alg_hom.map_one (comul K), -- ⊢ 1 = 1 ⊗ₜ[K] 1
  refl,
end

@[simp] lemma comul_X : comul K X = X ⊗ₜ 1 + 1 ⊗ₜ X :=
begin
  unfold comul,
  rw aeval_X,
end


noncomputable def map1 : K[X] →ₐ[K] K[X] ⊗ K[X] ⊗ K[X] := (algebra.tensor_product.assoc K K[X] K[X] K[X]).symm.to_alg_hom.comp ((map (alg_hom.id K K[X]) (comul K)).comp (comul K))

noncomputable def map2 : (K[X] →ₐ[K] K[X] ⊗[K] K[X] ⊗[K] K[X] ) :=  (map (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X]) (alg_hom.id K K[X])).comp (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X])
. -- this tells Lean not to recompile definitions


lemma coassoc : map1 K = map2 K :=
begin
  have P1 : map1 K X = X ⊗ₜ 1 ⊗ₜ 1 + 1 ⊗ₜ X ⊗ₜ 1 + 1 ⊗ₜ 1 ⊗ₜ X,
    unfold map1,
    simp [tensor_product.tmul_add, add_assoc],

  have P2 : map2 K X = X ⊗ₜ 1 ⊗ₜ 1 + 1 ⊗ₜ X ⊗ₜ 1 + 1 ⊗ₜ 1 ⊗ₜ X,
    unfold map2,
    simp only [tensor_product.add_tmul, alg_hom.coe_comp, function.comp_app, comul_X, _root_.map_add, map_tmul, alg_hom.coe_id, id.def, comul_1],

  ext,
  rw P1,
  rw P2,
end

[Jireh Loreaux]

I haven't played around with your file at all, but squeeze_simp is helpful, and set_option profiler true can help determine where Lean is spending its time. You can also comment out portions of proofs (or use sorry), especially if you use tactic blocks.

For example, you can (temporarily) skip the proofs of the two have statements as follows (I think you need Lean 3.41 or 3.42 for this). So if you can't speed up the proof enough, you can at least make it less painful to edit around the file.

lemma coassoc : map1 K = map2 K :=
begin
  have P1 : map1 K X = X ⊗ₜ 1 ⊗ₜ 1 + 1 ⊗ₜ X ⊗ₜ 1 + 1 ⊗ₜ 1 ⊗ₜ X,
  sorry { unfold map1,
    simp [tensor_product.tmul_add, add_assoc] },

  have P2 : map2 K X = X ⊗ₜ 1 ⊗ₜ 1 + 1 ⊗ₜ X ⊗ₜ 1 + 1 ⊗ₜ 1 ⊗ₜ X,
  sorry {  unfold map2,
     simp only [tensor_product.add_tmul, alg_hom.coe_comp, function.comp_app, comul_X, _root_.map_add, map_tmul, alg_hom.coe_id, id.def, comul_1] },

  ext,
  rw P1,
  rw P2,
end

[Damiano Testa]

I did not actually re-think proofs, I simply restructured the ones that you had and squeezed the simps, as Jireh also suggested. The last proof still take ~2-3 secs, but the file compiles faster than before:

import ring_theory.tensor_product
import tactic

open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial

universe u
variables (K : Type u) [comm_semiring K]

@[simp] lemma assoc_symm_tmul {R : Type u} [comm_semiring R] {A : Type u} [semiring A] [algebra R A] {B : Type u} [semiring B] [algebra R B] {C : Type u} [semiring C] [algebra R C] (a : A) (b : B) (c : C) :
(algebra.tensor_product.assoc R A B C).symm (a ⊗ₜ[R] (b ⊗ₜ[R] c)) = a ⊗ₜ[R] b ⊗ₜ[R] c :=
begin
  apply_fun (algebra.tensor_product.assoc R A B C),
  rw [assoc_tmul, alg_equiv.apply_symm_apply],
  exact (embedding_like.comp_injective _ _).mpr (λ a b h, h),
end

-- noncomputable def counit : K[X] →ₐ[K] K := polynomial.aeval 0

noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := aeval ((X ⊗ₜ 1) + (1 ⊗ₜ X))

@[simp] lemma comul_1 : comul K (1 : K[X]) = (1 ⊗ₜ 1 : K[X] ⊗[K] K[X]) :=
begin
  rw map_one, -- ⊢ 1 = 1 ⊗ₜ[K] 1
  refl,
end

@[simp] lemma comul_X : comul K X = X ⊗ₜ 1 + 1 ⊗ₜ X :=
by rw [comul, aeval_X]

noncomputable def map1 : K[X] →ₐ[K] K[X] ⊗ K[X] ⊗ K[X] := (algebra.tensor_product.assoc K K[X] K[X] K[X]).symm.to_alg_hom.comp ((map (alg_hom.id K K[X]) (comul K)).comp (comul K))

noncomputable def map2 : (K[X] →ₐ[K] K[X] ⊗[K] K[X] ⊗[K] K[X] ) :=  (map (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X]) (alg_hom.id K K[X])).comp (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X])
. -- this tells Lean not to recompile definitions


lemma coassoc : map1 K = map2 K :=
begin
  ext,
  simp only [map1, map2, alg_equiv.to_alg_hom_eq_coe, alg_hom.coe_comp, alg_equiv.coe_alg_hom,
    function.comp_app, comul_X, map_tmul, alg_hom.coe_id, id.def, comul_1,
    tensor_product.tmul_add, add_assoc, assoc_symm_tmul, tensor_product.add_tmul, _root_.map_add],
end

[Damiano Testa]

Note that, placing set_option profiler true somewhere in your file gives you information about all the subsequent compilation times.

[Vasily Ilin]

I am using set_option profiler true as suggested and getting weird results. I have two lemmas that are exactly the same, with the same exact proof except that I give one a little more information. And the one I give more information takes 16 times longer! See the code below

import ring_theory.tensor_product
import tactic

open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial

universe u
variables (K : Type u) [comm_semiring K]

set_option profiler true

noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := aeval ((X ⊗ₜ 1) + (1 ⊗ₜ X))

@[simp] lemma comul_1 : comul K (1 : K[X]) = (1 ⊗ₜ 1 : K[X] ⊗[K] K[X]) := -- elaboration of comul_1 took 4.18s
begin
  rw alg_hom.map_one (comul K), -- ⊢ 1 = 1 ⊗ₜ[K] 1
  refl,
end

@[simp] lemma comul_1' : comul K (1 : K[X]) = (1 ⊗ₜ 1 : K[X] ⊗[K] K[X]) := -- elaboration of comul_1' took 189ms
begin
  rw alg_hom.map_one,
  refl,
end

[Vasily Ilin]

Also, doing something as simple as the following takes 3 seconds! This seems way too long, especially with all the types annotated

import ring_theory.tensor_product
import tactic

open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial

universe u
variables (K : Type u) [comm_semiring K]

set_option profiler true

noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := aeval ((X ⊗ₜ 1) + (1 ⊗ₜ X))

noncomputable def map2 : (K[X] →ₐ[K] K[X] ⊗[K] K[X] ⊗[K] K[X] ) :=  (map (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X]) (alg_hom.id K K[X])).comp (comul K : K[X] →ₐ[K] K[X] ⊗[K] K[X]) -- elaboration of map2 took 2.98s!

[Vasily Ilin]

@Damiano Testa , your proofs compile much faster than mine. How did you know to change the things you changed to make it faster? For example, why is rw alg_hom.map_one faster than rw alg_hom.map_one (comul K)?

[Damiano Testa]

Honestly, I do not know. I think that hints are generally good, but sometimes they get Lean into trying to prove some defeq that you want, but it is able to find more quickly some other way.

I have observed similar patterns with localization, mv_polynomial, monoid_algebra. I suspect that the implementation has several layers of defeqs and lean can get confused.

[Damiano Testa]

Btw, on my computer (which is not particularly fast and is already over two years old), map2 elaborates in approximately .5s.

The slowness on your computer might be due to the fact that you have changed also some files imported by this PR and Lean has to struggle with some incomplete/missing oleans. Maybe...

[Eric Wieser]

I would guess that alg_hom.map_one (comul K) is slower than alg_hom.map_one because the first one:

• Works out all the types for comul
• Tries to match up all those types in the goal state
• Possibly has to unify defeq typeclass diamonds in doing so

while the second one:

• Tries to match any alg_hom in the goal, and deduces the type of comul from there

[Vasily Ilin]

Damiano Testa said:

Btw, on my computer (which is not particularly fast and is already over two years old), map2 elaborates in approximately .5s.

The slowness on your computer might be due to the fact that you have changed also some files imported by this PR and Lean has to struggle with some incomplete/missing oleans. Maybe...

Huh, this is much faster than on mine. How would I fix this issue with oleans you are referring to?

[Vasily Ilin]

I tried leanproject build but it did not improve the elaboration speed

[Damiano Testa]

If leanproject built successfully your repository, then this should have taken care of the oleans... I'm not sure what explains the difference in performance, then.

[Vasily Ilin]

I have this proof, which is conceptually very simple: I have proof coinv_left K that two algebra maps are equal, and I want to prove that two set maps that happen to be set_maps of the algebra morphisms are equal (coinv_left'). It seems like it should be quite easy, maybe even just a simp. But I wasn't able to refactor the proof below to something more elegant. Any suggestions?

lemma coinv_left' : (lmul' K) ∘ (map (coinv K) (alg_hom.id K K[X])) ∘ (comul K) = (algebra.of_id K K[X]) ∘ (counit K) :=
begin
  let f' := (lmul' K).comp ((map (coinv K) (alg_hom.id K K[X])).comp (comul K)),
  let g' := (algebra.of_id K K[X]).comp (counit K),
  have h1 : f' = g',
    exact coinv_left K,
  have h2 : f'.to_fun = (lmul' K) ∘ (map (coinv K) (alg_hom.id K K[X])) ∘ (comul K),
    simp only [alg_hom.to_fun_eq_coe, alg_hom.coe_comp],
  have h3 : g'.to_fun = (algebra.of_id K K[X]) ∘ (counit K),
    simp only [alg_hom.to_fun_eq_coe, alg_hom.coe_comp],
  rw [← h2, ← h3],
  simp only [h1],
end

[Vasily Ilin]

Here is the whole file:

import ring_theory.tensor_product
import tactic

open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial

variables (K : Type*) [comm_ring K]

@[simp] lemma assoc_symm_tmul {R : Type*} [comm_semiring R] {A : Type*} [semiring A] [algebra R A] {B : Type*} [semiring B] [algebra R B] {C : Type*} [semiring C] [algebra R C] (a : A) (b : B) (c : C) :
(algebra.tensor_product.assoc R A B C).symm (a ⊗ₜ[R] (b ⊗ₜ[R] c)) = a ⊗ₜ[R] b ⊗ₜ[R] c :=
begin
  apply_fun (algebra.tensor_product.assoc R A B C),
  rw [assoc_tmul, alg_equiv.apply_symm_apply],
  exact (algebra.tensor_product.assoc R A B C).injective,
end

noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := aeval ((X ⊗ₜ 1) + (1 ⊗ₜ X))

@[simp] lemma comul_1 : comul K (1 : K[X]) = (1 ⊗ₜ 1 : K[X] ⊗[K] K[X]) :=
begin
  rw alg_hom.map_one, -- ⊢ 1 = 1 ⊗ₜ[K] 1
  refl,
end

@[simp] lemma comul_X : comul K X = X ⊗ₜ 1 + 1 ⊗ₜ X :=
begin
  unfold comul,
  rw aeval_X,
end

noncomputable def counit : K[X] →ₐ[K] K := aeval 0

@[simp] lemma counit_X : counit K X = 0 :=
begin
  unfold counit,
  simp only [coe_aeval_eq_eval, eval_X],
end

.

noncomputable def coinv : K[X] →ₐ[K] K[X] := aeval (-X)

@[simp] lemma coinv_X : coinv K X = -X :=
begin
  unfold coinv,
  rw aeval_X,
end

lemma coinv_left : (lmul' K).comp ((map (coinv K) (alg_hom.id K K[X])).comp (comul K) )= (algebra.of_id K K[X]).comp (counit K) :=
begin
  ext,
  simp only [alg_hom.coe_comp, function.comp_app, comul_X, _root_.map_add, map_tmul, coinv_X, alg_hom.coe_id, id.def, _root_.map_one, lmul'_apply_tmul, _root_.mul_one, _root_.one_mul, add_left_neg, counit_X, _root_.map_zero],
end
.

lemma coinv_left' : (lmul' K) ∘ (map (coinv K) (alg_hom.id K K[X])) ∘ (comul K) = (algebra.of_id K K[X]) ∘ (counit K) :=
begin
  let f' := (lmul' K).comp ((map (coinv K) (alg_hom.id K K[X])).comp (comul K)),
  let g' := (algebra.of_id K K[X]).comp (counit K),
  have h1 : f' = g',
    exact coinv_left K,
  have h2 : f'.to_fun = (lmul' K) ∘ (map (coinv K) (alg_hom.id K K[X])) ∘ (comul K),
    simp only [alg_hom.to_fun_eq_coe, alg_hom.coe_comp],
  have h3 : g'.to_fun = (algebra.of_id K K[X]) ∘ (counit K),
    simp only [alg_hom.to_fun_eq_coe, alg_hom.coe_comp],
  rw [← h2, ← h3],
  simp only [h1],
end

[Damiano Testa]

Does beginning with ext or funext work better?

[Vasily Ilin]

Damiano Testa said:

Does beginning with ext or funext work better?

I think no, because it just gives me an arbitrary element x. I think I instead want to use the fact that the algebra maps are equal to imply that their set maps are equal. I came up with the following still-not-elegant proof:

lemma coinv_left' : (lmul' K) ∘ (map (coinv K) (alg_hom.id K K[X])) ∘ (comul K) = (algebra.of_id K K[X]) ∘ (counit K) :=
  calc (lmul' K) ∘ (map (coinv K) (alg_hom.id K K[X])) ∘ (comul K)
        = ((lmul' K).comp ((map (coinv K) (alg_hom.id K K[X])).comp (comul K))).to_fun : by simp only [alg_hom.to_fun_eq_coe, alg_hom.coe_comp]
    ... = ((algebra.of_id K K[X]).comp (counit K)).to_fun : by simp only [coinv_left]
    ... = (algebra.of_id K K[X]) ∘ (counit K) : by simp only [alg_hom.to_fun_eq_coe, alg_hom.coe_comp]

[Vasily Ilin]

Since I only use simps in the calc block, I would expect this to work but it does not:

lemma coinv_left' : (lmul' K) ∘ (map (coinv K) (alg_hom.id K K[X])) ∘ (comul K) = (algebra.of_id K K[X]) ∘ (counit K) := by simp only [coinv_left, alg_hom.to_fun_eq_coe, alg_hom.coe_comp]

[Damiano Testa]

I am not sure if others agree, but I find it easier to work with "applied" functions, rather than non-applied ones, in Lean.

That was the reason for suggesting funext. If it does not work, maybe this just means that this is the one time developing the API that you have to do something awkward... :shrug:

[Vasily Ilin]

I decided to change the definition of my class to require equality of algebra maps as opposed to set maps (even though mathematically it's equivalent). I had not realized that it is easier to prove equality of algebra maps than set maps...

[Vasily Ilin]

What should I do if simp works but squeeze_simp times out? I don't want to just keep simp there since it will always take a long time to compile. Instead I want to switch it to simp only [...].

[Damiano Testa]

I sometimes save the file with the squeeze_simp in, and the lean --make <path_to_file>. This has a longer timeout threshold and will print the output.

[Damiano Testa]

Also, if you can guess what simp will do first, you can try simp only [your guesses], squeeze_simp.

[Vasily Ilin]

What if my guesses include like 20 things and simp only [my guesses] solves it? How do I boil it down?

[Damiano Testa]

If you squeeze the simp only, as in squeeze_simp only [guesses] also times out?

[Damiano Testa]

(Anyways, if yes, I would go with the lean --make step)

[Damiano Testa]

you can also mess with the timeout threshold on VSCode, but I usually prefer not to, since I want things to work quickly when I am proving stuff.

[Damiano Testa]

You can always put a sorry before the simp, if you know that simp will close the goal and leave it there while you develop the rest of the proof/file.

[Vasily Ilin]

Damiano Testa said:

If you squeeze the simp only, as in squeeze_simp only [guesses] also times out?

yea

[Vasily Ilin]

I am also getting a timeout on something pretty unexpected. I include the full file below but only the last two instances and the lemma coassoc are important. My instance times out when I include coassoc K in it and does not time out otherwise. Does it mean I need to make coassoc run faster? If so how can I do it?

import ring_theory.tensor_product
import tactic

open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial

variables (K : Type*) [comm_ring K]


variables (V : Type*) [comm_ring V] [algebra K V]
class hopf_algebra :=
(comul : V →ₐ[K] V ⊗[K] V)
(counit : V →ₐ[K] K)
(coinv : V →ₐ[K] V)
(coassoc : (algebra.tensor_product.assoc K V V V).to_alg_hom.comp ((map comul (alg_hom.id K V)).comp comul) = (map (alg_hom.id K V) comul).comp comul)
(counit_left : (algebra.tensor_product.lid K V).to_alg_hom.comp ((map counit (alg_hom.id K V)).comp comul) = (alg_hom.id K V))
(counit_right : (algebra.tensor_product.rid K V).to_alg_hom.comp ((map (alg_hom.id K V) counit).comp comul) = (alg_hom.id K V))
(coinv_right : (lmul' K).comp ((map (alg_hom.id K V) coinv).comp comul) = (algebra.of_id K V).comp counit)
(coinv_left : (lmul' K).comp ((map coinv (alg_hom.id K V)).comp comul) = (algebra.of_id K V).comp counit)

-- set_option profiler true -- time everything

noncomputable def comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := aeval ((X ⊗ₜ 1) + (1 ⊗ₜ X))

@[simp] lemma comul_1 : comul K (1 : K[X]) = (1 ⊗ₜ 1 : K[X] ⊗[K] K[X]) :=
begin
  rw alg_hom.map_one, -- ⊢ 1 = 1 ⊗ₜ[K] 1
  refl,
end

@[simp] lemma comul_X : comul K X = X ⊗ₜ 1 + 1 ⊗ₜ X :=
begin
  unfold comul,
  rw aeval_X,
end

lemma coassoc :  (algebra.tensor_product.assoc K K[X] K[X] K[X]).to_alg_hom.comp ((map (comul K) (alg_hom.id K K[X])).comp (comul K)) = (map (alg_hom.id K K[X]) (comul K)).comp (comul K) := -- TODO this still takes 10 seconds to elaborate
begin
  ext,
  simp only [algebra.tensor_product.assoc_tmul, alg_equiv.to_alg_hom_eq_coe, alg_hom.coe_comp, alg_equiv.coe_alg_hom, function.comp_app, comul_X, map_tmul, alg_hom.coe_id, id.def, comul_1, tensor_product.tmul_add, add_assoc, tensor_product.add_tmul, _root_.map_add],
end

noncomputable def counit : K[X] →ₐ[K] K := aeval 0

@[simp] lemma counit_X : counit K X = 0 :=
begin
  unfold counit,
  simp only [coe_aeval_eq_eval, eval_X],
end

.

lemma counit_left : (algebra.tensor_product.lid K K[X]).to_alg_hom.comp ((map (counit K) (alg_hom.id K K[X])).comp (comul K)) = (alg_hom.id K K[X]) :=
begin
  ext,
  simp only [counit, alg_equiv.to_alg_hom_eq_coe, alg_hom.coe_comp, alg_equiv.coe_alg_hom, function.comp_app, comul_X, _root_.map_add, map_tmul, coe_aeval_eq_eval, eval_X, tensor_product.zero_tmul, eval_one, zero_add, lid_tmul, one_smul],
end

lemma counit_right : (algebra.tensor_product.rid K K[X]).to_alg_hom.comp ((map (alg_hom.id K K[X]) (counit K)).comp (comul K)) = (alg_hom.id K K[X]) :=
begin
  ext,
  simp only [counit, alg_equiv.to_alg_hom_eq_coe, alg_hom.coe_comp, alg_equiv.coe_alg_hom, function.comp_app, comul_X, _root_.map_add, map_tmul, coe_aeval_eq_eval, eval_one, eval_X, tensor_product.tmul_zero, add_zero, rid_tmul, one_smul],
end

noncomputable def coinv : K[X] →ₐ[K] K[X] := aeval (-X)

@[simp] lemma coinv_X : coinv K X = -X :=
begin
  unfold coinv,
  rw aeval_X,
end

lemma coinv_right : (lmul' K).comp ((map (alg_hom.id K K[X]) (coinv K)).comp (comul K)) = (algebra.of_id K K[X]).comp (counit K) :=
begin
  ext,
  simp only [alg_hom.coe_comp, function.comp_app, comul_X, _root_.map_add, map_tmul, alg_hom.coe_id, id.def, _root_.map_one, coinv_X, lmul'_apply_tmul, _root_.mul_one, _root_.one_mul, add_right_neg, counit_X, _root_.map_zero],
end

lemma coinv_left : (lmul' K).comp ((map (coinv K) (alg_hom.id K K[X])).comp (comul K) )= (algebra.of_id K K[X]).comp (counit K) :=
begin
  ext,
  simp only [alg_hom.coe_comp, function.comp_app, comul_X, _root_.map_add, map_tmul, coinv_X, alg_hom.coe_id, id.def, _root_.map_one, lmul'_apply_tmul, _root_.mul_one, _root_.one_mul, add_left_neg, counit_X, _root_.map_zero],
end
.

set_option profiler true -- time everything

noncomputable instance polynomial_hopf : hopf_algebra K K[X] := { -- TIMEOUT
  comul := comul K,
  counit := counit K,
  coinv := coinv K,
  coassoc := coassoc K,
  counit_left := counit_left K,
  counit_right := counit_right K,
  coinv_right := coinv_right K,
  coinv_left := coinv_left K,
}

noncomputable instance polynomial_hopf : hopf_algebra K K[X] := { -- elaboration of polynomial_hopf took 10.4s
  comul := comul K,
  counit := counit K,
  coinv := coinv K,
  coassoc := sorry,
  counit_left := counit_left K,
  counit_right := counit_right K,
  coinv_right := coinv_right K,
  coinv_left := coinv_left K,
}

[Vasily Ilin]

I did lean --make src/polynomial_example.lean and it did not tell me that it timed out. So I guess it compiled it fine? Here is the output:

hopf_algebra :User\Github\Hopf\src\Hopf.lean: parsing at line 18←[2K
cumulative profiling times:
        compilation 0.0022ms
        decl post-processing 103ms
        elaboration 27.4s
        parsing 0.686ms
        type checking 100ms

[Damiano Testa]

If there were an error, you would see what the error was. Since you are only seeing the output of the profiler, you are good.

[Damiano Testa]

On my computer, your first noncomputable instance polynomial_hopf elaborates in 11s, while the one with the sorryed coassoc elaborates in 3.5s.

I do not know why your times are so much higher, though.

[Alex J. Best]

What sort of computer are you using Vasily? Is it a laptop? If it was a small laptop it's conceivable that it could take a few times longer than for others i guess.

[Vasily Ilin]

@Alex J. Best , it's a surface pro 6 with Intel i5 CPU.

[Alex J. Best]

Yeah that's a fairly low power device so I'm not surprised lean is taking a long time for you compared with others.