make a group

Stream: new members

[orlando]

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]

You could just ask for a: units R

[orlando]

Yes !

[Kevin Buzzard]

In your definition

[Kevin Buzzard]

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

[orlando]

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]

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

[Kevin Buzzard]

You need to prove an ext lemma for your structure

[Kevin Buzzard]

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]

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]

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]

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

[orlando]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

A term of type units R is a and b and a proof that ab=1 and a proof that ba=1

[Kevin Buzzard]

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

[Kevin Buzzard]

Your namespace is agl_1 but your structure is AGL_1

[Kevin Buzzard]

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

[Kevin Buzzard]

begin exact X end can just be shortened to X

[orlando]

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]

Yes sure, but after you write begin exact mul_one 1 end you can just change it to mul_one 1 :-)

[Kevin Buzzard]

begin end and by turns Lean from term mode into tactic mode; exact turns Lean from tactic mode into term mode.

[Patrick Massot]

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]

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]

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]

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]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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

[orlando]

Ok Patrick ! Thx !!!

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

Note you can write by ext ; AGL_ring to save some space.