Simple proof takes 4 seconds

Stream: new members

[Vasily Ilin]

I have a simple proof that consists of ext, about 30 rewrites, and a refl, which takes 4 seconds to elaborate. This seems excessive. Any advice on making it faster? I am also getting a (deterministic) timeout on defining an instance that uses this proof. The timeout goes away if I do not use coassoc. This leads me to believe that something is wrong with coassoc. From the experimentation I've done, it seems that lean has a hard time dealing with tensor product of algebras, especially triple tensor product.

import ring_theory.tensor_product
import tactic

open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial

-- TODO variables {K : Type*} [comm_ring K]
variables (K : Type*) [comm_ring K]

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

-- TODO convert to dot notation
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) :=
begin
  ext,
  rw [alg_hom.coe_comp, alg_hom.coe_comp, alg_hom.coe_comp,
      function.comp_app, function.comp_app, function.comp_app,
      comul_X K,
      alg_hom.map_add, alg_hom.map_add, alg_hom.map_add,
      map_tmul, map_tmul, map_tmul, map_tmul,
      comul_X K, comul_1 K,
      alg_hom.coe_id, id.def, id.def,
      tensor_product.tmul_add, tensor_product.add_tmul,
      alg_hom.map_add,
      alg_equiv.to_alg_hom_eq_coe, alg_equiv.coe_alg_hom,
      algebra.tensor_product.assoc_tmul, algebra.tensor_product.assoc_tmul, algebra.tensor_product.assoc_tmul],
  refl,
end

[Vasily Ilin]

Posting the full file here. If you have any advice on style, a better way to structure anything, I would be grateful.

import Hopf
import ring_theory.tensor_product
import tactic

open_locale tensor_product
open_locale polynomial
open algebra.tensor_product
open polynomial

-- TODO variables {K : Type*} [comm_ring K]
variables (K : Type*) [comm_ring K]

set_option profiler true -- time everything

-- noncomputable def comm_ring.comul : K[X] →ₐ[K] K[X] ⊗[K] K[X] := aeval ((X ⊗ₜ 1) + (1 ⊗ₜ X))
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

-- TODO convert to dot notation
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) :=
begin
  ext,
  rw [alg_hom.coe_comp, alg_hom.coe_comp, alg_hom.coe_comp,
      function.comp_app, function.comp_app, function.comp_app,
      comul_X K,
      alg_hom.map_add, alg_hom.map_add, alg_hom.map_add,
      map_tmul, map_tmul, map_tmul, map_tmul,
      comul_X K, comul_1 K,
      alg_hom.coe_id, id.def, id.def,
      tensor_product.tmul_add, tensor_product.add_tmul,
      alg_hom.map_add,
      alg_equiv.to_alg_hom_eq_coe, alg_equiv.coe_alg_hom,
      algebra.tensor_product.assoc_tmul, algebra.tensor_product.assoc_tmul, algebra.tensor_product.assoc_tmul],
  refl,
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, alg_hom.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] := { -- No timeout!
  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,
}

[Johan Commelin]

I agree that it's strange that rw is taking such a long time.

[Johan Commelin]

The only unhelpful comment that I have for now, is that

  apply polynomial.alg_hom_ext,
  simp only [alg_hom.coe_comp, function.comp_app, map_add, map_tmul,
      comul_X K, comul_1 K, alg_hom.coe_id, id.def,
      tensor_product.tmul_add, tensor_product.add_tmul,
      alg_equiv.to_alg_hom_eq_coe, alg_equiv.coe_alg_hom,
      algebra.tensor_product.assoc_tmul, add_assoc],

is a shorter proof that takes twice as long...

[Johan Commelin]

Using show to blast through some defeqs even bumps the time to 10s on my box

  apply polynomial.alg_hom_ext,
  show (algebra.tensor_product.assoc K K[X] K[X] K[X]) ((map (comul K) (alg_hom.id K K[X])) ((comul K) X)) =
    (map (alg_hom.id K K[X]) (comul K)) ((comul K) X),
  simp only [alg_hom.coe_comp, function.comp_app, map_add, map_tmul,
      comul_X K, comul_1 K, alg_hom.coe_id, id.def,
      tensor_product.tmul_add, tensor_product.add_tmul,
      alg_equiv.to_alg_hom_eq_coe, alg_equiv.coe_alg_hom,
      algebra.tensor_product.assoc_tmul, add_assoc],

[Anne Baanen]

Looking at the types, this might just be because Lean can become very slow in typechecking when a type has a lot of dependencies: basically, since alg_hom, tensor_product and polynomial depend on the ring/module/etc structure of the arguments, and we have a type like alg_hom (tensor_product (tensor_product (polynomial _) _) _) _ _ the types grow at least with the fourth power (where quadratic is already big). And since algebra and module also depend on the ring structure it might even be more like to the seventh power.

[Anne Baanen]

I'll see if I can investigate in some more detail later today.

[Jake Levinson]

That's interesting. Is that something that could be made faster by some kind of additional tooling? Like adding extra functions / tactics to the algebra library to assist / direct this typechecking?

I have also found the mathlib algebra library to be quite heavy on my computer (though I haven't tried to use it too much yet).

[Anne Baanen]

It took a few days, but I finally have some time!

[Anne Baanen]

One interesting result is that replacing rw with simp only cuts the time in half, so perhaps a lot of time is spent in recomputing the motive (which parts of the expression stay fixed and which ones get rewritten) each time? In contrast, simp works by simplifying each subexpression fully before going to a larger expression so I assume it can reuse more if most subexpressions don't change.

[Anne Baanen]

Also, adding map_add to the simp only parameters makes elaboration time go from about 500ms to 3s on my machine. Very strange...

[Anne Baanen]

Both with rw and simp only with set_option trace.type_context.is_def_eq_detail true I see that unification goes up to 46 levels deep when trying to unify ⇑(?m_12.comp ?m_13) =?= ⇑((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))) which is pretty suggestive of the types being too complicated.

[Anne Baanen]

I can't find anywhere that a strategic local attribute [irreducible] will help, so basically the only useful suggestion I have at the moment to use simp only instead of rw.