Zulip Chat Archive

Stream: new members

Topic: refactoring proofs


Vasily Ilin (Apr 21 2022 at 01:02):

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 (Apr 21 2022 at 01:09):

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 (Apr 21 2022 at 03:44):

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 (Apr 21 2022 at 03:45):

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

Vasily Ilin (Apr 21 2022 at 04:47):

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 (Apr 21 2022 at 05:04):

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 (Apr 21 2022 at 05:05):

@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 (Apr 21 2022 at 05:46):

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 (Apr 21 2022 at 07:45):

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 (Apr 21 2022 at 10:18):

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 (Apr 21 2022 at 16:05):

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 (Apr 21 2022 at 16:11):

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

Damiano Testa (Apr 21 2022 at 17:56):

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 (Apr 22 2022 at 00:00):

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 (Apr 22 2022 at 00:02):

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 (Apr 22 2022 at 00:08):

Does beginning with ext or funext work better?

Vasily Ilin (Apr 22 2022 at 00:14):

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 (Apr 22 2022 at 00:17):

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 (Apr 22 2022 at 00:20):

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 (Apr 22 2022 at 00:38):

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 (Apr 22 2022 at 00:41):

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 (Apr 22 2022 at 00:42):

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 (Apr 22 2022 at 00:43):

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

Vasily Ilin (Apr 22 2022 at 00:44):

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

Damiano Testa (Apr 22 2022 at 00:45):

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

Damiano Testa (Apr 22 2022 at 00:46):

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

Damiano Testa (Apr 22 2022 at 00:47):

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 (Apr 22 2022 at 00:48):

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 (Apr 22 2022 at 00:56):

Damiano Testa said:

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

yea

Vasily Ilin (Apr 22 2022 at 00:59):

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 (Apr 22 2022 at 01:03):

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 (Apr 22 2022 at 01:48):

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 (Apr 22 2022 at 01:49):

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 (Apr 22 2022 at 01:52):

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 (Apr 22 2022 at 20:29):

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

Alex J. Best (Apr 22 2022 at 21:19):

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


Last updated: Dec 20 2023 at 11:08 UTC