## 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,
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

Yes !

#### 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):

@[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: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

λ ⟨x1, y1⟩ ⟨x2, y2⟩, ⟨x1 + x2, y1 + y2⟩

def add_good (z w : ℂ) : ℂ := ⟨z.re + w.re, z.im + w.im⟩

@[priority 100]

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

section good

@[priority 100000] -- new addition will be used instead of old one

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
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