Zulip Chat Archive

Stream: general

Topic: monoid_algebra.mul_apply


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 03 2020 at 08:49):

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

view this post on Zulip Scott Morrison (Jun 03 2020 at 08:49):

Nope! :-(

view this post on Zulip 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...

view this post on Zulip Gabriel Ebner (Jun 03 2020 at 08:58):

I'm starting to see a pattern...

local attribute [instance, priority 1001] classical.prop_decidable

view this post on Zulip Johan Commelin (Jun 03 2020 at 09:00):

Is this priority simply the better one for open_locale classical?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 03 2020 at 09:03):

Ouch

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Jun 03 2020 at 09:14):

@Sebastien Gouezel This seems like a reasonable change.

view this post on Zulip Sebastien Gouezel (Jun 03 2020 at 09:28):

#2932


Last updated: May 10 2021 at 23:11 UTC