# Zulip Chat Archive

## 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?

#### Scott Morrison (Jun 03 2020 at 08:49):

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
```

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

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):

Last updated: May 10 2021 at 23:11 UTC