Zulip Chat Archive

Stream: new members

Topic: problem trying to prove instance comm_group


view this post on Zulip Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:20):

I am a total Lean newbie, so maybe I am trying something too advanced, but anyway: I was trying to prove that a normal subgroup of a group is a commutative group. I am running into some problem with coercions (or my understanding of type classes is wrong, I can't quite tell). What I tried is this:

import group_theory.subgroup

variables (G : Type*) [group G]

instance normal_subgroup_is_comm_group (s: set G) [normal_subgroup s] : comm_group s := {
    mul_comm := begin
        -- here * is not expanded
        rintros a, ha b, hb,
        simp, -- can't simplify the definition of *, for some reason?!
        sorry,
    end,
    mul_assoc := begin -- part of ..subtype.group, but I include it to show the difference to mul_comm
        -- here the definition of * from subtype.monoid (via subtype.group) is used
        rintros a, ha b, hb c, hc,
        simp, -- simplifies the definition of * just fine
        exact mul_assoc a b c,
    end,
    ..subtype.group
}

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 18:23):

One issue here is the fact that it's not true that an arbitrary normal subgroup of an arbitrary group is always commutative.

view this post on Zulip Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:23):

that would be a problem ;-)

view this post on Zulip Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:24):

but I still don't understand why the first simp doesn't manage to expand *

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 18:24):

In fact I think this might be the only issue, you seem to have proved associativity just fine

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 18:25):

I get unknown identifier 'normal_subgroup'. I'm using today's mathlib. -- Aah, I need to add import deprecated.subgroup

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 18:28):

So your goal is ⊢ ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨b, hb⟩ * ⟨a, ha⟩ and simp doesn't do anything -- I don't understand the question. You want to change it to a * b = b * a? This works:

        rintros a, ha b, hb,
        change (a * b, _⟩ : s) = b * a, _⟩,
        simp,

view this post on Zulip Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:29):

I don't understand why the second simp does something, and the first doesn't

view this post on Zulip Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:36):

But anyway, change helped me already, thanks

view this post on Zulip Johan Commelin (Jun 12 2020 at 18:43):

@Carl Friedrich Bolz-Tereick Are you thinking of "a subgroup of a commutative group is always normal"?

view this post on Zulip Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:47):

no, I arrived at this mathematically wrong example above while trying to reduce more and more what I actually tried to prove, which is that the center of a division_ring is a comm_ring. with kevin's hint I now managed to do that. I don't completely understand how the change tactic he proposed works, though

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 18:50):

The second simp doesn't do anything useful. * is notation for has_mul.mul which simp has changed to the definitionally equal group.mul.

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 18:51):

If the goal is X then change Y will successfully change the goal to Y if and only if X and Y are definitionally equal.

view this post on Zulip Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:58):

thanks

view this post on Zulip Bryan Gin-ge Chen (Jun 12 2020 at 18:59):

Here's the tactic doc: tactic#change

view this post on Zulip Carl Friedrich Bolz-Tereick (Jun 13 2020 at 06:48):

and I managed to show that the center of a division_ring is a field, which is what I originally wanted to try :-). the proof is pretty hairy though, need to simplify it


Last updated: May 10 2021 at 19:16 UTC