Zulip Chat Archive

Stream: new members

Topic: make a group


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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 17:46):

You could just ask for a: units R

view this post on Zulip orlando (Mar 21 2020 at 17:47):

Yes !

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 17:47):

In your definition

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 17:47):

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

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 17:48):

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 17:49):

You need to prove an ext lemma for your structure

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

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

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 17:51):

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

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 17:52):

Take a look at the ext lemma for units. There is something interesting going on there

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

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

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 17:54):

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 17:56):

Your namespace is agl_1 but your structure is AGL_1

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 17:57):

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

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 17:59):

begin exact X end can just be shortened to X

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

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

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

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

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

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

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

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

view this post on Zulip orlando (Mar 21 2020 at 18:34):

hum ,it's because i put y2y1y_2 y_1 ?

view this post on Zulip Patrick Massot (Mar 21 2020 at 18:35):

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

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

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

view this post on Zulip Patrick Massot (Mar 21 2020 at 18:36):

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

view this post on Zulip orlando (Mar 21 2020 at 18:37):

Ok Patrick ! Thx !!!

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

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

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

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

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

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

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

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

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

view this post on Zulip Patrick Massot (Mar 21 2020 at 20:33):

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

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

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

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