Basic Question

Stream: new members

[De Paz]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Yury G. Kudryashov]

BTW, you can drop right_neutral and right_inverse from your axioms.

[De Paz]

Thank you, that helped me a lot!

[Kevin Buzzard]

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]

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]

You can delete [e : G] from the variables line. You've already declared e as a component of Group.

[Callum MacAskill]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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!