Proving group theory exercises in lean

Stream: new members

[Alexander Belov]

I have picked up a set of group theory exercises recently and have solved a dozen of them. Now I would like to print my solution in lean. I know full well how to do 100% formal proofs on paper and had a little bit of experience with formalizing my proofs in Mizar and Lean but that was few years ago and let's say I know 0% about lean. My current goals are: introduce my own definition of a group G and definitions of neutral element e_G and inverse element inv(f). My approach on paper is: any ordered pair (X, circ) consisting of some set Xand a function circ : X to X -> such that the following properties hold: 1) forall f,g in X g circ f in X 2) forall f,g,h in X (h circ g) circ f = h circ (g circ f), 3) exists e in X (forall f in X f circ e = e circ f = f and forall f in X exists g in X g circ f = f circ g = e) is a group. After introducing my definition I would like to prove first property that forall G if G is a group then exists! e in X (forall f in X f circ e = e circ f = f and forall f in X exists! g in X g circ f = f circ g = e) (Exists single neutral and inverse element). Based on this theorem I would like to introduce two more definitions with new notations for neutral element and inverse element. First definition is forall G - group e_G in X and forall f in X f circ e_G = e_G circ f = f. Second definition is forall G - group forall f in X inv(f) in X and inv(f) circ f = f circ inv(f) = e_G. Can I do that in lean? Second question: what first material should I start from? I saw Natural Number Game recommended.

[Alexander Belov]

On a second thought I think I might want to postpone knowing how to make definitions in Lean. I will be more than happy if you teach me how to use the existing group definition. I would like to prove that if G is a group then the following cancellation law holds: forall x,y,z in X x circ z = y circ z => x circ y.

[Sky Wilshaw]

Here's some example code defining a group.

import Std

/-- A type `G` is called a `Group` if it has the following data and proofs. -/
class Group (G : Type _) where
  /-- The identity element `e`. -/
  e : G
  /-- The composition of two group elements. -/
  circ : G → G → G
  /-- Associativity. -/
  assoc : circ (circ f g) h = circ f (circ g h)
  /-- Left identity. -/
  e_circ : circ e f = f
  /-- Right identity. -/
  circ_e : circ f e = f
  /-- The inverse operation. -/
  inv : G → G
  /-- Left inverse. -/
  circ_inv_left : circ (inv f) f = e
  /-- Right inverse. -/
  circ_inv_right : circ f (inv f) = e

-- Note: closure is implicit as `circ : G → G → G`.

[Sky Wilshaw]

I made inv a function instead of an existential so that it's easier to work with. Generally if you have something of the form "there exists a unique x such that y", it's better to just store x as data and y as a proof about x.

[Sky Wilshaw]

Here's an example of a proof of the cancellation law with Mathlib's definition of a group (not the one I just gave).

import Mathlib.Algebra.Group.Defs

example {G : Type _} [Group G] (x y z : G) (hx : x * z = y * z) : x = y :=
  by rw [← mul_one x, ← mul_right_inv z, ← mul_assoc, hx, mul_assoc, mul_right_inv, mul_one]

There are quicker ones but this just shows you each step in the process quite clearly.

[Alexander Belov]

How does a proof look like as a sequence of rw's? Also, I'm a little bit confused why there is no forall quantifier for f inside the definition of properties for group G.

[Dan Velleman]

Here is essentially the same proof, rewritten as a calculational proof.

example {G : Type _} [Group G] (x y z : G) (hx : x * z = y * z) : x = y :=
  calc x
    _ = x * 1 := (mul_one x).symm
    _ = x * (z * z⁻¹) := by rw [mul_right_inv]
    _ = (x * z) * z⁻¹ := by rw [mul_assoc]
    _ = (y * z) * z⁻¹ := by rw [hx]
    _ = y * (z * z⁻¹) := by rw [mul_assoc]
    _ = y * 1 := by rw [mul_right_inv]
    _ = y := mul_one y

[Alexander Belov]

Okay, why there is no forall quantifier for f,g,h inside associativity, identity and inverse properties of Group G?

[Martin Dvořák]

Is it autoImplicit?
[somebody please clarify; I turn autoImplicit off in all my projects]

PS: In the examples (as well as in all theorems and lemmas) all terms before : are forall-quantified.
For example lemma foo (c : Char) : something and lemma foo : ∀ c : Char, something are equivalent.
They behave identically on the outside.
However, in their proofs, the former start with c already in the context.

[Alexander Belov]

Even in the two examples provided x y z are being used without forall quantifier. Has it always been like that in lean? I think I remember seeing forall quantifiers several years ago.

[Notification Bot]

Alexander Belov has marked this topic as resolved.

[Dan Velleman]

The same things happens in informal mathematics written for humans. You could state the theorem in the example above in two ways:

1. Let G be a group, and let x, y, and z be elements of G such that x * z = y * z. Then x = y.
   The proof would be essentially as above.

2. Let G be a group. Then for all x, y, and z in G, if x * z = y * z then x = y.
   You would probably start the proof with "Let x, y, and z be arbitrary elements of G and suppose x * z = y * z." The rest of the proof would be as above.
   You can do it either way in Lean.

[Notification Bot]

Alexander Belov has marked this topic as unresolved.

[Alexander Belov]

Okay, what still confuses me a little bit is why elements f,g,h are omitted in the beginning of assoc property. Should not it look like assoc : (f g h : G) : (circ f g) h = circ f (circ g circ h)?

[Alexander Belov]

import Std
import Mathlib.Algebra.Group.Defs

/-- A type `G` is called a `Group` if it has the following data and proofs. -/
class MyGroup (G : Type _) where
  /-- The identity element `e`. -/
  e : G
  /-- The composition of two group elements. -/
  circ : G → G → G
  /-- Associativity. -/
  assoc (f g h : G) : circ (circ f g) h = circ f (circ g h)
  /-- Left identity. -/
  e_circ (f : G) : circ e f = f
  /-- Right identity. -/
  circ_e (f : G) : circ f e = f
  /-- The inverse operation. -/
  inv : G → G
  /-- Left inverse. -/
  circ_inv_left (f : G) : circ (inv f) f = e
  /-- Right inverse. -/
  circ_inv_right (f : G) : circ f (inv f) = e

[Alexander Belov]

This seems to work.

[Notification Bot]

Alexander Belov has marked this topic as resolved.

[Junyan Xu]

Okay, what still confuses me a little bit is why elements f,g,h are omitted in the beginning of assoc property. Should not it look like assoc : (f g h : G) : (circ f g) h = circ f (circ g circ h)?

I think this is the "autoImplicit" feature mentioned by Martin. Basically, Lean automatically universally quantifies over all free variables (which humans also do in informal math).

[Notification Bot]

Alexander Belov has marked this topic as unresolved.

[Alexander Belov]

How to show that (Z, +) , (Q/{0}, *) is a group and (N, +) is not in Lean?

[Notification Bot]

Alexander Belov has marked this topic as unresolved.

[Alex J. Best]

It depends how much you want to define yourself (are you happy using mathlib's definition of addition for example?

instance : MyGroup ℤ where
  e := 0
  circ := fun a b => a + b -- using mathlibs add which is a bit circular....
  assoc := sorry
  -- ... etc for the other fields

[Alexander Belov]

Yes, I just want to see examples how one does such things in Lean. Math library built ins are fine

[Kevin Buzzard]

Here's how to show that (Z,+) is a group in Lean:

import Mathlib.Tactic

example : AddCommGroup ℤ := by
  infer_instance

Your question is far too imprecise to have a sensible answer. What do you mean by Z? What do you mean by addition on Z? You want to define these things yourself or use mathlib's definition? The proof that addition on Z is associative is a horrible 8 case case split because Z is defined in a really horrible way in mathlib as the disjoint union of two copies of the naturals.

Let me turn the question on its head. Say you read in a textbook the question "prove that (Z,+) is a group." What would you write? I'm pretty sure that whatever you write can be translated into Lean but this question is far more ill-posed than I suspect you think.

[Alexander Belov]

Okay, got that. Too early for questions like that.