monoid_algebra.mul_apply

Stream: general

[Johan Commelin]

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]

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]

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

[Scott Morrison]

Nope! :-(

[Johan Commelin]

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

[Gabriel Ebner]

I'm starting to see a pattern...

local attribute [instance, priority 1001] classical.prop_decidable

[Johan Commelin]

Is this priority simply the better one for open_locale classical?

[Gabriel Ebner]

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]

Ouch

[Gabriel Ebner]

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]

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]

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]

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]

@Sebastien Gouezel This seems like a reasonable change.

[Sebastien Gouezel]

#2932