# Zulip Chat Archive

## Stream: new members

### Topic: Basic Question

#### De Paz (Dec 27 2019 at 17:14):

Hello!

Undergraduate student from Germany here who is interested in Lean!

I read the tutorial about Propositions and I'm currently reading the Logic and Proof manual and want to try the following:

I want to proof that the identity element in a goup is unique by defining a group and using that definition. Here is my code:

universe u

variables α : Type u

class Group (α : Type u) :=

(operation : α × α → α)

(one : α )

( associativity : ∀ a b c: α, operation(a, operation(b,c) ) = operation( operation(a,b), c) )

( left_neutral: ∀ a : α, operation(a, one) = a )

( right_neutral : ∀ a : α, operation(one, a ) = a )

( left_inverse: ∀ a : α, ∃ l_inverse : α , operation(l_inverse, a) = one )

( right_inverse: ∀ a : α, ∃ r_inverse : α , operation(a, r_inverse) = one )

My problem is that I don't know how to use this defintion.

Can someone tell me where I can find an example related to my problem ?

I'm looking forward to learn more about Lean!

Thank you

#### Jesse Michael Han (Dec 27 2019 at 17:35):

i think you want a statement like this:

example {α : Type*} [G : Group α] {e : α} (H_left : ∀ a : α, Group.operation(a, e) = a) : e = (Group.one α)

#### Jesse Michael Han (Dec 27 2019 at 17:38):

(note: the proof of this can be one-lined with `by finish using Group.right_neutral e`

)

#### Kevin Buzzard (Dec 27 2019 at 17:41):

man that's too many axioms for a group ;-)

#### Kevin Buzzard (Dec 27 2019 at 17:41):

https://xenaproject.wordpress.com/2018/04/30/group-theory-revision/

#### Kevin Buzzard (Dec 27 2019 at 17:42):

Example of using groups in Lean: https://github.com/kbuzzard/xena/blob/master/blog/group_axioms_class.lean

#### Yury G. Kudryashov (Dec 27 2019 at 18:15):

BTW, you can drop `right_neutral`

and `right_inverse`

from your axioms.

#### De Paz (Dec 27 2019 at 19:30):

Thank you, that helped me a lot!

#### Kevin Buzzard (Dec 27 2019 at 22:52):

BTW, you can drop

`right_neutral`

and`right_inverse`

from your axioms.

You can drop e.g. `right_neutral`

and `left_inverse`

, but if you drop `right_neutral`

and `right_inverse`

then I think `operation(a,b):=a`

is a (non-group) model for the remaining axioms.

#### Callum MacAskill (Feb 24 2020 at 18:07):

I was wondering if I could get some help on a fairly basic question? I'm currently working on a project comparing Coq and Lean, and as part of it I'm coding basic group theory into both. I've adapted the code from Coq to Lean and it all seems fine, but breaks down when I start trying to prove further lemmas, I'm getting a "don't know how to synthesize placeholder" error. I know I'm missing something simple, could anyone point it out?

class Group (G : Type) := (Op: G → (G → G)) (Inv : G → G) (e : G) (Power : G → nat → G) (InvPower : G → nat → G) (RightId : ∀ x : G, Op e x = x) (Associativity: ∀ x y z:G, Op (Op x y) z = Op x (Op y z)) (LeftInverse : ∀ x : G, Op (Inv x) x = e) (LeftIdentity : ∀ x : G, Op e x = x) namespace Group variables {G : Type} [Group G] [e : G] theorem RightIdentity: ∀ (x : G), Op x e = x := begin intro x,

#### Rob Lewis (Feb 24 2020 at 18:11):

You can delete `[e : G]`

from the `variables`

line. You've already declared `e`

as a component of `Group`

.

#### Callum MacAskill (Feb 24 2020 at 18:20):

That was in my original code, however when I don't declare it I get the error message

group.lean:21:34: error type mismatch at application Op x e term e has type Π (G : Type) [c : Group G], G : Type 1 but is expected to have type G : Type

I'm assuming I've done something wrong when setting up the group axioms, but still can't see it?

#### Patrick Massot (Feb 24 2020 at 18:21):

Callum MacAskill said:

I was wondering if I could get some help on a fairly basic question?

Yes, this is the right place.

I'm currently working on a project comparing Coq and Lean, and as part of it I'm coding basic group theory into both. I've adapted the code from Coq to Lean and it all seems fine

This sounds like a very bad way of comparing Coq and Lean. Directly translating a Coq file into a Lean file will simply prove that Lean is not good at being Coq. The same would work in the opposite direction. You should try to do the same math in idiomatic Coq and then in idiomatic Lean. Your definition of `Group`

is nothing you would see in a Lean file

#### Patrick Massot (Feb 24 2020 at 18:22):

We would never write such a definition without inserting a notation for `Op`

right after `(Op: G → (G → G))`

(and we wouldn't put that many parentheses).

#### Patrick Massot (Feb 24 2020 at 18:22):

Dinner is calling, other people will probably rewrite your code.

#### Kevin Buzzard (Feb 24 2020 at 18:27):

Here's how I'd define groups from scratch in Lean: https://github.com/kbuzzard/group-theory-game/blob/master/src/group/definitions.lean . Check out the repo for the Lean idiomatic way to do things. Note: none of this `Op`

stuff -- we use the standard notation `*`

right from square 1.

#### Kevin Buzzard (Feb 24 2020 at 18:28):

Here are some examples of how to start setting up the theory, with comments: https://github.com/kbuzzard/group-theory-game/blob/master/src/group/theorems.lean

#### Callum MacAskill (Feb 24 2020 at 19:36):

Thank you both for the replies. I'll reread your code and start again from the top. I'd seen the link when searching earlier but avoided it at first as I was trying to use only definitions that I'd typed myself (as I'd had to do in Coq), but I'm definitely not treating the two distinctly enough. I'll try again, thank you!

Last updated: May 15 2021 at 22:14 UTC