# Zulip Chat Archive

## Stream: new members

### Topic: make a group

#### orlando (Mar 21 2020 at 17:44):

Hello,

I try to construct a group, and i have a problem i don't understand what i have to do :D

import algebra.category.CommRing.basic import algebra.ring /-- ## This is the groupe AGL_1(R) : x ↦ ax + b invertible i.e with a inveritible ! The goal is to make ## into a groupe for composition ! -/ structure AGL_1 ( R : Type) [comm_ring R] := mk {} :: (a b : R) (y : R) (certif : a * y = 1) namespace agl_1 section parameters (R : Type)[comm_ring R] def one : AGL_1(R) := {a := 1 ,b:=0, y := 1,certif := begin exact mul_one 1 end} instance : has_one (AGL_1 R) := ⟨one⟩ def of (r : R) : AGL_1(R) := {a := 1, b := r, y := 1,certif := begin exact mul_one 1, end} lemma one_eq_of_one : one = of (0) := rfl protected def mul_map' : AGL_1(R) → AGL_1 (R) → AGL_1(R) := λ ⟨a1,b1,y1,certif_1⟩ ⟨a2,b2,y2,certif_2⟩, begin have certif_ : (a1 * a2) * (y2 * y1) = 1, rw ← mul_assoc (a1 * a2) y2 y1, rw mul_assoc a1 a2 y2, rw certif_2, rw mul_one, rw certif_1, exact {a := a1 * a2, b := a1 * b2 + b1, y := y2 * y1 , certif := certif_}, end instance : inhabited (AGL_1 R) := ⟨1⟩ instance : has_mul (AGL_1 R) := ⟨mul_map'⟩ protected def mul_inv : AGL_1 R → AGL_1 R := λ ⟨a,b,y,certif⟩, begin exact {a := y, b:= -y * b , y := a , certif := begin rw mul_comm at certif, assumption end } end instance : has_inv (AGL_1 R) := ⟨ mul_inv⟩ def Rotation (R : Type)[comm_ring R] (a : R) (y : R): ( a * y = 1 ) → AGL_1(R) := λ certif, begin exact {a := a, b := 0, y := y, certif := certif}, end def mul_one' : ∀ g : AGL_1 R, g * 1 = g := λ ⟨a1,b1,y1,certif_1⟩, begin --- i thinck it's ok g * 1 cause has_instance mul ! have certif_a : a1 * 1 = a1, exact mul_one a1, have certif_b : a1 * 0 + b1 = b1, rw [mul_zero,zero_add], have certif_y : 1 * y1 = y1, exact one_mul y1, have certif_certif : (a1 * 1) * (1 * y1) = a1 * y1, rw [mul_one,one_mul], sorry, --- I don't know what i have to do :D end end end agl_1

#### Kevin Buzzard (Mar 21 2020 at 17:46):

You could just ask for a: units R

#### orlando (Mar 21 2020 at 17:47):

Yes !

#### Kevin Buzzard (Mar 21 2020 at 17:47):

In your definition

#### Kevin Buzzard (Mar 21 2020 at 17:47):

I'm not at a computer right now, what is the goal you're stuck on?

#### orlando (Mar 21 2020 at 17:48):

1 goal R : Type, _inst_1 : comm_ring R, _x : AGL_1 R, _fun_match : ∀ (_a : AGL_1 R), _a * 1 = _a, a1 b1 y1 : R, certif_1 : a1 * y1 = 1, certif_a : a1 * 1 = a1, certif_b : a1 * 0 + b1 = b1, certif_y : 1 * y1 = y1, certif_certif : a1 * 1 * (1 * y1) = a1 * y1 ⊢ {a := a1, b := b1, y := y1, certif := certif_1} * 1 = {a := a1, b := b1, y := y1, certif := certif_1} << --- Here Kevin,

#### Kevin Buzzard (Mar 21 2020 at 17:48):

You know that all these basic ring theory equalities can be proved with the `ring`

tactic?

#### Kevin Buzzard (Mar 21 2020 at 17:49):

You need to prove an `ext`

lemma for your structure

#### Kevin Buzzard (Mar 21 2020 at 17:50):

I am on my phone at the minute so it's difficult for me to give precise links but take a look at data.conplex.basic in mathlib

#### orlando (Mar 21 2020 at 17:50):

For ring : Yes i know but here calculus are not too complicated so i do by hand for fun !

Ah ok, ext is the equality of two elements of the structure !

#### Kevin Buzzard (Mar 21 2020 at 17:51):

If my memory is correct, very soon after the definition of a complex number they prove that if two complex numbers have the same real and imaginary part then they are equal

#### Kevin Buzzard (Mar 21 2020 at 17:51):

If you apply the ext lemma then you will immediately get a bunch of trivial goals

#### orlando (Mar 21 2020 at 17:52):

Your memory is good !

@[ext] theorem ext : ∀ {z w : ℂ}, z.re = w.re → z.im = w.im → z = w | ⟨zr, zi⟩ ⟨_, _⟩ rfl rfl := rfl

#### Kevin Buzzard (Mar 21 2020 at 17:52):

Take a look at the ext lemma for `units`

. There is something interesting going on there

#### Kevin Buzzard (Mar 21 2020 at 17:52):

If you find the definition of units in mathlib it is probably one of the first lemmas afterwards

#### Kevin Buzzard (Mar 21 2020 at 17:53):

The interesting thing here is that you only need some of the structure fields to be equal in order to reduce that the terms are equal

#### Kevin Buzzard (Mar 21 2020 at 17:54):

A term of type `units R`

is a and b and a proof that ab=1 and a proof that ba=1

#### Kevin Buzzard (Mar 21 2020 at 17:54):

But if two units have the same a, they are the same :-)

#### Kevin Buzzard (Mar 21 2020 at 17:56):

Your namespace is agl_1 but your structure is AGL_1

#### Kevin Buzzard (Mar 21 2020 at 17:57):

If you make them the same, then you will have access to "dot notation"

#### Kevin Buzzard (Mar 21 2020 at 17:59):

`begin exact X end`

can just be shortened to `X`

#### orlando (Mar 21 2020 at 18:15):

Yes i'm ok for the interesting thing !

For the shortened : the problem is if i don't write begin ... end, i d'ont see the goal in lean so i always start with begin end !

#### Kevin Buzzard (Mar 21 2020 at 18:23):

Yes sure, but after you write `begin exact mul_one 1 end`

you can just change it to ` mul_one 1`

:-)

#### Kevin Buzzard (Mar 21 2020 at 18:23):

`begin end`

and `by`

turns Lean from term mode into tactic mode; `exact`

turns Lean from tactic mode into term mode.

#### Patrick Massot (Mar 21 2020 at 18:26):

Orlando, you need the first lemma after the definition to be:

@[ext] lemma ext : ∀ {x y : AGL_1 R}, x.a = y.a → x.b = y.b → x = y := begin intros x y h h', cases x, cases y, congr ; try { assumption }, change x_a = y_a at h, rw h at x_certif, apply_fun (*) y_y at x_certif, rwa [← mul_assoc, mul_comm y_y, y_certif, one_mul, mul_one] at x_certif, end

#### Patrick Massot (Mar 21 2020 at 18:27):

Then, each time you need to prove equality of two elements of `AGL_1 R`

you'll be able to use the `ext`

tactic.

#### Patrick Massot (Mar 21 2020 at 18:28):

Next you need to get rid of `parameter`

. There is a very simple rule deciding whether you want `variables`

or `parameters`

: you want `variables`

.

#### Patrick Massot (Mar 21 2020 at 18:29):

Then your multiplication definition is wrong, for a very subtle reason. Using pattern matching from the beginning, you won't get that `(x*y).a = x.a*y.a`

*by definition* (in the very specific type theory sense of this word). This is will bring hell on you.

#### Kevin Buzzard (Mar 21 2020 at 18:31):

By "wrong" Patricks means that *mathematically* it is correct, but if two things are equal because of a theorem, this is far less convenient than if they are equal by definition.

#### orlando (Mar 21 2020 at 18:34):

hum ,it's because i put $y_2 y_1$ ?

#### Patrick Massot (Mar 21 2020 at 18:35):

No, it's because of your angle bracket pattern matching.

#### Patrick Massot (Mar 21 2020 at 18:36):

I cleaned up the beginning:

import algebra.category.CommRing.basic import algebra.ring import tactic /-- ## This is the groupe AGL_1(R) : x ↦ ax + b invertible i.e with a inveritible ! The goal is to make ## into a groupe for composition ! -/ structure AGL_1 ( R : Type) [comm_ring R] := (a b : R) (y : R) (certif : a * y = 1) namespace agl_1 section variables {R : Type} [comm_ring R] @[ext] lemma ext : ∀ {x y : AGL_1 R}, x.a = y.a → x.b = y.b → x = y := begin intros x y h h', cases x, cases y, congr ; try { assumption }, change x_a = y_a at h, rw h at x_certif, apply_fun (*) y_y at x_certif, rwa [← mul_assoc, mul_comm y_y, y_certif, one_mul, mul_one] at x_certif, end def one : AGL_1(R) := {a := 1, b:=0, y := 1, certif := mul_one 1} instance : has_one (AGL_1 R) := ⟨one⟩ def of (r : R) : AGL_1(R) := {a := 1, b := r, y := 1, certif := mul_one 1} lemma one_eq_of_one : one = of (0 : R) := rfl protected def mul_map' : AGL_1(R) → AGL_1 (R) → AGL_1(R) := λ x y, { a := x.a * y.a, b := x.a * y.b + x.b, y := x.y * y.y , certif := begin sorry -- too lazy to retype the proof with dot notations end} instance : inhabited (AGL_1 R) := ⟨1⟩ instance : has_mul (AGL_1 R) := ⟨agl_1.mul_map'⟩ protected def mul_inv : AGL_1 R → AGL_1 R := λ ⟨a,b,y,certif⟩, { a := y, b:= -y * b, y := a , certif := by rwa mul_comm at certif } instance : has_inv (AGL_1 R) := ⟨agl_1.mul_inv⟩ def Rotation (R : Type)[comm_ring R] (a : R) (y : R): ( a * y = 1 ) → AGL_1(R) := λ certif, {a := a, b := 0, y := y, certif := certif} def mul_one' : ∀ g : AGL_1 R, g * 1 = g := begin intros g, ext, { change g.a*1 = g.a, rw mul_one }, { change g.a*0 + g.b = g.b, simp } end end end agl_1

#### Patrick Massot (Mar 21 2020 at 18:36):

My advice is to very carefully compare, line by line, with your version. There are many small tricks to learn here.

#### Patrick Massot (Mar 21 2020 at 18:36):

I'm not saying anything about your global strategy, only locally cleaning things.

#### orlando (Mar 21 2020 at 18:37):

Ok Patrick ! Thx !!!

#### Kevin Buzzard (Mar 21 2020 at 18:44):

For technical reasons, `λ ⟨a1,b1,y1,certif_1⟩ ...`

is almost never right. I'm talking about `mul_map'`

. Mathematically what you and Patrick did is the same, but Patrick's version is better for Lean for computer-science reasons.

#### orlando (Mar 21 2020 at 18:45):

Ok if a understand, i need to use a.a a.b a.y etc and not bracket !

#### Kevin Buzzard (Mar 21 2020 at 18:46):

protected def mul_map' : AGL_1(R) → AGL_1 (R) → AGL_1(R) := λ x y, { a := x.a * y.a, b := x.a * y.b + x.b, y := x.y * y.y , certif := begin rw [(show x.a * y.a * (x.y * y.y) = (x.a * x.y) * (y.a * y.y), by ring), x.certif, y.certif, mul_one], end}

I filled in a sorry in a fairly efficient way

#### Kevin Buzzard (Mar 21 2020 at 18:47):

orlando said:

Ok if a understand, i need to use a.a a.b a.y etc and not bracket !

In your definitions, it is better.

#### Kevin Buzzard (Mar 21 2020 at 19:02):

import data.real.basic structure complex := (re : ℝ) (im : ℝ) notation `ℂ` := complex @[ext] theorem ext : ∀ {z w : ℂ}, z.re = w.re → z.im = w.im → z = w | ⟨zr, zi⟩ ⟨_, _⟩ rfl rfl := rfl def add_bad : ℂ → ℂ → ℂ := λ ⟨x1, y1⟩ ⟨x2, y2⟩, ⟨x1 + x2, y1 + y2⟩ def add_good (z w : ℂ) : ℂ := ⟨z.re + w.re, z.im + w.im⟩ section bad @[priority 100] instance : has_add ℂ := ⟨add_bad⟩ def add_bad_assoc (a b c : ℂ) : (a + b) + c = a + (b + c) := begin ext, -- what now? { cases a, cases b, cases c, show a_re + b_re + c_re = a_re + (b_re + c_re), ring, }, { cases a, cases b, cases c, change a_im + b_im + c_im = a_im + (b_im + c_im), ring, }, end end bad section good @[priority 100000] -- new addition will be used instead of old one instance complex.has_good_add : has_add ℂ := ⟨add_good⟩ def add_good_assoc (a b c : ℂ) : (a + b) + c = a + (b + c) := begin ext, { change a.re + b.re + c.re = a.re + (b.re + c.re), ring, }, { show a.im + b.im + c.im = a.im + (b.im + c.im), ring, }, end end good

There is one simple reason why using dot is better than using bracket: I don't have to do `cases`

lots of times in my proofs.

#### Johan Commelin (Mar 21 2020 at 19:03):

orlando said:

Yes i'm ok for the interesting thing !

For the shortened : the problem is if i don't write begin ... end, i d'ont see the goal in lean so i always start with begin end !

If you write `:= _`

, then you can see the goal if you put your cursor on the `_`

. This is a way to write things without `begin ... end`

. Just always keep a `_`

to the right of your cursor.

#### Kevin Buzzard (Mar 21 2020 at 19:03):

In fact with the good addition I can just do

def add_good_assoc (a b c : ℂ) : (a + b) + c = a + (b + c) := begin ext; apply add_assoc end

#### Kevin Buzzard (Mar 21 2020 at 19:05):

and this is very close to a way a mathematician thinks about the proof: "suffices to check on real and imaginary parts, where it follows from associativity of addition on the reals"

#### orlando (Mar 21 2020 at 20:10):

I do the associativity :grinning:

import algebra.category.CommRing.basic import algebra.ring import tactic /-- ## This is the groupe AGL_1(R) : x ↦ ax + b invertible i.e with a inveritible ! The goal is to make ## into a groupe for composition ! -/ structure AGL_1 ( R : Type) [comm_ring R] := (a b : R) (y : R) (certif : a * y = 1) namespace AGL_1 section variables {R : Type} [comm_ring R] @[ext] lemma ext : ∀ {g1 g2 : AGL_1 R}, g1.a = g2.a → g1.b = g2.b → g1 = g2 := λ g1 g2, --- it's ok ? just don't use Bracket ? begin intros h1 h2, cases g1, --- difficult i have to analyse ! cases g2, congr ; try { assumption }, change g1_a = g2_a at h1, rw h1 at g1_certif, apply_fun (*) g2_y at g1_certif, rwa [← mul_assoc, mul_comm g2_y, g2_certif, one_mul, mul_one] at g1_certif, end def one : AGL_1(R) := {a := 1, b:=0, y := 1, certif := mul_one 1} instance : has_one (AGL_1 R) := ⟨one⟩ def of (r : R) : AGL_1(R) := {a := 1, b := r, y := 1, certif := mul_one 1} lemma one_eq_of_one : one = of (0 : R) := rfl protected def mul_map' : AGL_1(R) → AGL_1 (R) → AGL_1(R) := λ g1 g2, { a := g1.a * g2.a, b := g1.a * g2.b + g1.b, y := g1.y * g2.y , certif := begin have H : g1.a * g2.a * (g1.y * g2.y) = (g1.a * g1.y) * (g2.a * g2.y), ring, rw H, rw [g1.certif,g2.certif], exact one_mul 1, end} instance : inhabited (AGL_1 R) := ⟨1⟩ instance : has_mul (AGL_1 R) := ⟨AGL_1.mul_map'⟩ lemma a_comp (g1 g2 : AGL_1 R) : (g1 * g2).a = g1.a * g2.a := rfl lemma b_comp (g1 g2 : AGL_1 R) : (g1 * g2).b = g1.a * g2.b + g1.b := rfl protected def mul_inv : AGL_1 R → AGL_1 R := λ ⟨a,b,y,certif⟩, --- change here ? { a := y, b:= -y * b, y := a , certif := by rwa mul_comm at certif } instance : has_inv (AGL_1 R) := ⟨AGL_1.mul_inv⟩ def Rotation (R : Type)[comm_ring R] (a : R) (y : R): ( a * y = 1 ) → AGL_1(R) := λ certif, {a := a, b := 0, y := y, certif := certif} def mul_one' : ∀ g : AGL_1 R, g * 1 = g := begin intros g, ext, { change g.a*1 = g.a, rw mul_one }, { change g.a*0 + g.b = g.b, simp } end def mul_assoc' (g1 g2 g3 : AGL_1 R) : (g1 * g2) * g3 = g1 * (g2 * g3) := begin ext, rw [a_comp,a_comp, a_comp g1 (g2 *g3), a_comp g2 g3, mul_assoc], rw [b_comp,a_comp,b_comp,b_comp,b_comp], ring, end end end AGL_1

#### Patrick Massot (Mar 21 2020 at 20:33):

I didn't notice earlier, but you have definitions that should be lemmas.

#### Kevin Buzzard (Mar 21 2020 at 20:33):

I think `a_comp`

and `b_comp`

should be simp lemmas. See if you can train simp to solve some of these things. And you should now make a group instance for your structure I guess

#### Patrick Massot (Mar 21 2020 at 20:40):

Going a bit along the Kevin-like automation path can be a fun path too. Have a look at:

lemma one_a : (1 : AGL_1 R).a = 1 := rfl lemma one_b : (1 : AGL_1 R).b = 0 := rfl lemma a_comp (g1 g2 : AGL_1 R) : (g1 * g2).a = g1.a * g2.a := rfl lemma b_comp (g1 g2 : AGL_1 R) : (g1 * g2).b = g1.a * g2.b + g1.b := rfl meta def AGL_ring : tactic unit := `[simp only [one_a, one_b, a_comp, b_comp], ring] run_cmd add_interactive [`AGL_ring] lemma mul_one' (g : AGL_1 R) : g * 1 = g := begin ext ; AGL_ring, end lemma mul_assoc' (g1 g2 g3 : AGL_1 R) : (g1 * g2) * g3 = g1 * (g2 * g3) := begin ext ; AGL_ring, end

#### Patrick Massot (Mar 21 2020 at 21:13):

Note you can write `by ext ; AGL_ring`

to save some space.

Last updated: May 13 2021 at 17:42 UTC