Zulip Chat Archive

Stream: general

Topic: is_group_hom.mul


view this post on Zulip Kenny Lau (Apr 12 2018 at 05:54):

This is what is_group_hom.mul looked like on Apr 5:

namespace is_group_hom
variables {f : α → β} (H : is_group_hom f)
include H

theorem mul : ∀ a b : α, f (a * b) = f a * f b := H

Now, the function variable became explicit, which broke some of my files. Are changes like this just going to happen randomly without any notice?

view this post on Zulip Mario Carneiro (Apr 12 2018 at 05:55):

short answer: yes

view this post on Zulip Kenny Lau (Apr 12 2018 at 05:55):

wonderful

view this post on Zulip Mario Carneiro (Apr 12 2018 at 05:56):

mathlib is not stable any more than lean itself is, be prepared for this sort of thing

view this post on Zulip Kenny Lau (Apr 12 2018 at 05:56):

https://github.com/leanprover/mathlib/commit/fa86d349527766c2d0fc3173fcda302cdd5673f3#diff-52b9e281e7667f88f8203fb617843d93L488

view this post on Zulip Mario Carneiro (Apr 12 2018 at 05:56):

It's not clear what kind of notice would be appropriate here in any case

view this post on Zulip Kenny Lau (Apr 12 2018 at 05:57):

so if i werent clever enough to know exactly that my files broke because they made this variable explicit, I'm just going to have to sit down for an hour?

view this post on Zulip Kenny Lau (Apr 12 2018 at 05:58):

also, this change broke h.one where h is the proof that some function is a group homomorphism

view this post on Zulip Kenny Lau (Apr 12 2018 at 05:58):

now I have to do is_group_hom.one _ h

view this post on Zulip Mario Carneiro (Apr 12 2018 at 05:58):

If you update and your files break, double check what changed in the update, should give you a hint at what to do

view this post on Zulip Mario Carneiro (Apr 12 2018 at 05:58):

or ask here, of coure

view this post on Zulip Mario Carneiro (Apr 12 2018 at 05:58):

Now you do is_group_hom.one f I think

view this post on Zulip Kenny Lau (Apr 12 2018 at 06:00):

right

view this post on Zulip Kenny Lau (Apr 12 2018 at 06:00):

suddenly is_group_hom became a class

view this post on Zulip Kenny Lau (Apr 12 2018 at 06:00):

and guess what

view this post on Zulip Kenny Lau (Apr 12 2018 at 06:00):

https://github.com/leanprover/mathlib/commit/fa86d349527766c2d0fc3173fcda302cdd5673f3#diff-52b9e281e7667f88f8203fb617843d93L515

view this post on Zulip Mario Carneiro (Apr 12 2018 at 06:00):

Complain to @Scott Morrison and @Johannes Hölzl, I think this change is still in its probationary period

view this post on Zulip Kenny Lau (Apr 12 2018 at 06:01):

before: theorem inv (a : α) : (f a)⁻¹ = f a⁻¹
after: theorem inv (a : α) : f a⁻¹ = (f a)⁻¹

view this post on Zulip Kenny Lau (Apr 12 2018 at 06:01):

really

view this post on Zulip Mario Carneiro (Apr 12 2018 at 06:01):

I agree with that change, it makes more sense the other way around to match with one and mul

view this post on Zulip Mario Carneiro (Apr 12 2018 at 06:03):

but one thing I will not do is avoid small consistency changes because of a worry of breaking things. Once you start doing that, it will only become more crufty as time goes on


Last updated: May 11 2021 at 23:11 UTC