Zulip Chat Archive

Stream: maths

Topic: Writing readable uncluttered group theory


view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:39):

I noticed that the definition of a group in Lean was one more axiom than it could be

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:40):

you can prove mul_one from the other axioms

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:40):

This may well have been talked about before

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:40):

But I thought I'd write a blog post on this

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:40):

and I wanted to talk about the proof of mul_one (which goes via mul_left_cancel)

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:41):

for Lean-groups-without-mul_one

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:41):

But I could not make the arguments look beautiful

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:41):

This is kind of OK

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:42):

lemma gripe.mul_left_cancel {G : Type} [has_mul G] [has_one G] [has_inv G] [gripe G]
:  (a b c : G), a * b = a * c  b = c :=
begin
  intros a b c Habac,
  exact calc b = 1 * b : (one_mul b).symm
           ... = (a⁻¹ * a) * b : by rw [gripe.mul_left_inv a]
           ... = a⁻¹ * (a * b) : mul_assoc _ _ _
           ... = a⁻¹ * (a * c) : by rw Habac
-- ... = c : by simp only [mul_assoc,one_mul,mul_left_inv] -- fails
           ... = (a⁻¹ * a) * c : (gripe.mul_assoc _ _ _).symm
           ... = 1 * c : by rw [gripe.mul_left_inv a]
           ... = c : one_mul _
end

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:42):

although all this has_mul stuff is both really cluttering things up and not actually telling us the one useful thing about it, which is that it is a map alpha -> alpha -> alpha

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:43):

I made a type for that

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:43):

class gripe (G : Type) [has_mul G] [has_one G] [has_inv G] :=
(mul_assoc :  (a b c : G), a * b * c = a * (b * c))
(one_mul :  (a : G), 1 * a = a)
(mul_left_inv :  (a : G), a⁻¹ * a = 1)

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:44):

But got a bit sick about still having to say we have a has_mul. On the other hand I really want the notation.

view this post on Zulip Reid Barton (Apr 28 2018 at 05:45):

can you use extends instead of those extra parameters to the class? I've never used it myself but I see it in the algebraic classes

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:45):

Other complains about that calc proof is that I need to give too many hint, I seem to have to mention the type's name (gripe) randomly and I can only sometimes get away with _s, and why do I even have to put them at all?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:45):

I tried without the structure

view this post on Zulip Kenny Lau (Apr 28 2018 at 05:45):

This may well have been talked about before

https://gitter.im/leanprover_public/Lobby?at=59fd723d976e63937e268f50

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:46):

lemma mul_left_cancel' {G : Type} [has_mul G] [has_one G] [has_inv G]
(mul_assoc :  (a b c : G), a * b * c = a * (b * c))
(one_mul :  (a : G), 1 * a = a)
(mul_left_inv :  (a : G), a⁻¹ * a = 1)
:  (a b c : G), a * b = a * c  b = c :=
begin
  intros a b c Habac,
  exact calc b = 1 * b : (one_mul _).symm
           ... = (a⁻¹ * a) * b : by rw [mul_left_inv]
           ... = a⁻¹ * (a * b) : mul_assoc _ _ _ -- why not just mul_assoc?
           ... = a⁻¹ * (a * c) : by rw Habac
-- ... = c : by simp only [mul_assoc,one_mul,mul_left_inv] -- fails
           ... = (a⁻¹ * a) * c : (mul_assoc _ _ _).symm
           ... = 1 * c : by rw [mul_left_inv]
           ... = c : one_mul _ -- why the _ ?
end

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:48):

and that seemed to go better, but then

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:48):

theorem mul_one' {G : Type} [has_mul G] [has_one G] [has_inv G]
(mul_assoc :  (a b c : G), a * b * c = a * (b * c))
(one_mul :  (a : G), 1 * a = a)
(mul_left_inv :  (a : G), a⁻¹ * a = 1)
:  (a : G), a * 1 = a :=
begin
intro a,
 apply (mul_left_cancel' mul_assoc one_mul mul_left_inv a⁻¹ _ _), -- aargh
 rw [mul_assoc,mul_left_inv,one_mul],
end

view this post on Zulip Kenny Lau (Apr 28 2018 at 05:48):

@Kevin Buzzard edit > change title

view this post on Zulip Reid Barton (Apr 28 2018 at 05:48):

Oh, I guess you are complaining about has_mul being opaque to the reader wherever it appears, not that you had to write it twice?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:49):

I couldn't apply the theorem I proved without carrying around all the axioms.

view this post on Zulip Kenny Lau (Apr 28 2018 at 05:49):

wrong thread

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:49):

I want to write a blog post which looks good and works in Lean and proves clearly that one of the axioms of a group follows from the others

view this post on Zulip Kenny Lau (Apr 28 2018 at 05:49):

god

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:50):

but I really want the kids to understand that they can also do some of their group theory example sheets in Lean

view this post on Zulip Kenny Lau (Apr 28 2018 at 05:50):

whatever

view this post on Zulip Reid Barton (Apr 28 2018 at 05:50):

How do you feel about using variables instead?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:50):

can I move this?

view this post on Zulip Kenny Lau (Apr 28 2018 at 05:51):

@Scott Morrison sorry, had to move your messages as well; could you move your messages back to "notations in category theory"?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:51):

Sorry

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:52):

The stupidity of all the has_one has_mul stuff

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:52):

is that these typeclasses have notation attached to them

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:52):

and you want to use the notation

view this post on Zulip Reid Barton (Apr 28 2018 at 05:52):

variable {G : Type}
variable (mul : G  G  G)
variable (one : G)
variable (inv : G  G)

local notation a `*` b := mul a b
local notation 1 := one
local notation a `⁻¹` := inv a

variable (mul_assoc :  (a b c : G), a * b * c = a * (b * c))
variable (one_mul :  (a : G), 1 * a = a)
variable (mul_left_inv :  (a : G), a⁻¹ * a = 1)

lemma mul_left_cancel' :  (a b c : G), a * b = a * c  b = c :=

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 05:52):

Maybe instead of local notation I can use instances

view this post on Zulip Reid Barton (Apr 28 2018 at 06:00):

oh, I forgot variables don't get along well with tactics

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:36):

I am just going to bite the bullet and implement it in 5 different ways and see which one is best

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:37):

class has_group_notation (G : Type) extends has_mul G, has_one G, has_inv G

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:37):

Does that class exist @Mario Carneiro ?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:37):

It seems to come with free and painless type class inference

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:39):

I had not appreciated how that barrage of classes in core.lean was actually just a barrage of notation. Each typeclass corresponds to precisely one piece of notation. I had not realised this before!

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:40):

I don't really understand notation and don't use any in my schemes work.

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:40):

actually I think I suddenly understand it a whole lot better

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:41):

my class corresponds to a finite set of notations.

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:50):

class group' (G : Type) extends has_group_notation G :=
(mul_assoc :  (a b c : G), a * b * c = a * (b * c))
(one_mul :  (a : G), 1 * a = a)
(mul_left_inv :  (a : G), a⁻¹ * a = 1)

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:50):

@Reid Barton

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:50):

That's the way to get rid of all that continually carrying around [has_add]

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:51):

lemma group'.mul_left_cancel {G : Type} [group' G]
:  (a b c : G), a * b = a * c  b = c := sorry

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:51):

This thread is about making the proof that one of the axioms of a group as defined by Lean follows from all of the others

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:52):

look as nice and uncluttered as possible

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:53):

The strat is : first prove mul_left_cancel (without using mul_one of course), and then deduce mul_one. I know there are other strategies but that's the strategy I'd like to showcase in Lean

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:53):

so I can show the undergraduates one way of revising for their upcoming group theory exam

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:54):

I want to show them that using Lean to do abstract basic chase stuff around stuff in group theory is really easy in Lean

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:54):

I'll blog about it but I need to get it as nice looking as possible first

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 16:42):

https://gist.github.com/kbuzzard/2adf2b42a9ea23dabc2eb26a1a4b20fb

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 16:42):

My efforts using classes

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 16:43):

I had to keep writing the class name

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 16:43):

and the calc proof needed a lot of blanks

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 16:43):

How could this be improved?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 16:44):

I am going to try other ways of setting this up to see pros and cons

view this post on Zulip Kenny Lau (Apr 28 2018 at 16:44):

Change

(mul_assoc :  (a b c : G), a * b * c = a * (b * c))

to

(mul_assoc :  {a b c : G}, a * b * c = a * (b * c))

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:12):

Do you think that's right?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:12):

I changed it for the constants example

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:12):

and my tactic proof got worse

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:13):

if you change it then you don't need to put underscores

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:13):

I'll show you you're wrong

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:14):

https://github.com/kbuzzard/xena/blob/master/canonical_isomorphism/group_axioms_constants.lean

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:14):

But maybe you can fix it :-)

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:14):

there is a point in tactic mode where I needed underscores :-(

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:15):

where?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:15):

https://github.com/kbuzzard/xena/blob/master/canonical_isomorphism/group_axioms_class.lean

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:15):

not there

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:15):

so where am I wrong?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:15):

https://github.com/kbuzzard/xena/blob/48ce83d8bc9782a08ee852d126e784f696086846/canonical_isomorphism/group_axioms_constants.lean#L48

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:15):

there

view this post on Zulip Reid Barton (Apr 28 2018 at 17:16):

In the calc proof, if you just begin every justification with by rw, you can make it quite uniform (at least in this case)

  exact calc b = 1 * b         : by rw group'.one_mul
           ... = (a⁻¹ * a) * b : by rw group'.mul_left_inv
           ... = a⁻¹ * (a * b) : by rw group'.mul_assoc
           ... = a⁻¹ * (a * c) : by rw Habac
           ... = (a⁻¹ * a) * c : by rw group'.mul_assoc
           ... = 1 * c         : by rw group'.mul_left_inv
           ... = c             : by rw group'.one_mul

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:16):

Change

lemma mul_left_cancel :  {a b c : G}, a * b = a * c  b = c :=

to

lemma mul_left_cancel :  (a) {b c : G}, a * b = a * c  b = c :=

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:17):

do you feel that this change is actually justified rather than it being an attempt to sort out a problem?

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:17):

yes, because a could not be infered from the final type b = c

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:17):

yes

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:17):

I wondered if that was a reasonable justification for the change

view this post on Zulip Chris Hughes (Apr 28 2018 at 17:18):

It can be inferred from the hypothesis though.

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:18):

exactly

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:18):

well if you don't want to change it you can state the hypothesis explicitly using have

view this post on Zulip Reid Barton (Apr 28 2018 at 17:18):

... = (a⁻¹ * a) * b : by rw [mul_left_inv] -- why does that line even work? I believe it should fail. Is it a bug?

I was puzzled by this too up until quite recently. The reason it works is that rw does not rewrite the left hand side to the right hand side as one might think. Rather, it rewrites the desired equality 1 * b = (a⁻¹ * a) * b to whatever it becomes after the rewrite, and that rewrite might occur on either side.

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:18):

so Kenny based on your logic what are the forms of the other axioms that I should be using?

view this post on Zulip Reid Barton (Apr 28 2018 at 17:19):

Then because the rewritten goal is of the form a = a, it gets solved by rfl automatically

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:19):

@Kevin Buzzard maybe don't make a explicit afterall, lol

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:19):

:-)

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:21):

I don't quite know what I am looking for here. I guess what is going on is that different conventions produce different results which may or may not have slight annoyances

view this post on Zulip Reid Barton (Apr 28 2018 at 17:21):

Also if you use by rw on every line of the calc proof, then it doesn't matter whether you make the arguments of the axioms explicit or not

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:24):

Kenny in none of the standard typeclasses do I see variables in axioms being introduced with {}. I am imagining there is a good reason for this

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:25):

Letting them all be {} announces that you're 100 percent convinced that unification will save you

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:25):

well they have interface like

class semigroup (α : Type u) extends has_mul α :=
(mul_assoc :  a b c : α, a * b * c = a * (b * c))

lemma mul_assoc [semigroup α] :  a b c : α, a * b * c = a * (b * c) :=
semigroup.mul_assoc

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:25):

but letting them all be () does not mean you're giving up home

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:25):

oh wait

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:25):

because other things might fill in the gaps later

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:25):

right, you still need _ for mul_assoc lol

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:26):

so maybe change back to () and use Reid's approach

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:26):

Sometimes I did

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:26):

sometimes I didn't

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:26):

Oh I make the interface!

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:27):

I'm saying, the interface in the library still uses explicit variables

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:28):

exact calc b = 1 * b : by rw group'.one_mul -- that "shouldn't work" either

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:28):

why not?

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:28):

the goal is b = 1 * b

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:29):

Oh I see

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:29):

of course

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:29):

Kenny do you understand why that bug is not a bug?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:30):

line 33

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:30):

Oh I now understand

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:30):

I should think of what the rw actually does

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:30):

not what I want it to do

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:32):

lemma mul_left_cancel :  {a b c : G}, a * b = a * c  b = c :=
begin
  intros a b c Habac,
  exact calc b = 1 * b         : by rw one_mul
           ... = (a⁻¹ * a) * b : by rw mul_left_inv
           ... = a⁻¹ * (a * b) : by rw mul_assoc
           ... = a⁻¹ * (a * c) : by rw Habac
           ... = (a⁻¹ * a) * c : by rw mul_assoc
           ... = 1 * c         : by rw mul_left_inv
           ... = c : one_mul
end

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:32):

Yes that's really nice

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:32):

That's just how a mathematician would explain it

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:33):

"apply this axiom"

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:33):

"I don't care which way"

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:33):

"the obvious way"

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:33):

I'm sure you can have fewer lines lol

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:33):

of course

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:34):

but this is the raw beauty which you see here

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:34):

and then your begin intros exact kind of defeat the purpose of entering tactic mode

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 17:34):

ha ha you are exactly right

view this post on Zulip Reid Barton (Apr 28 2018 at 17:35):

I wasn't sure whether to comment about the intros line, haha

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:35):

comment about them.

view this post on Zulip Kenny Lau (Apr 28 2018 at 17:40):

@Kevin Buzzard I just finished writing a file without ever entering tactic mode

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:47):

All the rewrites fail in the below

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:47):

class has_group_notation (G : Type) extends has_mul G, has_one G, has_inv G

structure group' (G : Type) extends has_group_notation G :=
(mul_assoc :  (a b c : G), a * b * c = a * (b * c))
(one_mul :  (a : G), 1 * a = a)
(mul_left_inv :  (a : G), a⁻¹ * a = 1)

variables {G : Type} (group'.G : group' G) [has_group_notation G]
-- variables (H : Type) [has_mul H] [has_one H] [has_inv H]

-- We prove left_mul_cancel for group'

lemma group'.mul_left_cancel :  (a b c : G), a * b = a * c  b = c :=
λ a b c Habac,
 calc b = 1 * b         : by rw one_mul
    ... = (a⁻¹ * a) * b : by rw mul_left_inv
    ... = a⁻¹ * (a * b) : by rw mul_assoc
    ... = a⁻¹ * (a * c) : by rw Habac
    ... = (a⁻¹ * a) * c : by rw mul_assoc
    ... = 1 * c         : by rw mul_left_inv
                ... = c : by rw one_mul

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:47):

I am using a structure

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:47):

I don't understand the error messages

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:47):

First is

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:47):

rewrite tactic failed, did not find instance of the pattern in the target expression
  1 * ?m_3
state:
G : Type,
_inst_1 : has_group_notation G,
a b c : G,
Habac : a * b = a * c
⊢ b = 1 * b

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:48):

I am unimpressed with Lean's instance-finding abilities here

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:48):

what am i missing?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:48):

I wondered how changing a class to astructure changed things

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:49):

I think all notation as a notational typeclass works great in these sorts of situations

view this post on Zulip Kenny Lau (Apr 28 2018 at 20:49):

Lean only finds classes, not structures

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:49):

it's clear what it's doing

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:49):

and it's doing nothing more

view this post on Zulip Kenny Lau (Apr 28 2018 at 20:49):

the structure isnt even in the hypotheses

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:50):

I don't understand

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:50):

I will take notation off

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:50):

and put pp.all on

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:50):

am I missing something simple?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:51):

kenny can you fix it?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:51):

that might help me understand

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:55):

Look at this beautiful proof

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:55):

lemma mul_left_cancel' {G : Type} [has_mul G] [has_one G] [has_inv G]
(mul_assoc :  (a b c : G), a * b * c = a * (b * c))
(one_mul :  (a : G), 1 * a = a)
(mul_left_inv :  (a : G), a⁻¹ * a = 1)
:  (a b c : G), a * b = a * c  b = c :=
λ a b c Habac,
 calc b = 1 * b         : by rw one_mul
    ... = (a⁻¹ * a) * b : by rw mul_left_inv
    ... = a⁻¹ * (a * b) : by rw mul_assoc
    ... = a⁻¹ * (a * c) : by rw Habac
    ... = (a⁻¹ * a) * c : by rw mul_assoc
    ... = 1 * c         : by rw mul_left_inv
    ... = c             : by rw one_mul

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:55):

Can you show me how to make a proof which is just as beautiful, but using a class or structure?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:57):

I am getting sick of carrying the axioms around with me

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:58):

I have packaged up all the notation in a typeclass

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:58):

but I want to package all the group axioms up as well

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:59):

The typeclass system is perfect for notation.

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 20:59):

There is very little risk of a diamond :-)

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 21:00):

I want to package everything away but keep the proof beautiful

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 21:00):

and once I have managed that, I think I am done.

view this post on Zulip Chris Hughes (Apr 28 2018 at 21:03):

Why aren't you just using the group typeclass?

view this post on Zulip Mario Carneiro (Apr 28 2018 at 21:21):

The has_group_notation class has been discussed in some of Jeremy's explorations, called group_struct, but it's not needed in mathlib as it is now

view this post on Zulip Mario Carneiro (Apr 28 2018 at 21:25):

The standard way to show that an axiom is redundant is to have an auxiliary constructor for group that doesn't have the redundant axioms

view this post on Zulip Chris Hughes (Apr 28 2018 at 21:32):

Is this better?

class has_group_notation (G : Type) extends has_mul G, has_one G, has_inv G

class group' (G : Type) extends has_group_notation G :=
(mul_assoc' :  (a b c : G), a * b * c = a * (b * c))
(one_mul' :  (a : G), 1 * a = a)
(mul_left_inv' :  (a : G), a⁻¹ * a = 1)

variables {G : Type} [group' G]
open group'
-- variables (H : Type) [has_mul H] [has_one H] [has_inv H]

-- We prove left_mul_cancel for group'

lemma group'.mul_left_cancel :  (a b c : G), a * b = a * c  b = c :=
λ a b c Habac,
 calc b = 1 * b         : by rw one_mul' b
    ... = (a⁻¹ * a) * b : by rw mul_left_inv'
    ... = a⁻¹ * (a * b) : by rw mul_assoc'
    ... = a⁻¹ * (a * c) : by rw Habac
    ... = (a⁻¹ * a) * c : by rw mul_assoc'
    ... = 1 * c         : by rw mul_left_inv'
                ... = c : by rw one_mul'

view this post on Zulip Chris Hughes (Apr 28 2018 at 21:33):

You had two has_group_notation instances, one from group' and another one

view this post on Zulip Kenny Lau (Apr 28 2018 at 21:33):

Just use a namespace and drop the fucking primes

view this post on Zulip Chris Hughes (Apr 28 2018 at 21:33):

one mul is global

view this post on Zulip Kenny Lau (Apr 28 2018 at 21:34):

protected

view this post on Zulip Chris Hughes (Apr 28 2018 at 21:34):

but it doesn't know which one_mul I mean.

view this post on Zulip Mario Carneiro (Apr 28 2018 at 21:54):

def group.mk' {α : Type*} [semigroup α] [has_one α] [has_inv α]
  (one_mul : ∀ (a : α), 1 * a = a)
  (mul_left_inv : ∀ (a : α), a⁻¹ * a = 1) : group α :=
have ∀ a : α, a * a = a → a = 1, from λ a h,
  calc a = a⁻¹ * a * a : by simp [mul_left_inv, one_mul]
    ... = a⁻¹ * a : by rw [mul_assoc, h]
    ... = 1 : mul_left_inv _,
have ∀ a : α, a * a⁻¹ = 1, from
λ a, this _ $ calc
  a * a⁻¹ * (a * a⁻¹)
      = a * (a⁻¹ * a) * a⁻¹ : by simp [mul_assoc]
  ... = a * a⁻¹ : by rw mul_left_inv; simp [mul_assoc, one_mul],
{ one_mul := one_mul,
  mul_left_inv := mul_left_inv,
  mul_one := λ a, show a * 1 = a,
    by rw [← mul_left_inv a, ← mul_assoc, this, one_mul],
  ..‹semigroup α›, ..‹has_one α›, ..‹has_inv α› }

view this post on Zulip Scott Morrison (Apr 28 2018 at 22:54):

This is a common problem in making definitions --- do you go for maximal axioms (so that you don't need lots of lemmas later, and the big results follow easily from the definitions), or minimal axioms (so instances are easy to construct)? Often, the right solution in Lean is to go for maximal axioms with alternate constructors that require minimal axioms.

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:38):

The standard way to show that an axiom is redundant is to have an auxiliary constructor for group that doesn't have the redundant axioms

Yes but these are mathematicians with no functional programming background and I think they would prefer to see something which looks like an honest proof (never mention the axiom, then prove it) rather than wrapping anything in a complicated structure.

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:41):

Mario your proof is in some sense canonical, but I prefer mine for pedagogical reasons.

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 02:27):

Just use a namespace and drop the fucking primes

Kenny can you do it? Namespaces seem to lead to overloading anyway.

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 02:28):

I am reluctant to prime the axioms

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 02:28):

but maybe I have to

view this post on Zulip Mario Carneiro (Apr 29 2018 at 03:18):

something which looks like an honest proof (never mention the axiom, then prove it)

I'm confused. Isn't that pretty much exactly what my proof does? I start with a semigroup with a one and inv, and the left_inv and one_mul axioms, and derive mul_one. There is no funny business at all, or complicated structures, it's literally just proving one statement from another, and then wrapping it up in a group. The proof part could also be factored out like so:

section
parameters {α : Type*} [semigroup α] [has_one α] [has_inv α]
  (one_mul : ∀ (a : α), 1 * a = a)
  (mul_left_inv : ∀ (a : α), a⁻¹ * a = 1)
include one_mul mul_left_inv

theorem group.mk'_aux1 {a : α} (h : a * a = a) : a = 1 :=
calc a = a⁻¹ * a * a : by simp [mul_left_inv, one_mul]
   ... = a⁻¹ * a : by rw [mul_assoc, h]
   ... = 1 : mul_left_inv _

theorem group.mk'_aux2 (a : α) : a * a⁻¹ = 1 :=
group.mk'_aux1 $ calc
  a * a⁻¹ * (a * a⁻¹)
      = a * (a⁻¹ * a) * a⁻¹ : by simp [mul_assoc]
  ... = a * a⁻¹ : by rw mul_left_inv; simp [mul_assoc, one_mul]

theorem group.mk'_aux3 (a : α) : a * 1 = a :=
by rw [← mul_left_inv a, ← mul_assoc, group.mk'_aux2, one_mul]

def group.mk' : group α :=
{ one_mul := one_mul,
  mul_left_inv := mul_left_inv,
  mul_one := group.mk'_aux3,
  ..‹semigroup α›, ..‹has_one α›, ..‹has_inv α› }

end

view this post on Zulip Mario Carneiro (Apr 29 2018 at 03:45):

Another way to present a proof like this is via an auxiliary class like your gripe, like so:

class gripe (α : Type*) extends semigroup α, has_one α, has_inv α :=
(one_mul : ∀ (a : α), 1 * a = a)
(mul_left_inv : ∀ (a : α), a⁻¹ * a = 1)

namespace gripe
variables {α : Type*} [gripe α]

theorem eq_one_of_idem {a : α} (h : a * a = a) : a = 1 :=
calc a = a⁻¹ * a * a : by simp [mul_left_inv, one_mul]
   ... = a⁻¹ * a : by rw [mul_assoc, h]
   ... = 1 : mul_left_inv _

theorem mul_right_inv (a : α) : a * a⁻¹ = 1 :=
eq_one_of_idem $ calc
  a * a⁻¹ * (a * a⁻¹)
      = a * (a⁻¹ * a) * a⁻¹ : by simp [mul_assoc]
  ... = a * a⁻¹ : by rw mul_left_inv; simp [mul_assoc, one_mul]

theorem mul_one (a : α) : a * 1 = a :=
by rw [← mul_left_inv a, ← mul_assoc, mul_right_inv, one_mul]

instance (α) [gripe α] : group α :=
{ one_mul := one_mul,
  mul_left_inv := mul_left_inv,
  mul_one := mul_one,
  ..gripe.to_semigroup α,
  ..gripe.to_has_one α,
  ..gripe.to_has_inv α }

end gripe

view this post on Zulip Kevin Buzzard (May 02 2018 at 17:47):

Here's how it ended up. https://xenaproject.wordpress.com/2018/04/30/group-theory-revision/


Last updated: May 09 2021 at 11:09 UTC