## Stream: general

### Topic: monoid_algebra.mul_apply

#### Johan Commelin (Jun 02 2020 at 18:05):

For some reason the statement of monoid_algebra.mul_apply (data/monoid_algebra, line 77) takes about 4 seconds to elaborate. (I commented out the proof.)
What's the reason for this?

#### Johan Commelin (Jun 02 2020 at 18:47):

monoid_algebra.lean:79:6: information
parsing took 0.508ms
monoid_algebra.lean:79:6: information
type checking of mul_apply took 0.503ms
monoid_algebra.lean:79:6: information
decl post-processing of mul_apply took 0.0135ms
monoid_algebra.lean:79:6: information
elaboration of mul_apply took 22.9ms


But it certainly takes a lot more than 1s when I watch the orange bars. So there is some secret time sink here.

#### Johan Commelin (Jun 03 2020 at 08:49):

@Scott Morrison Any idea what's going on here?

Nope! :-(

#### Johan Commelin (Jun 03 2020 at 08:49):

Was it snappy when you wrote it? If so, lean got worse at this part of the game...

#### Gabriel Ebner (Jun 03 2020 at 08:58):

I'm starting to see a pattern...

local attribute [instance, priority 1001] classical.prop_decidable


#### Johan Commelin (Jun 03 2020 at 09:00):

Is this priority simply the better one for open_locale classical?

#### Gabriel Ebner (Jun 03 2020 at 09:02):

The priority is dangerous in general: if 1 = 2 then 3 else 4 is elaborated to a definitionally not equal term if you change the priority:

noncomputable theory
def A := if 1 = 2 then 3 else 4
local attribute [instance, priority 1001] classical.prop_decidable
def B := if 1 = 2 then 3 else 4
example : A = B := rfl -- fails


Ouch

#### Gabriel Ebner (Jun 03 2020 at 09:04):

It might also be a good idea to add explicit decidable_eq assumptions to lemmas with if-then-else:

lemma mul_apply (f g : monoid_algebra k G) (x : G) [decidable_eq G] :
(f * g) x = (f.sum $λa₁ b₁, g.sum$ λa₂ b₂, if a₁ * a₂ = x then b₁ * b₂ else 0) :=
-- also fast, but proof's broken


#### Gabriel Ebner (Jun 03 2020 at 09:06):

I have no idea if you ever want to apply results about monoid algebras to things like natural numbers. But if you do, you'll quickly run into multiple different decidability instances and you won't be able to (directly) apply mul_apply to an if-then-else.

#### Sebastien Gouezel (Jun 03 2020 at 09:10):

Would it be reasonable if open_locale classical also set

local attribute [instance, priority 8] eq.decidable decidable_eq_of_decidable_le


? These seem to be the problematic instances that make Lean search through all the algebraic hierarchy whenever it wants to solve any decidability problem.

#### Johan Commelin (Jun 03 2020 at 09:12):

Gabriel Ebner said:

I have no idea if you ever want to apply results about monoid algebras to things like natural numbers. But if you do, you'll quickly run into multiple different decidability instances and you won't be able to (directly) apply mul_apply to an if-then-else.

I think that occasionally we will want to do that (or with int or zmod n). Same is true for polynomials.

#### Gabriel Ebner (Jun 03 2020 at 09:14):

@Sebastien Gouezel This seems like a reasonable change.

#### Sebastien Gouezel (Jun 03 2020 at 09:28):

#2932

Last updated: May 10 2021 at 23:11 UTC