groups

Stream: lean4

[learnerofmaths]

Hello, I am trying to define groups in lean4 to get a sense of what it would mean to use a theorem prover for work. Here is how far I have gotten:

section groupdefs

class One (α : Type u) where
  one : α

class Inv (α : Type u) where
  inv : α → α

class Mul (G : Type u) where
  mul : G → G

-- Set up notation typeclass using `extends`.
class has_group_notation (G : Type u) extends Mul G, One G, Inv G

-- definition of the group structure
class group (G : Type u) extends has_group_notation G where
  mul_assoc (a b c : G) : a * b * c = a * (b * c)

But I am having issues here since I keep getting an error "(kernel) declaration has metavariables 'mygroup.group.mk'Lean 4" . Does anyone know what's happening? Is this the right way to start defining one's own definition of a group?
Best!

[Mario Carneiro]

I get an error on class Mul saying that Mul is already declared. What version of lean 4 are you using?

[Mario Carneiro]

You need to use the Mul declared in the core library if you want to get the * notation, or declare your own * notation in terms of your Mul

[Mario Carneiro]

Here's a version using the classes from core:

class abbrev One (α : Type u) := OfNat α 1

class Inv (α : Type u) where
  inv : α → α

-- Set up notation typeclass using `extends`.
class has_group_notation (G : Type u) extends Mul G, One G, Inv G

-- definition of the group structure
class group (G : Type u) extends has_group_notation G where
  mul_assoc (a b c : G) : a * b * c = a * (b * c)

[learnerofmaths]

Sorry about that you need a custom namespace. I missed that

namespace mygroup

-- definitions of the group classes

section groupdefs

class One (α : Type u) where
  one : α

class Inv (α : Type u) where
  inv : α → α

class Mul (G : Type u) where
  mul : G → G

-- Set up notation typeclass using `extends`.
class has_group_notation (G : Type u) extends Mul G, One G, Inv G

-- definition of the group structure
class group (G : Type u) extends has_group_notation G where
  mul_assoc (a b c : G) : a * b * c = a * (b * c)

The version of lean is "leanprover/lean4:4.0.0"

[learnerofmaths]

I see thank you!

[learnerofmaths]

Mario Carneiro said:

You need to use the Mul declared in the core library if you want to get the * notation, or declare your own * notation in terms of your Mul

Thank you!

[learnerofmaths]

section groupdefs

class abbrev One (α : Type u) := OfNat α 1

class Inv (α : Type u) where
  inv : α → α

-- Set up notation typeclass using `extends`.
class has_group_notation (G : Type u) extends Mul G, One G, Inv G

-- definition of the group structure
class group (G : Type u) extends has_group_notation G where
  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

Now almost works. But I get a strange error with using \^-1. "expected termLean 4" Screen-Shot-2021-05-19-at-7.20.50-PM.png

[Mario Carneiro]

Just like Mul, Inv doesn't itself come with any notation, especially since it was just defined

[Mario Carneiro]

notation a "⁻¹" => Inv.inv a

[learnerofmaths]

ah! Ok, starting to get the hang of that.

[learnerofmaths]

makes sense.

[Mario Carneiro]

One does work because it is abbreviating the class OfNat A 1 that is used to resolve the meaning of 1 : A

[learnerofmaths]

I see. But why is 1 not considered a type of "notation" but rather a class?

[Mario Carneiro]

Just like inv and mul, there is a notation that says that number literals are defined to be OfNat.ofNat A n where OfNat is a class

[Mario Carneiro]

it's defined somewhere in the core library and it's a bit more complicated because it has to match on number literals

[learnerofmaths]

So something like notation "1" => OfNat.ofNat 1 (This is wrong, but something like this?) ? But my 1 has nothing to do with natural numbers, right? It's just notation?

[Mario Carneiro]

Conceptually that's what it is doing, yes

[Mario Carneiro]

there are an infinite number of such notations that have to be declared though so it is written in a more complicated way

[Mario Carneiro]

the actual code is here. It is using the more low level interface that notation desugars into

[Mario Carneiro]

it's probably unreadable but you can see OfNat.ofNat getting referenced

[learnerofmaths]

Alright. Sometimes the easiest things are so fundamental they are complicated. Off to prove some theorems and excited to learn lean : )

[learnerofmaths]

Hello again, I am trying to prove some properties of groups. But I am getting hung up on various syntax issues. Here is my initial definition

-- We're overwriting inbuilt group theory here so we always work in
-- a namespace
namespace mygroup

-- definitions of the group classes
section groupdefs

-- Notation for One done in an odd way
class abbrev One (α : Type u) := OfNat α 1

-- define inverse class and notation
class Inv (α : Type u) where
  inv : α → α

notation a "⁻¹" => Inv.inv a

-- Set up notation typeclass using `extends` for define classes
class has_group_notation (G : Type u) extends Mul G, One G, Inv G

-- definition of the group structure
class group (G : Type u) extends has_group_notation G where
  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


export group (mul_assoc one_mul mul_left_inv )

-- example of abelian group
class comm_group (G : Type u) extends group G where
  mul_comm (a b : G) : a * b = b * a
end groupdefs

namespace group


theorem inv_mul_cancel_left [group G] (a b : G) : a⁻¹ * (a * b) = b := by
  have a⁻¹ * (a * b) = (a⁻¹ * a) * b := by rw [mul_assoc]
  have (a⁻¹ * a) = 1 := by rw [mul_left_inv]
  have 1 * b = b := by rw [one_mul]

end group

end mygroup

1. the first issue is that [group G ] (a b : G) is not valid while [group α ] (a b : α ) why this statement sensitive to Unicode greek letters? I get an "unknown identifier 'G'".

2. My next issue is that I am not sure how to tell lean to complete a proof when I replace G with α:

theorem inv_mul_cancel_left [group α ] (a b : α ) : a⁻¹ * (a * b) = b := by
  have a⁻¹ * (a * b) = (a⁻¹ * a) * b := by rw [mul_assoc]
  have (a⁻¹ * a) = 1 := by rw [mul_left_inv]
  have 1 * b = b := by rw [one_mul]

Gives a bunch of errors that I attached.

Thank your help. Screen-Shot-2021-05-23-at-6.25.54-PM.png

[Alex J. Best]

Mac said:

Kevin Buzzard said:

I'm on today's nightly.

example : ∀ (x : Prop), x ↔ x ↔ x := sorry -- compiles
example : ∀ (A : Prop), A ↔ A ↔ A := sorry -- fails on third A
example : ∀ (A : Prop), a ↔ a ↔ a := sorry -- compiles?!

This is because it is being parsed as Mario Carneiro showed and then the unbound lowercase latin letters are being auto bound as specified in https://leanprover.github.io/lean4/doc/autobound.html

I'm guessing you are seeing this behaviour and you need to add {G : Type u} to have it work

[learnerofmaths]

I checked it out. I tried that change and a different error happened. I attached it. Screen-Shot-2021-05-23-at-11.17.43-PM.png

[Scott Morrison]

Please post code blocks (ideally as #mwe), rather than screenshots! You'll get much more help. :-)

[Yakov Pechersky]

You need {G : Type u} [group G] (a b : G)

[Yakov Pechersky]

We first postulate an arbitrary type G, then postulate that it has a group structure, then say "let a and b be terms of G"

[learnerofmaths]

ahhh! I see that. Makes total sense @Yakov Pechersky . Now I get some of others with

-- We're overwriting inbuilt group theory here so we always work in
-- a namespace
namespace mygroup

-- definitions of the group classes
section groupdefs

-- Notation for One done in an odd way
class abbrev One (α : Type u) := OfNat α 1

-- define inverse class and notation
class Inv (α : Type u) where
  inv : α → α

notation a "⁻¹" => Inv.inv a

-- Set up notation typeclass using `extends` for define classes
class has_group_notation (G : Type u) extends Mul G, One G, Inv G

-- definition of the group structure
class group (G : Type u) extends has_group_notation G where
  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


export group (mul_assoc one_mul mul_left_inv )

-- example of abelian group
class comm_group (G : Type u) extends group G where
  mul_comm (a b : G) : a * b = b * a
end groupdefs

namespace group


theorem inv_mul_cancel_left {G : Type u} [group G] (a b : G) : a⁻¹ * (a * b) = b := by
  have a⁻¹ * (a * b) = (a⁻¹ * a) * b := by rw [mul_assoc]
  have (a⁻¹ * a) = 1 := by rw [mul_left_inv]
  have 1 * b = b := by rw [one_mul]

end group

end mygroup

I get two instances of "failed to synthesize instance OfNat G 1" and I can't seem to tell lean that I have proved the theorem.

Thanks for the tip @Scott Morrison ! : )

[Eric Wieser]

You haven't proved the theorem, you've proved three intermediate results without joining them together

[Eric Wieser]

Adding rw this after each have probably resolves that

[Kevin Buzzard]

Your first comment in the code is not correct. Lean 4 does not have inbuilt groups

[learnerofmaths]

Hi, @Kevin Buzzard I was referring to https://github.com/leanprover/lean4/blob/master/tests/lean/run/alg.lean and https://github.com/leanprover/lean4/blob/master/tests/lean/run/alg.lean . But these appear as tests, so I will remove that comment.

[Kevin Buzzard]

If you import Mathlib.Algebra.Group.Defs from mathlib4 you can have groups :-)

[learnerofmaths]

@Eric Wieser , awesome. But I still get "failed to synthesize instance OfNat G 1" and red squiggly lines under the ones ('1'). Have you seen that before?

Do you happen to know what "rw this" means? Is there another way without rw this? My understanding was that for lean3 there was something called 'calc' and you could write proofs using chains of implications that looked like:

calc a⁻¹ * (a * b) = (a⁻¹ * a) * b : by rw mul_assoc
...  (a⁻¹ * a) * b : by  rw mul_left_inv
...  1 * b = b :  by rw one_mul

Here's the current code so far. Thank you for getting me on board.

-- 'If you import Mathlib.Algebra.Group.Defs from mathlib4 you can have groups :-)' ~ Kevin Buzzard
-- To get the swing of things built everything here
namespace mygroup

-- definitions of the group classes
section groupdefs

-- Notation for One done in an odd way
class abbrev One (α : Type u) := OfNat α 1

-- define inverse class and notation
class Inv (α : Type u) where
  inv : α → α

notation a "⁻¹" => Inv.inv a

-- Set up notation typeclass using `extends` for define classes
class has_group_notation (G : Type u) extends Mul G, One G, Inv G

-- definition of the group structure
class group (G : Type u) extends has_group_notation G where
  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


export group (mul_assoc one_mul mul_left_inv )

-- example of abelian group
class comm_group (G : Type u) extends group G where
  mul_comm (a b : G) : a * b = b * a
end groupdefs

namespace group


theorem inv_mul_cancel_left {G : Type u} [group G] (a b : G) : a⁻¹ * (a * b) = b := by
  have a⁻¹ * (a * b) = (a⁻¹ * a) * b := by rw [mul_assoc]
  rw this
  have (a⁻¹ * a) = 1 := by rw [mul_left_inv]
  rw this
  have 1 * b = b := by rw [one_mul]
  rw this

end group

end mygroup

Screen-Shot-2021-05-24-at-9.14.17-AM.png

[Eric Wieser]

have some_statement := sorry is short for have this : some_statement := sorry, meaning "prove some_statement and put the proof in a hypothesis called this" (at least, it is in lean3 and I assume it hasn't changed in lean 4).

[Eric Wieser]

Someone else who actually knows lean4 will have to help you with your ofNat problem

[Eric Wieser]

The calc proof you show there doesn't work in lean3 either though - an= is in the wrong place

[Kevin Buzzard]

Check out Mathlib.Algebra.Group.Defs for how to do 1 in Lean 4.

[learnerofmaths]

I see @Eric Wieser . I am very new to lean. I saw that notation used elsewhere. I have also seen

theorem inv_mul_cancel_left (a b : G) : a⁻¹ * (a * b) = b :=
by rw [← mul_assoc, mul_left_inv, one_mul]

Is the above version with the "have" and "rw this" the same? What is "← " doing here? I am happy to look at documentation just not sure what to search for. Are there names for these different styles?

[Ruben Van de Velde]

rw mul_assoc rewrites a * b * c to a * (b * c); rw ←mul_assoc rewrites a * (b * c) to a * b * c

[learnerofmaths]

@Kevin Buzzard I tried your suggestion. But I get unknown identifier 'nat_lit'Lean 4

-- 'If you import Mathlib.Algebra.Group.Defs from mathlib4 you can have groups :-)' ~ Kevin Buzzard
-- To get the swing of things built everything here

namespace mygroup

-- definitions of the group classes
section groupdefs

-- -- Notation for One done in an odd way
-- class abbrev One (α : Type u) := OfNat α 1
class One (α : Type u) where
  one : α

instance [One α] : OfNat α (nat_lit 1) where
  ofNat := One.one


-- define inverse class and notation
class Inv (α : Type u) where
  inv : α → α

notation a "⁻¹" => Inv.inv a

-- Set up notation typeclass using `extends` for define classes
class has_group_notation (G : Type u) extends Mul G, One G, Inv G

-- definition of the group structure
class group (G : Type u) extends has_group_notation G where
  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


export group (mul_assoc one_mul mul_left_inv )

-- example of abelian group
class comm_group (G : Type u) extends group G where
  mul_comm (a b : G) : a * b = b * a
end groupdefs

namespace group


theorem inv_mul_cancel_left {G : Type u} [group G] (a b : G) : a⁻¹ * (a * b) = b := by
  have intial_assumption : a⁻¹ * (a * b) = (a⁻¹ * a) * b := by rw [mul_assoc]
  rw intial_assumption
  have (a⁻¹ * a) = 1 := by rw [mul_left_inv]
  rw this
  have 1 * b = b := by rw [one_mul]
  rw this

end group

end mygroup

[Julian Berman]

I think that'll mean your lean4 is too old -- what does lean --version say? (Or just update to a more recent one). nat_lit used to be called natLit!.

[learnerofmaths]

Hi @Julian Berman . My current version of lean is

group_theory$ lean --version
Lean (version 4.0.0-m2, commit 26dda3f63d88, Release)

[Julian Berman]

Hello -- yeah natLit! got renamed about 10 days after that -- you should probably stick to the version of Lean that mathlib4 itself uses if you're going to use things from it

[Julian Berman]

which according to https://github.com/leanprover-community/mathlib4/blob/master/leanpkg.toml#L4 is leanprover/lean4:nightly-2021-05-18

[learnerofmaths]

Ah, cool! Changing to natLit! fixed it. But I will see about updating, too!

[learnerofmaths]

Thank you all!! Off to prove more theorems. Your help is really appreciated. Have a good day everyone.

[Jakob von Raumer]

To add what the others were saying: At some point we will surely have a calc and conv environment in Lean 4, they're not implemented yet, though.

[Alex J. Best]

Sebastian wrote a version of calc in a thread here: (maybe there was another one in a thread too)
Sebastian Ullrich said:

Here's one solution for a heterogeneous calc based on a Trans typeclass and ... as a term notation:

class Trans (r : α → β → Prop) (s : β → γ → Prop) (t : outParam (α → γ → Prop)) where
  trans {a b c} : r a b → s b c → t a c

export Trans (trans)

instance (r : α → γ → Prop) : Trans Eq r r where
  trans heq h' := heq ▸ h'

instance (r : α → β → Prop) : Trans r Eq r where
  trans h' heq := heq ▸ h'

notation "..." => _
-- enforce indentation of calc steps so we know when to stop parsing them
syntax calcStep := colGe term " := " term
syntax "calc " withPosition(calcStep+) : term

macro_rules
  | `(calc $p:term := $h:term) => `(($h : $p))
  | `(calc $p:term := $h:term $rest:calcStep*) => `(trans _ _ _ ($h : $p) (calc $rest:calcStep*))

variable (t1 t2 t3 t4 : Nat)
variable (pf12 : t1 = t2) (pf23 : t2 = t3) (pf34 : t3 = t4)

theorem foo : t1 = t4 :=
 calc
   t1 = t2 := pf12
   ... = t3 := pf23
   ... = t4 := pf34

variable (t5 : Nat)
variable (pf23' : t2 < t3) (pf45' : t4 < t5)

instance [HasLess α] : Trans (α := α) Less Less Less where
  trans := sorry

theorem foo' : t1 < t5 :=
 calc
   t1 = t2 := pf12
   ... < t3 := pf23'
   ... = t4 := pf34
   ... < t5 := pf45'