## Stream: maths

### Topic: Writing readable uncluttered group theory

#### 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

#### Kevin Buzzard (Apr 28 2018 at 05:40):

you can prove mul_one from the other axioms

#### Kevin Buzzard (Apr 28 2018 at 05:40):

This may well have been talked about before

#### Kevin Buzzard (Apr 28 2018 at 05:40):

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

#### 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)

#### Kevin Buzzard (Apr 28 2018 at 05:41):

for Lean-groups-without-mul_one

#### Kevin Buzzard (Apr 28 2018 at 05:41):

But I could not make the arguments look beautiful

#### Kevin Buzzard (Apr 28 2018 at 05:41):

This is kind of OK

#### 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


#### 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

#### Kevin Buzzard (Apr 28 2018 at 05:43):

I made a type for that

#### 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)


#### 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.

#### 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

#### 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?

#### Kevin Buzzard (Apr 28 2018 at 05:45):

I tried without the structure

#### Kenny Lau (Apr 28 2018 at 05:45):

This may well have been talked about before

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

#### 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


#### Kevin Buzzard (Apr 28 2018 at 05:48):

and that seemed to go better, but then

#### 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


#### Kenny Lau (Apr 28 2018 at 05:48):

@Kevin Buzzard edit > change title

#### 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?

#### Kevin Buzzard (Apr 28 2018 at 05:49):

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

#### 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

god

#### 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

whatever

#### Reid Barton (Apr 28 2018 at 05:50):

How do you feel about using variables instead?

can I move this?

#### 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"?

Sorry

#### Kevin Buzzard (Apr 28 2018 at 05:52):

The stupidity of all the has_one has_mul stuff

#### Kevin Buzzard (Apr 28 2018 at 05:52):

is that these typeclasses have notation attached to them

#### Kevin Buzzard (Apr 28 2018 at 05:52):

and you want to use the notation

#### 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 :=


#### Kevin Buzzard (Apr 28 2018 at 05:52):

Maybe instead of local notation I can use instances

#### Reid Barton (Apr 28 2018 at 06:00):

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

#### 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

#### Kevin Buzzard (Apr 28 2018 at 15:37):

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

#### Kevin Buzzard (Apr 28 2018 at 15:37):

Does that class exist @Mario Carneiro ?

#### Kevin Buzzard (Apr 28 2018 at 15:37):

It seems to come with free and painless type class inference

#### 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!

#### Kevin Buzzard (Apr 28 2018 at 15:40):

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

#### Kevin Buzzard (Apr 28 2018 at 15:40):

actually I think I suddenly understand it a whole lot better

#### Kevin Buzzard (Apr 28 2018 at 15:41):

my class corresponds to a finite set of notations.

#### 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)


@Reid Barton

#### Kevin Buzzard (Apr 28 2018 at 15:50):

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

#### 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


#### 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

#### Kevin Buzzard (Apr 28 2018 at 15:52):

look as nice and uncluttered as possible

#### 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

#### Kevin Buzzard (Apr 28 2018 at 15:53):

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

#### 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

#### 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

#### Kevin Buzzard (Apr 28 2018 at 16:42):

My efforts using classes

#### Kevin Buzzard (Apr 28 2018 at 16:43):

I had to keep writing the class name

#### Kevin Buzzard (Apr 28 2018 at 16:43):

and the calc proof needed a lot of blanks

#### Kevin Buzzard (Apr 28 2018 at 16:43):

How could this be improved?

#### Kevin Buzzard (Apr 28 2018 at 16:44):

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

#### 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))


#### Kevin Buzzard (Apr 28 2018 at 17:12):

Do you think that's right?

#### Kevin Buzzard (Apr 28 2018 at 17:12):

I changed it for the constants example

#### Kevin Buzzard (Apr 28 2018 at 17:12):

and my tactic proof got worse

#### Kenny Lau (Apr 28 2018 at 17:13):

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

#### Kevin Buzzard (Apr 28 2018 at 17:13):

I'll show you you're wrong

#### Kevin Buzzard (Apr 28 2018 at 17:14):

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

#### Kevin Buzzard (Apr 28 2018 at 17:14):

But maybe you can fix it :-)

#### Kevin Buzzard (Apr 28 2018 at 17:14):

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

where?

#### Kevin Buzzard (Apr 28 2018 at 17:15):

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

not there

#### Kenny Lau (Apr 28 2018 at 17:15):

so where am I wrong?

#### Kevin Buzzard (Apr 28 2018 at 17:15):

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

there

#### 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


#### 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 :=


#### 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?

#### Kenny Lau (Apr 28 2018 at 17:17):

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

yes

#### Kevin Buzzard (Apr 28 2018 at 17:17):

I wondered if that was a reasonable justification for the change

#### Chris Hughes (Apr 28 2018 at 17:18):

It can be inferred from the hypothesis though.

exactly

#### 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

#### 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.

#### 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?

#### 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

#### Kenny Lau (Apr 28 2018 at 17:19):

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

:-)

#### 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

#### 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

#### 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

#### Kevin Buzzard (Apr 28 2018 at 17:25):

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

#### 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


#### Kevin Buzzard (Apr 28 2018 at 17:25):

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

oh wait

#### Kevin Buzzard (Apr 28 2018 at 17:25):

because other things might fill in the gaps later

#### Kenny Lau (Apr 28 2018 at 17:25):

right, you still need _ for mul_assoc lol

#### Kenny Lau (Apr 28 2018 at 17:26):

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

Sometimes I did

#### Kevin Buzzard (Apr 28 2018 at 17:26):

sometimes I didn't

#### Kevin Buzzard (Apr 28 2018 at 17:26):

Oh I make the interface!

#### Kenny Lau (Apr 28 2018 at 17:27):

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

#### Kevin Buzzard (Apr 28 2018 at 17:28):

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

why not?

#### Kenny Lau (Apr 28 2018 at 17:28):

the goal is b = 1 * b

Oh I see

of course

#### Kevin Buzzard (Apr 28 2018 at 17:29):

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

line 33

#### Kevin Buzzard (Apr 28 2018 at 17:30):

Oh I now understand

#### Kevin Buzzard (Apr 28 2018 at 17:30):

I should think of what the rw actually does

#### Kevin Buzzard (Apr 28 2018 at 17:30):

not what I want it to do

#### 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


#### Kevin Buzzard (Apr 28 2018 at 17:32):

Yes that's really nice

#### Kevin Buzzard (Apr 28 2018 at 17:32):

That's just how a mathematician would explain it

#### Kevin Buzzard (Apr 28 2018 at 17:33):

"apply this axiom"

#### Kevin Buzzard (Apr 28 2018 at 17:33):

"I don't care which way"

#### Kevin Buzzard (Apr 28 2018 at 17:33):

"the obvious way"

#### Kenny Lau (Apr 28 2018 at 17:33):

I'm sure you can have fewer lines lol

of course

#### Kevin Buzzard (Apr 28 2018 at 17:34):

but this is the raw beauty which you see here

#### Kenny Lau (Apr 28 2018 at 17:34):

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

#### Kevin Buzzard (Apr 28 2018 at 17:34):

ha ha you are exactly right

#### Reid Barton (Apr 28 2018 at 17:35):

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

#### Kenny Lau (Apr 28 2018 at 17:40):

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

#### Kevin Buzzard (Apr 28 2018 at 20:47):

All the rewrites fail in the below

#### 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


#### Kevin Buzzard (Apr 28 2018 at 20:47):

I am using a structure

#### Kevin Buzzard (Apr 28 2018 at 20:47):

I don't understand the error messages

First is

#### 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


#### Kevin Buzzard (Apr 28 2018 at 20:48):

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

#### Kevin Buzzard (Apr 28 2018 at 20:48):

what am i missing?

#### Kevin Buzzard (Apr 28 2018 at 20:48):

I wondered how changing a class to astructure changed things

#### Kevin Buzzard (Apr 28 2018 at 20:49):

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

#### Kenny Lau (Apr 28 2018 at 20:49):

Lean only finds classes, not structures

#### Kevin Buzzard (Apr 28 2018 at 20:49):

it's clear what it's doing

#### Kevin Buzzard (Apr 28 2018 at 20:49):

and it's doing nothing more

#### Kenny Lau (Apr 28 2018 at 20:49):

the structure isnt even in the hypotheses

#### Kevin Buzzard (Apr 28 2018 at 20:50):

I don't understand

#### Kevin Buzzard (Apr 28 2018 at 20:50):

I will take notation off

#### Kevin Buzzard (Apr 28 2018 at 20:50):

and put pp.all on

#### Kevin Buzzard (Apr 28 2018 at 20:50):

am I missing something simple?

#### Kevin Buzzard (Apr 28 2018 at 20:51):

kenny can you fix it?

#### Kevin Buzzard (Apr 28 2018 at 20:51):

that might help me understand

#### Kevin Buzzard (Apr 28 2018 at 20:55):

Look at this beautiful proof

#### 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


#### 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?

#### Kevin Buzzard (Apr 28 2018 at 20:57):

I am getting sick of carrying the axioms around with me

#### Kevin Buzzard (Apr 28 2018 at 20:58):

I have packaged up all the notation in a typeclass

#### Kevin Buzzard (Apr 28 2018 at 20:58):

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

#### Kevin Buzzard (Apr 28 2018 at 20:59):

The typeclass system is perfect for notation.

#### Kevin Buzzard (Apr 28 2018 at 20:59):

There is very little risk of a diamond :-)

#### Kevin Buzzard (Apr 28 2018 at 21:00):

I want to package everything away but keep the proof beautiful

#### Kevin Buzzard (Apr 28 2018 at 21:00):

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

#### Chris Hughes (Apr 28 2018 at 21:03):

Why aren't you just using the group typeclass?

#### 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

#### 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

#### 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'


#### Chris Hughes (Apr 28 2018 at 21:33):

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

#### Kenny Lau (Apr 28 2018 at 21:33):

Just use a namespace and drop the fucking primes

#### Chris Hughes (Apr 28 2018 at 21:33):

one mul is global

protected

#### Chris Hughes (Apr 28 2018 at 21:34):

but it doesn't know which one_mul I mean.

#### 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 α› }  #### 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. #### 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. #### Kevin Buzzard (Apr 29 2018 at 00:41): Mario your proof is in some sense canonical, but I prefer mine for pedagogical reasons. #### 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. #### Kevin Buzzard (Apr 29 2018 at 02:28): I am reluctant to prime the axioms #### Kevin Buzzard (Apr 29 2018 at 02:28): but maybe I have to #### 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


#### 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


#### 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