Zulip Chat Archive

Stream: new members

Topic: Basic Question


view this post on Zulip 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

view this post on Zulip 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 α)

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Dec 27 2019 at 17:41):

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

view this post on Zulip Kevin Buzzard (Dec 27 2019 at 17:41):

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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Dec 27 2019 at 18:15):

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

view this post on Zulip De Paz (Dec 27 2019 at 19:30):

Thank you, that helped me a lot!

view this post on Zulip 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.

view this post on Zulip 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,

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Patrick Massot (Feb 24 2020 at 18:22):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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